Invertible coordinate substitutions, polynomial degree and explicit formulas.

theorem GaussianMomentsCounterexamples.inverseSub3_normalizedSub3 : inverseSub3.comp normalizedSub3 = AlgHom.id ℂ (MvPolynomial (Fin 3) ℂ)

theorem GaussianMomentsCounterexamples.inverseSub4_normalizedSub4 : inverseSub4.comp normalizedSub4 = AlgHom.id ℂ (MvPolynomial (Fin 4) ℂ)

theorem GaussianMomentsCounterexamples.normalizedSub3_inverseSub3 : normalizedSub3.comp inverseSub3 = AlgHom.id ℂ (MvPolynomial (Fin 3) ℂ)

theorem GaussianMomentsCounterexamples.normalizedSub4_inverseSub4 : normalizedSub4.comp inverseSub4 = AlgHom.id ℂ (MvPolynomial (Fin 4) ℂ)

noncomputable def GaussianMomentsCounterexamples.coordinateEquiv3 : MvPolynomial (Fin 3) ℂ ≃ₐ[ℂ] MvPolynomial (Fin 3) ℂ

The normalized coordinates form an invertible complex polynomial coordinate change.

Equations

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

noncomputable def GaussianMomentsCounterexamples.coordinateEquiv4 : MvPolynomial (Fin 4) ℂ ≃ₐ[ℂ] MvPolynomial (Fin 4) ℂ

The invertible polynomial coordinate change for two normalized conjugate pairs.

Equations

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

theorem GaussianMomentsCounterexamples.P3_ne_zero : P3 ≠ 0

theorem GaussianMomentsCounterexamples.P4_ne_zero : P4 ≠ 0

theorem GaussianMomentsCounterexamples.P3_formula : P3 = (1 + normalizedZ 0 1) * (normalizedW 0 1 - MvPolynomial.C (1 / 2) * (2 + normalizedZ 0 1) * MvPolynomial.X 2 ^ 2)

theorem GaussianMomentsCounterexamples.P4_formula : P4 = (1 + normalizedZ 2 3) * (normalizedW 0 1 * (1 - normalizedZ 0 1) + normalizedW 2 3)

theorem GaussianMomentsCounterexamples.P3_expansion : P3 = normalizedW 0 1 + normalizedW 0 1 * normalizedZ 0 1 - MvPolynomial.X 2 ^ 2 - MvPolynomial.C (3 / 2) * normalizedZ 0 1 * MvPolynomial.X 2 ^ 2 - MvPolynomial.C (1 / 2) * normalizedZ 0 1 ^ 2 * MvPolynomial.X 2 ^ 2

theorem GaussianMomentsCounterexamples.P4_expansion : P4 = normalizedW 0 1 - normalizedW 0 1 * normalizedZ 0 1 + normalizedW 2 3 + normalizedW 0 1 * normalizedZ 2 3 - normalizedW 0 1 * normalizedZ 0 1 * normalizedZ 2 3 + normalizedW 2 3 * normalizedZ 2 3

@[simp]

theorem GaussianMomentsCounterexamples.eval_normalizedZ {n : ℕ} (i j : Fin n) (x : Fin n → ℂ) : (MvPolynomial.eval x) (normalizedZ i j) = (x i + Complex.I * x j) / ↑√2

@[simp]

theorem GaussianMomentsCounterexamples.eval_normalizedW {n : ℕ} (i j : Fin n) (x : Fin n → ℂ) : (MvPolynomial.eval x) (normalizedW i j) = (x i - Complex.I * x j) / ↑√2

theorem GaussianMomentsCounterexamples.eval_normalizedW_conj {n : ℕ} (i j : Fin n) (x : Fin n → ℝ) : (MvPolynomial.eval fun (k : Fin n) => ↑(x k)) (normalizedW i j) = star ((MvPolynomial.eval fun (k : Fin n) => ↑(x k)) (normalizedZ i j))

theorem GaussianMomentsCounterexamples.totalDegree_aeval_linear {n k : ℕ} (f : Fin n → MvPolynomial (Fin k) ℂ) (hf : ∀ (i : Fin n), (f i).totalDegree ≤ 1) (P : MvPolynomial (Fin n) ℂ) : ((MvPolynomial.aeval f) P).totalDegree ≤ P.totalDegree

Linear substitutions do not increase total degree.

theorem GaussianMomentsCounterexamples.totalDegree_normalizedZ {n : ℕ} (i j : Fin n) : (normalizedZ i j).totalDegree ≤ 1

theorem GaussianMomentsCounterexamples.totalDegree_normalizedW {n : ℕ} (i j : Fin n) : (normalizedW i j).totalDegree ≤ 1

theorem GaussianMomentsCounterexamples.totalDegree_linear_pair {n : ℕ} (c : ℂ) (i j : Fin n) : (MvPolynomial.C c * (MvPolynomial.X i + MvPolynomial.X j)).totalDegree ≤ 1

theorem GaussianMomentsCounterexamples.totalDegree_linear_pair_sub {n : ℕ} (c : ℂ) (i j : Fin n) : (MvPolynomial.C c * (MvPolynomial.X i - MvPolynomial.X j)).totalDegree ≤ 1

theorem GaussianMomentsCounterexamples.totalDegree_normalizedSub3 (P : MvPolynomial (Fin 3) ℂ) : (normalizedSub3 P).totalDegree = P.totalDegree

theorem GaussianMomentsCounterexamples.totalDegree_normalizedSub4 (P : MvPolynomial (Fin 4) ℂ) : (normalizedSub4 P).totalDegree = P.totalDegree

theorem GaussianMomentsCounterexamples.P3_totalDegree : P3.totalDegree = 4

theorem GaussianMomentsCounterexamples.P4_totalDegree : P4.totalDegree = 3