refactor: index notation
This commit is contained in:
jstoobysmith
parent
4f9b572274
commit
6b0ecc4405
6 changed files with 1034 additions and 386 deletions
|
|
@ -169,387 +169,4 @@ def id (s : Index X) : Nat := s.tailNat.foldl (fun a b => 10 * a + b) 0
|
|||
|
||||
end Index
|
||||
|
||||
/-!
|
||||
|
||||
## List of indices
|
||||
|
||||
-/
|
||||
|
||||
/-- The type of lists of indices. -/
|
||||
structure IndexList where
|
||||
/-- The list of index values. For example `['ᵘ¹','ᵘ²','ᵤ₁']`. -/
|
||||
val : List (Index X)
|
||||
|
||||
namespace IndexList
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
|
||||
variable (l : IndexList X)
|
||||
|
||||
/-- The number of indices in an index list. -/
|
||||
def length : ℕ := l.val.length
|
||||
|
||||
lemma ext (h : l.val = l2.val) : l = l2 := by
|
||||
cases l
|
||||
cases l2
|
||||
simp_all
|
||||
|
||||
/-- The index list constructed by prepending an index to the list. -/
|
||||
def cons (i : Index X) : IndexList X := {val := i :: l.val}
|
||||
|
||||
@[simp]
|
||||
lemma cons_val (i : Index X) : (l.cons i).val = i :: l.val := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma cons_length (i : Index X) : (l.cons i).length = l.length + 1 := by
|
||||
rfl
|
||||
|
||||
/-- The tail of an index list. That is, the index list with the first index dropped. -/
|
||||
def tail : IndexList X := {val := l.val.tail}
|
||||
|
||||
@[simp]
|
||||
lemma tail_val : l.tail.val = l.val.tail := by
|
||||
rfl
|
||||
|
||||
/-- The first index in a non-empty index list. -/
|
||||
def head (h : l ≠ {val := ∅}) : Index X := l.val.head (by cases' l; simpa using h)
|
||||
|
||||
lemma head_cons_tail (h : l ≠ {val := ∅}) : l = (l.tail.cons (l.head h)) := by
|
||||
apply ext
|
||||
simp only [cons_val, tail_val]
|
||||
simp only [head, List.head_cons_tail]
|
||||
|
||||
lemma induction {P : IndexList X → Prop } (h_nil : P {val := ∅})
|
||||
(h_cons : ∀ (x : Index X) (xs : IndexList X), P xs → P (xs.cons x)) (l : IndexList X) : P l := by
|
||||
cases' l with val
|
||||
induction val with
|
||||
| nil => exact h_nil
|
||||
| cons x xs ih =>
|
||||
exact h_cons x ⟨xs⟩ ih
|
||||
|
||||
/-- The map of from `Fin s.numIndices` into colors associated to an index list. -/
|
||||
def colorMap : Fin l.length → X :=
|
||||
fun i => (l.val.get i).toColor
|
||||
|
||||
/-- The map of from `Fin s.numIndices` into the natural numbers associated to an index list. -/
|
||||
def idMap : Fin l.length → Nat :=
|
||||
fun i => (l.val.get i).id
|
||||
|
||||
lemma idMap_cast {l1 l2 : IndexList X} (h : l1 = l2) (i : Fin l1.length) :
|
||||
l1.idMap i = l2.idMap (Fin.cast (by rw [h]) i) := by
|
||||
subst h
|
||||
rfl
|
||||
|
||||
/-- Given a list of indices a subset of `Fin l.numIndices × Index X`
|
||||
of pairs of positions in `l` and the corresponding item in `l`. -/
|
||||
def toPosSet (l : IndexList X) : Set (Fin l.length × Index X) :=
|
||||
{(i, l.val.get i) | i : Fin l.length}
|
||||
|
||||
/-- Equivalence between `toPosSet` and `Fin l.numIndices`. -/
|
||||
def toPosSetEquiv (l : IndexList X) : l.toPosSet ≃ Fin l.length where
|
||||
toFun := fun x => x.1.1
|
||||
invFun := fun x => ⟨(x, l.val.get x), by simp [toPosSet]⟩
|
||||
left_inv x := by
|
||||
have hx := x.prop
|
||||
simp [toPosSet] at hx
|
||||
simp only [List.get_eq_getElem]
|
||||
obtain ⟨i, hi⟩ := hx
|
||||
have hi2 : i = x.1.1 := by
|
||||
obtain ⟨val, property⟩ := x
|
||||
obtain ⟨fst, snd⟩ := val
|
||||
simp_all only [Prod.mk.injEq]
|
||||
subst hi2
|
||||
simp_all only [Subtype.coe_eta]
|
||||
right_inv := by
|
||||
intro x
|
||||
rfl
|
||||
|
||||
lemma toPosSet_is_finite (l : IndexList X) : l.toPosSet.Finite :=
|
||||
Finite.intro l.toPosSetEquiv
|
||||
|
||||
instance : Fintype l.toPosSet where
|
||||
elems := Finset.map l.toPosSetEquiv.symm.toEmbedding Finset.univ
|
||||
complete := by
|
||||
intro x
|
||||
simp_all only [Finset.mem_map_equiv, Equiv.symm_symm, Finset.mem_univ]
|
||||
|
||||
/-- Given a list of indices a finite set of `Fin l.length × Index X`
|
||||
of pairs of positions in `l` and the corresponding item in `l`. -/
|
||||
def toPosFinset (l : IndexList X) : Finset (Fin l.length × Index X) :=
|
||||
l.toPosSet.toFinset
|
||||
|
||||
/-- The construction of a list of indices from a map
|
||||
from `Fin n` to `Index X`. -/
|
||||
def fromFinMap {n : ℕ} (f : Fin n → Index X) : IndexList X where
|
||||
val := (Fin.list n).map f
|
||||
|
||||
@[simp]
|
||||
lemma fromFinMap_numIndices {n : ℕ} (f : Fin n → Index X) :
|
||||
(fromFinMap f).length = n := by
|
||||
simp [fromFinMap, length]
|
||||
|
||||
/-!
|
||||
|
||||
## Appending index lists.
|
||||
|
||||
-/
|
||||
|
||||
section append
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
variable (l l2 l3 : IndexList X)
|
||||
|
||||
instance : HAppend (IndexList X) (IndexList X) (IndexList X) where
|
||||
hAppend := fun l l2 => {val := l.val ++ l2.val}
|
||||
|
||||
@[simp]
|
||||
lemma cons_append (i : Index X) : (l.cons i) ++ l2 = (l ++ l2).cons i := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma append_length : (l ++ l2).length = l.length + l2.length := by
|
||||
simp [IndexList.length]
|
||||
exact List.length_append l.val l2.val
|
||||
|
||||
lemma append_assoc : l ++ l2 ++ l3 = l ++ (l2 ++ l3) := by
|
||||
apply ext
|
||||
change l.val ++ l2.val ++ l3.val = l.val ++ (l2.val ++ l3.val)
|
||||
exact List.append_assoc l.val l2.val l3.val
|
||||
|
||||
/-- An equivalence between the sum of the types of indices of `l` an `l2` and the type
|
||||
of indices of the joined index list `l ++ l2`. -/
|
||||
def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length :=
|
||||
finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv
|
||||
|
||||
/-- The inclusion of the indices of `l` into the indices of `l ++ l2`. -/
|
||||
def appendInl : Fin l.length ↪ Fin (l ++ l2).length where
|
||||
toFun := appendEquiv ∘ Sum.inl
|
||||
inj' := by
|
||||
intro i j h
|
||||
simp [Function.comp] at h
|
||||
exact h
|
||||
|
||||
/-- The inclusion of the indices of `l2` into the indices of `l ++ l2`. -/
|
||||
def appendInr : Fin l2.length ↪ Fin (l ++ l2).length where
|
||||
toFun := appendEquiv ∘ Sum.inr
|
||||
inj' := by
|
||||
intro i j h
|
||||
simp [Function.comp] at h
|
||||
exact h
|
||||
|
||||
@[simp]
|
||||
lemma appendInl_appendEquiv :
|
||||
(l.appendInl l2).trans appendEquiv.symm.toEmbedding =
|
||||
{toFun := Sum.inl, inj' := Sum.inl_injective} := by
|
||||
ext i
|
||||
simp [appendInl]
|
||||
|
||||
@[simp]
|
||||
lemma appendInr_appendEquiv :
|
||||
(l.appendInr l2).trans appendEquiv.symm.toEmbedding =
|
||||
{toFun := Sum.inr, inj' := Sum.inr_injective} := by
|
||||
ext i
|
||||
simp [appendInr]
|
||||
|
||||
@[simp]
|
||||
lemma append_val {l l2 : IndexList X} : (l ++ l2).val = l.val ++ l2.val := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
|
||||
(l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
|
||||
simp [appendEquiv, idMap]
|
||||
rw [List.getElem_append_left]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
|
||||
(l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
|
||||
simp [appendEquiv, idMap, IndexList.length]
|
||||
rw [List.getElem_append_right]
|
||||
· simp only [Nat.add_sub_cancel_left]
|
||||
· omega
|
||||
· omega
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
|
||||
(l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by
|
||||
simp [appendEquiv, colorMap, IndexList.length]
|
||||
rw [List.getElem_append_left]
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inl' :
|
||||
(l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inl = l.colorMap := by
|
||||
funext i
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
|
||||
(l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by
|
||||
simp [appendEquiv, colorMap, IndexList.length]
|
||||
rw [List.getElem_append_right]
|
||||
· simp only [Nat.add_sub_cancel_left]
|
||||
· omega
|
||||
· omega
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inr' :
|
||||
(l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inr = l2.colorMap := by
|
||||
funext i
|
||||
simp
|
||||
|
||||
lemma colorMap_sumELim (l1 l2 : IndexList X) :
|
||||
Sum.elim l1.colorMap l2.colorMap =
|
||||
(l1 ++ l2).colorMap ∘ appendEquiv := by
|
||||
funext x
|
||||
match x with
|
||||
| Sum.inl i => simp
|
||||
| Sum.inr i => simp
|
||||
|
||||
end append
|
||||
|
||||
/-!
|
||||
|
||||
## countId
|
||||
|
||||
-/
|
||||
|
||||
/-- The number of times the id of an index `I` appears in a list of indices `l`. -/
|
||||
def countId (I : Index X) : ℕ :=
|
||||
l.val.countP (fun J => I.id = J.id)
|
||||
|
||||
@[simp]
|
||||
lemma countId_append (I : Index X) : (l ++ l2).countId I = l.countId I + l2.countId I := by
|
||||
simp [countId]
|
||||
|
||||
lemma countId_eq_length_filter (I : Index X) :
|
||||
l.countId I = (l.val.filter (fun J => I.id = J.id)).length := by
|
||||
simp [countId]
|
||||
rw [List.countP_eq_length_filter]
|
||||
|
||||
lemma countId_index_neq_zero (i : Fin l.length) : l.countId (l.val.get i) ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [List.length_eq_zero] at hn
|
||||
have hm : l.val.get i ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l.val := by
|
||||
simpa using List.getElem_mem l.val i.1 i.isLt
|
||||
rw [hn] at hm
|
||||
simp at hm
|
||||
|
||||
lemma countId_append_symm (I : Index X) : (l ++ l2).countId I = (l2 ++ l).countId I := by
|
||||
simp only [countId_append]
|
||||
omega
|
||||
|
||||
lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.val)
|
||||
(h : (l ++ l2).countId I = 1) : l2.countId I = 1 := by
|
||||
simp at h
|
||||
have hmem : I ∈ l2.val.filter (fun J => I.id = J.id) := by
|
||||
simp [List.mem_filter, decide_True, and_true, hI]
|
||||
have h1 : l2.countId I ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [@List.length_eq_zero] at hn
|
||||
rw [hn] at hmem
|
||||
simp at hmem
|
||||
omega
|
||||
|
||||
lemma countId_eq_one_append_mem_right_other_eq_zero {I : Index X} (hI : I ∈ l2.val)
|
||||
(h : (l ++ l2).countId I = 1) : l.countId I = 0 := by
|
||||
simp at h
|
||||
have hmem : I ∈ l2.val.filter (fun J => I.id = J.id) := by
|
||||
simp [List.mem_filter, decide_True, and_true, hI]
|
||||
have h1 : l2.countId I ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [@List.length_eq_zero] at hn
|
||||
rw [hn] at hmem
|
||||
simp at hmem
|
||||
omega
|
||||
|
||||
@[simp]
|
||||
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
|
||||
|
||||
-/
|
||||
/-! TODO: Replace with Mathlib lemma. -/
|
||||
lemma filter_sort_comm {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [DecidablePred p] :
|
||||
List.filter p (Finset.sort (fun i j => i ≤ j) s) =
|
||||
Finset.sort (fun i j => i ≤ j) (Finset.filter p s) := by
|
||||
simp [Finset.filter, Finset.sort]
|
||||
have : ∀ (m : Multiset (Fin n)), List.filter p (Multiset.sort (fun i j => i ≤ j) m) =
|
||||
Multiset.sort (fun i j => i ≤ j) (Multiset.filter p m) := by
|
||||
apply Quot.ind
|
||||
intro m
|
||||
simp [List.mergeSort]
|
||||
have h1 : List.Sorted (fun i j => i ≤ j) (List.filter (fun b => decide (p b))
|
||||
(List.mergeSort (fun i j => i ≤ j) m)) := by
|
||||
simp [List.Sorted]
|
||||
rw [List.pairwise_filter]
|
||||
rw [@List.pairwise_iff_get]
|
||||
intro i j h1 _ _
|
||||
have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort (fun i j => i ≤ j) m) := by
|
||||
exact List.sorted_mergeSort (fun i j => i ≤ j) m
|
||||
simp [List.Sorted] at hs
|
||||
rw [List.pairwise_iff_get] at hs
|
||||
exact hs i j h1
|
||||
have hp1 : (List.mergeSort (fun i j => i ≤ j) m).Perm m := by
|
||||
exact List.perm_mergeSort (fun i j => i ≤ j) m
|
||||
have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort (fun i j => i ≤ j) m))).Perm
|
||||
(List.filter (fun b => decide (p b)) m) := by
|
||||
exact List.Perm.filter (fun b => decide (p b)) hp1
|
||||
have hp3 : (List.filter (fun b => decide (p b)) m).Perm
|
||||
(List.mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
|
||||
exact List.Perm.symm (List.perm_mergeSort (fun i j => i ≤ j)
|
||||
(List.filter (fun b => decide (p b)) m))
|
||||
have hp4 := hp2.trans hp3
|
||||
refine List.eq_of_perm_of_sorted hp4 h1 ?_
|
||||
exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
|
||||
exact this s.val
|
||||
|
||||
lemma filter_id_eq_sort (i : Fin l.length) : l.val.filter (fun J => (l.val.get i).id = J.id) =
|
||||
List.map l.val.get (Finset.sort (fun i j => i ≤ j)
|
||||
(Finset.filter (fun j => l.idMap i = l.idMap j) Finset.univ)) := by
|
||||
have h1 := (List.finRange_map_get l.val).symm
|
||||
have h2 : l.val = List.map l.val.get (Finset.sort (fun i j => i ≤ j) Finset.univ) := by
|
||||
nth_rewrite 1 [h1, (Fin.sort_univ l.val.length).symm]
|
||||
rfl
|
||||
nth_rewrite 3 [h2]
|
||||
rw [List.filter_map]
|
||||
apply congrArg
|
||||
rw [← filter_sort_comm]
|
||||
apply List.filter_congr
|
||||
intro x _
|
||||
simp [idMap]
|
||||
|
||||
end IndexList
|
||||
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -11,7 +11,9 @@ import Init.Data.List.Lemmas
|
|||
|
||||
# Appending two ColorIndexLists
|
||||
|
||||
We define the contraction of ColorIndexLists.
|
||||
We define conditional appending of `ColorIndexList`'s.
|
||||
|
||||
It is conditional on `AppendCond` being true, which we define.
|
||||
|
||||
-/
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,312 @@
|
|||
/-
|
||||
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.Basic
|
||||
/-!
|
||||
|
||||
# Index lists
|
||||
|
||||
i.e. lists of indices.
|
||||
|
||||
-/
|
||||
|
||||
namespace IndexNotation
|
||||
|
||||
variable (X : Type) [IndexNotation X]
|
||||
variable [Fintype X] [DecidableEq X]
|
||||
|
||||
/-- The type of lists of indices. -/
|
||||
structure IndexList where
|
||||
/-- The list of index values. For example `['ᵘ¹','ᵘ²','ᵤ₁']`. -/
|
||||
val : List (Index X)
|
||||
|
||||
namespace IndexList
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
|
||||
variable (l : IndexList X)
|
||||
|
||||
/-- The number of indices in an index list. -/
|
||||
def length : ℕ := l.val.length
|
||||
|
||||
lemma ext (h : l.val = l2.val) : l = l2 := by
|
||||
cases l
|
||||
cases l2
|
||||
simp_all
|
||||
|
||||
/-- The index list constructed by prepending an index to the list. -/
|
||||
def cons (i : Index X) : IndexList X := {val := i :: l.val}
|
||||
|
||||
@[simp]
|
||||
lemma cons_val (i : Index X) : (l.cons i).val = i :: l.val := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma cons_length (i : Index X) : (l.cons i).length = l.length + 1 := by
|
||||
rfl
|
||||
|
||||
/-- The tail of an index list. That is, the index list with the first index dropped. -/
|
||||
def tail : IndexList X := {val := l.val.tail}
|
||||
|
||||
@[simp]
|
||||
lemma tail_val : l.tail.val = l.val.tail := by
|
||||
rfl
|
||||
|
||||
/-- The first index in a non-empty index list. -/
|
||||
def head (h : l ≠ {val := ∅}) : Index X := l.val.head (by cases' l; simpa using h)
|
||||
|
||||
lemma head_cons_tail (h : l ≠ {val := ∅}) : l = (l.tail.cons (l.head h)) := by
|
||||
apply ext
|
||||
simp only [cons_val, tail_val]
|
||||
simp only [head, List.head_cons_tail]
|
||||
|
||||
lemma induction {P : IndexList X → Prop } (h_nil : P {val := ∅})
|
||||
(h_cons : ∀ (x : Index X) (xs : IndexList X), P xs → P (xs.cons x)) (l : IndexList X) : P l := by
|
||||
cases' l with val
|
||||
induction val with
|
||||
| nil => exact h_nil
|
||||
| cons x xs ih =>
|
||||
exact h_cons x ⟨xs⟩ ih
|
||||
|
||||
/-- The map of from `Fin s.numIndices` into colors associated to an index list. -/
|
||||
def colorMap : Fin l.length → X :=
|
||||
fun i => (l.val.get i).toColor
|
||||
|
||||
/-- The map of from `Fin s.numIndices` into the natural numbers associated to an index list. -/
|
||||
def idMap : Fin l.length → Nat :=
|
||||
fun i => (l.val.get i).id
|
||||
|
||||
lemma idMap_cast {l1 l2 : IndexList X} (h : l1 = l2) (i : Fin l1.length) :
|
||||
l1.idMap i = l2.idMap (Fin.cast (by rw [h]) i) := by
|
||||
subst h
|
||||
rfl
|
||||
|
||||
/-- Given a list of indices a subset of `Fin l.numIndices × Index X`
|
||||
of pairs of positions in `l` and the corresponding item in `l`. -/
|
||||
def toPosSet (l : IndexList X) : Set (Fin l.length × Index X) :=
|
||||
{(i, l.val.get i) | i : Fin l.length}
|
||||
|
||||
/-- Equivalence between `toPosSet` and `Fin l.numIndices`. -/
|
||||
def toPosSetEquiv (l : IndexList X) : l.toPosSet ≃ Fin l.length where
|
||||
toFun := fun x => x.1.1
|
||||
invFun := fun x => ⟨(x, l.val.get x), by simp [toPosSet]⟩
|
||||
left_inv x := by
|
||||
have hx := x.prop
|
||||
simp [toPosSet] at hx
|
||||
simp only [List.get_eq_getElem]
|
||||
obtain ⟨i, hi⟩ := hx
|
||||
have hi2 : i = x.1.1 := by
|
||||
obtain ⟨val, property⟩ := x
|
||||
obtain ⟨fst, snd⟩ := val
|
||||
simp_all only [Prod.mk.injEq]
|
||||
subst hi2
|
||||
simp_all only [Subtype.coe_eta]
|
||||
right_inv := by
|
||||
intro x
|
||||
rfl
|
||||
|
||||
lemma toPosSet_is_finite (l : IndexList X) : l.toPosSet.Finite :=
|
||||
Finite.intro l.toPosSetEquiv
|
||||
|
||||
instance : Fintype l.toPosSet where
|
||||
elems := Finset.map l.toPosSetEquiv.symm.toEmbedding Finset.univ
|
||||
complete := by
|
||||
intro x
|
||||
simp_all only [Finset.mem_map_equiv, Equiv.symm_symm, Finset.mem_univ]
|
||||
|
||||
/-- Given a list of indices a finite set of `Fin l.length × Index X`
|
||||
of pairs of positions in `l` and the corresponding item in `l`. -/
|
||||
def toPosFinset (l : IndexList X) : Finset (Fin l.length × Index X) :=
|
||||
l.toPosSet.toFinset
|
||||
|
||||
/-- The construction of a list of indices from a map
|
||||
from `Fin n` to `Index X`. -/
|
||||
def fromFinMap {n : ℕ} (f : Fin n → Index X) : IndexList X where
|
||||
val := (Fin.list n).map f
|
||||
|
||||
@[simp]
|
||||
lemma fromFinMap_numIndices {n : ℕ} (f : Fin n → Index X) :
|
||||
(fromFinMap f).length = n := by
|
||||
simp [fromFinMap, length]
|
||||
|
||||
/-!
|
||||
|
||||
## Appending index lists.
|
||||
|
||||
-/
|
||||
|
||||
section append
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
variable (l l2 l3 : IndexList X)
|
||||
|
||||
instance : HAppend (IndexList X) (IndexList X) (IndexList X) where
|
||||
hAppend := fun l l2 => {val := l.val ++ l2.val}
|
||||
|
||||
@[simp]
|
||||
lemma cons_append (i : Index X) : (l.cons i) ++ l2 = (l ++ l2).cons i := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma append_length : (l ++ l2).length = l.length + l2.length := by
|
||||
simp [IndexList.length]
|
||||
exact List.length_append l.val l2.val
|
||||
|
||||
lemma append_assoc : l ++ l2 ++ l3 = l ++ (l2 ++ l3) := by
|
||||
apply ext
|
||||
change l.val ++ l2.val ++ l3.val = l.val ++ (l2.val ++ l3.val)
|
||||
exact List.append_assoc l.val l2.val l3.val
|
||||
|
||||
/-- An equivalence between the sum of the types of indices of `l` an `l2` and the type
|
||||
of indices of the joined index list `l ++ l2`. -/
|
||||
def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length :=
|
||||
finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv
|
||||
|
||||
/-- The inclusion of the indices of `l` into the indices of `l ++ l2`. -/
|
||||
def appendInl : Fin l.length ↪ Fin (l ++ l2).length where
|
||||
toFun := appendEquiv ∘ Sum.inl
|
||||
inj' := by
|
||||
intro i j h
|
||||
simp [Function.comp] at h
|
||||
exact h
|
||||
|
||||
/-- The inclusion of the indices of `l2` into the indices of `l ++ l2`. -/
|
||||
def appendInr : Fin l2.length ↪ Fin (l ++ l2).length where
|
||||
toFun := appendEquiv ∘ Sum.inr
|
||||
inj' := by
|
||||
intro i j h
|
||||
simp [Function.comp] at h
|
||||
exact h
|
||||
|
||||
@[simp]
|
||||
lemma appendInl_appendEquiv :
|
||||
(l.appendInl l2).trans appendEquiv.symm.toEmbedding =
|
||||
{toFun := Sum.inl, inj' := Sum.inl_injective} := by
|
||||
ext i
|
||||
simp [appendInl]
|
||||
|
||||
@[simp]
|
||||
lemma appendInr_appendEquiv :
|
||||
(l.appendInr l2).trans appendEquiv.symm.toEmbedding =
|
||||
{toFun := Sum.inr, inj' := Sum.inr_injective} := by
|
||||
ext i
|
||||
simp [appendInr]
|
||||
|
||||
@[simp]
|
||||
lemma append_val {l l2 : IndexList X} : (l ++ l2).val = l.val ++ l2.val := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
|
||||
(l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
|
||||
simp [appendEquiv, idMap]
|
||||
rw [List.getElem_append_left]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
|
||||
(l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
|
||||
simp [appendEquiv, idMap, IndexList.length]
|
||||
rw [List.getElem_append_right]
|
||||
· simp only [Nat.add_sub_cancel_left]
|
||||
· omega
|
||||
· omega
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
|
||||
(l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by
|
||||
simp [appendEquiv, colorMap, IndexList.length]
|
||||
rw [List.getElem_append_left]
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inl' :
|
||||
(l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inl = l.colorMap := by
|
||||
funext i
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
|
||||
(l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by
|
||||
simp [appendEquiv, colorMap, IndexList.length]
|
||||
rw [List.getElem_append_right]
|
||||
· simp only [Nat.add_sub_cancel_left]
|
||||
· omega
|
||||
· omega
|
||||
|
||||
@[simp]
|
||||
lemma colorMap_append_inr' :
|
||||
(l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inr = l2.colorMap := by
|
||||
funext i
|
||||
simp
|
||||
|
||||
lemma colorMap_sumELim (l1 l2 : IndexList X) :
|
||||
Sum.elim l1.colorMap l2.colorMap =
|
||||
(l1 ++ l2).colorMap ∘ appendEquiv := by
|
||||
funext x
|
||||
match x with
|
||||
| Sum.inl i => simp
|
||||
| Sum.inr i => simp
|
||||
|
||||
end append
|
||||
|
||||
/-!
|
||||
|
||||
## Filter id
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: Replace with Mathlib lemma. -/
|
||||
lemma filter_sort_comm {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [DecidablePred p] :
|
||||
List.filter p (Finset.sort (fun i j => i ≤ j) s) =
|
||||
Finset.sort (fun i j => i ≤ j) (Finset.filter p s) := by
|
||||
simp [Finset.filter, Finset.sort]
|
||||
have : ∀ (m : Multiset (Fin n)), List.filter p (Multiset.sort (fun i j => i ≤ j) m) =
|
||||
Multiset.sort (fun i j => i ≤ j) (Multiset.filter p m) := by
|
||||
apply Quot.ind
|
||||
intro m
|
||||
simp [List.mergeSort]
|
||||
have h1 : List.Sorted (fun i j => i ≤ j) (List.filter (fun b => decide (p b))
|
||||
(List.mergeSort (fun i j => i ≤ j) m)) := by
|
||||
simp [List.Sorted]
|
||||
rw [List.pairwise_filter]
|
||||
rw [@List.pairwise_iff_get]
|
||||
intro i j h1 _ _
|
||||
have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort (fun i j => i ≤ j) m) := by
|
||||
exact List.sorted_mergeSort (fun i j => i ≤ j) m
|
||||
simp [List.Sorted] at hs
|
||||
rw [List.pairwise_iff_get] at hs
|
||||
exact hs i j h1
|
||||
have hp1 : (List.mergeSort (fun i j => i ≤ j) m).Perm m := by
|
||||
exact List.perm_mergeSort (fun i j => i ≤ j) m
|
||||
have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort (fun i j => i ≤ j) m))).Perm
|
||||
(List.filter (fun b => decide (p b)) m) := by
|
||||
exact List.Perm.filter (fun b => decide (p b)) hp1
|
||||
have hp3 : (List.filter (fun b => decide (p b)) m).Perm
|
||||
(List.mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
|
||||
exact List.Perm.symm (List.perm_mergeSort (fun i j => i ≤ j)
|
||||
(List.filter (fun b => decide (p b)) m))
|
||||
have hp4 := hp2.trans hp3
|
||||
refine List.eq_of_perm_of_sorted hp4 h1 ?_
|
||||
exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
|
||||
exact this s.val
|
||||
|
||||
lemma filter_id_eq_sort (i : Fin l.length) : l.val.filter (fun J => (l.val.get i).id = J.id) =
|
||||
List.map l.val.get (Finset.sort (fun i j => i ≤ j)
|
||||
(Finset.filter (fun j => l.idMap i = l.idMap j) Finset.univ)) := by
|
||||
have h1 := (List.finRange_map_get l.val).symm
|
||||
have h2 : l.val = List.map l.val.get (Finset.sort (fun i j => i ≤ j) Finset.univ) := by
|
||||
nth_rewrite 1 [h1, (Fin.sort_univ l.val.length).symm]
|
||||
rfl
|
||||
nth_rewrite 3 [h2]
|
||||
rw [List.filter_map]
|
||||
apply congrArg
|
||||
rw [← filter_sort_comm]
|
||||
apply List.filter_congr
|
||||
intro x _
|
||||
simp [idMap]
|
||||
|
||||
end IndexList
|
||||
|
||||
end IndexNotation
|
||||
|
|
@ -0,0 +1,339 @@
|
|||
/-
|
||||
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.IndexList.Duals
|
||||
/-!
|
||||
|
||||
# Counting ids
|
||||
|
||||
|
||||
-/
|
||||
|
||||
|
||||
namespace IndexNotation
|
||||
|
||||
namespace IndexList
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
variable (l l2 l3 : IndexList X)
|
||||
|
||||
|
||||
/-!
|
||||
|
||||
## countId
|
||||
|
||||
-/
|
||||
|
||||
/-- The number of times the id of an index `I` appears in a list of indices `l`. -/
|
||||
def countId (I : Index X) : ℕ :=
|
||||
l.val.countP (fun J => I.id = J.id)
|
||||
|
||||
/-!
|
||||
|
||||
## Basic properties
|
||||
|
||||
-/
|
||||
@[simp]
|
||||
lemma countId_append (I : Index X) : (l ++ l2).countId I = l.countId I + l2.countId I := by
|
||||
simp [countId]
|
||||
|
||||
lemma countId_eq_length_filter (I : Index X) :
|
||||
l.countId I = (l.val.filter (fun J => I.id = J.id)).length := by
|
||||
simp [countId]
|
||||
rw [List.countP_eq_length_filter]
|
||||
|
||||
lemma countId_index_neq_zero (i : Fin l.length) : l.countId (l.val.get i) ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [List.length_eq_zero] at hn
|
||||
have hm : l.val.get i ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l.val := by
|
||||
simpa using List.getElem_mem l.val i.1 i.isLt
|
||||
rw [hn] at hm
|
||||
simp at hm
|
||||
|
||||
lemma countId_append_symm (I : Index X) : (l ++ l2).countId I = (l2 ++ l).countId I := by
|
||||
simp only [countId_append]
|
||||
omega
|
||||
|
||||
lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.val)
|
||||
(h : (l ++ l2).countId I = 1) : l2.countId I = 1 := by
|
||||
simp at h
|
||||
have hmem : I ∈ l2.val.filter (fun J => I.id = J.id) := by
|
||||
simp [List.mem_filter, decide_True, and_true, hI]
|
||||
have h1 : l2.countId I ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [@List.length_eq_zero] at hn
|
||||
rw [hn] at hmem
|
||||
simp at hmem
|
||||
omega
|
||||
|
||||
lemma countId_eq_one_append_mem_right_other_eq_zero {I : Index X} (hI : I ∈ l2.val)
|
||||
(h : (l ++ l2).countId I = 1) : l.countId I = 0 := by
|
||||
simp at h
|
||||
have hmem : I ∈ l2.val.filter (fun J => I.id = J.id) := by
|
||||
simp [List.mem_filter, decide_True, and_true, hI]
|
||||
have h1 : l2.countId I ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [@List.length_eq_zero] at hn
|
||||
rw [hn] at hmem
|
||||
simp at hmem
|
||||
omega
|
||||
|
||||
@[simp]
|
||||
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
|
||||
|
||||
lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
|
||||
(List.finRange l2.length).countP (fun j => l.AreDualInOther l2 i j) := by
|
||||
rw [countId_eq_length_filter]
|
||||
rw [List.countP_eq_length_filter]
|
||||
have hl2 : l2.val = List.map l2.val.get (List.finRange l2.length) := by
|
||||
simp only [length, List.finRange_map_get]
|
||||
nth_rewrite 1 [hl2]
|
||||
rw [List.filter_map, List.length_map]
|
||||
apply congrArg
|
||||
refine List.filter_congr (fun j _ => ?_)
|
||||
simp [AreDualInOther, idMap]
|
||||
|
||||
/-! TODO: Replace with mathlib lemma. -/
|
||||
lemma filter_finRange (i : Fin l.length) : List.filter (fun j => i = j) (List.finRange l.length) = [i] := by
|
||||
have h3 : (List.filter (fun j => i = j) (List.finRange l.length)).length = 1 := by
|
||||
rw [← List.countP_eq_length_filter]
|
||||
trans List.count i (List.finRange l.length)
|
||||
· simp [List.count]
|
||||
apply List.countP_congr (fun j _ => ?_)
|
||||
simp
|
||||
exact eq_comm
|
||||
· exact List.nodup_iff_count_eq_one.mp (List.nodup_finRange l.length) _ (List.mem_finRange i)
|
||||
have h4 : i ∈ List.filter (fun j => i = j) (List.finRange l.length) := by
|
||||
simp
|
||||
rw [@List.length_eq_one] at h3
|
||||
obtain ⟨a, ha⟩ := h3
|
||||
rw [ha] at h4
|
||||
simp at h4
|
||||
subst h4
|
||||
exact ha
|
||||
|
||||
lemma countId_get (i : Fin l.length) : l.countId (l.val.get i) =
|
||||
(List.finRange l.length).countP (fun j => l.AreDualInSelf i j) + 1 := by
|
||||
rw [countId_get_other l l]
|
||||
have h1 : (List.finRange l.length).countP (fun j => l.AreDualInSelf i j)
|
||||
= ((List.finRange l.length).filter (fun j => l.AreDualInOther l i j)).countP
|
||||
(fun j => ¬ i = j) := by
|
||||
rw [List.countP_filter]
|
||||
refine List.countP_congr ?_
|
||||
intro j _
|
||||
simp [AreDualInSelf, AreDualInOther]
|
||||
rw [h1]
|
||||
have h1 := List.length_eq_countP_add_countP (fun j => i = j) ((List.finRange l.length).filter (fun j => l.AreDualInOther l i j))
|
||||
have h2 : List.countP (fun j => i = j)
|
||||
(List.filter (fun j => l.AreDualInOther l i j) (List.finRange l.length)) =
|
||||
List.countP (fun j => l.AreDualInOther l i j)
|
||||
(List.filter (fun j => i = j) (List.finRange l.length)) := by
|
||||
rw [List.countP_filter, List.countP_filter]
|
||||
refine List.countP_congr (fun j _ => ?_)
|
||||
simpa using And.comm
|
||||
have ha := l.filter_finRange
|
||||
rw [ha] at h2
|
||||
rw [h2] at h1
|
||||
rw [List.countP_eq_length_filter, h1, add_comm]
|
||||
simp
|
||||
simp [List.countP, List.countP.go, AreDualInOther]
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
/-!
|
||||
|
||||
## Duals and countId
|
||||
|
||||
-/
|
||||
|
||||
lemma countId_gt_zero_of_mem_withDual (i : Fin l.length) (h : i ∈ l.withDual) :
|
||||
1 < l.countId (l.val.get i) := by
|
||||
rw [countId_get]
|
||||
by_contra hn
|
||||
simp at hn
|
||||
rw [List.countP_eq_length_filter, List.length_eq_zero] at hn
|
||||
rw [mem_withDual_iff_exists] at h
|
||||
obtain ⟨j, hj⟩ := h
|
||||
have hjmem : j ∈ (List.finRange l.length).filter (fun j => decide (l.AreDualInSelf i j)) := by
|
||||
simpa using hj
|
||||
rw [hn] at hjmem
|
||||
simp at hjmem
|
||||
|
||||
|
||||
lemma countId_of_not_mem_withDual (i : Fin l.length)(h : i ∉ l.withDual) :
|
||||
l.countId (l.val.get i) = 1 := by
|
||||
rw [countId_get]
|
||||
simp only [add_left_eq_self]
|
||||
rw [List.countP_eq_length_filter]
|
||||
simp only [List.length_eq_zero]
|
||||
rw [List.filter_eq_nil]
|
||||
simp only [List.mem_finRange, decide_eq_true_eq, true_implies]
|
||||
rw [mem_withDual_iff_exists] at h
|
||||
simpa using h
|
||||
|
||||
lemma mem_withDual_iff_countId_gt_one (i : Fin l.length) :
|
||||
i ∈ l.withDual ↔ 1 < l.countId (l.val.get i) := by
|
||||
refine Iff.intro (fun h => countId_gt_zero_of_mem_withDual l i h) (fun h => ?_)
|
||||
by_contra hn
|
||||
have hn' := countId_of_not_mem_withDual l i hn
|
||||
omega
|
||||
|
||||
lemma countId_neq_zero_of_mem_withDualInOther (i : Fin l.length) (h : i ∈ l.withDualInOther l2) :
|
||||
l2.countId (l.val.get i) ≠ 0 := by
|
||||
rw [mem_withInDualOther_iff_exists] at h
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
rw [List.length_eq_zero] at hn
|
||||
obtain ⟨j, hj⟩ := h
|
||||
have hjmem : l2.val.get j ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l2.val := by
|
||||
simp
|
||||
apply And.intro
|
||||
· exact List.getElem_mem l2.val (↑j) j.isLt
|
||||
· simpa [AreDualInOther] using hj
|
||||
rw [hn] at hjmem
|
||||
simp at hjmem
|
||||
|
||||
lemma countId_of_not_mem_withDualInOther (i : Fin l.length) (h : i ∉ l.withDualInOther l2) :
|
||||
l2.countId (l.val.get i) = 0 := by
|
||||
by_contra hn
|
||||
rw [countId_eq_length_filter] at hn
|
||||
rw [← List.isEmpty_iff_length_eq_zero] at hn
|
||||
have hx := eq_false_of_ne_true hn
|
||||
rw [List.isEmpty_false_iff_exists_mem] at hx
|
||||
obtain ⟨j, hj⟩ := hx
|
||||
have hjmem : j ∈ l2.val := List.mem_of_mem_filter hj
|
||||
have hj' : l2.val.indexOf j < l2.length := List.indexOf_lt_length.mpr hjmem
|
||||
have hjid : l2.val.get ⟨l2.val.indexOf j, hj'⟩ = j := List.indexOf_get hj'
|
||||
rw [mem_withInDualOther_iff_exists] at h
|
||||
simp at h
|
||||
have hj' := h ⟨l2.val.indexOf j, hj'⟩
|
||||
simp [AreDualInOther, idMap] at hj'
|
||||
simp at hj
|
||||
simp_all only [List.get_eq_getElem, List.isEmpty_eq_true, List.getElem_indexOf, not_true_eq_false]
|
||||
|
||||
lemma mem_withDualInOther_iff_countId_neq_zero (i : Fin l.length) :
|
||||
i ∈ l.withDualInOther l2 ↔ l2.countId (l.val.get i) ≠ 0 := by
|
||||
refine Iff.intro (fun h => countId_neq_zero_of_mem_withDualInOther l l2 i h)
|
||||
(fun h => ?_)
|
||||
by_contra hn
|
||||
have hn' := countId_of_not_mem_withDualInOther l l2 i hn
|
||||
omega
|
||||
|
||||
lemma mem_withoutDual_iff_countId_eq_one (i : Fin l.length) :
|
||||
i ∈ l.withoutDual ↔ l.countId (l.val.get i) = 1 := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· exact countId_of_not_mem_withDual l i (l.not_mem_withDual_of_mem_withoutDual i h)
|
||||
· by_contra hn
|
||||
have h : i ∈ l.withDual := by
|
||||
simp [withoutDual] at hn
|
||||
simpa using Option.ne_none_iff_isSome.mp hn
|
||||
rw [mem_withDual_iff_countId_gt_one] at h
|
||||
omega
|
||||
|
||||
lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
|
||||
l.countId (l.val.get i) = 2 := by
|
||||
rw [countId_get]
|
||||
simp
|
||||
let i' := (l.getDual? i).get (mem_withUniqueDual_isSome l i h)
|
||||
have h1 : [i'] = (List.finRange l.length).filter (fun j => (l.AreDualInSelf i j)) := by
|
||||
trans List.filter (fun j => (l.AreDualInSelf i j)) [i']
|
||||
· simp [List.filter, i']
|
||||
trans List.filter (fun j => (l.AreDualInSelf i j))
|
||||
((List.finRange l.length).filter (fun j => j = i'))
|
||||
· apply congrArg
|
||||
rw [← filter_finRange l i']
|
||||
apply List.filter_congr (fun j _ => ?_)
|
||||
simpa using eq_comm
|
||||
trans List.filter (fun j => j = i')
|
||||
((List.finRange l.length).filter (fun j => (l.AreDualInSelf i j)))
|
||||
· simp
|
||||
apply List.filter_congr (fun j _ => ?_)
|
||||
exact Bool.and_comm (decide (l.AreDualInSelf i j)) (decide (j = i'))
|
||||
· simp
|
||||
refine List.filter_congr (fun j _ => ?_)
|
||||
simp
|
||||
simp [withUniqueDual] at h
|
||||
intro hj
|
||||
have hj' := h.2 j hj
|
||||
apply Option.some_injective
|
||||
rw [hj']
|
||||
simp [i']
|
||||
rw [List.countP_eq_length_filter, ← h1]
|
||||
simp
|
||||
|
||||
lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
|
||||
(h : l.countId (l.val.get i) = 2) : i ∈ l.withUniqueDual := by
|
||||
have hw : i ∈ l.withDual := by
|
||||
rw [mem_withDual_iff_countId_gt_one, h]
|
||||
exact Nat.one_lt_two
|
||||
simp [withUniqueDual]
|
||||
apply And.intro ((mem_withDual_iff_isSome l i).mp hw)
|
||||
intro j hj
|
||||
rw [@countId_get] at h
|
||||
simp [List.countP_eq_length_filter] at h
|
||||
rw [List.length_eq_one] at h
|
||||
obtain ⟨a, ha⟩ := h
|
||||
have hj : j ∈ List.filter (fun j => decide (l.AreDualInSelf i j)) (List.finRange l.length) := by
|
||||
simpa using hj
|
||||
rw [ha] at hj
|
||||
simp at hj
|
||||
subst hj
|
||||
have ht : (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp hw) ∈
|
||||
(List.finRange l.length).filter (fun j => decide (l.AreDualInSelf i j)) := by
|
||||
simp
|
||||
rw [ha] at ht
|
||||
simp at ht
|
||||
subst ht
|
||||
simp
|
||||
|
||||
lemma mem_withUniqueDual_iff_countId_eq_two (i : Fin l.length) :
|
||||
i ∈ l.withUniqueDual ↔ l.countId (l.val.get i) = 2 :=
|
||||
Iff.intro (fun h => l.countId_eq_two_of_mem_withUniqueDual i h)
|
||||
(fun h => l.mem_withUniqueDual_of_countId_eq_two i h)
|
||||
|
||||
lemma mem_withUniqueDualInOther_iff_countId_eq_one (i : Fin l.length) :
|
||||
i ∈ l.withUniqueDualInOther l2 ↔ l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1 := by
|
||||
simp only [withUniqueDualInOther, Finset.mem_filter, Finset.mem_univ, true_and,
|
||||
List.get_eq_getElem]
|
||||
rw [mem_withDual_iff_countId_gt_one]
|
||||
rw [mem_withDualInOther_iff_countId_neq_zero]
|
||||
have hneq : l.countId (l.val.get i) ≠ 0 := by exact countId_index_neq_zero l i
|
||||
|
||||
|
||||
|
||||
|
||||
end IndexList
|
||||
|
||||
end IndexNotation
|
||||
|
|
@ -0,0 +1,379 @@
|
|||
/-
|
||||
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.IndexList.Basic
|
||||
/-!
|
||||
|
||||
# Indices which are dual in an index list
|
||||
|
||||
Given an list of indices we say two indices are dual if they have the same id.
|
||||
|
||||
For example the `0`, `2` and `3` index in `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` are pairwise dual to
|
||||
one another. The `1` (`'ᵘ²'`) index is not dual to any other index in the list.
|
||||
|
||||
We also define the notion of dual indices in different lists. For example,
|
||||
the `1` index in `l₁` is dual to the `1` and the `4` indices in
|
||||
`l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']`.
|
||||
|
||||
-/
|
||||
|
||||
|
||||
namespace IndexNotation
|
||||
|
||||
namespace IndexList
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
variable (l l2 l3 : IndexList X)
|
||||
|
||||
/-!
|
||||
|
||||
## Definitions
|
||||
|
||||
-/
|
||||
|
||||
/-- Two indices are dual if they are not equivalent, but have the same id. -/
|
||||
def AreDualInSelf (i j : Fin l.length) : Prop :=
|
||||
i ≠ j ∧ l.idMap i = l.idMap j
|
||||
|
||||
instance (i j : Fin l.length) : Decidable (l.AreDualInSelf i j) :=
|
||||
instDecidableAnd
|
||||
|
||||
/-- Two indices in different `IndexLists` are dual to one another if they have the same `id`. -/
|
||||
def AreDualInOther (i : Fin l.length) (j : Fin l2.length) :
|
||||
Prop := l.idMap i = l2.idMap j
|
||||
|
||||
instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) :
|
||||
Decidable (l.AreDualInOther l2 i j) := (l.idMap i).decEq (l2.idMap j)
|
||||
|
||||
/-- Given an `i`, if a dual exists in the same list,
|
||||
outputs the first such dual, otherwise outputs `none`. -/
|
||||
def getDual? (i : Fin l.length) : Option (Fin l.length) :=
|
||||
Fin.find (fun j => l.AreDualInSelf i j)
|
||||
|
||||
/-- Given an `i`, if a dual exists in the other list,
|
||||
outputs the first such dual, otherwise outputs `none`. -/
|
||||
def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) :=
|
||||
Fin.find (fun j => l.AreDualInOther l2 i j)
|
||||
|
||||
/-- The finite set of indices of an index list which have a dual in that index list. -/
|
||||
def withDual : Finset (Fin l.length) :=
|
||||
Finset.filter (fun i => (l.getDual? i).isSome) Finset.univ
|
||||
|
||||
/-- The finite set of indices of an index list which do not have a dual. -/
|
||||
def withoutDual : Finset (Fin l.length) :=
|
||||
Finset.filter (fun i => (l.getDual? i).isNone) Finset.univ
|
||||
|
||||
/-- The finite set of indices of an index list which have a dual in another provided index list. -/
|
||||
def withDualInOther : Finset (Fin l.length) :=
|
||||
Finset.filter (fun i => (l.getDualInOther? l2 i).isSome) Finset.univ
|
||||
|
||||
/-- The finite set of indices of an index list which have a unique dual in that index list. -/
|
||||
def withUniqueDual : Finset (Fin l.length) :=
|
||||
Finset.filter (fun i => i ∈ l.withDual ∧
|
||||
∀ j, l.AreDualInSelf i j → j = l.getDual? i) Finset.univ
|
||||
|
||||
/-- The finite set of indices of an index list which have a unique dual in another, provided, index
|
||||
list. -/
|
||||
def withUniqueDualInOther : Finset (Fin l.length) :=
|
||||
Finset.filter (fun i => i ∉ l.withDual ∧ i ∈ l.withDualInOther l2
|
||||
∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ
|
||||
|
||||
/-!
|
||||
|
||||
## Basic properties
|
||||
|
||||
-/
|
||||
|
||||
@[simp, nolint simpNF]
|
||||
lemma mem_withDual_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
|
||||
i ∈ l.withDual := by
|
||||
simp only [withUniqueDual, Finset.mem_filter, Finset.mem_univ, true_and] at h
|
||||
simpa using h.1
|
||||
|
||||
lemma mem_withDual_of_withUniqueDual (i : l.withUniqueDual) :
|
||||
i.1 ∈ l.withDual :=
|
||||
mem_withDual_of_mem_withUniqueDual l (↑i) i.2
|
||||
|
||||
lemma not_mem_withDual_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
|
||||
i.1 ∉ l.withDual := by
|
||||
have hi := i.2
|
||||
simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach,
|
||||
true_and] at hi
|
||||
exact hi.2.1
|
||||
|
||||
lemma mem_withDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther l2) :
|
||||
i.1 ∈ l.withDualInOther l2 := by
|
||||
have hi := i.2
|
||||
simp only [withUniqueDualInOther, Finset.univ_eq_attach, Finset.mem_filter, Finset.mem_attach,
|
||||
true_and] at hi
|
||||
exact hi.2.2.1
|
||||
|
||||
@[simp]
|
||||
lemma withDual_isSome (i : l.withDual) : (l.getDual? i).isSome := by
|
||||
simpa [withDual] using i.2
|
||||
|
||||
@[simp]
|
||||
lemma mem_withDual_iff_isSome (i : Fin l.length) : i ∈ l.withDual ↔ (l.getDual? i).isSome := by
|
||||
simp [withDual]
|
||||
|
||||
@[simp]
|
||||
lemma mem_withUniqueDual_isSome (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
|
||||
(l.getDual? i).isSome := by
|
||||
simpa [withDual] using mem_withDual_of_mem_withUniqueDual l i h
|
||||
|
||||
@[simp]
|
||||
lemma mem_withInDualOther_iff_isSome (i : Fin l.length) :
|
||||
i ∈ l.withDualInOther l2 ↔ (l.getDualInOther? l2 i).isSome := by
|
||||
simp only [withDualInOther, getDualInOther?, Finset.mem_filter, Finset.mem_univ, true_and]
|
||||
|
||||
@[simp]
|
||||
lemma mem_withUniqueDualInOther_isSome (i : Fin l.length) (hi : i ∈ l.withUniqueDualInOther l2) :
|
||||
(l.getDualInOther? l2 i).isSome := by
|
||||
simp only [withUniqueDualInOther, Finset.mem_filter, Finset.mem_univ, true_and] at hi
|
||||
exact (mem_withInDualOther_iff_isSome l l2 i).mp hi.2.1
|
||||
|
||||
lemma not_mem_withDual_iff_isNone (i : Fin l.length) :
|
||||
i ∉ l.withDual ↔ (l.getDual? i).isNone := by
|
||||
simp only [mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
|
||||
Option.isNone_iff_eq_none]
|
||||
|
||||
lemma mem_withDual_iff_exists : i ∈ l.withDual ↔ ∃ j, l.AreDualInSelf i j := by
|
||||
simp [withDual, Finset.mem_filter, Finset.mem_univ, getDual?]
|
||||
exact Fin.isSome_find_iff
|
||||
|
||||
lemma mem_withInDualOther_iff_exists :
|
||||
i ∈ l.withDualInOther l2 ↔ ∃ (j : Fin l2.length), l.AreDualInOther l2 i j := by
|
||||
simp [withDualInOther, Finset.mem_filter, Finset.mem_univ, getDualInOther?]
|
||||
exact Fin.isSome_find_iff
|
||||
|
||||
lemma withDual_disjoint_withoutDual : Disjoint l.withDual l.withoutDual := by
|
||||
rw [Finset.disjoint_iff_ne]
|
||||
intro a ha b hb
|
||||
by_contra hn
|
||||
subst hn
|
||||
simp_all only [withDual, Finset.mem_filter, Finset.mem_univ, true_and, withoutDual,
|
||||
Option.isNone_iff_eq_none, Option.isSome_none, Bool.false_eq_true]
|
||||
|
||||
lemma not_mem_withDual_of_mem_withoutDual (i : Fin l.length) (h : i ∈ l.withoutDual) :
|
||||
i ∉ l.withDual := by
|
||||
have h1 := l.withDual_disjoint_withoutDual
|
||||
exact Finset.disjoint_right.mp h1 h
|
||||
/-!
|
||||
## Are dual properties
|
||||
-/
|
||||
|
||||
namespace AreDualInSelf
|
||||
|
||||
variable {l l2 : IndexList X} {i j : Fin l.length}
|
||||
|
||||
instance (i j : Fin l.length) : Decidable (l.AreDualInSelf i j) :=
|
||||
instDecidableAnd
|
||||
|
||||
@[symm]
|
||||
lemma symm (h : l.AreDualInSelf i j) : l.AreDualInSelf j i := by
|
||||
simp only [AreDualInSelf] at h ⊢
|
||||
exact ⟨h.1.symm, h.2.symm⟩
|
||||
|
||||
@[simp]
|
||||
lemma self_false (i : Fin l.length) : ¬ l.AreDualInSelf i i := by
|
||||
simp [AreDualInSelf]
|
||||
|
||||
@[simp]
|
||||
lemma append_inl_inl : (l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inl j))
|
||||
↔ l.AreDualInSelf i j := by
|
||||
simp [AreDualInSelf]
|
||||
|
||||
@[simp]
|
||||
lemma append_inr_inr (l l2 : IndexList X) (i j : Fin l2.length) :
|
||||
(l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inr j))
|
||||
↔ l2.AreDualInSelf i j := by
|
||||
simp [AreDualInSelf]
|
||||
|
||||
@[simp]
|
||||
lemma append_inl_inr (l l2 : IndexList X) (i : Fin l.length) (j : Fin l2.length) :
|
||||
(l ++ l2).AreDualInSelf (appendEquiv (Sum.inl i)) (appendEquiv (Sum.inr j)) =
|
||||
l.AreDualInOther l2 i j := by
|
||||
simp [AreDualInSelf, AreDualInOther]
|
||||
|
||||
@[simp]
|
||||
lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length) :
|
||||
(l ++ l2).AreDualInSelf (appendEquiv (Sum.inr i)) (appendEquiv (Sum.inl j)) =
|
||||
l2.AreDualInOther l i j := by
|
||||
simp [AreDualInSelf, AreDualInOther]
|
||||
|
||||
end AreDualInSelf
|
||||
|
||||
namespace AreDualInOther
|
||||
|
||||
variable {l l2 l3 : IndexList X} {i : Fin l.length} {j : Fin l2.length}
|
||||
|
||||
instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) :
|
||||
Decidable (l.AreDualInOther l2 i j) := (l.idMap i).decEq (l2.idMap j)
|
||||
|
||||
@[symm]
|
||||
lemma symm (h : l.AreDualInOther l2 i j) : l2.AreDualInOther l j i := by
|
||||
rw [AreDualInOther] at h ⊢
|
||||
exact h.symm
|
||||
|
||||
@[simp]
|
||||
lemma append_of_inl (i : Fin l.length) (j : Fin l3.length) :
|
||||
(l ++ l2).AreDualInOther l3 (appendEquiv (Sum.inl i)) j ↔ l.AreDualInOther l3 i j := by
|
||||
simp [AreDualInOther]
|
||||
|
||||
@[simp]
|
||||
lemma append_of_inr (i : Fin l2.length) (j : Fin l3.length) :
|
||||
(l ++ l2).AreDualInOther l3 (appendEquiv (Sum.inr i)) j ↔ l2.AreDualInOther l3 i j := by
|
||||
simp [AreDualInOther]
|
||||
|
||||
@[simp]
|
||||
lemma of_append_inl (i : Fin l.length) (j : Fin l2.length) :
|
||||
l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inl j)) ↔ l.AreDualInOther l2 i j := by
|
||||
simp [AreDualInOther]
|
||||
|
||||
@[simp]
|
||||
lemma of_append_inr (i : Fin l.length) (j : Fin l3.length) :
|
||||
l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inr j)) ↔ l.AreDualInOther l3 i j := by
|
||||
simp [AreDualInOther]
|
||||
|
||||
end AreDualInOther
|
||||
/-!
|
||||
|
||||
## Basic properties of getDual?
|
||||
|
||||
-/
|
||||
|
||||
lemma getDual?_isSome_iff_exists (i : Fin l.length) :
|
||||
(l.getDual? i).isSome ↔ ∃ j, l.AreDualInSelf i j := by
|
||||
rw [getDual?, Fin.isSome_find_iff]
|
||||
|
||||
lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
|
||||
l.getDual? j = i ∨ l.getDual? i = j ∨ l.getDual? j = l.getDual? i := by
|
||||
have h3 : (l.getDual? i).isSome := by
|
||||
simpa [getDual?, Fin.isSome_find_iff] using ⟨j, h⟩
|
||||
obtain ⟨k, hk⟩ := Option.isSome_iff_exists.mp h3
|
||||
rw [hk]
|
||||
rw [getDual?, Fin.find_eq_some_iff] at hk
|
||||
by_cases hik : i < k
|
||||
· apply Or.inl
|
||||
rw [getDual?, Fin.find_eq_some_iff]
|
||||
apply And.intro h.symm
|
||||
intro k' hk'
|
||||
by_cases hik' : i = k'
|
||||
· exact Fin.ge_of_eq (id (Eq.symm hik'))
|
||||
· have hik'' : l.AreDualInSelf i k' := by
|
||||
simp [AreDualInSelf, hik']
|
||||
simp_all [AreDualInSelf]
|
||||
have hk'' := hk.2 k' hik''
|
||||
exact (lt_of_lt_of_le hik hk'').le
|
||||
· by_cases hjk : j ≤ k
|
||||
· apply Or.inr
|
||||
apply Or.inl
|
||||
have hj := hk.2 j h
|
||||
simp only [Option.some.injEq]
|
||||
exact Fin.le_antisymm hj hjk
|
||||
· apply Or.inr
|
||||
apply Or.inr
|
||||
rw [getDual?, Fin.find_eq_some_iff]
|
||||
apply And.intro
|
||||
· simp_all [AreDualInSelf]
|
||||
exact Fin.ne_of_gt hjk
|
||||
intro k' hk'
|
||||
by_cases hik' : i = k'
|
||||
· subst hik'
|
||||
exact Lean.Omega.Fin.le_of_not_lt hik
|
||||
· have hik'' : l.AreDualInSelf i k' := by
|
||||
simp [AreDualInSelf, hik']
|
||||
simp_all [AreDualInSelf]
|
||||
exact hk.2 k' hik''
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_neq_self (i : Fin l.length) : ¬ l.getDual? i = some i := by
|
||||
intro h
|
||||
simp [getDual?] at h
|
||||
rw [Fin.find_eq_some_iff] at h
|
||||
simp [AreDualInSelf] at h
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_get_neq_self (i : Fin l.length) (h : (l.getDual? i).isSome) :
|
||||
¬ (l.getDual? i).get h = i := by
|
||||
have h1 := l.getDual?_neq_self i
|
||||
by_contra hn
|
||||
have h' : l.getDual? i = some i := by
|
||||
nth_rewrite 2 [← hn]
|
||||
exact Option.eq_some_of_isSome h
|
||||
exact h1 h'
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_get_id (i : Fin l.length) (h : (l.getDual? i).isSome) :
|
||||
l.idMap ((l.getDual? i).get h) = l.idMap i := by
|
||||
have h1 : l.getDual? i = some ((l.getDual? i).get h) := Option.eq_some_of_isSome h
|
||||
nth_rewrite 1 [getDual?] at h1
|
||||
rw [Fin.find_eq_some_iff] at h1
|
||||
simp [AreDualInSelf] at h1
|
||||
exact h1.1.2.symm
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_get_areDualInSelf (i : Fin l.length) (h : (l.getDual? i).isSome) :
|
||||
l.AreDualInSelf ((l.getDual? i).get h) i := by
|
||||
simp [AreDualInSelf]
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_areDualInSelf_get (i : Fin l.length) (h : (l.getDual? i).isSome) :
|
||||
l.AreDualInSelf i ((l.getDual? i).get h) :=
|
||||
AreDualInSelf.symm (getDual?_get_areDualInSelf l i h)
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_getDual?_get_isSome (i : Fin l.length) (h : (l.getDual? i).isSome) :
|
||||
(l.getDual? ((l.getDual? i).get h)).isSome := by
|
||||
rw [getDual?, Fin.isSome_find_iff]
|
||||
exact ⟨i, getDual?_get_areDualInSelf l i h⟩
|
||||
|
||||
/-!
|
||||
|
||||
## Basic properties of getDualInOther?
|
||||
|
||||
-/
|
||||
|
||||
lemma getDualInOther?_isSome_iff_exists (i : Fin l.length) :
|
||||
(l.getDualInOther? l2 i).isSome ↔ ∃ j, l.AreDualInOther l2 i j := by
|
||||
rw [getDualInOther?, Fin.isSome_find_iff]
|
||||
|
||||
@[simp]
|
||||
lemma getDualInOther?_id (i : Fin l.length) (h : (l.getDualInOther? l2 i).isSome) :
|
||||
l2.idMap ((l.getDualInOther? l2 i).get h) = l.idMap i := by
|
||||
have h1 : l.getDualInOther? l2 i = some ((l.getDualInOther? l2 i).get h) :=
|
||||
Option.eq_some_of_isSome h
|
||||
nth_rewrite 1 [getDualInOther?] at h1
|
||||
rw [Fin.find_eq_some_iff] at h1
|
||||
simp [AreDualInOther] at h1
|
||||
exact h1.1.symm
|
||||
|
||||
@[simp]
|
||||
lemma getDualInOther?_get_areDualInOther (i : Fin l.length) (h : (l.getDualInOther? l2 i).isSome) :
|
||||
l2.AreDualInOther l ((l.getDualInOther? l2 i).get h) i := by
|
||||
simp [AreDualInOther]
|
||||
|
||||
@[simp]
|
||||
lemma getDualInOther?_areDualInOther_get (i : Fin l.length) (h : (l.getDualInOther? l2 i).isSome) :
|
||||
l.AreDualInOther l2 i ((l.getDualInOther? l2 i).get h) :=
|
||||
AreDualInOther.symm (getDualInOther?_get_areDualInOther l l2 i h)
|
||||
|
||||
@[simp]
|
||||
lemma getDualInOther?_getDualInOther?_get_isSome (i : Fin l.length)
|
||||
(h : (l.getDualInOther? l2 i).isSome) :
|
||||
(l2.getDualInOther? l ((l.getDualInOther? l2 i).get h)).isSome := by
|
||||
rw [getDualInOther?, Fin.isSome_find_iff]
|
||||
exact ⟨i, getDualInOther?_get_areDualInOther l l2 i h⟩
|
||||
|
||||
@[simp]
|
||||
lemma getDualInOther?_self_isSome (i : Fin l.length) :
|
||||
(l.getDualInOther? l i).isSome := by
|
||||
simp [getDualInOther?]
|
||||
rw [@Fin.isSome_find_iff]
|
||||
exact ⟨i, rfl⟩
|
||||
|
||||
end IndexList
|
||||
|
||||
end IndexNotation
|
||||
|
|
@ -997,8 +997,7 @@ lemma mem_withUniqueDual_iff_countId_eq_two (i : Fin l.length) :
|
|||
(fun h => l.mem_withUniqueDual_of_countId_eq_two i h)
|
||||
|
||||
lemma getDual?_isSome_of_countId_eq_two {i : Fin l.length}
|
||||
(h : l.countId (l.val.get i) = 2) :
|
||||
(l.getDual? i).isSome := by
|
||||
(h : l.countId (l.val.get i) = 2) : (l.getDual? i).isSome := by
|
||||
rw [← l.mem_withUniqueDual_iff_countId_eq_two] at h
|
||||
exact mem_withUniqueDual_isSome l i h
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue