OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionWorkBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The compression trial's stored arrays and exact exponent margins

Every bound below concerns actual list lengths. Repeated raw weights remain separate occurrences; only the seven block lists are compacted.

  1. def OAI.LowSpaceSubsetSum.compressionRawHalfSize line 18
  2. theorem OAI.LowSpaceSubsetSum.compressionRightRaw_card line 22
  3. theorem OAI.LowSpaceSubsetSum.compressionRawHalfSize_add line 28
  4. theorem OAI.LowSpaceSubsetSum.compression_cap_rate line 33
  5. theorem OAI.LowSpaceSubsetSum.compression_leftRaw_rate line 48
  6. theorem OAI.LowSpaceSubsetSum.compression_rawHalf_rate line 65
  7. theorem OAI.LowSpaceSubsetSum.compression_right_product_rate line 78
  8. theorem OAI.LowSpaceSubsetSum.compression_regeneration_exponents line 91
  9. theorem OAI.LowSpaceSubsetSum.pow_cast_le line 117
  10. theorem OAI.LowSpaceSubsetSum.CompressionData.compact_length_bound line 126
  11. theorem OAI.LowSpaceSubsetSum.CompressionData.leftRaw_card line 132
  12. theorem OAI.LowSpaceSubsetSum.CompressionData.rightRaw_card line 136
  13. theorem OAI.LowSpaceSubsetSum.CompressionData.storedFirst_length_bound line 140
  14. theorem OAI.LowSpaceSubsetSum.CompressionData.storedSecond_length_bounds line 144
  15. theorem OAI.LowSpaceSubsetSum.CompressionData.streamLength_bounds line 161
  16. theorem OAI.LowSpaceSubsetSum.CompressionData.stream_products line 185
  17. theorem OAI.LowSpaceSubsetSum.CompressionData.prime_regeneration_bound line 202
  18. theorem OAI.LowSpaceSubsetSum.CompressionData.matching_product_bound line 226
  19. theorem OAI.LowSpaceSubsetSum.CompressionData.stored_lists_small line 234
  20. theorem OAI.LowSpaceSubsetSum.CompressionData.stored_lists_capacity line 257
  21. def OAI.LowSpaceSubsetSum.CompressionData.groupFootprint line 271

    Source documentation

    A conservative count of array entries, cached tournament nodes and constant-size row cursors, at any current state or replay snapshot.

    def groupFootprint (e : Equiv.Perm (Fin n)) (q : CompressionSetup.PrimeSpace n)
    (i : Fin 4) (mode : FilteredStream.Mode) (s : D.GroupState e q i mode) : ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.FilteredStream.Mode

  22. theorem OAI.LowSpaceSubsetSum.CompressionData.groupFootprint_bound line 276