Documentation

LeanPool.GaussianMomentsCounterexamples.Counterexamples

The unconditional Gaussian counterexamples and genuine failure of GMC in all n ≥ 3.

theorem GaussianMomentsCounterexamples.normalizedSub3_polyAt (A : Polynomial ℂ) :

normalizedSub3 ((polyAt 1) A) = Polynomial.eval₂ MvPolynomial.C Q3 A

theorem GaussianMomentsCounterexamples.normalizedSub4_polyAt (A : Polynomial ℂ) :

normalizedSub4 ((polyAt 3) A) = Polynomial.eval₂ MvPolynomial.C Q4 A

theorem GaussianMomentsCounterexamples.master_three (A : Polynomial ℂ) (m : ℕ) (hm : 1 ≤ m) :

expectation (Polynomial.eval₂ MvPolynomial.C Q3 A * P3 ^ m) = ↑m.factorial * (A * (1 + Polynomial.X) ^ (m - 1)).coeff m

Theorem 5.1, full arbitrary-polynomial coefficient identity with actual Gaussian expectations.

theorem GaussianMomentsCounterexamples.master_four (A : Polynomial ℂ) (m : ℕ) (hm : 1 ≤ m) :

expectation (Polynomial.eval₂ MvPolynomial.C Q4 A * P4 ^ m) = ↑m.factorial * (A * (1 + Polynomial.X) ^ (m - 1)).coeff m

Proposition 4.1, full arbitrary-polynomial coefficient identity with actual Gaussian expectations.

theorem GaussianMomentsCounterexamples.P3_moment (m : ℕ) (hm : 1 ≤ m) :

expectation (P3 ^ m) = 0

theorem GaussianMomentsCounterexamples.Q3_P3_moment (m : ℕ) (hm : 1 ≤ m) :

expectation (Q3 * P3 ^ m) = ↑m.factorial

theorem GaussianMomentsCounterexamples.P4_moment (m : ℕ) (hm : 1 ≤ m) :

expectation (P4 ^ m) = 0

theorem GaussianMomentsCounterexamples.Q4_P4_moment (m : ℕ) (hm : 1 ≤ m) :

expectation (Q4 * P4 ^ m) = ↑m.factorial

theorem GaussianMomentsCounterexamples.Q3_P3_moment_ne_zero (m : ℕ) (hm : 1 ≤ m) :

expectation (Q3 * P3 ^ m) ≠ 0

theorem GaussianMomentsCounterexamples.Q4_P4_moment_ne_zero (m : ℕ) (hm : 1 ≤ m) :

expectation (Q4 * P4 ^ m) ≠ 0

theorem GaussianMomentsCounterexamples.Q3_ne_zero :

theorem GaussianMomentsCounterexamples.Q4_ne_zero :

theorem GaussianMomentsCounterexamples.not_GMC_three :

Explicit witnesses violate the eventual-vanishing quantifier of GMC(3).

theorem GaussianMomentsCounterexamples.not_GMC_of_three_le (n : ℕ) (hn : 3 ≤ n) :

Corollary 5.2, including all higher-dimensional Gaussian marginal compatibility.

theorem GaussianMomentsCounterexamples.not_GMC_four :

A direct four-variable witness, separately from extending the three-variable example.

theorem GaussianMomentsCounterexamples.not_GMC_158 :

This is dimension extension, not a formalization of the Jacobian-reduction route.