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

theorem BooleanFourier.vol_nonneg {n : ℕ} (f : (Fin n → Bool) → Bool) : 0 ≤ vol f

theorem BooleanFourier.vol_le_one {n : ℕ} (f : (Fin n → Bool) → Bool) : vol f ≤ 1

theorem BooleanFourier.parseval_signed {n : ℕ} (f : (Fin n → Bool) → Bool) : ∑ S : Finset (Fin n), fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ^ 2 = 1

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

theorem BooleanFourier.boolToReal_agreement_indicator {n : ℕ} (f : (Fin n → Bool) → Bool) (x y : Fin n → Bool) : (if boolToReal (f x) * boolToReal (f y) = boolToReal (f (boolMul x y)) then 1 else 0) = (1 + boolToReal (f x) * boolToReal (f y) * boolToReal (f (boolMul x y))) / 2

theorem BooleanFourier.tripleCorrelation_eq_sum_cube {n : ℕ} (g : (Fin n → Bool) → ℝ) : (1 / 2 ^ n) ^ 2 * ∑ x : Fin n → Bool, ∑ y : Fin n → Bool, g x * g y * g (boolMul x y) = ∑ S : Finset (Fin n), fourierCoeff g S ^ 3

theorem BooleanFourier.agreementProb_eq {n : ℕ} (f : (Fin n → Bool) → Bool) : agreementProb f = (1 + ∑ S : Finset (Fin n), fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ^ 3) / 2

theorem flipCoord_eq_flipAt {n : ℕ} (x : Fin n → Bool) (i : Fin n) : BooleanFourier.flipCoord x i = BooleanFourier.flipAt i x

theorem influence_eq_influenceReal {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) : BooleanFourier.influence f i = BooleanFourier.influenceReal (fun (x : Fin n → Bool) => BooleanFourier.boolToReal (f x)) i

theorem totalInfluence_eq_totalInfluenceReal {n : ℕ} (f : (Fin n → Bool) → Bool) : BooleanFourier.totalInfluence f = BooleanFourier.totalInfluenceReal fun (x : Fin n → Bool) => BooleanFourier.boolToReal (f x)

theorem totalInfluence_eq_weighted_fourier' {n : ℕ} (f : (Fin n → Bool) → Bool) : BooleanFourier.totalInfluence f = ∑ S : Finset (Fin n), ↑S.card * BooleanFourier.fourierCoeff (fun (x : Fin n → Bool) => BooleanFourier.boolToReal (f x)) S ^ 2

theorem BooleanFourier.exists_fourierCoeff_ge_of_sum_cube_ge {n : ℕ} (f : (Fin n → Bool) → Bool) (δ : ℝ) (hδ : ∑ S : Finset (Fin n), fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ^ 3 ≥ 2 * δ) : ∃ (S : Finset (Fin n)), fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ≥ 2 * δ

theorem BooleanFourier.exists_fourierCoeff_ge_of_agreementProb {n : ℕ} (f : (Fin n → Bool) → Bool) (δ : ℝ) (hδ : agreementProb f ≥ 1 / 2 + δ) : ∃ (S : Finset (Fin n)), fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) S ≥ 2 * δ