OAI/Combinatorics/EditApproximation/Binary/BinaryLocalRepresentativeWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complete bit work of the query-local scale and center loops. The one-dimensional grid size follows from the tested scale inequality.

  1. def OAI.EditApproximation.BinaryFraction.queryExponentsBitBudget line 14
  2. theorem OAI.EditApproximation.BinaryFraction.queryExponentsWithWork_bounds line 17
  3. theorem OAI.EditApproximation.BinaryFraction.query_grid_count line 58
  4. def OAI.EditApproximation.BinaryFraction.localRepresentativeScaleBitBudget line 70
  5. def OAI.EditApproximation.BinaryFraction.localRepresentativesBitBudget line 76
  6. theorem OAI.EditApproximation.BinaryFraction.localRepresentativesWithWork_cost line 80