OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedLocalOnline.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One rounded center is queried at each retained dyadic scale. Both eligibility and the complete online optimizer are charged.

  1. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleWithWork line 12
  2. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleWithWork_value line 30
  3. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsWithWork line 62
  4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsWithWork_value line 76