Algebraic Gaussian moment functionals and their coefficient identities.

def GaussianMomentsCounterexamples.pairMoment (a b : ℕ) : ℂ

The contraction of a normalized conjugate Gaussian pair.

Equations

• GaussianMomentsCounterexamples.pairMoment a b = if a = b then ↑a.factorial else 0

noncomputable def GaussianMomentsCounterexamples.naturalMoment3 : MvPolynomial (Fin 3) ℂ →ₗ[ℂ] ℂ

Linear extension from monomials of the three-coordinate Gaussian moments.

Equations

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

noncomputable def GaussianMomentsCounterexamples.naturalMoment4 : MvPolynomial (Fin 4) ℂ →ₗ[ℂ] ℂ

Linear extension from monomials for two independent normalized conjugate pairs.

Equations

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

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment3_monomial (d : Fin 3 →₀ ℕ) (c : ℂ) : naturalMoment3 ((MvPolynomial.monomial d) c) = c * (pairMoment (d 0) (d 1) * ∫ (t : ℝ), ↑t ^ d 2 ∂ProbabilityTheory.gaussianReal 0 1)

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment4_monomial (d : Fin 4 →₀ ℕ) (c : ℂ) : naturalMoment4 ((MvPolynomial.monomial d) c) = c * (pairMoment (d 0) (d 1) * pairMoment (d 2) (d 3))

noncomputable def GaussianMomentsCounterexamples.polyAt {n : ℕ} (i : Fin n) : Polynomial ℂ →+* MvPolynomial (Fin n) ℂ

Embed a univariate polynomial in one specified natural coordinate.

Equations

• GaussianMomentsCounterexamples.polyAt i = Polynomial.eval₂RingHom MvPolynomial.C (MvPolynomial.X i)

@[simp]

theorem GaussianMomentsCounterexamples.polyAt_monomial {n : ℕ} (i : Fin n) (k : ℕ) (c : ℂ) : (polyAt i) ((Polynomial.monomial k) c) = MvPolynomial.C c * MvPolynomial.X i ^ k

@[simp]

theorem GaussianMomentsCounterexamples.polyAt_X {n : ℕ} (i : Fin n) : (polyAt i) Polynomial.X = MvPolynomial.X i

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment3_C_mul (c : ℂ) (p : MvPolynomial (Fin 3) ℂ) : naturalMoment3 (MvPolynomial.C c * p) = c * naturalMoment3 p

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment4_C_mul (c : ℂ) (p : MvPolynomial (Fin 4) ℂ) : naturalMoment4 (MvPolynomial.C c * p) = c * naturalMoment4 p

theorem GaussianMomentsCounterexamples.naturalMoment3_contraction (a b : ℕ) (f : Polynomial ℂ) : naturalMoment3 (MvPolynomial.X 0 ^ a * (polyAt 1) f * MvPolynomial.X 2 ^ b) = ↑a.factorial * f.coeff a * ∫ (t : ℝ), ↑t ^ b ∂ProbabilityTheory.gaussianReal 0 1

theorem GaussianMomentsCounterexamples.naturalMoment4_contraction (a b : ℕ) (f g : Polynomial ℂ) : naturalMoment4 (MvPolynomial.X 0 ^ a * (polyAt 1) f * MvPolynomial.X 2 ^ b * (polyAt 3) g) = ↑a.factorial * f.coeff a * (↑b.factorial * g.coeff b)

theorem GaussianMomentsCounterexamples.coeff_one_sub_X_pow (a : ℕ) : ((1 - Polynomial.X) ^ a).coeff a = (-1) ^ a

theorem GaussianMomentsCounterexamples.naturalMoment4_power_expansion (A : Polynomial ℂ) (m : ℕ) : naturalMoment4 ((polyAt 3) A * naturalP4 ^ m) = ↑m.factorial * ∑ a ∈ Finset.range (m + 1), (-1) ^ a * (A * (1 + Polynomial.X) ^ m).coeff (m - a)

theorem GaussianMomentsCounterexamples.naturalMoment4_master (A : Polynomial ℂ) (m : ℕ) (hm : 1 ≤ m) : naturalMoment4 ((polyAt 3) A * naturalP4 ^ m) = ↑m.factorial * (A * (1 + Polynomial.X) ^ (m - 1)).coeff m

The four-variable master identity in the natural-coordinate moment interface.

theorem GaussianMomentsCounterexamples.naturalMoment3_power_expansion_raw (A : Polynomial ℂ) (m : ℕ) : naturalMoment3 ((polyAt 1) A * naturalP3 ^ m) = ∑ k ∈ Finset.range (m + 1), ↑(m.choose k) * (-1 / 2) ^ k * ↑(m - k).factorial * (A * (1 + Polynomial.X) ^ m * (2 + Polynomial.X) ^ k).coeff (m - k) * (↑(2 * k).factorial / (2 ^ k * ↑k.factorial))

theorem GaussianMomentsCounterexamples.naturalMoment3_power_expansion (A : Polynomial ℂ) (m : ℕ) : naturalMoment3 ((polyAt 1) A * naturalP3 ^ m) = ↑m.factorial * ∑ k ∈ Finset.range (m + 1), (-1) ^ k / 4 ^ k * ↑((2 * k).choose k) * (A * (1 + Polynomial.X) ^ m * (2 + Polynomial.X) ^ k).coeff (m - k)

theorem GaussianMomentsCounterexamples.naturalMoment3_master (A : Polynomial ℂ) (m : ℕ) (hm : 1 ≤ m) : naturalMoment3 ((polyAt 1) A * naturalP3 ^ m) = ↑m.factorial * (A * (1 + Polynomial.X) ^ (m - 1)).coeff m

The three-variable master identity in the natural-coordinate moment interface.

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment3_positive_power (m : ℕ) (hm : 1 ≤ m) : naturalMoment3 (naturalP3 ^ m) = 0

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment4_positive_power (m : ℕ) (hm : 1 ≤ m) : naturalMoment4 (naturalP4 ^ m) = 0

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment3_mixed_power (m : ℕ) (hm : 1 ≤ m) : naturalMoment3 (MvPolynomial.X 1 * naturalP3 ^ m) = ↑m.factorial

@[simp]

theorem GaussianMomentsCounterexamples.naturalMoment4_mixed_power (m : ℕ) (hm : 1 ≤ m) : naturalMoment4 (MvPolynomial.X 3 * naturalP4 ^ m) = ↑m.factorial