Small-bias distributions and the XOR lemma

The bias of a distribution X on the cube ι → Bool at a set S of coordinates is the expectation of the character χ_S under X (Cslib.BitString.bias), which is Pr[⊕_{i ∈ S} xᵢ = 0] - Pr[⊕_{i ∈ S} xᵢ = 1] (Cslib.BitString.bias_eq_one_sub_two_mul). The uniform distribution has bias zero at every nonempty set. A distribution is ε-biased (Cslib.BitString.IsSmallBias) if its bias at every nonempty set is at most ε in absolute value Naor and Naor, and k-wise ε-biased (Cslib.BitString.IsKWiseSmallBias) if this holds for the nonempty sets of at most k coordinates Alon, Goldreich, Håstad and Peralta.

The bias at S is 2 ^ n times the Fourier coefficient of the mass function of X at S, so Parseval's identity gives ∑_S bias X S ^ 2 = 2 ^ n cp(X) for the collision probability cp (Cslib.BitString.sum_bias_sq). Combined with the collision bound on the distance to uniform, this is Vazirani's XOR lemma Vazirani (Cslib.BitString.four_mul_dist_uniform_sq_le_sum_bias_sq): the statistical distance of X from uniform is at most half the root of the sum of the squared biases at the nonempty sets. An ε-biased distribution on n bits is therefore within √(2 ^ n - 1) ε / 2 of uniform (Cslib.BitString.IsSmallBias.dist_uniform_le). The marginal of X on a set T of coordinates has the biases of X at the subsets of T (Cslib.BitString.bias_map_restrict), so a k-wise ε-biased distribution is almost k-wise independent: its marginal on any k coordinates is within √(2 ^ k - 1) ε / 2 of uniform (Cslib.BitString.IsKWiseSmallBias.dist_map_restrict_le).

Reading a distribution through n parities y_j = c_j ⬝ᵥ x of its bits turns the bias at a set T of outputs into the bias at the support of ∑_{j ∈ T} c_j (Cslib.BitString.bias_map_dotProduct). If the vectors c_j are k-wise linearly independent, an ε-biased distribution is read as a k-wise ε-biased one (Cslib.BitString.IsSmallBias.isKWiseSmallBias_map_dotProduct), the linear composition of Naor and Naor.

Main definitions

• Cslib.BitString.bias: the bias of a distribution on the cube at a set of coordinates.
• Cslib.BitString.IsSmallBias: ε-biased distributions.
• Cslib.BitString.IsKWiseSmallBias: k-wise ε-biased distributions.

Main results

• Cslib.BitString.bias_eq_one_sub_two_mul: the bias in terms of the probability of odd parity.
• Cslib.BitString.bias_uniformOfFintype: the uniform distribution is unbiased.
• Cslib.BitString.sum_bias_sq: Parseval's identity for the biases.
• Cslib.BitString.four_mul_dist_uniform_sq_le_sum_bias_sq, Cslib.BitString.dist_uniform_le_sqrt_sum_bias_sq: Vazirani's XOR lemma.
• Cslib.BitString.IsSmallBias.dist_uniform_le: ε-biased distributions are close to uniform.
• Cslib.BitString.IsKWiseSmallBias.dist_map_restrict_le: k-wise ε-biased distributions are almost k-wise independent.
• Cslib.BitString.IsSmallBias.isKWiseSmallBias_map_dotProduct: k-wise independent parities of an ε-biased distribution are k-wise ε-biased.

References

• J. Naor, M. Naor, Small-bias probability spaces: efficient constructions and applications
• N. Alon, O. Goldreich, J. Håstad, R. Peralta, Simple constructions of almost k-wise independent random variables
• U. V. Vazirani, Randomness, adversaries and computation

def Cslib.BitString.bias {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) (S : Finset ι) : ℝ

The bias of a distribution X on the cube at a set S of coordinates: the expectation of the character χ_S under X, which is Pr[⊕_{i ∈ S} xᵢ = 0] - Pr[⊕_{i ∈ S} xᵢ = 1] (bias_eq_one_sub_two_mul).

@[simp]

theorem Cslib.BitString.bias_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) : bias X ∅ = 1

Every distribution has bias one at the empty set.

theorem Cslib.BitString.bias_eq_one_sub_two_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) (S : Finset ι) : bias X S = 1 - 2 * (X.toOuterMeasure {x : ι → Bool | parityOn S x = true}).toReal

The bias is the probability of even parity minus the probability of odd parity on S.

theorem Cslib.BitString.abs_bias_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) (S : Finset ι) : |bias X S| ≤ 1

A bias lies in [-1, 1].

@[simp]

theorem Cslib.BitString.bias_pure {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : ι → Bool) (S : Finset ι) : bias (PMF.pure x) S = chi ℝ S x

A point mass has the bias of its point: the value of the character there.

theorem Cslib.BitString.bias_map {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] (X : PMF α) (g : α → ι → Bool) (S : Finset ι) : bias (PMF.map g X) S = ∑ a : α, (X a).toReal * chi ℝ S (g a)

The bias of the image of a distribution is the expectation of the character of the image.

theorem Cslib.BitString.bias_uniformOfFintype_map {ι : Type u_1} [Fintype ι] [DecidableEq ι] {σ : Type u_2} [Fintype σ] [Nonempty σ] (g : σ → ι → Bool) (S : Finset ι) : bias (PMF.map g (Probability.PMF.uniformOfFintype σ)) S = Finset.univ.expect fun (s : σ) => chi ℝ S (g s)

The bias of a sample space g, with a uniformly random seed, is the average of the character over the seeds.

theorem Cslib.BitString.bias_uniformOfFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) : bias (Probability.PMF.uniformOfFintype (ι → Bool)) S = if S = ∅ then 1 else 0

The uniform distribution has bias zero at every nonempty set.

theorem Cslib.BitString.sum_bias_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) : ∑ S : Finset ι, bias X S ^ 2 = 2 ^ Fintype.card ι * Probability.PMF.collisionProbability X

Parseval's identity for the biases: the squared biases of X sum to 2 ^ n times its collision probability.

theorem Cslib.BitString.four_mul_dist_uniform_sq_le_sum_bias_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) : 4 * dist X (Probability.PMF.uniformOfFintype (ι → Bool)) ^ 2 ≤ ∑ S : Finset ι with S.Nonempty, bias X S ^ 2

Vazirani's XOR lemma, squared form: four times the squared statistical distance of X from uniform is at most the sum of the squared biases of X at the nonempty sets.

theorem Cslib.BitString.dist_uniform_le_sqrt_sum_bias_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) : dist X (Probability.PMF.uniformOfFintype (ι → Bool)) ≤ √(∑ S : Finset ι with S.Nonempty, bias X S ^ 2) / 2

Vazirani's XOR lemma: the statistical distance of X from uniform is at most half the square root of the sum of the squared biases of X at the nonempty sets.

def Cslib.BitString.IsSmallBias {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ε : ℝ) (X : PMF (ι → Bool)) : Prop

A distribution X on the cube is ε-biased if its bias at every nonempty set of coordinates is at most ε in absolute value Naor and Naor.

def Cslib.BitString.IsKWiseSmallBias {ι : Type u_1} [Fintype ι] [DecidableEq ι] (k : ℕ) (ε : ℝ) (X : PMF (ι → Bool)) : Prop

A distribution X on the cube is k-wise ε-biased if its bias at every nonempty set of at most k coordinates is at most ε in absolute value Alon, Goldreich, Håstad and Peralta.

theorem Cslib.BitString.isSmallBias_uniformOfFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] : IsSmallBias 0 (Probability.PMF.uniformOfFintype (ι → Bool))

The uniform distribution is 0-biased.

theorem Cslib.BitString.isSmallBias_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) : IsSmallBias 1 X

Every distribution is 1-biased.

theorem Cslib.BitString.IsSmallBias.mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ε δ : ℝ} {X : PMF (ι → Bool)} (hX : IsSmallBias ε X) (h : ε ≤ δ) : IsSmallBias δ X

An ε-biased distribution is δ-biased for every δ ≥ ε.

theorem Cslib.BitString.IsSmallBias.isKWiseSmallBias {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ε : ℝ} {X : PMF (ι → Bool)} (hX : IsSmallBias ε X) (k : ℕ) : IsKWiseSmallBias k ε X

An ε-biased distribution is k-wise ε-biased for every k.

theorem Cslib.BitString.IsSmallBias.dist_uniform_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ε : ℝ} {X : PMF (ι → Bool)} (hX : IsSmallBias ε X) : dist X (Probability.PMF.uniformOfFintype (ι → Bool)) ≤ √(2 ^ Fintype.card ι - 1) * ε / 2

Small bias implies closeness to uniform: an ε-biased distribution on n bits is within statistical distance √(2 ^ n - 1) ε / 2 of uniform.

theorem Cslib.BitString.isKWiseSmallBias_card_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ε : ℝ} {X : PMF (ι → Bool)} : IsKWiseSmallBias (Fintype.card ι) ε X ↔ IsSmallBias ε X

A distribution is n-wise ε-biased on n bits exactly when it is ε-biased.

theorem Cslib.BitString.chi_restrict {ι : Type u_1} (T : Finset ι) (S : Finset ↥T) (x : ι → Bool) : chi ℝ S (T.restrict x) = chi ℝ (Finset.map (Function.Embedding.subtype fun (x : ι) => x ∈ T) S) x

The character of a set S of coordinates in T at the restriction of x to T is the character of S, as a set of coordinates of x.

theorem Cslib.BitString.bias_map_restrict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) (T : Finset ι) (S : Finset ↥T) : bias (PMF.map T.restrict X) S = bias X (Finset.map (Function.Embedding.subtype fun (x : ι) => x ∈ T) S)

The marginal of X on a set T of coordinates has the biases of X at the subsets of T.

theorem Cslib.BitString.IsKWiseSmallBias.mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {ε : ℝ} {X : PMF (ι → Bool)} (hX : IsKWiseSmallBias k ε X) {k' : ℕ} (hk : k' ≤ k) : IsKWiseSmallBias k' ε X

A k-wise ε-biased distribution is k'-wise ε-biased for every k' ≤ k.

theorem Cslib.BitString.IsKWiseSmallBias.isSmallBias_map_restrict {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {ε : ℝ} {X : PMF (ι → Bool)} (hX : IsKWiseSmallBias k ε X) {T : Finset ι} (hT : T.card ≤ k) : IsSmallBias ε (PMF.map T.restrict X)

The marginal of a k-wise ε-biased distribution on a set of at most k coordinates is ε-biased.

theorem Cslib.BitString.IsKWiseSmallBias.dist_map_restrict_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {ε : ℝ} {X : PMF (ι → Bool)} (hX : IsKWiseSmallBias k ε X) {T : Finset ι} (hT : T.card ≤ k) : dist (PMF.map T.restrict X) (Probability.PMF.uniformOfFintype (↥T → Bool)) ≤ √(2 ^ T.card - 1) * ε / 2

Almost k-wise independence: the marginal of a k-wise ε-biased distribution on a set T of at most k coordinates is within statistical distance √(2 ^ #T - 1) ε / 2 of uniform Alon, Goldreich, Håstad and Peralta.

theorem Cslib.BitString.signVal_dotProduct {ι : Type u_1} [Fintype ι] (u x : ι → Bool) : signVal (u ⬝ᵥ x) = chi ℝ {i : ι | u i = true} x

The real sign of the inner product of bit strings u ⬝ᵥ x is the character, at x, of the set of coordinates where u is true.

theorem Cslib.BitString.bias_map_dotProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (X : PMF (ι → Bool)) (c : κ → ι → Bool) (T : Finset κ) : bias (PMF.map (fun (x : ι → Bool) (j : κ) => c j ⬝ᵥ x) X) T = bias X {i : ι | (∑ j ∈ T, c j) i = true}

Reading X through the parities y_j = c j ⬝ᵥ x turns the bias at a set T of outputs into the bias of X at the coordinates where ∑_{j ∈ T} c j is true.

theorem Cslib.BitString.IsSmallBias.isKWiseSmallBias_map_dotProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {ε : ℝ} {X : PMF (ι → Bool)} (hX : IsSmallBias ε X) {k : ℕ} {c : κ → ι → Bool} (hc : ∀ (T : Finset κ), T.Nonempty → T.card ≤ k → ∑ j ∈ T, c j ≠ 0) : IsKWiseSmallBias k ε (PMF.map (fun (x : ι → Bool) (j : κ) => c j ⬝ᵥ x) X)

Linear composition Naor and Naor: if every nonempty set of at most k of the vectors c j has a nonzero sum, then the parities c j ⬝ᵥ x of an ε-biased distribution are k-wise ε-biased.