OAI/Combinatorics/EditApproximation/Binary/BinaryLocalOnlineSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Online candidate selection charges the finite source-buffer decoder at the point where its integer is consumed. Ineligible centers do not read a random coordinate.

  1. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWork line 21
  2. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWork_value line 36
  3. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWork_eq_cost_on line 45
  4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleSourceWithWork_eq_cost line 67
  5. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWork line 80
  6. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWork_value line 90
  7. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWork_eq_cost_on line 98
  8. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWork_eq_cost line 128