OAI/Combinatorics/EditApproximation/Binary/BinaryGatheredValues.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite stored-word tables for gathered earlier values. The lookup scan and the construction of every gathered warmup mean are explicit.

  1. theorem OAI.EditApproximation.BinaryFraction.gatheredWordLookupWithWork_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.gatheredWordLookupWithWork_cost line 34
  3. theorem OAI.EditApproximation.BinaryFraction.gatheredWordLookupWithWork_width line 49
  4. def OAI.EditApproximation.BinaryFraction.gatheredMassWordsWithWork line 64
  5. theorem OAI.EditApproximation.BinaryFraction.gatheredMassWordsWithWork_value line 69
  6. theorem OAI.EditApproximation.BinaryFraction.gatheredMassWordsWithWork_bounds line 76
  7. theorem OAI.EditApproximation.BinaryFraction.gatheredMassLookup_value line 98
  8. def OAI.EditApproximation.BinaryFraction.gatheredWordBits line 116
  9. theorem OAI.EditApproximation.BinaryFraction.gatheredWordBits_le line 119
  10. theorem OAI.EditApproximation.BinaryFraction.gatheredMassWordsWithWork_storage line 131