OAI/Combinatorics/EditApproximation/Binary/BinaryUnskippedReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The accepted-band record is built from the reader-aware tests. Only proof fields are erased; numerical tests and reads remain charged.

  1. theorem OAI.EditApproximation.BinaryFraction.rounded_action_congr line 13
  2. def OAI.EditApproximation.BinaryFraction.preparedUnskippedReadWithWork line 20
  3. theorem OAI.EditApproximation.BinaryFraction.preparedUnskippedReadWithWork_value line 60
  4. theorem OAI.EditApproximation.BinaryFraction.preparedUnskippedReadWithWork_cost line 86