noncomputable def BooleanFourier.boolToReal (b : Bool) : ℝ

@[simp]

theorem BooleanFourier.boolToReal_true : boolToReal true = 1

@[simp]

theorem BooleanFourier.boolToReal_false : boolToReal false = -1

theorem BooleanFourier.boolToReal_sq (b : Bool) : boolToReal b ^ 2 = 1

theorem BooleanFourier.boolToReal_ne_zero (b : Bool) : boolToReal b ≠ 0

theorem BooleanFourier.boolToReal_mul_self (b : Bool) : boolToReal b * boolToReal b = 1

theorem BooleanFourier.boolToReal_not (b : Bool) : (boolToReal !b) = -boolToReal b

theorem BooleanFourier.one_add_boolToReal_mul_boolToReal (a b : Bool) : 1 + boolToReal a * boolToReal b = if a = b then 2 else 0

noncomputable def BooleanFourier.chi {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) : ℝ

@[simp]

theorem BooleanFourier.chi_empty {n : ℕ} (x : Fin n → Bool) : chi ∅ x = 1

theorem BooleanFourier.chi_sq {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) : chi S x ^ 2 = 1

theorem BooleanFourier.chi_mul_self {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) : chi S x * chi S x = 1

theorem BooleanFourier.chi_ne_zero {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) : chi S x ≠ 0

noncomputable def BooleanFourier.fourierCoeff {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) : ℝ

def BooleanFourier.flipAt {n : ℕ} (j : Fin n) (x : Fin n → Bool) : Fin n → Bool

theorem BooleanFourier.flipAt_flipAt {n : ℕ} (j : Fin n) (x : Fin n → Bool) : flipAt j (flipAt j x) = x

theorem BooleanFourier.flipAt_ne_self {n : ℕ} (j : Fin n) (x : Fin n → Bool) : flipAt j x ≠ x

theorem BooleanFourier.chi_flipAt {n : ℕ} (S : Finset (Fin n)) (j : Fin n) (hj : j ∈ S) (x : Fin n → Bool) : chi S (flipAt j x) = -chi S x

theorem BooleanFourier.sum_chi {n : ℕ} (S : Finset (Fin n)) : ∑ x : Fin n → Bool, chi S x = if S = ∅ then 2 ^ n else 0

theorem BooleanFourier.sum_chi_mul_chi {n : ℕ} (x y : Fin n → Bool) : ∑ S : Finset (Fin n), chi S x * chi S y = if x = y then 2 ^ n else 0

theorem BooleanFourier.fourier_expansion {n : ℕ} (f : (Fin n → Bool) → ℝ) (x : Fin n → Bool) : f x = ∑ S : Finset (Fin n), fourierCoeff f S * chi S x

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

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