OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorSamplerBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The concrete family-sampler storage under the capacity guard

  1. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.reserve_le line 12
  2. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.four_cells line 32
  3. def OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.application line 54
  4. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.application_value line 58
  5. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.application_cells line 63
  6. theorem OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.representation_cells line 71

    Source documentation

    The concrete top blocks obey a stronger table-capacity guard, hence all four sampled families and their unread seed tails fit the same cap.

    theorem representation_cells {n : ℕ} (R : RepresentationSetup n)
    (h : R.PrimeHistory) (hn : 10000 ≤ n)
    (s : ((RepresentationSetup.separatorParameters h.1.1.2 (by omega)).samplerCoupling n).Seed) :
    (application (RepresentationSetup.separatorParameters h.1.1.2 (by omega)) n s).2 ≤
      inputScale R.input^6*(compressionDictionaryCapacity n+1) := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup, OAI.LowSpaceSubsetSum.RepresentationSetup.separatorParameters, OAI.LowSpaceSubsetSum.SeparatorSamplerBounds.application, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity