OAI/Combinatorics/EditApproximation/Binary/IntegerAlgorithm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The uniform algorithm on explicitly stored integer symbols, together with its conditional accuracy theorem. The hypothesis is a finite scalar Bernstein bound for the two computed finite product laws.

  1. def OAI.EditApproximation.ComputedBernsteinInputs line 14
  2. abbrev OAI.EditApproximation.IntegerApproximationOutcome line 23
  3. def OAI.EditApproximation.integerApproximationLaw line 27
  4. def OAI.EditApproximation.integerApproximationAnswer line 32
  5. theorem OAI.EditApproximation.integerApproximationAnswer_equal line 37
  6. theorem OAI.EditApproximation.integerApproximation_conditional_accuracy line 42