mkRegularFactorPhase

formal source

 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)