Merge pull request #129 from HEPLean/Tensors_with_indices

feat: contr commute with append index lists

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -472,6 +472,29 @@ lemma countId_cons_eq_two {I : Index X} :
     (l.cons I).countId I = 2 ↔ l.countId I = 1 := by
   simp [countId]
 
+lemma countId_congr {I J : Index X} (h : I.id = J.id) : l.countId I = l.countId J := by
+  simp [countId, h]
+
+lemma countId_neq_zero_mem (I : Index X) (h : l.countId I ≠ 0) :
+    ∃ I', I' ∈ l.val ∧ I.id = I'.id := by
+  rw [countId_eq_length_filter] at h
+  have h' := List.isEmpty_iff_length_eq_zero.mp.mt h
+  simp only at h'
+  have h'' := eq_false_of_ne_true h'
+  rw [List.isEmpty_false_iff_exists_mem] at h''
+  obtain ⟨I', hI'⟩ := h''
+  simp only [List.mem_filter, decide_eq_true_eq] at hI'
+  exact ⟨I', hI'⟩
+
+lemma countId_mem (I : Index X) (hI : I ∈ l.val) : l.countId I ≠ 0 := by
+  rw [countId_eq_length_filter]
+  by_contra hn
+  rw [List.length_eq_zero] at hn
+  have hIme : I ∈ List.filter (fun J => decide (I.id = J.id)) l.val := by
+    simp [hI]
+  rw [hn] at hIme
+  simp at hIme
+
 /-!
 
 ## Filter id

HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean

@@ -177,6 +177,12 @@ lemma countColorCond_cons_neg (l : IndexList 𝓒.Color) (I I' : Index 𝓒.Colo
     exact id (Ne.symm hid)
   rw [countColorCond, countColorCond, h1]
 
+lemma countColorCond_of_filter_eq (l l2 : IndexList 𝓒.Color) {I : Index 𝓒.Color}
+    (hf : l.val.filter (fun J => I.id = J.id) = l2.val.filter (fun J => I.id = J.id))
+    (h1 : countColorCond l I) : countColorCond l2 I := by
+  rw [countColorCond, ← hf]
+  exact h1
+
 lemma color_eq_of_countColorCond_cons_pos (l : IndexList 𝓒.Color) (I I' : Index 𝓒.Color)
     (hl : countColorCond (l.cons I) I') (hI : I.id = I'.id) : I.toColor = I'.toColor ∨
     I.toColor = 𝓒.τ I'.toColor := by

HepLean/SpaceTime/LorentzTensor/IndexNotation/ColorIndexList/Append.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Basic
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Contraction
 import HepLean.SpaceTime.LorentzTensor.Basic
 import Init.Data.List.Lemmas
 /-!
@@ -95,8 +96,79 @@ lemma swap (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
     simpa using h'.1
   · exact ColorCond.swap h'.1 h'.2
 
-/-! TODO: Show that `AppendCond l l2` implies `AppendCond l.contr l2.contr`. -/
-/-! TODO: Show that `(l1.contr ++[h.contr] l2.contr).contr = (l1 ++[h] l2)` -/
+/-- If `AppendCond l l2` then `AppendCond l.contr l2`. Note that the inverse
+  is generally not true. -/
+lemma contr_left (h : AppendCond l l2) : AppendCond l.contr l2 := by
+  apply And.intro (append_withDual_eq_withUniqueDual_contr_left l.toIndexList l2.toIndexList h.1)
+  · rw [ColorCond.iff_countColorCond_all]
+    · simp only [append_val, countId_append, List.all_append, Bool.and_eq_true, List.all_eq_true,
+      decide_eq_true_eq]
+      apply And.intro
+      · intro I hI hI2
+        have hIC1 : l.contr.countId I = 1 :=
+          mem_contrIndexList_countId_contrIndexList l.toIndexList hI
+        have hIC2 : l2.countId I = 1 := by omega
+        obtain ⟨I1, hI1, hI1'⟩ := countId_neq_zero_mem l.contr I (by omega)
+        apply ColorCond.countColorCond_of_filter_eq (l.toIndexList ++ l2.toIndexList) _ _
+        · have h2 := h.2
+          rw [ColorCond.iff_countColorCond_all] at h2
+          · simp only [append_val, countId_append, List.all_append, Bool.and_eq_true,
+            List.all_eq_true, decide_eq_true_eq] at h2
+            have hn := h2.1 I (List.mem_of_mem_filter hI)
+            have hc : l.countId I + l2.countId I = 2 := by
+              rw [contr, countId_contrIndexList_eq_one_iff_countId_eq_one] at hIC1
+              omega
+            exact hn hc
+          · exact h.1
+        · erw [List.filter_append, List.filter_append]
+          apply congrFun
+          apply congrArg
+          rw [countId_congr _ hI1'] at hIC1
+          rw [hI1', filter_id_of_countId_eq_one_mem l.contr hI1 hIC1]
+          simp [contr, contrIndexList] at hI1
+          exact filter_id_of_countId_eq_one_mem l hI1.1 hI1.2
+      · intro I hI1 hI2
+        by_cases hICz : l2.countId I = 0
+        · rw [hICz] at hI2
+          have hx : l.contr.countId I ≤ 1 := countId_contrIndexList_le_one l.toIndexList I
+          omega
+        · by_cases hICo : l2.countId I = 1
+          · have hIC1 : l.contr.countId I = 1 := by omega
+            obtain ⟨I1, hI', hI1'⟩ := countId_neq_zero_mem l.contr I (by omega)
+            apply ColorCond.countColorCond_of_filter_eq (l.toIndexList ++ l2.toIndexList) _ _
+            · have h2 := h.2
+              rw [ColorCond.iff_countColorCond_all] at h2
+              · simp only [append_val, countId_append, List.all_append, Bool.and_eq_true,
+                List.all_eq_true, decide_eq_true_eq] at h2
+                refine h2.2 I hI1 ?_
+                rw [contr, countId_contrIndexList_eq_one_iff_countId_eq_one] at hIC1
+                omega
+              · exact h.1
+            · erw [List.filter_append, List.filter_append]
+              apply congrFun
+              apply congrArg
+              rw [hI1']
+              rw [countId_congr _ hI1'] at hIC1
+              rw [filter_id_of_countId_eq_one_mem l.contr hI' hIC1]
+              simp [contr, contrIndexList] at hI'
+              exact filter_id_of_countId_eq_one_mem l hI'.1 hI'.2
+          · have hICt : l2.countId I = 2 := by
+              omega
+            apply ColorCond.countColorCond_of_filter_eq l2 _ _
+            · have hl2C := l2.dual_color
+              rw [ColorCond.iff_countColorCond_all] at hl2C
+              · simp only [List.all_eq_true, decide_eq_true_eq] at hl2C
+                exact hl2C I hI1 hICt
+              · exact l2.unique_duals.symm
+            · erw [List.filter_append]
+              rw [filter_id_of_countId_eq_zero' l.contr.toIndexList]
+              · rfl
+              · omega
+    · exact append_withDual_eq_withUniqueDual_contr_left l.toIndexList l2.toIndexList h.1
+
+lemma contr_right (h : AppendCond l l2) : AppendCond l l2.contr := (contr_left h.symm).symm
+
+lemma contr (h : AppendCond l l2) : AppendCond l.contr l2.contr := contr_left (contr_right h)
 
 lemma of_eq (h1 : l.withUniqueDual = l.withDual)
     (h2 : l2.withUniqueDual = l2.withDual)
@@ -127,7 +199,54 @@ lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndex
   rw [ColorCond.iff_bool]
   simp
 
+lemma countId_contr_fst_eq_zero_mem_snd (h : AppendCond l l2) {I : Index 𝓒.Color}
+    (hI : I ∈ l2.val) : l.contr.countId I = 0 ↔ l.countId I = 0 := by
+  rw [countId_contr_eq_zero_iff]
+  refine Iff.intro (fun h' => ?_) (fun h' => ?_)
+  · have h1 := h.1
+    rw [withUniqueDual_eq_withDual_iff_countId_leq_two'] at h1
+    have h1I := h1 I
+    simp at h1I
+    have h2 : l2.countId I ≠ 0 := countId_mem l2.toIndexList I hI
+    omega
+  · simp [h']
+
+lemma countId_contr_snd_eq_zero_mem_fst (h : AppendCond l l2) {I : Index 𝓒.Color}
+    (hI : I ∈ l.val) : l2.contr.countId I = 0 ↔ l2.countId I = 0 := by
+  exact countId_contr_fst_eq_zero_mem_snd h.symm hI
+
 end AppendCond
 
+lemma append_contr_left (h : AppendCond l l2) :
+    (l.contr ++[h.contr_left] l2).contr = (l ++[h] l2).contr := by
+  apply ext
+  simp only [contr, append_toIndexList]
+  rw [contrIndexList_append_eq_filter, contrIndexList_append_eq_filter,
+    contrIndexList_contrIndexList]
+  apply congrArg
+  apply List.filter_congr
+  intro I hI
+  simp only [decide_eq_decide]
+  simp [contrIndexList] at hI
+  exact AppendCond.countId_contr_fst_eq_zero_mem_snd h hI.1
+
+lemma append_contr_right (h : AppendCond l l2) :
+    (l ++[h.contr_right] l2.contr).contr = (l ++[h] l2).contr := by
+  apply ext
+  simp [contr]
+  rw [contrIndexList_append_eq_filter, contrIndexList_append_eq_filter,
+    contrIndexList_contrIndexList]
+  apply congrFun
+  apply congrArg
+  apply List.filter_congr
+  intro I hI
+  simp only [decide_eq_decide]
+  simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at hI
+  exact AppendCond.countId_contr_snd_eq_zero_mem_fst h hI.1
+
+lemma append_contr (h : AppendCond l l2) :
+    (l.contr ++[h.contr] l2.contr).contr = (l ++[h] l2).contr := by
+  rw [append_contr_left, append_contr_right]
+
 end ColorIndexList
 end IndexNotation

HepLean/SpaceTime/LorentzTensor/IndexNotation/ColorIndexList/Basic.lean

@@ -9,15 +9,13 @@ import HepLean.SpaceTime.LorentzTensor.Basic
 import Init.Data.List.Lemmas
 /-!
 
-# Index lists and color
+# Color index lists
 
-The main definiton of this file is `ColorIndexList`. This type defines the
-permissible index lists which can be used for a tensor. These are lists of indices for which
-every index with a dual has a unique dual, and the color of that dual (when it exists) is dual
-to the color of the index.
+A color index list is defined as a list of indices with two constraints. The first is that
+if an index has a dual, that dual is unique. The second is that if an index has a dual, the
+color of that dual is dual to the color of the index.
 
-We also define `AppendCond`, which is a condition on two `ColorIndexList`s which allows them to be
-appended to form a new `ColorIndexList`.
+The indices of a tensor are required to be of this type.
 
 -/
 
@@ -199,5 +197,15 @@ decreasing_by {
     exact h1
 }
 
+/-!
+
+## CountId for `ColorIndexList`
+
+-/
+
+lemma countId_le_two (l : ColorIndexList 𝓒) (I : Index 𝓒.Color) :
+    l.countId I ≤ 2 :=
+  (withUniqueDual_eq_withDual_iff_countId_leq_two' l.toIndexList).mp l.unique_duals.symm I
+
 end ColorIndexList
 end IndexNotation

HepLean/SpaceTime/LorentzTensor/IndexNotation/ColorIndexList/Contraction.lean

@@ -126,6 +126,21 @@ lemma countId_contr_le_one_of_countId (I : Index 𝓒.Color) (hI1 : l.countId I
     apply (List.countP_le_length _).trans
     rfl
 
+lemma countId_contr_eq_zero_iff (I : Index 𝓒.Color) :
+    l.contr.countId I = 0 ↔ l.countId I = 0 ∨ l.countId I = 2 := by
+  by_cases hI : l.contr.countId I = 1
+  · have hI' := hI
+    erw [countId_contrIndexList_eq_one_iff_countId_eq_one] at hI'
+    omega
+  · have hI' := hI
+    erw [countId_contrIndexList_eq_one_iff_countId_eq_one] at hI'
+    have hI2 := l.countId_le_two I
+    have hI3 := l.countId_contrIndexList_le_one I
+    have hI3 : l.contr.countId I = 0 := by
+      simp_all only [contr]
+      omega
+    omega
+
 /-!
 
 ## Contract equiv

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -319,8 +319,7 @@ lemma mem_contrIndexList_countId_contrIndexList {I : Index X} (h : I ∈ l.contr
       exact mem_contrIndexList_countId l h
 
 lemma countId_contrIndexList_zero_of_countId (I : Index X)
-    (h : l.countId I = 0) :
-    l.contrIndexList.countId I = 0 := by
+    (h : l.countId I = 0) : l.contrIndexList.countId I = 0 := by
   trans (l.val.filter (fun J => I.id = J.id)).countP
     (fun i => l.val.countP (fun j => i.id = j.id) = 1)
   · rw [contrIndexList]
@@ -334,6 +333,63 @@ lemma countId_contrIndexList_zero_of_countId (I : Index X)
     rw [h]
     simp only [List.countP_nil]
 
+lemma countId_contrIndexList_le_one (I : Index X) :
+    l.contrIndexList.countId I ≤ 1 := by
+  by_cases h : l.contrIndexList.countId I = 0
+  · simp [h]
+  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I h
+    rw [countId_congr l.contrIndexList hI2, mem_contrIndexList_countId_contrIndexList l hI1]
+
+lemma countId_contrIndexList_eq_one_iff_countId_eq_one (I : Index X) :
+    l.contrIndexList.countId I = 1 ↔ l.countId I = 1 := by
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I (by omega)
+    simp [contrIndexList] at hI1
+    rw [countId_congr l hI2]
+    exact hI1.2
+  · obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l I (by omega)
+    rw [countId_congr l hI2] at h
+    rw [countId_congr _ hI2]
+    refine mem_contrIndexList_countId_contrIndexList l ?_
+    simp [contrIndexList]
+    exact ⟨hI1, h⟩
+
+lemma countId_contrIndexList_le_countId (I : Index X) :
+    l.contrIndexList.countId I ≤ l.countId I := by
+  by_cases h : l.contrIndexList.countId I = 0
+  · exact StrictMono.minimal_preimage_bot (fun ⦃a b⦄ a => a) h (l.countId I)
+  · have ho : l.contrIndexList.countId I = 1 := by
+      have h1 := l.countId_contrIndexList_le_one I
+      omega
+    rw [ho]
+    rw [countId_contrIndexList_eq_one_iff_countId_eq_one] at ho
+    rw [ho]
+
+/-!
+
+## Append
+
+-/
+
+lemma contrIndexList_append_eq_filter : (l ++ l2).contrIndexList.val =
+    l.contrIndexList.val.filter (fun I => l2.countId I = 0) ++
+    l2.contrIndexList.val.filter (fun I => l.countId I = 0) := by
+  simp [contrIndexList]
+  congr 1
+  · apply List.filter_congr
+    intro I hI
+    have hIz : l.countId I ≠ 0 := countId_mem l I hI
+    have hx : l.countId I + l2.countId I = 1 ↔ (l2.countId I = 0 ∧ l.countId I = 1) := by
+      omega
+    simp only [hx, Bool.decide_and]
+  · apply List.filter_congr
+    intro I hI
+    have hIz : l2.countId I ≠ 0 := countId_mem l2 I hI
+    have hx : l.countId I + l2.countId I = 1 ↔ (l2.countId I = 1 ∧ l.countId I = 0) := by
+      omega
+    simp only [hx, Bool.decide_and]
+    exact Bool.and_comm (decide (l2.countId I = 1)) (decide (l.countId I = 0))
+
 /-!
 
 ## Splitting withUniqueDual

HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithUniqueDual
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.Contraction
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Finset.Sort
 /-!
@@ -154,6 +154,20 @@ lemma withUniqueDual_eq_withDual_iff_countId_leq_two :
     have hi := h i
     omega
 
+lemma withUniqueDual_eq_withDual_iff_countId_leq_two' :
+    l.withUniqueDual = l.withDual ↔ ∀ I, l.countId I ≤ 2 := by
+  rw [withUniqueDual_eq_withDual_iff_countId_leq_two]
+  refine Iff.intro (fun h I => ?_) (fun h i => h (l.val.get i))
+  by_cases hI : l.countId I = 0
+  · rw [hI]
+    exact Nat.zero_le 2
+  · obtain ⟨I', hI1', hI2'⟩ := countId_neq_zero_mem l I hI
+    rw [countId_congr _ hI2']
+    have hi : List.indexOf I' l.val < l.length := List.indexOf_lt_length.mpr hI1'
+    have hI' : I' = l.val.get ⟨List.indexOf I' l.val, hi⟩ := (List.indexOf_get hi).symm
+    rw [hI']
+    exact h ⟨List.indexOf I' l.val, hi⟩
+
 lemma withUniqueDual_eq_withDual_countId_cases (h : l.withUniqueDual = l.withDual)
     (i : Fin l.length) : l.countId (l.val.get i) = 0 ∨
     l.countId (l.val.get i) = 1 ∨ l.countId (l.val.get i) = 2 := by
@@ -168,6 +182,7 @@ lemma withUniqueDual_eq_withDual_countId_cases (h : l.withUniqueDual = l.withDua
 
 section filterID
 
+/-! TODO: Move this section. -/
 lemma filter_id_of_countId_eq_zero {i : Fin l.length} (h1 : l.countId (l.val.get i) = 0) :
     l.val.filter (fun J => (l.val.get i).id = J.id) = [] := by
   rw [countId_eq_length_filter, List.length_eq_zero] at h1
@@ -191,6 +206,19 @@ lemma filter_id_of_countId_eq_one {i : Fin l.length} (h1 : l.countId (l.val.get
   simp only [List.get_eq_getElem, List.cons.injEq, and_true]
   exact id (Eq.symm hme)
 
+lemma filter_id_of_countId_eq_one_mem {I : Index X} (hI : I ∈ l.val) (h : l.countId I = 1) :
+    l.val.filter (fun J => I.id = J.id) = [I] := by
+  rw [countId_eq_length_filter, List.length_eq_one] at h
+  obtain ⟨J, hJ⟩ := h
+  have hme : I ∈ List.filter (fun J => decide (I.id = J.id)) l.val := by
+    simp only [List.mem_filter, decide_True, and_true]
+    exact hI
+  rw [hJ] at hme
+  simp only [List.mem_singleton] at hme
+  erw [hJ]
+  simp only [List.cons.injEq, and_true]
+  exact id (Eq.symm hme)
+
 lemma filter_id_of_countId_eq_two {i : Fin l.length}
     (h : l.countId (l.val.get i) = 2) :
     l.val.filter (fun J => (l.val.get i).id = J.id) =
@@ -566,6 +594,25 @@ lemma append_withDual_eq_withUniqueDual_swap :
   rw [withUniqueDualInOther_eq_withDualInOther_of_append_symm]
   rw [withUniqueDualInOther_eq_withDualInOther_append_of_symm]
 
+lemma append_withDual_eq_withUniqueDual_contr_left
+    (h1 : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
+      (l.contrIndexList ++ l2).withUniqueDual = (l.contrIndexList ++ l2).withDual := by
+    rw [withUniqueDual_eq_withDual_iff_all_countId_le_two] at h1 ⊢
+    simp only [append_val, countId_append, List.all_append, Bool.and_eq_true, List.all_eq_true,
+      decide_eq_true_eq]
+    simp at h1
+    apply And.intro
+    · intro I hI
+      have hIl := h1.1 I (List.mem_of_mem_filter hI)
+      have ht : l.contrIndexList.countId I ≤ l.countId I :=
+        countId_contrIndexList_le_countId l I
+      omega
+    · intro I hI
+      have hIl2 := h1.2 I hI
+      have ht : l.contrIndexList.countId I ≤ l.countId I :=
+        countId_contrIndexList_le_countId l I
+      omega
+
 end IndexList
 
 end IndexNotation