OAI/Combinatorics/EditApproximation/Binary/BinaryCountedGroupWork.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The count used by every sampled scale is at most the actual child arity. Consequently the complete group counter is bounded from stored input widths, without assuming estimates on its internal callbacks.

  1. theorem OAI.EditApproximation.BinaryFraction.sumStorage_mono line 12
  2. theorem OAI.EditApproximation.BinaryFraction.storedSumWork_mono line 18
  3. def OAI.EditApproximation.BinaryFraction.boundedScaleWordBudget line 24
  4. def OAI.EditApproximation.BinaryFraction.boundedScaleBitBudget line 27
  5. theorem OAI.EditApproximation.BinaryFraction.groupScale_budget_le line 31
  6. def OAI.EditApproximation.BinaryFraction.countedGroupBitBudget line 49
  7. theorem OAI.EditApproximation.BinaryFraction.countedGroupMemberWithWork_bounds line 53