OAI/Combinatorics/EditApproximation/Binary/BinaryGroupActionReads.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The selected group action uses the same minimizing member and rounded endpoints, while charging both the initial and current-table readers.

  1. def OAI.EditApproximation.BinaryFraction.sampledGroupActionReadWithWork line 26
  2. theorem OAI.EditApproximation.BinaryFraction.sampledGroupActionReadWithWork_eq_cost line 34
  3. def OAI.EditApproximation.BinaryFraction.dyadicSampledGroupActionReadWithWork line 63