FiniteProductSamplerCoupling.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite arrays of bounded calls and permutation-generated partitions

def OAI.LowSpaceSubsetSum.SamplerCoupling.pi line 19
Source documentation
Independent fresh seeds for a finite array of calls. Each coordinate may have a different output type and a different number of internal attempts.
```
def pi : (k : ℕ) → (A : Fin k → Type) → [∀ i, Fintype (A i)] →
    (∀ i, SamplerCoupling (A i)) → SamplerCoupling (∀ i, A i)
  | 0, _, _, _ => SamplerCoupling.pure (fun i => Fin.elim0 i)
  | k + 1, A, _, S =>
      ((S 0).prod (pi k (fun i => A i.succ) (fun i => S i.succ))).map (Fin.consEquiv A)
```
Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.SamplerCoupling.pure, OAI.LowSpaceSubsetSum.SamplerCoupling.prod, OAI.LowSpaceSubsetSum.SamplerCoupling.map
theorem OAI.LowSpaceSubsetSum.SamplerCoupling.pi_uniform line 25
theorem OAI.LowSpaceSubsetSum.SamplerCoupling.pi_failure_le line 40
def OAI.LowSpaceSubsetSum.finiteChoiceCoupling line 57
Source documentation
A bounded choice from an explicitly enumerated finite set. This is used only for the polynomial-size interval guesses and residue ranges.
```
def finiteChoiceCoupling (n : ℕ) (A : Type) [Fintype A] [Nonempty A] :
    SamplerCoupling A :=
…
```
Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling
theorem OAI.LowSpaceSubsetSum.finiteChoiceCoupling_uniform line 61
theorem OAI.LowSpaceSubsetSum.finiteChoiceCoupling_failure line 66
def OAI.LowSpaceSubsetSum.finitePermutationCoupling line 71
theorem OAI.LowSpaceSubsetSum.finitePermutationCoupling_uniform line 76
theorem OAI.LowSpaceSubsetSum.finitePermutationCoupling_failure line 82
def OAI.LowSpaceSubsetSum.coloringOfPermutation line 90
Source documentation
Fix one block labeling; a uniformly permuted labeling has the exact uniform law on all labelings with these block sizes.
```
def coloringOfPermutation {A K : Type} [Fintype A] [Fintype K] [DecidableEq K]
    {t : K → ℕ} (f : MatchingSmoothing.Colorings A K t) (e : Equiv.Perm A) :
    MatchingSmoothing.Colorings A K t :=
…
```
Mentions: OAI.MatchingSmoothing.Colorings
theorem OAI.LowSpaceSubsetSum.coloringOfPermutation_uniform line 95
def OAI.LowSpaceSubsetSum.coloringCoupling line 119
theorem OAI.LowSpaceSubsetSum.coloringCoupling_uniform line 124
theorem OAI.LowSpaceSubsetSum.coloringCoupling_failure line 131