Source indexedtheorem · leanprover/lean4:v4.32.0

completedRiemannZeta₀_one_ne_zero

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:125 to 139

Source documentation

The entire completed zeta function Λ₀ is nonzero at 1.

This uses the Euler-Mascheroni formula for Λ₀(1) from ZetaAsymp, the lower bound 27 / 50 < γ, and an elementary numerical bound log (4π) < 127 / 50.

Exact Lean statement

theorem completedRiemannZeta₀_one_ne_zero :
    completedRiemannZeta₀ (1 : ℂ) ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem completedRiemannZeta₀_one_ne_zero :    completedRiemannZeta₀ (1 : ℂ) ≠ 0 := by  have hpos :      0 < (Real.eulerMascheroniConstant - Real.log (4 * Real.pi)) / 2 + 1 := by    have hγ : (27 / 50 : ℝ) < Real.eulerMascheroniConstant :=      twenty_seven_div_fifty_lt_eulerMascheroniConstant    have hlog : Real.log (4 * Real.pi) < 127 / 50 :=      log_four_mul_pi_lt_one_hundred_twenty_seven_div_fifty    linarith  have hreal :      ((Real.eulerMascheroniConstant - Real.log (4 * Real.pi)) / 2 + 1 : ℂ) ≠ 0 := by    exact_mod_cast ne_of_gt hpos  rw [completedRiemannZeta₀_one]  simpa [Complex.ofReal_log (by positivity : (0 : ℝ) ≤ 4 * Real.pi), sub_eq_add_neg,    add_assoc, add_left_comm, add_comm] using hreal