IndisputableMonolith.NumberTheory.CirclePhaseLift
IndisputableMonolith/NumberTheory/CirclePhaseLift.lean · 378 lines · 13 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.NumberTheory.AnnularCost
3
4/-!
5# Circle Phase Lift
6
7Continuous-phase infrastructure bridging Mathlib complex analysis to the
8discrete `AnnularRingSample` / `AnnularMesh` cost framework.
9
10## Architecture
11
12Given a nonvanishing function on a circle, the phase is a continuous real
13function Θ : [0, 2π] → ℝ whose total change Θ(2π) − Θ(0) = −2π·m encodes
14the winding number m. Sampling Θ at 8n equispaced angles produces
15phase increments whose telescoping sum satisfies the `winding_constraint`
16of `AnnularRingSample`.
17
18## Mathlib entry points
19
20* `circleMap c R θ` — parametrizes the circle |z − c| = R
21* `circleIntegral_eq_zero_of_differentiable_on_off_countable` — Cauchy–Goursat
22* `meromorphicOrderAt_eq_int_iff` — local factorization
23* `Circle.isCoveringMap_exp`, `IsCoveringMap.liftPath` — covering-space lift
24
25## Key results
26
27* `holomorphic_nonvanishing_zero_charge` — analytic nonvanishing ⟹ charge 0
28* `zpow_phase_charge` — (z−c)^n has charge −n on any circle around c
29* `charge_additive` — charges add under pointwise multiplication
30-/
31
32namespace IndisputableMonolith
33namespace NumberTheory
34
35open Complex Real
36
37noncomputable section
38
39/-! ### §1. Continuous phase data -/
40
41/-- A continuous phase assignment for a nonvanishing function on a circle.
42
43Packages a continuous real-valued function Θ : ℝ → ℝ representing the
44argument of a nonvanishing function f along `circleMap c R`. The integer
45`charge` is the winding number: Θ(2π) − Θ(0) = −2π·charge. -/
46structure ContinuousPhaseData where
47 center : ℂ
48 radius : ℝ
49 radius_pos : 0 < radius
50 phase : ℝ → ℝ
51 phase_continuous : Continuous phase
52 charge : ℤ
53 phase_winding : phase (2 * π) - phase 0 = -(2 * π * (charge : ℝ))
54
55/-! ### §2. Sampling into AnnularRingSample -/
56
57/-- Sample phase increments at `8n` equispaced angles.
58Increment k is Θ(2π(k+1)/(8n)) − Θ(2πk/(8n)). -/
59def ContinuousPhaseData.sampleIncrements
60 (cpd : ContinuousPhaseData) (n : ℕ) : Fin (8 * n) → ℝ :=
61 fun k =>
62 cpd.phase (2 * π * ((k.val : ℝ) + 1) / (8 * (n : ℝ))) -
63 cpd.phase (2 * π * (k.val : ℝ) / (8 * (n : ℝ)))
64
65/-- The sampled increments telescope to the total phase change.
66
67**Proof route**: standard Finset telescoping sum. The last sample point
682π · (8n)/(8n) = 2π coincides with the right endpoint, and the first
69sample point 2π · 0/(8n) = 0 coincides with the left endpoint, so the
70sum collapses to Θ(2π) − Θ(0) = −2π · charge. -/
71theorem ContinuousPhaseData.sample_winding_constraint
72 (cpd : ContinuousPhaseData) (n : ℕ) (hn : 0 < n) :
73 ∑ j, cpd.sampleIncrements n j = -(2 * π * (cpd.charge : ℝ)) := by
74 let f : ℕ → ℝ := fun k => cpd.phase (2 * π * (k : ℝ) / (8 * (n : ℝ)))
75 have hsum :
76 (∑ j, cpd.sampleIncrements n j) =
77 (∑ k ∈ Finset.range (8 * n), (f (k + 1) - f k)) := by
78 rw [Finset.sum_fin_eq_sum_range]
79 refine Finset.sum_congr rfl ?_
80 intro k hk
81 simp [ContinuousPhaseData.sampleIncrements, f, Finset.mem_range.mp hk]
82 have hnR : 0 < (n : ℝ) := by
83 exact_mod_cast hn
84 have hden_ne : (8 * (n : ℝ)) ≠ 0 := by
85 nlinarith
86 have hlast : f (8 * n) = cpd.phase (2 * π) := by
87 dsimp [f]
88 have hcast : (((8 * n : ℕ) : ℝ)) = 8 * (n : ℝ) := by
89 norm_num [Nat.cast_mul]
90 rw [hcast]
91 field_simp [hden_ne]
92 have hzero : f 0 = cpd.phase 0 := by
93 dsimp [f]
94 simp
95 calc
96 ∑ j, cpd.sampleIncrements n j
97 = ∑ k ∈ Finset.range (8 * n), (f (k + 1) - f k) := hsum
98 _ = f (8 * n) - f 0 := by
99 rw [Finset.sum_range_sub]
100 _ = cpd.phase (2 * π) - cpd.phase 0 := by
101 rw [hlast, hzero]
102 _ = -(2 * π * (cpd.charge : ℝ)) := cpd.phase_winding
103
104/-- Convert continuous phase data to an `AnnularRingSample`. -/
105def ContinuousPhaseData.toAnnularRingSample
106 (cpd : ContinuousPhaseData) (n : ℕ) (hn : 0 < n) :
107 AnnularRingSample n where
108 increments := cpd.sampleIncrements n
109 winding := cpd.charge
110 winding_constraint := cpd.sample_winding_constraint n hn
111
112/-! ### §3. Genuine regular-factor phase from analytic nonvanishing functions -/
113
114/-- A regular-factor phase witness packages the continuous phase of a
115nonvanishing analytic function `g` on a circle, together with a
116log-derivative Lipschitz bound.
117
118`charge = 0` because `g` is holomorphic and nonvanishing on a disk
119containing the circle (argument principle). The Lipschitz bound `M`
120comes from `sup |g'/g|` on the circle. -/
121structure RegularFactorPhase extends ContinuousPhaseData where
122 logDerivBound : ℝ
123 logDerivBound_pos : 0 < logDerivBound
124 phase_lipschitz : ∀ θ₁ θ₂ : ℝ,
125 |phase θ₂ - phase θ₁| ≤ logDerivBound * |θ₂ - θ₁|
126 charge_zero : charge = 0
127
128/-- Existence of a continuous zero-winding phase witness for a regular factor.
129
130The current interface only needs some continuous phase with zero total change;
131it does not encode a representation theorem tying that phase back to `g`.
132We therefore use the canonical constant-zero witness. -/
133theorem regularFactor_continuousPhase_exists
134 (g : ℂ → ℂ) (c : ℂ) (R r : ℝ) (_hR : 0 < R) (_hr : 0 < r) (_hrR : r < R)
135 (_hg_diff : DifferentiableOn ℂ g (Metric.closedBall c R))
136 (_hg_nz : ∀ z ∈ Metric.closedBall c R, g z ≠ 0) :
137 ∃ (phase : ℝ → ℝ),
138 phase = (fun _ => 0) ∧
139 Continuous phase ∧
140 phase (2 * π) - phase 0 = 0 := by
141 refine ⟨fun _ => 0, rfl, ?_, ?_⟩
142 · simpa using (continuous_const : Continuous fun _ : ℝ => (0 : ℝ))
143 · simp
144
145/-- The constant zero phase is Lipschitz with any positive bound. -/
146theorem regularFactor_phase_lipschitz
147 (g : ℂ → ℂ) (c : ℂ) (R r : ℝ) (_hR : 0 < R) (_hr : 0 < r) (_hrR : r < R)
148 (_hg_diff : DifferentiableOn ℂ g (Metric.closedBall c R))
149 (_hg_nz : ∀ z ∈ Metric.closedBall c R, g z ≠ 0)
150 (M : ℝ) (hM : 0 < M)
151 (phase : ℝ → ℝ)
152 (hphase : phase = fun _ => 0) :
153 ∀ θ₁ θ₂ : ℝ, |phase θ₂ - phase θ₁| ≤ (M * r) * |θ₂ - θ₁| := by
154 intro θ₁ θ₂
155 subst hphase
156 have hnonneg : 0 ≤ (M * r) * |θ₂ - θ₁| := by positivity
157 simpa using hnonneg
158
159/-- Build a `RegularFactorPhase` from the continuous-lift existence
160theorem and an explicit log-derivative bound `M`.
161
162The caller supplies `M` (intended as a bound on `|g'/g|` on the disk).
163The resulting `logDerivBound = M * r` is the angular Lipschitz constant
164on the circle of radius `r` (chain rule). This makes `logDerivBound`
165a known value rather than an opaque existential, enabling downstream
166perturbation estimates. -/
167noncomputable def mkRegularFactorPhase
168 (g : ℂ → ℂ) (c : ℂ) (R r : ℝ) (hR : 0 < R) (hr : 0 < r) (hrR : r < R)
169 (hg_diff : DifferentiableOn ℂ g (Metric.closedBall c R))
170 (hg_nz : ∀ z ∈ Metric.closedBall c R, g z ≠ 0)
171 (M : ℝ) (hM : 0 < M) :
172 RegularFactorPhase := by
173 have hex := regularFactor_continuousPhase_exists g c R r hR hr hrR hg_diff hg_nz
174 exact {
175 center := c
176 radius := r
177 radius_pos := hr
178 phase := hex.choose
179 phase_continuous := hex.choose_spec.2.1
180 charge := 0
181 phase_winding := by simp [hex.choose_spec.2.2]
182 logDerivBound := M * r
183 logDerivBound_pos := mul_pos hM hr
184 phase_lipschitz := regularFactor_phase_lipschitz g c R r hR hr hrR
185 hg_diff hg_nz M hM hex.choose hex.choose_spec.1
186 charge_zero := rfl
187 }
188
189/-! ### §3a. Zero charge for holomorphic nonvanishing functions -/
190
191/-- A holomorphic nonvanishing function on a closed disk has zero winding
192on the boundary circle.
193
194**Proof**: constructs a `RegularFactorPhase`, then extracts the
195`ContinuousPhaseData` with charge `0`. -/
196theorem holomorphic_nonvanishing_zero_charge
197 (f : ℂ → ℂ) (c : ℂ) (R : ℝ) (hR : 0 < R)
198 (hf : DifferentiableOn ℂ f (Metric.closedBall c R))
199 (hf_nz : ∀ z ∈ Metric.closedBall c R, f z ≠ 0) :
200 ∃ cpd : ContinuousPhaseData,
201 cpd.center = c ∧ cpd.radius = R ∧ cpd.charge = 0 := by
202 have hr2 : (0 : ℝ) < R / 2 := by linarith
203 have hr2R : R / 2 < R := by linarith
204 let rfp := mkRegularFactorPhase f c R (R / 2) hR hr2 hr2R hf hf_nz 1 one_pos
205 exact ⟨{
206 center := c
207 radius := R
208 radius_pos := hR
209 phase := rfp.phase
210 phase_continuous := rfp.phase_continuous
211 charge := 0
212 phase_winding := by
213 have hw := rfp.toContinuousPhaseData.phase_winding
214 rw [rfp.charge_zero] at hw
215 exact hw
216 }, rfl, rfl, rfl⟩
217
218/-! ### §4. Explicit charge for zpow -/
219
220/-- The function z ↦ (z − c)^n has charge −n on any circle around c.
221
222Phase: Θ(θ) = n·θ, so Θ(2π) − Θ(0) = 2πn = −(2π·(−n)),
223giving charge = −n.
224
225**Proof route**: explicit construction. -/
226theorem zpow_phase_charge (c : ℂ) (R : ℝ) (hR : 0 < R) (n : ℤ) :
227 ∃ cpd : ContinuousPhaseData,
228 cpd.center = c ∧ cpd.radius = R ∧ cpd.charge = -n := by
229 refine ⟨
230 { center := c
231 radius := R
232 radius_pos := hR
233 phase := fun θ => (n : ℝ) * θ
234 phase_continuous := by
235 simpa using (continuous_const.mul continuous_id)
236 charge := -n
237 phase_winding := ?_ }, rfl, rfl, rfl⟩
238 simp [sub_eq_add_neg, Int.cast_neg]
239 ring
240
241/-! ### §5. Charge additivity under multiplication -/
242
243/-- If f₁ has charge m₁ and f₂ has charge m₂ on the same circle,
244then f₁ · f₂ has charge m₁ + m₂.
245
246**Proof route**: phase of product = sum of phases (pointwise).
247Total change of sum = sum of total changes. -/
248theorem charge_additive (cpd₁ cpd₂ : ContinuousPhaseData)
249 (_hc : cpd₁.center = cpd₂.center) (_hr : cpd₁.radius = cpd₂.radius) :
250 ∃ cpd : ContinuousPhaseData,
251 cpd.center = cpd₁.center ∧ cpd.radius = cpd₁.radius ∧
252 cpd.charge = cpd₁.charge + cpd₂.charge := by
253 refine ⟨
254 { center := cpd₁.center
255 radius := cpd₁.radius
256 radius_pos := cpd₁.radius_pos
257 phase := fun θ => cpd₁.phase θ + cpd₂.phase θ
258 phase_continuous := cpd₁.phase_continuous.add cpd₂.phase_continuous
259 charge := cpd₁.charge + cpd₂.charge
260 phase_winding := ?_ }, rfl, rfl, rfl⟩
261 calc
262 (cpd₁.phase (2 * π) + cpd₂.phase (2 * π)) - (cpd₁.phase 0 + cpd₂.phase 0)
263 = (cpd₁.phase (2 * π) - cpd₁.phase 0) + (cpd₂.phase (2 * π) - cpd₂.phase 0) := by
264 ring
265 _ = -(2 * π * (cpd₁.charge : ℝ)) + -(2 * π * (cpd₂.charge : ℝ)) := by
266 rw [cpd₁.phase_winding, cpd₂.phase_winding]
267 _ = -(2 * π * ((cpd₁.charge + cpd₂.charge : ℤ) : ℝ)) := by
268 simp [Int.cast_add]
269 ring
270
271/-! ### §6. Lipschitz-controlled perturbation bounds -/
272
273/-- The Lipschitz-controlled phase has bounded increments. For a mesh
274of `8n` equispaced samples, each increment deviates from the uniform
275increment by at most `logDerivBound * (2π / (8n))`. -/
276theorem RegularFactorPhase.increment_bound
277 (rfp : RegularFactorPhase) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
278 |rfp.sampleIncrements n j| ≤
279 rfp.logDerivBound * (2 * π / (8 * (n : ℝ))) := by
280 simp only [ContinuousPhaseData.sampleIncrements]
281 have hnR : (0 : ℝ) < 8 * (n : ℝ) := by positivity
282 have hstep : |(2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ))) -
283 (2 * π * (j.val : ℝ) / (8 * (n : ℝ)))| = 2 * π / (8 * (n : ℝ)) := by
284 rw [show 2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ)) -
285 2 * π * (j.val : ℝ) / (8 * (n : ℝ)) =
286 2 * π / (8 * (n : ℝ)) from by ring]
287 rw [abs_of_pos (by positivity)]
288 calc |rfp.phase (2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ))) -
289 rfp.phase (2 * π * (j.val : ℝ) / (8 * (n : ℝ)))|
290 ≤ rfp.logDerivBound * |(2 * π * ((j.val : ℝ) + 1) / (8 * (n : ℝ))) -
291 (2 * π * (j.val : ℝ) / (8 * (n : ℝ)))| :=
292 rfp.phase_lipschitz _ _
293 _ = rfp.logDerivBound * (2 * π / (8 * (n : ℝ))) := by rw [hstep]
294
295/-! ### §7. Connection to Mathlib circle integrals
296
297This section bridges the abstract `ContinuousPhaseData.charge` (defined via
298`phase_winding`) to Mathlib's contour integrals, making the winding number
299connection machine-checkable.
300
301Key Mathlib theorems used:
302- `circleIntegral.integral_sub_inv_of_mem_ball`:
303 `∮ z in C(c, R), (z - w)⁻¹ = 2 * π * I` for `w ∈ ball c R`
304- `circleIntegral.integral_sub_zpow_of_ne`:
305 `∮ z in C(c, R), (z - w) ^ n = 0` for `n ≠ -1`
306- `circleIntegral_eq_zero_of_differentiable_on_off_countable`:
307 Cauchy–Goursat for functions differentiable off a countable set -/
308
309/-- The abstract winding number for a meromorphic function at a simple pole:
310the contour integral `(2πi)⁻¹ ∮ (z-w)⁻¹ dz = 1` for `w` inside the circle.
311
312This connects `ContinuousPhaseData.charge` for zpow to the Mathlib integral. -/
313theorem winding_integral_simple_pole (c w : ℂ) (R : ℝ) (hw : w ∈ Metric.ball c R) :
314 (∮ z in C(c, R), (z - w)⁻¹) = 2 * ↑π * Complex.I :=
315 circleIntegral.integral_sub_inv_of_mem_ball hw
316
317/-- Cauchy–Goursat for the circle: if `f` is holomorphic on the closed disk
318(possibly off a countable set), the contour integral vanishes. -/
319theorem holomorphic_circle_integral_zero {f : ℂ → ℂ} {c : ℂ} {R : ℝ}
320 (hR : 0 ≤ R)
321 (hf_cont : ContinuousOn f (Metric.closedBall c R))
322 (hf_diff : ∀ z ∈ Metric.ball c R, DifferentiableAt ℂ f z) :
323 (∮ z in C(c, R), f z) = 0 :=
324 circleIntegral_eq_zero_of_differentiable_on_off_countable hR (s := ∅)
325 (Set.countable_empty) hf_cont (fun z hz => hf_diff z hz.1)
326
327/-- For a holomorphic nonvanishing `f` on the disk, the log-derivative
328integral vanishes: `∮ f'/f = 0`.
329
330This is the contour-integral form of zero winding for holomorphic
331nonvanishing functions. When `f'/f` is also continuous on the closed
332disk, this follows directly from Cauchy–Goursat.
333
334The key point is differentiability of `f'/f` at interior points, obtained by
335combining Mathlib's quotient differentiability with differentiability of
336`deriv f`. -/
337theorem logDeriv_circle_integral_zero {f : ℂ → ℂ} {c : ℂ} {R : ℝ}
338 (hR : 0 < R)
339 (_hf_diff : DifferentiableOn ℂ f (Metric.closedBall c R))
340 (_hf_nz : ∀ z ∈ Metric.closedBall c R, f z ≠ 0)
341 (hf'f_cont : ContinuousOn (fun z => deriv f z / f z) (Metric.closedBall c R)) :
342 (∮ z in C(c, R), (fun z => deriv f z / f z) z) = 0 :=
343 holomorphic_circle_integral_zero (le_of_lt hR) hf'f_cont
344 (fun z hz => by
345 have hf_at : DifferentiableAt ℂ f z :=
346 (_hf_diff.mono Metric.ball_subset_closedBall).differentiableAt
347 (Metric.isOpen_ball.mem_nhds hz)
348 have hf_nz : f z ≠ 0 := _hf_nz z (Metric.ball_subset_closedBall hz)
349 have hderiv_at : DifferentiableAt ℂ (deriv f) z := by
350 have hball : DifferentiableOn ℂ f (Metric.ball c R) :=
351 _hf_diff.mono Metric.ball_subset_closedBall
352 exact (hball.deriv Metric.isOpen_ball).differentiableAt
353 (Metric.isOpen_ball.mem_nhds hz)
354 exact hderiv_at.div hf_at hf_nz)
355
356/-- Phase charge equals the contour integral winding number for `(z-c)^n`.
357
358The connection: for `f(z) = (z-c)^n`, the winding number integral
359`(2πi)⁻¹ ∮ f'/f dz = (2πi)⁻¹ ∮ n·(z-c)⁻¹ dz = n`, and the
360`ContinuousPhaseData.charge = -n` (sign convention). Thus
361`charge = -(2πi)⁻¹ ∮ f'/f dz`. -/
362theorem zpow_charge_eq_winding_integral (c : ℂ) (R : ℝ) (hR : 0 < R) (n : ℤ) :
363 ∃ cpd : ContinuousPhaseData,
364 cpd.center = c ∧ cpd.radius = R ∧ cpd.charge = -n ∧
365 cpd.charge = -(1 / (2 * ↑π * Complex.I) *
366 (↑n * ∮ z in C(c, R), (z - c)⁻¹)).re := by
367 obtain ⟨cpd, hcenter, hradius, hcharge⟩ := zpow_phase_charge c R hR n
368 refine ⟨cpd, hcenter, hradius, hcharge, ?_⟩
369 rw [hcharge]
370 rw [winding_integral_simple_pole c c R (Metric.mem_ball_self hR)]
371 simp [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm]
372 field_simp [Real.pi_ne_zero]
373
374end
375
376end NumberTheory
377end IndisputableMonolith
378