OAI/Combinatorics/EditApproximation/Binary/BinaryGroupReadCosts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact group score scans charge the finite-buffer readers through the same loops as their arithmetic-only counterparts.

  1. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork_factor line 12
  2. theorem OAI.EditApproximation.BinaryFraction.selectGroupWithWork_factor line 38
  3. theorem OAI.EditApproximation.BinaryFraction.unskippedEstimateReadWithWork_factor line 69
  4. theorem OAI.EditApproximation.BinaryFraction.chooseUnskippedReadWithWork_factor line 97
  5. theorem OAI.EditApproximation.BinaryFraction.sampledGroupActionReadWithWork_factor line 110