refactor: Update create annihilate section
This commit is contained in:
jstoobysmith
parent
bbd9be965b
commit
03b0c8cc15
1 changed files with 79 additions and 73 deletions
|
|
@ -12,36 +12,45 @@ import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
|
|||
|
||||
namespace Wick
|
||||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
/-- The sections of `Σ i, f i` over a list `l : List I`.
|
||||
/-- The sections of `Σ i, f i` over a list `l : List 𝓕`.
|
||||
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 :=
|
||||
def CreateAnnilateSect {𝓕 : Type} (f : 𝓕 → Type) (l : List 𝓕) : 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)
|
||||
section basic_defs
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {l : List 𝓕} (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
|
||||
def tail : {l : List 𝓕} → (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⟩
|
||||
def head {i : 𝓕} (a : CreateAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
|
||||
|
||||
end basic_defs
|
||||
|
||||
section toList_basic
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic)
|
||||
{l : List 𝓕} (a : CreateAnnilateSect f l)
|
||||
|
||||
/-- The list `List (Σ i, f i)` defined by `a`. -/
|
||||
def toList : {l : List I} → (a : CreateAnnilateSect f l) → List (Σ i, f i)
|
||||
def toList : {l : List 𝓕} → (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
|
||||
|
|
@ -50,18 +59,15 @@ 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
|
||||
lemma toList_tail : {l : List 𝓕} → (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)) :
|
||||
lemma toList_cons {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
|
||||
|
|
@ -80,46 +86,48 @@ 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
|
||||
lemma toList_grade :
|
||||
FieldStatistic.ofList (fun i => q i.fst) a.toList = fermionic ↔
|
||||
FieldStatistic.ofList q l = fermionic := by
|
||||
induction l with
|
||||
| nil =>
|
||||
simp [toList]
|
||||
| cons i r ih =>
|
||||
simp only [grade, Fin.isValue, ite_eq_right_iff, zero_ne_one, imp_false]
|
||||
simp only [ofList, Fin.isValue, ite_eq_right_iff, zero_ne_one, imp_false]
|
||||
have ih' := ih (fun i => a i.succ)
|
||||
have h1 : grade (fun i => q i.fst) a.tail.toList = grade q r := by
|
||||
by_cases h : grade q r = 1
|
||||
have h1 : ofList (fun i => q i.fst) a.tail.toList = ofList q r := by
|
||||
by_cases h : ofList q r = fermionic
|
||||
· simp_all
|
||||
· have h0 : grade q r = 0 := by
|
||||
omega
|
||||
· have h0 : ofList q r = bosonic := (neq_fermionic_iff_eq_bosonic (ofList q r)).mp h
|
||||
rw [h0] at ih'
|
||||
simp only [Fin.isValue, zero_ne_one, iff_false] at ih'
|
||||
have h0' : grade (fun i => q i.fst) a.tail.toList = 0 := by
|
||||
simp only [List.tail_cons, tail, Fin.isValue]
|
||||
omega
|
||||
simp only [reduceCtorEq, iff_false, neq_fermionic_iff_eq_bosonic] at ih'
|
||||
have h0' : ofList (fun i => q i.fst) a.tail.toList = bosonic := ih'
|
||||
rw [h0, h0']
|
||||
rw [h1]
|
||||
|
||||
@[simp]
|
||||
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)
|
||||
lemma toList_grade_take (q : 𝓕 → FieldStatistic) :
|
||||
(r : List 𝓕) → (a : CreateAnnilateSect f r) → (n : ℕ) →
|
||||
ofList (fun i => q i.fst) (List.take n a.toList) = ofList q (List.take n r)
|
||||
| [], _, _ => by
|
||||
simp [toList]
|
||||
| i :: r, a, 0 => by
|
||||
simp
|
||||
| i :: r, a, Nat.succ n => by
|
||||
simp only [grade, Fin.isValue]
|
||||
simp only [ofList, Fin.isValue]
|
||||
rw [toList_grade_take q r a.tail n]
|
||||
|
||||
end toList_basic
|
||||
|
||||
section toList_erase
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} {l : List 𝓕}
|
||||
|
||||
/-- 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 ≃
|
||||
def extractEquiv (n : Fin l.length) : CreateAnnilateSect f l ≃
|
||||
f (l.get n) × CreateAnnilateSect f (l.eraseIdx n) := by
|
||||
match l with
|
||||
| [] => exact Fin.elim0 n
|
||||
|
|
@ -153,8 +161,8 @@ def extractEquiv {I : Type} {f : I → Type} {l : List I}
|
|||
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}
|
||||
{l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreateAnnilateSect f (l.eraseIdx n)) :
|
||||
lemma extractEquiv_symm_toList_get_same (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
|
||||
| [] => exact Fin.elim0 n
|
||||
|
|
@ -173,12 +181,12 @@ lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type}
|
|||
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) :=
|
||||
def eraseIdx (a : CreateAnnilateSect f l) (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)) :
|
||||
lemma eraseIdx_zero_tail {i : 𝓕} (a : CreateAnnilateSect f (i :: l)) :
|
||||
(eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
|
||||
a.tail := by
|
||||
simp only [List.length_cons, Fin.val_zero, List.eraseIdx_cons_zero, eraseIdx, List.get_eq_getElem,
|
||||
|
|
@ -187,8 +195,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)
|
||||
lemma eraseIdx_succ_head {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]
|
||||
simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, List.eraseIdx_cons_succ,
|
||||
|
|
@ -209,8 +216,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)
|
||||
lemma eraseIdx_succ_tail {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
|
||||
match l with
|
||||
|
|
@ -272,8 +278,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) →
|
||||
lemma eraseIdx_toList : {l : List 𝓕} → {n : Fin l.length} → (a : CreateAnnilateSect f l) →
|
||||
(eraseIdx a n).toList = a.toList.eraseIdx n
|
||||
| [], n, _ => Fin.elim0 n
|
||||
| r0 :: r, ⟨0, h⟩, a => by
|
||||
|
|
@ -295,22 +300,25 @@ lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type}
|
|||
rw [eraseIdx, extractEquiv]
|
||||
simp
|
||||
|
||||
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 =
|
||||
koszulSignInsert le1 q x.1 l := by
|
||||
end toList_erase
|
||||
|
||||
section toList_sign_conditions
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
{l : List 𝓕} (a : CreateAnnilateSect f l)
|
||||
|
||||
lemma toList_koszulSignInsert (x : (i : 𝓕) × f i) :
|
||||
koszulSignInsert (fun i => q i.fst) (fun i j => le i.fst j.fst) x a.toList =
|
||||
koszulSignInsert q le x.1 l := by
|
||||
induction l with
|
||||
| nil => simp [koszulSignInsert]
|
||||
| cons b l ih =>
|
||||
simp only [koszulSignInsert, List.tail_cons, Fin.isValue]
|
||||
rw [ih]
|
||||
|
||||
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 =
|
||||
koszulSign le1 q l := by
|
||||
lemma toList_koszulSign :
|
||||
koszulSign (fun i => q i.fst) (fun i j => le i.fst j.fst) a.toList =
|
||||
koszulSign q le l := by
|
||||
induction l with
|
||||
| nil => simp [koszulSign]
|
||||
| cons i l ih =>
|
||||
|
|
@ -319,11 +327,9 @@ lemma toList_koszulSign {I : Type} {f : I → Type}
|
|||
congr 1
|
||||
rw [toList_koszulSignInsert]
|
||||
|
||||
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 =
|
||||
(Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le1 l).trans
|
||||
lemma insertionSortEquiv_toList :
|
||||
insertionSortEquiv (fun i j => le i.fst j.fst) a.toList =
|
||||
(Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le l).trans
|
||||
(Fin.castOrderIso (by simp)).toEquiv) := by
|
||||
induction l with
|
||||
| nil =>
|
||||
|
|
@ -341,13 +347,13 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
simp only [Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.cast_trans,
|
||||
Fin.coe_cast]
|
||||
have h2' (i : Σ i, f i) (l' : List (Σ i, f i)) :
|
||||
List.map (fun i => i.1) (List.orderedInsert (fun i j => le1 i.fst j.fst) i l') =
|
||||
List.orderedInsert le1 i.1 (List.map (fun i => i.1) l') := by
|
||||
List.map (fun i => i.1) (List.orderedInsert (fun i j => le i.fst j.fst) i l') =
|
||||
List.orderedInsert le i.1 (List.map (fun i => i.1) l') := by
|
||||
induction l' with
|
||||
| nil =>
|
||||
simp [HepLean.List.orderedInsertEquiv]
|
||||
| cons j l' ih' =>
|
||||
by_cases hij : (fun i j => le1 i.fst j.fst) i j
|
||||
by_cases hij : (fun i j => le i.fst j.fst) i j
|
||||
· rw [List.orderedInsert_of_le]
|
||||
· erw [List.orderedInsert_of_le]
|
||||
· simp
|
||||
|
|
@ -357,8 +363,8 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
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') =
|
||||
List.insertionSort le1 (List.map (fun i => i.1) l') := by
|
||||
List.map (fun i => i.1) (List.insertionSort (fun i j => le i.fst j.fst) l') =
|
||||
List.insertionSort le (List.map (fun i => i.1) l') := by
|
||||
induction l' with
|
||||
| nil =>
|
||||
simp [HepLean.List.orderedInsertEquiv]
|
||||
|
|
@ -370,10 +376,10 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
rw [HepLean.List.orderedInsertEquiv_congr _ _ _ (h2 _)]
|
||||
simp only [List.length_cons, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
|
||||
Fin.cast_trans, Fin.coe_cast]
|
||||
have h3 : (List.insertionSort le1 (List.map (fun i => i.1) a.tail.toList)) =
|
||||
List.insertionSort le1 l := by
|
||||
have h3 : (List.insertionSort le (List.map (fun i => i.1) a.tail.toList)) =
|
||||
List.insertionSort le l := by
|
||||
congr
|
||||
have h3' (l : List I) (a : CreateAnnilateSect f l) :
|
||||
have h3' (l : List 𝓕) (a : CreateAnnilateSect f l) :
|
||||
List.map (fun i => i.1) a.toList = l := by
|
||||
induction l with
|
||||
| nil => rfl
|
||||
|
|
@ -390,18 +396,17 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type}
|
|||
|
||||
/-- 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
|
||||
def sort :
|
||||
CreateAnnilateSect f (List.insertionSort le l) :=
|
||||
Equiv.piCongr (HepLean.List.insertionSortEquiv le l) (fun i => (Equiv.cast (by
|
||||
congr 1
|
||||
rw [← HepLean.List.insertionSortEquiv_get]
|
||||
simp))) a
|
||||
|
||||
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
|
||||
let l2 := (a.sort le1).toList
|
||||
lemma sort_toList :
|
||||
(a.sort le).toList = List.insertionSort (fun i j => le i.fst j.fst) a.toList := by
|
||||
let l1 := List.insertionSort (fun i j => le i.fst j.fst) a.toList
|
||||
let l2 := (a.sort le).toList
|
||||
symm
|
||||
change l1 = l2
|
||||
have hlen : l1.length = l2.length := by
|
||||
|
|
@ -415,7 +420,7 @@ lemma sort_toList {I : Type} {f : I → Type}
|
|||
OrderIso.toEquiv_symm, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
|
||||
Fin.cast_trans, Fin.cast_eq_self, id_eq, eq_mpr_eq_cast, Fin.coe_cast, Sigma.mk.inj_iff]
|
||||
apply And.intro
|
||||
· have h1 := congrFun (HepLean.List.insertionSortEquiv_get (r := le1) l) (Fin.cast (by simp) i)
|
||||
· have h1 := congrFun (HepLean.List.insertionSortEquiv_get (r := le) l) (Fin.cast (by simp) i)
|
||||
rw [← h1]
|
||||
simp
|
||||
· simp only [List.get_eq_getElem, sort, Equiv.piCongr, Equiv.trans_apply, Fin.coe_cast,
|
||||
|
|
@ -426,6 +431,7 @@ lemma sort_toList {I : Type} {f : I → Type}
|
|||
rw [hget]
|
||||
simp
|
||||
|
||||
end toList_sign_conditions
|
||||
end CreateAnnilateSect
|
||||
|
||||
end Wick
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue