Gaussian list moments imply polynomial integration by parts

This file bridges the Isserlis moment formula to the polynomial integration-by-parts interface used by the generic Wick orthogonality theorem.

def Anderson4D.gaussianListProduct {ι : Type u_1} {Ω : Type u_2} (X : ι → Ω → ℝ) (xs : List ι) (ω : Ω) : ℝ

Product of the coordinates selected by a list.

Equations

• Anderson4D.gaussianListProduct X xs ω = (List.map (fun (i : ι) => X i ω) xs).prod

@[simp]

theorem Anderson4D.gaussianListProduct_nil {ι : Type u_1} {Ω : Type u_2} (X : ι → Ω → ℝ) (ω : Ω) : gaussianListProduct X [] ω = 1

@[simp]

theorem Anderson4D.gaussianListProduct_cons {ι : Type u_1} {Ω : Type u_2} (X : ι → Ω → ℝ) (x : ι) (xs : List ι) (ω : Ω) : gaussianListProduct X (x :: xs) ω = X x ω * gaussianListProduct X xs ω

structure Anderson4D.GaussianListMomentLaw {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (C : ι → ι → ℝ) (X : ι → Ω → ℝ) : Prop

Raw Isserlis moment interface for a centered Gaussian family.

• covariance_symm (x y : ι) : C x y = C y x
• integrable_listProduct (xs : List ι) : MeasureTheory.Integrable (gaussianListProduct X xs) μ
• integral_listProduct (xs : List ι) : ∫ (ω : Ω), gaussianListProduct X xs ω ∂μ = wickPairingList C xs

noncomputable def Anderson4D.polynomialListExpectation {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → ℝ) (p : MvPolynomial ι ℝ) (xs : List ι) : ℝ

Expectation of a polynomial times a coordinate-list monomial.

Equations

• Anderson4D.polynomialListExpectation μ X p xs = ∫ (ω : Ω), (MvPolynomial.eval fun (i : ι) => X i ω) p * Anderson4D.gaussianListProduct X xs ω ∂μ

theorem Anderson4D.GaussianListMomentLaw.integrable_eval_mul_listProduct {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianListMomentLaw μ C X) (p : MvPolynomial ι ℝ) (xs : List ι) : MeasureTheory.Integrable (fun (ω : Ω) => (MvPolynomial.eval fun (i : ι) => X i ω) p * gaussianListProduct X xs ω) μ

theorem Anderson4D.GaussianListMomentLaw.integrable_eval {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianListMomentLaw μ C X) (p : MvPolynomial ι ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => (MvPolynomial.eval fun (i : ι) => X i ω) p) μ

theorem Anderson4D.GaussianListMomentLaw.expectation_C {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianListMomentLaw μ C X) (r : ℝ) (xs : List ι) : polynomialListExpectation μ X (MvPolynomial.C r) xs = r * wickPairingList C xs

theorem Anderson4D.GaussianListMomentLaw.expectation_add {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianListMomentLaw μ C X) (p q : MvPolynomial ι ℝ) (xs : List ι) : polynomialListExpectation μ X (p + q) xs = polynomialListExpectation μ X p xs + polynomialListExpectation μ X q xs

theorem Anderson4D.GaussianListMomentLaw.expectation_mul_X {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (_h : GaussianListMomentLaw μ C X) (p : MvPolynomial ι ℝ) (y : ι) (xs : List ι) : polynomialListExpectation μ X (p * MvPolynomial.X y) xs = polynomialListExpectation μ X p (y :: xs)

theorem Anderson4D.GaussianListMomentLaw.expectation_C_mul {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (_h : GaussianListMomentLaw μ C X) (r : ℝ) (p : MvPolynomial ι ℝ) (xs : List ι) : polynomialListExpectation μ X (MvPolynomial.C r * p) xs = r * polynomialListExpectation μ X p xs

theorem Anderson4D.GaussianListMomentLaw.integrationByParts_with_list {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianListMomentLaw μ C X) (x : ι) (p : MvPolynomial ι ℝ) (xs : List ι) : polynomialListExpectation μ X (MvPolynomial.X x * p) xs = polynomialListExpectation μ X ((covarianceDerivation C x) p) xs + ∑ j : Fin xs.length, C x (xs.get j) * polynomialListExpectation μ X p (xs.eraseIdx ↑j)

Strong polynomial integration by parts, with an additional coordinate list carried through the induction.

theorem Anderson4D.GaussianListMomentLaw.toGaussianPolynomialLaw {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianListMomentLaw μ C X) : GaussianPolynomialLaw μ C X

Isserlis list moments yield the exact polynomial integration-by-parts interface used by generic Wick orthogonality.