Source indexedlemma · leanprover/lean4:v4.32.0

Backlund.zeta_zero_re_mem_of_im_pos

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:898 to 950

Source documentation

Zeros of ζ with positive imaginary part lie in the closed strip 0 ≤ Re ≤ 1. Right edge: riemannZeta_ne_zero_of_one_le_re (mathlib) forces Re < 1. Left edge: for Re s < 0 the functional equation riemannZeta_one_sub writes ζ(s) as a nonvanishing prefactor times sin (π s / 2) · Γ(1 - s) · ζ(1 - s); the last two factors are nonzero (Re (1 - s) > 1), and Complex.sin_eq_zero_iff forces s real, contradicting 0 < Im s. Needed to place all counted zeros inside the single ball B(0, T + 1).

Exact Lean statement

lemma zeta_zero_re_mem_of_im_pos {s : ℂ} (hs : riemannZeta s = 0) (him : 0 < s.im) :
    0 ≤ s.re ∧ s.re ≤ 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zeta_zero_re_mem_of_im_pos {s : ℂ} (hs : riemannZeta s = 0) (him : 0 < s.im) :    0 ≤ s.re ∧ s.re ≤ 1 := by  refine ⟨?_, ?_⟩  · by_contra hre    push Not at hre    set w : ℂ := 1 - s with hw    have hwre : 1 < w.re := by      rw [hw]      simp only [Complex.sub_re, Complex.one_re]      linarith    have hwn : ∀ n : ℕ, w ≠ -(n : ℂ) := by      intro n h      have h' := congrArg Complex.re h      simp only [Complex.neg_re, Complex.natCast_re] at h'      have hn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n      linarith    have hw1 : w ≠ 1 := by      intro h      have h' := congrArg Complex.re h      simp only [Complex.one_re] at h'      linarith    have hfe := riemannZeta_one_sub hwn hw1    have h1w : (1 : ℂ) - w = s := by      rw [hw]; ring    rw [h1w, hs] at hfe    have hζw : riemannZeta w ≠ 0 := riemannZeta_ne_zero_of_one_le_re hwre.le    have hΓ : Complex.Gamma w ≠ 0 := Complex.Gamma_ne_zero hwn    have h2π : ((2 : ℂ) * (Real.pi : ℂ)) ^ (-w) ≠ 0 := by      rw [Complex.cpow_def_of_ne_zero (by        simp only [ne_eq, mul_eq_zero, not_or]        exact ⟨two_ne_zero, by exact_mod_cast Real.pi_ne_zero⟩)]      exact Complex.exp_ne_zero _    have hprod := hfe.symm    simp only [mul_eq_zero] at hprod    have hcos : Complex.cos ((Real.pi : ℂ) * w / 2) = 0 := by      rcases hprod with ((((h | h) | h) | h) | h)      · norm_num at h      · exact absurd h h2π      · exact absurd h hΓ      · exact h      · exact absurd h hζw    rw [Complex.cos_eq_zero_iff] at hcos    obtain ⟨k, hk⟩ := hcos    have hπ : ((Real.pi : ℝ) : ℂ) ≠ 0 := by exact_mod_cast Real.pi_ne_zero    have h2 : (Real.pi : ℂ) * w = (Real.pi : ℂ) * (2 * (k : ℂ) + 1) := by      linear_combination 2 * hk    have hwk : w = 2 * (k : ℂ) + 1 := mul_left_cancel₀ hπ h2    have himw := congrArg Complex.im hwk    simp [hw] at himw    linarith  · by_contra hre    push Not at hre    exact riemannZeta_ne_zero_of_one_le_re hre.le hs