Explicit polynomials and normalized complex Gaussian coordinates.

noncomputable def GaussianMomentsCounterexamples.naturalP3 : MvPolynomial (Fin 3) ℂ

Natural complex coordinates are ordered W, Z, T.

Equations

• GaussianMomentsCounterexamples.naturalP3 = (1 + MvPolynomial.X 1) * (MvPolynomial.X 0 - MvPolynomial.C (1 / 2) * (2 + MvPolynomial.X 1) * MvPolynomial.X 2 ^ 2)

noncomputable def GaussianMomentsCounterexamples.naturalP4 : MvPolynomial (Fin 4) ℂ

Natural complex coordinates are ordered W₁, Z₁, W₂, Z₂.

Equations

• GaussianMomentsCounterexamples.naturalP4 = (1 + MvPolynomial.X 3) * (MvPolynomial.X 0 * (1 - MvPolynomial.X 1) + MvPolynomial.X 2)

theorem GaussianMomentsCounterexamples.naturalP3_expansion : naturalP3 = MvPolynomial.X 0 + MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.X 2 ^ 2 - MvPolynomial.C (3 / 2) * MvPolynomial.X 1 * MvPolynomial.X 2 ^ 2 - MvPolynomial.C (1 / 2) * MvPolynomial.X 1 ^ 2 * MvPolynomial.X 2 ^ 2

theorem GaussianMomentsCounterexamples.naturalP4_expansion : naturalP4 = MvPolynomial.X 0 - MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.X 2 + MvPolynomial.X 0 * MvPolynomial.X 3 - MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 3 + MvPolynomial.X 2 * MvPolynomial.X 3

noncomputable def GaussianMomentsCounterexamples.exp3 (a b c : ℕ) : Fin 3 →₀ ℕ

Exponent vector for a monomial in three natural coordinates.

Equations

• GaussianMomentsCounterexamples.exp3 a b c = Finsupp.single 0 a + Finsupp.single 1 b + Finsupp.single 2 c

@[simp]

theorem GaussianMomentsCounterexamples.exp3_inj (a b c d e f : ℕ) : exp3 a b c = exp3 d e f ↔ a = d ∧ b = e ∧ c = f

theorem GaussianMomentsCounterexamples.naturalP3_monomials : naturalP3 = (MvPolynomial.monomial (exp3 1 0 0)) 1 + (MvPolynomial.monomial (exp3 1 1 0)) 1 + (MvPolynomial.monomial (exp3 0 0 2)) (-1) + (MvPolynomial.monomial (exp3 0 1 2)) (-(3 / 2)) + (MvPolynomial.monomial (exp3 0 2 2)) (-(1 / 2))

theorem GaussianMomentsCounterexamples.naturalP3_support : naturalP3.support = {exp3 1 0 0, exp3 1 1 0, exp3 0 0 2, exp3 0 1 2, exp3 0 2 2}

theorem GaussianMomentsCounterexamples.naturalP3_support_card : naturalP3.support.card = 5

theorem GaussianMomentsCounterexamples.naturalP3_totalDegree : naturalP3.totalDegree = 4

noncomputable def GaussianMomentsCounterexamples.exp4 (a b c d : ℕ) : Fin 4 →₀ ℕ

Exponent vector for a monomial in four natural coordinates.

Equations

• GaussianMomentsCounterexamples.exp4 a b c d = Finsupp.single 0 a + Finsupp.single 1 b + Finsupp.single 2 c + Finsupp.single 3 d

@[simp]

theorem GaussianMomentsCounterexamples.exp4_inj (a b c d e f g h : ℕ) : exp4 a b c d = exp4 e f g h ↔ a = e ∧ b = f ∧ c = g ∧ d = h

theorem GaussianMomentsCounterexamples.naturalP4_monomials : naturalP4 = (MvPolynomial.monomial (exp4 1 0 0 0)) 1 + (MvPolynomial.monomial (exp4 1 1 0 0)) (-1) + (MvPolynomial.monomial (exp4 0 0 1 0)) 1 + (MvPolynomial.monomial (exp4 1 0 0 1)) 1 + (MvPolynomial.monomial (exp4 1 1 0 1)) (-1) + (MvPolynomial.monomial (exp4 0 0 1 1)) 1

theorem GaussianMomentsCounterexamples.naturalP4_support : naturalP4.support = {exp4 1 0 0 0, exp4 1 1 0 0, exp4 0 0 1 0, exp4 1 0 0 1, exp4 1 1 0 1, exp4 0 0 1 1}

theorem GaussianMomentsCounterexamples.naturalP4_support_card : naturalP4.support.card = 6

theorem GaussianMomentsCounterexamples.naturalP4_totalDegree : naturalP4.totalDegree = 3

theorem GaussianMomentsCounterexamples.naturalP3_ne_zero : naturalP3 ≠ 0

theorem GaussianMomentsCounterexamples.naturalP4_ne_zero : naturalP4 ≠ 0

noncomputable def GaussianMomentsCounterexamples.normalization : ℂ

The normalization used in the manuscript.

Equations

• GaussianMomentsCounterexamples.normalization = (↑√2)⁻¹

theorem GaussianMomentsCounterexamples.normalization_sq : normalization ^ 2 = 1 / 2

noncomputable def GaussianMomentsCounterexamples.normalizedZ {n : ℕ} (i j : Fin n) : MvPolynomial (Fin n) ℂ

The normalized complex coordinate (Xᵢ + iXⱼ)/√2.

Equations

• GaussianMomentsCounterexamples.normalizedZ i j = MvPolynomial.C GaussianMomentsCounterexamples.normalization * (MvPolynomial.X i + MvPolynomial.C Complex.I * MvPolynomial.X j)

noncomputable def GaussianMomentsCounterexamples.normalizedW {n : ℕ} (i j : Fin n) : MvPolynomial (Fin n) ℂ

The conjugate normalized coordinate (Xᵢ - iXⱼ)/√2.

Equations

• GaussianMomentsCounterexamples.normalizedW i j = MvPolynomial.C GaussianMomentsCounterexamples.normalization * (MvPolynomial.X i - MvPolynomial.C Complex.I * MvPolynomial.X j)

theorem GaussianMomentsCounterexamples.recoverX {n : ℕ} (i j : Fin n) : MvPolynomial.C normalization * (normalizedW i j + normalizedZ i j) = MvPolynomial.X i

theorem GaussianMomentsCounterexamples.recoverY {n : ℕ} (i j : Fin n) : MvPolynomial.C (Complex.I * normalization) * (normalizedW i j - normalizedZ i j) = MvPolynomial.X j

theorem GaussianMomentsCounterexamples.recombineW {n : ℕ} (a b : MvPolynomial (Fin n) ℂ) : MvPolynomial.C normalization * (MvPolynomial.C normalization * (a + b) - MvPolynomial.C Complex.I * (MvPolynomial.C (Complex.I * normalization) * (a - b))) = a

theorem GaussianMomentsCounterexamples.recombineZ {n : ℕ} (a b : MvPolynomial (Fin n) ℂ) : MvPolynomial.C normalization * (MvPolynomial.C normalization * (a + b) + MvPolynomial.C Complex.I * (MvPolynomial.C (Complex.I * normalization) * (a - b))) = b

noncomputable def GaussianMomentsCounterexamples.normalizedSub3 : MvPolynomial (Fin 3) ℂ →ₐ[ℂ] MvPolynomial (Fin 3) ℂ

Substitution from natural complex coordinates into the real-coordinate polynomial ring.

Equations

• GaussianMomentsCounterexamples.normalizedSub3 = MvPolynomial.aeval ![GaussianMomentsCounterexamples.normalizedW 0 1, GaussianMomentsCounterexamples.normalizedZ 0 1, MvPolynomial.X 2]

noncomputable def GaussianMomentsCounterexamples.normalizedSub4 : MvPolynomial (Fin 4) ℂ →ₐ[ℂ] MvPolynomial (Fin 4) ℂ

Substitute two normalized conjugate pairs into four real coordinates.

Equations

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

noncomputable def GaussianMomentsCounterexamples.inverseSub3 : MvPolynomial (Fin 3) ℂ →ₐ[ℂ] MvPolynomial (Fin 3) ℂ

Recover three original coordinates from the natural complex coordinates.

Equations

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

noncomputable def GaussianMomentsCounterexamples.inverseSub4 : MvPolynomial (Fin 4) ℂ →ₐ[ℂ] MvPolynomial (Fin 4) ℂ

Recover four original coordinates from two natural conjugate pairs.

Equations

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

noncomputable def GaussianMomentsCounterexamples.P3 : MvPolynomial (Fin 3) ℂ

The explicit three-variable counterexample, on the original real coordinates.

Equations

• GaussianMomentsCounterexamples.P3 = GaussianMomentsCounterexamples.normalizedSub3 GaussianMomentsCounterexamples.naturalP3

noncomputable def GaussianMomentsCounterexamples.Q3 : MvPolynomial (Fin 3) ℂ

The linear multiplier witnessing nonvanishing mixed moments in three dimensions.

Equations

• GaussianMomentsCounterexamples.Q3 = GaussianMomentsCounterexamples.normalizedZ 0 1

noncomputable def GaussianMomentsCounterexamples.P4 : MvPolynomial (Fin 4) ℂ

The explicit four-variable counterexample, on the original real coordinates.

Equations

• GaussianMomentsCounterexamples.P4 = GaussianMomentsCounterexamples.normalizedSub4 GaussianMomentsCounterexamples.naturalP4

noncomputable def GaussianMomentsCounterexamples.Q4 : MvPolynomial (Fin 4) ℂ

The linear multiplier witnessing nonvanishing mixed moments in four dimensions.

Equations

• GaussianMomentsCounterexamples.Q4 = GaussianMomentsCounterexamples.normalizedZ 2 3