Influence and sensitivity

The total influence of a Boolean function, read as signs, is its average sensitivity, the expected value of sensitivityAt f x (BitString.totalInfluence_eq_expect_sensitivityAt) O'Donnell, Section 2.3, so it is at most the sensitivity (BitString.totalInfluence_le_sensitivity). A function computed by a decision tree of depth d has Fourier degree at most d, so its total influence is at most d (DecisionTree.totalInfluence_le_depth, a case of BitString.totalInfluence_signVal_le_of_degree).

Main results

• Cslib.BitString.totalInfluence_eq_expect_sensitivityAt: total influence is average sensitivity.
• Cslib.BitString.totalInfluence_le_sensitivity: total influence is at most sensitivity.
• Cslib.DecisionTree.totalInfluence_le_depth: functions of decision trees of depth d have total influence at most d.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.totalInfluence_eq_expect_sensitivityAt {n : ℕ} (f : BooleanFunction n) : (totalInfluence fun (x : Fin n → Bool) => signVal (f x)) = Finset.univ.expect fun (x : BitString n) => ↑(sensitivityAt f x)

The expected sensitivity at a uniformly sampled input is the total influence.

theorem Cslib.BitString.totalInfluence_le_sensitivity {n : ℕ} (f : BooleanFunction n) : (totalInfluence fun (x : Fin n → Bool) => signVal (f x)) ≤ ↑(sensitivity f)

The total influence of a Boolean function, read as signs, is at most its sensitivity.

theorem Cslib.DecisionTree.totalInfluence_le_depth {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] (g : β → Bool) (t : DecisionTree ι β) : (BitString.totalInfluence fun (x : ι → Bool) => BitString.signVal (g (t.eval x))) ≤ ↑t.depth

Decision trees of depth d have total influence at most d: a Boolean function of the output of a decision tree of depth d, read as signs, has Fourier weight only on sets of at most d coordinates, and its squared coefficients sum to one.