OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionPreparationLedger.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Paying for every compression reader initialization

The arrays have nonempty factors, so their lengths are bounded by the corresponding stream lengths. The stream-regeneration exponent margins therefore also bound initialization at every residue.

  1. theorem OAI.LowSpaceSubsetSum.CompressionData.stored_lengths_positive line 18
  2. theorem OAI.LowSpaceSubsetSum.CompressionData.preparation_size_le line 43
  3. theorem OAI.LowSpaceSubsetSum.CompressionData.half_power_ceiling line 56
  4. theorem OAI.LowSpaceSubsetSum.CompressionData.preparation_regeneration_bound line 64
  5. theorem OAI.LowSpaceSubsetSum.CompressionData.preparedSchedule_allowance line 81