Functions of low degree: influence and Schwartz–Zippel on the cube

A real function g on the cube has degree at most d when g ∈ BitString.lowDegree ℝ ι d, equivalently when its Fourier coefficients vanish on the sets of more than d coordinates (BitString.mem_lowDegree_iff_fourierCoeff_eq_zero), as in DecisionTree.comp_eval_mem_lowDegree and DecisionTree.fourierCoeff_eq_zero_of_depth_lt.

By the spectral formula for the total influence, such a function has total influence at most d times its mean square (BitString.totalInfluence_le_mul_expect_sq_of_degree), so a Boolean function of degree at most d, read as signs, has total influence at most d (BitString.totalInfluence_signVal_le_of_degree) O'Donnell, Chapter 3.

Schwartz–Zippel on the cube: a nonzero function of degree at most k is nonzero on at least a 2 ^ (-k) fraction of the cube (BitString.one_le_two_pow_mul_dens_ne_zero, BitString.two_pow_card_le_two_pow_mul_card_ne_zero) O'Donnell, Chapter 3. Take a set S of the Fourier support that is maximal for inclusion. Differentiating in a coordinate of S keeps S minus that coordinate maximal in the support of the derivative, while a derivative is nonzero on at most twice as many points as the function (averaging over one bit); after differentiating in every coordinate of S, the derivative is a nonzero constant.

Main results

• Cslib.BitString.totalInfluence_le_mul_expect_sq_of_degree, Cslib.BitString.totalInfluence_le_mul_expect_sq_of_fourierCoeff_eq_zero, Cslib.BitString.totalInfluence_signVal_le_of_degree, Cslib.BitString.totalInfluence_signVal_le_of_fourierCoeff_eq_zero: the total influence is at most the degree times the mean square; a Boolean function has total influence at most its degree.
• Cslib.BitString.dens_derivative_ne_zero_le: a derivative is nonzero at most twice as often as the function.
• Cslib.BitString.one_le_two_pow_mul_dens_ne_zero, Cslib.BitString.one_le_two_pow_mul_dens_ne_zero_of_fourierCoeff_eq_zero, Cslib.BitString.two_pow_card_le_two_pow_mul_card_ne_zero, Cslib.BitString.two_pow_card_le_two_pow_mul_card_ne_zero_of_fourierCoeff_eq_zero: Schwartz–Zippel on the cube.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.totalInfluence_le_mul_expect_sq_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → ℝ) {d : ℕ} (hdeg : ∀ (S : Finset ι), d < S.card → fourierCoeff g S = 0) : totalInfluence g ≤ ↑d * Finset.univ.expect fun (x : ι → Bool) => g x ^ 2

Total influence at most the degree times the mean square, Fourier-coefficient form: a real function whose Fourier coefficients vanish above degree d has total influence at most d times its mean square.

theorem Cslib.BitString.totalInfluence_le_mul_expect_sq_of_degree {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → ℝ) {d : ℕ} (hdeg : g ∈ lowDegree ℝ ι d) : totalInfluence g ≤ ↑d * Finset.univ.expect fun (x : ι → Bool) => g x ^ 2

Total influence at most the degree times the mean square: a real function of degree at most d has total influence at most d times its mean square.

theorem Cslib.BitString.totalInfluence_signVal_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) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ ↑d

Total influence at most the degree, Fourier-coefficient form: a Boolean function whose Fourier coefficients, read as signs, vanish above degree d has total influence at most d O'Donnell, Chapter 3.

theorem Cslib.BitString.totalInfluence_signVal_le_of_degree {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {d : ℕ} (hdeg : (fun (x : ι → Bool) => signVal (f x)) ∈ lowDegree ℝ ι d) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ ↑d

Total influence at most the degree: a Boolean function of degree at most d, read as signs, has total influence at most d O'Donnell, Chapter 3.

theorem Cslib.BitString.dens_derivative_ne_zero_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (h : (ι → Bool) → ℝ) (i : ι) : ↑{x : ι → Bool | derivative i h x ≠ 0}.dens ≤ 2 * ↑{x : ι → Bool | h x ≠ 0}.dens

A derivative is nonzero at most twice as often as the function: the density of the points where the derivative of h in i is nonzero is at most twice the density of the points where h is nonzero.

theorem Cslib.BitString.one_le_two_pow_mul_dens_ne_zero_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → ℝ) {k : ℕ} (hdeg : ∀ (S : Finset ι), k < S.card → fourierCoeff g S = 0) (hg : g ≠ 0) : 1 ≤ 2 ^ k * ↑{x : ι → Bool | g x ≠ 0}.dens

Schwartz–Zippel on the cube, Fourier-coefficient form: a nonzero real function whose Fourier coefficients vanish above degree k is nonzero on at least a 2 ^ (-k) fraction of the cube.

theorem Cslib.BitString.one_le_two_pow_mul_dens_ne_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → ℝ) {k : ℕ} (hdeg : g ∈ lowDegree ℝ ι k) (hg : g ≠ 0) : 1 ≤ 2 ^ k * ↑{x : ι → Bool | g x ≠ 0}.dens

Schwartz–Zippel on the cube: a nonzero real function of degree at most k is nonzero on at least a 2 ^ (-k) fraction of the cube.

theorem Cslib.BitString.two_pow_card_le_two_pow_mul_card_ne_zero_of_fourierCoeff_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → ℝ) {k : ℕ} (hdeg : ∀ (S : Finset ι), k < S.card → fourierCoeff g S = 0) (hg : g ≠ 0) : 2 ^ Fintype.card ι ≤ 2 ^ k * {x : ι → Bool | g x ≠ 0}.card

Schwartz–Zippel on the cube, counting and Fourier-coefficient form: a nonzero real function whose Fourier coefficients vanish above degree k on n coordinates is nonzero on at least 2 ^ (n - k) points of the cube.

theorem Cslib.BitString.two_pow_card_le_two_pow_mul_card_ne_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → ℝ) {k : ℕ} (hdeg : g ∈ lowDegree ℝ ι k) (hg : g ≠ 0) : 2 ^ Fintype.card ι ≤ 2 ^ k * {x : ι → Bool | g x ≠ 0}.card

Schwartz–Zippel on the cube, counting form: a nonzero real function of degree at most k on n coordinates is nonzero on at least 2 ^ (n - k) points of the cube.