Factorial and double-factorial expressions for Gaussian moments.

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

The double-factorial version of every even Gaussian moment. At k = 0, truncated natural subtraction gives 0!! = 1, representing the conventional value (-1)!! = 1 in the manuscript.

theorem GaussianMomentsCounterexamples.gaussian_doubleFactorial_eq_factorial (k : ℕ) : ↑(2 * k - 1).doubleFactorial = ↑(2 * k).factorial / (2 ^ k * ↑k.factorial)

The two closed forms of the real Gaussian moment agree, including order zero.

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