OAI/Combinatorics/EditApproximation/Binary/BinaryInitialGridWork.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Construction of every local initial-cone center is charged, including rejected center predicates. The scale test itself bounds the emitted grid.

  1. theorem OAI.EditApproximation.BinaryFraction.dyadicScale_size line 13
  2. theorem OAI.EditApproximation.BinaryFraction.initialGrid_count line 23
  3. theorem OAI.EditApproximation.BinaryFraction.initialScale_radius line 35
  4. def OAI.EditApproximation.BinaryFraction.initialGridScaleBitBudget line 47
  5. theorem OAI.EditApproximation.BinaryFraction.initialGridScale_bounds line 55
  6. def OAI.EditApproximation.BinaryFraction.initialCentersBitBudget line 110
  7. theorem OAI.EditApproximation.BinaryFraction.initialCentersWithWork_bounds line 115
  8. def OAI.EditApproximation.BinaryFraction.initialProgramBitBudget line 171
  9. theorem OAI.EditApproximation.BinaryFraction.initialMinimumBitBudget_mono_count line 175
  10. theorem OAI.EditApproximation.BinaryFraction.initialProgramWithWork_bounds line 180