Exact radial and two-weight moment formulas in dimension two. No one-variable Factorial Conjecture or two-dimensional exclusion theorem is assumed.

def GaussianMomentsCounterexamples.factorialFunctional : Polynomial ℂ →ₗ[ℂ] ℂ

The linear factorial functional on the polynomial ring in U.

Equations

• GaussianMomentsCounterexamples.factorialFunctional = Polynomial.lsum fun (j : ℕ) => (LinearMap.ringLmapEquivSelf ℂ ℂ ℂ).symm ↑j.factorial

@[simp]

theorem GaussianMomentsCounterexamples.factorialFunctional_monomial (j : ℕ) (c : ℂ) : factorialFunctional ((Polynomial.monomial j) c) = c * ↑j.factorial

@[simp]

theorem GaussianMomentsCounterexamples.factorialFunctional_X_pow (j : ℕ) : factorialFunctional (Polynomial.X ^ j) = ↑j.factorial

noncomputable def GaussianMomentsCounterexamples.radialLift : Polynomial ℂ →+* MvPolynomial (Fin 2) ℂ

Substitute U=WZ in a univariate polynomial.

Equations

• GaussianMomentsCounterexamples.radialLift = Polynomial.eval₂RingHom MvPolynomial.C (MvPolynomial.X 0 * MvPolynomial.X 1)

@[simp]

theorem GaussianMomentsCounterexamples.radialLift_monomial (j : ℕ) (c : ℂ) : radialLift ((Polynomial.monomial j) c) = MvPolynomial.C c * (MvPolynomial.X 0 * MvPolynomial.X 1) ^ j

@[simp]

theorem GaussianMomentsCounterexamples.radialLift_X : radialLift Polynomial.X = MvPolynomial.X 0 * MvPolynomial.X 1

theorem GaussianMomentsCounterexamples.pairExpectation_radial (A : Polynomial ℂ) : pairExpectation (radialLift A) = factorialFunctional A

Gaussian expectation on C[U] is exactly the factorial functional.

theorem GaussianMomentsCounterexamples.pairExpectation_eval_radial (A : Polynomial ℂ) : pairExpectation (Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X 0 * MvPolynomial.X 1) A) = factorialFunctional A

Explicit eval₂ form of the factorial correspondence.

theorem GaussianMomentsCounterexamples.pairExpectation_unbalanced_radial (a b : ℕ) (hab : a ≠ b) (A : Polynomial ℂ) : pairExpectation (MvPolynomial.X 0 ^ a * MvPolynomial.X 1 ^ b * radialLift A) = 0

theorem GaussianMomentsCounterexamples.pairExpectation_balanced_radial (a : ℕ) (A : Polynomial ℂ) : pairExpectation (MvPolynomial.X 0 ^ a * MvPolynomial.X 1 ^ a * radialLift A) = factorialFunctional (Polynomial.X ^ a * A)

noncomputable def GaussianMomentsCounterexamples.twoWeightPolynomial (A B : Polynomial ℂ) : MvPolynomial (Fin 2) ℂ

A general two-weight polynomial in the manuscript's natural coordinates.

Equations

• GaussianMomentsCounterexamples.twoWeightPolynomial A B = MvPolynomial.X 1 * GaussianMomentsCounterexamples.radialLift A + MvPolynomial.X 0 * GaussianMomentsCounterexamples.radialLift B

theorem GaussianMomentsCounterexamples.pairExpectation_C_mul (c : ℂ) (P : MvPolynomial (Fin 2) ℂ) : pairExpectation (MvPolynomial.C c * P) = c * pairExpectation P

theorem GaussianMomentsCounterexamples.twoWeight_moment_expansion (A B : Polynomial ℂ) (m : ℕ) : pairExpectation (twoWeightPolynomial A B ^ m) = ∑ a ∈ Finset.range (m + 1), ↑(m.choose a) * pairExpectation (MvPolynomial.X 0 ^ (m - a) * MvPolynomial.X 1 ^ a * radialLift (A ^ a * B ^ (m - a)))

theorem GaussianMomentsCounterexamples.twoWeight_odd_moment (A B : Polynomial ℂ) (r : ℕ) : pairExpectation (twoWeightPolynomial A B ^ (2 * r + 1)) = 0

Every odd moment of ZA(U)+WB(U) vanishes, for arbitrary complex A and B.

theorem GaussianMomentsCounterexamples.twoWeight_even_moment (A B : Polynomial ℂ) (r : ℕ) : pairExpectation (twoWeightPolynomial A B ^ (2 * r)) = ↑((2 * r).choose r) * factorialFunctional ((Polynomial.X * A * B) ^ r)

The exact even-moment identity displayed in Section 7.

theorem GaussianMomentsCounterexamples.twoWeight_actual_odd_moment (A B : Polynomial ℂ) (r : ℕ) : expectation (pairSub (twoWeightPolynomial A B) ^ (2 * r + 1)) = 0

The odd-moment identity explicitly on the original real Gaussian coordinate space.

theorem GaussianMomentsCounterexamples.twoWeight_actual_even_moment (A B : Polynomial ℂ) (r : ℕ) : expectation (pairSub (twoWeightPolynomial A B) ^ (2 * r)) = ↑((2 * r).choose r) * factorialFunctional ((Polynomial.X * A * B) ^ r)

The even-moment identity explicitly on the original real Gaussian coordinate space.