List of uncontracted elements of a Wick contraction

Some properties of lists of fin

theorem WickContraction.fin_list_sorted_monotone_sorted {n m : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (f : Fin n → Fin m) (hf : StrictMono f) : List.Sorted (fun (x1 x2 : Fin m) => x1 ≤ x2) (List.map f l)

theorem WickContraction.fin_list_sorted_succAboveEmb_sorted {n : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (i : Fin n.succ) : List.Sorted (fun (x1 x2 : Fin (n + 1)) => x1 ≤ x2) (List.map (⇑i.succAboveEmb) l)

theorem WickContraction.fin_finset_sort_map_monotone {n m : ℕ} (a : Finset (Fin n)) (f : Fin n ↪ Fin m) (hf : StrictMono ⇑f) : List.map (⇑f) (Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) a) = Finset.sort (fun (x1 x2 : Fin m) => x1 ≤ x2) (Finset.map f a)

theorem WickContraction.fin_list_sorted_split {n : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (i : ℕ) : l = List.filter (fun (x : Fin n) => decide (↑x < i)) l ++ List.filter (fun (x : Fin n) => decide (i ≤ ↑x)) l

theorem WickContraction.fin_list_sorted_indexOf_filter_le_mem {n : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (i : Fin n) : i ∈ l → List.idxOf i (List.filter (fun (x : Fin n) => decide (i ≤ x)) l) = 0

theorem WickContraction.fin_list_sorted_indexOf_mem {n : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (i : Fin n) (hi : i ∈ l) : List.idxOf i l = (List.filter (fun (x : Fin n) => decide (↑x < ↑i)) l).length

theorem WickContraction.orderedInsert_of_fin_list_sorted {n : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (i : Fin n) : List.orderedInsert (fun (x1 x2 : Fin n) => x1 ≤ x2) i l = List.filter (fun (x : Fin n) => decide (↑x < ↑i)) l ++ i :: List.filter (fun (x : Fin n) => decide (↑i ≤ ↑x)) l

theorem WickContraction.orderedInsert_eq_insertIdx_of_fin_list_sorted {n : ℕ} (l : List (Fin n)) (hl : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) l) (i : Fin n) : List.orderedInsert (fun (x1 x2 : Fin n) => x1 ≤ x2) i l = List.insertIdx (List.filter (fun (x : Fin n) => decide (↑x < ↑i)) l).length i l

Uncontracted List

def WickContraction.uncontractedList {n : ℕ} (c : WickContraction n) : List (Fin n)

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.

Equations

• c.uncontractedList = List.filter (fun (x : Fin n) => decide (x ∈ c.uncontracted)) (List.finRange n)

theorem WickContraction.uncontractedList_mem_iff {n : ℕ} (c : WickContraction n) (i : Fin n) : i ∈ c.uncontractedList ↔ i ∈ c.uncontracted

@[simp]

theorem WickContraction.uncontractedList_empty {n : ℕ} : empty.uncontractedList = List.finRange n

theorem WickContraction.nil_zero_uncontractedList : empty.uncontractedList = []

theorem WickContraction.congr_uncontractedList {n m : ℕ} (h : n = m) (c : WickContraction n) : ((congr h) c).uncontractedList = List.map (⇑(finCongr h)) c.uncontractedList

theorem WickContraction.uncontractedList_get_mem_uncontracted {n : ℕ} (c : WickContraction n) (i : Fin c.uncontractedList.length) : c.uncontractedList.get i ∈ c.uncontracted

theorem WickContraction.uncontractedList_sorted {n : ℕ} (c : WickContraction n) : List.Sorted (fun (x1 x2 : Fin n) => x1 ≤ x2) c.uncontractedList

theorem WickContraction.uncontractedList_sorted_lt {n : ℕ} (c : WickContraction n) : List.Sorted (fun (x1 x2 : Fin n) => x1 < x2) c.uncontractedList

theorem WickContraction.uncontractedList_nodup {n : ℕ} (c : WickContraction n) : c.uncontractedList.Nodup

theorem WickContraction.uncontractedList_toFinset {n : ℕ} (c : WickContraction n) : c.uncontractedList.toFinset = c.uncontracted

theorem WickContraction.uncontractedList_eq_sort {n : ℕ} (c : WickContraction n) : c.uncontractedList = Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) c.uncontracted

theorem WickContraction.uncontractedList_length_eq_card {n : ℕ} (c : WickContraction n) : c.uncontractedList.length = c.uncontracted.card

theorem WickContraction.filter_uncontractedList {n : ℕ} (c : WickContraction n) (p : Fin n → Prop) [DecidablePred p] : List.filter (fun (b : Fin n) => decide (p b)) c.uncontractedList = Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) (Finset.filter p c.uncontracted)

uncontractedIndexEquiv

def WickContraction.uncontractedIndexEquiv {n : ℕ} (c : WickContraction n) : Fin c.uncontractedList.length ≃ { x : Fin n // x ∈ c.uncontracted }

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.

Equations

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

@[simp]

theorem WickContraction.uncontractedList_getElem_uncontractedIndexEquiv_symm {n : ℕ} (c : WickContraction n) (k : { x : Fin n // x ∈ c.uncontracted }) : c.uncontractedList[↑(c.uncontractedIndexEquiv.symm k)] = ↑k

theorem WickContraction.uncontractedIndexEquiv_symm_eq_filter_length {n : ℕ} (c : WickContraction n) (k : { x : Fin n // x ∈ c.uncontracted }) : ↑(c.uncontractedIndexEquiv.symm k) = (List.filter (fun (i : Fin n) => decide (i < ↑k)) c.uncontractedList).length

theorem WickContraction.take_uncontractedIndexEquiv_symm {n : ℕ} (c : WickContraction n) (k : { x : Fin n // x ∈ c.uncontracted }) : List.take (↑(c.uncontractedIndexEquiv.symm k)) c.uncontractedList = List.filter (fun (i : Fin n) => decide (i < ↑k)) c.uncontractedList

Uncontracted List get

def WickContraction.uncontractedListGet {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : List 𝓕.FieldOp

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.

Equations

• φsΛ.uncontractedListGet = List.map φs.get φsΛ.uncontractedList

def WickContraction.«term[_]ᵘᶜ» : Lean.ParserDescr

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.

Equations

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

@[simp]

theorem WickContraction.uncontractedListGet_empty {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} : empty.uncontractedListGet = φs

uncontractedFieldOpEquiv

def WickContraction.uncontractedFieldOpEquiv {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted } ≃ Option (Fin φsΛ.uncontractedListGet.length)

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.

Equations

• WickContraction.uncontractedFieldOpEquiv φs φsΛ = (φsΛ.uncontractedIndexEquiv.symm.trans (finCongr ⋯)).optionCongr

@[simp]

theorem WickContraction.uncontractedFieldOpEquiv_none {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : (uncontractedFieldOpEquiv φs φsΛ).toFun none = none

theorem WickContraction.uncontractedFieldOpEquiv_list_sum {𝓕 : FieldSpecification} {α : Type u_1} [AddCommMonoid α] (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (f : Option (Fin φsΛ.uncontractedListGet.length) → α) : ∑ i : Option (Fin φsΛ.uncontractedListGet.length), f i = ∑ i : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted }, f ((uncontractedFieldOpEquiv φs φsΛ) i)

uncontractedListEmd

def WickContraction.uncontractedListEmd {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} : Fin φsΛ.uncontractedListGet.length ↪ Fin φs.length

The embedding of Fin [φsΛ]ᵘᶜ.length into Fin φs.length.

Equations

• WickContraction.uncontractedListEmd = ((finCongr ⋯).trans φsΛ.uncontractedIndexEquiv).toEmbedding.trans (Function.Embedding.subtype fun (x : Fin φs.length) => x ∈ φsΛ.uncontracted)

theorem WickContraction.uncontractedListEmd_congr {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ φsΛ' : WickContraction φs.length} (h : φsΛ = φsΛ') : uncontractedListEmd = (finCongr ⋯).toEmbedding.trans uncontractedListEmd

theorem WickContraction.uncontractedListEmd_toFun_eq_get {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : uncontractedListEmd.toFun = φsΛ.uncontractedList.get ∘ ⇑(finCongr ⋯)

theorem WickContraction.uncontractedListEmd_strictMono {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {i j : Fin φsΛ.uncontractedListGet.length} (h : i < j) : uncontractedListEmd i < uncontractedListEmd j

theorem WickContraction.uncontractedListEmd_mem_uncontracted {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (i : Fin φsΛ.uncontractedListGet.length) : uncontractedListEmd i ∈ φsΛ.uncontracted

theorem WickContraction.uncontractedListEmd_surjective_mem_uncontracted {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (i : Fin φs.length) (hi : i ∈ φsΛ.uncontracted) : ∃ (j : Fin φsΛ.uncontractedListGet.length), uncontractedListEmd j = i

@[simp]

theorem WickContraction.uncontractedListEmd_finset_disjoint_left {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (a : Finset (Fin φsΛ.uncontractedListGet.length)) (b : Finset (Fin φs.length)) (hb : b ∈ ↑φsΛ) : Disjoint (Finset.map uncontractedListEmd a) b

theorem WickContraction.uncontractedListEmd_finset_not_mem {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (a : Finset (Fin φsΛ.uncontractedListGet.length)) : Finset.map uncontractedListEmd a ∉ ↑φsΛ

@[simp]

theorem WickContraction.getElem_uncontractedListEmd {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (k : Fin φsΛ.uncontractedListGet.length) : φs[↑(uncontractedListEmd k)] = φsΛ.uncontractedListGet[↑k]

@[simp]

theorem WickContraction.uncontractedListEmd_empty {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} : uncontractedListEmd = (finCongr ⋯).toEmbedding

Uncontracted List for extractEquiv symm none

theorem WickContraction.uncontractedList_succAboveEmb_sorted {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : List.Sorted (fun (x1 x2 : Fin (n + 1)) => x1 ≤ x2) (List.map (⇑i.succAboveEmb) c.uncontractedList)

theorem WickContraction.uncontractedList_succAboveEmb_nodup {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : (List.map (⇑i.succAboveEmb) c.uncontractedList).Nodup

theorem WickContraction.uncontractedList_succAbove_orderedInsert_nodup {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : (List.orderedInsert (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList)).Nodup

theorem WickContraction.uncontractedList_succAbove_orderedInsert_sorted {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : List.Sorted (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) (List.orderedInsert (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList))

theorem WickContraction.uncontractedList_succAbove_orderedInsert_toFinset {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : (List.orderedInsert (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList)).toFinset = insert i (Finset.map i.succAboveEmb c.uncontracted)

theorem WickContraction.uncontractedList_succAbove_orderedInsert_eq_sort {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : List.orderedInsert (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList) = Finset.sort (fun (x1 x2 : Fin (n + 1)) => x1 ≤ x2) (insert i (Finset.map i.succAboveEmb c.uncontracted))

theorem WickContraction.uncontractedList_extractEquiv_symm_none {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : ((extractEquiv i).symm ⟨c, none⟩).uncontractedList = List.orderedInsert (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList)

Uncontracted List for extractEquiv symm some

theorem WickContraction.uncontractedList_succAboveEmb_eraseIdx_toFinset {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (k : ℕ) (hk : k < c.uncontractedList.length) : ((List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k).toFinset = (Finset.map i.succAboveEmb c.uncontracted).erase (i.succAboveEmb c.uncontractedList[k])

theorem WickContraction.uncontractedList_succAboveEmb_eraseIdx_sorted {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (k : ℕ) : List.Sorted (fun (x1 x2 : Fin (n + 1)) => x1 ≤ x2) ((List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k)

theorem WickContraction.uncontractedList_succAboveEmb_eraseIdx_nodup {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (k : ℕ) : ((List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k).Nodup

theorem WickContraction.uncontractedList_succAboveEmb_eraseIdx_eq_sort {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (k : ℕ) (hk : k < c.uncontractedList.length) : (List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx k = Finset.sort (fun (x1 x2 : Fin (n + 1)) => x1 ≤ x2) ((Finset.map i.succAboveEmb c.uncontracted).erase (i.succAboveEmb c.uncontractedList[k]))

theorem WickContraction.uncontractedList_extractEquiv_symm_some {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (k : { x : Fin n // x ∈ c.uncontracted }) : ((extractEquiv i).symm ⟨c, some k⟩).uncontractedList = (List.map (⇑i.succAboveEmb) c.uncontractedList).eraseIdx ↑(c.uncontractedIndexEquiv.symm k)

theorem WickContraction.uncontractedList_succAboveEmb_toFinset {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : (List.map (⇑i.succAboveEmb) c.uncontractedList).toFinset = Finset.map i.succAboveEmb c.uncontracted

uncontractedListOrderPos

def WickContraction.uncontractedListOrderPos {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : ℕ

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.

Equations

• c.uncontractedListOrderPos i = (List.filter (fun (x : Fin n) => decide (↑x < ↑i)) c.uncontractedList).length

@[simp]

theorem WickContraction.uncontractedListOrderPos_lt_length_add_one {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : c.uncontractedListOrderPos i < c.uncontractedList.length + 1

theorem WickContraction.take_uncontractedListOrderPos_eq_filter {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : List.take (c.uncontractedListOrderPos i) c.uncontractedList = List.filter (fun (x : Fin n) => decide (↑x < ↑i)) c.uncontractedList

theorem WickContraction.take_uncontractedListOrderPos_eq_filter_sort {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : List.take (c.uncontractedListOrderPos i) c.uncontractedList = Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) (Finset.filter (fun (x : Fin n) => ↑x < ↑i) c.uncontracted)

theorem WickContraction.orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : List.orderedInsert (fun (x1 x2 : Fin n.succ) => x1 ≤ x2) i (List.map (⇑i.succAboveEmb) c.uncontractedList) = List.insertIdx (c.uncontractedListOrderPos i) i (List.map (⇑i.succAboveEmb) c.uncontractedList)