Uncontracted elements

def WickContraction.uncontracted {n : ℕ} (c : WickContraction n) : Finset (Fin n)

For a Wick contraction c, c.uncontracted is defined as the finset of elements of Fin n which are not in any contracted pair.

Equations

• c.uncontracted = Finset.filter (fun (i : Fin n) => c.getDual? i = none) Finset.univ

theorem WickContraction.congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) : ((congr h) c).uncontracted = Finset.map (finCongr h).toEmbedding c.uncontracted

theorem WickContraction.getDual?_eq_none_iff_mem_uncontracted {n : ℕ} (c : WickContraction n) (i : Fin n) : c.getDual? i = none ↔ i ∈ c.uncontracted

def WickContraction.uncontractedCongr {n : ℕ} {c c' : WickContraction n} (h : c = c') : Option { x : Fin n // x ∈ c.uncontracted } ≃ Option { x : Fin n // x ∈ c'.uncontracted }

The equivalence of Option c.uncontracted for two propositionally equal Wick contractions.

Equations

• WickContraction.uncontractedCongr h = (Equiv.subtypeEquivRight ⋯).optionCongr

@[simp]

theorem WickContraction.uncontractedCongr_none {n : ℕ} {c c' : WickContraction n} (h : c = c') : (uncontractedCongr h) none = none

@[simp]

theorem WickContraction.uncontractedCongr_some {n : ℕ} {c c' : WickContraction n} (h : c = c') (i : { x : Fin n // x ∈ c.uncontracted }) : (uncontractedCongr h) (some i) = some ((Equiv.subtypeEquivRight ⋯) i)

theorem WickContraction.mem_uncontracted_iff_not_contracted {n : ℕ} (c : WickContraction n) (i : Fin n) : i ∈ c.uncontracted ↔ ∀ p ∈ ↑c, i ∉ p

theorem WickContraction.mem_uncontracted_empty {n : ℕ} (i : Fin n) : i ∈ empty.uncontracted

@[simp]

theorem WickContraction.getDual?_empty_eq_none {n : ℕ} (i : Fin n) : empty.getDual? i = none

@[simp]

theorem WickContraction.uncontracted_empty {n : ℕ} : empty.uncontracted = Finset.univ

theorem WickContraction.uncontracted_card_le {n : ℕ} (c : WickContraction n) : c.uncontracted.card ≤ n

theorem WickContraction.uncontracted_card_eq_iff {n : ℕ} (c : WickContraction n) : c.uncontracted.card = n ↔ c = empty