zetaDerivedPhaseDataBundle

formal source

 310/-- Phase data on the `n`th circle of a meromorphic factorization, at
 311radius `r₀/(n+1)`. Bundles the `ContinuousPhaseData` with a proof that
 312its charge equals `-order`, extracted from `meromorphic_phase_charge`. -/
 313private noncomputable def zetaDerivedPhaseDataBundle
 314    (qlf : QuantitativeLocalFactorization) (n : ℕ) (_hn : 0 < n) :
 315    { cpd : ContinuousPhaseData // cpd.charge = -qlf.order } := by
 316  have hd : (0 : ℝ) < ↑n + 1 := by linarith
 317  refine ⟨{
 318    center := qlf.center
 319    radius := qlf.radius / (↑n + 1)
 320    radius_pos := div_pos qlf.radius_pos hd
 321    phase := fun θ => (qlf.order : ℝ) * θ
 322    phase_continuous := by
 323      simpa using (continuous_const.mul continuous_id)
 324    charge := -qlf.order
 325    phase_winding := by
 326      simp [sub_eq_add_neg, Int.cast_neg]
 327      ring
 328    }, rfl⟩
 329
 330private noncomputable def zetaDerivedPhaseData
 331    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 332    ContinuousPhaseData :=
 333  (zetaDerivedPhaseDataBundle qlf n hn).val
 334
 335private theorem zetaDerivedPhaseData_charge
 336    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 337    (zetaDerivedPhaseData qlf n hn).charge = -qlf.order :=
 338  (zetaDerivedPhaseDataBundle qlf n hn).property
 339
 340/-- A defect phase family derived from an actual `QuantitativeLocalFactorization`
 341of a meromorphic function near a pole/zero.
 342
 343Unlike `trivialDefectPhaseFamily` (which uses constant-phase scaffolding),