SignedZeroLocalization.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.RegularPolygonGap
6 import KomorebiPaperIV.ZeroPerturbation
7 import Mathlib.Topology.Algebra.InfiniteSum.Constructions
8 
9 /-! # Actual large local zero strings of the signed denominator
10 
11 This module applies the contraction theorem to the canonical finite sum and
12 derives its smallness hypotheses. Global exclusion outside these disks is not
13 assumed or asserted.
14 -/
15 
16 namespace Komorebi.PaperIV
17 noncomputable section
18 open Metric
19 
20 def canonicalSignedDenominator (N : ℕ) : ℂ → ℂ :=
21   entireSigned N 0 (canonicalPrimitiveRoot N) (canonicalSignedRoot N)
22 
23 def signedZeroFrequency (N : ℕ) : ℂ :=
24   canonicalSignedRoot N - canonicalSignedVertex N (N - 1)
25 
26 def signedZeroCenter (N m : ℕ) : ℝ :=
27   (Real.pi / Real.sin (Real.pi / N)) * (m + 1 / 2)
28 
29 theorem signed_sine_pos {N : ℕ} (hN : 2 ≤ N) : 0 < Real.sin (Real.pi / N) := by
30   have hn : (2 : ℝ) ≤ N := by exact_mod_cast hN
31   have hp : 0 < Real.pi / N := div_pos Real.pi_pos (by linarith)
32   have he : Real.pi / N * N = Real.pi := div_mul_cancel₀ _ (by linarith)
33   exact Real.sin_pos_of_pos_of_lt_pi hp (by nlinarith)
34 
35 theorem signedZeroFrequency_ne_zero {N : ℕ} (hN : 2 ≤ N) : signedZeroFrequency N ≠ 0 := by
36   rw [signedZeroFrequency, canonicalSignedVertex_adjacent_difference (by omega)]
37   exact mul_ne_zero (mul_ne_zero (by norm_num) (by exact_mod_cast (signed_sine_pos hN).ne')) Complex.I_ne_zero
38 
39 theorem signedZeroCenter_cancellation {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
40     Complex.exp (signedZeroFrequency N * (signedZeroCenter N m : ℂ)) = -1 := by
41   have hs : (Real.sin (Real.pi / N) : ℂ) ≠ 0 := by exact_mod_cast (signed_sine_pos hN).ne'
42   have he : signedZeroFrequency N * (signedZeroCenter N m : ℂ) =
43       (Real.pi : ℂ) * Complex.I + (m : ℤ) * (2 * (Real.pi : ℂ) * Complex.I) := by
44     rw [signedZeroFrequency, canonicalSignedVertex_adjacent_difference (by omega)]
45     unfold signedZeroCenter
46     push_cast
47     push_cast at hs
48     field_simp [hs]
49     ring
50   rw [he, ← Complex.exp_pi_mul_I]
51   apply Complex.exp_eq_exp_iff_exists_int.mpr
52   exact ⟨(m : ℤ), rfl⟩
53 
54 /-- Uniform exponential decay on a fixed-radius disk translated along the real axis. -/
55 theorem canonicalSignedRemainder_disk_bound {N : ℕ} (hN : 3 ≤ N)
56     {t r : ℝ} (ht : r ≤ t) {z : ℂ} (hz : z ∈ closedBall (t : ℂ) r) (q : ℕ) :
57     ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤
58       (((N - 2 : ℕ) : ℝ) * 2 ^ q * Real.exp (signedPolygonGap N * r + 2 * r)) *
59         Real.exp (-signedPolygonGap N * t) := by
60   have hzN : ‖z - (t : ℂ)‖ ≤ r := by simpa [mem_closedBall, dist_eq_norm] using hz
61   have hreal : t - r ≤ z.re := by
62     have h := (Complex.abs_re_le_norm (z - (t : ℂ))).trans hzN
63     simp only [Complex.sub_re, Complex.ofReal_re] at h
64     have := (abs_le.mp h).1
65     linarith
66   have him : |z.im| ≤ r := by
67     simpa only [Complex.sub_im, Complex.ofReal_im, sub_zero] using
68       (Complex.abs_im_le_norm (z - (t : ℂ))).trans hzN
69   have hb := canonicalSignedRemainder_strip_bound hN (by linarith : 0 ≤ z.re) him q
70   calc
71     _ ≤ ((N - 2 : ℕ) : ℝ) * 2 ^ q * Real.exp (-signedPolygonGap N * z.re + 2 * r) := hb
72     _ ≤ ((N - 2 : ℕ) : ℝ) * 2 ^ q *
73         Real.exp ((signedPolygonGap N * r + 2 * r) + (-signedPolygonGap N * t)) := by
74       apply mul_le_mul_of_nonneg_left _ (by positivity)
75       apply Real.exp_le_exp.mpr
76       nlinarith [signedPolygonGap_pos hN]
77     _ = _ := by rw [Real.exp_add]; ring
78 
79 /-- An explicit threshold exists for smallness on every translated fixed disk. -/
80 theorem signedRemainder_eventually_small_on_disks {N : ℕ} (hN : 3 ≤ N)
81     {r ε : ℝ} (_hr : 0 ≤ r) (hε : 0 < ε) (q : ℕ) :
82     ∃ T : ℝ, r ≤ T ∧ ∀ t : ℝ, T ≤ t → ∀ z ∈ closedBall (t : ℂ) r,
83       ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) q z‖ ≤ ε := by
84   let γ := signedPolygonGap N
85   let C : ℝ := ((N - 2 : ℕ) : ℝ) * 2 ^ q
86   have hγ : 0 < γ := signedPolygonGap_pos hN
87   have hC : 0 < C := by
88     dsimp [C]
89     have hn : 0 < N - 2 := by omega
90     positivity
91   let T := max r ((γ * r + 2 * r - Real.log (ε / C)) / γ)
92   refine ⟨T, le_max_left _ _, ?_⟩
93   intro t ht z hz
94   have htR : r ≤ t := (le_max_left _ _).trans ht
95   have hzN : ‖z - (t : ℂ)‖ ≤ r := by simpa [mem_closedBall, dist_eq_norm] using hz
96   have hreal : t - r ≤ z.re := by
97     have h := (Complex.abs_re_le_norm (z - (t : ℂ))).trans hzN
98     simp only [Complex.sub_re, Complex.ofReal_re] at h
99     have := (abs_le.mp h).1
100     linarith
101   have him : |z.im| ≤ r := by
102     simpa only [Complex.sub_im, Complex.ofReal_im, sub_zero] using
103       (Complex.abs_im_le_norm (z - (t : ℂ))).trans hzN
104   have hb := canonicalSignedRemainder_strip_bound hN (by linarith : 0 ≤ z.re) him q
105   have hexp : Real.exp (-γ * t + γ * r + 2 * r) ≤ ε / C := by
106     apply (Real.le_log_iff_exp_le (div_pos hε hC)).mp
107     have hh : (γ * r + 2 * r - Real.log (ε / C)) / γ ≤ t := (le_max_right _ _).trans ht
108     have := (div_le_iff₀ hγ).mp hh
109     linarith
110   calc
111     _ ≤ C * Real.exp (-γ * z.re + 2 * r) := hb
112     _ ≤ C * Real.exp (-γ * t + γ * r + 2 * r) := by
113       apply mul_le_mul_of_nonneg_left _ hC.le
114       apply Real.exp_le_exp.mpr
115       nlinarith
116     _ ≤ C * (ε / C) := mul_le_mul_of_nonneg_left hexp hC.le
117     _ = ε := by field_simp
118 
119 theorem canonicalSignedDenominator_conj {N : ℕ} (hN : 0 < N) (z : ℂ) :
120     canonicalSignedDenominator N (star z) = star (canonicalSignedDenominator N z) := by
121   have hs := (hasSum_entireSigned hN hN (canonicalPrimitiveRoot_isPrimitive hN)
122     (canonicalSignedRoot_pow hN) z).star
123   have ht := hasSum_entireSigned hN hN (canonicalPrimitiveRoot_isPrimitive hN)
124     (canonicalSignedRoot_pow hN) (star z)
125   apply ht.unique
126   convert hs using 1
127   · funext n
128     by_cases h : n % N = 0
129     · simp [coeff_signedSection, signedSectionCoeff, h]
130     · simp [coeff_signedSection, signedSectionCoeff, h]
131   · rfl
132 
133 /-- Every sufficiently large cancellation center has a unique actual denominator zero. -/
134 theorem canonicalSignedDenominator_eventual_local_zero {N : ℕ} (hN : 3 ≤ N) :
135     ∃ T : ℝ, 1 / ‖signedZeroFrequency N‖ ≤ T ∧ ∀ t : ℝ, T ≤ t →
136       Complex.exp (signedZeroFrequency N * (t : ℂ)) = -1 →
137       ∃! z : ℂ, z ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
138         canonicalSignedDenominator N z = 0 := by
139   have ha := signedZeroFrequency_ne_zero (show 2 ≤ N by omega)
140   let ε := min (1 / 2 : ℝ) (‖signedZeroFrequency N‖ / 4)
141   have hε : 0 < ε := lt_min (by norm_num) (div_pos (norm_pos_iff.mpr ha) (by norm_num))
142   obtain ⟨T0, hT0, hb0⟩ := signedRemainder_eventually_small_on_disks hN
143     (by positivity : 0 ≤ 1 / ‖signedZeroFrequency N‖) hε 0
144   obtain ⟨T1, hT1, hb1⟩ := signedRemainder_eventually_small_on_disks hN
145     (by positivity : 0 ≤ 1 / ‖signedZeroFrequency N‖) hε 1
146   refine ⟨max T0 T1, hT0.trans (le_max_left _ _), ?_⟩
147   intro t ht hc
148   have h0 := hb0 t ((le_max_left _ _).trans ht)
149   have h1 := hb1 t ((le_max_right _ _).trans ht)
150   have hzero := perturbed_exponential_unique_zero ha hc
151     (fun z hz => (h0 z hz).trans (min_le_left _ _))
152     (fun z _ => hasDerivAt_finiteExponentialRemainder _ _ _ 0 z)
153     (fun z hz => (h1 z hz).trans (min_le_right _ _))
154   convert hzero using 1
155   funext z
156   congr 1
157   exact propext (signed_two_term_zero_iff (show 2 ≤ N by omega)
158     (canonicalPrimitiveRoot N) (canonicalSignedRoot N) z)
159 
160 /-- A unique zero in a disk centered on the real axis is itself real. -/
161 theorem canonicalSignedDenominator_unique_zero_real {N : ℕ} (hN : 0 < N)
162     {t r : ℝ} {z : ℂ} (hz : z ∈ closedBall (t : ℂ) r)
163     (hz0 : canonicalSignedDenominator N z = 0)
164     (hu : ∀ w : ℂ, w ∈ closedBall (t : ℂ) r ∧ canonicalSignedDenominator N w = 0 → w = z) :
165     z.im = 0 := by
166   have hzstar : star z ∈ closedBall (t : ℂ) r := by
167     have he : star z - (t : ℂ) = star (z - (t : ℂ)) := by simp
168     simpa only [mem_closedBall, dist_eq_norm, he, norm_star] using hz
169   have heq := hu (star z) ⟨hzstar, by rw [canonicalSignedDenominator_conj hN, hz0, star_zero]⟩
170   have him := congrArg Complex.im heq
171   change -z.im = z.im at him
172   linarith
173 
174 /-- Simplicity transfers from the normalized exponential sum to the actual denominator. -/
175 theorem canonicalSignedDenominator_local_zero_simple {N : ℕ} (hN : 3 ≤ N)
176     {z : ℂ} (hz : canonicalSignedDenominator N z = 0)
177     (h0 : ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z‖ ≤ 1 / 2)
178     (h1 : ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z‖ ≤
179       ‖signedZeroFrequency N‖ / 4) :
180     analyticOrderAt (canonicalSignedDenominator N) z = 1 := by
181   let R := signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0
182   let P := fun w => (N : ℂ) * Complex.exp (-(canonicalSignedVertex N (N - 1) * w))
183   have hR : AnalyticAt ℂ R z := analyticAt_finiteExponentialRemainder _ _ _ _ _
184   have hdR : deriv R z =
185       signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z :=
186     (hasDerivAt_finiteExponentialRemainder _ _ _ _ _).deriv
187   have hzero : 1 + Complex.exp (signedZeroFrequency N * z) + R z = 0 :=
188     (signed_two_term_zero_iff (by omega) _ _ z).mp hz
189   have hs := perturbed_exponential_zero_order_one (signedZeroFrequency_ne_zero (by omega))
190     hR hzero h0 (by rw [hdR]; exact h1)
191   have he : (fun w => 1 + Complex.exp (signedZeroFrequency N * w) + R w) =
192       fun w => P w * canonicalSignedDenominator N w := by
193     funext w
194     exact (signed_two_term_normalization (by omega) _ _ w).symm
195   have hP : AnalyticAt ℂ P z := by dsimp [P]; fun_prop
196   have hD : AnalyticAt ℂ (canonicalSignedDenominator N) z := analyticAt_entireSigned _ _ _ _ _
197   have hP0 : analyticOrderAt P z = 0 := hP.analyticOrderAt_eq_zero.mpr
198     (mul_ne_zero (by exact_mod_cast (show N ≠ 0 by omega)) (Complex.exp_ne_zero _))
199   rw [he] at hs
200   change analyticOrderAt (P * canonicalSignedDenominator N) z = 1 at hs
201   rw [analyticOrderAt_mul hP hD, hP0, zero_add] at hs
202   exact hs
203 
204 /-- There are positive real simple zeros near every sufficiently large lattice center.
205 This proves existence of the strings, without a claim that they exhaust all large zeros. -/
206 theorem canonicalSignedDenominator_eventual_positive_simple_zeros {N : ℕ} (hN : 3 ≤ N) :
207     ∃ m0 : ℕ, ∀ m : ℕ, m0 ≤ m → ∃ z : ℂ,
208       z ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
209       canonicalSignedDenominator N z = 0 ∧ z.im = 0 ∧ 0 < z.re ∧
210       analyticOrderAt (canonicalSignedDenominator N) z = 1 ∧
211       ∀ w : ℂ, w ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
212         canonicalSignedDenominator N w = 0 → w = z := by
213   have ha := signedZeroFrequency_ne_zero (show 2 ≤ N by omega)
214   let r := 1 / ‖signedZeroFrequency N‖
215   obtain ⟨T, _, hT⟩ := canonicalSignedDenominator_eventual_local_zero hN
216   obtain ⟨T0, _, hT0⟩ := signedRemainder_eventually_small_on_disks hN
217     (by positivity : 0 ≤ r) (by norm_num : (0 : ℝ) < 1 / 2) 0
218   obtain ⟨T1, _, hT1⟩ := signedRemainder_eventually_small_on_disks hN
219     (by positivity : 0 ≤ r) (div_pos (norm_pos_iff.mpr ha) (by norm_num : (0 : ℝ) < 4)) 1
220   let A := Real.pi / Real.sin (Real.pi / N)
221   have hA : 0 < A := div_pos Real.pi_pos (signed_sine_pos (by omega))
222   let B := max T (max T0 (max T1 r))
223   obtain ⟨m0, hm0⟩ := exists_nat_gt (B / A)
224   refine ⟨m0, ?_⟩
225   intro m hm
226   have hmm : (m0 : ℝ) ≤ m := by exact_mod_cast hm
227   have hB : B < signedZeroCenter N m := by
228     have hh := (div_lt_iff₀ hA).mp hm0
229     change B < A * ((m : ℝ) + 1 / 2)
230     nlinarith
231   have ht : T ≤ signedZeroCenter N m := (le_max_left _ _).trans hB.le
232   have ht0 : T0 ≤ signedZeroCenter N m := (le_trans (le_max_left _ _) (le_max_right _ _)).trans hB.le
233   have ht1 : T1 ≤ signedZeroCenter N m :=
234     (le_trans (le_max_left _ _) (le_trans (le_max_right _ _) (le_max_right _ _))).trans hB.le
235   have htr : r < signedZeroCenter N m :=
236     lt_of_le_of_lt (le_trans (le_max_right _ _) (le_trans (le_max_right _ _) (le_max_right _ _))) hB
237   obtain ⟨z, ⟨hz, hz0⟩, hu⟩ := hT (signedZeroCenter N m) ht (signedZeroCenter_cancellation (by omega) m)
238   refine ⟨z, hz, hz0, canonicalSignedDenominator_unique_zero_real (by omega) hz hz0 hu, ?_, ?_, hu⟩
239   · have h := (Complex.abs_re_le_norm (z - (signedZeroCenter N m : ℂ))).trans
240       (show ‖z - (signedZeroCenter N m : ℂ)‖ ≤ r by simpa [r, mem_closedBall, dist_eq_norm] using hz)
241     simp only [Complex.sub_re, Complex.ofReal_re] at h
242     have := (abs_le.mp h).1
243     linarith
244   · exact canonicalSignedDenominator_local_zero_simple hN hz0
245       (hT0 _ ht0 z hz) (hT1 _ ht1 z hz)
246 
247 /-- Quantified exponentially small displacement for a localized denominator zero. -/
248 theorem canonicalSignedDenominator_local_zero_exponential_distance {N : ℕ} (hN : 3 ≤ N)
249     {t : ℝ} (ht : 1 / ‖signedZeroFrequency N‖ ≤ t)
250     (hc : Complex.exp (signedZeroFrequency N * (t : ℂ)) = -1)
251     (hsmall : ∀ w ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖),
252       ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 w‖ ≤ 1 / 2)
253     {z : ℂ} (hz : z ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖))
254     (hz0 : canonicalSignedDenominator N z = 0) :
255     ‖z - (t : ℂ)‖ ≤
256       ((3 / 2 : ℝ) * ((N - 2 : ℕ) : ℝ) *
257         Real.exp (signedPolygonGap N * (1 / ‖signedZeroFrequency N‖) + 2 * (1 / ‖signedZeroFrequency N‖)) /
258           ‖signedZeroFrequency N‖) * Real.exp (-signedPolygonGap N * t) := by
259   have hd := perturbed_exponential_pointwise_distance (signedZeroFrequency_ne_zero (by omega))
260     hc hsmall hz ((signed_two_term_zero_iff (by omega) _ _ z).mp hz0)
261   have hb := canonicalSignedRemainder_disk_bound hN ht hz 0
262   simp only [pow_zero, mul_one] at hb
263   apply hd.trans
264   calc
265     _ ≤ (3 / 2 : ℝ) *
266         ((((N - 2 : ℕ) : ℝ) * Real.exp (signedPolygonGap N * (1 / ‖signedZeroFrequency N‖) +
267           2 * (1 / ‖signedZeroFrequency N‖))) * Real.exp (-signedPolygonGap N * t)) /
268           ‖signedZeroFrequency N‖ := by gcongr
269     _ = _ := by ring
270 
271 /-- The positive real simple zero strings have the manuscript's exponential location rate.
272 Completeness of these strings among all large complex zeros remains a separate theorem. -/
273 theorem canonicalSignedDenominator_local_strings {N : ℕ} (hN : 3 ≤ N) :
274     ∃ C : ℝ, 0 < C ∧ ∃ m0 : ℕ, ∀ m : ℕ, m0 ≤ m → ∃ z : ℂ,
275       z ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
276       canonicalSignedDenominator N z = 0 ∧ z.im = 0 ∧ 0 < z.re ∧
277       analyticOrderAt (canonicalSignedDenominator N) z = 1 ∧
278       ‖z - (signedZeroCenter N m : ℂ)‖ ≤ C * Real.exp (-signedPolygonGap N * signedZeroCenter N m) ∧
279       ∀ w : ℂ, w ∈ closedBall (signedZeroCenter N m : ℂ) (1 / ‖signedZeroFrequency N‖) ∧
280         canonicalSignedDenominator N w = 0 → w = z := by
281   have ha := signedZeroFrequency_ne_zero (show 2 ≤ N by omega)
282   let r := 1 / ‖signedZeroFrequency N‖
283   let C := (3 / 2 : ℝ) * ((N - 2 : ℕ) : ℝ) * Real.exp (signedPolygonGap N * r + 2 * r) /
284     ‖signedZeroFrequency N‖
285   have hC : 0 < C := by
286     dsimp [C]
287     have hn : 0 < N - 2 := by omega
288     have := norm_pos_iff.mpr ha
289     positivity
290   obtain ⟨m0, hm0⟩ := canonicalSignedDenominator_eventual_positive_simple_zeros hN
291   obtain ⟨T, hTr, hT⟩ := signedRemainder_eventually_small_on_disks hN
292     (by positivity : 0 ≤ r) (by norm_num : (0 : ℝ) < 1 / 2) 0
293   let A := Real.pi / Real.sin (Real.pi / N)
294   have hA : 0 < A := div_pos Real.pi_pos (signed_sine_pos (by omega))
295   obtain ⟨m1, hm1⟩ := exists_nat_gt (T / A)
296   refine ⟨C, hC, max m0 m1, ?_⟩
297   intro m hm
298   have hmn : (m1 : ℝ) ≤ m := by exact_mod_cast (le_max_right m0 m1).trans hm
299   have ht : T ≤ signedZeroCenter N m := by
300     have hh := (div_lt_iff₀ hA).mp hm1
301     change T ≤ A * ((m : ℝ) + 1 / 2)
302     nlinarith
303   obtain ⟨z, hz, hz0, hzim, hzpos, hzs, hu⟩ := hm0 m ((le_max_left _ _).trans hm)
304   refine ⟨z, hz, hz0, hzim, hzpos, hzs, ?_, hu⟩
305   exact canonicalSignedDenominator_local_zero_exponential_distance hN (hTr.trans ht)
306     (signedZeroCenter_cancellation (by omega) m) (hT _ ht) hz hz0
307 
308 /-- Every zero with a small normalized remainder is assigned to one lattice center. -/
309 theorem canonicalSignedDenominator_zero_lattice_distance {N : ℕ} (hN : 3 ≤ N)
310     {z : ℂ} (hz : canonicalSignedDenominator N z = 0)
311     (hsmall : ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z‖ ≤ 1 / 2) :
312     ∃! k : ℤ, ‖z - oddExponentialCenter k / signedZeroFrequency N‖ ≤
313       (3 / 2 : ℝ) *
314         ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z‖ /
315           ‖signedZeroFrequency N‖ := by
316   have ha := signedZeroFrequency_ne_zero (show 2 ≤ N by omega)
317   have hz0 := (signed_two_term_zero_iff (show 2 ≤ N by omega)
318     (canonicalPrimitiveRoot N) (canonicalSignedRoot N) z).mp hz
319   change 1 + Complex.exp (signedZeroFrequency N * z) +
320     signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z = 0 at hz0
321   have he : ‖1 + Complex.exp (signedZeroFrequency N * z)‖ =
322       ‖signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z‖ := by
323     have h : 1 + Complex.exp (signedZeroFrequency N * z) =
324         -signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0 z := by
325       linear_combination hz0
326     rw [h, norm_neg]
327   have h := near_cancellation_unique (he.trans_le hsmall)
328   rw [he] at h
329   convert h using 1
330   funext k
331   apply propext
332   have heq : z - oddExponentialCenter k / signedZeroFrequency N =
333       (signedZeroFrequency N * z - oddExponentialCenter k) / signedZeroFrequency N := by
334     field_simp
335   rw [heq, norm_div]
336   exact div_le_div_iff_of_pos_right (norm_pos_iff.mpr ha)
337 
338 end
339 end Komorebi.PaperIV

Back to source controls