Documentation

Complexity.Probability.Uniform

Uniform sampling and subset sums #

A surjective additive homomorphism between finite groups preserves the uniform distribution. Consequently, the sum over any nonempty subset of independently uniform group elements is uniform, and two distinct nonempty subsets give independent uniform sums. Replacing any one summand by a fresh uniform value also makes the complete sum uniform.

For bitstrings, addition is pointwise XOR. These subset sums are the pairwise independent masks used by the Goldreich–Levin decoder. The joint-distribution theorem does not assert mutual independence of three or more subset sums. The fiber-counting criterion is shared with PairwiseIndependentHash.Shift; the subset-sum results are adapted from the cslib crypto branch at 5ff69ca.

Main results #

References #

source
theorem Cslib.Probability.card_mul_card_filter_eq_of_shift {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddGroup G] [Fintype G] [DecidableEq G] {f : ι → G} (hf : ∀ (c : G), ∃ (e : Equiv.Perm ι), ∀ (i : ι), f (e i) = f i + c) (y : G) :
Fintype.card G * {i : ι | f i = y}.card = Fintype.card ι

If every translate f + c of a function f : ι → G into a finite group is f ∘ e for a permutation e of ι, then all fibers of f have the same size |ι| / |G|.

source
theorem Cslib.Probability.dens_filter_eq_of_shift {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty ι] {f : ι → G} (hf : ∀ (c : G), ∃ (e : Equiv.Perm ι), ∀ (i : ι), f (e i) = f i + c) (y : G) :
{i : ι | f i = y}.dens = (↑(Fintype.card G))⁻¹

Uniformity from shifts: if every translate f + c of a function f : ι → G into a finite group is f ∘ e for a permutation e of ι, then f is uniformly distributed: for a uniformly random i, f i takes each value with probability 1 / |G|.

source
theorem Cslib.Probability.PMF.uniformOfFintype_map_of_shift {ι : Type u_1} {G : Type u_2} [Fintype ι] [Nonempty ι] [AddGroup G] [Fintype G] {f : ι → G} (hf : ∀ (c : G), ∃ (e : Equiv.Perm ι), ∀ (i : ι), f (e i) = f i + c) :
PMF.map f (uniformOfFintype ι) = uniformOfFintype G

A function whose output translations are realized by permutations of its input sends uniform inputs to uniform outputs.

source
theorem Cslib.Probability.PMF.uniformOfFintype_map_sum_update {ι : Type u_1} {G : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype G] [AddCommGroup G] (values : ι → G) (i : ι) :
PMF.map (fun (value : G) => ∑ j : ι, Function.update values i value j) (uniformOfFintype G) = uniformOfFintype G

A finite sum is uniform if any one summand is fresh uniform, regardless of the others.

source
theorem Cslib.Probability.PMF.uniformOfFintype_map_addHom {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [Fintype G] [Fintype H] (f : G →+ H) (hf : Function.Surjective ⇑f) :
PMF.map (⇑f) (uniformOfFintype G) = uniformOfFintype H

A surjective additive homomorphism of finite groups sends uniform inputs to uniform outputs.

source
theorem Cslib.Probability.PMF.uniformOfFintype_map_sum {ι : Type u_1} {G : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype G] [AddCommGroup G] (s : Finset ι) (hs : s.Nonempty) :
PMF.map (fun (masks : ι → G) => ∑ i ∈ s, masks i) (uniformOfFintype (ι → G)) = uniformOfFintype G

A nonempty subset sum of independent uniform group elements is uniform.

source
theorem Cslib.Probability.PMF.uniformOfFintype_map_sum_pair {ι : Type u_1} {G : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype G] [AddCommGroup G] (s t : Finset ι) (hs : s.Nonempty) (ht : t.Nonempty) (hst : s ≠ t) :
PMF.map (fun (masks : ι → G) => (∑ i ∈ s, masks i, ∑ i ∈ t, masks i)) (uniformOfFintype (ι → G)) = uniformOfFintype (G × G)

Distinct nonempty subset sums have the joint distribution of two independent uniform samples.