OAI/Combinatorics/EditApproximation/Coarse/CoarseCellBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork_bounds line 8
  2. theorem OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork_bounds line 27
  3. theorem OAI.EditApproximation.BinaryFraction.coarseGridCell_mono line 45
  4. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipMinimum_property line 49
  5. theorem OAI.EditApproximation.BinaryFraction.coarseGridPenaltyWithWork_bounds line 69
  6. theorem OAI.EditApproximation.BinaryFraction.coarseContributionWithWork_bounds line 80