Recursive Wick pairing sums #

This file isolates the finite combinatorics used by Isserlis' theorem. The recursion pairs the first label with each remaining label exactly once and then removes that partner. Thus it enumerates labeled full pairings without quotients or a choice of ordering inside each pair.

The constant-covariance specialization is proved to satisfy exactly the same recurrence as the centered univariate Gaussian moments. A later bridge identifies this recursive presentation with the project's PartialPairing.IsFull sum.

source

@[irreducible]

def Anderson4D.wickPairingList {α : Type u_1} (C : α → α → ℝ) :

List α → ℝ

Recursive sum of covariance products over all full pairings of a list of labeled variables. An odd list evaluates to zero because the recursion eventually reaches a singleton.

Equations

Anderson4D.wickPairingList C [] = 1
Anderson4D.wickPairingList C (x_1 :: xs) = ∑ j : Fin xs.length, C x_1 (xs.get j) * Anderson4D.wickPairingList C (xs.eraseIdx ↑j)

Instances For

source

@[simp]

theorem Anderson4D.wickPairingList_nil {α : Type u_1} (C : α → α → ℝ) :

wickPairingList C [] = 1

source

@[simp]

theorem Anderson4D.wickPairingList_cons {α : Type u_1} (C : α → α → ℝ) (x : α) (xs : List α) :

wickPairingList C (x :: xs) = ∑ j : Fin xs.length, C x (xs.get j) * wickPairingList C (xs.eraseIdx ↑j)

source

@[simp]

theorem Anderson4D.wickPairingList_singleton {α : Type u_1} (C : α → α → ℝ) (x : α) :

wickPairingList C [x] = 0

source

@[simp]

theorem Anderson4D.wickPairingList_pair {α : Type u_1} (C : α → α → ℝ) (x y : α) :

wickPairingList C [x, y] = C x y

source

theorem Anderson4D.wickPairingList_odd_length {α : Type u_1} (C : α → α → ℝ) (q : ℕ) (xs : List α) :

xs.length = 2 * q + 1 → wickPairingList C xs = 0

Recursive Wick sums vanish on lists of odd length.

source

theorem Anderson4D.wickPairingList_const_even {α : Type u_1} (c : ℝ) (q : ℕ) (xs : List α) :

xs.length = 2 * q → wickPairingList (fun (x x_1 : α) => c) xs = ↑(gaussianPairingCount q) * c ^ q

If every covariance entry equals c, the recursive full-pairing sum on 2q labels is (2q-1)!! c^q, with the double factorial represented by gaussianPairingCount.

source