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

QuantitativeLocalFactorization

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)

 269structure QuantitativeLocalFactorization extends LocalMeromorphicWitness where
 270  logDerivBound : ℝ
 271  logDerivBound_pos : 0 < logDerivBound
 272  perturbation_regime : logDerivBound * radius ≤ 1
 273
 274/-- On a circle of radius `r` centered at `w.center`, adjacent sample
 275points at angular spacing `2π/(8n)` are separated by arc length
 276`2πr/(8n)`. If the regular factor has log-derivative bounded by `M`,
 277then each phase perturbation satisfies `|ε_j| ≤ M · 2πr/(8n)`. -/

used by (31)

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

… and 1 more

depends on (12)

Lean names referenced from this declaration's body.