def BooleanFourier.boolMul {n : ℕ} (x y : Fin n → Bool) : Fin n → Bool

theorem BooleanFourier.boolToReal_xnor (a b : Bool) : (boolToReal !(a ^^ b)) = boolToReal a * boolToReal b

theorem BooleanFourier.chi_boolMul {n : ℕ} (S : Finset (Fin n)) (x y : Fin n → Bool) : chi S (boolMul x y) = chi S x * chi S y

theorem BooleanFourier.boolMul_comm {n : ℕ} (x y : Fin n → Bool) : boolMul x y = boolMul y x

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

theorem BooleanFourier.fourierCoeff_conv {n : ℕ} (f g : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) : fourierCoeff (conv f g) S = fourierCoeff f S * fourierCoeff g S