theorem BooleanFourier.sum_boolToReal_eq {n : ℕ} (f : (Fin n → Bool) → Bool) : ∑ x : Fin n → Bool, boolToReal (f x) = 2 * ↑{x : Fin n → Bool | f x = true}.card - 2 ^ n

theorem BooleanFourier.fourierCoeff_empty_eq {n : ℕ} (f : (Fin n → Bool) → Bool) : fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) ∅ = 2 * vol f - 1

theorem BooleanFourier.varianceReal_boolToReal_eq {n : ℕ} (f : (Fin n → Bool) → Bool) : (varianceReal fun (x : Fin n → Bool) => boolToReal (f x)) = 4 * vol f * (1 - vol f)

theorem BooleanFourier.edge_isoperimetric_inequality {n : ℕ} (f : (Fin n → Bool) → Bool) : totalInfluence f ≥ 4 * vol f * (1 - vol f)

theorem BooleanFourier.corollary_3_2 {n : ℕ} (f : (Fin n → Bool) → Bool) : 4 * vol f * (1 - vol f) ≤ totalInfluence f