def
definition
zetaDerivedPhaseData
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 330.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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),
344this construction extracts genuine phase data from `meromorphic_phase_charge`
345on circles of decreasing radius `r₀/(n+1)` around the factorization center.
346The charge on each circle equals `-order`, which for `zetaReciprocal` at a
347zero of ζ with multiplicity `m` gives charge `m = sensor.charge`. -/
348noncomputable def zetaDerivedPhaseFamily
349 (sensor : DefectSensor)
350 (qlf : QuantitativeLocalFactorization)
351 (horder : qlf.order = -sensor.charge) : DefectPhaseFamily where
352 sensor := sensor
353 witnessRadius := qlf.radius
354 witnessRadius_pos := qlf.radius_pos
355 phaseAtLevel n hn := zetaDerivedPhaseData qlf n hn
356 charge_uniform n hn := by
357 have := zetaDerivedPhaseData_charge qlf n hn
358 rw [this, horder, neg_neg]
359
360@[simp] theorem zetaDerivedPhaseFamily_sensor