Agreement of the natural-coordinate algebraic moment functionals with actual integrals.

theorem GaussianMomentsCounterexamples.normalizedSub3_monomial (d : Fin 3 →₀ ℕ) (c : ℂ) : normalizedSub3 ((MvPolynomial.monomial d) c) = MvPolynomial.C c * (normalizedW 0 1 ^ d 0 * normalizedZ 0 1 ^ d 1 * MvPolynomial.X 2 ^ d 2)

theorem GaussianMomentsCounterexamples.normalizedSub4_monomial (d : Fin 4 →₀ ℕ) (c : ℂ) : normalizedSub4 ((MvPolynomial.monomial d) c) = MvPolynomial.C c * (normalizedW 0 1 ^ d 0 * normalizedZ 0 1 ^ d 1 * (normalizedW 2 3 ^ d 2 * normalizedZ 2 3 ^ d 3))

theorem GaussianMomentsCounterexamples.expectation_normalizedSub3 (P : MvPolynomial (Fin 3) ℂ) : expectation (normalizedSub3 P) = naturalMoment3 P

Full agreement, for every polynomial, of the three-coordinate functional and integration.

theorem GaussianMomentsCounterexamples.expectation_normalizedSub4 (P : MvPolynomial (Fin 4) ℂ) : expectation (normalizedSub4 P) = naturalMoment4 P

Full agreement, for every polynomial, of the four-coordinate functional and integration.