noncomputable def BooleanFourier.rademacherMeasure : MeasureTheory.Measure ℝ

instance BooleanFourier.rademacherMeasure_isFiniteMeasure : MeasureTheory.IsFiniteMeasure rademacherMeasure

instance BooleanFourier.rademacherMeasure_sigmaFinite : MeasureTheory.SigmaFinite rademacherMeasure

noncomputable def BooleanFourier.hybridMeasure (n k : ℕ) : MeasureTheory.Measure (Fin n → ℝ)

theorem BooleanFourier.hybridMeasure_zero (n : ℕ) : hybridMeasure n 0 = MeasureTheory.Measure.pi fun (x : Fin n) => rademacherMeasure

theorem BooleanFourier.hybridMeasure_n (n : ℕ) : hybridMeasure n n = GaussianHypercontractivity.stdGaussianMeasure n

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

theorem BooleanFourier.hybridExpectation_n {n : ℕ} (f : (Fin n → Bool) → ℝ) (Ψ : ℝ → ℝ) : hybridExpectation f Ψ n = gaussianExpectation f Ψ

noncomputable def BooleanFourier.boolToRealVec {n : ℕ} (b : Fin n → Bool) : Fin n → ℝ

theorem BooleanFourier.pi_rademacher_eq_sum_dirac (n : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin n) => rademacherMeasure) = 2⁻¹ ^ n • ∑ b : Fin n → Bool, MeasureTheory.Measure.dirac (boolToRealVec b)

theorem BooleanFourier.integral_pi_rademacher {n : ℕ} (g : (Fin n → ℝ) → ℝ) : (∫ (z : Fin n → ℝ), g z ∂MeasureTheory.Measure.pi fun (x : Fin n) => rademacherMeasure) = 1 / 2 ^ n * ∑ b : Fin n → Bool, g (boolToRealVec b)

theorem BooleanFourier.hybridExpectation_zero {n : ℕ} (f : (Fin n → Bool) → ℝ) (Ψ : ℝ → ℝ) : hybridExpectation f Ψ 0 = booleanExpectation f Ψ

theorem BooleanFourier.lindeberg_telescoping {n : ℕ} (f : (Fin n → Bool) → ℝ) (Ψ : ℝ → ℝ) : booleanExpectation f Ψ - gaussianExpectation f Ψ = ∑ k : Fin n, (hybridExpectation f Ψ ↑k - hybridExpectation f Ψ (↑k + 1))