Algebraic orthogonality of multivariate Wick polynomials

This file proves the Wick-product orthogonality theorem from one transparent Gaussian integration-by-parts interface. The proof is polynomial and works for a possibly degenerate covariance matrix.

The polynomial normal ordering is implemented by the creation operator

Aₓ p = Xₓ p - Dₓ p,

where Dₓ is the derivation sending Xᵧ to the covariance C x y. The commutator identity and Gaussian integration by parts give

E[(Aₓ p)q] = E[p(Dₓ q)].

Iterating this identity leaves exactly the recursive sum of cross contractions and proves that different homogeneous Wick orders are orthogonal.

noncomputable def Anderson4D.covarianceDerivation {ι : Type u_1} (C : ι → ι → ℝ) (x : ι) : Derivation ℝ (MvPolynomial ι ℝ) (MvPolynomial ι ℝ)

Covariance-weighted derivation on the multivariate polynomial ring.

Equations

• Anderson4D.covarianceDerivation C x = MvPolynomial.mkDerivation ℝ fun (y : ι) => MvPolynomial.C (C x y)

@[simp]

theorem Anderson4D.covarianceDerivation_X {ι : Type u_1} (C : ι → ι → ℝ) (x y : ι) : (covarianceDerivation C x) (MvPolynomial.X y) = MvPolynomial.C (C x y)

@[simp]

theorem Anderson4D.covarianceDerivation_C {ι : Type u_1} (C : ι → ι → ℝ) (x : ι) (r : ℝ) : (covarianceDerivation C x) (MvPolynomial.C r) = 0

theorem Anderson4D.covarianceDerivation_mul {ι : Type u_1} (C : ι → ι → ℝ) (x : ι) (p q : MvPolynomial ι ℝ) : (covarianceDerivation C x) (p * q) = (covarianceDerivation C x) p * q + p * (covarianceDerivation C x) q

theorem Anderson4D.covarianceDerivation_comm {ι : Type u_1} (C : ι → ι → ℝ) (_hC : ∀ (x y : ι), C x y = C y x) (x y : ι) (p : MvPolynomial ι ℝ) : (covarianceDerivation C x) ((covarianceDerivation C y) p) = (covarianceDerivation C y) ((covarianceDerivation C x) p)

Covariance derivations commute when the covariance is symmetric.

noncomputable def Anderson4D.wickCreation {ι : Type u_1} (C : ι → ι → ℝ) (x : ι) (p : MvPolynomial ι ℝ) : MvPolynomial ι ℝ

Creation operator associated with the covariance.

Equations

• Anderson4D.wickCreation C x p = MvPolynomial.X x * p - (Anderson4D.covarianceDerivation C x) p

def Anderson4D.wickMvPolynomial {ι : Type u_1} (C : ι → ι → ℝ) : List ι → MvPolynomial ι ℝ

Polynomial obtained by iterated normal ordering.

Equations

• Anderson4D.wickMvPolynomial C [] = 1
• Anderson4D.wickMvPolynomial C (x_1 :: xs) = Anderson4D.wickCreation C x_1 (Anderson4D.wickMvPolynomial C xs)

@[simp]

theorem Anderson4D.wickMvPolynomial_nil {ι : Type u_1} (C : ι → ι → ℝ) : wickMvPolynomial C [] = 1

@[simp]

theorem Anderson4D.wickMvPolynomial_cons {ι : Type u_1} (C : ι → ι → ℝ) (x : ι) (xs : List ι) : wickMvPolynomial C (x :: xs) = wickCreation C x (wickMvPolynomial C xs)

theorem Anderson4D.covarianceDerivation_wickCreation {ι : Type u_1} (C : ι → ι → ℝ) (hC : ∀ (x y : ι), C x y = C y x) (a x : ι) (p : MvPolynomial ι ℝ) : (covarianceDerivation C a) (wickCreation C x p) = MvPolynomial.C (C a x) * p + wickCreation C x ((covarianceDerivation C a) p)

The covariance derivation and creation operator satisfy the canonical commutator relation.

theorem Anderson4D.covarianceDerivation_wickMvPolynomial {ι : Type u_1} (C : ι → ι → ℝ) (hC : ∀ (x y : ι), C x y = C y x) (a : ι) (xs : List ι) : (covarianceDerivation C a) (wickMvPolynomial C xs) = ∑ j : Fin xs.length, MvPolynomial.C (C a (xs.get j)) * wickMvPolynomial C (xs.eraseIdx ↑j)

Appell property of the multivariate Wick polynomial.

theorem Anderson4D.wickMvPolynomial_cons_explicit {ι : Type u_1} (C : ι → ι → ℝ) (hC : ∀ (x y : ι), C x y = C y x) (x : ι) (xs : List ι) : wickMvPolynomial C (x :: xs) = MvPolynomial.X x * wickMvPolynomial C xs - ∑ j : Fin xs.length, MvPolynomial.C (C x (xs.get j)) * wickMvPolynomial C (xs.eraseIdx ↑j)

Normal ordering satisfies exactly the recursive definition frozen in Probability/Chaos.lean.

theorem Anderson4D.eval_wickMvPolynomial_eq_wickPolynomial {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (hC : ∀ (x y : ι), C x y = C y x) (X : ι → Ω → ℝ) (xs : List ι) (ω : Ω) : (MvPolynomial.eval fun (x : ι) => X x ω) (wickMvPolynomial C xs) = wickPolynomial C X xs ω

Evaluation of the polynomial normal ordering is the recursive random Wick polynomial.

def Anderson4D.crossWickList {ι : Type u_1} (C : ι → ι → ℝ) : List ι → List ι → ℝ

Recursive cross-contraction sum. It is automatically zero when the two lists have different lengths.

Equations

• Anderson4D.crossWickList C [] [] = 1
• Anderson4D.crossWickList C [] (head :: tail) = 0
• Anderson4D.crossWickList C (x_2 :: xs) x✝ = ∑ j : Fin x✝.length, C x_2 (x✝.get j) * Anderson4D.crossWickList C xs (x✝.eraseIdx ↑j)

@[simp]

theorem Anderson4D.crossWickList_nil_nil {ι : Type u_1} (C : ι → ι → ℝ) : crossWickList C [] [] = 1

@[simp]

theorem Anderson4D.crossWickList_nil_cons {ι : Type u_1} (C : ι → ι → ℝ) (y : ι) (ys : List ι) : crossWickList C [] (y :: ys) = 0

@[simp]

theorem Anderson4D.crossWickList_cons {ι : Type u_1} (C : ι → ι → ℝ) (x : ι) (xs ys : List ι) : crossWickList C (x :: xs) ys = ∑ j : Fin ys.length, C x (ys.get j) * crossWickList C xs (ys.eraseIdx ↑j)

theorem Anderson4D.crossWickList_eq_zero_of_length_ne {ι : Type u_1} (C : ι → ι → ℝ) (xs ys : List ι) : xs.length ≠ ys.length → crossWickList C xs ys = 0

Recursive cross-contraction sums vanish for unequal list lengths.

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

Polynomial integration-by-parts interface for a centered Gaussian family. The later noise specialization proves this from NoiseModel's joint Gaussianity; it is not an additional axiom.

• measureReal_univ : μ.real Set.univ = 1
• covariance_symm (x y : ι) : C x y = C y x
• integrable_eval (p : MvPolynomial ι ℝ) : MeasureTheory.Integrable (fun (ω : Ω) => (MvPolynomial.eval fun (x : ι) => X x ω) p) μ
• integration_by_parts (x : ι) (p : MvPolynomial ι ℝ) : ∫ (ω : Ω), (MvPolynomial.eval fun (y : ι) => X y ω) (MvPolynomial.X x * p) ∂μ = ∫ (ω : Ω), (MvPolynomial.eval fun (y : ι) => X y ω) ((covarianceDerivation C x) p) ∂μ

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

Expectation of a polynomial under a GaussianPolynomialLaw.

Equations

• Anderson4D.polynomialExpectation μ X p = ∫ (ω : Ω), (MvPolynomial.eval fun (x : ι) => X x ω) p ∂μ

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

theorem Anderson4D.GaussianPolynomialLaw.expectation_sub {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (p q : MvPolynomial ι ℝ) : polynomialExpectation μ X (p - q) = polynomialExpectation μ X p - polynomialExpectation μ X q

theorem Anderson4D.GaussianPolynomialLaw.expectation_finsetSum {ι : Type u_1} {Ω : Type u_2} {α : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (s : Finset α) (p : α → MvPolynomial ι ℝ) : polynomialExpectation μ X (∑ i ∈ s, p i) = ∑ i ∈ s, polynomialExpectation μ X (p i)

theorem Anderson4D.GaussianPolynomialLaw.expectation_fintypeSum {ι : Type u_1} {Ω : Type u_2} {α : Type u_3} [MeasurableSpace Ω] [Fintype α] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (p : α → MvPolynomial ι ℝ) : polynomialExpectation μ X (∑ i : α, p i) = ∑ i : α, polynomialExpectation μ X (p i)

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

theorem Anderson4D.GaussianPolynomialLaw.expectation_X_mul {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (x : ι) (p : MvPolynomial ι ℝ) : polynomialExpectation μ X (MvPolynomial.X x * p) = polynomialExpectation μ X ((covarianceDerivation C x) p)

theorem Anderson4D.GaussianPolynomialLaw.expectation_wickCreation_mul {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (x : ι) (p q : MvPolynomial ι ℝ) : polynomialExpectation μ X (wickCreation C x p * q) = polynomialExpectation μ X (p * (covarianceDerivation C x) q)

Creation is adjoint to covariance differentiation under Gaussian expectation.

theorem Anderson4D.GaussianPolynomialLaw.expectation_wickMvPolynomial_cons {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (x : ι) (xs : List ι) : polynomialExpectation μ X (wickMvPolynomial C (x :: xs)) = 0

A nonconstant Wick polynomial is centered.

theorem Anderson4D.GaussianPolynomialLaw.expectation_wickMvPolynomial_mul {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (xs ys : List ι) : polynomialExpectation μ X (wickMvPolynomial C xs * wickMvPolynomial C ys) = crossWickList C xs ys

Generic multivariate Wick orthogonality.

The expectation of two normal-ordered products is exactly the recursive sum of cross contractions.

theorem Anderson4D.GaussianPolynomialLaw.integral_wickPolynomial_mul {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (xs ys : List ι) : ∫ (ω : Ω), wickPolynomial C X xs ω * wickPolynomial C X ys ω ∂μ = crossWickList C xs ys

Function-level version of generic Wick orthogonality.

theorem Anderson4D.GaussianPolynomialLaw.integral_chaosProjProduct_mul_eq_zero_of_ne {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) {k l : ℕ} (hkl : k ≠ l) (xs ys : List ι) (hxs : xs.length = k) (hys : ys.length = l) : ∫ (ω : Ω), chaosProjProduct k C X xs ω * chaosProjProduct l C X ys ω ∂μ = 0

Finite Gaussian products projected to different chaos degrees are orthogonal. This is the precise Projₖ property used for the noise-product factors in the parametrix.

theorem Anderson4D.GaussianPolynomialLaw.integrable_wickPolynomial_mul {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} (h : GaussianPolynomialLaw μ C X) (xs ys : List ι) : MeasureTheory.Integrable (fun (ω : Ω) => wickPolynomial C X xs ω * wickPolynomial C X ys ω) μ

Every product of two Wick polynomials is integrable.