Marginal compatibility for any injective selection of real Gaussian coordinates.

theorem GaussianMomentsCounterexamples.continuous_realEval {n : ℕ} (P : MvPolynomial (Fin n) ℂ) : Continuous (realEval P)

theorem GaussianMomentsCounterexamples.gaussianMeasure_marginal {k n : ℕ} (e : Fin k → Fin n) (he : Function.Injective e) : MeasureTheory.MeasurePreserving (fun (x : Fin n → ℝ) (i : Fin k) => x (e i)) (gaussianMeasure n) (gaussianMeasure k)

Any injective coordinate selection preserves the standard Gaussian law.

theorem GaussianMomentsCounterexamples.expectation_rename {k n : ℕ} (e : Fin k → Fin n) (he : Function.Injective e) (P : MvPolynomial (Fin k) ℂ) : expectation ((MvPolynomial.rename e) P) = expectation P

Renaming into distinct Gaussian coordinates preserves every polynomial expectation.

theorem GaussianMomentsCounterexamples.not_GMC_of_le {k n : ℕ} (hkn : k ≤ n) (hk : ¬GMC k) : ¬GMC n

Failure in a smaller dimension propagates to every larger dimension.