Cones.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar steps of the refinement update

These are the min/max and first-crossing calculations in Sections 5 and 7 of An Almost-Linear Approximation Scheme for Edit Distance (2026). They are internal lemmas, not the main algorithmic theorem.

def OAI.EditApproximation.refinementUpdate line 17
Source documentation
The nonzero branch of the refinement update, for a nonempty online list. An empty list returns the cone minimum directly.
```
noncomputable def refinementUpdate (δ cone online : ℝ) : ℝ :=
…
```
theorem OAI.EditApproximation.refinementUpdate_sandwich line 20
theorem OAI.EditApproximation.refinementUpdate_div_le line 26

theorem OAI.EditApproximation.refinementUpdate_spatial line 35

Source documentation

The cone sandwich gives the multiplicative spatial regularity, regardless of the independently sampled online values.

theorem refinementUpdate_spatial {δ cone cone' online online' charge : ℝ}
    (hδ : 0 ≤ δ) (hcone' : 0 ≤ cone') (hspatial : cone ≤ cone' + charge) :
    refinementUpdate δ cone online ≤
      (1 + δ) * refinementUpdate δ cone' online' + charge := by
…

Mentions: OAI.EditApproximation.refinementUpdate

theorem OAI.EditApproximation.refinementUpdate_prefix line 46

Source documentation

Prefix step of Proposition prop:node-regret: if the group estimate succeeds, any excess over the sampled action is paid by its decrement.

theorem refinementUpdate_prefix {δ κ cone online action oldAction b c error : ℝ}
    (hδ : 0 < δ) (hκ : 0 ≤ κ) (hc0 : 0 ≤ c) (hb : b ≤ c)
    (hc : c ≤ action) (hmonotone : action ≤ oldAction)
    (honline : online ≤ action) (hbellman : cone ≤ oldAction)
    (hgroup : cone ≤ (1 + δ) * action + error * b)
    (herror : error * b ≤ κ * δ * b) :
    max c (refinementUpdate δ cone online) ≤
      action + κ * (oldAction - action) := by
…

Mentions: OAI.EditApproximation.refinementUpdate

theorem OAI.EditApproximation.refinementUpdate_crossing line 85

Source documentation

The crossing iteration is paid once; later Bellman bounds use the same action and make the clipped regret nonpositive.

theorem refinementUpdate_crossing {δ cone online action c : ℝ}
    (hδ : 0 ≤ δ) (hc : 0 ≤ c) (haction : action < c)
    (hgroup : cone ≤ (1 + δ) * action + δ * c) :
    max c (refinementUpdate δ cone online) ≤ c + 2 * δ * c := by
…

Mentions: OAI.EditApproximation.refinementUpdate

theorem OAI.EditApproximation.clipped_regret_nonpos line 93