A real-coefficient polynomial whose Gaussian second moment vanishes is zero.

instance GaussianMomentsCounterexamples.standardGaussian_isOpenPosMeasure : (ProbabilityTheory.gaussianReal 0 1).IsOpenPosMeasure

instance GaussianMomentsCounterexamples.gaussianMeasure_isOpenPosMeasure (n : ℕ) : (gaussianMeasure n).IsOpenPosMeasure

theorem GaussianMomentsCounterexamples.realEval_map_real {n : ℕ} (P : MvPolynomial (Fin n) ℝ) (x : Fin n → ℝ) : realEval ((MvPolynomial.map Complex.ofRealHom) P) x = ↑((MvPolynomial.eval x) P)

theorem GaussianMomentsCounterexamples.integrable_real_polynomial {n : ℕ} (P : MvPolynomial (Fin n) ℝ) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => (MvPolynomial.eval x) P) (gaussianMeasure n)

theorem GaussianMomentsCounterexamples.real_polynomial_eq_zero_of_second_moment {n : ℕ} (P : MvPolynomial (Fin n) ℝ) (h : ∫ (x : Fin n → ℝ), (MvPolynomial.eval x) P ^ 2 ∂gaussianMeasure n = 0) : P = 0

Nonnegative Gaussian second moment detects every nonzero real polynomial.

theorem GaussianMomentsCounterexamples.expectation_map_real {n : ℕ} (P : MvPolynomial (Fin n) ℝ) : expectation ((MvPolynomial.map Complex.ofRealHom) P) = ↑(∫ (x : Fin n → ℝ), (MvPolynomial.eval x) P ∂gaussianMeasure n)

Casting real coefficients commutes with the genuine Gaussian expectation.

theorem GaussianMomentsCounterexamples.real_polynomial_eq_zero_of_complex_second_moment {n : ℕ} (P : MvPolynomial (Fin n) ℝ) (h : expectation ((MvPolynomial.map Complex.ofRealHom) P ^ 2) = 0) : P = 0

The second-moment obstruction in the manuscript's complex-valued expectation interface.

theorem GaussianMomentsCounterexamples.real_polynomial_eq_zero_of_all_moments {n : ℕ} (P : MvPolynomial (Fin n) ℝ) (h : ∀ (m : ℕ), 1 ≤ m → expectation ((MvPolynomial.map Complex.ofRealHom) P ^ m) = 0) : P = 0

Consequently a real-coefficient polynomial with all positive Gaussian moments zero is zero.