charge_additive

formal source

 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| ≤