noncomputable def BooleanFourier.noiseSensitivity {n : ℕ} (δ : ℝ) (f : (Fin n → Bool) → Bool) : ℝ

theorem BooleanFourier.parseval_boolToReal {n : ℕ} (f : (Fin n → Bool) → Bool) : ∑ S : Finset (Fin n), fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ^ 2 = 1

theorem BooleanFourier.noiseSensitivity_eq_fourier_sum {n : ℕ} (δ : ℝ) (f : (Fin n → Bool) → Bool) : noiseSensitivity δ f = 1 / 2 * ∑ S : Finset (Fin n), (1 - (1 - 2 * δ) ^ S.card) * fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ^ 2