OAI/Combinatorics/EditApproximation/Binary/BinaryActualBandOptimizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete Boolean band optimizer constructs its envelopes from the stored initial table, then constructs the vertices and history vector. The normalized history bounds follow from actual band-coordinate membership.

  1. theorem OAI.EditApproximation.BinaryFraction.listedBandCoordinateVector_coverage line 15
  2. def OAI.EditApproximation.BinaryFraction.envelopeVectorWithWork line 27
  3. theorem OAI.EditApproximation.BinaryFraction.envelopeVectorWithWork_value line 32
  4. def OAI.EditApproximation.BinaryFraction.bandOptimizerWithWork line 40
  5. theorem OAI.EditApproximation.BinaryFraction.bandOptimizerWithWork_value line 49
  6. def OAI.EditApproximation.BinaryFraction.actualBandOptimizerBitBudget line 70
  7. theorem OAI.EditApproximation.BinaryFraction.bandOptimizerWithWork_cost line 75