refactor: Static Wick coef

HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean

@@ -61,7 +61,7 @@ lemma koszulSignInsert_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic)
     rw [koszulSignInsert, koszulSignInsert]
     rw [koszulSignInsert_erase_boson q le r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
 
-lemma koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le :𝓕 → 𝓕 → Prop)
+lemma koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop)
     [DecidableRel le] :
     (r : List 𝓕) → (n : Fin r.length) → (heq : q (r.get n) = bosonic) →
     koszulSign q le (r.eraseIdx n) = koszulSign q le r
@@ -78,20 +78,17 @@ lemma koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le :
     simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
       List.eraseIdx_cons_succ]
     intro h'
-    rw [koszulSign, koszulSign]
-    rw [koszulSign_erase_boson q le r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
+    rw [koszulSign, koszulSign, koszulSign_erase_boson q le r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
     congr 1
     rw [koszulSignInsert_erase_boson q le r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
     exact h'
 
 lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (i : 𝓕) :
     (r : List 𝓕) → (n : ℕ) → (hn : n ≤ r.length) →
-    koszulSign q le (List.insertIdx n i r) = insertSign q n i r
-      * koszulSign q le r
-      * insertSign q (insertionSortEquiv le (List.insertIdx n i r) ⟨n, by
+    koszulSign q le (List.insertIdx n i r) = insertSign q n i r * koszulSign q le r *
+      insertSign q (insertionSortEquiv le (List.insertIdx n i r) ⟨n, by
         rw [List.length_insertIdx _ _ hn]
-        omega⟩) i
-        (List.insertionSort le (List.insertIdx n i r))
+        omega⟩) i (List.insertionSort le (List.insertIdx n i r))
   | [], 0, h => by
     simp [koszulSign, insertSign, superCommuteCoef, koszulSignInsert]
   | [], n + 1, h => by
@@ -188,11 +185,9 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (i : 𝓕) :
       simp only [hc1 hn, ↓reduceIte]
       rw [superCommuteCoef_comm]
     · simp only [hn, ↓reduceIte, Fin.val_succ]
-      rw [insertSign_insert_lt]
-      rw [← mul_assoc]
+      rw [insertSign_insert_lt, ← mul_assoc]
       congr 1
-      rw [superCommuteCoef_mul_self]
-      rw [koszulSignCons]
+      rw [superCommuteCoef_mul_self, koszulSignCons]
       simp only [hc2 hn, ↓reduceIte]
       exact Nat.le_of_not_lt hn
       exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le rs r0)

HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean

@@ -17,28 +17,29 @@ namespace Wick
 
 open HepLean.List
 
+open FieldStatistic
+
+variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le :𝓕 → 𝓕 → Prop) [DecidableRel le]
+
 /-- 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)
+def staticWickCoef (r : List 𝓕) (i : 𝓕) (n : Fin r.length) : ℂ :=
+  koszulSign q le r *
+  superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le r) n))
+    (List.insertionSort le r)) *
+  koszulSign q le (r.eraseIdx ↑n)
 
-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)
+lemma staticWickCoef_eq_q (r : List 𝓕) (i : 𝓕) (n : Fin r.length)
     (hq : q i = q (r.get 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 [staticWickCoef, superCommuteCoef, grade, hq]
+    staticWickCoef q le r i n =
+    koszulSign q le r *
+    superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le r n))
+      (List.insertionSort le r)) *
+    koszulSign q le (r.eraseIdx ↑n) := by
+  simp [staticWickCoef, superCommuteCoef, ofList, hq]
 
-lemma insertIdx_eraseIdx {I : Type} :
-    (n : ℕ) → (r : List I) → (hn : n < r.length) →
+lemma insertIdx_eraseIdx {I : Type} : (n : ℕ) → (r : List I) → (hn : n < r.length) →
     List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
   | n, [], hn => by
     simp at hn
@@ -49,10 +50,9 @@ lemma insertIdx_eraseIdx {I : Type} :
       List.eraseIdx_cons_succ, List.insertIdx_succ_cons, List.cons.injEq, true_and]
     exact insertIdx_eraseIdx n r _
 
-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)
+lemma staticWickCoef_eq_get [IsTotal 𝓕 le] [IsTrans 𝓕 le] (r : List 𝓕) (i : 𝓕) (n : Fin r.length)
     (heq : q i = q (r.get n)) :
-    staticWickCoef q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
+    staticWickCoef q le 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
@@ -61,7 +61,7 @@ lemma staticWickCoef_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
     lhs
     lhs
     rw [← hr]
-    rw [koszulSign_insertIdx q le1 (r.get n) ((r.eraseIdx ↑n)) n (by
+    rw [koszulSign_insertIdx q le (r.get n) ((r.eraseIdx ↑n)) n (by
       rw [List.length_eraseIdx]
       simp only [Fin.is_lt, ↓reduceIte]
       omega)]