Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.riemannZeta_ne_zero_of_real_neg

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:285 to 305

Source documentation

ζ does not vanish on the real segment (-1, 0]. (The non-trivial zeros lie in the critical strip and the trivial zeros are at -2, -4, …; ζ(0) = -1/2.) Reusable for the left edge / real point of the eq.(12) rectangle.

Exact Lean statement

lemma riemannZeta_ne_zero_of_real_neg {σ : ℝ} (h1 : -1 < σ) (h2 : σ ≤ 0) :
    riemannZeta ((σ : ℝ) : ℂ) ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma riemannZeta_ne_zero_of_real_neg {σ : ℝ} (h1 : -1 < σ) (h2 : σ ≤ 0) :    riemannZeta ((σ : ℝ) : ℂ) ≠ 0 := by  rcases lt_or_eq_of_le h2 with hlt | h0  · have hrw : ((σ : ℝ) : ℂ) = 1 - ((1 - σ : ℝ) : ℂ) := by push_cast; ring    rw [hrw]    refine riemannZeta_one_sub_ne_zero_of_one_le_re ?_ ?_    · simp only [Complex.ofReal_re]; linarith    · have harg : (↑Real.pi * ((1 - σ : ℝ) : ℂ) / 2) = ((Real.pi * (1 - σ) / 2 : ℝ) : ℂ) := by        push_cast; ring      rw [harg, ← Complex.ofReal_cos, Complex.ofReal_ne_zero, Real.cos_ne_zero_iff]      intro k hk      have hk2 : Real.pi * (1 - σ) = Real.pi * (2 * (k : ℝ) + 1) := by        have h2' : Real.pi * (1 - σ) / 2 = Real.pi * (2 * (k : ℝ) + 1) / 2 := by rw [hk]; ring        linarith      have heq : 1 - σ = 2 * (k : ℝ) + 1 := mul_left_cancel₀ Real.pi_ne_zero hk2      have hk_pos : (0 : ℝ) < (k : ℝ) := by linarith      have hk_lt : (k : ℝ) < 1 := by linarith      have : 0 < k := by exact_mod_cast hk_pos      have : k < 1 := by exact_mod_cast hk_lt      omega  · rw [h0, show ((0 : ℝ) : ℂ) = 0 by norm_num, riemannZeta_zero]; norm_num