RegularFactorPhase

formal source

 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 : ℝ → ℝ)