Consequences of the Sensitivity Theorem

Main results

• degree_le_sensitivity_sq — the degree is at most the square of sensitivity

theorem Sensitivity.degree_le_sensitivity_sq {n : ℕ} (f : BoolFun n) : f.degree ≤ f.sensitivity ^ 2

The degree is at most the square of the sensitivity. Immediate corollary of the sensitivity theorem s(f) ≥ √deg(f): √d ≤ s implies d ≤ s².