QuadraticIteration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the quadratic boundary correction

The constants are the ones used by the cocycle averaging step: defect e improves to 16e², at displacement at most e + 4e².

theorem OAI.KadisonKastler.exists_zero_of_quadratic_improvement line 22

Source documentation

Iterating the quadratic improvement gives an exact solution within 2e, where e ≤ 1/64 is the original defect.

theorem exists_zero_of_quadratic_improvement
    {X : Type*} [MetricSpace X] [CompleteSpace X]
    (d : X → ℝ) (hd : Continuous d) (hd0 : ∀ x, 0 ≤ d x)
    (hstep : ∀ x, d x ≤ 1 / 64 → ∃ y,
      d y ≤ 16 * (d x) ^ 2 ∧ dist x y ≤ d x + 4 * (d x) ^ 2)
    (x₀ : X) (hx₀ : d x₀ ≤ 1 / 64) :
    ∃ y, d y = 0 ∧ dist x₀ y ≤ 2 * d x₀ := by
…