ReducedZeroCounting.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FullZeroCounting
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Metric
10 
11 def SignedZeroEnumeration.reducedRoot {N : ℕ} (e : SignedZeroEnumeration N) (m : ℕ) : ℂ :=
12   (e.root m : ℂ) ^ N
13 
14 def SignedZeroEnumeration.reducedDisk {N : ℕ} (e : SignedZeroEnumeration N) (r : ℝ) : Set ℂ :=
15   e.reducedRoot '' {m | e.root m ≤ r}
16 
17 def SignedZeroEnumeration.reducedExceptions {N : ℕ} (e : SignedZeroEnumeration N) : Set ℂ :=
18   zeroDisk (entireReducedDenominator N) (e.radius ^ N) \ range e.reducedRoot
19 
20 theorem SignedZeroEnumeration.reducedRoot_norm {N : ℕ} (e : SignedZeroEnumeration N) (m : ℕ) :
21     ‖e.reducedRoot m‖ = e.root m ^ N := by
22   rw [SignedZeroEnumeration.reducedRoot, norm_pow, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (e.positive m)]
23 
24 theorem SignedZeroEnumeration.reducedRoot_injective {N : ℕ} (hN : 0 < N)
25     (e : SignedZeroEnumeration N) : Function.Injective e.reducedRoot := by
26   intro m n h
27   apply e.injective
28   have hh := congrArg norm h
29   rw [e.reducedRoot_norm, e.reducedRoot_norm] at hh
30   exact (pow_left_strictMonoOn₀ hN.ne').injOn (e.positive m).le (e.positive n).le hh
31 
32 theorem SignedZeroEnumeration.reducedRoot_zero_simple {N : ℕ} (hN : 0 < N)
33     (e : SignedZeroEnumeration N) (m : ℕ) :
34     entireReducedDenominator N (e.reducedRoot m) = 0 ∧
35       analyticOrderNatAt (entireReducedDenominator N) (e.reducedRoot m) = 1 := by
36   constructor
37   · rw [SignedZeroEnumeration.reducedRoot, ← canonicalSignedDenominator_eq_reduced_power hN]
38     exact e.zero m
39   · rw [analyticOrderNatAt, SignedZeroEnumeration.reducedRoot,
40       ← canonicalSignedDenominator_order_eq_reduced hN (Complex.ofReal_ne_zero.mpr (ne_of_gt (e.positive m))), e.simple]
41     rfl
42 
43 theorem SignedZeroEnumeration.reducedExceptions_finite {N : ℕ} (hN : 0 < N)
44     (e : SignedZeroEnumeration N) : e.reducedExceptions.Finite :=
45   (entireReducedDenominator_zeroDisk_finite hN (e.radius ^ N)).sdiff
46 
47 theorem SignedZeroEnumeration.reducedDisk_finite_card {N : ℕ} (hN : 2 ≤ N)
48     (e : SignedZeroEnumeration N) {r : ℝ} (hr : 0 ≤ r) :
49     (e.reducedDisk r).Finite ∧ (e.reducedDisk r).ncard = sequenceCounting e.root r := by
50   have hf := (lattice_window_counting (div_pos Real.pi_pos (signed_sine_pos hN)) e.shift e.root e.windows hr).1
51   refine ⟨hf.image _, ?_⟩
52   exact ncard_image_of_injective _ (e.reducedRoot_injective (by omega))
53 
54 theorem SignedZeroEnumeration.reducedDisk_subset {N : ℕ} (hN : 0 < N)
55     (e : SignedZeroEnumeration N) (r : ℝ) :
56     e.reducedDisk r ⊆ zeroDisk (entireReducedDenominator N) (r ^ N) := by
57   rintro w ⟨m, hm, rfl⟩
58   refine ⟨?_, (e.reducedRoot_zero_simple hN m).1⟩
59   rw [e.reducedRoot_norm]
60   exact pow_le_pow_left₀ (e.positive m).le hm N
61 
62 theorem SignedZeroEnumeration.reducedZeroDisk_subset_union {N : ℕ} (hN : 0 < N)
63     (e : SignedZeroEnumeration N) {r : ℝ} (hr : 0 ≤ r) :
64     zeroDisk (entireReducedDenominator N) (r ^ N) ⊆ e.reducedDisk r ∪ e.reducedExceptions := by
65   classical
66   intro w hw
67   by_cases hwr : w ∈ range e.reducedRoot
68   · obtain ⟨m, rfl⟩ := hwr
69     apply Or.inl
70     refine ⟨m, ?_, rfl⟩
71     change e.root m ≤ r
72     by_contra hm
73     have hlt := pow_lt_pow_left₀ (lt_of_not_ge hm) hr hN.ne'
74     have hb := hw.1
75     rw [e.reducedRoot_norm] at hb
76     exact not_le_of_gt hlt hb
77   · apply Or.inr
78     refine ⟨⟨?_, hw.2⟩, hwr⟩
79     obtain ⟨z, hz⟩ := exists_complex_nth_root hN w
80     have hz0 : canonicalSignedDenominator N z = 0 := by
81       rw [canonicalSignedDenominator_eq_reduced_power hN, hz]; exact hw.2
82     have hb : ‖z‖ ≤ e.radius := by
83       by_contra h
84       obtain ⟨k, m, he⟩ := e.exhaustive z (le_of_lt (lt_of_not_ge h)) hz0
85       apply hwr
86       refine ⟨m, ?_⟩
87       have hu : (canonicalPrimitiveRoot N ^ k.val) ^ N = 1 := by
88         rw [← pow_mul, Nat.mul_comm, pow_mul, (canonicalPrimitiveRoot_isPrimitive hN).pow_eq_one, one_pow]
89       rw [← hz, he, mul_pow, hu, one_mul]
90       rfl
91     rw [← hz, norm_pow]
92     exact pow_le_pow_left₀ (norm_nonneg z) hb N
93 
94 theorem SignedZeroEnumeration.reduced_weighted_count_bounds {N : ℕ} (hN : 2 ≤ N)
95     (e : SignedZeroEnumeration N) {r : ℝ} (hr : 0 ≤ r) :
96     sequenceCounting e.root r ≤ analyticZeroCount (entireReducedDenominator N) (r ^ N) ∧
97       analyticZeroCount (entireReducedDenominator N) (r ^ N) ≤ sequenceCounting e.root r +
98         finiteWeight (analyticOrderNatAt (entireReducedDenominator N)) e.reducedExceptions := by
99   obtain ⟨hT, hc⟩ := e.reducedDisk_finite_card hN hr
100   have hw : ∀ w ∈ e.reducedDisk r, analyticOrderNatAt (entireReducedDenominator N) w = 1 := by
101     rintro _ ⟨m, _, rfl⟩
102     exact (e.reducedRoot_zero_simple (by omega) m).2
103   have h := finiteWeight_between_tail_and_exceptions (analyticOrderNatAt (entireReducedDenominator N))
104     (entireReducedDenominator_zeroDisk_finite (by omega) (r ^ N)) hT (e.reducedExceptions_finite (by omega))
105     (e.reducedDisk_subset (by omega) r) (e.reducedZeroDisk_subset_union (by omega) hr) hw
106   rwa [hc] at h
107 
108 theorem entireReducedDenominator_zero_counting_power {N : ℕ} (hN : 2 ≤ N) :
109     ∃ K : ℝ, 0 < K ∧ ∀ r : ℝ, 0 ≤ r →
110       |(analyticZeroCount (entireReducedDenominator N) (r ^ N) : ℝ) -
111         (Real.sin (Real.pi / N) / Real.pi) * r| ≤ K := by
112   let e := canonicalZeroEnumeration hN
113   let W := finiteWeight (analyticOrderNatAt (entireReducedDenominator N)) e.reducedExceptions
114   refine ⟨(W : ℝ) + e.shift + 3, by positivity, ?_⟩
115   intro r hr
116   have hw := e.reduced_weighted_count_bounds hN hr
117   have hl : (sequenceCounting e.root r : ℝ) ≤ analyticZeroCount (entireReducedDenominator N) (r ^ N) := by
118     exact_mod_cast hw.1
119   have hu : (analyticZeroCount (entireReducedDenominator N) (r ^ N) : ℝ) ≤ sequenceCounting e.root r + W := by
120     exact_mod_cast hw.2
121   have hc := (lattice_window_counting (div_pos Real.pi_pos (signed_sine_pos hN)) e.shift e.root e.windows hr).2
122   rw [abs_le] at hc ⊢
123   have he : (Real.sin (Real.pi / N) / Real.pi) * r = r / (Real.pi / Real.sin (Real.pi / N)) := by field_simp
124   rw [he]
125   constructor <;> linarith
126 
127 /-- Full reduced disk counting, including exceptional multiplicities and the N=2 boundary. -/
128 theorem entireReducedDenominator_zero_counting {N : ℕ} (hN : 2 ≤ N) :
129     ∃ K : ℝ, 0 < K ∧ ∀ R : ℝ, 0 ≤ R →
130       |(analyticZeroCount (entireReducedDenominator N) R : ℝ) -
131         (Real.sin (Real.pi / N) / Real.pi) * R ^ (1 / (N : ℝ))| ≤ K := by
132   obtain ⟨K, hK, hc⟩ := entireReducedDenominator_zero_counting_power hN
133   refine ⟨K, hK, ?_⟩
134   intro R hR
135   have h := hc (R ^ (1 / (N : ℝ))) (Real.rpow_nonneg hR _)
136   simpa only [one_div, Real.rpow_inv_natCast_pow hR (by omega : N ≠ 0)] using h
137 
138 end
139 end Komorebi.PaperIV

Back to source controls