def
definition
def or abbrev
qlf_regularFactorPhase
show as:
view Lean formalization →
formal statement (Lean)
457noncomputable def qlf_regularFactorPhase
458 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
459 RegularFactorPhase := by
proof body
Definition body.
460 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
461 have hd : (0 : ℝ) < ↑n + 1 := by linarith
462 have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
463 exact regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
464 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
465 qlf.logDerivBound qlf.logDerivBound_pos
466
467/-- A defect phase family using genuine regular-factor phase data.
468Each level carries non-trivial perturbation from the regular factor's
469Lipschitz-controlled phase, unlike the synthetic `zetaDerivedPhaseFamily`
470which has identically zero perturbation. -/