Elementary weight arguments in dimension two. No claim resolving GMC(2).

noncomputable def GaussianMomentsCounterexamples.pairSub : MvPolynomial (Fin 2) ℂ →ₐ[ℂ] MvPolynomial (Fin 2) ℂ

Natural coordinates [W,Z] for one normalized complex Gaussian pair.

Equations

• GaussianMomentsCounterexamples.pairSub = MvPolynomial.aeval ![GaussianMomentsCounterexamples.normalizedW 0 1, GaussianMomentsCounterexamples.normalizedZ 0 1]

noncomputable def GaussianMomentsCounterexamples.pairExpectation : MvPolynomial (Fin 2) ℂ →ₗ[ℂ] ℂ

Actual Gaussian expectation expressed in the two natural complex coordinates.

Equations

• GaussianMomentsCounterexamples.pairExpectation = GaussianMomentsCounterexamples.expectationLinear 2 ∘ₗ GaussianMomentsCounterexamples.pairSub.toLinearMap

@[simp]

theorem GaussianMomentsCounterexamples.pairExpectation_monomial (d : Fin 2 →₀ ℕ) (c : ℂ) : pairExpectation ((MvPolynomial.monomial d) c) = c * pairMoment (d 0) (d 1)

def GaussianMomentsCounterexamples.signedWeight (sign : ℤ) (d : Fin 2 →₀ ℕ) : ℤ

Z has weight +1 and W has weight -1; sign reverses the chosen direction.

Equations

• GaussianMomentsCounterexamples.signedWeight sign d = sign * (↑(d 1) - ↑(d 0))

theorem GaussianMomentsCounterexamples.signedWeight_add (sign : ℤ) (d e : Fin 2 →₀ ℕ) : signedWeight sign (d + e) = signedWeight sign d + signedWeight sign e

theorem GaussianMomentsCounterexamples.pairExpectation_eq_zero_of_no_balanced (P : MvPolynomial (Fin 2) ℂ) (hP : ∀ d ∈ P.support, d 0 ≠ d 1) : pairExpectation P = 0

Expectation kills any polynomial with no weight-zero monomials.

theorem GaussianMomentsCounterexamples.pairExpectation_eq_zero_of_weight (P : MvPolynomial (Fin 2) ℂ) (w : ℤ) (hw : w ≠ 0) (hP : ∀ d ∈ P.support, signedWeight 1 d = w) : pairExpectation P = 0

Every polynomial supported in one nonzero weight has zero expectation.

def GaussianMomentsCounterexamples.WeightLowerBound (sign : ℤ) (P : MvPolynomial (Fin 2) ℂ) (k : ℤ) : Prop

Every supported monomial has signed weight at least the given bound.

Equations

• GaussianMomentsCounterexamples.WeightLowerBound sign P k = ∀ d ∈ P.support, k ≤ GaussianMomentsCounterexamples.signedWeight sign d

theorem GaussianMomentsCounterexamples.weightLowerBound_mul (sign : ℤ) (P Q : MvPolynomial (Fin 2) ℂ) (a b : ℤ) (hP : WeightLowerBound sign P a) (hQ : WeightLowerBound sign Q b) : WeightLowerBound sign (P * Q) (a + b)

theorem GaussianMomentsCounterexamples.weightLowerBound_pow (sign : ℤ) (P : MvPolynomial (Fin 2) ℂ) (hP : WeightLowerBound sign P 1) (m : ℕ) : WeightLowerBound sign (P ^ m) ↑m

theorem GaussianMomentsCounterexamples.one_sided_eventual_vanishing (sign : ℤ) (P : MvPolynomial (Fin 2) ℂ) (hP : WeightLowerBound sign P 1) (Q : MvPolynomial (Fin 2) ℂ) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → pairExpectation (Q * P ^ m) = 0

Strictly positive weights, or strictly negative weights by sign=-1, give eventual vanishing for every polynomial multiplier. All expectations here are actual Gaussian integrals.

noncomputable def GaussianMomentsCounterexamples.pairInverseSub : MvPolynomial (Fin 2) ℂ →ₐ[ℂ] MvPolynomial (Fin 2) ℂ

The inverse linear substitution ensures one-sided claims cover arbitrary multipliers in the original real-coordinate polynomial ring as well.

Equations

• One or more equations did not get rendered due to their size.

theorem GaussianMomentsCounterexamples.pairSub_pairInverseSub : pairSub.comp pairInverseSub = AlgHom.id ℂ (MvPolynomial (Fin 2) ℂ)

theorem GaussianMomentsCounterexamples.one_sided_eventual_vanishing_real (sign : ℤ) (P : MvPolynomial (Fin 2) ℂ) (hP : WeightLowerBound sign P 1) (Q : MvPolynomial (Fin 2) ℂ) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → expectation (Q * pairSub P ^ m) = 0

Original-coordinate multipliers also vanish eventually for a polynomial supported strictly on one side of the weight grading in complex coordinates.