OAI/Combinatorics/EditApproximation/Binary/BinaryGroupSetupWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit bit costs of the dyadic-scale and exact sample-count builders. The generated count determines the finite draw type.

  1. theorem OAI.EditApproximation.BinaryFraction.signedPowerTwoWithWork_cost line 11
  2. def OAI.EditApproximation.BinaryFraction.groupScalesBitBudget line 17
  3. theorem OAI.EditApproximation.BinaryFraction.groupScalesWithWork_bounds line 21
  4. def OAI.EditApproximation.BinaryFraction.groupSampleCountWordBudget line 52
  5. def OAI.EditApproximation.BinaryFraction.groupSampleCountBitBudget line 54
  6. theorem OAI.EditApproximation.BinaryFraction.groupSampleCountWithWork_bounds line 59