Fooling functions on the cube, and k-wise independence

A distribution X on the cube ι → Bool ε-fools a real function F on the cube (Cslib.BitString.Fools) if the expectation of F under X is within ε of its expectation under the uniform distribution. A distribution is k-wise independent (Cslib.BitString.IsKWiseIndependent) if every k of its coordinates are uniformly distributed; in terms of biases, its bias at every nonempty set of at most k coordinates vanishes, and this is how the abbreviation is defined, as IsKWiseSmallBias k 0. A uniformly seeded k-wise independent family of bit strings, such as one built from Cslib.Probability.polynomialHash, induces a k-wise independent distribution (Cslib.Probability.IsKWiseIndependentHash.isKWiseIndependent_map).

The expectation of F under X is the sum of the Fourier coefficients of F weighted by the biases of X (Cslib.BitString.sum_mul_eq_sum_fourierCoeff_mul_bias). A function of degree at most k has no Fourier weight above level k, so a k-wise independent distribution fools it exactly Braverman, Proposition 6 (Cslib.BitString.IsKWiseIndependent.fools_of_mem_lowDegree).

A Boolean function is fooled once both it and its negation have one-sided lower bounds (Cslib.BitString.fools_bitVal_of_le), which is how Braverman obtains the two-sided bound of his Main Theorem from the one-sided Lemma 12.

Main definitions

• Cslib.BitString.Fools: X ε-fools F.
• Cslib.BitString.IsKWiseIndependent: k-wise independent distributions on the cube.

Main results

• Cslib.BitString.sum_mul_eq_sum_fourierCoeff_mul_bias: expectations through Fourier coefficients and biases.
• Cslib.BitString.IsKWiseIndependent.fools_of_mem_lowDegree: k-wise independence fools degree-k functions exactly.
• Cslib.Probability.IsKWiseIndependentHash.isKWiseIndependent_map: seeded k-wise independent families induce k-wise independent distributions.
• Cslib.BitString.isKWiseIndependent_uniformOfFintype: the uniform distribution is k-wise independent for every k.
• Cslib.BitString.fools_bitVal_of_le: two one-sided bounds fool a Boolean function.

References

• M. Braverman, Polylogarithmic independence fools AC⁰ circuits

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

A distribution X on the cube ε-fools a real function F if the expectation of F under X is within ε of its expectation under the uniform distribution.

theorem Cslib.BitString.sum_uniformOfFintype_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) : ∑ x : ι → Bool, ((Probability.PMF.uniformOfFintype (ι → Bool)) x).toReal * F x = Finset.univ.expect fun (x : ι → Bool) => F x

The expectation under the uniform distribution is the average.

theorem Cslib.BitString.fools_uniformOfFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : (ι → Bool) → ℝ) : Fools (Probability.PMF.uniformOfFintype (ι → Bool)) 0 F

The uniform distribution fools every function exactly.

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

Fooling with error ε implies fooling with any larger error.

theorem Cslib.BitString.fools_bitVal_of_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : PMF (ι → Bool)} {ε : ℝ} {F : (ι → Bool) → Bool} (h : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F x)) - ε ≤ ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (F x)) (hn : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ !F x) - ε ≤ ∑ x : ι → Bool, (X x).toReal * bitVal ℝ !F x) : Fools X ε fun (x : ι → Bool) => bitVal ℝ (F x)

Two one-sided bounds fool a Boolean function: if the expectations under X of a Boolean function F and of its negation are each at least their uniform expectation minus ε, then X ε-fools F Braverman, after Lemma 12.

@[reducible, inline]

abbrev Cslib.BitString.IsKWiseIndependent {ι : Type u_1} [Fintype ι] [DecidableEq ι] (k : ℕ) (X : PMF (ι → Bool)) : Prop

A distribution on the cube is k-wise independent if every k of its coordinates are independent and uniform; equivalently, its bias at every nonempty set of at most k coordinates vanishes (IsKWiseSmallBias.dist_map_restrict_le), which is the definition used here.

theorem Cslib.BitString.sum_mul_eq_sum_fourierCoeff_mul_bias {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : PMF (ι → Bool)) (f : (ι → Bool) → ℝ) : ∑ x : ι → Bool, (X x).toReal * f x = ∑ S : Finset ι, fourierCoeff f S * bias X S

The expectation of f under X is the sum over sets S of the Fourier coefficient of f at S times the bias of X at S.

theorem Cslib.BitString.isKWiseIndependent_uniformOfFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (k : ℕ) : IsKWiseIndependent k (Probability.PMF.uniformOfFintype (ι → Bool))

The uniform distribution is k-wise independent for every k.

theorem Cslib.BitString.IsKWiseIndependent.sum_mul_eq_expect_of_mem_lowDegree {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {X : PMF (ι → Bool)} {P : (ι → Bool) → ℝ} (hX : IsKWiseIndependent k X) (hP : P ∈ lowDegree ℝ ι k) : ∑ x : ι → Bool, (X x).toReal * P x = Finset.univ.expect fun (x : ι → Bool) => P x

A k-wise independent distribution gives a function of degree at most k its uniform expectation Braverman, Proposition 6.

theorem Cslib.BitString.IsKWiseIndependent.fools_of_mem_lowDegree {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {X : PMF (ι → Bool)} {P : (ι → Bool) → ℝ} (hX : IsKWiseIndependent k X) (hP : P ∈ lowDegree ℝ ι k) : Fools X 0 P

k-wise independence fools degree-k functions exactly Braverman, Proposition 6.

theorem Cslib.Probability.IsKWiseIndependentHash.isKWiseIndependent_map {ι : Type u_1} {Seed : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Seed] [Nonempty Seed] {k : ℕ} {h : Seed → ι → Bool} (hh : IsKWiseIndependentHash k h) : BitString.IsKWiseIndependent k (PMF.map h (PMF.uniformOfFintype Seed))

Seeded k-wise independent families are k-wise independent distributions: a uniformly random member of a k-wise independent family of bit strings is a k-wise independent distribution on the cube.