Source indexedlemma · leanprover/lean4:v4.32.0

Nat.Primes.multipliable_inv_one_add

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:130 to 138

Mathematical statement

Exact Lean statement

lemma multipliable_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_inv_one_add (r : ℝ) (hr : 1 < r) :    Multipliable fun p : Nat.Primes => (1 + ((p : ℕ) : ℝ) ^ (-r))⁻¹ := by  have hsum : Summable fun p : Nat.Primes => ((p : ℕ) : ℝ) ^ (-r) := by    rw [Nat.Primes.summable_rpow]    linarith  have hlog : Summable fun p : Nat.Primes => Real.log (1 + ((p : ℕ) : ℝ) ^ (-r)) :=    Real.summable_log_one_add_of_summable hsum  exact Real.multipliable_of_summable_log (fun _ => by positivity)    (by simpa [Real.log_inv, neg_mul] using hlog.neg)