Influences on the Boolean cube

The derivative of a real function f on the cube in coordinate i is half the difference between its values at bit i equal to false (sign 1) and to true (sign -1) (BitString.derivative); it is O'Donnell's Dᵢ f when bits are read as the signs BitString.signVal. The influence of i on f is the mean square of this derivative (BitString.influence), and the total influence of f is the sum of its influences (BitString.totalInfluence).

Differentiating in i removes i from the sets containing it and kills the others (BitString.fourierCoeff_derivative), so the influence of i is the Fourier weight of f on the sets containing i (BitString.influence_eq_sum_fourierCoeff_sq), and the total influence weighs each squared coefficient by the size of its set (BitString.totalInfluence_eq_sum_card_mul_fourierCoeff_sq). Since the variance is the weight on the nonempty sets (BitString.expect_sub_expect_sq_eq_sum_fourierCoeff_sq), it is at most the total influence (the Poincaré inequality, BitString.expect_sub_expect_sq_le_totalInfluence).

For a Boolean function read as signs, the derivative in i takes the values 0 and ±1 (BitString.sq_derivative_signVal) and is nonzero exactly where flipping bit i changes the value (BitString.derivative_signVal_ne_zero_iff). So the influence of i is the probability that flipping bit i changes the value (BitString.influence_signVal, BitString.influence_signVal_eq_dens), it is nonzero exactly when some flip of bit i changes the value (BitString.influence_signVal_ne_zero_iff), and the total influence is the expected number of bits whose flip changes the value, the average sensitivity (BitString.totalInfluence_signVal) O'Donnell, Sections 2.2 and 2.3.

Main definitions

• Cslib.BitString.derivative: the derivative in a coordinate.
• Cslib.BitString.influence: the influence of a coordinate.
• Cslib.BitString.totalInfluence: the total influence.

Main results

• Cslib.BitString.derivative_chi, Cslib.BitString.fourierCoeff_derivative: the derivative of a character, and the Fourier coefficients of a derivative.
• Cslib.BitString.influence_eq_sum_fourierCoeff_sq: the influence of i is the Fourier weight on the sets containing i.
• Cslib.BitString.influence_signVal, Cslib.BitString.influence_signVal_eq_dens: the influence on a Boolean function is the probability that a flip changes its value.
• Cslib.BitString.influence_signVal_ne_zero_iff: a coordinate has nonzero influence on a Boolean function exactly when flipping it changes the value on some input.
• Cslib.BitString.totalInfluence_eq_sum_card_mul_fourierCoeff_sq: the spectral formula for the total influence.
• Cslib.BitString.totalInfluence_signVal: the total influence of a Boolean function is the expected number of sensitive coordinates, for an arbitrary finite coordinate type.
• Cslib.BitString.expect_sub_expect_sq_eq_sum_fourierCoeff_sq: the variance is the Fourier weight on the nonempty sets.
• Cslib.BitString.expect_sub_expect_sq_le_totalInfluence: the Poincaré inequality.
• Cslib.BitString.influence_chi, Cslib.BitString.totalInfluence_chi: the influences of a character.
• Cslib.BitString.totalInfluence_le_mul_expect_sq: the total influence is at most the number of coordinates times the mean square.
• Cslib.BitString.expect_sub_expect_sq_signVal_le_one, Cslib.BitString.influence_signVal_le_one: a Boolean function read as signs has variance and influences at most one.

References

• R. O'Donnell, Analysis of Boolean Functions

noncomputable def Cslib.BitString.derivative {ι : Type u_1} [DecidableEq ι] (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ

The derivative of f in coordinate i: half the difference between the values of f at bit i equal to false, of sign 1, and to true, of sign -1.

@[simp]

theorem Cslib.BitString.derivative_update {ι : Type u_1} [DecidableEq ι] (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) (b : Bool) : derivative i f (Function.update x i b) = derivative i f x

The derivative in i does not depend on bit i.

theorem Cslib.BitString.derivative_chi {ι : Type u_1} [DecidableEq ι] (i : ι) (S : Finset ι) (x : ι → Bool) : derivative i (chi ℝ S) x = if i ∈ S then chi ℝ (S.erase i) x else 0

The derivative of a character: differentiating in i removes i from a set containing it, and kills the characters of the other sets.

theorem Cslib.BitString.sq_derivative_signVal {ι : Type u_1} [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) : derivative i (fun (x : ι → Bool) => signVal (f x)) x ^ 2 = |derivative i (fun (x : ι → Bool) => signVal (f x)) x|

The derivative of a Boolean function read as signs takes the values 0 and ±1, so its square is its absolute value.

theorem Cslib.BitString.derivative_signVal_ne_zero_iff {ι : Type u_1} [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) : derivative i (fun (x : ι → Bool) => signVal (f x)) x ≠ 0 ↔ f (Function.update x i !x i) ≠ f x

The derivative in i of a Boolean function read as signs is nonzero exactly where flipping bit i changes the value.

theorem Cslib.BitString.derivative_eq_sum {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) (x : ι → Bool) : derivative i f x = ∑ S : Finset ι with i ∈ S, fourierCoeff f S * chi ℝ (S.erase i) x

The Fourier expansion of a derivative: differentiating in i keeps the sets containing i, with i removed.

theorem Cslib.BitString.fourierCoeff_derivative {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) (T : Finset ι) : fourierCoeff (derivative i f) T = if i ∈ T then 0 else fourierCoeff f (insert i T)

The Fourier coefficients of a derivative: the coefficient of the derivative in i on a set avoiding i is the coefficient of f on the set with i added, and it vanishes on the sets containing i O'Donnell, Section 2.2.

noncomputable def Cslib.BitString.influence {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) : ℝ

The influence of coordinate i on f: the mean square of the derivative of f in i.

theorem Cslib.BitString.influence_nonneg {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) : 0 ≤ influence i f

Influences are nonnegative.

theorem Cslib.BitString.influence_eq_sum_fourierCoeff_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) : influence i f = ∑ S : Finset ι with i ∈ S, fourierCoeff f S ^ 2

The influence of i is the Fourier weight on the sets containing i O'Donnell, Section 2.2.

theorem Cslib.BitString.influence_le_expect_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) : influence i f ≤ Finset.univ.expect fun (x : ι → Bool) => f x ^ 2

The influence of a coordinate is at most the mean square.

theorem Cslib.BitString.influence_chi {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (S : Finset ι) : influence i (chi ℝ S) = if i ∈ S then 1 else 0

The influence of i on a character is one if i is in its set, and zero otherwise.

theorem Cslib.BitString.influence_signVal {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → Bool) : (influence i fun (x : ι → Bool) => signVal (f x)) = Finset.univ.expect fun (x : ι → Bool) => if f (Function.update x i !x i) = f x then 0 else 1

The influence on a Boolean function read as signs is the probability that flipping bit i changes the value O'Donnell, Section 2.2.

theorem Cslib.BitString.influence_signVal_eq_dens {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → Bool) (i : ι) : (influence i fun (x : ι → Bool) => signVal (f x)) = ↑{x : ι → Bool | derivative i (fun (x : ι → Bool) => signVal (f x)) x ≠ 0}.dens

The influence of i on a Boolean function read as signs is the density of the points where its derivative in i is nonzero.

theorem Cslib.BitString.influence_signVal_ne_zero_iff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → Bool) (i : ι) : (influence i fun (x : ι → Bool) => signVal (f x)) ≠ 0 ↔ ∃ (x : ι → Bool), f (Function.update x i !x i) ≠ f x

Relevant coordinates: a coordinate has nonzero influence on a Boolean function read as signs exactly when flipping it changes the value of the function on some input.

noncomputable def Cslib.BitString.totalInfluence {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) : ℝ

The total influence of f: the sum of the influences of the coordinates.

theorem Cslib.BitString.totalInfluence_nonneg {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) : 0 ≤ totalInfluence f

The total influence is nonnegative.

theorem Cslib.BitString.influence_le_totalInfluence {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (f : (ι → Bool) → ℝ) : influence i f ≤ totalInfluence f

The influence of a coordinate is at most the total influence.

theorem Cslib.BitString.totalInfluence_eq_sum_card_mul_fourierCoeff_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) : totalInfluence f = ∑ S : Finset ι, ↑S.card * fourierCoeff f S ^ 2

The spectral formula for the total influence: each squared Fourier coefficient counts as many times as its set has elements O'Donnell, Section 2.3.

theorem Cslib.BitString.totalInfluence_signVal {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → Bool) : (totalInfluence fun (x : ι → Bool) => signVal (f x)) = Finset.univ.expect fun (x : ι → Bool) => ↑{i : ι | f (Function.update x i !x i) ≠ f x}.card

The total influence of a Boolean function read as signs is its average sensitivity: the expected number of bits whose flip changes the value O'Donnell, Section 2.3.

theorem Cslib.BitString.totalInfluence_chi {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S : Finset ι) : totalInfluence (chi ℝ S) = ↑S.card

A character has total influence the size of its set.

theorem Cslib.BitString.expect_sub_expect_sq_eq_sum_fourierCoeff_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => (f x - Finset.univ.expect fun (y : ι → Bool) => f y) ^ 2) = ∑ S : Finset ι with S ≠ ∅, fourierCoeff f S ^ 2

The variance is the Fourier weight on the nonempty sets O'Donnell, Section 1.4.

theorem Cslib.BitString.expect_sub_expect_sq_le_totalInfluence {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => (f x - Finset.univ.expect fun (y : ι → Bool) => f y) ^ 2) ≤ totalInfluence f

The Poincaré inequality: the variance is at most the total influence O'Donnell, Section 2.3.

theorem Cslib.BitString.totalInfluence_le_mul_expect_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → ℝ) : totalInfluence f ≤ ↑(Fintype.card ι) * Finset.univ.expect fun (x : ι → Bool) => f x ^ 2

The total influence is at most the number of coordinates times the mean square.

theorem Cslib.BitString.expect_sub_expect_sq_signVal_le_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : (ι → Bool) → Bool) : (Finset.univ.expect fun (x : ι → Bool) => (signVal (f x) - Finset.univ.expect fun (y : ι → Bool) => signVal (f y)) ^ 2) ≤ 1

The variance of a Boolean function read as signs is at most one.

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

The influence of a coordinate on a Boolean function read as signs is at most one.