OAI/Combinatorics/EditApproximation/Binary/BinaryWideChildWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every child-grid list is constructed before the Cartesian product. These bounds include the balanced endpoints, integer spacing and radius, endpoint translations, and the two bounded grid loops.

  1. theorem OAI.EditApproximation.seedGridSpacingWithWork_bounds line 11
  2. theorem OAI.EditApproximation.gridStateBoxBitBudget_mono_count line 34
  3. def OAI.EditApproximation.wideChildGridBitBudget line 39
  4. theorem OAI.EditApproximation.wideChildGridWithWork_cost line 42