LiTrivialZeros.lean

Declarations

Source

/-
NguyenRH1/LiTrivialZeros.lean — ii′-5e prep (deferred from ii′-5d,
D-067 §6): the trivial-zero simplicity zeroMult(−2n) = 1 for ALL n ≥ 1,
generalizing ii′-4c's `zeroMult_neg_two` (LiContour.lean).

Structure (mirrors ii′-4c):
* §1 `gamma_mul_prod`: the product-form Γ recurrence
  Γ(z)·∏_{j<n}(z+j) = Γ(z+n) for z avoiding {0,…,−(n−1)} — induction
  on `Complex.Gamma_add_one`;
* §2 the cofactor HfunT n s = 2·π^{−s/2}·Γ(s/2+n+1)/Q_n(s) with
  Q_n(s) = ∏_{j<n}(s/2+j): analytic and nonzero at −2n, and the
  punctured identity (s+2n)·ΓR(s) = HfunT n s on ball(−2n, 1) ∖ {−2n};
* §3 `zeroMult_neg_two_mul`: ζ(s) = (s+2n)·(Λ(s)/HfunT n s) near −2n
  with Λ/HfunT analytic nonzero (Λ(−2n) = Λ(1+2n) = ΓR(1+2n)ζ(1+2n) ≠ 0)
  ⟹ analyticOrderAt = 1 ⟹ zeroMult = 1.

Archive references: D-067 §6, journal-025/026, LiContour (ii′-4c).
-/
import Mathlib
import Zeta23.Statement
import Zeta23.RvM.CountByIntegral

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The product-form Γ recurrence -/

/-- Γ(z)·∏_{j<n}(z+j) = Γ(z+n) for z avoiding {0, −1, …, −(n−1)}
(the poles crossed by the iteration of `Complex.Gamma_add_one`). -/
theorem gamma_mul_prod (z : ℂ) (n : ℕ) (hz : ∀ k : ℕ, k < n → z ≠ -(k : ℂ)) :
    Complex.Gamma z * ∏ j ∈ Finset.range n, (z + (j : ℂ))
      = Complex.Gamma (z + (n : ℂ)) := by
  induction n with
  | zero => simp
  | succ m ih =>
    have hz' : ∀ k : ℕ, k < m → z ≠ -(k : ℂ) :=
      fun k hk => hz k (hk.trans (Nat.lt_succ_self m))
    have hlast : z + (m : ℂ) ≠ 0 := by
      intro hzero
      exact hz m (Nat.lt_succ_self m) (eq_neg_of_add_eq_zero_left hzero)
    rw [Finset.prod_range_succ]
    calc Complex.Gamma z * ((∏ j ∈ Finset.range m, (z + (j : ℂ))) * (z + (m : ℂ)))
        = (Complex.Gamma z * ∏ j ∈ Finset.range m, (z + (j : ℂ))) * (z + (m : ℂ)) := by
          ring
      _ = Complex.Gamma (z + (m : ℂ)) * (z + (m : ℂ)) := by rw [ih hz']
      _ = Complex.Gamma (z + ((m + 1 : ℕ) : ℂ)) := by
          rw [show z + ((m + 1 : ℕ) : ℂ) = (z + (m : ℂ)) + 1 by push_cast; ring,
            Complex.Gamma_add_one _ hlast]
          ring

/-! ## 2. The cofactor HfunT -/

/-- The partial denominator product Q_n(s) = ∏_{j<n} (s/2 + j). -/
def trivQ (n : ℕ) (s : ℂ) : ℂ := ∏ j ∈ Finset.range n, (s / 2 + (j : ℂ))

/-- The cofactor: HfunT n s = 2·π^{−s/2}·Γ(s/2+n+1)/Q_n(s). Equals
(s+2n)·ΓR(s) off the recurrence's bad set (HfunT_eq); analytic and
nonzero at −2n. The local factorization is ζ(s) = (s+2n)·(Λ(s)/HfunT n s). -/
noncomputable def HfunT (n : ℕ) (s : ℂ) : ℂ :=
  2 * (Real.pi : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2 + (n : ℂ) + 1) / trivQ n s

/-- The recurrence's side conditions hold on the punctured unit ball:
if s/2 = −k with k ≤ n then s = −2k lies at distance ≥ 2 from −2n
unless k = n (the puncture). -/
theorem trivRecurrence_side (n : ℕ) {s : ℂ}
    (hs : s ∈ Metric.ball (-2 * (n : ℂ)) 1) (hsn : s ≠ -2 * (n : ℂ)) :
    ∀ k : ℕ, k < n + 1 → s / 2 ≠ -(k : ℂ) := by
  intro k hk h
  have h2 : s = -2 * (k : ℂ) := by
    have h3 := congrArg (· * (2 : ℂ)) h
    rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at h3
    rw [h3]; ring
  rw [h2, Metric.mem_ball, dist_eq_norm] at hs
  rw [Nat.lt_succ_iff] at hk
  rcases eq_or_ne k n with hkn | hkn
  · exact hsn (by rwa [hkn] at h2)
  · have hlt : k < n := lt_of_le_of_ne hk hkn
    have h4 : (-2 : ℂ) * (k : ℂ) - -2 * (n : ℂ) = (((2 * (n - k) : ℕ)) : ℂ) := by
      push_cast [Nat.cast_sub hk]
      ring
    rw [h4, RCLike.norm_natCast] at hs
    have h5 : (2 : ℝ) ≤ ((2 * (n - k) : ℕ) : ℝ) := by
      have h6 : (1 : ℕ) ≤ n - k := Nat.sub_pos_of_lt hlt
      have h7 : (2 : ℕ) ≤ 2 * (n - k) := by omega
      exact_mod_cast h7
    linarith [hs, h5]

/-- Q_n is nonzero on the punctured unit ball about −2n. -/
theorem trivQ_ne_zero (n : ℕ) {s : ℂ}
    (hs : s ∈ Metric.ball (-2 * (n : ℂ)) 1) (_hsn : s ≠ -2 * (n : ℂ)) :
    trivQ n s ≠ 0 := by
  unfold trivQ
  rw [Finset.prod_ne_zero_iff]
  intro j hj
  rw [Finset.mem_range] at hj
  intro h
  have h2 : s = -2 * (j : ℂ) := by
    have h1 : s / 2 = -(j : ℂ) := eq_neg_of_add_eq_zero_left h
    have h3 := congrArg (· * (2 : ℂ)) h1
    rw [div_mul_cancel₀ s (two_ne_zero : (2 : ℂ) ≠ 0)] at h3
    rw [h3]; ring
  rw [h2, Metric.mem_ball, dist_eq_norm] at hs
  have h4 : (-2 : ℂ) * (j : ℂ) - -2 * (n : ℂ) = (((2 * (n - j) : ℕ)) : ℂ) := by
    push_cast [Nat.cast_sub hj.le]
    ring
  rw [h4, RCLike.norm_natCast] at hs
  have h5 : (2 : ℝ) ≤ ((2 * (n - j) : ℕ) : ℝ) := by
    have h6 : (1 : ℕ) ≤ n - j := Nat.sub_pos_of_lt hj
    have h7 : (2 : ℕ) ≤ 2 * (n - j) := by omega
    exact_mod_cast h7
  linarith [hs, h5]

/-- Q_n(−2n) ≠ 0 (each factor is −n+j with j < n). -/
theorem trivQ_center_ne_zero (n : ℕ) : trivQ n (-2 * (n : ℂ)) ≠ 0 := by
  unfold trivQ
  rw [Finset.prod_ne_zero_iff]
  intro j hj
  rw [Finset.mem_range] at hj
  have h1 : (-2 * (n : ℂ)) / 2 + (j : ℂ) = -((n : ℂ) - (j : ℂ)) := by ring
  rw [h1, ne_eq, neg_eq_zero, sub_eq_zero]
  exact_mod_cast (ne_of_gt hj)

/-- HfunT is analytic at −2n: on ball(−2n, 1) the point s/2+n+1 stays in
re > 0 (away from the Gamma poles), and Q_n is a polynomial nonzero at
the center. -/
theorem HfunT_analyticAt (n : ℕ) : AnalyticAt ℂ (HfunT n) (-2 * (n : ℂ)) := by
  have hcpi : AnalyticAt ℂ (fun s : ℂ => (Real.pi : ℂ) ^ (-s / 2)) (-2 * (n : ℂ)) := by
    have hexp : AnalyticAt ℂ
        (fun s : ℂ => Complex.exp ((Complex.log (Real.pi : ℂ) * (-1 / 2)) * s))
        (-2 * (n : ℂ)) :=
      (analyticAt_const.mul analyticAt_id).cexp
    apply hexp.congr
    filter_upwards with s
    rw [Complex.cpow_def_of_ne_zero (by norm_num : (Real.pi : ℂ) ≠ 0)]
    ring_nf
  have hGamma : AnalyticAt ℂ (fun s : ℂ => Complex.Gamma (s / 2 + (n : ℂ) + 1))
      (-2 * (n : ℂ)) := by
    have hd : DifferentiableOn ℂ (fun s : ℂ => Complex.Gamma (s / 2 + (n : ℂ) + 1))
        (Metric.ball (-2 * (n : ℂ)) (1 : ℝ)) := by
      intro s hs
      have hg : DifferentiableAt ℂ Complex.Gamma (s / 2 + (n : ℂ) + 1) := by
        apply Complex.differentiableAt_Gamma
        intro m hm
        have hs_eq : s = -2 * ((n : ℂ) + 1 + (m : ℂ)) := by linear_combination 2 * hm
        rw [hs_eq, Metric.mem_ball, dist_eq_norm] at hs
        have h1 : (-2 : ℂ) * ((n : ℂ) + 1 + (m : ℂ)) - -2 * (n : ℂ)
            = -(((2 : ℝ) * (1 + m) : ℝ) : ℂ) := by push_cast; ring
        rw [h1, norm_neg, Complex.norm_real, Real.norm_eq_abs] at hs
        rw [abs_of_nonneg (by positivity : (0 : ℝ) ≤ 2 * (1 + (m : ℝ)))] at hs
        have hm0 : (0 : ℝ) ≤ (m : ℝ) := by positivity
        linarith
      exact (hg.comp s
        (show DifferentiableAt ℂ (fun s : ℂ => s / 2 + (n : ℂ) + 1) s from by
          fun_prop)).differentiableWithinAt
    exact (hd.analyticOnNhd Metric.isOpen_ball) _
      (Metric.mem_ball_self (zero_lt_one : (0 : ℝ) < 1))
  have hQ : AnalyticAt ℂ (fun s : ℂ => trivQ n s) (-2 * (n : ℂ)) := by
    apply Finset.analyticAt_fun_prod
    intro j _
    exact by fun_prop
  exact ((analyticAt_const.mul hcpi).mul hGamma).div hQ (trivQ_center_ne_zero n)

/-- HfunT(−2n) ≠ 0: the numerator is 2·πⁿ·Γ(1) = 2πⁿ and the denominator
is Q_n(−2n) ≠ 0. -/
theorem HfunT_ne_zero (n : ℕ) : HfunT n (-2 * (n : ℂ)) ≠ 0 := by
  unfold HfunT
  apply div_ne_zero _ (trivQ_center_ne_zero n)
  have h1 : -(-2 * (n : ℂ)) / 2 = (n : ℂ) := by ring
  have h2 : (-2 * (n : ℂ)) / 2 + (n : ℂ) + 1 = 1 := by ring
  rw [h1, h2, Complex.Gamma_one, mul_one]
  apply mul_ne_zero (by norm_num : (2 : ℂ) ≠ 0)
  rw [Complex.cpow_natCast]
  exact pow_ne_zero n (by exact_mod_cast Real.pi_ne_zero)

/-- The punctured identity: (s+2n)·ΓR(s) = HfunT n s on ball(−2n, 1)
minus the center (the product-form recurrence in solved form). -/
theorem HfunT_eq (n : ℕ) {s : ℂ}
    (hs : s ∈ Metric.ball (-2 * (n : ℂ)) 1) (hsn : s ≠ -2 * (n : ℂ)) :
    (s + 2 * (n : ℂ)) * Complex.Gammaℝ s = HfunT n s := by
  have hside : ∀ k : ℕ, k < n + 1 → s / 2 ≠ -(k : ℂ) := trivRecurrence_side n hs hsn
  have hQne : trivQ n s ≠ 0 := trivQ_ne_zero n hs hsn
  have hsn2 : s / 2 + (n : ℂ) ≠ 0 := by
    intro h
    exact hside n (Nat.lt_succ_self n) (eq_neg_of_add_eq_zero_left h)
  have hrec := gamma_mul_prod (s / 2) (n + 1) hside
  rw [Finset.prod_range_succ] at hrec
  have hcast : s / 2 + ((n + 1 : ℕ) : ℂ) = s / 2 + (n : ℂ) + 1 := by push_cast; ring
  rw [hcast] at hrec
  have hQu : trivQ n s = ∏ j ∈ Finset.range n, (s / 2 + (j : ℂ)) := rfl
  have hGamma : Complex.Gamma (s / 2)
      = Complex.Gamma (s / 2 + (n : ℂ) + 1) / (trivQ n s * (s / 2 + (n : ℂ))) := by
    rw [hQu]
    exact (eq_div_iff (mul_ne_zero hQne hsn2)).mpr hrec
  have hs2n : s + 2 * (n : ℂ) ≠ 0 := by
    intro h
    apply hsn
    have h1 := add_eq_zero_iff_eq_neg.mp h
    rw [h1]; ring
  rw [Complex.Gammaℝ_def, hGamma]
  unfold HfunT
  field_simp [hQne, hsn2, hs2n]

/-! ## 3. zeroMult(−2n) = 1 -/

/-- **Trivial-zero simplicity, general case** (ii′-5e prep, generalizing
ii′-4c's `zeroMult_neg_two`): zeroMult(−2n) = 1 for all n ≥ 1. The local
factorization ζ(s) = (s+2n)·G(s) holds near −2n with G = Λ/HfunT n
analytic and G(−2n) ≠ 0, since Λ(−2n) = Λ(1+2n) = ΓR(1+2n)·ζ(1+2n) ≠ 0
(functional equation + ΓR ≠ 0 on re > 0 + ζ ≠ 0 on re > 1). -/
theorem zeroMult_neg_two_mul (n : ℕ) (hn : 1 ≤ n) :
    zeroMult (-2 * (n : ℂ)) = 1 := by
  have hH_an : AnalyticAt ℂ (HfunT n) (-2 * (n : ℂ)) := HfunT_analyticAt n
  have hH_ne : HfunT n (-2 * (n : ℂ)) ≠ 0 := HfunT_ne_zero n
  have hΛ_an : AnalyticAt ℂ completedRiemannZeta (-2 * (n : ℂ)) := by
    have hd : DifferentiableOn ℂ completedRiemannZeta (Metric.ball (-2 * (n : ℂ)) 1) := by
      intro s hs
      have hs0 : s ≠ 0 := by
        rintro h
        rw [h, Metric.mem_ball, dist_eq_norm] at hs
        have h1 : ((0 : ℂ) - -2 * (n : ℂ)) = ((2 * n : ℕ) : ℂ) := by push_cast; ring
        rw [h1, RCLike.norm_natCast] at hs
        have h2 : (2 : ℝ) ≤ ((2 * n : ℕ) : ℝ) := by
          have h3 : (2 : ℕ) ≤ 2 * n := by omega
          exact_mod_cast h3
        linarith [hs, h2]
      have hs1 : s ≠ 1 := by
        rintro h
        rw [h, Metric.mem_ball, dist_eq_norm] at hs
        have h1 : ((1 : ℂ) - -2 * (n : ℂ)) = ((2 * n + 1 : ℕ) : ℂ) := by push_cast; ring
        rw [h1, RCLike.norm_natCast] at hs
        have h2 : (3 : ℝ) ≤ ((2 * n + 1 : ℕ) : ℝ) := by
          have h3 : (3 : ℕ) ≤ 2 * n + 1 := by omega
          exact_mod_cast h3
        linarith [hs, h2]
      exact (differentiableAt_completedZeta hs0 hs1).differentiableWithinAt
    exact (hd.analyticOnNhd Metric.isOpen_ball) _
      (Metric.mem_ball_self (zero_lt_one : (0 : ℝ) < 1))
  have hΛ_ne : completedRiemannZeta (-2 * (n : ℂ)) ≠ 0 := by
    have hre : (1 + 2 * (n : ℂ)).re = 1 + 2 * (n : ℝ) := by
      simp [Complex.add_re, Complex.mul_re, Complex.one_re]
    have hΓR : Complex.Gammaℝ (1 + 2 * (n : ℂ)) ≠ 0 :=
      Complex.Gammaℝ_ne_zero_of_re_pos (by rw [hre]; positivity)
    have hζ : riemannZeta (1 + 2 * (n : ℂ)) ≠ 0 := by
      apply riemannZeta_ne_zero_of_one_lt_re
      rw [hre]
      have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
      linarith
    have h1ne : (1 : ℂ) + 2 * (n : ℂ) ≠ 0 := by
      intro h
      have h3 := congrArg Complex.re h
      rw [hre] at h3
      have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
      simp at h3
      linarith
    have hΛ1 : completedRiemannZeta (1 + 2 * (n : ℂ)) ≠ 0 := by
      rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul h1ne hΓR]
      exact mul_ne_zero hΓR hζ
    have hfe : completedRiemannZeta (-2 * (n : ℂ))
        = completedRiemannZeta (1 + 2 * (n : ℂ)) := by
      have h := completedRiemannZeta_one_sub (-2 * (n : ℂ))
      rw [show (1 : ℂ) - -2 * (n : ℂ) = 1 + 2 * (n : ℂ) by ring] at h
      exact h.symm
    rw [hfe]
    exact hΛ1
  have hG_an : AnalyticAt ℂ (fun s => completedRiemannZeta s / HfunT n s) (-2 * (n : ℂ)) :=
    hΛ_an.div hH_an hH_ne
  have hG_ne : completedRiemannZeta (-2 * (n : ℂ)) / HfunT n (-2 * (n : ℂ)) ≠ 0 :=
    div_ne_zero hΛ_ne hH_ne
  have hEv : ∀ᶠ s in 𝓝 (-2 * (n : ℂ)),
      riemannZeta s = (s - -2 * (n : ℂ)) ^ 1 • (completedRiemannZeta s / HfunT n s) := by
    have hHne_ev : ∀ᶠ s in 𝓝 (-2 * (n : ℂ)), HfunT n s ≠ 0 :=
      hH_an.continuousAt.eventually_ne hH_ne
    filter_upwards [Metric.ball_mem_nhds _ (zero_lt_one : (0 : ℝ) < 1), hHne_ev]
      with s hs1 hHne
    by_cases hs : s = -2 * (n : ℂ)
    · subst hs
      have hz0 : riemannZeta (-2 * (n : ℂ)) = 0 := by
        have h := riemannZeta_neg_two_mul_nat_add_one (n - 1)
        have hcast : ((n - 1 : ℕ) : ℂ) + 1 = (n : ℂ) := by
          rw [← Nat.cast_add_one, Nat.sub_add_cancel hn]
        rwa [hcast] at h
      rw [hz0]
      simp
    · have hs0 : s ≠ 0 := by
        rintro h
        rw [h, Metric.mem_ball, dist_eq_norm] at hs1
        have h1 : ((0 : ℂ) - -2 * (n : ℂ)) = ((2 * n : ℕ) : ℂ) := by push_cast; ring
        rw [h1, RCLike.norm_natCast] at hs1
        have h2 : (2 : ℝ) ≤ ((2 * n : ℕ) : ℝ) := by
          have h3 : (2 : ℕ) ≤ 2 * n := by omega
          exact_mod_cast h3
        linarith [hs1, h2]
      have hΓR : Complex.Gammaℝ s ≠ 0 := by
        rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]
        rintro ⟨m, hm⟩
        rw [hm, Metric.mem_ball, dist_eq_norm] at hs1
        rcases lt_trichotomy m n with hmn | hmn | hmn
        · have h4 : -(2 * (m : ℂ)) - -2 * (n : ℂ) = (((2 * (n - m) : ℕ)) : ℂ) := by
            push_cast [Nat.cast_sub hmn.le]
            ring
          rw [h4, RCLike.norm_natCast] at hs1
          have h5 : (2 : ℝ) ≤ ((2 * (n - m) : ℕ) : ℝ) := by
            have h7 : (2 : ℕ) ≤ 2 * (n - m) := by
              have h6 : (1 : ℕ) ≤ n - m := Nat.sub_pos_of_lt hmn
              omega
            exact_mod_cast h7
          linarith [hs1, h5]
        · subst hmn
          exact hs (by rw [hm]; ring)
        · have h4 : -(2 * (m : ℂ)) - -2 * (n : ℂ) = -(((2 * (m - n) : ℕ)) : ℂ) := by
            push_cast [Nat.cast_sub hmn.le]
            ring
          rw [h4, norm_neg, RCLike.norm_natCast] at hs1
          have h5 : (2 : ℝ) ≤ ((2 * (m - n) : ℕ) : ℝ) := by
            have h7 : (2 : ℕ) ≤ 2 * (m - n) := by
              have h6 : (1 : ℕ) ≤ m - n := Nat.sub_pos_of_lt hmn
              omega
            exact_mod_cast h7
          linarith [hs1, h5]
      have hΛ := RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hΓR
      have hH : (s + 2 * (n : ℂ)) * Complex.Gammaℝ s = HfunT n s := HfunT_eq n hs1 hs
      have hsn2n : s - -2 * (n : ℂ) = s + 2 * (n : ℂ) := by ring
      rw [pow_one, smul_eq_mul, hsn2n]
      have hz : riemannZeta s = completedRiemannZeta s / Complex.Gammaℝ s := by
        rw [hΛ, mul_div_cancel_left₀ _ hΓR]
      rw [hz, ← mul_div_assoc, div_eq_div_iff hΓR hHne, ← hH]
      ring
  have hRHS_an : AnalyticAt ℂ
      (fun s => (s - -2 * (n : ℂ)) ^ 1 • (completedRiemannZeta s / HfunT n s))
      (-2 * (n : ℂ)) :=
    ((analyticAt_id.sub analyticAt_const).pow 1).smul hG_an
  have hzeta_an : AnalyticAt ℂ riemannZeta (-2 * (n : ℂ)) :=
    hRHS_an.congr (EventuallyEq.symm hEv)
  have horder : analyticOrderAt riemannZeta (-2 * (n : ℂ)) = 1 :=
    (hzeta_an.analyticOrderAt_eq_natCast).mpr
      ⟨fun s => completedRiemannZeta s / HfunT n s, hG_an, hG_ne, hEv⟩
  rw [zeroMult, horder]
  exact ENat.toNat_one

end NguyenRH1

end