LiGapCircles.lean

Declarations

Source

/-
NguyenRH1/LiGapCircles.lean — tier ii′ sub-stage 5e-i (D-068 §2): the
γ-gap circles for the partial-fraction identity's growth step.

`exists_gapCircle_radius` (given the perimeter `ZeroCountProp`): for each
k ≥ 1 a radius R ∈ [4k+5/2, 4k+3] with
  (i)  dist(R/2, ℤ) ≥ 1/4 — the trivial-zero clearance for the near-axis
       digamma bound (D-068 §1 C2);
  (ii) every nontrivial zero ordinate either far (|γ − R| ≥ 1) or at
       clearance |γ − R| ≥ 1/(16·C0hat(4k+9/2)) — the critical-annulus
       gap for the circle bounds (D-068 §1 C1).
Route: the ×2-RESCALE TRICK on ii′-4's `exists_avoiding_midpoint` (the
5c ×10-trick verbatim — zero new pigeonhole code): apply the unit-window
midpoint lemma at A = 8k+5 to the ×2-scaled ordinate finset of the zeros
with ordinate in [4k+3/2, 4k+9/2] (three unit windows, count ≤
3·C0hat(4k+9/2) via the perimeter + `C0hat_mono`), then halve.

Archive references: D-068 §2, D-067 §6, journal-024 (×10 trick),
journal-026.
-/
import Mathlib
import NguyenRH1.LiContour

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-- Ĉ₀ is monotone for t ≥ 1 (both log and log log terms increase). -/
theorem C0hat_mono {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) : C0hat a ≤ C0hat b := by
  have hapos : (0 : ℝ) < a + 2 := by linarith
  have h1 : Real.log (a + 2) ≤ Real.log (b + 2) := Real.log_le_log hapos (by linarith)
  have hlog1 : (1 : ℝ) ≤ Real.log (a + 2) := by
    rw [Real.le_log_iff_exp_le hapos]
    have he := Real.exp_one_lt_d9.le
    linarith
  have h2 : Real.log (Real.log (a + 2)) ≤ Real.log (Real.log (b + 2)) :=
    Real.log_le_log (by linarith) h1
  unfold C0hat
  have h3 : (0 : ℝ) ≤ (0.886 : ℝ) := by norm_num
  have h4 : (0 : ℝ) ≤ (0.433 : ℝ) := by norm_num
  nlinarith [h1, h2, h3, h4]

/-- **The γ-gap circle radius** (ii′-5e-i, D-068 §2). -/
theorem exists_gapCircle_radius (hZC : ZeroCountProp) {k : ℕ} (hk : 1 ≤ k) :
    ∃ R : ℝ, 4 * (k : ℝ) + 5 / 2 ≤ R ∧ R ≤ 4 * (k : ℝ) + 3 ∧
      (∀ m : ℤ, 1 / 4 ≤ |R / 2 - (m : ℝ)|) ∧
      ∀ ρ : ℂ, IsNontrivialZero ρ →
        (1 / (16 * C0hat (4 * (k : ℝ) + 9 / 2))) ≤ |ρ.im - R| ∨ 1 ≤ |ρ.im - R| := by
  classical
  have hk1 : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
  -- the three window finsets covering [4k+3/2, 4k+9/2]
  set W1 := (zeroWindow_finite (4 * (k : ℝ) + 3 / 2)).toFinset
  set W2 := (zeroWindow_finite (4 * (k : ℝ) + 5 / 2)).toFinset
  set W3 := (zeroWindow_finite (4 * (k : ℝ) + 7 / 2)).toFinset
  have h2t1 : (2 : ℝ) ≤ 4 * (k : ℝ) + 3 / 2 := by linarith
  have h2t2 : (2 : ℝ) ≤ 4 * (k : ℝ) + 5 / 2 := by linarith
  have h2t3 : (2 : ℝ) ≤ 4 * (k : ℝ) + 7 / 2 := by linarith
  have hW1card : (W1.card : ℝ) ≤ C0hat (4 * (k : ℝ) + 3 / 2 + 1) := by
    have h1 := hZC _ h2t1
    -- h1 : (∑ ρ ∈ W1, (zeroMult ρ : ℝ)) ≤ C0hat _; card ≤ Σ mult
    have h2 : (W1.card : ℝ) ≤ ∑ ρ ∈ W1, (zeroMult ρ : ℝ) := by
      rw [show (W1.card : ℝ) = ∑ _ρ ∈ W1, (1 : ℝ) by simp]
      apply Finset.sum_le_sum
      intro ρ hρ
      exact_mod_cast one_le_zeroMult
        (((Set.Finite.mem_toFinset (zeroWindow_finite (4 * (k : ℝ) + 3 / 2))).mp hρ).1)
    exact h2.trans h1
  have hW2card : (W2.card : ℝ) ≤ C0hat (4 * (k : ℝ) + 5 / 2 + 1) := by
    have h1 := hZC _ h2t2
    have h2 : (W2.card : ℝ) ≤ ∑ ρ ∈ W2, (zeroMult ρ : ℝ) := by
      rw [show (W2.card : ℝ) = ∑ _ρ ∈ W2, (1 : ℝ) by simp]
      apply Finset.sum_le_sum
      intro ρ hρ
      exact_mod_cast one_le_zeroMult
        (((Set.Finite.mem_toFinset (zeroWindow_finite (4 * (k : ℝ) + 5 / 2))).mp hρ).1)
    exact h2.trans h1
  have hW3card : (W3.card : ℝ) ≤ C0hat (4 * (k : ℝ) + 7 / 2 + 1) := by
    have h1 := hZC _ h2t3
    have h2 : (W3.card : ℝ) ≤ ∑ ρ ∈ W3, (zeroMult ρ : ℝ) := by
      rw [show (W3.card : ℝ) = ∑ _ρ ∈ W3, (1 : ℝ) by simp]
      apply Finset.sum_le_sum
      intro ρ hρ
      exact_mod_cast one_le_zeroMult
        (((Set.Finite.mem_toFinset (zeroWindow_finite (4 * (k : ℝ) + 7 / 2))).mp hρ).1)
    exact h2.trans h1
  -- monotonicity of the three bounds up to C0hat (4k+9/2)
  have hm1 : C0hat (4 * (k : ℝ) + 3 / 2 + 1) ≤ C0hat (4 * (k : ℝ) + 9 / 2) :=
    C0hat_mono (by linarith) (by linarith)
  have hm2 : C0hat (4 * (k : ℝ) + 5 / 2 + 1) ≤ C0hat (4 * (k : ℝ) + 9 / 2) :=
    C0hat_mono (by linarith) (by linarith)
  have hm3 : C0hat (4 * (k : ℝ) + 7 / 2 + 1) ≤ C0hat (4 * (k : ℝ) + 9 / 2) :=
    C0hat_mono (by linarith) (by linarith)
  -- the ×2-scaled ordinate finset
  set S : Finset ℝ := (W1 ∪ W2 ∪ W3).image (fun ρ : ℂ => 2 * ρ.im) with hS_def
  set k₀ := ⌈3 * C0hat (4 * (k : ℝ) + 9 / 2)⌉₊ with hk₀
  have hC2 : (2 : ℝ) ≤ C0hat (4 * (k : ℝ) + 9 / 2) := two_le_C0hat (by linarith)
  have hScardNat : S.card ≤ k₀ := by
    have hcard1 : S.card ≤ (W1 ∪ W2 ∪ W3).card := Finset.card_image_le
    have hcard2 : (W1 ∪ W2 ∪ W3).card ≤ W1.card + W2.card + W3.card := by
      calc (W1 ∪ W2 ∪ W3).card ≤ (W1 ∪ W2).card + W3.card := Finset.card_union_le _ _
        _ ≤ (W1.card + W2.card) + W3.card :=
            add_le_add_left (Finset.card_union_le W1 W2) _
        _ = W1.card + W2.card + W3.card := rfl
    have hcard3 : ((W1.card + W2.card + W3.card : ℕ) : ℝ) ≤ 3 * C0hat (4 * (k : ℝ) + 9 / 2) := by
      push_cast
      linarith [hW1card, hW2card, hW3card, hm1, hm2, hm3]
    have h2 : (S.card : ℝ) ≤ (k₀ : ℝ) :=
      (Nat.cast_le.mpr (hcard1.trans hcard2)).trans
        (hcard3.trans (by rw [hk₀]; exact Nat.le_ceil _))
    exact Nat.cast_le.mp h2
  obtain ⟨T', hT1, hT2, hT3⟩ := exists_avoiding_midpoint (8 * (k : ℝ) + 5) S hScardNat
  set R := T' / 2 with hR_def
  have hRlo : 4 * (k : ℝ) + 5 / 2 ≤ R := by rw [hR_def]; linarith [hT1]
  have hRhi : R ≤ 4 * (k : ℝ) + 3 := by rw [hR_def]; linarith [hT2]
  refine ⟨R, hRlo, hRhi, ?_, ?_⟩
  · -- (i) the ℤ-clearance: R/2 = T'/4 ∈ [2k+5/4, 2k+3/2]
    intro m
    by_cases hmc : m ≤ 2 * (k : ℤ) + 1
    · have hmcR : (m : ℝ) ≤ 2 * (k : ℝ) + 1 := by
        have h1 : ((2 * (k : ℤ) + 1 : ℤ) : ℝ) = 2 * (k : ℝ) + 1 := by push_cast; ring
        rw [← h1]
        exact_mod_cast hmc
      have hge : (1 : ℝ) / 4 ≤ R / 2 - (m : ℝ) := by rw [hR_def]; linarith [hT1, hmcR]
      rw [abs_of_nonneg (by linarith [hge])]
      exact hge
    · push Not at hmc
      have hmc2 : (2 * (k : ℤ) + 2 : ℤ) ≤ m := by omega
      have hmcR : (2 : ℝ) * (k : ℝ) + 2 ≤ (m : ℝ) := by
        have h1 : ((2 * (k : ℤ) + 2 : ℤ) : ℝ) = 2 * (k : ℝ) + 2 := by push_cast; ring
        rw [← h1]
        exact_mod_cast hmc2
      have hge : (1 : ℝ) / 4 ≤ (m : ℝ) - R / 2 := by rw [hR_def]; linarith [hT2, hmcR]
      rw [abs_of_nonpos (by linarith [hge])]
      linarith [hge]
  · -- (ii) the ordinate clearance
    intro ρ hρ
    by_cases hcase : |ρ.im - R| < 1
    · left
      -- ρ.im ∈ (R−1, R+1) ⊆ [4k+3/2, 4k+9/2]
      have hrange1 : 4 * (k : ℝ) + 3 / 2 ≤ ρ.im := by
        have h1 := (abs_lt.mp hcase).1
        linarith [h1, hRlo]
      have hrange2 : ρ.im ≤ 4 * (k : ℝ) + 9 / 2 := by
        have h2 := (abs_lt.mp hcase).2
        linarith [h2, hRhi]
      -- window membership
      have hmem : ρ ∈ W1 ∪ W2 ∪ W3 := by
        by_cases hsplit1 : ρ.im ≤ 4 * (k : ℝ) + 5 / 2
        · have hρ1 : ρ ∈ W1 := by
            apply (Set.Finite.mem_toFinset (zeroWindow_finite (4 * (k : ℝ) + 3 / 2))).mpr
            exact ⟨hρ, hrange1, by linarith [hsplit1]⟩
          exact Finset.mem_union_left _ (Finset.mem_union_left _ hρ1)
        · push Not at hsplit1
          by_cases hsplit2 : ρ.im ≤ 4 * (k : ℝ) + 7 / 2
          · have hρ2 : ρ ∈ W2 := by
              apply (Set.Finite.mem_toFinset (zeroWindow_finite (4 * (k : ℝ) + 5 / 2))).mpr
              exact ⟨hρ, hsplit1.le, by linarith [hsplit2]⟩
            exact Finset.mem_union_left _ (Finset.mem_union_right _ hρ2)
          · push Not at hsplit2
            have hρ3 : ρ ∈ W3 := by
              apply (Set.Finite.mem_toFinset (zeroWindow_finite (4 * (k : ℝ) + 7 / 2))).mpr
              exact ⟨hρ, hsplit2.le, by linarith [hrange2]⟩
            exact Finset.mem_union_right _ hρ3
      have h2mem : 2 * ρ.im ∈ S :=
        Finset.mem_image.mpr ⟨ρ, hmem, rfl⟩
      have hgap := hT3 (2 * ρ.im) h2mem
      -- halving the ×2 clearance
      have hhalve : |ρ.im - R| = |2 * ρ.im - T'| / 2 := by
        rw [hR_def]
        have h1 : 2 * ρ.im - T' = 2 * (ρ.im - T' / 2) := by ring
        rw [h1, abs_mul, show |(2 : ℝ)| = 2 by norm_num]
        ring
      -- k₀ + 1 ≤ 4·C₀ ⟹ 1/(16 C₀) ≤ 1/(4 (k₀+1))
      have hk0bound : ((k₀ : ℝ) + 1) ≤ 4 * C0hat (4 * (k : ℝ) + 9 / 2) := by
        have h0 : (0 : ℝ) ≤ 3 * C0hat (4 * (k : ℝ) + 9 / 2) := by linarith [hC2]
        have h1 := Nat.ceil_lt_add_one h0
        have h2 : (k₀ : ℝ) < 3 * C0hat (4 * (k : ℝ) + 9 / 2) + 1 := by
          rw [hk₀]; exact_mod_cast h1
        linarith [h2, hC2]
      have hone : (1 : ℝ) / (16 * C0hat (4 * (k : ℝ) + 9 / 2))
          ≤ 1 / (4 * ((k₀ : ℝ) + 1)) := by
        apply one_div_le_one_div_of_le
        · have hk₀pos : (0 : ℝ) ≤ (k₀ : ℝ) := by positivity
          positivity
        · linarith [hk0bound]
      rw [hhalve]
      refine hone.trans ?_
      have hpos : (0 : ℝ) < 2 * ((k₀ : ℝ) + 1) := by positivity
      have hgap2 : 1 / (4 * ((k₀ : ℝ) + 1)) ≤ |2 * ρ.im - T'| / 2 := by
        rw [le_div_iff₀ (by norm_num : (0 : ℝ) < 2)]
        have heq : (1 : ℝ) / (4 * ((k₀ : ℝ) + 1)) * 2 = 1 / (2 * ((k₀ : ℝ) + 1)) := by
          have h4 : (4 : ℝ) * ((k₀ : ℝ) + 1) = (2 * ((k₀ : ℝ) + 1)) * 2 := by ring
          rw [h4, ← div_div, div_mul_cancel₀ _ (by norm_num : (2 : ℝ) ≠ 0)]
        rw [heq]
        exact hgap
      exact hgap2
    · right
      exact (not_lt.mp hcase)

end NguyenRH1

end