Influences of monotone Boolean functions

The derivative in i of a Boolean function read as signs takes the values 0 and ±1, so its square is its absolute value (BitString.sq_derivative_signVal). The coefficient of a function on {i} is the average of its derivative in i, so for every Boolean function it is at most the influence of i in absolute value (BitString.abs_fourierCoeff_singleton_le_influence). With the order false < true on bits and the signs signVal false = 1, signVal true = -1, the derivative of a monotone function is nonnegative, so its influences are its degree-one coefficients (BitString.influence_eq_fourierCoeff_singleton_of_monotone) O'Donnell, Section 2.2; for an antitone function they are their negatives.

The degree-one coefficients carry at most the variance (BitString.sum_fourierCoeff_singleton_sq_le), so by the Cauchy–Schwarz inequality a monotone or antitone Boolean function on n coordinates with variance σ² has total influence at most √(n σ²) (BitString.totalInfluence_le_sqrt_card_mul_of_monotone), in particular at most √n (BitString.totalInfluence_le_sqrt_card_of_monotone) O'Donnell, Section 2.3.

Main results

• Cslib.BitString.derivative_signVal_nonneg_of_monotone, Cslib.BitString.derivative_signVal_nonpos_of_antitone: the sign of the derivatives of a monotone or antitone function.
• Cslib.BitString.abs_fourierCoeff_singleton_le_influence: a degree-one coefficient is at most the influence in absolute value.
• Cslib.BitString.influence_eq_fourierCoeff_singleton_of_monotone, Cslib.BitString.influence_eq_neg_fourierCoeff_singleton_of_antitone: the influences of a monotone or antitone function are its degree-one coefficients, up to sign.
• Cslib.BitString.fourierCoeff_singleton_nonneg_of_monotone, Cslib.BitString.fourierCoeff_singleton_nonpos_of_antitone: the sign of the degree-one coefficients of a monotone or antitone function.
• Cslib.BitString.sum_fourierCoeff_singleton_sq_le: the degree-one weight is at most the variance.
• Cslib.BitString.sum_influence_sq_le_of_monotone: the squared influences of a monotone function sum to at most its variance.
• Cslib.BitString.totalInfluence_le_sqrt_card_mul_of_monotone, Cslib.BitString.totalInfluence_le_sqrt_card_of_monotone, Cslib.BitString.totalInfluence_le_sqrt_card_mul_of_antitone, Cslib.BitString.totalInfluence_le_sqrt_card_of_antitone: monotone and antitone functions have total influence at most √(n σ²) ≤ √n.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.derivative_signVal_nonneg_of_monotone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} (hf : Monotone f) (i : ι) (x : ι → Bool) : 0 ≤ derivative i (fun (x : ι → Bool) => signVal (f x)) x

The derivative of a monotone Boolean function read as signs is nonnegative: raising bit i from false (sign 1) to true (sign -1) can only raise the value.

theorem Cslib.BitString.derivative_signVal_nonpos_of_antitone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} (hf : Antitone f) (i : ι) (x : ι → Bool) : derivative i (fun (x : ι → Bool) => signVal (f x)) x ≤ 0

The derivative of an antitone Boolean function read as signs is nonpositive.

theorem Cslib.BitString.abs_fourierCoeff_singleton_le_influence {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → Bool) (i : ι) : |fourierCoeff (fun (x : ι → Bool) => signVal (f x)) {i}| ≤ influence i fun (x : ι → Bool) => signVal (f x)

The coefficient of a Boolean function, read as signs, on {i} is at most the influence of i in absolute value.

theorem Cslib.BitString.influence_eq_fourierCoeff_singleton_of_monotone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Monotone f) (i : ι) : (influence i fun (x : ι → Bool) => signVal (f x)) = fourierCoeff (fun (x : ι → Bool) => signVal (f x)) {i}

The influences of a monotone Boolean function are its degree-one coefficients: for a monotone function read as signs, the influence of i is the coefficient on {i} O'Donnell, Section 2.2.

theorem Cslib.BitString.influence_eq_neg_fourierCoeff_singleton_of_antitone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Antitone f) (i : ι) : (influence i fun (x : ι → Bool) => signVal (f x)) = -fourierCoeff (fun (x : ι → Bool) => signVal (f x)) {i}

The influences of an antitone Boolean function read as signs are the negatives of its degree-one coefficients.

theorem Cslib.BitString.fourierCoeff_singleton_nonneg_of_monotone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Monotone f) (i : ι) : 0 ≤ fourierCoeff (fun (x : ι → Bool) => signVal (f x)) {i}

A monotone Boolean function read as signs has nonnegative degree-one coefficients.

theorem Cslib.BitString.fourierCoeff_singleton_nonpos_of_antitone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Antitone f) (i : ι) : fourierCoeff (fun (x : ι → Bool) => signVal (f x)) {i} ≤ 0

An antitone Boolean function read as signs has nonpositive degree-one coefficients.

theorem Cslib.BitString.sum_fourierCoeff_singleton_sq_le {ι : Type u_1} [DecidableEq ι] [Fintype ι] (g : (ι → Bool) → ℝ) : ∑ i : ι, fourierCoeff g {i} ^ 2 ≤ Finset.univ.expect fun (x : ι → Bool) => (g x - Finset.univ.expect fun (y : ι → Bool) => g y) ^ 2

The degree-one weight is at most the variance: the squared coefficients on the singletons sum to at most the variance.

theorem Cslib.BitString.sum_influence_sq_le_of_monotone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Monotone f) : ∑ i : ι, (influence i fun (x : ι → Bool) => signVal (f x)) ^ 2 ≤ Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2

For a monotone Boolean function read as signs, the squared influences sum to at most the variance.

theorem Cslib.BitString.totalInfluence_le_sqrt_card_mul_of_monotone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Monotone f) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ √(↑(Fintype.card ι) * Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2)

Monotone functions have total influence at most √(n σ²): a monotone Boolean function on n coordinates, read as signs with variance σ², has total influence at most √(n σ²) O'Donnell, Section 2.3.

theorem Cslib.BitString.totalInfluence_le_sqrt_card_mul_of_antitone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Antitone f) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ √(↑(Fintype.card ι) * Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2)

Antitone functions have total influence at most √(n σ²): an antitone Boolean function on n coordinates, read as signs with variance σ², has total influence at most √(n σ²).

theorem Cslib.BitString.totalInfluence_le_sqrt_card_of_monotone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Monotone f) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ √↑(Fintype.card ι)

Monotone functions have total influence at most √n: a monotone Boolean function on n coordinates, read as signs, has total influence at most √n O'Donnell, Section 2.3.

theorem Cslib.BitString.totalInfluence_le_sqrt_card_of_antitone {ι : Type u_1} [DecidableEq ι] {f : (ι → Bool) → Bool} [Fintype ι] (hf : Antitone f) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) ≤ √↑(Fintype.card ι)

Antitone functions have total influence at most √n: an antitone Boolean function on n coordinates, read as signs, has total influence at most √n.