ZeroSequenceCounting.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroSequenceAsymptotics
6 import Mathlib.Data.Set.Card
7 import Mathlib.Order.Interval.Set.Nat
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Metric
12 
13 /-- Number of entries of a real sequence at or below a real cutoff. -/
14 def sequenceCounting (f : ℕ → ℝ) (R : ℝ) : ℕ := {m | f m ≤ R}.ncard
15 
16 /-- A finite counting estimate for any sequence trapped in bounded lattice windows. -/
17 theorem lattice_window_counting {A : ℝ} (hA : 0 < A) (B : ℕ) (f : ℕ → ℝ)
18     (hf : ∀ m, A * m ≤ f m ∧ f m ≤ A * ((m : ℝ) + B))
19     {R : ℝ} (hR : 0 ≤ R) :
20     {m | f m ≤ R}.Finite ∧ |(sequenceCounting f R : ℝ) - R / A| ≤ B + 2 := by
21   let k := Nat.floor (R / A)
22   have hupper : {m | f m ≤ R} ⊆ Iio (k + 1) := by
23     intro m hm
24     change f m ≤ R at hm
25     have hh : (m : ℝ) ≤ R / A := (le_div_iff₀ hA).mpr (by nlinarith [(hf m).1])
26     have hk : m ≤ k := Nat.le_floor hh
27     exact Nat.lt_succ_of_le hk
28   have hfinite := (finite_Iio (k + 1)).subset hupper
29   have hlower : Iio (k - B) ⊆ {m | f m ≤ R} := by
30     intro m hm
31     have hm' : m + B ≤ k := by simp only [mem_Iio] at hm; omega
32     have hmreal : (m : ℝ) + B ≤ k := by exact_mod_cast hm'
33     have hk : (k : ℝ) ≤ R / A := Nat.floor_le (div_nonneg hR hA.le)
34     have hh : A * ((m : ℝ) + B) ≤ R := by
35       have := (le_div_iff₀ hA).mp (hmreal.trans hk)
36       nlinarith
37     exact (hf m).2.trans hh
38   have hcupper : sequenceCounting f R ≤ k + 1 := by
39     simpa [sequenceCounting] using ncard_le_ncard hupper
40   have hclower : k - B ≤ sequenceCounting f R := by
41     simpa [sequenceCounting] using ncard_le_ncard hlower hfinite
42   have hklower : k ≤ sequenceCounting f R + B := by omega
43   have hcu : (sequenceCounting f R : ℝ) ≤ k + 1 := by exact_mod_cast hcupper
44   have hcl : (k : ℝ) ≤ sequenceCounting f R + B := by exact_mod_cast hklower
45   have hfloorlo : (k : ℝ) ≤ R / A := Nat.floor_le (div_nonneg hR hA.le)
46   have hfloorhi : R / A < (k : ℝ) + 1 := Nat.lt_floor_add_one _
47   exact ⟨hfinite, abs_le.mpr ⟨by linarith, by have := Nat.cast_nonneg (α := ℝ) B; linarith⟩⟩
48 
49 theorem signedPositiveZero_lattice_windows {N : ℕ} (hN : 3 ≤ N) :
50     ∃ m0 : ℕ, ∀ m : ℕ,
51       (Real.pi / Real.sin (Real.pi / N)) * m ≤ signedPositiveZero N (m + m0) ∧
52       signedPositiveZero N (m + m0) ≤
53         (Real.pi / Real.sin (Real.pi / N)) * ((m : ℝ) + (m0 + 1 : ℕ)) := by
54   obtain ⟨C, _, m0, hm0⟩ := signedPositiveZero_local_strings hN
55   refine ⟨m0, ?_⟩
56   intro m
57   have hb := (hm0 (m + m0) (by omega)).1.2.2
58   have he : |signedPositiveZero N (m + m0) - signedZeroCenter N (m + m0)| ≤
59       1 / ‖signedZeroFrequency N‖ := by
60     simpa only [mem_closedBall, dist_eq_norm, ← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] using hb
61   have hr := signedZeroCenter_ge_radius (by omega : 2 ≤ N) 0
62   have ha : 0 < Real.pi / Real.sin (Real.pi / N) := div_pos Real.pi_pos (signed_sine_pos (by omega))
63   rw [abs_le] at he
64   simp only [signedZeroCenter, Nat.cast_zero, zero_add] at hr
65   simp only [signedZeroCenter, Nat.cast_add, Nat.cast_one] at he ⊢
66   have hm0' := Nat.cast_nonneg (α := ℝ) m0
67   constructor <;> nlinarith
68 
69 /-- The positive zero tail has density `sin(pi/N)/pi` with a uniform bounded counting error. -/
70 theorem signedPositiveZero_tail_counting {N : ℕ} (hN : 3 ≤ N) :
71     ∃ m0 : ℕ, ∃ K : ℝ, 0 < K ∧ ∀ R : ℝ, 0 ≤ R →
72       {m | signedPositiveZero N (m + m0) ≤ R}.Finite ∧
73       |(sequenceCounting (fun m => signedPositiveZero N (m + m0)) R : ℝ) -
74         (Real.sin (Real.pi / N) / Real.pi) * R| ≤ K := by
75   obtain ⟨m0, hm0⟩ := signedPositiveZero_lattice_windows hN
76   refine ⟨m0, (m0 + 1 : ℕ) + 2, by positivity, ?_⟩
77   intro R hR
78   have h := lattice_window_counting (div_pos Real.pi_pos (signed_sine_pos (by omega)))
79     (m0 + 1) (fun m => signedPositiveZero N (m + m0)) hm0 hR
80   convert h using 2
81   field_simp
82 
83 end
84 end Komorebi.PaperIV

Back to source controls