Inserting an element into a contraction based on a list

Inserting an element into a list

def WickContraction.insertAndContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : WickContraction (List.insertIdx (↑i) φ φs).length

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.

Equations

• WickContraction.insertAndContract φ φsΛ i k = (WickContraction.congr ⋯) (φsΛ.insertAndContractNat i k)

def WickContraction.«term_↩Λ___» : Lean.TrailingParserDescr

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.

Equations

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

@[simp]

theorem WickContraction.insertAndContract_fstFieldOfContract {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) : (insertAndContract φ φsΛ i j).fstFieldOfContract (congrLift ⋯ (insertLift i j a)) = (finCongr ⋯) (i.succAbove (φsΛ.fstFieldOfContract a))

@[simp]

theorem WickContraction.insertAndContract_sndFieldOfContract {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) : (insertAndContract φ φsΛ i j).sndFieldOfContract (congrLift ⋯ (insertLift i j a)) = (finCongr ⋯) (i.succAbove (φsΛ.sndFieldOfContract a))

@[simp]

theorem WickContraction.insertAndContract_fstFieldOfContract_some_incl {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ i (some j)).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩) = if i < i.succAbove ↑j then (finCongr ⋯) i else (finCongr ⋯) (i.succAbove ↑j)

insertAndContract and getDual?

@[simp]

theorem WickContraction.insertAndContract_none_getDual?_self {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : (insertAndContract φ φsΛ i none).getDual? (Fin.cast ⋯ i) = none

theorem WickContraction.insertAndContract_isSome_getDual?_self {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : ((insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast ⋯ i)).isSome = true

theorem WickContraction.insertAndContract_some_getDual?_self_not_none {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : ¬(insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast ⋯ i) = none

@[simp]

theorem WickContraction.insertAndContract_some_getDual?_self_eq {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast ⋯ i) = some (Fin.cast ⋯ (i.succAbove ↑j))

@[simp]

theorem WickContraction.insertAndContract_some_getDual?_some_eq {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ i (some j)).getDual? (Fin.cast ⋯ (i.succAbove ↑j)) = some (Fin.cast ⋯ i)

@[simp]

theorem WickContraction.insertAndContract_none_succAbove_getDual?_eq_none_iff {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) : (insertAndContract φ φsΛ i none).getDual? (Fin.cast ⋯ (i.succAbove j)) = none ↔ φsΛ.getDual? j = none

@[simp]

theorem WickContraction.insertAndContract_some_succAbove_getDual?_eq_option {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (hkj : j ≠ ↑k) : (insertAndContract φ φsΛ i (some k)).getDual? (Fin.cast ⋯ (i.succAbove j)) = Option.map (Fin.cast ⋯ ∘ i.succAbove) (φsΛ.getDual? j)

@[simp]

theorem WickContraction.insertAndContract_none_succAbove_getDual?_isSome_iff {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) : ((insertAndContract φ φsΛ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).isSome = true ↔ (φsΛ.getDual? j).isSome = true

@[simp]

theorem WickContraction.insertAndContract_none_getDual?_get_eq {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : Fin φs.length) (h : ((insertAndContract φ φsΛ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).isSome = true) : ((insertAndContract φ φsΛ i none).getDual? (Fin.cast ⋯ (i.succAbove j))).get h = Fin.cast ⋯ (i.succAbove ((φsΛ.getDual? j).get ⋯))

@[simp]

theorem WickContraction.insertAndContract_sndFieldOfContract_some_incl {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ i (some j)).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩) = if i < i.succAbove ↑j then (finCongr ⋯) (i.succAbove ↑j) else (finCongr ⋯) i

theorem WickContraction.insertAndContract_none_prod_contractions {𝓕 : FieldSpecification} {M : Type u_1} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (f : { x : Finset (Fin (List.insertIdx (↑i) φ φs).length) // x ∈ ↑(insertAndContract φ φsΛ i none) } → M) [CommMonoid M] : ∏ a : { x : Finset (Fin (List.insertIdx (↑i) φ φs).length) // x ∈ ↑(insertAndContract φ φsΛ i none) }, f a = ∏ a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }, f (congrLift ⋯ (insertLift i none a))

theorem WickContraction.insertAndContract_some_prod_contractions {𝓕 : FieldSpecification} {M : Type u_1} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) (f : { x : Finset (Fin (List.insertIdx (↑i) φ φs).length) // x ∈ ↑(insertAndContract φ φsΛ i (some j)) } → M) [CommMonoid M] : ∏ a : { x : Finset (Fin (List.insertIdx (↑i) φ φs).length) // x ∈ ↑(insertAndContract φ φsΛ i (some j)) }, f a = f (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩) * ∏ a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }, f (congrLift ⋯ (insertLift i (some j) a))

def WickContraction.insertAndContractLiftFinset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) : Finset (Fin (List.insertIdx (↑i) φ φs).length)

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.

Equations

• WickContraction.insertAndContractLiftFinset φ i a = Finset.map (finCongr ⋯).toEmbedding (Finset.map i.succAboveEmb a)

@[simp]

theorem WickContraction.self_not_mem_insertAndContractLiftFinset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) : Fin.cast ⋯ i ∉ insertAndContractLiftFinset φ i a

theorem WickContraction.succAbove_mem_insertAndContractLiftFinset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) (j : Fin φs.length) : Fin.cast ⋯ (i.succAbove j) ∈ insertAndContractLiftFinset φ i a ↔ j ∈ a

theorem WickContraction.insert_fin_eq_self {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (i : Fin φs.length.succ) (j : Fin (List.insertIdx (↑i) φ φs).length) : j = Fin.cast ⋯ i ∨ ∃ (k : Fin φs.length), j = Fin.cast ⋯ (i.succAbove k)

theorem WickContraction.insertLift_sum {𝓕 : FieldSpecification} {M : Type u_1} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (List.insertIdx (↑i) φ φs).length → M) : ∑ c : WickContraction (List.insertIdx (↑i) φ φs).length, f c = ∑ φsΛ : WickContraction φs.length, ∑ k : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted }, f (insertAndContract φ φsΛ i k)

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.

Uncontracted list

theorem WickContraction.insertAndContract_uncontractedList_none_map {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : (insertAndContract φ φsΛ i none).uncontractedListGet = List.insertIdx (φsΛ.uncontractedListOrderPos i) φ φsΛ.uncontractedListGet

@[simp]

theorem WickContraction.insertAndContract_uncontractedList_none_zero {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : (insertAndContract φ φsΛ 0 none).uncontractedListGet = φ :: φsΛ.uncontractedListGet

theorem WickContraction.stat_ofFinset_of_insertAndContractLiftFinset {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) : FieldStatistic.ofFinset 𝓕.fieldOpStatistic (List.insertIdx (↑i) φ φs).get (insertAndContractLiftFinset φ i a) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get a