Equivalence extracting element from contraction

theorem WickContraction.extractEquiv_equiv {n : ℕ} {c1 c2 : (c : WickContraction n) × Option ↥c.uncontracted} (h : c1.fst = c2.fst) (ho : c1.snd = (uncontractedCongr ⋯) c2.snd) : c1 = c2

def WickContraction.extractEquiv {n : ℕ} (i : Fin n.succ) : WickContraction n.succ ≃ (c : WickContraction n) × Option ↥c.uncontracted

The equivalence between WickContraction n.succ and the sigma type (c : WickContraction n) × Option c.uncontracted formed by inserting and erasing elements from a contraction.

Equations

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

theorem WickContraction.extractEquiv_symm_none_uncontracted {n : ℕ} (i : Fin n.succ) (c : WickContraction n) : ((extractEquiv i).symm ⟨c, none⟩).uncontracted = insert i (Finset.map i.succAboveEmb c.uncontracted)

@[simp]

theorem WickContraction.extractEquiv_apply_congr_symm_apply {n m : ℕ} (k : ℕ) (hnk : k < n.succ) (hkm : k < m.succ) (hnm : n = m) (c : WickContraction n) (i : ↥c.uncontracted) : (congr ⋯) ((extractEquiv ⟨k, hkm⟩) ((congr ⋯) ((extractEquiv ⟨k, hnk⟩).symm ⟨c, some i⟩))).fst = c

instance WickContraction.fintype_zero : Fintype (WickContraction 0)

The fintype instance of WickContraction 0 defined through its single element empty.

Equations

• WickContraction.fintype_zero = { elems := {WickContraction.empty}, complete := WickContraction.fintype_zero._proof_1 }

theorem WickContraction.sum_WickContraction_nil {M : Type u_1} (f : WickContraction 0 → M) [AddCommMonoid M] : ∑ c : WickContraction 0, f c = f empty

instance WickContraction.fintype_succ (n : ℕ) : Fintype (WickContraction n)

The fintype instance of WickContraction n, for n.succ this is defined through the equivalence extractEquiv.

Equations

• WickContraction.fintype_succ 0 = WickContraction.fintype_zero
• WickContraction.fintype_succ n.succ = Fintype.ofEquiv ((c : WickContraction n) × Option ↥c.uncontracted) (WickContraction.extractEquiv 0).symm

theorem WickContraction.sum_extractEquiv_congr {M : Type u_1} [AddCommMonoid M] {n m : ℕ} (i : Fin n) (f : WickContraction n → M) (h : n = m.succ) : ∑ c : WickContraction n, f c = ∑ c : WickContraction m, ∑ k : Option ↥c.uncontracted, f ((congr ⋯) ((extractEquiv ((finCongr h) i)).symm ⟨c, k⟩))

theorem WickContraction.mem_three (c : WickContraction 3) : ↑c ∈ {∅, {{0, 1}}, {{0, 2}}, {{1, 2}}}

For n = 3 there are 4 possible Wick contractions:

• ∅, corresponding to the case where no fields are contracted.
• {{0, 1}}, corresponding to the case where the field at position 0 and 1 are contracted.
• {{0, 2}}, corresponding to the case where the field at position 0 and 2 are contracted.
• {{1, 2}}, corresponding to the case where the field at position 1 and 2 are contracted.

The proof of this result uses the fact that Lean is an executable programming language and can calculate all Wick contractions for a given n.

theorem WickContraction.mem_four (c : WickContraction 4) : ↑c ∈ {∅, {{0, 1}}, {{0, 2}}, {{0, 3}}, {{1, 2}}, {{1, 3}}, {{2, 3}}, {{0, 1}, {2, 3}}, {{0, 2}, {1, 3}}, {{0, 3}, {1, 2}}}

For n = 4 there are 10 possible Wick contractions including e.g.

• ∅, corresponding to the case where no fields are contracted.
• {{0, 1}, {2, 3}}, corresponding to the case where the fields at position 0 and 1 are contracted, and the fields at position 2 and 3 are contracted.
• {{0, 2}, {1, 3}}, corresponding to the case where the fields at position 0 and 2 are contracted, and the fields at position 1 and 3 are contracted.

The proof of this result uses the fact that Lean is an executable programming language and can calculate all Wick contractions for a given n.