`zetaDerivedPhaseFamily_sensor`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
domain: NumberTheory
line: 360 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 360.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 357    have := zetaDerivedPhaseData_charge qlf n hn
 358    rw [this, horder, neg_neg]
 359
 360@[simp] theorem zetaDerivedPhaseFamily_sensor
 361    (sensor : DefectSensor) (qlf : QuantitativeLocalFactorization)
 362    (horder : qlf.order = -sensor.charge) :
 363    (zetaDerivedPhaseFamily sensor qlf horder).sensor = sensor := rfl
 364
 365/-- The current `zetaDerivedPhaseFamily` carries a zero-perturbation witness:
 366its sampled increments are exactly the pure winding increments. -/
 367noncomputable def zetaDerivedPhasePerturbationWitness
 368    (sensor : DefectSensor)
 369    (qlf : QuantitativeLocalFactorization)
 370    (horder : qlf.order = -sensor.charge) :
 371    DefectPhasePerturbationWitness (zetaDerivedPhaseFamily sensor qlf horder) where
 372  epsilon := fun _ _ _ => 0
 373  increment_eq := by
 374    intro n hn j
 375    have hnR : (8 * (n : ℝ)) ≠ 0 := by
 376      have hnR' : 0 < (n : ℝ) := by
 377        exact_mod_cast hn
 378      nlinarith
 379    simp [zetaDerivedPhaseFamily, zetaDerivedPhaseData, zetaDerivedPhaseDataBundle,
 380      ContinuousPhaseData.sampleIncrements, defectPhasePureIncrement, horder]
 381    field_simp [hnR]
 382    ring
 383  small := by
 384    intro n hn j
 385    simp
 386  linear_term_bounded := by
 387    refine ⟨0, ?_⟩
 388    intro N
 389    simp
 390  quadratic_term_bounded := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.