Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.multipliable_complex_inv_one_add

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:140 to 149

Mathematical statement

Exact Lean statement

lemma multipliable_complex_inv_one_add (r : ℝ) (hr : 1 < r) :
    Multipliable fun p : Nat.Primes => (1 + ((p : ℕ) : ℂ) ^ (-((r : ℝ) : ℂ)))⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma multipliable_complex_inv_one_add (r : ℝ) (hr : 1 < r) :    Multipliable fun p : Nat.Primes => (1 + ((p : ℕ) : ℂ) ^ (-((r : ℝ) : ℂ)))⁻¹ := by  have hu := multipliable_inv_one_add r hr  have hmap := hu.map Complex.ofRealHom Complex.continuous_ofReal  have h_eq :      (fun p : Nat.Primes => (1 + ((p : ℕ) : ℂ) ^ (-((r : ℝ) : ℂ)))⁻¹) =        (fun x : ℝ => (x : ℂ)) ∘ fun p : Nat.Primes => (1 + ((p : ℕ) : ℝ) ^ (-r))⁻¹ := by    funext p    exact cast_inv_one_add p r  simpa [h_eq, Function.comp_def] using hmap