regularFactorPhaseFromWitness

formal source

 399
 400The caller provides `M` (a bound on `|g'/g|` over the disk). The
 401resulting `logDerivBound = M * r` (chain rule). -/
 402noncomputable def regularFactorPhaseFromWitness
 403    (w : LocalMeromorphicWitness) (r : ℝ) (hr : 0 < r) (hrw : r < w.radius)
 404    (M : ℝ) (hM : 0 < M) :
 405    RegularFactorPhase :=
 406  mkRegularFactorPhase
 407    w.regularFactor w.center w.radius r
 408    w.radius_pos hr hrw
 409    w.regularFactor_diff w.regularFactor_nz
 410    M hM
 411
 412/-- Phase data using the genuine regular factor phase: combines pole winding
 413with the Lipschitz-controlled regular-factor phase from the covering-space
 414lift, producing non-trivial perturbation data.
 415
 416Unlike `zetaDerivedPhaseDataBundle` (which uses synthetic linear phase),
 417this construction passes through `charge_additive` to combine:
 418- pole factor: charge = -order, phase = order * θ
 419- regular factor: charge = 0, phase = genuine covering-space lift -/
 420private noncomputable def genuineZetaDerivedPhaseData
 421    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 422    ContinuousPhaseData :=
 423  let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 424  let hd : (0 : ℝ) < ↑n + 1 := by linarith
 425  let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
 426  let hr : 0 < qlf.radius / (↑n + 1) := div_pos qlf.radius_pos hd
 427  let hrw : qlf.radius / (↑n + 1) < qlf.radius :=
 428    div_lt_self qlf.radius_pos hgt1
 429  let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
 430    (qlf.radius / (↑n + 1)) hr hrw qlf.logDerivBound qlf.logDerivBound_pos
 431  { center := qlf.center
 432    radius := qlf.radius / (↑n + 1)