AlmostLinear.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform binary approximation scheme for edit distance. The finite Bernstein inequality supplies the concentration bounds for the initial estimator and the refinement samples.

theorem OAI.EditApproximation.computedBernsteinInputs line 14
Source documentation
Finite product-measure concentration for the initial estimator and refinement.
```
theorem computedBernsteinInputs (N : ℕ) : ComputedBernsteinInputs N := by
…
```
Mentions: OAI.EditApproximation.ComputedBernsteinInputs

theorem OAI.EditApproximation.almostLinearEditDistance line 22

Source documentation

A uniform almost-linear approximation scheme. The same binary algorithm satisfies the approximation, equality, expected-work and space bounds.

theorem almostLinearEditDistance (epsilon : BinaryFraction)
    (hepsilon : 0 < epsilon.value) (_hepsilonOne : epsilon.value < 1)
    :
    (∀ (source target : List ℤ) (N : ℕ), source.length + target.length ≤ N →
      (2 / 3 : ℝ) ≤ (computedFullLaw (source.map integerSymbolCode) (target.map integerSymbolCode) N epsilon).real
        {outcome | EditDistortion.edit source target ≤ integerBinaryAnswer source target N epsilon outcome ∧
          (integerBinaryAnswer source target N epsilon outcome : ℝ) ≤
            (1 + (epsilon.value : ℝ)) * EditDistortion.edit source target}) ∧
    (∀ (source target : List ℤ) (N : ℕ), source = target → ∀ outcome,
      integerBinaryAnswer source target N epsilon outcome = 0) ∧
    (∀ (C : ℕ) (eta : ℝ), 0 < eta → ∀ᶠ N : ℕ in atTop,
      ∀ source target : List ℤ, source.length + target.length ≤ N →
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.computedFullLaw, OAI.EditApproximation.integerSymbolCode, OAI.EditDistortion.edit, OAI.EditApproximation.integerBinaryAnswer