Recursive Gaussian Wick polynomials

This file supplies the algebraic core of the minimal chaos API used in paper equations (2.4) and (3.16). A Wick polynomial is defined by the creation--contraction recursion. The defining identity says that multiplication by one Gaussian coordinate either creates a new single or contracts it with exactly one existing single.

The construction is pointwise and therefore independent of a probability space. Probabilistic moment and orthogonality statements can subsequently identify this recursion with Wiener-chaos projection without changing the combinatorial object used by the parametrix proof.

@[irreducible]

def Anderson4D.wickPolynomial {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) : List ι → Ω → ℝ

The recursively normal-ordered product of a labeled list of real variables with covariance kernel C.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.wickPolynomial C X [] = fun (x : Ω) => 1

@[simp]

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

@[simp]

theorem Anderson4D.wickPolynomial_cons {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x : ι) (xs : List ι) (ω : Ω) : wickPolynomial C X (x :: xs) ω = X x ω * wickPolynomial C X xs ω - ∑ j : Fin xs.length, C x (xs.get j) * wickPolynomial C X (xs.eraseIdx ↑j) ω

@[simp]

theorem Anderson4D.wickPolynomial_singleton {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x : ι) (ω : Ω) : wickPolynomial C X [x] ω = X x ω

@[simp]

theorem Anderson4D.wickPolynomial_pair {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x y : ι) (ω : Ω) : wickPolynomial C X [x, y] ω = X x ω * X y ω - C x y

theorem Anderson4D.mul_wickPolynomial_eq_create_add_contract {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x : ι) (xs : List ι) (ω : Ω) : X x ω * wickPolynomial C X xs ω = wickPolynomial C X (x :: xs) ω + ∑ j : Fin xs.length, C x (xs.get j) * wickPolynomial C X (xs.eraseIdx ↑j) ω

Creation--contraction identity. This is the exact algebra used when the new noise index in Proposition 3.4 is either left single or paired with one of the old single indices.

theorem Anderson4D.wickPolynomial_zeroCovariance {ι : Type u_1} {Ω : Type u_2} (X : ι → Ω → ℝ) (xs : List ι) (ω : Ω) : wickPolynomial (fun (x x_1 : ι) => 0) X xs ω = (List.map (fun (x : ι) => X x ω) xs).prod

With zero covariance there are no contractions, so normal ordering is the ordinary product.

theorem Anderson4D.measurable_wickPolynomial {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (hX : ∀ (i : ι), Measurable (X i)) (xs : List ι) : Measurable (wickPolynomial C X xs)

Wick polynomials are measurable whenever all generating coordinates are measurable.

The finite-product chaos projection used in the paper

def Anderson4D.chaosProjProduct {ι : Type u_1} {Ω : Type u_2} (k : ℕ) (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (xs : List ι) : Ω → ℝ

The degree-k chaos projection of one finite coordinate product.

The paper only applies Projₖ to a product of exactly k Gaussian coordinates. On that domain the projection is the normal-ordered product; a mismatched degree is set to zero. This deliberately avoids claiming a global orthogonal-projection operator on all of L²(Ω), which is not needed by the parametrix construction.

Equations

• Anderson4D.chaosProjProduct k C X xs = if xs.length = k then Anderson4D.wickPolynomial C X xs else 0

@[simp]

theorem Anderson4D.chaosProjProduct_eq_wickPolynomial {ι : Type u_1} {Ω : Type u_2} {k : ℕ} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) {xs : List ι} (hdegree : xs.length = k) : chaosProjProduct k C X xs = wickPolynomial C X xs

@[simp]

theorem Anderson4D.chaosProjProduct_eq_zero {ι : Type u_1} {Ω : Type u_2} {k : ℕ} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) {xs : List ι} (hdegree : xs.length ≠ k) : chaosProjProduct k C X xs = 0

theorem Anderson4D.measurable_chaosProjProduct {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (k : ℕ) (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (hX : ∀ (i : ι), Measurable (X i)) (xs : List ι) : Measurable (chaosProjProduct k C X xs)

Finite-product chaos projections are measurable whenever the underlying Gaussian coordinates are measurable.

structure Anderson4D.WickRecursionLaw {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (W : List ι → Ω → ℝ) : Prop

A pointwise family obeys the Gaussian Wick recursion when it has the empty value 1 and the same creation--contraction rule as wickPolynomial.

• empty (ω : Ω) : W [] ω = 1
• create_contract (x : ι) (xs : List ι) (ω : Ω) : X x ω * W xs ω = W (x :: xs) ω + ∑ j : Fin xs.length, C x (xs.get j) * W (xs.eraseIdx ↑j) ω

theorem Anderson4D.wickPolynomial_recursionLaw {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) : WickRecursionLaw C X (wickPolynomial C X)

The recursively defined Wick polynomial satisfies its abstract creation--contraction specification.

theorem Anderson4D.WickRecursionLaw.eq_wickPolynomial {ι : Type u_1} {Ω : Type u_2} {C : ι → ι → ℝ} {X : ι → Ω → ℝ} {W : List ι → Ω → ℝ} (hW : WickRecursionLaw C X W) (xs : List ι) : W xs = wickPolynomial C X xs

The creation--contraction law determines the Wick family uniquely. This is the comparison principle used later to identify the combinatorial normal ordering with a Hilbert-space Wiener-chaos projection.