pith. machine review for the scientific record. sign in
def definition def or abbrev

genuineRegularFactorPhaseAt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 486noncomputable def genuineRegularFactorPhaseAt
 487    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 488    RegularFactorPhase :=

proof body

Definition body.

 489  let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 490  let hd : (0 : ℝ) < ↑n + 1 := by linarith
 491  let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
 492  regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
 493    (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
 494    qlf.logDerivBound qlf.logDerivBound_pos
 495
 496/-- The log-derivative bound of the genuine regular factor phase at level `n`
 497is definitionally `qlf.logDerivBound * (qlf.radius / (n + 1))`.
 498
 499This is the critical identity that connects the analytic input
 500(`QuantitativeLocalFactorization.logDerivBound`) to the phase-level
 501Lipschitz constant, enabling discharge of perturbation-witness bounds. -/

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.