`and`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.CirclePhaseLift
domain: NumberTheory
line: 160 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.CirclePhaseLift on GitHub at line 160.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.