PermutationSampling.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Actual permutation sampling has uniform fixed-size block marginals

The seven compressed blocks and the mixer blocks need only marginal uniformity; they need not be independent. The proof counts fibers of the permutation action, using an explicit bijection between any two fibers.

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_mono line 21

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_map_of_constant_fibers line 31

Source documentation

A finite map with constant fiber cardinality preserves the uniform law.

theorem finiteUniformProbability_map_of_constant_fibers {Ω Ψ : Type*}
    [Fintype Ω] [Nonempty Ω] [Fintype Ψ] [Nonempty Ψ] [DecidableEq Ψ]
    (f : Ω → Ψ) {c : ℕ} (hf : ∀ y, Fintype.card {x // f x = y} = c)
    (P : Ψ → Prop) :
    finiteUniformProbability (fun x => P (f x)) = finiteUniformProbability P := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

def OAI.LowSpaceSubsetSum.permuteSubset line 57
theorem OAI.LowSpaceSubsetSum.permuteSubset_card line 60
theorem OAI.LowSpaceSubsetSum.permuteSubset_trans line 64
theorem OAI.LowSpaceSubsetSum.permuteSubset_refl line 70
theorem OAI.LowSpaceSubsetSum.exists_permutation_of_card_eq line 73
def OAI.LowSpaceSubsetSum.permutationBlock line 91
theorem OAI.LowSpaceSubsetSum.permutationBlock_fiber_card_eq line 95
theorem OAI.LowSpaceSubsetSum.permutationBlock_uniform line 124
Source documentation
The image of any fixed block under a uniform permutation is a uniform subset of the same cardinality, including empty and full blocks.
```
theorem permutationBlock_uniform (K : Finset ι) (P : Finset ι → Prop) :
    finiteUniformProbability (fun e : Equiv.Perm ι => P (permuteSubset e K)) =
      finiteUniformProbability (fun S : ↥((Finset.univ : Finset ι).powersetCard K.card) => P S.val) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.permuteSubset
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_finset line 140
theorem OAI.LowSpaceSubsetSum.permutationBlock_uniform_ratio line 160