OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedLocalGroupWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bit work of the literal query-local whole-cell loops. The tested scale inequality bounds both coordinate ranges; every generated cell invokes the complete counted band and sampled-action routine.

  1. theorem OAI.EditApproximation.BinaryFraction.queryCellCoordinates_length line 14
  2. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleBitBudget line 35
  3. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleWithWork_cost line 43
  4. theorem OAI.EditApproximation.BinaryFraction.flatMap_cost_sum line 153
  5. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupsBitBudget line 166
  6. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsWithWork_cost line 173