OAI/Combinatorics/LowSpaceSubsetSum/Counting/RejectionSamplerCoupling.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.FiniteLaw.eq_of_mass line 17
2. theorem OAI.LowSpaceSubsetSum.FiniteLaw.map_equiv_uniform line 24
3. def OAI.LowSpaceSubsetSum.SamplerCoupling.map line 42
4. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.map_failure line 53
5. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.map_idealLaw line 58
6. def OAI.LowSpaceSubsetSum.firstAcceptSubtype line 70
7. theorem OAI.LowSpaceSubsetSum.firstAcceptSubtype_none line 76
8. def OAI.LowSpaceSubsetSum.firstAcceptCoupling line 83

   Source documentation

   The bounded marginal ignores the independent eligible backup. The ideal completion uses it precisely on exhaustion of the fresh candidate tuple.

   def firstAcceptCoupling [Fintype Ω] [Nonempty Ω]
       (A : Ω → Prop) [DecidablePred A] [Nonempty {a : Ω // A a}] (N : ℕ) :
       SamplerCoupling {a : Ω // A a} where
   …

   Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling

9. theorem OAI.LowSpaceSubsetSum.firstAcceptCoupling_uniform line 101
10. theorem OAI.LowSpaceSubsetSum.firstAcceptCoupling_failure line 112
11. def OAI.LowSpaceSubsetSum.rangeEligibleEquiv line 122
12. def OAI.LowSpaceSubsetSum.rangeCoupling line 128
13. theorem OAI.LowSpaceSubsetSum.rangeCoupling_uniform line 134
14. theorem OAI.LowSpaceSubsetSum.rangeCoupling_failure line 143
15. def OAI.LowSpaceSubsetSum.primeEligibleEquiv line 151
16. def OAI.LowSpaceSubsetSum.primeCoupling line 158
17. theorem OAI.LowSpaceSubsetSum.primeCoupling_uniform line 165
18. theorem OAI.LowSpaceSubsetSum.primeCoupling_failure line 175