theorem
proved
tactic proof
charge_additive
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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. -/