Koszul sign insert

def Wick.koszulSignInsert {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) : List 𝓕 → ℂ

Gives a factor of -1 when inserting a into a list List I in the ordered position for each fermion-fermion cross.

Equations

• One or more equations did not get rendered due to their size.
• Wick.koszulSignInsert q le φ [] = 1

theorem Wick.koszulSignInsert_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) (ha : q φ = FieldStatistic.bosonic) (φs : List 𝓕) : koszulSignInsert q le φ φs = 1

When inserting a boson the koszulSignInsert is always 1.

@[simp]

theorem Wick.koszulSignInsert_mul_self {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) (φs : List 𝓕) : koszulSignInsert q le φ φs * koszulSignInsert q le φ φs = 1

theorem Wick.koszulSignInsert_le_forall {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) (φs : List 𝓕) (hi : ∀ (φ' : 𝓕), le φ φ') : koszulSignInsert q le φ φs = 1

theorem Wick.koszulSignInsert_ge_forall_append {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φs : List 𝓕) (φ' φ : 𝓕) (hi : ∀ (φ'' : 𝓕), le φ'' φ) : koszulSignInsert q le φ' φs = koszulSignInsert q le φ' (φs ++ [φ])

theorem Wick.koszulSignInsert_eq_filter {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) (φs : List 𝓕) : koszulSignInsert q le φ φs = koszulSignInsert q le φ (List.filter (fun (i : 𝓕) => decide ¬le φ i) φs)

theorem Wick.koszulSignInsert_eq_cons {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] (φ : 𝓕) (φs : List 𝓕) : koszulSignInsert q le φ φs = koszulSignInsert q le φ (φ :: φs)

theorem Wick.koszulSignInsert_eq_grade {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ : 𝓕) (φs : List 𝓕) : koszulSignInsert q le φ φs = if FieldStatistic.ofList q [φ] = FieldStatistic.fermionic ∧ FieldStatistic.ofList q (List.filter (fun (i : 𝓕) => decide ¬le φ i) φs) = FieldStatistic.fermionic then -1 else 1

theorem Wick.koszulSignInsert_eq_perm {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φs φs' : List 𝓕) (φ : 𝓕) (h : φs.Perm φs') : koszulSignInsert q le φ φs = koszulSignInsert q le φ φs'

theorem Wick.koszulSignInsert_eq_sort {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φs : List 𝓕) (φ : 𝓕) : koszulSignInsert q le φ φs = koszulSignInsert q le φ (List.insertionSort le φs)

theorem Wick.koszulSignInsert_eq_exchangeSign_take {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) (φs : List 𝓕) : koszulSignInsert q le φ φs = (FieldStatistic.exchangeSign (q φ)) (FieldStatistic.ofList q (List.take (↑(PhysLean.List.orderedInsertPos le (List.insertionSort le φs) φ)) (List.insertionSort le φs)))

theorem Wick.koszulSignInsert_insertIdx {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (i j : 𝓕) (r : List 𝓕) (n : ℕ) (hn : n ≤ r.length) : koszulSignInsert q le j (r.insertIdx n i) = koszulSignInsert q le j (i :: r)

def Wick.koszulSignCons {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ0 φ1 : 𝓕) : ℂ

The difference in koszulSignInsert on inserting r0 into r compared to into r1 :: r for any r.

Equations

• Wick.koszulSignCons q le φ0 φ1 = if le φ0 φ1 then 1 else if q φ0 = FieldStatistic.fermionic ∧ q φ1 = FieldStatistic.fermionic then -1 else 1

theorem Wick.koszulSignCons_eq_exchangeSign {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ0 φ1 : 𝓕) : koszulSignCons q le φ0 φ1 = if le φ0 φ1 then 1 else (FieldStatistic.exchangeSign (q φ0)) (q φ1)

theorem Wick.koszulSignInsert_cons {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (r0 r1 : 𝓕) (r : List 𝓕) : koszulSignInsert q le r0 (r1 :: r) = koszulSignCons q le r0 r1 * koszulSignInsert q le r0 r

theorem Wick.koszulSignInsert_of_le_mem {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] (φ0 : 𝓕) (φs : List 𝓕) (h : ∀ b ∈ φs, le φ0 b) : koszulSignInsert q le φ0 φs = 1

theorem Wick.koszulSignInsert_eq_rel_eq_stat {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] {ψ φ : 𝓕} [IsTrans 𝓕 le] (h1 : le φ ψ) (h2 : le ψ φ) (hq : q ψ = q φ) (φs : List 𝓕) : koszulSignInsert q le φ φs = koszulSignInsert q le ψ φs

theorem Wick.koszulSignInsert_eq_remove_same_stat_append {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le] {ψ φ φ' : 𝓕} [IsTrans 𝓕 le] (h1 : le φ ψ) (h2 : le ψ φ) (hq : q ψ = q φ) (φs : List 𝓕) : koszulSignInsert q le φ' (φ :: ψ :: φs) = koszulSignInsert q le φ' φs