noncomputable def BooleanFourier.expect {n : ℕ} (f : BoolFn n) : ℝ

noncomputable def BooleanFourier.variance {n : ℕ} (f : BoolFn n) : ℝ

noncomputable def BooleanFourier.fourierInfluence {n : ℕ} (f : BoolFn n) (i : Fin n) : ℝ

theorem BooleanFourier.fourierCoeff_sq_le_fourierInfluence {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) (i : Fin n) (hi : i ∈ S) : fourierCoeff f S ^ 2 ≤ fourierInfluence f i

theorem BooleanFourier.fourierCoeff_sq_le_avg_fourierInfluence {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) (hS : S.Nonempty) : fourierCoeff f S ^ 2 ≤ 1 / ↑S.card * ∑ i ∈ S, fourierInfluence f i

theorem BooleanFourier.variance_le_talagrand_functional {n : ℕ} (f : BoolFn n) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) : variance f ≤ 2 * Real.exp 1 * ∑ i : Fin n, fourierInfluence f i / (1 + Real.log (1 / fourierInfluence f i))

theorem BooleanFourier.talagrand_influence_inequality : ∃ c > 0, ∀ (n : ℕ) (f : BoolFn n), (∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) → ∑ i : Fin n, fourierInfluence f i / (1 + Real.log (1 / fourierInfluence f i)) ≥ c * variance f