Erasing an element from a contraction

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

Given a Wick contraction WickContraction n.succ and a i : Fin n.succ the Wick contraction associated with n obtained by removing i. If i is contracted with j in the new Wick contraction j will be uncontracted.

Equations

• c.erase i = ⟨Finset.filter (fun (x : Finset (Fin n)) => Finset.map i.succAboveEmb x ∈ ↑c) Finset.univ, ⋯⟩

theorem WickContraction.mem_erase_uncontracted_iff {n : ℕ} (c : WickContraction n.succ) (i : Fin n.succ) (j : Fin n) : j ∈ (c.erase i).uncontracted ↔ i.succAbove j ∈ c.uncontracted ∨ c.getDual? (i.succAbove j) = some i

theorem WickContraction.mem_not_eq_erase_of_isSome {n : ℕ} {a : Finset (Fin n.succ)} (c : WickContraction n.succ) (i : Fin n.succ) (h : (c.getDual? i).isSome = true) (ha : a ∈ ↑c) (ha2 : a ≠ {i, (c.getDual? i).get h}) : ∃ a' ∈ ↑(c.erase i), a = Finset.map i.succAboveEmb a'

theorem WickContraction.mem_not_eq_erase_of_isNone {n : ℕ} {a : Finset (Fin n.succ)} (c : WickContraction n.succ) (i : Fin n.succ) (h : (c.getDual? i).isNone = true) (ha : a ∈ ↑c) : ∃ a' ∈ ↑(c.erase i), a = Finset.map i.succAboveEmb a'

def WickContraction.getDualErase {n : ℕ} (c : WickContraction n.succ) (i : Fin n.succ) : Option { x : Fin n // x ∈ (c.erase i).uncontracted }

Given a Wick contraction c : WickContraction n.succ and a i : Fin n.succ the (optional) element of (erase c i).uncontracted which comes from the element in c contracted with i.

Equations

• c_2.getDualErase i_2 = none
• c_2.getDualErase i_2 = if hj : (c_2.getDual? i_2).isSome = true then some ⟨PhysLean.Fin.predAboveI i_2 ((c_2.getDual? i_2).get hj), ⋯⟩ else none

@[simp]

theorem WickContraction.getDualErase_isSome_iff_getDual?_isSome {n : ℕ} (c : WickContraction n.succ) (i : Fin n.succ) : (c.getDualErase i).isSome = true ↔ (c.getDual? i).isSome = true

@[simp]

theorem WickContraction.getDualErase_one (c : WickContraction 1) (i : Fin 1) : c.getDualErase i = none