OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorSamplerCoupling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Bounded sampling of the four actual separator families

  1. instance OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.sampleNonempty line 18
  2. def OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.samplerCoupling line 23
  3. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.samplerCoupling_uniform line 30
  4. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.counts_le line 38
  5. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.RoundedParameters.samplerCoupling_failure line 44

    Source documentation

    Each subset uses at most g range calls. Repeated subset occurrences remain independent calls, exactly as in the stored sampled family.

    theorem samplerCoupling_failure (n : ℕ) :
    (S.samplerCoupling n).failure ≤ (44 * g * 2 ^ g : ℕ) / (2 : ℝ) ^ (n ^ 3) := by
…
  6. def OAI.LowSpaceSubsetSum.RepresentationSetup.separatorCoupling line 76
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.separatorCoupling_uniform line 80
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.separatorCoupling_failure line 84