Singleton of contractions

def WickContraction.singleton {n : ℕ} {i j : Fin n} (hij : i < j) : WickContraction n

The Wick contraction formed from a single ordered pair.

Equations

• WickContraction.singleton hij = ⟨{{i, j}}, ⋯⟩

theorem WickContraction.mem_singleton {n : ℕ} {i j : Fin n} (hij : i < j) : {i, j} ∈ ↑(singleton hij)

theorem WickContraction.mem_singleton_iff {n : ℕ} {i j : Fin n} (hij : i < j) {a : Finset (Fin n)} : a ∈ ↑(singleton hij) ↔ a = {i, j}

theorem WickContraction.of_singleton_eq {n : ℕ} {i j : Fin n} (hij : i < j) (a : { x : Finset (Fin n) // x ∈ ↑(singleton hij) }) : a = ⟨{i, j}, ⋯⟩

theorem WickContraction.singleton_prod {𝓕 : FieldSpecification} {M : Type u_1} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) (f : { x : Finset (Fin φs.length) // x ∈ ↑(singleton hij) } → M) [CommMonoid M] : ∏ a : { x : Finset (Fin φs.length) // x ∈ ↑(singleton hij) }, f a = f ⟨{i, j}, ⋯⟩

@[simp]

theorem WickContraction.singleton_fstFieldOfContract {n : ℕ} {i j : Fin n} (hij : i < j) : (singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩ = i

@[simp]

theorem WickContraction.singleton_sndFieldOfContract {n : ℕ} {i j : Fin n} (hij : i < j) : (singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩ = j

theorem WickContraction.singleton_sign_expand {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) : sign φs (singleton hij) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φs[j])) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j))

theorem WickContraction.singleton_getDual?_eq_none_iff_neq {n : ℕ} {i j : Fin n} (hij : i < j) (a : Fin n) : (singleton hij).getDual? a = none ↔ i ≠ a ∧ j ≠ a

theorem WickContraction.singleton_uncontractedEmd_neq_left {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) (a : Fin (singleton hij).uncontractedListGet.length) : uncontractedListEmd a ≠ i

theorem WickContraction.singleton_uncontractedEmd_neq_right {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) (a : Fin (singleton hij).uncontractedListGet.length) : uncontractedListEmd a ≠ j

@[simp]

theorem WickContraction.mem_signFinset {n : ℕ} {i j : Fin n} (hij : i < j) (a : Fin n) : a ∈ (singleton hij).signFinset i j ↔ i < a ∧ a < j

theorem WickContraction.subContraction_singleton_eq_singleton {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) : subContraction {↑a} ⋯ = singleton ⋯

theorem WickContraction.singleton_timeContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) : (singleton hij).timeContract = ⟨FieldSpecification.FieldOpAlgebra.timeContract φs[i] φs[j], ⋯⟩

theorem WickContraction.singleton_staticContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) : ↑(singleton hij).staticContract = (FieldSpecification.FieldOpAlgebra.superCommute (FieldSpecification.FieldOpAlgebra.anPart φs[i])) (FieldSpecification.FieldOpAlgebra.ofFieldOp φs[j])