riemannZeta_one_ne_zero — Mathlib

English

The value ζ(1) is nonzero: ζ(1) ≠ 0.

Русский

Значение ζ(1) отлично от нуля: ζ(1) ≠ 0.

LaTeX

$$$$ \zeta(1) \neq 0. $$$$

Lean4

/-- With Mathlib's particular conventions, we have `ζ 1 ≠ 0`. -/
theorem _root_.riemannZeta_one_ne_zero : riemannZeta 1 ≠ 0 := by
  -- This one's for you, Kevin.

  suffices (γ - (4 * π).log) / 2 ≠ 0 by
    simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π), push_cast]
  refine div_ne_zero (sub_lt_zero.mpr (lt_trans ?_ ?_ (b := 1))).ne two_ne_zero
  · exact Real.eulerMascheroniConstant_lt_two_thirds.trans (by norm_num)
  · rw [lt_log_iff_exp_lt (by positivity)]
    exact (lt_trans Real.exp_one_lt_d9 (by norm_num)).trans_le <| mul_le_mul_of_nonneg_left two_le_pi (by simp)

Похожие утверждения