Source indexedtheorem · leanprover/lean4:v4.32.0

completedRiemannZeta₀_two

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:84 to 98

Source documentation

The entire completed zeta function Λ₀ has value (π - 3) / 6 at 2.

Exact Lean statement

theorem completedRiemannZeta₀_two :
    completedRiemannZeta₀ (2 : ℂ) = ((Real.pi : ℂ) - 3) / 6

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem completedRiemannZeta₀_two :    completedRiemannZeta₀ (2 : ℂ) = ((Real.pi : ℂ) - 3) / 6 := by  have h := completedRiemannZeta_eq (2 : ℂ)  have h' :      completedRiemannZeta (2 : ℂ) + (1 : ℂ) / 2 + (1 : ℂ) / (1 - (2 : ℂ)) =        completedRiemannZeta₀ (2 : ℂ) := by    have := congrArg (fun x => x + (1 : ℂ) / 2 + (1 : ℂ) / (1 - (2 : ℂ))) h    simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using this  have h'' :      completedRiemannZeta₀ (2 : ℂ) =        completedRiemannZeta (2 : ℂ) + (1 : ℂ) / 2 + (1 : ℂ) / (1 - (2 : ℂ)) := by    simpa [add_assoc, add_left_comm, add_comm] using h'.symm  have hden : (1 : ℂ) / (1 - (2 : ℂ)) = (-1 : ℂ) := by norm_num  simpa [h'', completedRiemannZeta_two, hden] using (by ring :    (Real.pi : ℂ) / 6 + (1 : ℂ) / 2 + (-1 : ℂ) = ((Real.pi : ℂ) - 3) / 6)