OAI/Combinatorics/LowSpaceSubsetSum/Word/WordActionBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Prepared-action costs on every finite word stream

These counters account for the prepared action after seed generation. Seed construction work and its live buffer are separate from these bounds.

  1. theorem OAI.LowSpaceSubsetSum.WordActionBounds.pow_product_positive line 16
  2. theorem OAI.LowSpaceSubsetSum.WordActionBounds.pow_product_mono line 19
  3. theorem OAI.LowSpaceSubsetSum.WordActionBounds.combine_work line 23
  4. theorem OAI.LowSpaceSubsetSum.WordActionBounds.round_work_generic line 29
  5. theorem OAI.LowSpaceSubsetSum.WordActionBounds.combine_cells line 37
  6. theorem OAI.LowSpaceSubsetSum.WordActionBounds.scale_large line 43
  7. theorem OAI.LowSpaceSubsetSum.WordActionBounds.law_nonempty line 49
  8. theorem OAI.LowSpaceSubsetSum.WordActionBounds.compression_source_work line 56
  9. theorem OAI.LowSpaceSubsetSum.WordActionBounds.representation_source_work line 68
  10. theorem OAI.LowSpaceSubsetSum.WordActionBounds.compression_work line 81
  11. theorem OAI.LowSpaceSubsetSum.WordActionBounds.representation_work line 92
  12. theorem OAI.LowSpaceSubsetSum.WordActionBounds.combine_majorize line 104
  13. theorem OAI.LowSpaceSubsetSum.WordActionBounds.round_work line 113
  14. theorem OAI.LowSpaceSubsetSum.WordActionBounds.compression_cells line 125
  15. theorem OAI.LowSpaceSubsetSum.WordActionBounds.representation_cells line 140
  16. theorem OAI.LowSpaceSubsetSum.WordActionBounds.round_cells line 154
  17. theorem OAI.LowSpaceSubsetSum.WordActionBounds.repeat_majorize line 172
  18. theorem OAI.LowSpaceSubsetSum.WordActionBounds.repeated_work line 183
  19. theorem OAI.LowSpaceSubsetSum.WordActionBounds.repeated_cells line 196