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.ExtractEquivList of uncontracted elements of a Wick contraction
@[expose] public sectionSome properties of lists of fin
lemma fin_list_sorted_monotone_sorted {n m : ℕ} (l: List (Fin n)) (hl : l.Pairwise (· ≤ ·))
(f : Fin n → Fin m) (hf : StrictMono f) : (List.map f l).Pairwise (· ≤ ·) :=
hl.map f fun _ _ hab => hf.monotone hablemma fin_list_sorted_succAboveEmb_sorted (l: List (Fin n)) (hl : l.Pairwise (· ≤ ·))
(i : Fin n.succ) : ((List.map i.succAboveEmb l)).Pairwise (· ≤ ·) := n:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin n.succ⊢ List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.map (⇑i.succAboveEmb) l)
n:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin n.succ⊢ StrictMono ⇑i.succAboveEmb
All goals completed! 🐙n:ℕm:ℕa:Finset (Fin n)f:Fin n ↪ Fin mhf:StrictMono ⇑fh1:List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.map (⇑f) (a.sort fun x1 x2 => x1 ≤ x2))h2:(List.map (⇑f) (a.sort fun x1 x2 => x1 ≤ x2)).Noduph3:(List.map (⇑f) (a.sort fun x1 x2 => x1 ≤ x2)).toFinset = Finset.map f a⊢ List.map (⇑f) (a.sort fun x1 x2 => x1 ≤ x2) =
(List.map (⇑f) (a.sort fun x1 x2 => x1 ≤ x2)).toFinset.sort fun x1 x2 => x1 ≤ x2
All goals completed! 🐙n:ℕa:Fin nl:List (Fin n)i:ℕhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬↑a < ihx✝:List.filter (fun x => decide (↑x < i)) (a :: l) = []hl':l = List.filter (fun x => decide (↑x < i)) l ++ List.filter (fun x => decide (i ≤ ↑x)) lhx:List.filter (fun x => decide (↑x < i)) l = []⊢ l = List.filter (fun x => decide (i ≤ ↑x)) ln:ℕa:Fin nl:List (Fin n)i:ℕhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬↑a < ihx:List.filter (fun x => decide (↑x < i)) (a :: l) = []⊢ decide (i ≤ ↑a) = true
n:ℕa:Fin nl:List (Fin n)i:ℕhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬↑a < ihx✝:List.filter (fun x => decide (↑x < i)) (a :: l) = []hx:List.filter (fun x => decide (↑x < i)) l = []hl':l = List.filter (fun x => decide (i ≤ ↑x)) l⊢ l = List.filter (fun x => decide (i ≤ ↑x)) ln:ℕa:Fin nl:List (Fin n)i:ℕhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬↑a < ihx:List.filter (fun x => decide (↑x < i)) (a :: l) = []⊢ decide (i ≤ ↑a) = true
conv_lhs => n:ℕa:Fin nl:List (Fin n)i:ℕhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬↑a < ihx✝:List.filter (fun x => decide (↑x < i)) (a :: l) = []hx:List.filter (fun x => decide (↑x < i)) l = []hl':l = List.filter (fun x => decide (i ≤ ↑x)) l| List.filter (fun x => decide (i ≤ ↑x)) l
n:ℕa:Fin nl:List (Fin n)i:ℕhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬↑a < ihx:List.filter (fun x => decide (↑x < i)) (a :: l) = []⊢ i ≤ ↑a
All goals completed! 🐙n:ℕa:Fin nl:List (Fin n)i:Fin nhi:i ∈ a :: lhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:a < i⊢ i ∈ l
n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:a < ihi:i = a ∨ i ∈ l⊢ i ∈ l
n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:a < ihi:i = a⊢ i ∈ ln:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:a < ihi:i ∈ l⊢ i ∈ l
n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:a < ihi:i = a⊢ i ∈ l All goals completed! 🐙
n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:a < ihi:i ∈ l⊢ i ∈ l All goals completed! 🐙n:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nhi:i ∈ l⊢ (List.filter (fun x => decide (↑x < ↑i)) l).length + List.idxOf i (List.filter (fun x => decide (↑i ≤ ↑x)) l) =
(List.filter (fun x => decide (↑x < ↑i)) l).lengthn:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nhi:i ∈ l⊢ i ∉ List.filter (fun x => decide (↑x < ↑i)) l
n:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nhi:i ∈ l⊢ (List.filter (fun x => decide (↑x < ↑i)) l).length + List.idxOf i (List.filter (fun x => decide (↑i ≤ ↑x)) l) =
(List.filter (fun x => decide (↑x < ↑i)) l).length erw [n:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nhi:i ∈ l⊢ (List.filter (fun x => decide (↑x < ↑i)) l).length + 0 = (List.filter (fun x => decide (↑x < ↑i)) l).lengthn:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nhi:i ∈ l⊢ (List.filter (fun x => decide (↑x < ↑i)) l).length + 0 = (List.filter (fun x => decide (↑x < ↑i)) l).length
All goals completed! 🐙
n:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nhi:i ∈ l⊢ i ∉ List.filter (fun x => decide (↑x < ↑i)) l All goals completed! 🐙n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬i ≤ a⊢ a :: (List.filter (fun x => decide (↑x < ↑i)) l ++ i :: List.filter (fun x => decide (↑i ≤ ↑x)) l) =
a :: List.filter (fun x => decide (x < i)) l ++ i :: List.filter (fun x => decide (i ≤ x)) ln:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬i ≤ a⊢ decide (a < i) = true
n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬i ≤ a⊢ decide (a < i) = true
n:ℕa:Fin nl:List (Fin n)i:Fin nhl:(∀ a' ∈ l, a ≤ a') ∧ List.Pairwise (fun x1 x2 => x1 ≤ x2) lha:¬i ≤ a⊢ a < i
All goals completed! 🐙n✝:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nn:Fin l.length.succ := ⟨(List.filter (fun x => decide (x < i)) l).length, ⋯⟩⊢ List.filter (fun x => decide (↑x < ↑i)) l ++ i :: List.filter (fun x => decide (↑i ≤ ↑x)) l =
List.take (↑n) l ++ i :: List.drop (↑n) l
n✝:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nn:Fin l.length.succ := ⟨(List.filter (fun x => decide (x < i)) l).length, ⋯⟩⊢ List.filter (fun x => decide (↑x < ↑i)) l = List.take (↑n) ln✝:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nn:Fin l.length.succ := ⟨(List.filter (fun x => decide (x < i)) l).length, ⋯⟩⊢ List.filter (fun x => decide (↑i ≤ ↑x)) l = List.drop (↑n) l
all_goals
conv_rhs =>
n✝:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nn:Fin l.length.succ := ⟨(List.filter (fun x => decide (x < i)) l).length, ⋯⟩| l
n✝:ℕl:List (Fin n)hl:List.Pairwise (fun x1 x2 => x1 ≤ x2) li:Fin nn:Fin l.length.succ := ⟨(List.filter (fun x => decide (x < i)) l).length, ⋯⟩| List.filter (fun x => decide (↑x < ↑i)) l ++ List.filter (fun x => decide (↑i ≤ ↑x)) l
All goals completed! 🐙Uncontracted List
Given a Wick contraction c, the ordered list of elements of Fin n which are not contracted,
i.e. do not appear anywhere in c.1.
def uncontractedList : List (Fin n) := List.filter (fun x => x ∈ c.uncontracted) (List.finRange n)lemma uncontractedList_mem_iff (i : Fin n) :
i ∈ c.uncontractedList ↔ i ∈ c.uncontracted := n:ℕc:WickContraction ni:Fin n⊢ i ∈ c.uncontractedList ↔ i ∈ c.uncontracted
All goals completed! 🐙@[simp]
lemma uncontractedList_empty : (empty (n := n)).uncontractedList = List.finRange n := n:ℕ⊢ empty.uncontractedList = List.finRange n
All goals completed! 🐙lemma nil_zero_uncontractedList : (empty (n := 0)).uncontractedList = [] := ⊢ empty.uncontractedList = []
All goals completed! 🐙lemma congr_uncontractedList {n m : ℕ} (h : n = m) (c : WickContraction n) :
((congr h) c).uncontractedList = List.map (finCongr h) c.uncontractedList := n:ℕm:ℕh:n = mc:WickContraction n⊢ ((congr h) c).uncontractedList = List.map (⇑(finCongr h)) c.uncontractedList
n:ℕc:WickContraction n⊢ ((congr ⋯) c).uncontractedList = List.map (⇑(finCongr ⋯)) c.uncontractedList
All goals completed! 🐙lemma uncontractedList_get_mem_uncontracted (i : Fin c.uncontractedList.length) :
c.uncontractedList.get i ∈ c.uncontracted := n:ℕc:WickContraction ni:Fin c.uncontractedList.length⊢ c.uncontractedList.get i ∈ c.uncontracted
All goals completed! 🐙n:ℕc:WickContraction n⊢ List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.ofFn id)
All goals completed! 🐙n:ℕc:WickContraction n⊢ List.Pairwise (fun x1 x2 => x1 < x2) (List.ofFn id)
All goals completed! 🐙n:ℕc:WickContraction n⊢ (List.filter (fun x => decide (x ∈ c.uncontracted)) (List.finRange n)).Nodup
All goals completed! 🐙lemma uncontractedList_toFinset (c : WickContraction n) :
c.uncontractedList.toFinset = c.uncontracted := n:ℕc:WickContraction n⊢ c.uncontractedList.toFinset = c.uncontracted
All goals completed! 🐙n:ℕc:WickContraction n⊢ (c.uncontractedList.toFinset.sort fun x1 x2 => x1 ≤ x2) = c.uncontractedList
All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙uncontractedIndexEquiv
The equivalence between the positions of c.uncontractedList i.e. elements of
Fin (c.uncontractedList).length and the finite set c.uncontracted considered as a finite type.
def uncontractedIndexEquiv (c : WickContraction n) :
Fin (c.uncontractedList).length ≃ c.uncontracted where
toFun i := ⟨c.uncontractedList.get i, c.uncontractedList_get_mem_uncontracted i⟩
invFun i := ⟨List.idxOf i.1 c.uncontractedList,
List.idxOf_lt_length_iff.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩
left_inv i := 𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin c.uncontractedList.length⊢ (fun i => ⟨List.idxOf (↑i) c.uncontractedList, ⋯⟩) ((fun i => ⟨c.uncontractedList.get i, ⋯⟩) i) = i
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:Fin c.uncontractedList.length⊢ ↑((fun i => ⟨List.idxOf (↑i) c.uncontractedList, ⋯⟩) ((fun i => ⟨c.uncontractedList.get i, ⋯⟩) i)) = ↑i
All goals completed! 🐙
right_inv i := 𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:↥c.uncontracted⊢ (fun i => ⟨c.uncontractedList.get i, ⋯⟩) ((fun i => ⟨List.idxOf (↑i) c.uncontractedList, ⋯⟩) i) = i
𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:WickContraction ni:↥c.uncontracted⊢ ↑↑((fun i => ⟨c.uncontractedList.get i, ⋯⟩) ((fun i => ⟨List.idxOf (↑i) c.uncontractedList, ⋯⟩) i)) = ↑↑i
All goals completed! 🐙@[simp]
lemma uncontractedList_getElem_uncontractedIndexEquiv_symm (k : c.uncontracted) :
c.uncontractedList[(c.uncontractedIndexEquiv.symm k).val] = k := n:ℕc:WickContraction nk:↥c.uncontracted⊢ c.uncontractedList[↑(c.uncontractedIndexEquiv.symm k)] = ↑k
All goals completed! 🐙n:ℕc:WickContraction nk:↥c.uncontracted⊢ (List.filter (fun x => decide (↑x < ↑↑k)) c.uncontractedList).length =
(List.filter (fun i => decide (i < ↑k)) c.uncontractedList).length
All goals completed! 🐙n:ℕc:WickContraction nk:↥c.uncontracted⊢ List.take (List.filter (fun i => decide (i < ↑k)) c.uncontractedList).length
(List.filter (fun x => decide (↑x < ↑↑k)) c.uncontractedList ++
List.filter (fun x => decide (↑↑k ≤ ↑x)) c.uncontractedList) =
List.filter (fun i => decide (i < ↑k)) c.uncontractedList
All goals completed! 🐙Uncontracted List get
Given a Wick Contraction φsΛ of a list φs of 𝓕.FieldOp. The list
φsΛ.uncontractedListGet of 𝓕.FieldOp is defined as the list φs with
all contracted positions removed, leaving the uncontracted 𝓕.FieldOp.
The notation [φsΛ]ᵘᶜ is used for φsΛ.uncontractedListGet.
def uncontractedListGet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) :
List 𝓕.FieldOp := φsΛ.uncontractedList.map φs.get@[inherit_doc uncontractedListGet]
scoped[WickContraction] notation "[" φsΛ "]ᵘᶜ" => uncontractedListGet φsΛ@[simp]
lemma uncontractedListGet_empty {φs : List 𝓕.FieldOp} :
(empty (n := φs.length)).uncontractedListGet = φs := 𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ [empty]ᵘᶜ = φs
All goals completed! 🐙uncontractedFieldOpEquiv
The equivalence between the type Option c.uncontracted for WickContraction φs.length and
Option (Fin (c.uncontractedList.map φs.get).length), that is optional positions of
c.uncontractedList.map φs.get induced by uncontractedIndexEquiv.
def uncontractedFieldOpEquiv (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :
Option φsΛ.uncontracted ≃ Option (Fin [φsΛ]ᵘᶜ.length) :=
Equiv.optionCongr (φsΛ.uncontractedIndexEquiv.symm.trans
(finCongr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ φsΛ.uncontractedList.length = [φsΛ]ᵘᶜ.length All goals completed! 🐙)))@[simp]
lemma uncontractedFieldOpEquiv_none (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :
(uncontractedFieldOpEquiv φs φsΛ).toFun none = none := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ (uncontractedFieldOpEquiv φs φsΛ).toFun none = none
All goals completed! 🐙All goals completed! 🐙uncontractedListEmd
The embedding of Fin [φsΛ]ᵘᶜ.length into Fin φs.length.
def uncontractedListEmd {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} :
Fin [φsΛ]ᵘᶜ.length ↪ Fin φs.length := ((finCongr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ [φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.length All goals completed! 🐙)).trans
φsΛ.uncontractedIndexEquiv).toEmbedding.trans
(Function.Embedding.subtype fun x => x ∈ φsΛ.uncontracted)lemma uncontractedListEmd_congr {φs : List 𝓕.FieldOp} {φsΛ φsΛ' : WickContraction φs.length}
(h : φsΛ = φsΛ') : φsΛ.uncontractedListEmd =
(finCongr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsΛ':WickContraction φs.lengthh:φsΛ = φsΛ'⊢ [φsΛ]ᵘᶜ.length = [φsΛ']ᵘᶜ.length All goals completed! 🐙)).toEmbedding.trans φsΛ'.uncontractedListEmd := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsΛ':WickContraction φs.lengthh:φsΛ = φsΛ'⊢ uncontractedListEmd = (finCongr ⋯).toEmbedding.trans uncontractedListEmd
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ uncontractedListEmd = (finCongr ⋯).toEmbedding.trans uncontractedListEmd
All goals completed! 🐙lemma uncontractedListEmd_toFun_eq_get (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :
(uncontractedListEmd (φsΛ := φsΛ)).toFun =
φsΛ.uncontractedList.get ∘ (finCongr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ [φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.length All goals completed! 🐙)) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ uncontractedListEmd.toFun = φsΛ.uncontractedList.get ∘ ⇑(finCongr ⋯)
All goals completed! 🐙lemma uncontractedListEmd_strictMono {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length}
{i j : Fin [φsΛ]ᵘᶜ.length} (h : i < j) : uncontractedListEmd i < uncontractedListEmd j := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengthh:i < j⊢ uncontractedListEmd i < uncontractedListEmd j
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengthh:i < j⊢ φsΛ.uncontractedList[↑i] < φsΛ.uncontractedList[↑j]
All goals completed! 🐙lemma uncontractedListEmd_mem_uncontracted {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length}
(i : Fin [φsΛ]ᵘᶜ.length) : uncontractedListEmd i ∈ φsΛ.uncontracted := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin [φsΛ]ᵘᶜ.length⊢ uncontractedListEmd i ∈ φsΛ.uncontracted
All goals completed! 🐙lemma uncontractedListEmd_surjective_mem_uncontracted {φs : List 𝓕.FieldOp}
{φsΛ : WickContraction φs.length} (i : Fin φs.length) (hi : i ∈ φsΛ.uncontracted) :
∃ j, φsΛ.uncontractedListEmd j = i := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontracted⊢ ∃ j, uncontractedListEmd j = i
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontracted⊢ ∃ j, ↑(φsΛ.uncontractedIndexEquiv (Fin.cast ⋯ j)) = i
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontractedhj:∃ j, φsΛ.uncontractedIndexEquiv j = ⟨i, hi⟩⊢ ∃ j, ↑(φsΛ.uncontractedIndexEquiv (Fin.cast ⋯ j)) = i
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontractedhj:∃ j, φsΛ.uncontractedIndexEquiv j = ⟨i, hi⟩h1:[φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.length⊢ ∃ j, ↑(φsΛ.uncontractedIndexEquiv (Fin.cast h1 j)) = i
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontractedh1:[φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.lengthj:Fin φsΛ.uncontractedList.lengthhj:φsΛ.uncontractedIndexEquiv j = ⟨i, hi⟩⊢ ∃ j, ↑(φsΛ.uncontractedIndexEquiv (Fin.cast h1 j)) = i
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontractedh1:[φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.lengthj':Fin [φsΛ]ᵘᶜ.lengthhj:φsΛ.uncontractedIndexEquiv ((finCongr h1) j') = ⟨i, hi⟩⊢ ∃ j, ↑(φsΛ.uncontractedIndexEquiv (Fin.cast h1 j)) = i
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontractedh1:[φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.lengthj':Fin [φsΛ]ᵘᶜ.lengthhj:φsΛ.uncontractedIndexEquiv ((finCongr h1) j') = ⟨i, hi⟩⊢ ↑(φsΛ.uncontractedIndexEquiv (Fin.cast h1 j')) = i
erw [𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthhi:i ∈ φsΛ.uncontractedh1:[φsΛ]ᵘᶜ.length = φsΛ.uncontractedList.lengthj':Fin [φsΛ]ᵘᶜ.lengthhj:φsΛ.uncontractedIndexEquiv ((finCongr h1) j') = ⟨i, hi⟩⊢ ↑⟨i, hi⟩ = iAll goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)b:Finset (Fin φs.length)hb:b ∈ ↑φsΛx:Fin [φsΛ]ᵘᶜ.lengthhx:x ∈ ah1:∀ p ∈ ↑φsΛ, uncontractedListEmd x ∉ p⊢ uncontractedListEmd x ∉ b
All goals completed! 🐙lemma uncontractedListEmd_finset_not_mem {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length}
(a : Finset (Fin [φsΛ]ᵘᶜ.length)) :
a.map uncontractedListEmd ∉ φsΛ.1 := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)⊢ Finset.map uncontractedListEmd a ∉ ↑φsΛ
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)hn:Finset.map uncontractedListEmd a ∈ ↑φsΛ⊢ False
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)hn:Finset.map uncontractedListEmd a ∈ ↑φsΛh1:Disjoint (Finset.map uncontractedListEmd a) (Finset.map uncontractedListEmd a)⊢ False
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)hn:Finset.map uncontractedListEmd a ∈ ↑φsΛh1:a = ∅⊢ False
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)hn:Finset.map uncontractedListEmd a ∈ ↑φsΛh1:a = ∅h2:(Finset.map uncontractedListEmd a).card = 2⊢ False
All goals completed! 🐙@[simp]
lemma getElem_uncontractedListEmd {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length}
(k : Fin [φsΛ]ᵘᶜ.length) : φs[(uncontractedListEmd k).1] = [φsΛ]ᵘᶜ[k.1] := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthk:Fin [φsΛ]ᵘᶜ.length⊢ φs[↑(uncontractedListEmd k)] = [φsΛ]ᵘᶜ[↑k]
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthk:Fin [φsΛ]ᵘᶜ.length⊢ φs[↑(uncontractedListEmd k)] = φs[↑φsΛ.uncontractedList[↑k]]
All goals completed! 🐙@[simp]
lemma uncontractedListEmd_empty {φs : List 𝓕.FieldOp} :
(empty (n := φs.length)).uncontractedListEmd = (finCongr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOp⊢ [empty]ᵘᶜ.length = φs.length All goals completed! 🐙)).toEmbedding := 𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ uncontractedListEmd = (finCongr ⋯).toEmbedding
𝓕:FieldSpecificationφs:List 𝓕.FieldOpx:Fin [empty]ᵘᶜ.length⊢ ↑(uncontractedListEmd x) = ↑((finCongr ⋯).toEmbedding x)
All goals completed! 🐙Uncontracted List for extractEquiv symm none
lemma uncontractedList_succAboveEmb_sorted (c : WickContraction n) (i : Fin n.succ) :
((List.map i.succAboveEmb c.uncontractedList)).Pairwise (· ≤ ·) := n:ℕc:WickContraction ni:Fin n.succ⊢ List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.map (⇑i.succAboveEmb) c.uncontractedList)
All goals completed! 🐙lemma uncontractedList_succAboveEmb_nodup (c : WickContraction n) (i : Fin n.succ) :
((List.map i.succAboveEmb c.uncontractedList)).Nodup := n:ℕc:WickContraction ni:Fin n.succ⊢ (List.map (⇑i.succAboveEmb) c.uncontractedList).Nodup
All goals completed! 🐙lemma uncontractedList_succAbove_orderedInsert_nodup (c : WickContraction n) (i : Fin n.succ) :
(List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).Nodup := n:ℕc:WickContraction ni:Fin n.succ⊢ (List.orderedInsert (fun x1 x2 => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList)).Nodup
n:ℕc:WickContraction ni:Fin n.succ⊢ (i :: List.map (⇑i.succAboveEmb) c.uncontractedList).Nodup
n:ℕc:WickContraction ni:Fin n.succ⊢ (∀ x ∈ c.uncontractedList, ¬i.succAboveEmb x = i) ∧ (List.map (⇑i.succAboveEmb) c.uncontractedList).Nodup
All goals completed! 🐙lemma uncontractedList_succAbove_orderedInsert_sorted (c : WickContraction n) (i : Fin n.succ) :
(List.orderedInsert (· ≤ ·) i
(List.map i.succAboveEmb c.uncontractedList)).Pairwise (· ≤ ·) := n:ℕc:WickContraction ni:Fin n.succ⊢ List.Pairwise (fun x1 x2 => x1 ≤ x2)
(List.orderedInsert (fun x1 x2 => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList))
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succa:Fin n.succ⊢ a ∈ (List.orderedInsert (fun x1 x2 => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList)).toFinset ↔
a ∈ insert i (Finset.map i.succAboveEmb c.uncontractedList.toFinset)
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succ⊢ List.orderedInsert (fun x1 x2 => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList) =
(List.orderedInsert (fun x1 x2 => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList)).toFinset.sort
fun x1 x2 => x1 ≤ x2
All goals completed! 🐙All goals completed! 🐙Uncontracted List for extractEquiv symm some
n:ℕc:WickContraction ni:Fin n.succk:ℕhk:k < c.uncontractedList.lengtha:Fin (n + 1)⊢ a ∈ List.map i.succAbove c.uncontractedList ∧ a ≠ (List.map i.succAbove c.uncontractedList)[k] ↔
¬a = i.succAbove c.uncontractedList[k] ∧ ∃ a_1 ∈ c.uncontracted, i.succAbove a_1 = an:ℕc:WickContraction ni:Fin n.succk:ℕhk:k < c.uncontractedList.lengtha:Fin (n + 1)⊢ (List.map i.succAbove c.uncontractedList).Nodup
n:ℕc:WickContraction ni:Fin n.succk:ℕhk:k < c.uncontractedList.lengtha:Fin (n + 1)⊢ a ∈ List.map i.succAbove c.uncontractedList ∧ a ≠ (List.map i.succAbove c.uncontractedList)[k] ↔
¬a = i.succAbove c.uncontractedList[k] ∧ ∃ a_1 ∈ c.uncontracted, i.succAbove a_1 = a n:ℕc:WickContraction ni:Fin n.succk:ℕhk:k < c.uncontractedList.lengtha:Fin (n + 1)⊢ (∃ a_1 ∈ c.uncontracted, i.succAbove a_1 = a) ∧ ¬a = i.succAbove c.uncontractedList[k] ↔
¬a = i.succAbove c.uncontractedList[k] ∧ ∃ a_1 ∈ c.uncontracted, i.succAbove a_1 = a
All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succk:ℕhk:k < c.uncontractedList.lengtha:Fin (n + 1)⊢ (List.map i.succAbove c.uncontractedList).Nodup All goals completed! 🐙lemma uncontractedList_succAboveEmb_eraseIdx_sorted (c : WickContraction n) (i : Fin n.succ)
(k: ℕ) : ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Pairwise (· ≤ ·) := n:ℕc:WickContraction ni:Fin n.succk:ℕ⊢ List.Pairwise (fun x1 x2 => x1 ≤ x2) ((List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k)
n:ℕc:WickContraction ni:Fin n.succk:ℕ⊢ List.Pairwise (fun x1 x2 => x1 ≤ x2) (List.map (⇑i.succAboveEmb) c.uncontractedList)
All goals completed! 🐙lemma uncontractedList_succAboveEmb_eraseIdx_nodup (c : WickContraction n) (i : Fin n.succ) (k: ℕ) :
((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Nodup := n:ℕc:WickContraction ni:Fin n.succk:ℕ⊢ ((List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k).Nodup
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succk:ℕhk:k < c.uncontractedList.length⊢ (List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k =
((List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k).toFinset.sort fun x1 x2 => x1 ≤ x2
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succk:↥c.uncontracted⊢ Finset.map i.succAboveEmb (c.uncontracted.erase ↑k) = (Finset.map i.succAboveEmb c.uncontracted).erase (i.succAbove ↑k)
n:ℕc:WickContraction ni:Fin n.succk:↥c.uncontracteda:Fin (n + 1)⊢ a ∈ Finset.map i.succAboveEmb (c.uncontracted.erase ↑k) ↔
a ∈ (Finset.map i.succAboveEmb c.uncontracted).erase (i.succAbove ↑k)
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succa:Fin (n + 1)⊢ a ∈ (List.map (⇑i.succAboveEmb) c.uncontractedList).toFinset ↔ a ∈ Finset.map i.succAboveEmb c.uncontractedList.toFinset
All goals completed! 🐙uncontractedListOrderPos
Given a Wick contraction c : WickContraction n and a Fin n.succ, the number of elements
of c.uncontractedList which are less than i.
Suppose we want to insert into c at position i, then this is the position we would
need to insert into c.uncontractedList.
def uncontractedListOrderPos (c : WickContraction n) (i : Fin n.succ) : ℕ :=
(List.filter (fun x => x.1 < i.1) c.uncontractedList).length@[simp]
lemma uncontractedListOrderPos_le_length (c : WickContraction n) (i : Fin n.succ) :
c.uncontractedListOrderPos i ≤ c.uncontractedList.length := n:ℕc:WickContraction ni:Fin n.succ⊢ c.uncontractedListOrderPos i ≤ c.uncontractedList.length
All goals completed! 🐙lemma take_uncontractedListOrderPos_eq_filter (c : WickContraction n) (i : Fin n.succ) :
(c.uncontractedList.take (c.uncontractedListOrderPos i)) =
c.uncontractedList.filter (fun x => x.1 < i.1) := n:ℕc:WickContraction ni:Fin n.succ⊢ List.take (c.uncontractedListOrderPos i) c.uncontractedList = List.filter (fun x => decide (↑x < ↑i)) c.uncontractedList
n:ℕc:WickContraction ni:Fin n.succ⊢ List.take (c.uncontractedListOrderPos i)
(List.filter (fun x => decide (↑x < ↑i)) c.uncontractedList ++
List.filter (fun x => decide (↑i ≤ ↑x)) c.uncontractedList) =
List.filter (fun x => decide (↑x < ↑i)) c.uncontractedList
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succ⊢ List.filter (fun x => decide (↑x < ↑i)) c.uncontractedList = {x ∈ c.uncontracted | ↑x < ↑i}.sort fun x1 x2 => x1 ≤ x2
All goals completed! 🐙n:ℕc:WickContraction ni:Fin n.succ⊢ (List.map i.succAbove (List.filter ((fun x => decide (x < i)) ∘ i.succAbove) c.uncontractedList)).length =
(List.filter (fun x => decide (↑x < ↑i)) c.uncontractedList).length
n:ℕc:WickContraction ni:Fin n.succ⊢ (List.filter ((fun x => decide (x < i)) ∘ i.succAbove) c.uncontractedList).length =
(List.filter (fun x => decide (↑x < ↑i)) c.uncontractedList).length
n:ℕc:WickContraction ni:Fin n.succ⊢ (fun x => decide (x < i)) ∘ i.succAbove = fun x => decide (↑x < ↑i)
n:ℕc:WickContraction ni:Fin n.succx:Fin n⊢ ((fun x => decide (x < i)) ∘ i.succAbove) x = decide (↑x < ↑i)
n:ℕc:WickContraction ni:Fin n.succx:Fin n⊢ (if x.castSucc < i then x.castSucc else x.succ) < i ↔ ↑x < ↑i
n:ℕc:WickContraction ni:Fin n.succx:Fin nh✝:x.castSucc < i⊢ x.castSucc < i ↔ ↑x < ↑in:ℕc:WickContraction ni:Fin n.succx:Fin nh✝:¬x.castSucc < i⊢ x.succ < i ↔ ↑x < ↑i
n:ℕc:WickContraction ni:Fin n.succx:Fin nh✝:x.castSucc < i⊢ x.castSucc < i ↔ ↑x < ↑i All goals completed! 🐙
n:ℕc:WickContraction ni:Fin n.succx:Fin nh✝:¬x.castSucc < i⊢ x.succ < i ↔ ↑x < ↑i n:ℕc:WickContraction ni:Fin n.succx:Fin nh:¬x.castSucc < i⊢ x.succ < i ↔ ↑x < ↑i
n:ℕc:WickContraction ni:Fin n.succx:Fin nh:↑i ≤ ↑x⊢ ↑x + 1 < ↑i ↔ ↑x < ↑i
All goals completed! 🐙