OAI/Combinatorics/LowSpaceSubsetSum/Counting/PrimeSamplerCoupling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Bounded fresh-prime calls for the nested three-factor sampler

  1. instance OAI.LowSpaceSubsetSum.factorNonempty line 14
  2. def OAI.LowSpaceSubsetSum.factorOneEquiv line 17
  3. def OAI.LowSpaceSubsetSum.factorPrimeEquiv line 26
  4. def OAI.LowSpaceSubsetSum.factorCoupling line 32
  5. theorem OAI.LowSpaceSubsetSum.factorCoupling_uniform line 36
  6. theorem OAI.LowSpaceSubsetSum.factorCoupling_failure line 47
  7. def OAI.LowSpaceSubsetSum.tripleFactorEquiv line 56
  8. def OAI.LowSpaceSubsetSum.triplePrimeCoupling line 68
  9. theorem OAI.LowSpaceSubsetSum.triplePrimeCoupling_uniform line 72
  10. theorem OAI.LowSpaceSubsetSum.triplePrimeCoupling_failure line 82