Explicit partial-pairing expansion of Wick polynomials

This file expands the recursive Wick polynomial as a finite sum over actual PartialPairings. Every two-cycle is represented at its smaller endpoint; the corresponding factor is -C, while fixed points contribute the field value. The head-classification equivalence from PairingRecursion then gives the creation--contraction recursion without any symmetry assumption on C.

def Anderson4D.PartialPairing.representativesBy {α : Type u_1} [Fintype α] [DecidableEq α] (lt : α → α → Prop) [DecidableRel lt] (κ : PartialPairing α) : Finset α

Representatives selected by an explicit strict relation.

Equations

• Anderson4D.PartialPairing.representativesBy lt κ = {i ∈ κ.pairSupport | lt i (κ i)}

def Anderson4D.PartialPairing.representatives {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (κ : PartialPairing α) : Finset α

Smaller endpoints of the two-cycles of a linearly ordered pairing.

Equations

• κ.representatives = Anderson4D.PartialPairing.representativesBy (fun (x1 x2 : α) => x1 < x2) κ

@[simp]

theorem Anderson4D.PartialPairing.mem_representatives {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] {κ : PartialPairing α} {i : α} : i ∈ κ.representatives ↔ κ i ≠ i ∧ i < κ i

def Anderson4D.PartialPairing.optionHeadLT {α : Type u_1} [LT α] : Option α → Option α → Prop

Head-first strict order used only for the Option classification.

Equations

• Anderson4D.PartialPairing.optionHeadLT none (some val) = True
• Anderson4D.PartialPairing.optionHeadLT (some a) (some b) = (a < b)
• Anderson4D.PartialPairing.optionHeadLT x✝¹ x✝ = False

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidableRelOptionOptionHeadLTOfLt {α : Type u_1} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] : DecidableRel optionHeadLT

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.PartialPairing.subtype_lt_iff_val_lt {α : Type u_1} [LT α] {p : α → Prop} (a b : Subtype p) : a < b ↔ ↑a < ↑b

theorem Anderson4D.PartialPairing.representatives_optionFixed {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (κ : PartialPairing α) : representativesBy optionHeadLT κ.optionFixed = Finset.image some κ.representatives

theorem Anderson4D.PartialPairing.singles_optionFixed {α : Type u_1} [Fintype α] [DecidableEq α] (κ : PartialPairing α) : κ.optionFixed.singles = insert none (Finset.image some κ.singles)

theorem Anderson4D.PartialPairing.representatives_optionPaired {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : representativesBy optionHeadLT (optionPaired j κ) = insert none (Finset.image (fun (i : { i : α // i ≠ j }) => some ↑i) κ.representatives)

theorem Anderson4D.PartialPairing.singles_optionPaired {α : Type u_1} [Fintype α] [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (optionPaired j κ).singles = Finset.image (fun (i : { i : α // i ≠ j }) => some ↑i) κ.singles

theorem Anderson4D.PartialPairing.singles_congr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (κ : PartialPairing α) : ((congr e) κ).singles = Finset.image (⇑e) κ.singles

theorem Anderson4D.PartialPairing.representativesBy_congr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ltα : α → α → Prop) [DecidableRel ltα] (ltβ : β → β → Prop) [DecidableRel ltβ] (e : α ≃ β) (hlt : ∀ (i j : α), ltβ (e i) (e j) ↔ ltα i j) (κ : PartialPairing α) : representativesBy ltβ ((congr e) κ) = Finset.image (⇑e) (representativesBy ltα κ)

def Anderson4D.PartialPairing.eraseIdxOrderIso {ι : Type u_1} (xs : List ι) (p : Fin xs.length) : Fin (xs.eraseIdx ↑p).length ≃o { i : Fin xs.length // i ≠ p }

The increasing enumeration of all positions of a list except p.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.PartialPairing.get_eraseIdxOrderIso {ι : Type u_1} (xs : List ι) (p : Fin xs.length) (i : Fin (xs.eraseIdx ↑p).length) : xs.get ↑((eraseIdxOrderIso xs p) i) = (xs.eraseIdx ↑p).get i

theorem Anderson4D.PartialPairing.finSuccEquiv_symm_lt_iff (n : ℕ) (a b : Option (Fin n)) : (finSuccEquiv n).symm a < (finSuccEquiv n).symm b ↔ optionHeadLT a b

def Anderson4D.partialPairingWickWeightBy {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] (lt : α → α → Prop) [DecidableRel lt] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : α → ι) (κ : PartialPairing α) (ω : Ω) : ℝ

One summand of the explicit Wick expansion, with the endpoint of each two-cycle selected by an explicit strict relation.

Equations

• Anderson4D.partialPairingWickWeightBy lt C X v κ ω = (∏ i ∈ Anderson4D.PartialPairing.representativesBy lt κ, -C (v i) (v (κ i))) * ∏ i ∈ κ.singles, X (v i) ω

def Anderson4D.partialPairingWickWeight {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : α → ι) (κ : PartialPairing α) (ω : Ω) : ℝ

One summand of the explicit Wick expansion on a linearly ordered carrier.

Equations

• Anderson4D.partialPairingWickWeight C X v κ ω = Anderson4D.partialPairingWickWeightBy (fun (x1 x2 : α) => x1 < x2) C X v κ ω

def Anderson4D.explicitPartialPairingWickBy {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] (lt : α → α → Prop) [DecidableRel lt] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : α → ι) (ω : Ω) : ℝ

Finite sum over every partial pairing, with representatives selected by an explicit strict relation.

Equations

• Anderson4D.explicitPartialPairingWickBy lt C X v ω = ∑ κ : Anderson4D.PartialPairing α, Anderson4D.partialPairingWickWeightBy lt C X v κ ω

def Anderson4D.explicitPartialPairingWick {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : α → ι) (ω : Ω) : ℝ

Finite sum over every partial pairing of the labelled carrier.

Equations

• Anderson4D.explicitPartialPairingWick C X v ω = Anderson4D.explicitPartialPairingWickBy (fun (x1 x2 : α) => x1 < x2) C X v ω

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

theorem Anderson4D.explicitPartialPairingWickBy_congr {α : Type u_1} {β : Type u_2} {ι : Type u_3} {Ω : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ltα : α → α → Prop) [DecidableRel ltα] (ltβ : β → β → Prop) [DecidableRel ltβ] (e : α ≃ β) (hlt : ∀ (i j : α), ltβ (e i) (e j) ↔ ltα i j) (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : β → ι) (ω : Ω) : explicitPartialPairingWickBy ltβ C X v ω = explicitPartialPairingWickBy ltα C X (v ∘ ⇑e) ω

@[simp]

theorem Anderson4D.partialPairingWickWeightBy_optionFixed {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x : ι) (v : α → ι) (κ : PartialPairing α) (ω : Ω) : partialPairingWickWeightBy PartialPairing.optionHeadLT C X (fun (o : Option α) => o.elim x v) κ.optionFixed ω = X x ω * partialPairingWickWeight C X v κ ω

@[simp]

theorem Anderson4D.partialPairingWickWeightBy_optionPaired {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x : ι) (v : α → ι) (j : α) (κ : PartialPairing { i : α // i ≠ j }) (ω : Ω) : partialPairingWickWeightBy PartialPairing.optionHeadLT C X (fun (o : Option α) => o.elim x v) (PartialPairing.optionPaired j κ) ω = -C x (v j) * partialPairingWickWeight C X (fun (i : { i : α // i ≠ j }) => v ↑i) κ ω

theorem Anderson4D.explicitPartialPairingWickBy_option_recursion {α : Type u_1} {ι : Type u_2} {Ω : Type u_3} [Fintype α] [DecidableEq α] [LinearOrder α] (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (x : ι) (v : α → ι) (ω : Ω) : explicitPartialPairingWickBy PartialPairing.optionHeadLT C X (fun (o : Option α) => o.elim x v) ω = X x ω * explicitPartialPairingWick C X v ω - ∑ j : α, C x (v j) * explicitPartialPairingWick C X (fun (i : { i : α // i ≠ j }) => v ↑i) ω

Splitting according to the partner of the distinguished none index gives the creation--contraction recursion on Option α.

theorem Anderson4D.explicitPartialPairingWick_compl_eq_eraseIdx {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (xs : List ι) (p : Fin xs.length) (ω : Ω) : explicitPartialPairingWick C X (fun (i : { i : Fin xs.length // i ≠ p }) => xs.get ↑i) ω = explicitPartialPairingWick C X (fun (i : Fin (xs.eraseIdx ↑p).length) => (xs.eraseIdx ↑p).get i) ω

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

The standard finite-index version of the explicit partial-pairing expansion for a labelled list.

Equations

• Anderson4D.explicitPartialPairingWickList C X xs ω = Anderson4D.explicitPartialPairingWick C X (fun (i : Fin xs.length) => xs.get i) ω

@[simp]

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

@[simp]

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

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

The explicit partial-pairing expansion satisfies the abstract creation--contraction specification.

theorem Anderson4D.explicitPartialPairingWickList_eq_wickPolynomial {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (xs : List ι) : explicitPartialPairingWickList C X xs = wickPolynomial C X xs

Generic Wick formula: the finite sum over partial pairings is exactly the recursively normal-ordered polynomial.

@[simp]

theorem Anderson4D.explicitPartialPairingWickList_apply_eq_wickPolynomial {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (xs : List ι) (ω : Ω) : explicitPartialPairingWickList C X xs ω = wickPolynomial C X xs ω

theorem Anderson4D.sum_partialPairingWickWeight_eq_wickPolynomial {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (xs : List ι) (ω : Ω) : ∑ κ : PartialPairing (Fin xs.length), partialPairingWickWeight C X (fun (i : Fin xs.length) => xs.get i) κ ω = wickPolynomial C X xs ω

The Wick formula with the explicit summation and weight visible in the statement.