OAI/Combinatorics/EditApproximation/Binary/BinarySampledSourcePort.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Table-reader and random-source costs are retained together through member estimation, tie-broken selection, and rounded action return.

  1. def OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceWithWork line 23
  2. theorem OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceWithWork_eq_cost line 31
  3. theorem OAI.EditApproximation.BinaryFraction.unskippedEstimateSourceWithWork_value line 52
  4. def OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceWithWork line 59
  5. theorem OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceWithWork_eq_cost line 63
  6. theorem OAI.EditApproximation.BinaryFraction.chooseUnskippedSourceWithWork_value line 79
  7. def OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceWithWork line 89
  8. theorem OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceWithWork_eq_cost line 97
  9. theorem OAI.EditApproximation.BinaryFraction.sampledGroupActionSourceWithWork_value line 133