LiSqueeze.lean

Declarations

Source

/-
NguyenRH1/LiSqueeze.lean — tier ii′ sub-stage ii′-5e-v-d (D-068 §5):
the Schwarz squeeze ⟹ the partial-fraction capstone.

§1: the Ĉ₀ growth bound `C0hat_add_two_le` (Ĉ₀(R+2) ≤ 5·log R).
§2: `not_badPoint_on_gapCircle` — every point of a γ-gap circle is good.
§3: `gentire_circle_le` — the Fexpr circle bound transferred to Gentire.
§4: `gentire_const` — max-modulus + Schwarz on the gap-circle sequence:
    the (log R)³/R → 0 squeeze forces Gentire ≡ Gentire 0.
§5: the capstone `partialFraction_identity (hZC : ZeroCountProp)`.

Archive references: D-068 §5, STATE.md session-034 next-action design.
-/
import Mathlib
import NguyenRH1.LiCircleBound

open Zeta23 Complex Filter Topology

noncomputable section

namespace NguyenRH1

/-! ## 1. The Ĉ₀ growth bound -/

/-- Ĉ₀(R+2) ≤ 5·log R for R ≥ 16002 (so log R ≥ 9): log(R+4) ≤ 2·log R,
log log(R+4) ≤ 2·log R, and 2.9 ≤ (1/3)·log R; total 2.97·log R. -/
lemma C0hat_add_two_le {R : ℝ} (hR : 16002 ≤ R) :
    C0hat (R + 2) ≤ 5 * Real.log R := by
  have hRpos : (0 : ℝ) < R := by linarith
  have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR
  have h1 : Real.log (R + 2 + 2) ≤ 2 * Real.log R := by
    have hle : R + 2 + 2 ≤ R ^ 2 := by nlinarith [hR]
    have h2 : Real.log (R + 2 + 2) ≤ Real.log (R ^ 2) :=
      Real.log_le_log (by linarith : (0 : ℝ) < R + 2 + 2) hle
    rwa [Real.log_pow, Nat.cast_two] at h2
  have h2 : Real.log (Real.log (R + 2 + 2)) ≤ 2 * Real.log R := by
    have hpos1 : (0 : ℝ) < Real.log (R + 2 + 2) := by
      have hle : Real.log R ≤ Real.log (R + 2 + 2) :=
        Real.log_le_log hRpos (by linarith)
      linarith [hlogR]
    have h3 : Real.log (Real.log (R + 2 + 2)) ≤ Real.log (2 * Real.log R) :=
      Real.log_le_log hpos1 h1
    have h4 : Real.log (2 * Real.log R) = Real.log 2 + Real.log (Real.log R) := by
      rw [Real.log_mul (by norm_num) (by linarith [hlogR] : Real.log R ≠ 0)]
    have h5 : Real.log 2 ≤ 1 := by
      have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2)
      linarith
    have h6 : Real.log (Real.log R) ≤ Real.log R := by
      have h := Real.log_le_sub_one_of_pos (by linarith [hlogR] : (0 : ℝ) < Real.log R)
      linarith
    linarith [h3, h4, h5, h6, hlogR]
  unfold C0hat
  linarith [h1, h2, hlogR]

/-! ## 2. Every γ-gap-circle point is good -/

/-- A point on a γ-gap circle is not a bad point: not a nontrivial zero
(the circle-bound lemma), not 0 or 1 (norm too large), not −2n (the
ℤ-clearance of R/2). -/
lemma not_badPoint_on_gapCircle {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}
    (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R)
    (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →
      1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)
    (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)
    {s : ℂ} (hs : ‖s‖ = R) : ¬ badPoint s := by
  have hR16002 : (16002 : ℝ) ≤ R := by
    have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
    linarith [hRlo]
  have hRpos : (0 : ℝ) < R := by linarith [hR16002]
  rintro (h | h | h | ⟨n, -, h⟩)
  · exact not_isNontrivialZero_on_gapCircle hk hRlo hgap hs h
  · rw [h, norm_zero] at hs
    linarith [hRpos]
  · rw [h, norm_one] at hs
    linarith [hR16002]
  · have hR2 : R = 2 * (n : ℝ) := by
      rw [← hs, h, norm_mul]
      have h1 : ‖(-2 : ℂ)‖ = 2 := by
        rw [show (-2 : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]
        norm_num
      rw [h1, Complex.norm_natCast]
    have hcon := hgapInt (n : ℤ)
    rw [Int.cast_natCast] at hcon
    have h0 : R / 2 - (n : ℝ) = 0 := by rw [hR2]; ring
    rw [h0, abs_zero] at hcon
    linarith [hcon]

/-! ## 3. The circle bound for Gentire -/

/-- The Fexpr circle bound transfers to Gentire on the γ-gap circles
(every circle point is good, so Gentire = Fexpr there). -/
theorem gentire_circle_le {k : ℕ} (hk : 4000 ≤ k) {R : ℝ}
    (hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R) (hRhi : R ≤ 4 * (k : ℝ) + 3)
    (hgap : ∀ ρ : ℂ, IsNontrivialZero ρ →
      1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2)) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R|)
    (hgapInt : ∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|)
    {s : ℂ} (hs : ‖s‖ = R) :
    ‖Gentire s‖ ≤ 2 * lowZeroConst + dirichletC2 +
      400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 := by
  have hgood : ¬ badPoint s := not_badPoint_on_gapCircle hk hRlo hgap hgapInt hs
  rw [gentire_eq_Fexpr hgood]
  exact Fexpr_circle_le hk hRlo hRhi hgap hgapInt hs

/-! ## 4. The squeeze: Gentire is constant -/

/-- **The Schwarz squeeze**: under the perimeter zero count, Gentire is
constant. For each ε > 0 pick a γ-gap circle of radius R ≥ 16002 with
R^{1/4} ≥ 2 + (128·C₁ + 2·C₀')·‖z₀‖/ε; max-modulus bounds Gentire on the
ball by the circle bound, Schwarz then gives
dist (Gentire z₀) (Gentire 0) ≤ (C₀' + 64·C₁·R^{3/4})·‖z₀‖/R ≤ ε. -/
theorem gentire_const (hZC : ZeroCountProp) (z₀ : ℂ) : Gentire z₀ = Gentire 0 := by
  classical
  have hA0nn : (0 : ℝ) ≤ A0count := A0count_pos.le
  have key : ∀ ε : ℝ, 0 < ε → dist (Gentire z₀) (Gentire 0) ≤ ε := by
    intro ε hε
    -- the constants
    set C₀' := 2 * lowZeroConst + dirichletC2 + ‖Gentire 0‖ with hC0'
    set C₁ := 2000000 * A0count with hC1
    have hC₀'nn : (0 : ℝ) ≤ C₀' := by
      rw [hC0']
      linarith [lowZeroConst_nonneg, dirichletC2_nonneg, norm_nonneg (Gentire 0)]
    have hC₁nn : (0 : ℝ) ≤ C₁ := by
      rw [hC1]
      exact mul_nonneg (by norm_num) hA0nn
    set c := 2 + (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε with hc
    have hXnn : (0 : ℝ) ≤ (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε :=
      div_nonneg (mul_nonneg (add_nonneg (mul_nonneg (by norm_num) hC₁nn)
        (mul_nonneg (by norm_num) hC₀'nn)) (norm_nonneg _)) hε.le
    have hcz : (2 : ℝ) ≤ c := by rw [hc]; linarith [hXnn]
    have hcnn : (0 : ℝ) ≤ c := by linarith [hcz]
    -- the radius choice
    set M := max (c ^ 4) (‖z₀‖ + 1) with hM
    obtain ⟨k, hk4000, hkM⟩ : ∃ k : ℕ, 4000 ≤ k ∧ M ≤ 4 * (k : ℝ) := by
      refine ⟨max 4000 ⌈M / 4⌉₊, le_max_left _ _, ?_⟩
      have h1 : M / 4 ≤ (⌈M / 4⌉₊ : ℝ) := Nat.le_ceil _
      have h2 : (⌈M / 4⌉₊ : ℝ) ≤ ((max 4000 ⌈M / 4⌉₊ : ℕ) : ℝ) := by
        exact_mod_cast le_max_right _ _
      linarith [h1, h2]
    obtain ⟨R, hRlo, hRhi, hgapInt, hgap⟩ :=
      exists_gapCircle_radius hZC (k := k) (by omega)
    have hR16002 : (16002 : ℝ) ≤ R := by
      have h1 : (4000 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk4000
      linarith [hRlo]
    have hRpos : (0 : ℝ) < R := by linarith [hR16002]
    have hlogR : (9 : ℝ) ≤ Real.log R := nine_le_log_of_16002_le hR16002
    have hMR : M ≤ R := by linarith [hkM, hRlo]
    -- the circle bound on the sphere, then the ball by max-modulus
    set RB := 2 * lowZeroConst + dirichletC2 +
      400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2 with hRB
    have hsphere : ∀ z ∈ Metric.sphere (0 : ℂ) R, ‖Gentire z‖ ≤ RB := by
      intro z hz
      have hznorm : ‖z‖ = R := by
        have h := Metric.mem_sphere.mp hz
        rwa [dist_eq_norm, sub_zero] at h
      exact gentire_circle_le hk4000 hRlo hRhi hgap hgapInt hznorm
    have hGan : AnalyticOn ℂ Gentire (Metric.closedBall 0 R) :=
      AnalyticOnNhd.analyticOn (fun s _ => gentire_analyticAt_and_eq.1 s)
    have hball : ∀ z ∈ Metric.closedBall (0 : ℂ) R, ‖Gentire z‖ ≤ RB :=
      fun z hz => AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl hGan hsphere hz
    -- the Schwarz inputs
    have hmaps : Set.MapsTo Gentire (Metric.ball 0 R)
        (Metric.closedBall (Gentire 0) (RB + ‖Gentire 0‖)) := by
      intro z hz
      have hzball : z ∈ Metric.closedBall (0 : ℂ) R := by
        rw [Metric.mem_ball] at hz
        rw [Metric.mem_closedBall]
        exact hz.le
      have h1 := hball z hzball
      rw [Metric.mem_closedBall, dist_eq_norm]
      calc ‖Gentire z - Gentire 0‖ ≤ ‖Gentire z‖ + ‖Gentire 0‖ := norm_sub_le _ _
        _ ≤ RB + ‖Gentire 0‖ := by linarith [h1]
    have hdiff : DifferentiableOn ℂ Gentire (Metric.ball 0 R) :=
      fun z _ => (gentire_analyticAt_and_eq.1 z).differentiableAt.differentiableWithinAt
    have hz0mem : z₀ ∈ Metric.ball (0 : ℂ) R := by
      rw [Metric.mem_ball, dist_eq_norm, sub_zero]
      have h1 : ‖z₀‖ + 1 ≤ M := le_max_right _ _
      linarith [hMR]
    have hschwarz := Complex.dist_le_div_mul_dist_of_mapsTo_ball hdiff hmaps hz0mem
    -- the growth estimates: RB + ‖Gentire 0‖ ≤ C₀' + 64·C₁·Q³, R = Q⁴
    set Q := R ^ ((4 : ℝ)⁻¹) with hQ
    have hQnn : (0 : ℝ) ≤ Q := Real.rpow_nonneg hRpos.le _
    have hQpos : (0 : ℝ) < Q := Real.rpow_pos_of_pos hRpos _
    have hQc : c ≤ Q := by
      have hc4 : c ^ 4 ≤ R := by
        have h : c ^ 4 ≤ M := le_max_left _ _
        linarith [hMR]
      have h1 : c = (c ^ 4) ^ ((4 : ℝ)⁻¹) := by
        have h := (Real.pow_rpow_inv_natCast hcnn (show (4 : ℕ) ≠ 0 by norm_num)).symm
        push_cast at h
        exact h
      have h2 : (c ^ 4) ^ ((4 : ℝ)⁻¹) ≤ Q :=
        Real.rpow_le_rpow (pow_nonneg (by linarith [hcz] : (0 : ℝ) ≤ c) 4) hc4
          (by positivity : (0 : ℝ) ≤ (4 : ℝ)⁻¹)
      rw [h1]
      exact h2
    have hL : Real.log R ≤ 4 * Q := by
      have h := Real.log_le_rpow_div hRpos.le (show (0 : ℝ) < (4 : ℝ)⁻¹ by positivity)
      have h2 : R ^ ((4 : ℝ)⁻¹) / (4 : ℝ)⁻¹ = 4 * (R ^ ((4 : ℝ)⁻¹)) := by
        rw [div_eq_mul_inv, inv_inv]
        ring
      rwa [h2] at h
    have hL3 : (Real.log R) ^ 3 ≤ 64 * Q ^ 3 := by
      have h1 : (Real.log R) ^ 3 ≤ (4 * Q) ^ 3 :=
        pow_le_pow_left₀ (by linarith [hlogR]) hL 3
      have h2 : (4 * Q) ^ 3 = 64 * Q ^ 3 := by ring
      rwa [h2] at h1
    have hR4 : R = Q ^ 4 := by
      have h := Real.rpow_inv_natCast_pow hRpos.le (show (4 : ℕ) ≠ 0 by norm_num)
      push_cast at h
      rw [← hQ] at h
      exact h.symm
    have hĈ5 : C0hat (R + 2) ≤ 5 * Real.log R := C0hat_add_two_le hR16002
    have hbig : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2
        ≤ 64 * C₁ * Q ^ 3 := by
      have hlogRnn : (0 : ℝ) ≤ Real.log R := by linarith [hlogR]
      have h1 : 400000 * A0count * C0hat (R + 2) * (Real.log R) ^ 2
          ≤ 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2 := by
        apply mul_le_mul_of_nonneg_right _ (pow_nonneg hlogRnn 2)
        exact mul_le_mul_of_nonneg_left hĈ5
          (mul_nonneg (by norm_num : (0 : ℝ) ≤ 400000) hA0nn)
      have h2 : 400000 * A0count * (5 * Real.log R) * (Real.log R) ^ 2
          = C₁ * (Real.log R) ^ 3 := by
        rw [hC1]
        ring
      have h3 : C₁ * (Real.log R) ^ 3 ≤ 64 * C₁ * Q ^ 3 := by
        have h := mul_le_mul_of_nonneg_left hL3 hC₁nn
        have h' : C₁ * (64 * Q ^ 3) = 64 * C₁ * Q ^ 3 := by ring
        rwa [h'] at h
      linarith [h1, h2, h3]
    have hRBle : RB + ‖Gentire 0‖ ≤ C₀' + 64 * C₁ * Q ^ 3 := by
      rw [hRB, hC0']
      linarith [hbig]
    -- the real squeeze: (RB + ‖Gentire 0‖)/R·‖z₀‖ ≤ ε
    have hc1 : 128 * C₁ * ‖z₀‖ ≤ ε * Q := by
      have h1 : (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε ≤ c := by rw [hc]; linarith
      have h2 : (128 * C₁) * ‖z₀‖ ≤ (128 * C₁ + 2 * C₀') * ‖z₀‖ := by
        apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
        linarith [hC₀'nn]
      have h3 : (128 * C₁) * ‖z₀‖ / ε ≤ c :=
        (div_le_div_of_nonneg_right h2 hε.le).trans h1
      calc (128 * C₁) * ‖z₀‖ = (128 * C₁) * ‖z₀‖ / ε * ε := by
            rw [div_mul_cancel₀ _ hε.ne']
        _ ≤ c * ε := mul_le_mul_of_nonneg_right h3 hε.le
        _ ≤ Q * ε := mul_le_mul_of_nonneg_right hQc hε.le
        _ = ε * Q := by ring
    have hA : 64 * C₁ * Q ^ 3 * ‖z₀‖ ≤ (ε / 2) * Q ^ 4 := by
      have h1 : (64 * C₁ * ‖z₀‖) * Q ^ 3 ≤ ((ε / 2) * Q) * Q ^ 3 := by
        apply mul_le_mul_of_nonneg_right _ (pow_nonneg hQnn 3)
        have h64 : (64 : ℝ) * C₁ * ‖z₀‖ = (128 * C₁ * ‖z₀‖) / 2 := by ring
        have hhalf : (ε / 2) * Q = (ε * Q) / 2 := by ring
        rw [h64, hhalf]
        linarith [hc1]
      have hL' : (64 * C₁ * ‖z₀‖) * Q ^ 3 = 64 * C₁ * Q ^ 3 * ‖z₀‖ := by ring
      have hR' : ((ε / 2) * Q) * Q ^ 3 = (ε / 2) * Q ^ 4 := by ring
      rwa [hL', hR'] at h1
    have hB : C₀' * ‖z₀‖ ≤ (ε / 2) * Q ^ 4 := by
      have h1 : (2 * C₀') * ‖z₀‖ ≤ ε * Q := by
        have h2 : (2 * C₀') * ‖z₀‖ ≤ (128 * C₁ + 2 * C₀') * ‖z₀‖ := by
          apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
          linarith [hC₁nn]
        have h3 : (128 * C₁ + 2 * C₀') * ‖z₀‖ / ε ≤ c := by rw [hc]; linarith
        have h4 : (2 * C₀') * ‖z₀‖ / ε ≤ c :=
          (div_le_div_of_nonneg_right h2 hε.le).trans h3
        calc (2 * C₀') * ‖z₀‖ = (2 * C₀') * ‖z₀‖ / ε * ε := by
              rw [div_mul_cancel₀ _ hε.ne']
          _ ≤ c * ε := mul_le_mul_of_nonneg_right h4 hε.le
          _ ≤ Q * ε := mul_le_mul_of_nonneg_right hQc hε.le
          _ = ε * Q := by ring
      have hQ2 : (2 : ℝ) ≤ Q := by linarith [hQc, hcz]
      have hQ3 : (2 : ℝ) ≤ Q ^ 3 := by
        have h := pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 2) hQ2 3
        norm_num at h
        linarith [h]
      have h2 : ε * Q ≤ (ε / 2) * Q ^ 4 := by
        have h3 : (ε / 2) * Q ^ 4 = ((ε / 2) * Q) * Q ^ 3 := by ring
        rw [h3]
        have h6 : (ε / 2) * Q * 2 ≤ (ε / 2) * Q * Q ^ 3 :=
          mul_le_mul_of_nonneg_left hQ3 (by positivity)
        have h5 : ε * Q = (ε / 2) * Q * 2 := by ring
        rw [h5]
        exact h6
      have h7 : C₀' * ‖z₀‖ ≤ 2 * C₀' * ‖z₀‖ := by
        have h : (0 : ℝ) ≤ C₀' * ‖z₀‖ := mul_nonneg hC₀'nn (norm_nonneg _)
        linarith [h]
      linarith [h7, h1, h2]
    have hsum : (RB + ‖Gentire 0‖) * ‖z₀‖ ≤ ε * Q ^ 4 := by
      have h1 : (RB + ‖Gentire 0‖) * ‖z₀‖ ≤ (C₀' + 64 * C₁ * Q ^ 3) * ‖z₀‖ :=
        mul_le_mul_of_nonneg_right hRBle (norm_nonneg _)
      have h2 : (C₀' + 64 * C₁ * Q ^ 3) * ‖z₀‖
          = C₀' * ‖z₀‖ + 64 * C₁ * Q ^ 3 * ‖z₀‖ := by ring
      linarith [h1, h2, hA, hB]
    have hmain : (RB + ‖Gentire 0‖) / R * ‖z₀‖ ≤ ε := by
      have hQ4pos : (0 : ℝ) < Q ^ 4 := pow_pos hQpos 4
      have h1 : (RB + ‖Gentire 0‖) / R * ‖z₀‖ = (RB + ‖Gentire 0‖) * ‖z₀‖ / Q ^ 4 := by
        rw [hR4]
        ring
      rw [h1, div_le_iff₀ hQ4pos]
      exact hsum
    -- assemble
    have hdz0 : dist z₀ (0 : ℂ) = ‖z₀‖ := by rw [dist_eq_norm, sub_zero]
    calc dist (Gentire z₀) (Gentire 0)
        ≤ (RB + ‖Gentire 0‖) / R * dist z₀ 0 := hschwarz
      _ = (RB + ‖Gentire 0‖) / R * ‖z₀‖ := by rw [hdz0]
      _ ≤ ε := hmain
  -- dist < every ε ⟹ dist = 0
  rcases le_or_gt (dist (Gentire z₀) (Gentire 0)) 0 with h | h
  · exact dist_eq_zero.mp (le_antisymm h dist_nonneg)
  · have h2 := key (dist (Gentire z₀) (Gentire 0) / 2) (by linarith)
    linarith

/-! ## 5. The capstone: the partial-fraction identity -/

/-- **The ii′-5e capstone** (D-068 §5): under the perimeter zero count
`ZeroCountProp`, the completed partial-fraction identity
ζ′/ζ(s) = B + Σ_ρ m_ρ(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2)
holds at every s off the excluded set. Proof: the difference Fexpr is
entire (5e-iv) and O((log R)²·Ĉ₀) = o(R) on the γ-gap circles
(`Fexpr_circle_le`), so the max-modulus + Schwarz squeeze (`gentire_const`)
forces it constant. -/
theorem partialFraction_identity (hZC : ZeroCountProp) :
    ∃ B : ℂ, ∀ s : ℂ, riemannZeta s ≠ 0 → s ≠ 0 → s ≠ 1 →
      (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) →
      logDeriv riemannZeta s
        = B + seriesFun s - 1 / s - 1 / (s - 1) + (Real.log Real.pi : ℂ) / 2
          - Complex.digamma (s / 2) / 2 := by
  refine ⟨Gentire 0, fun s hζ hs0 hs1 hsn => ?_⟩
  have hgood : ¬ badPoint s := by
    rintro (h | h | h | ⟨n, hn, h⟩)
    · exact hζ h.1
    · exact hs0 h
    · exact hs1 h
    · exact hsn n hn h
  have hG : Fexpr s = Gentire 0 := by
    rw [← gentire_eq_Fexpr hgood]
    exact gentire_const hZC s
  rw [Fexpr] at hG
  linear_combination hG

end NguyenRH1

end