pith. machine review for the scientific record. sign in
theorem proved term proof

epsilon_abs_bound

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)

 510theorem epsilon_abs_bound
 511    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
 512    |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| ≤
 513      qlf.logDerivBound * (qlf.radius / (↑n + 1)) * (2 * π / (8 * ↑n)) := by

proof body

Term-mode proof.

 514  exact (genuineRegularFactorPhaseAt qlf n hn).increment_bound n hn j
 515
 516/-- At the genuine phase family, `|ε| ≤ M * R / (n+1) * π / (4n)`, and
 517with `perturbation_regime` this is `≤ π / (4n(n+1)) ≤ π/8 < 1`.
 518So `|log(φ) * ε| < 1 * 1 = 1`. -/

used by (3)

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

depends on (12)

Lean names referenced from this declaration's body.