PhysLean Documentation

PhysLean.QFT.PerturbationTheory.Koszul.KoszulSignInsert

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
Instances For
    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 𝓕) :
    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 𝓕) (φ : 𝓕) :
    theorem Wick.koszulSignInsert_eq_exchangeSign_take {𝓕 : Type} (q : 𝓕FieldStatistic) (le : 𝓕𝓕Prop) [DecidableRel le] [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) (φs : List 𝓕) :
    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
    Instances For
      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