Koszul sign insert #
def
Wick.koszulSignInsert
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φ : 𝓕)
:
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
Instances For
theorem
Wick.koszulSignInsert_boson
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φ : 𝓕)
(ha : q φ = FieldStatistic.bosonic)
(φs : List 𝓕)
:
When inserting a boson the koszulSignInsert
is always 1
.
@[simp]
theorem
Wick.koszulSignInsert_mul_self
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φ : 𝓕)
(φs : List 𝓕)
:
theorem
Wick.koszulSignInsert_le_forall
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φ : 𝓕)
(φs : List 𝓕)
(hi : ∀ (φ' : 𝓕), le φ φ')
:
theorem
Wick.koszulSignInsert_ge_forall_append
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φs : List 𝓕)
(φ' φ : 𝓕)
(hi : ∀ (φ'' : 𝓕), le φ'' φ)
:
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 𝓕)
:
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')
:
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 𝓕)
:
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)
:
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
Instances For
theorem
Wick.koszulSignCons_eq_exchangeSign
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φ0 φ1 : 𝓕)
:
theorem
Wick.koszulSignInsert_cons
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(r0 r1 : 𝓕)
(r : List 𝓕)
:
theorem
Wick.koszulSignInsert_of_le_mem
{𝓕 : Type}
(q : 𝓕 → FieldStatistic)
(le : 𝓕 → 𝓕 → Prop)
[DecidableRel le]
(φ0 : 𝓕)
(φs : List 𝓕)
(h : ∀ b ∈ φs, le φ0 b)
:
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 𝓕)
:
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 𝓕)
: