Flat sources

A flat source is the uniform distribution on a finite set. A distribution on a finite type whose outcomes all have probability at most 1 / K is a mixture of flat distributions on sets of exactly K outcomes (exists_eq_bind_uniformOfFinset). In particular, for a natural number k, every k-source is a mixture of flat k-sources, the uniform distributions on sets of 2^k outcomes Chor, Goldreich, Vadhan, Chapter 6. Since mixtures of k-sources are k-sources (le_minEntropy_bind), this characterizes the k-sources (le_minEntropy_iff_exists_eq_bind_uniformOfFinset).

The proof is combinatorial. Scaled by K, the masses form a point of [0, 1]^α with coordinate sum K. Moving weight between two coordinates strictly between 0 and 1 writes such a point as a convex combination of two points with fewer such coordinates. When no such coordinate remains, the point is the indicator of a set of K outcomes.

Main results

• Cslib.Probability.PMF.exists_eq_bind_uniformOfFinset: a distribution with masses at most 1 / K is a mixture of flat distributions on K outcomes.
• Cslib.Probability.PMF.le_minEntropy_iff_exists_eq_bind_uniformOfFinset: the k-sources are exactly the mixtures of flat k-sources.

References

• B. Chor, O. Goldreich, Unbiased Bits from Sources of Weak Randomness and Probabilistic Communication Complexity
• S. Vadhan, Pseudorandomness, Chapter 6

Points of the hypersimplex

Flat decompositions

theorem Cslib.Probability.PMF.exists_eq_bind_uniformOfFinset {α : Type u_1} [Finite α] (p : PMF α) {K : ℕ} (hK : K ≠ 0) (hp : ∀ (a : α), (p a).toReal ≤ (↑K)⁻¹) : ∃ (mix : PMF { S : Finset α // S.card = K }), p = mix.bind fun (S : { S : Finset α // S.card = K }) => uniformOfFinset ↑S ⋯

Flat decomposition. A distribution on a finite type whose outcomes all have probability at most 1 / K is a mixture of uniform distributions on sets of exactly K outcomes.

theorem Cslib.Probability.PMF.exists_eq_bind_uniformOfFinset_of_le_minEntropy {α : Type u_1} [Finite α] (p : PMF α) {k : ℕ} (hk : ↑k ≤ minEntropy p) : ∃ (mix : PMF { S : Finset α // S.card = 2 ^ k }), p = mix.bind fun (S : { S : Finset α // S.card = 2 ^ k }) => uniformOfFinset ↑S ⋯

Every k-source is a mixture of flat k-sources. A distribution with min-entropy at least a natural number k is a mixture of uniform distributions on sets of 2^k outcomes.

theorem Cslib.Probability.PMF.le_minEntropy_iff_exists_eq_bind_uniformOfFinset {α : Type u_1} [Finite α] (p : PMF α) (k : ℕ) : ↑k ≤ minEntropy p ↔ ∃ (mix : PMF { S : Finset α // S.card = 2 ^ k }), p = mix.bind fun (S : { S : Finset α // S.card = 2 ^ k }) => uniformOfFinset ↑S ⋯

k-sources are mixtures of flat k-sources. For a natural number k, a distribution has min-entropy at least k exactly when it is a mixture of uniform distributions on sets of 2^k outcomes.