Low-degree Boolean functions have few relevant coordinates

A coordinate i is relevant to a Boolean function f when flipping bit i changes the value of f on some input; read as signs, this is exactly when the influence of i on f is nonzero (BitString.influence_signVal_ne_zero_iff). A Boolean function of degree at most d has at most d * 2 ^ (d - 1) relevant coordinates (BitString.card_filter_influence_ne_zero_le, BitString.card_filter_exists_update_ne_le) [NS94] O'Donnell, Chapter 3. The other bound of the same paper, bs(f) ≤ 2 deg(f)², is QueryComplexity.blockSensitivity_le_two_mul_degree_sq.

The degree hypothesis is that f, read as signs, lies in BitString.lowDegree ℝ ι d, equivalently that its Fourier coefficients vanish on the sets of more than d coordinates (BitString.mem_lowDegree_iff_fourierCoeff_eq_zero). For f : BooleanFunction n it holds with d = QueryComplexity.degree f (QueryComplexity.degree_le_iff_mem_lowDegree, BitString.signVal_comp_mem_lowDegree_iff), and for a function computed by a decision tree of depth d (DecisionTree.comp_eval_mem_lowDegree).

The influence of i is the density of the points where the derivative in i is nonzero (BitString.influence_signVal_eq_dens), and this derivative has degree at most d - 1. By Schwartz–Zippel on the cube, a nonzero influence is therefore at least 2 ^ (1 - d) (BitString.one_le_two_pow_mul_influence_of_degree), while the influences sum to at most d (BitString.totalInfluence_signVal_le_of_degree).

Main results

• Cslib.BitString.one_le_two_pow_mul_influence_of_degree, Cslib.BitString.one_le_two_pow_mul_influence_of_fourierCoeff_eq_zero: granularity of the influences of a low-degree Boolean function.
• Cslib.BitString.card_filter_influence_ne_zero_le, Cslib.BitString.card_filter_influence_ne_zero_le_of_fourierCoeff_eq_zero, Cslib.BitString.card_filter_exists_update_ne_le, Cslib.BitString.card_filter_exists_update_ne_le_of_fourierCoeff_eq_zero: the Nisan–Szegedy bound on the number of relevant coordinates.

References

• N. Nisan and M. Szegedy, On the Degree of Boolean Functions as Real Polynomials
• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.one_le_two_pow_mul_influence_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : ∀ (S : Finset ι), d < S.card → fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S = 0) (i : ι) (hi : (influence i fun (x : ι → Bool) => signVal (f x)) ≠ 0) : 1 ≤ 2 ^ (d - 1) * influence i fun (x : ι → Bool) => signVal (f x)

Granularity of influences, Fourier-coefficient form: a nonzero influence of a Boolean function whose Fourier coefficients, read as signs, vanish above degree d is at least 2 ^ (1 - d).

theorem Cslib.BitString.one_le_two_pow_mul_influence_of_degree {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : (fun (x : ι → Bool) => signVal (f x)) ∈ lowDegree ℝ ι d) (i : ι) (hi : (influence i fun (x : ι → Bool) => signVal (f x)) ≠ 0) : 1 ≤ 2 ^ (d - 1) * influence i fun (x : ι → Bool) => signVal (f x)

Granularity of influences: a nonzero influence of a Boolean function of degree at most d, read as signs, is at least 2 ^ (1 - d).

theorem Cslib.BitString.card_filter_influence_ne_zero_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : (fun (x : ι → Bool) => signVal (f x)) ∈ lowDegree ℝ ι d) : {i : ι | (influence i fun (x : ι → Bool) => signVal (f x)) ≠ 0}.card ≤ d * 2 ^ (d - 1)

The Nisan–Szegedy bound, in terms of influences: a Boolean function of degree at most d, read as signs, has at most d * 2 ^ (d - 1) coordinates of nonzero influence [NS94].

theorem Cslib.BitString.card_filter_influence_ne_zero_le_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : ∀ (S : Finset ι), d < S.card → fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S = 0) : {i : ι | (influence i fun (x : ι → Bool) => signVal (f x)) ≠ 0}.card ≤ d * 2 ^ (d - 1)

The Nisan–Szegedy bound, in terms of influences and Fourier coefficients: a Boolean function whose Fourier coefficients, read as signs, vanish above degree d has at most d * 2 ^ (d - 1) coordinates of nonzero influence [NS94].

theorem Cslib.BitString.card_filter_exists_update_ne_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : (fun (x : ι → Bool) => signVal (f x)) ∈ lowDegree ℝ ι d) : {i : ι | ∃ (x : ι → Bool), f (Function.update x i !x i) ≠ f x}.card ≤ d * 2 ^ (d - 1)

The Nisan–Szegedy bound on relevant coordinates: a Boolean function of degree at most d, read as signs, has at most d * 2 ^ (d - 1) coordinates whose flip changes its value on some input [NS94].

theorem Cslib.BitString.card_filter_exists_update_ne_le_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : ∀ (S : Finset ι), d < S.card → fourierCoeff (fun (x : ι → Bool) => signVal (f x)) S = 0) : {i : ι | ∃ (x : ι → Bool), f (Function.update x i !x i) ≠ f x}.card ≤ d * 2 ^ (d - 1)

The Nisan–Szegedy bound on relevant coordinates, Fourier-coefficient form: a Boolean function whose Fourier coefficients, read as signs, vanish above degree d has at most d * 2 ^ (d - 1) coordinates whose flip changes its value on some input [NS94].