OAI/Combinatorics/EditApproximation/Binary/BinaryGroupReads.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Group estimates and the ordered minimizing scan retain finite-table lookup costs, using Fin-indexed source arrays.

  1. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork_extra line 12
  2. theorem OAI.EditApproximation.BinaryFraction.selectGroupWithWork_extra line 32
  3. def OAI.EditApproximation.BinaryFraction.unskippedEstimateReadWithWork line 62
  4. theorem OAI.EditApproximation.BinaryFraction.unskippedEstimateReadWithWork_eq_cost line 70
  5. def OAI.EditApproximation.BinaryFraction.chooseUnskippedReadWithWork line 95
  6. theorem OAI.EditApproximation.BinaryFraction.chooseUnskippedReadWithWork_eq_cost line 99