OAI/Combinatorics/EditApproximation/Binary/BinaryGroupSpace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Literal exact/sample reductions and the sample-count constructor. The child-index list cells and every comparison are included.

  1. theorem OAI.EditApproximation.BinaryFraction.equalAllocation_le_work line 16
  2. theorem OAI.EditApproximation.BinaryFraction.groupTermsAllocation_le_work line 26
  3. theorem OAI.EditApproximation.BinaryFraction.groupIndexAllocation_le_work line 37
  4. def OAI.EditApproximation.BinaryFraction.groupScaleAllocation line 46
  5. theorem OAI.EditApproximation.BinaryFraction.groupScaleAllocation_le_work line 55
  6. theorem OAI.EditApproximation.BinaryFraction.groupSampleCountAllocation_le_work line 75
  7. def OAI.EditApproximation.BinaryFraction.equalInvocations line 88
  8. theorem OAI.EditApproximation.BinaryFraction.equalInvocations_le_work line 91
  9. def OAI.EditApproximation.BinaryFraction.groupTermsInvocations line 99
  10. theorem OAI.EditApproximation.BinaryFraction.groupTermsInvocations_le_work_add_one line 103
  11. def OAI.EditApproximation.BinaryFraction.groupIndexInvocations line 112
  12. theorem OAI.EditApproximation.BinaryFraction.groupIndexInvocations_le_work_add_one line 117
  13. def OAI.EditApproximation.BinaryFraction.groupScaleInvocations line 126
  14. theorem OAI.EditApproximation.BinaryFraction.groupScaleInvocations_le_work line 135
  15. def OAI.EditApproximation.BinaryFraction.groupSampleCountInvocations line 153
  16. theorem OAI.EditApproximation.BinaryFraction.groupSampleCountInvocations_le_work line 162