Huang's sensitivity theorem

Every Boolean function satisfies deg(f) ≤ s(f)² [Hua19]. Gotsman and Linial reduced this to the induced subgraph theorem [GL92]: if f, read as signs, has a nonzero Fourier coefficient on S, then g = f ⊕ parity_S is unbalanced, so one of its fibers V contains more than half of the cube. By Huang's induced subgraph theorem (BitString.exists_mem_sqrt_card_le_card_update_mem) some x ∈ V has at least √|S| neighbors in V in the directions of S. Flipping a bit of S flips parity_S, so along these directions g is constant and f changes: f has at least √|S| sensitive coordinates at x (BitString.sqrt_card_le_sensitivity_of_fourierCoeff_ne_zero). A coefficient on a set of deg(f) coordinates gives √deg(f) ≤ s(f) (QueryComplexity.sqrt_degree_le_sensitivity).

Main results

• Cslib.BitString.sqrt_card_le_sensitivity_of_fourierCoeff_ne_zero: a nonzero Fourier coefficient on S forces sensitivity at least √|S|.
• Cslib.QueryComplexity.degree_le_sensitivity_sq: Huang's sensitivity theorem, deg(f) ≤ s(f)².
• Cslib.QueryComplexity.sqrt_degree_le_sensitivity: √deg(f) ≤ s(f).

References

• H. Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture
• C. Gotsman, N. Linial, The equivalence of two problems on the cube

theorem Cslib.BitString.sqrt_card_le_sensitivity_of_fourierCoeff_ne_zero {n : ℕ} {f : BooleanFunction n} {S : Finset (Fin n)} (h : fourierCoeff (fun (x : Fin n → Bool) => signVal (f x)) S ≠ 0) : √↑S.card ≤ ↑(sensitivity f)

A nonzero Fourier coefficient forces sensitivity: if f, read as signs, has a nonzero Fourier coefficient on S, then f has at least √|S| sensitive coordinates at some input.

theorem Cslib.QueryComplexity.degree_le_sensitivity_sq {n : ℕ} (f : BooleanFunction n) : degree f ≤ BitString.sensitivity f ^ 2

Huang's sensitivity theorem: the degree of a Boolean function is at most the square of its sensitivity, deg(f) ≤ s(f)² [Hua19].

theorem Cslib.QueryComplexity.sqrt_degree_le_sensitivity {n : ℕ} (f : BooleanFunction n) : √↑(degree f) ≤ ↑(BitString.sensitivity f)

Huang's sensitivity theorem: √deg(f) ≤ s(f).