All-order Gaussian moments from integration by parts.

theorem GaussianMomentsCounterexamples.integrable_pow_mul_density (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n * ProbabilityTheory.gaussianPDFReal 0 1 x) MeasureTheory.volume

theorem GaussianMomentsCounterexamples.hasDerivAt_standardGaussianDensity (x : ℝ) : HasDerivAt (ProbabilityTheory.gaussianPDFReal 0 1) (-x * ProbabilityTheory.gaussianPDFReal 0 1 x) x

theorem GaussianMomentsCounterexamples.real_gaussian_moment_recurrence (n : ℕ) : ∫ (x : ℝ), x ^ (n + 2) ∂ProbabilityTheory.gaussianReal 0 1 = (↑n + 1) * ∫ (x : ℝ), x ^ n ∂ProbabilityTheory.gaussianReal 0 1

Gaussian integration by parts gives the all-order real moment recurrence.

theorem GaussianMomentsCounterexamples.real_gaussian_moment_zero : ∫ (x : ℝ), x ^ 0 ∂ProbabilityTheory.gaussianReal 0 1 = 1

theorem GaussianMomentsCounterexamples.real_gaussian_moment_one : ∫ (x : ℝ), x ^ 1 ∂ProbabilityTheory.gaussianReal 0 1 = 0

theorem GaussianMomentsCounterexamples.real_gaussian_odd_moment (n : ℕ) : ∫ (x : ℝ), x ^ (2 * n + 1) ∂ProbabilityTheory.gaussianReal 0 1 = 0

theorem GaussianMomentsCounterexamples.complex_gaussian_moment_eq_real (n : ℕ) : ∫ (x : ℝ), ↑x ^ n ∂ProbabilityTheory.gaussianReal 0 1 = ↑(∫ (x : ℝ), x ^ n ∂ProbabilityTheory.gaussianReal 0 1)

theorem GaussianMomentsCounterexamples.complex_gaussian_moment_succ (k : ℕ) : ∫ (x : ℝ), ↑x ^ (k + 1) ∂ProbabilityTheory.gaussianReal 0 1 = ↑k * ∫ (x : ℝ), ↑x ^ (k - 1) ∂ProbabilityTheory.gaussianReal 0 1

The recurrence in the form used for polynomial Gaussian integration by parts.

theorem GaussianMomentsCounterexamples.complex_gaussian_odd_moment (n : ℕ) : ∫ (x : ℝ), ↑x ^ (2 * n + 1) ∂ProbabilityTheory.gaussianReal 0 1 = 0

theorem GaussianMomentsCounterexamples.real_gaussian_even_moment (n : ℕ) : ∫ (x : ℝ), x ^ (2 * n) ∂ProbabilityTheory.gaussianReal 0 1 = ↑(2 * n).factorial / (2 ^ n * ↑n.factorial)

The even moments of the standard Gaussian, valid at every order.

theorem GaussianMomentsCounterexamples.complex_gaussian_even_moment (n : ℕ) : ∫ (x : ℝ), ↑x ^ (2 * n) ∂ProbabilityTheory.gaussianReal 0 1 = ↑(2 * n).factorial / (2 ^ n * ↑n.factorial)

theorem GaussianMomentsCounterexamples.integral_complex_pow_succ (k : ℕ) : ∫ (x : ℝ), ↑x ^ (k + 1) ∂ProbabilityTheory.gaussianReal 0 1 = ↑k * ∫ (x : ℝ), ↑x ^ (k - 1) ∂ProbabilityTheory.gaussianReal 0 1

Alias of GaussianMomentsCounterexamples.complex_gaussian_moment_succ.

---

The recurrence in the form used for polynomial Gaussian integration by parts.