One-sided approximation and k-wise independence

This file isolates the analytic part of Braverman's proof that bounded independence fools AC⁰, which does not mention circuits. Braverman approximates a Boolean function F from below by a low-degree polynomial that may depend on the distribution, so the bounds here are one-sided; the two-sided bound follows by applying them to F and to its negation (Cslib.BitString.fools_bitVal_of_le).

• Mollification [Braverman, Lemma 10]: suppose a real function f agrees with F off an error event E, is bounded by L, and Ẽ approximates the indicator of E in L² with error δ. Then f (1 - Ẽ) vanishes wherever F ∨ E is false, and its squared L² distance from F ∨ E is at most 2 P[E] + 2 L² δ (Cslib.BitString.expect_sq_bitVal_or_sub_mul_one_sub_le).
• Squaring trick [Braverman, Lemma 11]: if f vanishes wherever a Boolean function F' is false, then 1 - (1 - f)² lies below F', has at most twice the degree of f, and its expected gap to F' is the squared L² distance from f to F'.
• One-sided chain [Braverman, proof of Lemma 12]: if a k-wise independent distribution μ and the uniform distribution both see F ≠ F' with probability at most a, and a polynomial of degree at most k lies below F' with expected gap at most b, then the expectation of F under μ is at least its uniform expectation minus 2 a + b.

Main results

• Cslib.BitString.expect_sq_bitVal_or_sub_mul_one_sub_le: the mollification bound.
• Cslib.BitString.one_sub_one_sub_sq_le_bitVal, Cslib.BitString.expect_bitVal_sub_one_sub_one_sub_sq, Cslib.BitString.one_sub_one_sub_sq_mem_lowDegree: the squaring trick.
• Cslib.BitString.IsKWiseIndependent.expect_bitVal_sub_le_of_le: the one-sided chain.
• Cslib.BitString.IsKWiseIndependent.expect_bitVal_sub_le_of_eq_zero: the squaring trick and the chain combined, [Braverman, Lemmas 11 and 12].
• Cslib.BitString.IsKWiseIndependent.expect_bitVal_sub_le_of_witness, Cslib.BitString.IsKWiseIndependent.fools_bitVal_of_witness: all three combined, for a function approximated off a rare witness event whose indicator has a low-degree L² approximation.

References

Lemma numbers follow the ECCC report TR09-011.

• M. Braverman, Polylogarithmic independence fools AC⁰ circuits

Mollification

theorem Cslib.BitString.bitVal_or_sub_mul_one_sub {ι : Type u_1} {F E : (ι → Bool) → Bool} {f : (ι → Bool) → ℝ} {x : ι → Bool} (hf : E x = false → f x = bitVal ℝ (F x)) : bitVal ℝ (F x || E x) - f x * (1 - bitVal ℝ (E x)) = bitVal ℝ (E x)

If f agrees with F off E, then F ∨ E minus f (1 - E) is the indicator of E.

theorem Cslib.BitString.mul_one_sub_eq_zero_of_or_eq_false {ι : Type u_1} {F E : (ι → Bool) → Bool} {f e : (ι → Bool) → ℝ} {x : ι → Bool} (hf : E x = false → f x = bitVal ℝ (F x)) (h : (F x || E x) = false) : f x * (1 - e x) = 0

If f agrees with F off E, then f (1 - e) vanishes wherever F ∨ E is false.

theorem Cslib.BitString.expect_sq_bitVal_or_sub_mul_one_sub_le {ι : Type u_1} {F E : (ι → Bool) → Bool} {f e : (ι → Bool) → ℝ} [Fintype ι] [DecidableEq ι] {L : ℝ} (hf : ∀ (x : ι → Bool), E x = false → f x = bitVal ℝ (F x)) (hL : ∀ (x : ι → Bool), |f x| ≤ L) : (Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (F x || E x) - f x * (1 - e x)) ^ 2) ≤ (2 * Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (E x)) + 2 * L ^ 2 * Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (E x) - e x) ^ 2

Mollification [Braverman, Lemma 10]: if f agrees with F off E and is bounded by L, then the squared L² distance from F ∨ E to f (1 - e) is at most twice the probability of E plus 2 L² times the squared L² distance from the indicator of E to e.

The squaring trick

theorem Cslib.BitString.bitVal_sub_one_sub_one_sub_sq {ι : Type u_1} {F' : (ι → Bool) → Bool} {f : (ι → Bool) → ℝ} {x : ι → Bool} (hf : F' x = false → f x = 0) : bitVal ℝ (F' x) - (1 - (1 - f x) ^ 2) = (bitVal ℝ (F' x) - f x) ^ 2

If f vanishes wherever F' is false, then the gap from 1 - (1 - f)² to F' is the square of the gap from f to F' [Braverman, Lemma 11].

theorem Cslib.BitString.one_sub_one_sub_sq_le_bitVal {ι : Type u_1} {F' : (ι → Bool) → Bool} {f : (ι → Bool) → ℝ} {x : ι → Bool} (hf : F' x = false → f x = 0) : 1 - (1 - f x) ^ 2 ≤ bitVal ℝ (F' x)

If f vanishes wherever F' is false, then 1 - (1 - f)² lies below F' [Braverman, Lemma 11].

theorem Cslib.BitString.expect_bitVal_sub_one_sub_one_sub_sq {ι : Type u_1} {F' : (ι → Bool) → Bool} {f : (ι → Bool) → ℝ} [Fintype ι] [DecidableEq ι] (hf : ∀ (x : ι → Bool), F' x = false → f x = 0) : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F' x) - (1 - (1 - f x) ^ 2)) = Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (F' x) - f x) ^ 2

If f vanishes wherever F' is false, then the expected gap from 1 - (1 - f)² to F' is the squared L² distance from f to F' [Braverman, Lemma 11].

theorem Cslib.BitString.one_sub_one_sub_sq_mem_lowDegree {ι : Type u_1} {R : Type u_2} [CommRing R] {g : (ι → Bool) → R} {D : ℕ} (hg : g ∈ lowDegree R ι D) : (fun (x : ι → Bool) => 1 - (1 - g x) ^ 2) ∈ lowDegree R ι (2 * D)

If f has degree at most D, then 1 - (1 - f)² has degree at most 2 D [Braverman, Lemma 11].

The one-sided chain

theorem Cslib.BitString.IsKWiseIndependent.expect_bitVal_sub_le_of_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {X : PMF (ι → Bool)} {F F' : (ι → Bool) → Bool} {a b : ℝ} (hX : IsKWiseIndependent k X) {p : (ι → Bool) → ℝ} (hpk : p ∈ lowDegree ℝ ι k) (hpF : ∀ (x : ι → Bool), p x ≤ bitVal ℝ (F' x)) (hXa : ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (F x ^^ F' x) ≤ a) (hUa : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F x ^^ F' x)) ≤ a) (hb : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F' x) - p x) ≤ b) : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F x)) - 2 * a - b ≤ ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (F x)

The one-sided chain [Braverman, proof of Lemma 12]: suppose F' disagrees with F with probability at most a under both a k-wise independent distribution X and the uniform distribution, and p has degree at most k, lies below F' and has expected gap at most b to F'. Then the expectation of F under X is at least its uniform expectation minus 2 a + b.

theorem Cslib.BitString.IsKWiseIndependent.expect_bitVal_sub_le_of_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {X : PMF (ι → Bool)} {F F' : (ι → Bool) → Bool} {a b : ℝ} (hX : IsKWiseIndependent k X) {f : (ι → Bool) → ℝ} {D : ℕ} (hf : f ∈ lowDegree ℝ ι D) (hDk : 2 * D ≤ k) (hf0 : ∀ (x : ι → Bool), F' x = false → f x = 0) (hXa : ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (F x ^^ F' x) ≤ a) (hUa : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F x ^^ F' x)) ≤ a) (hb : (Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (F' x) - f x) ^ 2) ≤ b) : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F x)) - 2 * a - b ≤ ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (F x)

Low-degree approximations vanishing off F' give one-sided bounds [Braverman, Lemmas 11 and 12]: suppose F' disagrees with F with probability at most a under both a k-wise independent distribution X and the uniform distribution, and f has degree at most D with 2 D ≤ k, vanishes wherever F' is false and has squared L² distance at most b to F'. Then the expectation of F under X is at least its uniform expectation minus 2 a + b.

theorem Cslib.BitString.IsKWiseIndependent.expect_bitVal_sub_le_of_witness {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {X : PMF (ι → Bool)} {F : (ι → Bool) → Bool} {a : ℝ} {E : (ι → Bool) → Bool} {f e : (ι → Bool) → ℝ} {D t : ℕ} {L δ : ℝ} (hX : IsKWiseIndependent k X) (hf : f ∈ lowDegree ℝ ι D) (he : e ∈ lowDegree ℝ ι t) (hk : 2 * (D + t) ≤ k) (hfE : ∀ (x : ι → Bool), E x = false → f x = bitVal ℝ (F x)) (hL : ∀ (x : ι → Bool), |f x| ≤ L) (hXE : ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (E x) ≤ a) (hUE : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (E x)) ≤ a) (hδ : (Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (E x) - e x) ^ 2) ≤ δ) : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (F x)) - 4 * a - 2 * L ^ 2 * δ ≤ ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (F x)

One-sided bound from an approximation with a witness [Braverman, Lemmas 10–12]: suppose f has degree at most D, is bounded by L and agrees with F wherever an event E fails, E has probability at most a under both a k-wise independent distribution X and the uniform distribution, and e of degree at most t, with 2 (D + t) ≤ k, approximates the indicator of E with squared L² error at most δ. Then the expectation of F under X is at least its uniform expectation minus 4 a + 2 L² δ.

theorem Cslib.BitString.IsKWiseIndependent.fools_bitVal_of_witness {ι : Type u_1} [Fintype ι] [DecidableEq ι] {k : ℕ} {X : PMF (ι → Bool)} {F : (ι → Bool) → Bool} {a : ℝ} {E : (ι → Bool) → Bool} {f e : (ι → Bool) → ℝ} {D t : ℕ} {L δ : ℝ} (hX : IsKWiseIndependent k X) (hf : f ∈ lowDegree ℝ ι D) (he : e ∈ lowDegree ℝ ι t) (hk : 2 * (D + t) ≤ k) (hfE : ∀ (x : ι → Bool), E x = false → f x = bitVal ℝ (F x)) (hL : ∀ (x : ι → Bool), |f x| ≤ L) (hXE : ∑ x : ι → Bool, (X x).toReal * bitVal ℝ (E x) ≤ a) (hUE : (Finset.univ.expect fun (x : ι → Bool) => bitVal ℝ (E x)) ≤ a) (hδ : (Finset.univ.expect fun (x : ι → Bool) => (bitVal ℝ (E x) - e x) ^ 2) ≤ δ) : Fools X (4 * a + 2 * (L + 1) ^ 2 * δ) fun (x : ι → Bool) => bitVal ℝ (F x)

Fooling from an approximation with a witness [Braverman, Lemmas 10–12 and Main Theorem]: under the hypotheses of expect_bitVal_sub_le_of_witness, the k-wise independent distribution X fools F with error 4 a + 2 (L + 1)² δ.

Braverman obtains the other direction by applying Lemma 12 to 1 - F, with a fresh approximation; reusing f and the witness via 1 - f is our variant (it avoids a NOT layer).