theorem BooleanFourier.fourierCoeff_empty_eq_expect {n : ℕ} (f : BoolFn n) : fourierCoeff f ∅ = expect f

theorem BooleanFourier.variance_eq_sum_fourierCoeff_sq_nonempty {n : ℕ} (f : BoolFn n) : variance f = ∑ S : Finset (Fin n) with S ≠ ∅, fourierCoeff f S ^ 2

theorem BooleanFourier.poincare_inequality {n : ℕ} (f : BoolFn n) : variance f ≤ totalInfluenceReal f