Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.QFT.PerturbationTheory.WickContraction.UncontractedListInserting an element into a contraction based on a list
@[expose] public sectionInserting an element into a list
Given a Wick contraction φsΛ for a list φs of 𝓕.FieldOp,
an element φ of 𝓕.FieldOp, an i ≤ φs.length and a k
in Option φsΛ.uncontracted i.e. is either none or
some element of φsΛ.uncontracted, the new Wick contraction
φsΛ.insertAndContract φ i k is defined by inserting φ into φs after
the first i-elements and moving the values representing the contracted pairs in φsΛ
accordingly.
If k is not none, but rather some k, to this contraction is added the contraction
of φ (at position i) with the new position of k after φ is added.
In other words, φsΛ.insertAndContract φ i k is formed by adding φ to φs at position i,
and contracting φ with the field originally at position k if k is not none.
It is a Wick contraction of the list φs.insertIdx φ i corresponding to φs with φ inserted at
position i.
The notation φsΛ ↩Λ φ i k is used to denote φsΛ.insertAndContract φ i k.
def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length)
(i : Fin φs.length.succ) (k : Option φsΛ.uncontracted) :
WickContraction (φs.insertIdx i φ).length :=
congr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφ:𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:Option ↥φsΛ.uncontracted⊢ φs.length.succ = (φs.insertIdx (↑i) φ).length All goals completed! 🐙) (φsΛ.insertAndContractNat i k)@[inherit_doc insertAndContract]
scoped[WickContraction] notation φs "↩Λ" φ:max i:max j => insertAndContract φ φs i j@[simp]
lemma insertAndContract_fstFieldOfContract (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted)
(a : φsΛ.1) : (φsΛ ↩Λ φ i j).fstFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (φsΛ.fstFieldOfContract a)) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Option ↥φsΛ.uncontracteda:↥↑φsΛ⊢ (φsΛ↩Λφ i j).fstFieldOfContract (congrLift ⋯ (insertLift i j a)) = (finCongr ⋯) (i.succAbove (φsΛ.fstFieldOfContract a))
All goals completed! 🐙@[simp]
lemma insertAndContract_sndFieldOfContract (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option (φsΛ.uncontracted))
(a : φsΛ.1) : (φsΛ ↩Λ φ i j).sndFieldOfContract
(congrLift (insertIdx_length_fin φ φs i).symm (insertLift i j a)) =
finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove (φsΛ.sndFieldOfContract a)) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Option ↥φsΛ.uncontracteda:↥↑φsΛ⊢ (φsΛ↩Λφ i j).sndFieldOfContract (congrLift ⋯ (insertLift i j a)) = (finCongr ⋯) (i.succAbove (φsΛ.sndFieldOfContract a))
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh:¬↑i < ↑(i.succAbove ↑j)⊢ ↑((finCongr ⋯) (i.succAbove ↑j)) < ↑((finCongr ⋯) i)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh:i.succAbove ↑j ≤ i⊢ i.succAbove ↑j < i
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh:i.succAbove ↑j ≤ ihi:i.succAbove ↑j ≠ i⊢ i.succAbove ↑j < i
All goals completed! 🐙insertAndContract and getDual?
@[simp]
lemma insertAndContract_none_getDual?_self (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
(φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i) = none := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (φsΛ↩Λφ i none).getDual? (Fin.cast ⋯ i) = none
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (φsΛ.insertAndContractNat i none).getDual? i = none
All goals completed! 🐙lemma insertAndContract_isSome_getDual?_self (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
((φsΛ ↩Λ φ i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm i)).isSome := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ((φsΛ↩Λφ i some j).getDual? (Fin.cast ⋯ i)).isSome = true
All goals completed! 🐙lemma insertAndContract_some_getDual?_self_not_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
¬ ((φsΛ ↩Λ φ i (some j)).getDual?
(Fin.cast (insertIdx_length_fin φ φs i).symm i)) = none := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ¬(φsΛ↩Λφ i some j).getDual? (Fin.cast ⋯ i) = none
All goals completed! 🐙@[simp]
lemma insertAndContract_some_getDual?_self_eq (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
((φsΛ ↩Λ φ i (some j)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm i))
= some (Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove j)) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ (φsΛ↩Λφ i some j).getDual? (Fin.cast ⋯ i) = some (Fin.cast ⋯ (i.succAbove ↑j))
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ (φsΛ↩Λφ i some j).getDual? (Fin.cast ⋯ i) = some (Fin.cast ⋯ (i.succAbove ↑j))
All goals completed! 🐙@[simp]
lemma insertAndContract_none_succAbove_getDual?_eq_none_iff (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) :
(φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j)) = none ↔ φsΛ.getDual? j = none := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Fin φs.length⊢ (φsΛ↩Λφ i none).getDual? (Fin.cast ⋯ (i.succAbove j)) = none ↔ φsΛ.getDual? j = none
All goals completed! 🐙@[simp]
lemma insertAndContract_some_succAbove_getDual?_eq_option (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
(k : φsΛ.uncontracted) (hkj : j ≠ k.1) :
(φsΛ ↩Λ φ i (some k)).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j)) = Option.map (Fin.cast (insertIdx_length_fin φ φs i).symm ∘ i.succAbove)
(φsΛ.getDual? j) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Fin φs.lengthk:↥φsΛ.uncontractedhkj:j ≠ ↑k⊢ (φsΛ↩Λφ i some k).getDual? (Fin.cast ⋯ (i.succAbove j)) = Option.map (Fin.cast ⋯ ∘ i.succAbove) (φsΛ.getDual? j)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Fin φs.lengthk:↥φsΛ.uncontractedhkj:j ≠ ↑k⊢ Option.map (⇑(finCongr ⋯) ∘ i.succAbove) (φsΛ.getDual? j) = Option.map (Fin.cast ⋯ ∘ i.succAbove) (φsΛ.getDual? j)
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Fin φs.length⊢ ¬((φsΛ↩Λφ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).isSome = true ↔ ¬(φsΛ.getDual? j).isSome = true
All goals completed! 🐙@[simp]
lemma insertAndContract_none_getDual?_get_eq (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length)
(h : ((φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).isSome) :
((φsΛ ↩Λ φ i none).getDual? (Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove j))).get h = Fin.cast (insertIdx_length_fin φ φs i).symm
(i.succAbove ((φsΛ.getDual? j).get (𝓕:FieldSpecificationn:ℕc:WickContraction nφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Fin φs.lengthh:((φsΛ↩Λφ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).isSome = true⊢ (φsΛ.getDual? j).isSome = true All goals completed! 🐙))) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:Fin φs.lengthh:((φsΛ↩Λφ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).isSome = true⊢ ((φsΛ↩Λφ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).get h = Fin.cast ⋯ (i.succAbove ((φsΛ.getDual? j).get ⋯))
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh:¬↑i < ↑(i.succAbove ↑j)⊢ ↑((finCongr ⋯) (i.succAbove ↑j)) < ↑((finCongr ⋯) i)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh:i.succAbove ↑j ≤ i⊢ i.succAbove ↑j < i
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh:i.succAbove ↑j ≤ ihi:i.succAbove ↑j ≠ i⊢ i.succAbove ↑j < i
All goals completed! 🐙𝓕:FieldSpecificationM:Type u_1φ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succf:↥↑(φsΛ↩Λφ i none) → Minst✝:CommMonoid Me1:↥↑φsΛ ≃ ↥↑(φsΛ.insertAndContractNat i none) := Equiv.ofBijective (insertLift i none) ⋯e2:↥↑(φsΛ.insertAndContractNat i none) ≃ ↥↑((congr ⋯) (φsΛ.insertAndContractNat i none)) := Equiv.ofBijective (congrLift ⋯) ⋯⊢ ∏ i_1, f (e2 (e1 i_1)) = ∏ a, f (congrLift ⋯ (insertLift i none a))
All goals completed! 🐙𝓕:FieldSpecificationM:Type u_1φ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedf:↥↑(φsΛ↩Λφ i some j) → Minst✝:CommMonoid Me2:↥↑(φsΛ.insertAndContractNat i (some j)) ≃ ↥↑((congr ⋯) (φsΛ.insertAndContractNat i (some j))) := Equiv.ofBijective (congrLift ⋯) ⋯e1:Unit ⊕ ↥↑φsΛ ≃ ↥↑(φsΛ.insertAndContractNat i (some j)) := Equiv.ofBijective (insertLiftSome i j) ⋯⊢ (∏ a₁, f (e2 (e1 (Sum.inl a₁)))) * ∏ a₂, f (e2 (e1 (Sum.inr a₂))) =
f (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩) * ∏ a, f (congrLift ⋯ (insertLift i (some j) a))
𝓕:FieldSpecificationM:Type u_1φ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedf:↥↑(φsΛ↩Λφ i some j) → Minst✝:CommMonoid Me2:↥↑(φsΛ.insertAndContractNat i (some j)) ≃ ↥↑((congr ⋯) (φsΛ.insertAndContractNat i (some j))) := Equiv.ofBijective (congrLift ⋯) ⋯e1:Unit ⊕ ↥↑φsΛ ≃ ↥↑(φsΛ.insertAndContractNat i (some j)) := Equiv.ofBijective (insertLiftSome i j) ⋯⊢ f (e2 (e1 (Sum.inl PUnit.unit))) * ∏ x ∈ (↑φsΛ).attach, f (e2 (e1 (Sum.inr x))) =
f (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩) * ∏ x ∈ (↑φsΛ).attach, f (congrLift ⋯ (insertLift i (some j) x))
All goals completed! 🐙
Given a finite set of Fin φs.length the finite set of (φs.insertIdx i φ).length
formed by mapping elements using i.succAboveEmb and finCongr.
def insertAndContractLiftFinset (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
(i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
Finset (Fin (φs.insertIdx i φ).length) :=
(a.map i.succAboveEmb).map (finCongr (insertIdx_length_fin φ φs i).symm).toEmbedding@[simp]
lemma self_not_mem_insertAndContractLiftFinset (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
(i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
Fin.cast (insertIdx_length_fin φ φs i).symm i ∉ insertAndContractLiftFinset φ i a := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)⊢ Fin.cast ⋯ i ∉ insertAndContractLiftFinset φ i a
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)⊢ i ∉ Finset.map i.succAboveEmb a
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)⊢ ∀ x ∈ a, ¬i.succAbove x = i
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)x:Fin φs.length⊢ x ∈ a → ¬i.succAbove x = i
All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)j:Fin φs.lengthx:Fin φs.lengthhx1:x ∈ ahx2:x = j⊢ j ∈ a
All goals completed! 🐙
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)j:Fin φs.length⊢ j ∈ a → ∃ a_2 ∈ a, i.succAbove a_2 = i.succAbove j 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succa:Finset (Fin φs.length)j:Fin φs.lengthh:j ∈ a⊢ ∃ a_1 ∈ a, i.succAbove a_1 = i.succAbove j
All goals completed! 🐙lemma insert_fin_eq_self (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
(i : Fin φs.length.succ) (j : Fin (List.insertIdx φs i φ).length) :
j = Fin.cast (insertIdx_length_fin φ φs i).symm i
∨ ∃ k, j = Fin.cast (insertIdx_length_fin φ φs i).symm (i.succAbove k) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succj:Fin (φs.insertIdx (↑i) φ).length⊢ j = Fin.cast ⋯ i ∨ ∃ k, j = Fin.cast ⋯ (i.succAbove k)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succj:Fin (φs.insertIdx (↑i) φ).lengthk:Fin φs.length.succhk:(finCongr ⋯) k = j⊢ j = Fin.cast ⋯ i ∨ ∃ k, j = Fin.cast ⋯ (i.succAbove k)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succ⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succhi:k = i⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succhi:¬k = i⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succhi:k = i⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1) All goals completed! 🐙
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succhi:¬k = i⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1) 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succhi:∃ z, i.succAbove z = k⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succk:Fin φs.length.succz:Fin φs.lengthhk:i.succAbove z = k⊢ (finCongr ⋯) k = Fin.cast ⋯ i ∨ ∃ k_1, (finCongr ⋯) k = Fin.cast ⋯ (i.succAbove k_1)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succz:Fin φs.length⊢ (finCongr ⋯) (i.succAbove z) = Fin.cast ⋯ i ∨ ∃ k, (finCongr ⋯) (i.succAbove z) = Fin.cast ⋯ (i.succAbove k)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succz:Fin φs.length⊢ ∃ k, (finCongr ⋯) (i.succAbove z) = Fin.cast ⋯ (i.succAbove k)
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succz:Fin φs.length⊢ (finCongr ⋯) (i.succAbove z) = Fin.cast ⋯ (i.succAbove z)
All goals completed! 🐙
For a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of
𝓕.FieldOp and a i ≤ φs.length then a sum over
Wick contractions of φs with φ inserted at i is equal to the sum over Wick contractions
φsΛ of just φs and the sum over optional uncontracted elements of the φsΛ.
In other words,
∑ (φsΛ : WickContraction (φs.insertIdx i φ).length), f φsΛ
where (φs.insertIdx i φ) is φs with φ inserted at position i. is equal to
∑ (φsΛ : WickContraction φs.length), ∑ k, f (φsΛ ↩Λ φ i k) .
where the sum over k is over all k in Option φsΛ.uncontracted.
𝓕:FieldSpecificationM:Type u_1φ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succinst✝:AddCommMonoid Mf:WickContraction (φs.insertIdx (↑i) φ).length → M⊢ ∑ c, ∑ k, f ((congr ⋯) ((extractEquiv ((finCongr ⋯) ((finCongr ⋯) i))).symm ⟨c, k⟩)) = ∑ φsΛ, ∑ k, f (φsΛ↩Λφ i k)
All goals completed! 🐙Uncontracted list
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (List.map (φs.insertIdx (↑i) φ).get
(List.map (⇑(finCongr ⋯)) (List.map (⇑i.succAboveEmb) φsΛ.uncontractedList))).insertIdx
(φsΛ.uncontractedListOrderPos i) ((φs.insertIdx (↑i) φ).get ((finCongr ⋯) i)) =
(List.map φs.get φsΛ.uncontractedList).insertIdx (φsΛ.uncontractedListOrderPos i) φ
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ List.map (φs.insertIdx (↑i) φ).get (List.map (⇑(finCongr ⋯)) (List.map (⇑i.succAboveEmb) φsΛ.uncontractedList)) =
List.map φs.get φsΛ.uncontractedList𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (φs.insertIdx (↑i) φ).get ((finCongr ⋯) i) = φ
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ List.map (φs.insertIdx (↑i) φ).get (List.map (⇑(finCongr ⋯)) (List.map (⇑i.succAboveEmb) φsΛ.uncontractedList)) =
List.map φs.get φsΛ.uncontractedList All goals completed! 🐙
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (φs.insertIdx (↑i) φ).get ((finCongr ⋯) i) = φ All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ [φsΛ]ᵘᶜ.insertIdx (φsΛ.uncontractedListOrderPos 0) φ = φ :: [φsΛ]ᵘᶜ
All goals completed! 🐙