OAI/Combinatorics/EditApproximation/Binary/BinarySampledGroups.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The sampled group continuation uses the executed envelopes, rounded states, exact finite sample counts, and ordered minimizing scan. Its output is the same physical action as the group program used by the accuracy proof.

  1. def OAI.EditApproximation.BinaryFraction.unskippedEstimateWithWork line 26
  2. theorem OAI.EditApproximation.BinaryFraction.unskippedEstimateWithWork_value line 35
  3. def OAI.EditApproximation.BinaryFraction.chooseBinaryUnskippedWithWork line 47
  4. theorem OAI.EditApproximation.BinaryFraction.chooseBinaryUnskippedWithWork_value line 52
  5. def OAI.EditApproximation.BinaryFraction.sampledGroupActionWithWork line 61
  6. theorem OAI.EditApproximation.BinaryFraction.sampledGroupActionWithWork_value line 70