regularFactor_phase_lipschitz

formal source

 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