OAI/Combinatorics/EditApproximation/Binary/BinaryCellGridWork.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Word-size bounds for the literal whole-cell index scans. The cardinalities here are the emitted local ranges, not the target length.

  1. theorem OAI.EditApproximation.BinaryFraction.naturalWordSize_le line 13
  2. def OAI.EditApproximation.BinaryFraction.cellCoordinateSetupBitBudget line 16
  3. theorem OAI.EditApproximation.BinaryFraction.cellCoordinatesWithWork_bounds line 19
  4. theorem OAI.EditApproximation.BinaryFraction.cellCoordinatesWithWork_cost line 94
  5. def OAI.EditApproximation.BinaryFraction.targetCellsBitBudget line 100
  6. theorem OAI.EditApproximation.BinaryFraction.targetCellsWithWork_cost line 103
  7. theorem OAI.EditApproximation.BinaryFraction.targetCellsWithWork_keys line 140
  8. def OAI.EditApproximation.BinaryFraction.cellGridSetupBitBudget line 155
  9. def OAI.EditApproximation.BinaryFraction.cellGridPointBitBudget line 157
  10. def OAI.EditApproximation.BinaryFraction.cellGridPointsBitBudget line 159
  11. theorem OAI.EditApproximation.BinaryFraction.cellGridPointsWithWork_bounds line 162
  12. theorem OAI.EditApproximation.BinaryFraction.cellGridPointsWithWork_cost line 267
  13. def OAI.EditApproximation.BinaryFraction.cellStatesBitBudget line 274
  14. theorem OAI.EditApproximation.BinaryFraction.cellStatesWithWork_cost line 278