theorem BooleanFourier.expected_sqrt_sensitivity_lower_bound {n : ℕ} (f : (Fin n → Bool) → Bool) : 1 / 2 ^ n * ∑ x : Fin n → Bool, √↑(sensitivity f x) ≥ 1 / 2 * variance fun (x : Fin n → Bool) => boolToReal (f x)