OAI/Combinatorics/EditApproximation/Binary/BinaryBandAction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Materialized Boolean vertices retain their band labels. The resulting selected action, including every tie, is the action used by the online sampler in the accuracy development.

  1. def OAI.EditApproximation.BinaryFraction.labeledBandVerticesWithWork line 13
  2. theorem OAI.EditApproximation.BinaryFraction.labeledBandVerticesWithWork_vectors line 23
  3. theorem OAI.EditApproximation.BinaryFraction.labeledBandVerticesWithWork_values line 30
  4. theorem OAI.EditApproximation.BinaryFraction.labeledBandVerticesWithWork_cost line 49
  5. def OAI.EditApproximation.BinaryFraction.preparedBandActionWithWork line 57
  6. theorem OAI.EditApproximation.BinaryFraction.preparedBandActionWithWork_value line 68
  7. def OAI.EditApproximation.BinaryFraction.preparedBandActionBitBudget line 95
  8. theorem OAI.EditApproximation.BinaryFraction.preparedBandActionWithWork_cost line 101
  9. def OAI.EditApproximation.BinaryFraction.bandActionWithWork line 161
  10. theorem OAI.EditApproximation.BinaryFraction.bandActionWithWork_value line 170
  11. def OAI.EditApproximation.BinaryFraction.bandActionBitBudget line 191
  12. theorem OAI.EditApproximation.BinaryFraction.bandActionWithWork_cost line 196