pith. machine review for the scientific record. sign in
def definition def or abbrev

zetaDerivedPhasePerturbationWitness

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Definition body.

 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
 391    refine ⟨0, ?_⟩
 392    intro N
 393    simp
 394
 395/-! ### §5a. Genuine phase family using regular-factor phase -/
 396
 397/-- Build a `RegularFactorPhase` directly from a `LocalMeromorphicWitness`
 398using the regular factor's analytic and nonvanishing properties.
 399
 400The caller provides `M` (a bound on `|g'/g|` over the disk). The
 401resulting `logDerivBound = M * r` (chain rule). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.