Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.summable_one_div_two_pi_sq_nat_add_one_sq

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2907 to 2919

Mathematical statement

Exact Lean statement

lemma summable_one_div_two_pi_sq_nat_add_one_sq :
    Summable fun n : ℕ ↦
      (1 : ℝ) / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma summable_one_div_two_pi_sq_nat_add_one_sq :    Summable fun n : ℕ ↦      (1 : ℝ) / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2) := by  have hp : Summable fun n : ℕ ↦ (1 : ℝ) / (n + 1 : ℝ) ^ 2 := by    simpa [one_div] using      ((summable_nat_add_iff 1).mpr        (Real.summable_one_div_nat_pow.mpr (by norm_num : 1 < 2)))  have hscale := hp.mul_left ((2 * Real.pi ^ 2)⁻¹)  convert! hscale using 1  ext n  have hden : 2 * Real.pi ^ 2 ≠ 0 := by positivity  have hn : (n + 1 : ℝ) ≠ 0 := by positivity  field_simp [hden, hn]