Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.riemannZeta_one_sub_ne_zero_of_one_le_re

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:259 to 280

Source documentation

Shared functional-equation factorization: if 1 ≤ Re w and cos(π w / 2) ≠ 0, then the reflected value ζ(1 - w) is non-zero. (The factors 2, (2π)^{-w}, Γ(w), ζ(w) are all non-zero for Re w ≥ 1, so only the cosine factor can vanish.)

Exact Lean statement

lemma riemannZeta_one_sub_ne_zero_of_one_le_re {w : ℂ}
    (hw_re : 1 ≤ w.re) (hcos : Complex.cos (↑Real.pi * w / 2) ≠ 0) :
    riemannZeta (1 - w) ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma riemannZeta_one_sub_ne_zero_of_one_le_re {w : ℂ}    (hw_re : 1 ≤ w.re) (hcos : Complex.cos (↑Real.pi * w / 2) ≠ 0) :    riemannZeta (1 - w) ≠ 0 := by  have hw_neg_nat : ∀ n : ℕ, w ≠ -↑n := by    intro n hn    have hre' : w.re = -(n : ℝ) := by rw [hn]; simp    have : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n    rw [hre'] at hw_re; linarith  have hw_ne_one : w ≠ 1 := by    rintro rfl    refine hcos ?_    have h2 : (↑Real.pi * (1 : ℂ) / 2) = ((Real.pi / 2 : ℝ) : ℂ) := by push_cast; ring    rw [h2, ← Complex.ofReal_cos, Real.cos_pi_div_two, Complex.ofReal_zero]  have hpow : (2 * ↑Real.pi : ℂ) ^ (-w) ≠ 0 := by    rw [Complex.cpow_ne_zero_iff]; left    norm_num [Complex.ofReal_ne_zero, Real.pi_ne_zero]  have hGamma : Complex.Gamma w ≠ 0 := Complex.Gamma_ne_zero hw_neg_nat  have hzeta_w : riemannZeta w ≠ 0 := riemannZeta_ne_zero_of_one_le_re hw_re  have hfe := riemannZeta_one_sub (s := w) hw_neg_nat hw_ne_one  rw [hfe]  exact mul_ne_zero    (mul_ne_zero (mul_ne_zero (mul_ne_zero (by norm_num) hpow) hGamma) hcos) hzeta_w