OAI/Combinatorics/EditApproximation/Binary/BinaryCellGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The whole-cell grids and nearby cell indices are generated by literal binary quotient, endpoint and bounded-range operations.

  1. theorem OAI.EditApproximation.BinaryFraction.naturalFloorWithWork_value line 16
  2. theorem OAI.EditApproximation.BinaryFraction.naturalFloorWithWork_bounds line 33
  3. theorem OAI.EditApproximation.BinaryFraction.cellCoordinatesWithWork_value line 47
  4. theorem OAI.EditApproximation.BinaryFraction.targetCellsWithWork_value line 55
  5. theorem OAI.EditApproximation.BinaryFraction.cellGridPointsWithWork_value line 63
  6. theorem OAI.EditApproximation.BinaryFraction.cellStatesWithWork_value line 72