refactor: Lint
This commit is contained in:
jstoobysmith
parent
c993de36f6
commit
cd63ec0716
13 changed files with 181 additions and 84 deletions
|
|
@ -125,6 +125,7 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
|
|||
simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
|
||||
· simp [hPa]
|
||||
|
||||
/-- The position `r0` ends up in `r` on adding it via `List.orderedInsert _ r0 r`. -/
|
||||
def orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
|
||||
Fin (List.orderedInsert le1 r0 r).length :=
|
||||
⟨(List.takeWhile (fun b => decide ¬ le1 r0 b) r).length, by
|
||||
|
|
@ -167,7 +168,7 @@ lemma orderedInsertPos_cons {I : Type} (le1 : I → I → Prop) [DecidableRel le
|
|||
· simp [h]
|
||||
· simp [h]
|
||||
|
||||
lemma orderedInsertPos_sigma {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma orderedInsertPos_sigma {I : Type} {f : I → Type}
|
||||
(le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i))
|
||||
(k : I) (a : f k) :
|
||||
(orderedInsertPos (fun (i j : Σ i, f i) => le1 i.1 j.1) l ⟨k, a⟩).1 =
|
||||
|
|
@ -188,7 +189,6 @@ lemma orderedInsertPos_sigma {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
simp_all only [Bool.not_eq_eq_eq_not, Bool.not_false, decide_eq_true_eq, List.length_nil,
|
||||
decide_True, Bool.not_true]
|
||||
|
||||
@[simp]
|
||||
lemma orderedInsert_get_lt {I : Type} (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(r : List I) (r0 : I) (i : ℕ)
|
||||
(hi : i < orderedInsertPos le1 r r0) :
|
||||
|
|
@ -336,6 +336,8 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
|
|||
· simp only [orderedInsertPos] at hi
|
||||
omega
|
||||
|
||||
/-- The equivalence between `Fin (r0 :: r).length` and `Fin (List.orderedInsert le1 r0 r).length`
|
||||
according to where the elements map. I.e. `0` is taken to `orderedInsertPos le1 r r0`. -/
|
||||
def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
|
||||
Fin (r0 :: r).length ≃ Fin (List.orderedInsert le1 r0 r).length := by
|
||||
let e2 : Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length :=
|
||||
|
|
@ -345,12 +347,10 @@ def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r
|
|||
finExtractOne ⟨orderedInsertPos le1 r r0, orderedInsertPos_lt_length le1 r r0⟩
|
||||
exact e3.trans (e4.symm.trans e2.symm)
|
||||
|
||||
@[simp]
|
||||
lemma orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
|
||||
(r0 : I) : orderedInsertEquiv le1 r r0 ⟨0, by simp⟩ = orderedInsertPos le1 r r0 := by
|
||||
simp [orderedInsertEquiv]
|
||||
|
||||
@[simp]
|
||||
lemma orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
|
||||
(r0 : I) (n : ℕ) (hn : Nat.succ n < (r0 :: r).length) :
|
||||
orderedInsertEquiv le1 r r0 ⟨Nat.succ n, hn⟩ =
|
||||
|
|
@ -369,7 +369,6 @@ lemma orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel
|
|||
rfl
|
||||
exact ne_of_beq_false rfl
|
||||
|
||||
@[simp]
|
||||
lemma orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I)
|
||||
(r0 : I) (n : Fin r.length) :
|
||||
orderedInsertEquiv le1 r r0 n.succ = Fin.cast (List.orderedInsert_length le1 r r0).symm
|
||||
|
|
@ -411,7 +410,7 @@ lemma get_eq_orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRe
|
|||
erw [orderedInsertEquiv_succ]
|
||||
simp only [Fin.succAbove, Fin.castSucc_mk, Fin.mk_lt_mk, Fin.succ_mk, Fin.coe_cast]
|
||||
by_cases hn : n < ↑(orderedInsertPos le1 r r0)
|
||||
· simp [hn]
|
||||
· simp [hn, orderedInsert_get_lt]
|
||||
· simp only [hn, ↓reduceIte]
|
||||
simp only [List.orderedInsert_eq_take_drop, decide_not]
|
||||
rw [List.getElem_append]
|
||||
|
|
@ -478,7 +477,7 @@ lemma orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ
|
|||
rw [hn]
|
||||
exact orderedInsert_eraseIdx_orderedInsertEquiv_succ le1 r r0 n.val _ hr
|
||||
|
||||
lemma orderedInsertEquiv_sigma {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma orderedInsertEquiv_sigma {I : Type} {f : I → Type}
|
||||
(le1 : I → I → Prop) [DecidableRel le1] (l : List (Σ i, f i))
|
||||
(i : I) (a : f i) :
|
||||
(orderedInsertEquiv (fun i j => le1 i.fst j.fst) l ⟨i, a⟩) =
|
||||
|
|
@ -656,11 +655,17 @@ lemma insertionSort_eq_ofFn {α : Type} {r : α → α → Prop} [DecidableRel r
|
|||
rw [insertionSortEquiv_get (r := r)]
|
||||
exact Eq.symm (List.ofFn_get (List.insertionSort r l))
|
||||
|
||||
/-- Optional erase of an element in a list. For `none` returns the list, for `some i` returns
|
||||
the list with the `i`'th element erased. -/
|
||||
def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
|
||||
match i with
|
||||
| none => l
|
||||
| some i => List.eraseIdx l i
|
||||
|
||||
/-- Optional erase of an element in a list, with addition for `none`. For `none` adds `a` to the
|
||||
front of the list, for `some i` removes the `i`th element of the list (does not add `a`).
|
||||
E.g. `optionEraseZ [0, 1, 2] 4 none = [4, 0, 1, 2]` and
|
||||
`optionEraseZ [0, 1, 2] 4 (some 1) = [0, 2]`. -/
|
||||
def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I :=
|
||||
match i with
|
||||
| none => a :: l
|
||||
|
|
@ -718,9 +723,6 @@ lemma eraseIdx_insertionSort {I : Type} (le1 : I → I → Prop) [DecidableRel l
|
|||
intro i j hij hn
|
||||
have hx := List.Sorted.rel_get_of_lt (r := le1) (l := (List.insertionSort le1 r))
|
||||
(List.sorted_insertionSort le1 r) hij
|
||||
have hr : le1 ((List.insertionSort le1 r).get j) r0 := by
|
||||
have hn := IsTotal.total (r := le1) ((List.insertionSort le1 r).get j) r0
|
||||
simp_all only [List.get_eq_getElem, List.length_cons, or_false]
|
||||
have ht (i j k : I) (hij : le1 i j) (hjk : ¬ le1 k j) : ¬ le1 k i := by
|
||||
intro hik
|
||||
have ht := IsTrans.trans (r := le1) k i j hik hij
|
||||
|
|
|
|||
|
|
@ -16,17 +16,21 @@ noncomputable section
|
|||
|
||||
open HepLean.List
|
||||
|
||||
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`
|
||||
which have the list `aux` uncontracted. -/
|
||||
inductive ContractionsAux {I : Type} : (l : List I) → (aux : List I) → Type
|
||||
| nil : ContractionsAux [] []
|
||||
| cons {l : List I} {aux : List I} {a : I} (i : Option (Fin aux.length)) :
|
||||
ContractionsAux l aux → ContractionsAux (a :: l) (optionEraseZ aux a i)
|
||||
|
||||
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`. -/
|
||||
def Contractions {I : Type} (l : List I) : Type := Σ aux, ContractionsAux l aux
|
||||
|
||||
namespace Contractions
|
||||
|
||||
variable {I : Type} {l : List I} (c : Contractions l)
|
||||
|
||||
/-- The list of uncontracted fields. -/
|
||||
def normalize : List I := c.1
|
||||
|
||||
lemma contractions_nil (a : Contractions ([] : List I)) : a = ⟨[], ContractionsAux.nil⟩ := by
|
||||
|
|
@ -47,12 +51,16 @@ lemma contractions_single {i : I} (a : Contractions [i]) : a =
|
|||
rename_i x
|
||||
exact Fin.elim0 x
|
||||
|
||||
/-- For the nil list of fields there is only one contraction. -/
|
||||
def nilEquiv : Contractions ([] : List I) ≃ Unit where
|
||||
toFun _ := ()
|
||||
invFun _ := ⟨[], ContractionsAux.nil⟩
|
||||
left_inv a := Eq.symm (contractions_nil a)
|
||||
right_inv _ := rfl
|
||||
|
||||
/-- The equivalence between contractions of `a :: l` and contractions of
|
||||
`Contractions l` paired with an optional element of `Fin (c.normalize).length` specifying
|
||||
what `a` contracts with if any. -/
|
||||
def consEquiv {a : I} {l : List I} :
|
||||
Contractions (a :: l) ≃ (c : Contractions l) × Option (Fin (c.normalize).length) where
|
||||
toFun c :=
|
||||
|
|
@ -69,6 +77,7 @@ def consEquiv {a : I} {l : List I} :
|
|||
| ContractionsAux.cons (aux := aux') i c => rfl
|
||||
right_inv ci := by rfl
|
||||
|
||||
/-- The type of contractions is decidable. -/
|
||||
instance decidable : (l : List I) → DecidableEq (Contractions l)
|
||||
| [] => fun a b =>
|
||||
match a, b with
|
||||
|
|
@ -81,6 +90,7 @@ instance decidable : (l : List I) → DecidableEq (Contractions l)
|
|||
Sigma.instDecidableEqSigma
|
||||
Equiv.decidableEq consEquiv
|
||||
|
||||
/-- The type of contractions is finite. -/
|
||||
instance fintype : (l : List I) → Fintype (Contractions l)
|
||||
| [] => {
|
||||
elems := {⟨[], ContractionsAux.nil⟩}
|
||||
|
|
@ -94,21 +104,31 @@ instance fintype : (l : List I) → Fintype (Contractions l)
|
|||
Sigma.instFintype
|
||||
Fintype.ofEquiv _ consEquiv.symm
|
||||
|
||||
/-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
|
||||
the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
|
||||
structure Splitting {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] where
|
||||
/-- The creation part of the fields. The label `n` corresponds to the fact that
|
||||
in normal ordering these feilds get pushed to the negative (left) direction. -/
|
||||
𝓑n : I → (Σ i, f i)
|
||||
/-- The annhilation part of the fields. The label `p` corresponds to the fact that
|
||||
in normal ordering these feilds get pushed to the positive (right) direction. -/
|
||||
𝓑p : I → (Σ i, f i)
|
||||
/-- The complex coefficent of creation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧n : I → ℂ
|
||||
/-- The complex coefficent of annhilation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧p : I → ℂ
|
||||
h𝓑 : ∀ i, ofListLift f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
|
||||
h𝓑n : ∀ i j, le1 (𝓑n i) j
|
||||
h𝓑p : ∀ i j, le1 j (𝓑p i)
|
||||
|
||||
/-- In the static wick's theorem, the term associated with a contraction `c` containing
|
||||
the contractions. -/
|
||||
def toCenterTerm {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A) :
|
||||
{r : List I} → (c : Contractions r) → (S : Splitting f le1) → A
|
||||
| [], ⟨[], .nil⟩, _ => 1
|
||||
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S
|
||||
|
|
@ -120,7 +140,7 @@ lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
|
|||
(q : I → Fin 2) {r : List I}
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A)
|
||||
(S : Splitting f le1) (a : I) (c : Contractions r) :
|
||||
toCenterTerm (r := a :: r) f q le1 F (Contractions.consEquiv.symm ⟨c, none⟩) S =
|
||||
toCenterTerm f q le1 F c S := by
|
||||
|
|
|
|||
|
|
@ -13,25 +13,35 @@ import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
|
|||
namespace Wick
|
||||
open HepLean.List
|
||||
|
||||
def CreateAnnilateSect {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) : Type :=
|
||||
/-- The sections of `Σ i, f i` over a list `l : List I`.
|
||||
In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
|
||||
each field as a `creation` or an `annilation` operator. E.g. the number of terms
|
||||
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
|
||||
operators at this point (e.g. ansymptotic states) this is accounted for. -/
|
||||
def CreateAnnilateSect {I : Type} (f : I → Type) (l : List I) : Type :=
|
||||
Π i, f (l.get i)
|
||||
|
||||
namespace CreateAnnilateSect
|
||||
|
||||
variable {I : Type} {f : I → Type} [∀ i, Fintype (f i)] {l : List I} (a : CreateAnnilateSect f l)
|
||||
|
||||
/-- The type `CreateAnnilateSect f l` is finite. -/
|
||||
instance fintype : Fintype (CreateAnnilateSect f l) := Pi.fintype
|
||||
|
||||
/-- The section got by dropping the first element of `l` if it exists. -/
|
||||
def tail : {l : List I} → (a : CreateAnnilateSect f l) → CreateAnnilateSect f l.tail
|
||||
| [], a => a
|
||||
| _ :: _, a => fun i => a (Fin.succ i)
|
||||
|
||||
/-- For a list of fields `i :: l` the value of the section at the head `i`. -/
|
||||
def head {i : I} (a : CreateAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
|
||||
|
||||
/-- The list `List (Σ i, f i)` defined by `a`. -/
|
||||
def toList : {l : List I} → (a : CreateAnnilateSect f l) → List (Σ i, f i)
|
||||
| [], _ => []
|
||||
| i :: _, a => ⟨i, a.head⟩ :: toList a.tail
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
@[simp]
|
||||
lemma toList_length : (toList a).length = l.length := by
|
||||
induction l with
|
||||
|
|
@ -40,15 +50,18 @@ lemma toList_length : (toList a).length = l.length := by
|
|||
simp only [toList, List.length_cons, Fin.zero_eta]
|
||||
rw [ih]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma toList_tail : {l : List I} → (a : CreateAnnilateSect f l) → toList a.tail = (toList a).tail
|
||||
| [], _ => rfl
|
||||
| i :: l, a => by
|
||||
simp [toList]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma toList_cons {i : I} (a : CreateAnnilateSect f (i :: l)) :
|
||||
(toList a) = ⟨i, a.head⟩ :: toList a.tail := by
|
||||
rfl
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma toList_get (a : CreateAnnilateSect f l) :
|
||||
(toList a).get = (fun i => ⟨l.get i, a i⟩) ∘ Fin.cast (by simp) := by
|
||||
induction l with
|
||||
|
|
@ -67,6 +80,7 @@ lemma toList_get (a : CreateAnnilateSect f l) :
|
|||
rw [ih]
|
||||
simp [tail]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
@[simp]
|
||||
lemma toList_grade (q : I → Fin 2) :
|
||||
grade (fun i => q i.fst) a.toList = 1 ↔ grade q l = 1 := by
|
||||
|
|
@ -90,7 +104,7 @@ lemma toList_grade (q : I → Fin 2) :
|
|||
rw [h1]
|
||||
|
||||
@[simp]
|
||||
lemma toList_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma toList_grade_take {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) : (r : List I) → (a : CreateAnnilateSect f r) → (n : ℕ) →
|
||||
grade (fun i => q i.fst) (List.take n a.toList) = grade q (List.take n r)
|
||||
| [], _, _ => by
|
||||
|
|
@ -101,7 +115,10 @@ lemma toList_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
simp only [grade, Fin.isValue]
|
||||
rw [toList_grade_take q r a.tail n]
|
||||
|
||||
def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : List I}
|
||||
/-- The equivalence between `CreateAnnilateSect f l` and
|
||||
`f (l.get n) × CreateAnnilateSect f (l.eraseIdx n)` obtained by extracting the `n`th field
|
||||
from `l`. -/
|
||||
def extractEquiv {I : Type} {f : I → Type} {l : List I}
|
||||
(n : Fin l.length) : CreateAnnilateSect f l ≃
|
||||
f (l.get n) × CreateAnnilateSect f (l.eraseIdx n) := by
|
||||
match l with
|
||||
|
|
@ -136,7 +153,7 @@ def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : Li
|
|||
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]))
|
||||
exact (Fin.insertNthEquiv _ _).symm.trans (Equiv.prodCongr (Equiv.refl _) e1.symm)
|
||||
|
||||
lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
|
||||
lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type}
|
||||
{l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreateAnnilateSect f (l.eraseIdx n)) :
|
||||
((extractEquiv n).symm (a0, a)).toList[n] = ⟨l[n], a0⟩ := by
|
||||
match l with
|
||||
|
|
@ -155,9 +172,11 @@ lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I) →
|
|||
erw [Fin.insertNthEquiv_apply]
|
||||
simp only [Fin.insertNth_apply_same]
|
||||
|
||||
/-- The section obtained by dropping the `n`th field. -/
|
||||
def eraseIdx (n : Fin l.length) : CreateAnnilateSect f (l.eraseIdx n) :=
|
||||
(extractEquiv n a).2
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
@[simp]
|
||||
lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreateAnnilateSect f (i :: l)) :
|
||||
(eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
|
||||
|
|
@ -168,6 +187,7 @@ lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreateAnnilateSect f (i :: l)
|
|||
Equiv.cast_refl, Equiv.trans_apply, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_snd]
|
||||
rfl
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
|
||||
(a : CreateAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
|
||||
rw [eraseIdx, extractEquiv]
|
||||
|
|
@ -189,6 +209,7 @@ lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
|
|||
congr
|
||||
simp [Fin.ext_iff]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
|
||||
(a : CreateAnnilateSect f (i :: l)) :
|
||||
(eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n, Nat.succ_lt_succ_iff.mp hn⟩ := by
|
||||
|
|
@ -250,6 +271,7 @@ lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
|
|||
omega
|
||||
next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]
|
||||
|
||||
omit [∀ i, Fintype (f i)] in
|
||||
lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreateAnnilateSect f l) →
|
||||
(eraseIdx a n).toList = a.toList.eraseIdx n
|
||||
| [], n, _ => Fin.elim0 n
|
||||
|
|
@ -263,7 +285,7 @@ lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreateAnnil
|
|||
· conv_rhs => rw [← eraseIdx_toList (l := r) (n := ⟨n, Nat.succ_lt_succ_iff.mp h⟩) a.tail]
|
||||
rw [eraseIdx_succ_tail]
|
||||
|
||||
lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
|
||||
lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type}
|
||||
{l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnilateSect f (l.eraseIdx n)) :
|
||||
((extractEquiv n).symm (a0, a)).eraseIdx n = a := by
|
||||
match l with
|
||||
|
|
@ -272,7 +294,7 @@ lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type} [(i : I) → Fintyp
|
|||
rw [eraseIdx, extractEquiv]
|
||||
simp
|
||||
|
||||
lemma toList_koszulSignInsert {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma toList_koszulSignInsert {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(l : List I) (a : CreateAnnilateSect f l) (x : (i : I) × f i) :
|
||||
koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x a.toList =
|
||||
|
|
@ -283,7 +305,7 @@ lemma toList_koszulSignInsert {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
simp only [koszulSignInsert, List.tail_cons, Fin.isValue]
|
||||
rw [ih]
|
||||
|
||||
lemma toList_koszulSign {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma toList_koszulSign {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(l : List I) (a : CreateAnnilateSect f l) :
|
||||
koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) a.toList =
|
||||
|
|
@ -296,7 +318,7 @@ lemma toList_koszulSign {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
congr 1
|
||||
rw [toList_koszulSignInsert]
|
||||
|
||||
lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
||||
(le1 : I → I → Prop) [DecidableRel le1](l : List I)
|
||||
(a : CreateAnnilateSect f l) :
|
||||
insertionSortEquiv (fun i j => le1 i.fst j.fst) a.toList =
|
||||
|
|
@ -331,8 +353,7 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
|
|||
· exact hij
|
||||
· exact hij
|
||||
· simp only [List.orderedInsert, hij, ↓reduceIte, List.unzip_snd, List.map_cons]
|
||||
have hn : ¬ le1 i.1 j.1 := hij
|
||||
simp only [hn, ↓reduceIte, List.cons.injEq, true_and]
|
||||
simp only [↓reduceIte, List.cons.injEq, true_and]
|
||||
simpa using ih'
|
||||
have h2 (l' : List (Σ i, f i)) :
|
||||
List.map (fun i => i.1) (List.insertionSort (fun i j => le1 i.fst j.fst) l') =
|
||||
|
|
@ -366,13 +387,16 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
|
|||
Fin.cast_trans, Fin.cast_eq_self, Fin.coe_cast]
|
||||
rfl
|
||||
|
||||
def sort (le1 : I → I → Prop) [DecidableRel le1] : CreateAnnilateSect f (List.insertionSort le1 l) :=
|
||||
/-- Given a section for `l` the corresponding section
|
||||
for `List.insertionSort le1 l`. -/
|
||||
def sort (le1 : I → I → Prop) [DecidableRel le1] :
|
||||
CreateAnnilateSect f (List.insertionSort le1 l) :=
|
||||
Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
|
||||
congr 1
|
||||
rw [← HepLean.List.insertionSortEquiv_get]
|
||||
simp))) a
|
||||
|
||||
lemma sort_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma sort_toList {I : Type} {f : I → Type}
|
||||
(le1 : I → I → Prop) [DecidableRel le1] (l : List I) (a : CreateAnnilateSect f l) :
|
||||
(a.sort le1).toList = List.insertionSort (fun i j => le1 i.fst j.fst) a.toList := by
|
||||
let l1 := List.insertionSort (fun i j => le1 i.fst j.fst) a.toList
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ open HepLean.List
|
|||
|
||||
noncomputable section
|
||||
|
||||
/-- The element of the free algebra `FreeAlgebra ℂ I` associated with a `List I`. -/
|
||||
def ofList {I : Type} (l : List I) (x : ℂ) : FreeAlgebra ℂ I :=
|
||||
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)
|
||||
|
||||
|
|
@ -76,6 +77,9 @@ lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [Dec
|
|||
rw [koszulSign_mul_self]
|
||||
simp
|
||||
|
||||
/-- The map of algebras from `FreeAlgebra ℂ I` to `FreeAlgebra ℂ (Σ i, f i)` taking
|
||||
the monomial `i` to the sum of elements in `(Σ i, f i)` above `i`, i.e. the sum of the fiber
|
||||
above `i`. -/
|
||||
def sumFiber {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
|
||||
FreeAlgebra ℂ I →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
|
||||
FreeAlgebra.lift ℂ fun i => ∑ (j : f i), FreeAlgebra.ι ℂ ⟨i, j⟩
|
||||
|
|
@ -84,6 +88,12 @@ lemma sumFiber_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
|
|||
sumFiber f (FreeAlgebra.ι ℂ i) = ∑ (b : f i), FreeAlgebra.ι ℂ ⟨i, b⟩ := by
|
||||
simp [sumFiber]
|
||||
|
||||
/-- Given a list `l : List I` the corresponding element of `FreeAlgebra ℂ (Σ i, f i)`
|
||||
by mapping each `i : I` to the sum of it's fiber in `Σ i, f i` and taking the product of the
|
||||
result.
|
||||
For example, in terms of creation and annihlation opperators,
|
||||
`[φ₁, φ₂, φ₃]` gets taken to `(φ₁⁰ + φ₁¹)(φ₂⁰ + φ₂¹)(φ₃⁰ + φ₃¹)`.
|
||||
-/
|
||||
def ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x : ℂ) :
|
||||
FreeAlgebra ℂ (Σ i, f i) :=
|
||||
sumFiber f (ofList l x)
|
||||
|
|
@ -155,7 +165,8 @@ lemma ofListLift_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x :
|
|||
|
||||
lemma koszulOrder_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListLift f l x) =
|
||||
(l : List I) (x : ℂ) :
|
||||
koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListLift f l x) =
|
||||
sumFiber f (koszulOrder le1 q (ofList l x)) := by
|
||||
rw [koszulOrder_ofList]
|
||||
rw [map_smul]
|
||||
|
|
|
|||
|
|
@ -16,6 +16,14 @@ namespace Wick
|
|||
|
||||
noncomputable section
|
||||
|
||||
/-- A map from the free algebra of fields `FreeAlgebra ℂ I` to an algebra `A`, to be
|
||||
thought of as the operator algebra is said to be an operator map if
|
||||
all super commutors of fields land in the center of `A`,
|
||||
if two fields are of a different grade then their super commutor lands on zero,
|
||||
and the `koszulOrder` (normal order) of any term with a super commutor of two fields present
|
||||
is zero.
|
||||
This can be thought as as a condtion on the operator algebra `A` as much as it can
|
||||
on `F`. -/
|
||||
class OperatorMap {A : Type} [Semiring A] [Algebra ℂ A] (q : I → Fin 2) (le1 : I → I → Prop)
|
||||
[DecidableRel le1] (F : FreeAlgebra ℂ I →ₐ[ℂ] A) : Prop where
|
||||
superCommute_mem_center : ∀ i j, F (superCommute q (FreeAlgebra.ι ℂ i) (FreeAlgebra.ι ℂ j)) ∈
|
||||
|
|
@ -135,9 +143,9 @@ lemma superCommute_koszulOrder_le_ofList {I : Type}
|
|||
rw [ofList_singleton, hn]
|
||||
simp
|
||||
· congr 1
|
||||
trans superCommuteCoefLE q le1 r i n
|
||||
· rw [superCommuteCoefLE, mul_assoc]
|
||||
refine superCommuteCoefLE_eq_get q le1 r i n ?_
|
||||
trans staticWickCoef q le1 r i n
|
||||
· rw [staticWickCoef, mul_assoc]
|
||||
refine staticWickCoef_eq_get q le1 r i n ?_
|
||||
simpa using hq
|
||||
|
||||
lemma koszulOrder_of_le_all_ofList {I : Type}
|
||||
|
|
@ -199,6 +207,8 @@ lemma le_all_mul_koszulOrder_ofList {I : Type}
|
|||
· rw [map_smul, map_smul]
|
||||
· exact fun j => hi j
|
||||
|
||||
/-- In the expansions of `F (FreeAlgebra.ι ℂ i * koszulOrder le1 q (ofList r x))`
|
||||
the ter multiplying `F ((koszulOrder le1 q) (ofList (optionEraseZ r i n) x))`. -/
|
||||
def superCommuteCenterOrder {I : Type}
|
||||
(q : I → Fin 2) (r : List I) (i : I)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
|
|
|
|||
|
|
@ -14,6 +14,8 @@ import Mathlib.Analysis.Complex.Basic
|
|||
|
||||
namespace Wick
|
||||
|
||||
/-- Given a grading map `q : I → Fin 2` and a list `l : List I` counts the parity of the number of
|
||||
elements in `l` which are of grade `1`. -/
|
||||
def grade {I : Type} (q : I → Fin 2) : (l : List I) → Fin 2
|
||||
| [] => 0
|
||||
| a :: l => if q a = grade q l then 0 else 1
|
||||
|
|
|
|||
|
|
@ -14,7 +14,8 @@ import HepLean.PerturbationTheory.Wick.Signs.SuperCommuteCoef
|
|||
namespace Wick
|
||||
open HepLean.List
|
||||
|
||||
|
||||
/-- The sign associated with inserting `r0` into `r` at the position `n`.
|
||||
That is the sign associated with commuting `r0` with `List.take n r`. -/
|
||||
def insertSign {I : Type} (q : I → Fin 2) (n : ℕ) (r0 : I) (r : List I) : ℂ :=
|
||||
superCommuteCoef q [r0] (List.take n r)
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,6 @@ def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin
|
|||
| [] => 1
|
||||
| a :: l => koszulSignInsert r q a l * koszulSign r q l
|
||||
|
||||
|
||||
lemma koszulSign_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
|
||||
(l : List I) : koszulSign r q l * koszulSign r q l = 1 := by
|
||||
induction l with
|
||||
|
|
@ -84,36 +83,6 @@ lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop
|
|||
rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
|
||||
exact h'
|
||||
|
||||
|
||||
|
||||
def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
|
||||
ℂ :=
|
||||
if le1 r0 r1 then 1 else
|
||||
if q r0 = 1 ∧ q r1 = 1 then -1 else 1
|
||||
|
||||
lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
||||
[DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
|
||||
if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
|
||||
simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
|
||||
imp_false]
|
||||
congr 1
|
||||
by_cases h0 : q r0 = 1
|
||||
· by_cases h1 : q r1 = 1
|
||||
· simp [h0, h1]
|
||||
· have h1 : q r1 = 0 := by omega
|
||||
simp [h0, h1]
|
||||
· have h0 : q r0 = 0 := by omega
|
||||
by_cases h1 : q r1 = 1
|
||||
· simp [h0, h1]
|
||||
· have h1 : q r1 = 0 := by omega
|
||||
simp [h0, h1]
|
||||
|
||||
lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
[IsTotal I le1] [IsTrans I le1] (r0 r1 : I) (r : List I) :
|
||||
koszulSignInsert le1 q r0 (r1 :: r) = (koszulSignCons q le1 r0 r1) *
|
||||
koszulSignInsert le1 q r0 r := by
|
||||
simp [koszulSignInsert, koszulSignCons]
|
||||
|
||||
lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
|
||||
koszulSign le1 q (List.insertIdx n i r) = insertSign q n i r
|
||||
|
|
@ -199,8 +168,6 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
rw [← insertionSortEquiv_get]
|
||||
simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
|
||||
simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
|
||||
have hms : (List.orderedInsert le1 r0 rs).get ⟨nro, by simp⟩ = r0 := by
|
||||
simp [nro]
|
||||
have hc1 : ni.castSucc < nro → ¬ le1 r0 i := by
|
||||
intro hninro
|
||||
rw [← hns]
|
||||
|
|
@ -231,5 +198,4 @@ lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
|||
· exact Nat.le_of_lt_succ h
|
||||
· exact Nat.le_of_lt_succ h
|
||||
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -98,14 +98,13 @@ lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I →
|
|||
simp
|
||||
|
||||
lemma koszulSignInsert_eq_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
[IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
|
||||
[IsTotal I le1] (r0 : I) (r : List I) :
|
||||
koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r) := by
|
||||
simp only [koszulSignInsert, Fin.isValue, and_self]
|
||||
have h1 : le1 r0 r0 := by
|
||||
simpa using IsTotal.total (r := le1) r0 r0
|
||||
simp [h1]
|
||||
|
||||
|
||||
lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(r0 : I) (r : List I) : koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
|
||||
grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
|
||||
|
|
@ -206,9 +205,39 @@ lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I
|
|||
· simp [orderedInsertPos]
|
||||
|
||||
lemma koszulSignInsert_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(i j : I) [IsTotal I le1] [IsTrans I le1] (r : List I) (n : ℕ) (hn : n ≤ r.length) :
|
||||
(i j : I) (r : List I) (n : ℕ) (hn : n ≤ r.length) :
|
||||
koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
|
||||
apply koszulSignInsert_eq_perm
|
||||
exact List.perm_insertIdx i r hn
|
||||
|
||||
/-- The difference in `koszulSignInsert` on inserting `r0` into `r` compared to
|
||||
into `r1 :: r` for any `r`. -/
|
||||
def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
|
||||
ℂ :=
|
||||
if le1 r0 r1 then 1 else
|
||||
if q r0 = 1 ∧ q r1 = 1 then -1 else 1
|
||||
|
||||
lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
|
||||
[DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
|
||||
if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
|
||||
simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
|
||||
imp_false]
|
||||
congr 1
|
||||
by_cases h0 : q r0 = 1
|
||||
· by_cases h1 : q r1 = 1
|
||||
· simp [h0, h1]
|
||||
· have h1 : q r1 = 0 := by omega
|
||||
simp [h0, h1]
|
||||
· have h0 : q r0 = 0 := by omega
|
||||
by_cases h1 : q r1 = 1
|
||||
· simp [h0, h1]
|
||||
· have h1 : q r1 = 0 := by omega
|
||||
simp [h0, h1]
|
||||
|
||||
lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
|
||||
(r0 r1 : I) (r : List I) :
|
||||
koszulSignInsert le1 q r0 (r1 :: r) = (koszulSignCons q le1 r0 r1) *
|
||||
koszulSignInsert le1 q r0 r := by
|
||||
simp [koszulSignInsert, koszulSignCons]
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -17,23 +17,25 @@ namespace Wick
|
|||
|
||||
open HepLean.List
|
||||
|
||||
def superCommuteCoefLE {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
/-- The sign that appears in the static version of Wicks theorem.
|
||||
This is actually equal to `superCommuteCoef q [r.get n] (r.take n)`, something
|
||||
which will be proved in a lemma. -/
|
||||
def staticWickCoef {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
[DecidableRel le1] (i : I) (n : Fin r.length) : ℂ :=
|
||||
koszulSign le1 q r *
|
||||
superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le1 r) n))
|
||||
(List.insertionSort le1 r)) *
|
||||
koszulSign le1 q (r.eraseIdx ↑n)
|
||||
|
||||
lemma superCommuteCoefLE_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
lemma staticWickCoef_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
[DecidableRel le1] (i : I) (n : Fin r.length)
|
||||
(hq : q i = q (r.get n)) :
|
||||
superCommuteCoefLE q le1 r i n =
|
||||
staticWickCoef q le1 r i n =
|
||||
koszulSign le1 q r *
|
||||
superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le1 r n))
|
||||
(List.insertionSort le1 r)) *
|
||||
koszulSign le1 q (r.eraseIdx ↑n) := by
|
||||
simp [superCommuteCoefLE, superCommuteCoef, grade, hq]
|
||||
|
||||
simp [staticWickCoef, superCommuteCoef, grade, hq]
|
||||
|
||||
lemma insertIdx_eraseIdx {I : Type} :
|
||||
(n : ℕ) → (r : List I) → (hn : n < r.length) →
|
||||
|
|
@ -47,11 +49,11 @@ lemma insertIdx_eraseIdx {I : Type} :
|
|||
List.eraseIdx_cons_succ, List.insertIdx_succ_cons, List.cons.injEq, true_and]
|
||||
exact insertIdx_eraseIdx n r _
|
||||
|
||||
lemma superCommuteCoefLE_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
lemma staticWickCoef_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
|
||||
[DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length)
|
||||
(heq : q i = q (r.get n)) :
|
||||
superCommuteCoefLE q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
|
||||
rw [superCommuteCoefLE_eq_q]
|
||||
staticWickCoef q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
|
||||
rw [staticWickCoef_eq_q]
|
||||
let r' := r.eraseIdx ↑n
|
||||
have hr : List.insertIdx n (r.get n) (r.eraseIdx n) = r := by
|
||||
exact insertIdx_eraseIdx n.1 r n.prop
|
||||
|
|
|
|||
|
|
@ -14,6 +14,10 @@ import HepLean.PerturbationTheory.Wick.Signs.Grade
|
|||
namespace Wick
|
||||
open HepLean.List
|
||||
|
||||
/-- Given two lists `la` and `lb` returns `-1` if they are both of grade `1` and
|
||||
`1` otherwise. This corresponds to the sign associated with the super commutator
|
||||
when commuting `la` and `lb` in the free algebra.
|
||||
In terms of physics it is `-1` if commuting two fermionic operators and `1` otherwise. -/
|
||||
def superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) : ℂ :=
|
||||
if grade q la = 1 ∧ grade q lb = 1 then - 1 else 1
|
||||
|
||||
|
|
@ -23,11 +27,17 @@ lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
|
|||
congr 1
|
||||
exact Eq.propIntro (fun a => id (And.symm a)) fun a => id (And.symm a)
|
||||
|
||||
def superCommuteLiftCoef {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
/-- Given a list `l : List (Σ i, f i)` and a list `r : List I` returns `-1` if the
|
||||
grade of `l` is `1` and the grade of `r` is `1` and `1` otherwise. This corresponds
|
||||
to the sign associated with the super commutator when commuting
|
||||
the lift of `l` and `r` (by summing over fibers) in the
|
||||
free algebra over `Σ i, f i`.
|
||||
In terms of physics it is `-1` if commuting two fermionic operators and `1` otherwise. -/
|
||||
def superCommuteLiftCoef {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) : ℂ :=
|
||||
(if grade (fun i => q i.fst) l = 1 ∧ grade q r = 1 then -1 else 1)
|
||||
|
||||
lemma superCommuteLiftCoef_empty {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma superCommuteLiftCoef_empty {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) :
|
||||
superCommuteLiftCoef q l [] = 1 := by
|
||||
simp [superCommuteLiftCoef]
|
||||
|
|
@ -79,5 +89,4 @@ lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I
|
|||
simp only [List.singleton_append]
|
||||
rw [superCommuteCoef_append]
|
||||
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
|||
(q : I → Fin 2)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A)
|
||||
(S : Contractions.Splitting f le1) :
|
||||
F (ofListLift f [] 1) = ∑ c : Contractions [],
|
||||
c.toCenterTerm f q le1 F S *
|
||||
|
|
|
|||
|
|
@ -14,6 +14,10 @@ namespace Wick
|
|||
|
||||
noncomputable section
|
||||
|
||||
/-- Given a grading `q : I → Fin 2` and a list `l : List I` the super-commutor on the free algebra
|
||||
`FreeAlgebra ℂ I` corresponding to commuting with `l`
|
||||
as a linear map from `MonoidAlgebra ℂ (FreeMonoid I)` (the module of lists in `I`)
|
||||
to itself. -/
|
||||
def superCommuteMonoidAlgebra {I : Type} (q : I → Fin 2) (l : List I) :
|
||||
MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] MonoidAlgebra ℂ (FreeMonoid I) :=
|
||||
Finsupp.lift (MonoidAlgebra ℂ (FreeMonoid I)) ℂ (List I)
|
||||
|
|
@ -24,6 +28,9 @@ def superCommuteMonoidAlgebra {I : Type} (q : I → Fin 2) (l : List I) :
|
|||
else
|
||||
- Finsupp.lsingle (R := ℂ) (r ++ l) 1)
|
||||
|
||||
/-- Given a grading `q : I → Fin 2` the super-commutor on the free algebra `FreeAlgebra ℂ I`
|
||||
as a linear map from `MonoidAlgebra ℂ (FreeMonoid I)` (the module of lists in `I`)
|
||||
to `FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I`. -/
|
||||
def superCommuteAlgebra {I : Type} (q : I → Fin 2) :
|
||||
MonoidAlgebra ℂ (FreeMonoid I) →ₗ[ℂ] FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
|
||||
Finsupp.lift (FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I) ℂ (List I) fun l =>
|
||||
|
|
@ -31,6 +38,8 @@ def superCommuteAlgebra {I : Type} (q : I → Fin 2) :
|
|||
∘ₗ superCommuteMonoidAlgebra q l
|
||||
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap)
|
||||
|
||||
/-- Given a grading `q : I → Fin 2` the super-commutor on the free algebra `FreeAlgebra ℂ I`
|
||||
as a bi-linear map. -/
|
||||
def superCommute {I : Type} (q : I → Fin 2) :
|
||||
FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I →ₗ[ℂ] FreeAlgebra ℂ I :=
|
||||
superCommuteAlgebra q
|
||||
|
|
@ -193,6 +202,11 @@ lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (
|
|||
mul_neg, smul_add, one_smul, smul_neg]
|
||||
abel
|
||||
|
||||
/-- Given two lists `la lb : List I`, in the expansion of the supercommutor of `la` and `lb`
|
||||
via elements of `lb`the term associated with the `n`th element.
|
||||
E.g. in the commutator
|
||||
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
|
||||
and for `n=1` is `b [a, c]`. -/
|
||||
def superCommuteSplit {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ)
|
||||
(hn : n < lb.length) : FreeAlgebra ℂ I :=
|
||||
superCommuteCoef q la (List.take n lb) •
|
||||
|
|
@ -268,7 +282,6 @@ lemma ofListLift_ofList_superCommute' {I : Type}
|
|||
· simp [hq, superCommuteCoef]
|
||||
· simp [hq]
|
||||
|
||||
|
||||
lemma superCommute_ofList_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
|
||||
|
|
@ -322,17 +335,19 @@ lemma ofList_ofListLift_superCommute {I : Type} {f : I → Type} [∀ i, Fintype
|
|||
lemma ofListLift_ofList_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
|
||||
ofListLift f r y * ofList l x = superCommuteLiftCoef q l r • (ofList l x * ofListLift f r y)
|
||||
- superCommuteLiftCoef q l r • superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
|
||||
- superCommuteLiftCoef q l r •
|
||||
superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
|
||||
rw [ofList_ofListLift_superCommute, superCommuteLiftCoef]
|
||||
by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
|
||||
· simp [hq]
|
||||
· simp [hq]
|
||||
|
||||
lemma superCommuteLiftCoef_append {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
lemma superCommuteLiftCoef_append {I : Type} {f : I → Type}
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r1 r2 : List I) :
|
||||
superCommuteLiftCoef q l (r1 ++ r2) = superCommuteLiftCoef q l r1 * superCommuteLiftCoef q l r2 := by
|
||||
simp only [superCommuteLiftCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
|
||||
mul_ite, mul_neg, mul_one]
|
||||
superCommuteLiftCoef q l (r1 ++ r2) =
|
||||
superCommuteLiftCoef q l r1 * superCommuteLiftCoef q l r2 := by
|
||||
simp only [superCommuteLiftCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one,
|
||||
imp_false, mul_ite, mul_neg, mul_one]
|
||||
by_cases hla : grade (fun i => q i.1) l = 1
|
||||
· by_cases hlb : grade q r1 = 1
|
||||
· by_cases hlc : grade q r2 = 1
|
||||
|
|
@ -351,6 +366,12 @@ lemma superCommuteLiftCoef_append {I : Type} {f : I → Type} [∀ i, Fintype (f
|
|||
omega
|
||||
simp [ha]
|
||||
|
||||
/-- Given two lists `l : List (Σ i, f i)` and `r : List I`, on
|
||||
in the expansion of the supercommutor of `l` and the lift of `r`
|
||||
via elements of `r`the term associated with the `n`th element.
|
||||
E.g. in the commutator
|
||||
`[a, bc] = [a, b] c + b [a, c] ` the `superCommuteSplit` for `n=0` is `[a, b] c`
|
||||
and for `n=1` is `b [a, c]`. -/
|
||||
def superCommuteLiftSplit {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
|
||||
(q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
|
||||
(hn : n < r.length) : FreeAlgebra ℂ (Σ i, f i) :=
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue