noncomputable def BooleanFourier.linearBooleanFunction {n : ℕ} (a : Fin n → ℝ) : (Fin n → Bool) → ℝ

noncomputable def BooleanFourier.singletonCoeffs {n : ℕ} (a : Fin n → ℝ) : Finset (Fin n) → ℝ

theorem BooleanFourier.singletonCoeffs_singleton {n : ℕ} (a : Fin n → ℝ) (i : Fin n) : singletonCoeffs a {i} = a i

theorem BooleanFourier.singletonCoeffs_non_singleton {n : ℕ} (a : Fin n → ℝ) (S : Finset (Fin n)) (hS : ¬∃ (i : Fin n), S = {i}) : singletonCoeffs a S = 0

theorem BooleanFourier.singleton_filter_eq_image {n : ℕ} : {S : Finset (Fin n) | ∃ (i : Fin n), S = {i}} = Finset.image (fun (i : Fin n) => {i}) Finset.univ

theorem BooleanFourier.singletonCoeffs_agree {n : ℕ} (a : Fin n → ℝ) (b : Fin n → Bool) : ∑ S : Finset (Fin n), singletonCoeffs a S * ∏ i ∈ S, boolToReal (b i) = linearBooleanFunction a b

theorem BooleanFourier.singletonCoeffs_eval {n : ℕ} (a z : Fin n → ℝ) : ∑ S : Finset (Fin n), singletonCoeffs a S * ∏ i ∈ S, z i = ∑ i : Fin n, a i * z i

theorem BooleanFourier.linear_hybrid_fubini_bound {n : ℕ} (a : Fin n → ℝ) (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) (k : Fin n) (h_bound : ∀ (c : ℝ), |(Ψ (c + a k) + Ψ (c - a k)) / 2 - ∫ (t : ℝ), Ψ (c + a k * t) ∂ProbabilityTheory.gaussianReal 0 1| ≤ 1 / 2 * hΨ.thirdDerivBound * |a k| ^ 3) : |hybridExpectation (linearBooleanFunction a) Ψ ↑k - hybridExpectation (linearBooleanFunction a) Ψ (↑k + 1)| ≤ 1 / 2 * hΨ.thirdDerivBound * |a k| ^ 3

theorem BooleanFourier.lindeberg_per_step_bound_linear {n : ℕ} (a : Fin n → ℝ) (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) (k : Fin n) : |hybridExpectation (linearBooleanFunction a) Ψ ↑k - hybridExpectation (linearBooleanFunction a) Ψ (↑k + 1)| ≤ 1 / 2 * hΨ.thirdDerivBound * |a k| ^ 3

theorem BooleanFourier.invariance_principle {n : ℕ} (a : Fin n → ℝ) (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) : |booleanExpectation (linearBooleanFunction a) Ψ - gaussianExpectation (linearBooleanFunction a) Ψ| ≤ 1 / 2 * hΨ.thirdDerivBound * ∑ i : Fin n, |a i| ^ 3

theorem BooleanFourier.invariance_principle_general {n : ℕ} (f : (Fin n → Bool) → ℝ) (d : ℕ) (hdeg : degree f ≤ d) (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) : |booleanExpectation f Ψ - gaussianExpectation f Ψ| ≤ 1 / 2 * 2 ^ (3 * ↑d / 2) * hΨ.thirdDerivBound * ∑ i : Fin n, fourierInfluence f i ^ (3 / 2)

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

def BooleanFourier.HasUnitVariance {n : ℕ} (f : (Fin n → Bool) → ℝ) : Prop

theorem BooleanFourier.claim_2_2_invariance {n : ℕ} (f : (Fin n → Bool) → ℝ) (τ : ℝ) (_hτ : 0 ≤ τ) (hInf : ∀ (i : Fin n), fourierInfluence f i ≤ τ) : ∑ i : Fin n, fourierInfluence f i ^ (3 / 2) ≤ τ ^ (1 / 2) * ∑ i : Fin n, fourierInfluence f i

theorem BooleanFourier.fourierInfluence_eq_influenceReal {n : ℕ} (f : (Fin n → Bool) → ℝ) (i : Fin n) : fourierInfluence f i = influenceReal f i

theorem BooleanFourier.sum_fourierInfluence_eq_totalInfluenceReal {n : ℕ} (f : (Fin n → Bool) → ℝ) : ∑ i : Fin n, fourierInfluence f i = totalInfluenceReal f

theorem BooleanFourier.totalInfluenceReal_le_degree_mul_varianceReal {n : ℕ} (f : (Fin n → Bool) → ℝ) (d : ℕ) (hdeg : degree f ≤ d) : totalInfluenceReal f ≤ ↑d * varianceReal f

theorem BooleanFourier.invariance_principle_corollary (C : ℝ) (hC : C > 0) (ε : ℝ) (hε : ε > 0) (d : ℕ) : ∃ τ > 0, ∀ (n : ℕ) (f : (Fin n → Bool) → ℝ), degree f ≤ d → (∀ (i : Fin n), fourierInfluence f i ≤ τ) → varianceReal f ≤ C → ∀ (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ), hΨ.thirdDerivBound ≤ C → |booleanExpectation f Ψ - gaussianExpectation f Ψ| ≤ ε