theorem GaussianFourthMoment.hasDerivAt_exp_half_sq (t : ℝ) : HasDerivAt (fun (t : ℝ) => Real.exp (t ^ 2 / 2)) (t * Real.exp (t ^ 2 / 2)) t

theorem GaussianFourthMoment.hasDerivAt_d1 (t : ℝ) : HasDerivAt (fun (t : ℝ) => t * Real.exp (t ^ 2 / 2)) ((1 + t ^ 2) * Real.exp (t ^ 2 / 2)) t

theorem GaussianFourthMoment.hasDerivAt_d2 (t : ℝ) : HasDerivAt (fun (t : ℝ) => (1 + t ^ 2) * Real.exp (t ^ 2 / 2)) ((3 * t + t ^ 3) * Real.exp (t ^ 2 / 2)) t

theorem GaussianFourthMoment.hasDerivAt_d3 (t : ℝ) : HasDerivAt (fun (t : ℝ) => (3 * t + t ^ 3) * Real.exp (t ^ 2 / 2)) ((3 + 6 * t ^ 2 + t ^ 4) * Real.exp (t ^ 2 / 2)) t

theorem GaussianFourthMoment.deriv_four_exp_half_sq_zero : deriv (deriv (deriv (deriv fun (t : ℝ) => Real.exp (t ^ 2 / 2)))) 0 = 3

theorem GaussianFourthMoment.mgf_standard_gaussian : ProbabilityTheory.mgf id (ProbabilityTheory.gaussianReal 0 1) = fun (t : ℝ) => Real.exp (t ^ 2 / 2)

theorem GaussianFourthMoment.fourth_moment_standard_gaussian : ∫ (x : ℝ), x ^ 4 ∂ProbabilityTheory.gaussianReal 0 1 = 3

theorem GaussianFourthMoment.abs_mul_four_le_sum_pow_four (a b c d : ℝ) : |a * b * c * d| ≤ (a ^ 4 + b ^ 4 + c ^ 4 + d ^ 4) / 4

theorem GaussianFourthMoment.product_bound_equidistributed {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Fin 4 → Ω → ℝ) (hf_int : ∀ (i : Fin 4), MeasureTheory.Integrable (fun (ω : Ω) => f i ω ^ 4) μ) (hf_equi : ∀ (i : Fin 4), ∫ (ω : Ω), f i ω ^ 4 ∂μ = ∫ (ω : Ω), f 0 ω ^ 4 ∂μ) (hf_abs_int : MeasureTheory.Integrable (fun (ω : Ω) => |f 0 ω * f 1 ω * f 2 ω * f 3 ω|) μ) : ∫ (ω : Ω), |f 0 ω * f 1 ω * f 2 ω * f 3 ω| ∂μ ≤ ∫ (ω : Ω), f 0 ω ^ 4 ∂μ

theorem GaussianFourthMoment.gaussian_fourth_moment_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Fin 4 → Ω → ℝ) (hf_int : ∀ (i : Fin 4), MeasureTheory.Integrable (fun (ω : Ω) => f i ω ^ 4) μ) (hf_equi : ∀ (i : Fin 4), ∫ (ω : Ω), f i ω ^ 4 ∂μ = ∫ (ω : Ω), f 0 ω ^ 4 ∂μ) (hf_abs_int : MeasureTheory.Integrable (fun (ω : Ω) => |f 0 ω * f 1 ω * f 2 ω * f 3 ω|) μ) (hf_gaussian : ∫ (ω : Ω), f 0 ω ^ 4 ∂μ = ∫ (x : ℝ), x ^ 4 ∂ProbabilityTheory.gaussianReal 0 1) : ∫ (ω : Ω), |f 0 ω * f 1 ω * f 2 ω * f 3 ω| ∂μ ≤ 3