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

theorem BooleanFourier.plancherel {n : ℕ} (f g : (Fin n → Bool) → ℝ) : ∑ S : Finset (Fin n), fourierCoeff f S * fourierCoeff g S = innerProduct f g

theorem BooleanFourier.parseval {n : ℕ} (f : (Fin n → Bool) → ℝ) : ∑ S : Finset (Fin n), fourierCoeff f S ^ 2 = 1 / 2 ^ n * ∑ x : Fin n → Bool, f x ^ 2

theorem BooleanFourier.claim_2_2 {n : ℕ} (f g : (Fin n → Bool) → ℝ) : ∑ S : Finset (Fin n), fourierCoeff f S * fourierCoeff g S = 1 / 2 ^ n * ∑ x : Fin n → Bool, f x * g x ∧ ∑ S : Finset (Fin n), fourierCoeff f S ^ 2 = 1 / 2 ^ n * ∑ x : Fin n → Bool, f x ^ 2