theorem BooleanFourier.gaussianReal_third_abs_moment_le_two : ∫ (t : ℝ), |t| ^ 3 ∂ProbabilityTheory.gaussianReal 0 1 ≤ 2

theorem BooleanFourier.rademacher_avg_taylor (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) (c a : ℝ) : |(Ψ (c + a) + Ψ (c - a)) / 2 - Ψ c - 1 / 2 * iteratedDeriv 2 Ψ c * a ^ 2| ≤ 1 / 6 * hΨ.thirdDerivBound * |a| ^ 3

theorem BooleanFourier.gaussian_integral_taylor (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) (c a : ℝ) : |∫ (t : ℝ), Ψ (c + a * t) ∂ProbabilityTheory.gaussianReal 0 1 - Ψ c - 1 / 2 * iteratedDeriv 2 Ψ c * a ^ 2| ≤ 1 / 6 * hΨ.thirdDerivBound * |a| ^ 3 * ∫ (t : ℝ), |t| ^ 3 ∂ProbabilityTheory.gaussianReal 0 1

theorem BooleanFourier.lindeberg_one_dim_comparison (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) (c a : ℝ) : |(Ψ (c + a) + Ψ (c - a)) / 2 - ∫ (t : ℝ), Ψ (c + a * t) ∂ProbabilityTheory.gaussianReal 0 1| ≤ 1 / 2 * hΨ.thirdDerivBound * |a| ^ 3