Gaussian coefficient contraction for arbitrary univariate polynomials.

theorem GaussianMomentsCounterexamples.expectation_coefficient_contraction {n : ℕ} {i j : Fin n} (hij : i ≠ j) (a : ℕ) (R : Polynomial ℂ) : expectation (normalizedW i j ^ a * Polynomial.eval₂ MvPolynomial.C (normalizedZ i j) R) = ↑a.factorial * R.coeff a

The coefficient-contraction identity with genuine integration on any canonical Gaussian space and any two distinct coordinates.