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

theorem BooleanFourier.chi_flipAt_of_not_mem {n : ℕ} (S : Finset (Fin n)) (i : Fin n) (hi : i ∉ S) (x : Fin n → Bool) : chi S (flipAt i x) = chi S x

theorem BooleanFourier.chi_mul_chi_eq {n : ℕ} (S S' : Finset (Fin n)) (x : Fin n → Bool) : chi S x * chi S' x = chi (symmDiff S S') x

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

theorem BooleanFourier.influenceReal_eq_sum_fourierCoeff_sq {n : ℕ} (f : (Fin n → Bool) → ℝ) (i : Fin n) : influenceReal f i = ∑ S : Finset (Fin n) with i ∈ S, fourierCoeff f S ^ 2

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

theorem BooleanFourier.totalInfluenceReal_eq_sum_card_fourierCoeff_sq {n : ℕ} (f : (Fin n → Bool) → ℝ) : totalInfluenceReal f = ∑ S : Finset (Fin n), ↑S.card * fourierCoeff f S ^ 2

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

theorem BooleanFourier.totalInfluenceReal_ge_varianceReal {n : ℕ} (f : (Fin n → Bool) → ℝ) : totalInfluenceReal f ≥ varianceReal f

theorem BooleanFourier.sq_eq_self_of_zero_one {n : ℕ} (f : (Fin n → Bool) → ℝ) (hf : ∀ (x : Fin n → Bool), f x = 0 ∨ f x = 1) (x : Fin n → Bool) : f x ^ 2 = f x

theorem BooleanFourier.varianceReal_eq_quarter_of_balanced {n : ℕ} (f : (Fin n → Bool) → ℝ) (hf : ∀ (x : Fin n → Bool), f x = 0 ∨ f x = 1) (hbal : fourierCoeff f ∅ = 1 / 2) : varianceReal f = 1 / 4

theorem BooleanFourier.totalInfluenceReal_ge_quarter_of_balanced {n : ℕ} (f : (Fin n → Bool) → ℝ) (hf : ∀ (x : Fin n → Bool), f x = 0 ∨ f x = 1) (hbal : fourierCoeff f ∅ = 1 / 2) : totalInfluenceReal f ≥ 1 / 4