Full partial pairings and the recursive Wick sum

The paper writes Wick limits as a sum over full PartialPairings, whereas the finite multilinearity API uses the head-partner recursion finWickPairing. This file proves that the two presentations agree, for an arbitrary commutative semiring of edge weights.

def Anderson4D.PartialPairing.covarianceProductBy {α : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype α] [DecidableEq α] (lt : α → α → Prop) [DecidableRel lt] [CommMonoid R] (C : ι → ι → R) (v : α → ι) (κ : PartialPairing α) : R

Product of edge weights, selecting the lower endpoint of every two-cycle by an explicit strict relation.

Equations

• Anderson4D.PartialPairing.covarianceProductBy lt C v κ = ∏ i ∈ Anderson4D.PartialPairing.representativesBy lt κ, C (v i) (v (κ i))

def Anderson4D.PartialPairing.fullCovarianceSumBy {α : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype α] [DecidableEq α] (lt : α → α → Prop) [DecidableRel lt] [CommSemiring R] (C : ι → ι → R) (v : α → ι) : R

Sum of covariance products over full pairings, with representatives selected by an explicit strict relation.

Equations

• Anderson4D.PartialPairing.fullCovarianceSumBy lt C v = ∑ κ : Anderson4D.PartialPairing α, if κ.IsFull then Anderson4D.PartialPairing.covarianceProductBy lt C v κ else 0

def Anderson4D.PartialPairing.fullCovarianceSum {α : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] [CommSemiring R] (C : ι → ι → R) (v : α → ι) : R

The standard linearly ordered presentation of the full-pairing covariance sum.

Equations

• Anderson4D.PartialPairing.fullCovarianceSum C v = Anderson4D.PartialPairing.fullCovarianceSumBy (fun (x1 x2 : α) => x1 < x2) C v

theorem Anderson4D.PartialPairing.fullCovarianceSum_eq_filter_sum {α : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] [CommSemiring R] (C : ι → ι → R) (v : α → ι) : fullCovarianceSum C v = ∑ κ : PartialPairing α with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, C (v i) (v (κ i))

Filtered-finset presentation used verbatim by Proposition 3.6.

theorem Anderson4D.PartialPairing.covarianceProductBy_congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} {R : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ltα : α → α → Prop) [DecidableRel ltα] (ltβ : β → β → Prop) [DecidableRel ltβ] [CommMonoid R] (e : α ≃ β) (hlt : ∀ (i j : α), ltβ (e i) (e j) ↔ ltα i j) (C : ι → ι → R) (v : β → ι) (κ : PartialPairing α) : covarianceProductBy ltβ C v ((congr e) κ) = covarianceProductBy ltα C (v ∘ ⇑e) κ

theorem Anderson4D.PartialPairing.isFull_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) (κ : PartialPairing α) : ((congr e) κ).IsFull ↔ κ.IsFull

theorem Anderson4D.PartialPairing.fullCovarianceSumBy_congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} {R : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ltα : α → α → Prop) [DecidableRel ltα] (ltβ : β → β → Prop) [DecidableRel ltβ] [CommSemiring R] (e : α ≃ β) (hlt : ∀ (i j : α), ltβ (e i) (e j) ↔ ltα i j) (C : ι → ι → R) (v : β → ι) : fullCovarianceSumBy ltβ C v = fullCovarianceSumBy ltα C (v ∘ ⇑e)

theorem Anderson4D.PartialPairing.isFull_optionFixed {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) : ¬κ.optionFixed.IsFull

theorem Anderson4D.PartialPairing.isFull_optionPaired {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (optionPaired j κ).IsFull ↔ κ.IsFull

theorem Anderson4D.PartialPairing.covarianceProductBy_optionPaired {α : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] [CommMonoid R] (C : ι → ι → R) (x : ι) (v : α → ι) (j : α) (κ : PartialPairing { i : α // i ≠ j }) : covarianceProductBy optionHeadLT C (fun (o : Option α) => o.elim x v) (optionPaired j κ) = C x (v j) * covarianceProductBy (fun (x1 x2 : { i : α // i ≠ j }) => x1 < x2) C (fun (i : { i : α // i ≠ j }) => v ↑i) κ

theorem Anderson4D.PartialPairing.fullCovarianceSumBy_option {α : Type u_1} {ι : Type u_2} {R : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] [CommSemiring R] (C : ι → ι → R) (x : ι) (v : α → ι) : (fullCovarianceSumBy optionHeadLT C fun (o : Option α) => o.elim x v) = ∑ j : α, C x (v j) * fullCovarianceSum C fun (i : { i : α // i ≠ j }) => v ↑i

Head-partner recurrence for the full partial-pairing sum.

theorem Anderson4D.PartialPairing.fullCovarianceSum_orderIso {α : Type u_1} {β : Type u_2} {ι : Type u_3} {R : Type u_4} [Fintype α] [DecidableEq α] [LinearOrder α] [Fintype β] [DecidableEq β] [LinearOrder β] [CommSemiring R] (e : α ≃o β) (C : ι → ι → R) (v : β → ι) : fullCovarianceSum C v = fullCovarianceSum C (v ∘ ⇑e)

Transporting labels through an order isomorphism does not change a full-pairing covariance sum.

@[simp]

theorem Anderson4D.PartialPairing.fullCovarianceSum_fin_zero {ι : Type u_1} {R : Type u_2} [CommSemiring R] (C : ι → ι → R) (v : Fin 0 → ι) : fullCovarianceSum C v = 1

Full-pairing sum on Fin 0.

@[simp]

theorem Anderson4D.PartialPairing.fullCovarianceSum_fin_one {ι : Type u_1} {R : Type u_2} [CommSemiring R] (C : ι → ι → R) (v : Fin 1 → ι) : fullCovarianceSum C v = 0

There is no full pairing of a singleton.

theorem Anderson4D.PartialPairing.fullCovarianceSum_fin_add_two {ι : Type u_1} {R : Type u_2} [CommSemiring R] (C : ι → ι → R) (n : ℕ) (v : Fin (n + 2) → ι) : fullCovarianceSum C v = ∑ j : Fin (n + 1), C (v 0) (v j.succ) * fullCovarianceSum C fun (i : Fin n) => v (j.succAbove i).succ

Removing the head and its selected partner gives the same head-partner recurrence as finWickPairing.

theorem Anderson4D.PartialPairing.fullCovarianceSum_fin_eq_finWickPairing {ι : Type u_1} {R : Type u_2} [CommSemiring R] (C : ι → ι → R) (n : ℕ) (v : Fin n → ι) : fullCovarianceSum C v = finWickPairing C n v

The paper's explicit sum over full involutions is exactly the recursive Wick-pairing sum.

Constant covariance

theorem Anderson4D.finWickPairing_const_odd {α : Type u_1} {R : Type u_2} [CommSemiring R] (c : R) (q : ℕ) (v : Fin (2 * q + 1) → α) : finWickPairing (fun (x x_1 : α) => c) (2 * q + 1) v = 0

A recursive full-pairing sum with constant covariance vanishes in odd degree.

theorem Anderson4D.finWickPairing_const_even {α : Type u_1} {R : Type u_2} [CommSemiring R] (c : R) (q : ℕ) (v : Fin (2 * q) → α) : finWickPairing (fun (x x_1 : α) => c) (2 * q) v = ↑(gaussianPairingCount q) * c ^ q

A recursive full-pairing sum with constant covariance is the pairing count times the corresponding covariance power.