OAI/Combinatorics/EditApproximation/Binary/IntegerBinaryAccuracy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.integerBinaryAnswer line 10

   Source documentation

   The uniform implementation uses exact dynamic programming below the proved cutoff and the evaluated binary memo above it.

   noncomputable def integerBinaryAnswer (source target : List ℤ) (N : ℕ) (epsilon : BinaryFraction)
       (outcome : ComputedFullOutcome (source.map integerSymbolCode) (target.map integerSymbolCode) N) : ℕ :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.ComputedFullOutcome, OAI.EditApproximation.integerSymbolCode

2. theorem OAI.EditApproximation.integerBinaryAnswer_large line 19
3. theorem OAI.EditApproximation.integerBinaryAnswer_equal line 30
4. theorem OAI.EditApproximation.integerBinaryAnswer_conditional_accuracy line 46

   Source documentation

   Accuracy of the concrete binary answer under the finite Bernstein hypothesis for the reference algorithm.

   theorem integerBinaryAnswer_conditional_accuracy (source target : List ℤ) (N : ℕ)
       (epsilon : BinaryFraction) (hepsilon : 0 < epsilon.value)
       (hsize : source.length + target.length ≤ N) (bernstein : ComputedBernsteinInputs 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} := by
   …

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