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

theorem BooleanFourier.multilinearExtension_eq_on_boolToReal {n : ℕ} (f : (Fin n → Bool) → ℝ) (b : Fin n → Bool) : (multilinearExtension f fun (i : Fin n) => boolToReal (b i)) = f b

theorem BooleanFourier.multilinearExtension_unique {n : ℕ} (f : (Fin n → Bool) → ℝ) (coeffs : Finset (Fin n) → ℝ) (hagree : ∀ (b : Fin n → Bool), ∑ S : Finset (Fin n), coeffs S * ∏ i ∈ S, boolToReal (b i) = f b) : coeffs = fun (S : Finset (Fin n)) => fourierCoeff f S

theorem BooleanFourier.multilinearExtension_unique' {n : ℕ} (f : (Fin n → Bool) → ℝ) (coeffs : Finset (Fin n) → ℝ) (hagree : ∀ (b : Fin n → Bool), ∑ S : Finset (Fin n), coeffs S * ∏ i ∈ S, boolToReal (b i) = f b) (x : Fin n → ℝ) : ∑ S : Finset (Fin n), coeffs S * ∏ i ∈ S, x i = multilinearExtension f x