Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.eulerFactor_two_mul

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:167 to 179

Mathematical statement

Exact Lean statement

lemma eulerFactor_two_mul (p : Nat.Primes) (s : ℂ) (hs : 1 < s.re) :
    (1 - ((p : ℕ) : ℂ) ^ (-(2 * s)))⁻¹ =
      (1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹ * (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eulerFactor_two_mul (p : Nat.Primes) (s : ℂ) (hs : 1 < s.re) :    (1 - ((p : ℕ) : ℂ) ^ (-(2 * s)))⁻¹ =      (1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹ * (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹ := by  set z := ((p : ℕ) : ℂ) ^ (-s)  have hz : ‖z‖ < 1 := norm_cpow_neg_lt_one p s hs  have hpow : ((p : ℕ) : ℂ) ^ (-(2 * s)) = z ^ 2 := by    simp only [z]    rw [show -(2 * s) = (2 : ℂ) * (-s) by ring,      show (2 : ℂ) * (-s) = ((2 : ℕ) : ℂ) * (-s) by norm_num, Complex.cpow_nat_mul]  calc    (1 - ((p : ℕ) : ℂ) ^ (-(2 * s)))⁻¹ = (1 - z ^ 2)⁻¹ := by rw [hpow]    _ = (1 - z)⁻¹ * (1 + z)⁻¹ := inv_one_sub_sq_eq_mul_inv_one_sub_one_add z hz    _ = (1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹ * (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹ := by simp [z]