Reindexing cross Wick contractions by finite equivalences

The recursive list contraction used by the generic Wick theorem is the same finite sum as the paper's bijection-between-single-sets representation.

def Anderson4D.listEquivCovarianceProduct {ι : Type u_1} {R : Type u_2} [CommMonoid R] (C : ι → ι → R) (xs ys : List ι) (e : Fin xs.length ≃ Fin ys.length) : R

The product attached to a bijection between the positions of two lists.

Equations

• Anderson4D.listEquivCovarianceProduct C xs ys e = ∏ i : Fin xs.length, C (xs.get i) (ys.get (e i))

def Anderson4D.listEquivCovarianceSum {ι : Type u_1} {R : Type u_2} [CommSemiring R] (C : ι → ι → R) (xs ys : List ι) : R

Sum of covariance products over all bijections between list positions.

Equations

• Anderson4D.listEquivCovarianceSum C xs ys = ∑ e : Fin xs.length ≃ Fin ys.length, Anderson4D.listEquivCovarianceProduct C xs ys e

theorem Anderson4D.CrossWickEquiv.listEquivCovarianceSum_cons {ι : Type u_1} {R : Type u_2} [CommSemiring R] (C : ι → ι → R) (x : ι) (xs ys : List ι) : listEquivCovarianceSum C (x :: xs) ys = ∑ j : Fin ys.length, C x (ys.get j) * listEquivCovarianceSum C xs (ys.eraseIdx ↑j)

Expanding a list-position bijection by the image of its head gives the same one-step recursion as crossWickList.

theorem Anderson4D.crossWickList_eq_listEquivCovarianceSum {ι : Type u_1} (C : ι → ι → ℝ) (xs ys : List ι) : crossWickList C xs ys = listEquivCovarianceSum C xs ys

The recursive cross-contraction polynomial equals the explicit sum over all bijections between the two lists' positions.

theorem Anderson4D.listEquivCovarianceSum_reindex {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (C : ι → ι → ℝ) (xs ys : List ι) (ep : Fin xs.length ≃ α) (em : Fin ys.length ≃ β) : listEquivCovarianceSum C xs ys = ∑ π : α ≃ β, ∏ i : α, C (xs.get (ep.symm i)) (ys.get (em.symm (π i)))

Reindexing the positions of two lists transports the explicit bijection sum without changing its weights.

theorem Anderson4D.listEquivCovarianceSum_orderedFinsets {α : Type u_1} {β : Type u_2} {ι : Type u_3} [LinearOrder α] [LinearOrder β] (sp : Finset α) (sm : Finset β) (C : ι → ι → ℝ) (lp : ↥sp → ι) (lm : ↥sm → ι) : listEquivCovarianceSum C (List.ofFn fun (j : Fin sp.card) => lp ((sp.orderIsoOfFin ⋯) j)) (List.ofFn fun (j : Fin sm.card) => lm ((sm.orderIsoOfFin ⋯) j)) = ∑ π : ↥sp ≃ ↥sm, ∏ i : ↥sp, C (lp i) (lm (π i))

Ordered enumeration of two finite sets transports the list-position bijection sum to a sum over bijections of the finite-set subtypes.