OAI/Combinatorics/LowSpaceSubsetSum/Storage/PermutationSamplerCoupling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.FiniteLaw.uniform_bind_const line 18
2. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.pure_failure line 34
3. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.pure_uniform line 37
4. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.bind_idealLaw line 45
5. def OAI.LowSpaceSubsetSum.SamplerCoupling.prod line 53
6. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.prod_uniform line 56
7. theorem OAI.LowSpaceSubsetSum.SamplerCoupling.prod_failure_le line 65
8. def OAI.LowSpaceSubsetSum.finCoupling line 74

   Source documentation

   Range one is returned directly. Every other range uses exactly the fresh low-bit candidate sampler with at most n³ attempts.

   def finCoupling (n D : ℕ) [NeZero D] : SamplerCoupling (Fin D) :=
   …

   Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling

9. theorem OAI.LowSpaceSubsetSum.finCoupling_uniform line 78
10. theorem OAI.LowSpaceSubsetSum.finCoupling_failure line 87
11. def OAI.LowSpaceSubsetSum.permutationCoupling line 96

    Source documentation

    Insert one uniformly chosen location, then permute the remaining locations. The insertion bijection is Mathlib's explicit swap-based permutation code.

    def permutationCoupling (n : ℕ) : (k : ℕ) → SamplerCoupling (Equiv.Perm (Fin k))
      | 0 => SamplerCoupling.pure (Equiv.refl _)
      | k + 1 => ((finCoupling n (k + 1)).prod (permutationCoupling n k)).map
          Equiv.Perm.decomposeFin.symm

    Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.SamplerCoupling.pure, OAI.LowSpaceSubsetSum.finCoupling

12. theorem OAI.LowSpaceSubsetSum.permutationCoupling_uniform line 101
13. theorem OAI.LowSpaceSubsetSum.permutationCoupling_failure line 110
14. def OAI.LowSpaceSubsetSum.subsetCoupling line 123
15. theorem OAI.LowSpaceSubsetSum.subsetCoupling_uniform line 127
16. theorem OAI.LowSpaceSubsetSum.subsetCoupling_failure line 152