DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: version which builds

Browse source
This commit is contained in:
jstoobysmith 2024-08-28 14:35:01 -04:00
parent 47d639bb1a
commit b96e437c45
14 changed files with 61 additions and 3150 deletions
Download patch file Download diff file Expand all files Collapse all files

15
HepLean.lean
View file

@ -76,20 +76,21 @@ import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Basic
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.IndexNotation
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Lemmas
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.RisingLowering
import HepLean.SpaceTime.LorentzTensor.IndexNotation.AreDual
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Append
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Basic
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Contraction
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Relations
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Contraction
import HepLean.SpaceTime.LorentzTensor.IndexNotation.GetDual
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Basic
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Color
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Contraction
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.CountId
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Duals
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Equivs
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.OnlyUniqueDuals
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Subperm
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
import HepLean.SpaceTime.LorentzTensor.IndexNotation.OnlyUniqueDuals
import HepLean.SpaceTime.LorentzTensor.IndexNotation.TensorIndex
import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithDual
import HepLean.SpaceTime.LorentzTensor.IndexNotation.WithUniqueDual
import HepLean.SpaceTime.LorentzTensor.MulActionTensor
import HepLean.SpaceTime.LorentzTensor.Real.Basic
import HepLean.SpaceTime.LorentzTensor.Real.IndexNotation

8
HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean
View file

@ -61,7 +61,7 @@ noncomputable def fromIndexStringColor {R : Type} [CommSemiring R]
(T : (einsteinTensor R m).Tensor cn) (s : String)
(hs : listCharIsIndexString einsteinTensorColor.Color s.toList = true)
(hn : n = (toIndexList' s hs).length)
(hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
(hD : (toIndexList' s hs).OnlyUniqueDuals)
(hC : IndexList.ColorCond.bool (toIndexList' s hs))
(hd : TensorColor.ColorMap.DualMap.boolFin'
(toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) :
@ -76,7 +76,7 @@ lemma fromIndexStringColor_indexList {R : Type} [CommSemiring R]
(T : (einsteinTensor R m).Tensor cn) (s : String)
(hs : listCharIsIndexString einsteinTensorColor.Color s.toList = true)
(hn : n = (toIndexList' s hs).length)
(hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
(hD : (toIndexList' s hs).OnlyUniqueDuals)
(hC : IndexList.ColorCond.bool (toIndexList' s hs))
(hd : TensorColor.ColorMap.DualMap.boolFin'
(toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) :
@ -93,7 +93,7 @@ macro "dualMapTactic" : tactic =>
Conditions are checked automatically. -/
notation:20 T "|" S:21 => fromIndexStringColor T S
(by decide)
(by decide) (by decide)
(by decide) (by rfl)
(by decide)
(by dualMapTactic)
@ -102,7 +102,7 @@ macro "prodTactic" : tactic =>
`(tactic| {
apply (ColorIndexList.AppendCond.iff_bool _ _).mpr
change @ColorIndexList.AppendCond.bool einsteinTensorColor
instIndexNotationColorEinsteinTensorColor instDecidableEqColorEinsteinTensorColor _ _
instDecidableEqColorEinsteinTensorColor _ _
simp only [prod_toIndexList, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
toTensorColor_eq, decidableEq_eq_color]
decide})

120
HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean
View file

@ -1,120 +0,0 @@
/-
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
/-!
# 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)
/-!
## Are dual indices
-/
/-- 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
/-- 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
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
end IndexList
end IndexNotation

1
HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
View file

@ -198,5 +198,6 @@ def tailNat (s : IndexRep X) : List ℕ := s.tail.map charToNat
/-- The id of an index, as a natural number. -/
def id (s : IndexRep X) : ℕ := s.tailNat.foldl (fun a b => 10 * a + b) 0
def toIndex (s : IndexRep X) : Index X := (s.toColor, s.id)
end IndexRep
end IndexNotation

626
HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean
View file

@ -1,626 +0,0 @@
/-
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 Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Data.Finset.Sort
import Mathlib.Tactic.FinCases
/-!
# Contraction of an index list.
In this file we define the contraction of an index list `l` to be the index list formed by
by the subset of indices of `l` which do not have a dual in `l`.
For example, the contraction of the index list `['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` is the index list
`['ᵘ²']`.
We also define the following finite sets
- `l.withoutDual` the finite set of indices of `l` which do not have a dual in `l`.
- `l.withUniqueDualLT` the finite set of those indices of `l` which have a unique dual, and
for which that dual is greater-then (determined by the ordering on `Fin`) then the index itself.
- `l.withUniqueDualGT` the finite set of those indices of `l` which have a unique dual, and
for which that dual is less-then (determined by the ordering on `Fin`) then the index itself.
We define an equivalence `l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual`.
We prove properties related to when `l.withUniqueDualInOther l2 = Finset.univ` for two
index lists `l` and `l2`.
-/
namespace IndexNotation
namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 l3 : IndexList X)
/-!
## Indices which do not have duals.
-/
/-- 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
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
lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ := by
rw [Finset.eq_univ_iff_forall]
intro i
by_cases h : (l.getDual? i).isSome
· simp [withDual, Finset.mem_filter, Finset.mem_univ, h]
· simp at h
simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h]
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 list_ofFn_withoutDualEquiv_eq_sort :
List.ofFn (Subtype.val ∘ l.withoutDualEquiv) = l.withoutDual.sort (fun i j => i ≤ j) := by
rw [@List.ext_get_iff]
refine And.intro ?_ (fun n h1 h2 => ?_)
· simp only [List.length_ofFn, Finset.length_sort]
· simp only [List.get_eq_getElem, List.getElem_ofFn, Function.comp_apply]
rfl
lemma withoutDual_sort_eq_filter : l.withoutDual.sort (fun i j => i ≤ j) =
(List.finRange l.length).filter (fun i => i ∈ l.withoutDual) := by
rw [withoutDual]
rw [← filter_sort_comm]
simp only [Option.isNone_iff_eq_none, Finset.mem_filter, Finset.mem_univ, true_and]
apply congrArg
exact Fin.sort_univ l.length
/-- An equivalence splitting the indices of an index list `l` into those indices
which have a dual in `l` and those which do not have a dual in `l`. -/
def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
(Equiv.sumCongr (Equiv.refl _) l.withoutDualEquiv).trans <|
(Equiv.Finset.union _ _ l.withDual_disjoint_withoutDual).trans <|
Equiv.subtypeUnivEquiv (by simp [withDual_union_withoutDual])
/-!
## The contraction list
-/
/-- The index list formed from `l` by selecting only those indices in `l` which
do not have a dual. -/
def contrIndexList : IndexList X where
val := l.val.filter (fun I => l.countId I = 1)
@[simp]
lemma contrIndexList_empty : (⟨[]⟩ : IndexList X).contrIndexList = { val := [] } := by
apply ext
simp [contrIndexList]
lemma contrIndexList_val : l.contrIndexList.val =
l.val.filter (fun I => l.countId I = 1) := by
rfl
/-- An alternative form of the contracted index list. -/
@[simp]
def contrIndexList' : IndexList X where
val := List.ofFn (l.val.get ∘ Subtype.val ∘ l.withoutDualEquiv)
lemma contrIndexList_eq_contrIndexList' : l.contrIndexList = l.contrIndexList' := by
apply ext
simp only [contrIndexList']
trans List.map l.val.get (List.ofFn (Subtype.val ∘ ⇑l.withoutDualEquiv))
· rw [list_ofFn_withoutDualEquiv_eq_sort, withoutDual_sort_eq_filter]
simp only [contrIndexList]
let f1 : Index X → Bool := fun (I : Index X) => l.countId I = 1
let f2 : (Fin l.length) → Bool := fun i => i ∈ l.withoutDual
change List.filter f1 l.val = List.map l.val.get (List.filter f2 (List.finRange l.length))
have hf : f2 = f1 ∘ l.val.get := by
funext i
simp only [mem_withoutDual_iff_countId_eq_one l, List.get_eq_getElem, Function.comp_apply, f2,
f1]
rw [hf, ← List.filter_map]
apply congrArg
simp [length]
· simp only [List.map_ofFn]
@[simp]
lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by
simp [contrIndexList_eq_contrIndexList', withoutDual, length]
@[simp]
lemma contrIndexList_idMap (i : Fin l.contrIndexList.length) : l.contrIndexList.idMap i
= l.idMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
simp [contrIndexList_eq_contrIndexList', idMap]
rfl
@[simp]
lemma contrIndexList_colorMap (i : Fin l.contrIndexList.length) : l.contrIndexList.colorMap i
= l.colorMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
simp [contrIndexList_eq_contrIndexList', colorMap]
rfl
lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) :
l.contrIndexList.AreDualInSelf i j ↔
l.AreDualInSelf (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1
(l.withoutDualEquiv (Fin.cast l.contrIndexList_length j)).1 := by
simp [AreDualInSelf]
intro _
trans ¬ (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)) =
(l.withoutDualEquiv (Fin.cast l.contrIndexList_length j))
· rw [l.withoutDualEquiv.apply_eq_iff_eq]
simp [Fin.ext_iff]
· exact Iff.symm Subtype.coe_ne_coe
@[simp]
lemma contrIndexList_getDual? (i : Fin l.contrIndexList.length) :
l.contrIndexList.getDual? i = none := by
rw [← Option.not_isSome_iff_eq_none, ← mem_withDual_iff_isSome, mem_withDual_iff_exists]
simp only [contrIndexList_areDualInSelf, not_exists]
have h1 := (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).2
have h1' := Finset.disjoint_right.mp l.withDual_disjoint_withoutDual h1
rw [mem_withDual_iff_exists] at h1'
exact fun x => forall_not_of_not_exists h1'
↑(l.withoutDualEquiv (Fin.cast (contrIndexList_length l) x))
@[simp]
lemma contrIndexList_withDual : l.contrIndexList.withDual = ∅ := by
rw [Finset.eq_empty_iff_forall_not_mem]
intro x
simp [withDual]
@[simp]
lemma contrIndexList_areDualInSelf_false (i j : Fin l.contrIndexList.length) :
l.contrIndexList.AreDualInSelf i j ↔ False := by
refine Iff.intro (fun h => ?_) (fun h => False.elim h)
have h1 : i ∈ l.contrIndexList.withDual := by
rw [@mem_withDual_iff_exists]
exact Exists.intro j h
simp_all
@[simp]
lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList = l := by
have h1 := l.withDual_union_withoutDual
rw [h, Finset.empty_union] at h1
apply ext
rw [@List.ext_get_iff]
change l.contrIndexList.length = l.length ∧ _
rw [contrIndexList_length, h1]
simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and]
intro n h1' h2
simp [contrIndexList_eq_contrIndexList']
congr
simp [withoutDualEquiv]
simp [h1]
rw [(Finset.orderEmbOfFin_unique' _
(fun x => Finset.mem_univ ((Fin.castOrderIso _).toOrderEmbedding x))).symm]
· exact Eq.symm (Nat.add_zero n)
· rw [h1]
exact Finset.card_fin l.length
lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrIndexList := by
simp
@[simp]
lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) :
l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by
simp [getDualInOther?]
rw [@Fin.find_eq_some_iff]
simp [AreDualInOther]
intro j hj
have h1 : i = j := by
by_contra hn
have h : l.contrIndexList.AreDualInSelf i j := by
simp only [AreDualInSelf]
simp [hj]
exact hn
exact (contrIndexList_areDualInSelf_false l i j).mp h
exact Fin.ge_of_eq (id (Eq.symm h1))
lemma mem_contrIndexList_countId {I : Index X} (h : I ∈ l.contrIndexList.val) :
l.countId I = 1 := by
simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at h
exact h.2
lemma mem_contrIndexList_filter {I : Index X} (h : I ∈ l.contrIndexList.val) :
l.val.filter (fun J => I.id = J.id) = [I] := by
have h1 : (l.val.filter (fun J => I.id = J.id)).length = 1 := by
rw [← List.countP_eq_length_filter]
exact l.mem_contrIndexList_countId h
have h2 : I ∈ l.val.filter (fun J => I.id = J.id) := by
simp only [List.mem_filter, decide_True, and_true]
simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at h
exact h.1
rw [List.length_eq_one] at h1
obtain ⟨J, hJ⟩ := h1
rw [hJ] at h2
simp at h2
subst h2
exact hJ
lemma cons_contrIndexList_of_countId_eq_zero {I : Index X}
(h : l.countId I = 0) :
(l.cons I).contrIndexList = l.contrIndexList.cons I := by
apply ext
simp [contrIndexList, countId]
rw [List.filter_cons_of_pos]
· apply congrArg
apply List.filter_congr
intro J hJ
simp only [decide_eq_decide]
rw [countId, List.countP_eq_zero] at h
simp only [decide_eq_true_eq] at h
rw [List.countP_cons_of_neg]
simp only [decide_eq_true_eq]
exact fun a => h J hJ (id (Eq.symm a))
· simp only [decide_True, List.countP_cons_of_pos, add_left_eq_self, decide_eq_true_eq]
exact h
lemma cons_contrIndexList_of_countId_neq_zero {I : Index X} (h : l.countId I ≠ 0) :
(l.cons I).contrIndexList.val = l.contrIndexList.val.filter (fun J => ¬ I.id = J.id) := by
simp only [contrIndexList, countId, cons_val, decide_not, List.filter_filter, Bool.not_eq_true',
decide_eq_false_iff_not, decide_eq_true_eq, Bool.decide_and]
rw [List.filter_cons_of_neg]
· apply List.filter_congr
intro J hJ
by_cases hI : I.id = J.id
· simp only [hI, decide_True, List.countP_cons_of_pos, add_left_eq_self, Bool.not_true,
Bool.false_and, decide_eq_false_iff_not, countId]
rw [countId, hI] at h
simp only [h, not_false_eq_true]
· simp only [hI, decide_False, Bool.not_false, Bool.true_and, decide_eq_decide]
rw [List.countP_cons_of_neg]
simp only [decide_eq_true_eq]
exact fun a => hI (id (Eq.symm a))
· simp only [decide_True, List.countP_cons_of_pos, add_left_eq_self, decide_eq_true_eq]
exact h
lemma mem_contrIndexList_countId_contrIndexList {I : Index X} (h : I ∈ l.contrIndexList.val) :
l.contrIndexList.countId I = 1 := 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]
simp only [countId]
rw [List.countP_filter, List.countP_filter]
simp only [decide_eq_true_eq, Bool.decide_and]
congr
funext a
rw [Bool.and_comm]
· rw [l.mem_contrIndexList_filter h, List.countP_cons_of_pos]
· rfl
· simp only [decide_eq_true_eq]
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
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]
simp only [countId]
rw [List.countP_filter, List.countP_filter]
simp only [decide_eq_true_eq, Bool.decide_and]
congr
funext a
rw [Bool.and_comm]
· rw [countId_eq_length_filter, List.length_eq_zero] at h
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
-/
instance (i j : Option (Fin l.length)) : Decidable (i < j) :=
match i, j with
| none, none => isFalse (fun a => a)
| none, some _ => isTrue (by trivial)
| some _, none => isFalse (fun a => a)
| some i, some j => Fin.decLt i j
/-- The finite set of those indices of `l` which have a unique dual, and for which
that dual is greater-then (determined by the ordering on `Fin`) then the index itself. -/
def withUniqueDualLT : Finset (Fin l.length) :=
Finset.filter (fun i => i < l.getDual? i) l.withUniqueDual
/-- The casting of an element of `withUniqueDualLT` to an element of `withUniqueDual`. -/
def withUniqueDualLTToWithUniqueDual (i : l.withUniqueDualLT) : l.withUniqueDual :=
⟨i.1, Finset.mem_of_mem_filter i.1 i.2⟩
instance : Coe l.withUniqueDualLT l.withUniqueDual where
coe := l.withUniqueDualLTToWithUniqueDual
/-- The finite set of those indices of `l` which have a unique dual, and for which
that dual is less-then (determined by the ordering on `Fin`) then the index itself. -/
def withUniqueDualGT : Finset (Fin l.length) :=
Finset.filter (fun i => ¬ i < l.getDual? i) l.withUniqueDual
/-- The casting of an element in `withUniqueDualGT` to an element of `withUniqueDual`. -/
def withUniqueDualGTToWithUniqueDual (i : l.withUniqueDualGT) : l.withUniqueDual :=
⟨i.1, Finset.mem_of_mem_filter _ i.2⟩
instance : Coe l.withUniqueDualGT l.withUniqueDual where
coe := l.withUniqueDualGTToWithUniqueDual
lemma withUniqueDualLT_disjoint_withUniqueDualGT :
Disjoint l.withUniqueDualLT l.withUniqueDualGT := by
rw [Finset.disjoint_iff_inter_eq_empty]
exact @Finset.filter_inter_filter_neg_eq (Fin l.length) _ _ _ _ _
lemma withUniqueDualLT_union_withUniqueDualGT :
l.withUniqueDualLT ∪ l.withUniqueDualGT = l.withUniqueDual :=
Finset.filter_union_filter_neg_eq _ _
/-! TODO: Replace with a mathlib lemma. -/
lemma option_not_lt (i j : Option (Fin l.length)) : i < j → i ≠ j → ¬ j < i := by
match i, j with
| none, none =>
exact fun a _ _ => a
| none, some k =>
exact fun _ _ a => a
| some i, none =>
exact fun h _ _ => h
| some i, some j =>
intro h h'
simp_all
change i < j at h
change ¬ j < i
exact Fin.lt_asymm h
/-! TODO: Replace with a mathlib lemma. -/
lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → i < j := by
match i, j with
| none, none =>
exact fun a b => a (a (a (b rfl)))
| none, some k =>
exact fun _ _ => trivial
| some i, none =>
exact fun a _ => a trivial
| some i, some j =>
intro h h'
simp_all
change ¬ j < i at h
change i < j
omega
/-- The equivalence between `l.withUniqueDualLT` and `l.withUniqueDualGT` obtained by
taking an index to its dual. -/
def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where
toFun i := ⟨l.getDualEquiv i, by
have hi := i.2
simp only [withUniqueDualGT, Finset.mem_filter, Finset.coe_mem, true_and]
simp only [getDualEquiv, Equiv.coe_fn_mk, Option.some_get, Finset.coe_mem,
getDual?_getDual?_get_of_withUniqueDual]
simp only [withUniqueDualLT, Finset.mem_filter] at hi
apply option_not_lt
· simpa [withUniqueDualLTToWithUniqueDual] using hi.2
· exact Ne.symm (getDual?_neq_self l i)⟩
invFun i := ⟨l.getDualEquiv.symm i, by
have hi := i.2
simp only [withUniqueDualLT, Finset.mem_filter, Finset.coe_mem, true_and, gt_iff_lt]
simp only [getDualEquiv, Equiv.coe_fn_symm_mk, Option.some_get, Finset.coe_mem,
getDual?_getDual?_get_of_withUniqueDual]
simp only [withUniqueDualGT, Finset.mem_filter] at hi
apply lt_option_of_not
· simpa [withUniqueDualLTToWithUniqueDual] using hi.2
· exact (getDual?_neq_self l i)⟩
left_inv x := SetCoe.ext (by simp [withUniqueDualGTToWithUniqueDual,
withUniqueDualLTToWithUniqueDual])
right_inv x := SetCoe.ext (by simp [withUniqueDualGTToWithUniqueDual,
withUniqueDualLTToWithUniqueDual])
/-- An equivalence from `l.withUniqueDualLT ⊕ l.withUniqueDualLT` to `l.withUniqueDual`.
The first `l.withUniqueDualLT` are taken to themselves, whilst the second copy are
taken to their dual. -/
def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual := by
apply (Equiv.sumCongr (Equiv.refl _) l.withUniqueDualLTEquivGT).trans
apply (Equiv.Finset.union _ _ l.withUniqueDualLT_disjoint_withUniqueDualGT).trans
apply (Equiv.subtypeEquivRight (by simp only [l.withUniqueDualLT_union_withUniqueDualGT,
implies_true]))
/-!
## withUniqueDualInOther equal univ
-/
/-! TODO: There is probably a better place for this section. -/
lemma withUniqueDualInOther_eq_univ_fst_withDual_empty
(h : l.withUniqueDualInOther l2 = Finset.univ) : l.withDual = ∅ := by
rw [@Finset.eq_empty_iff_forall_not_mem]
intro x
have hx : x ∈ l.withUniqueDualInOther l2 := by
rw [h]
exact Finset.mem_univ x
rw [withUniqueDualInOther] at hx
simp only [mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and] at hx
simpa using hx.1
lemma withUniqueDualInOther_eq_univ_fst_eq_contrIndexList
(h : l.withUniqueDualInOther l2 = Finset.univ) :
l = l.contrIndexList := by
refine Eq.symm (contrIndexList_of_withDual_empty l ?h)
exact withUniqueDualInOther_eq_univ_fst_withDual_empty l l2 h
lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length)
(h : l.withUniqueDualInOther l2 = Finset.univ) :
l2.withUniqueDualInOther l = Finset.univ := by
let S' : Finset (Fin l2.length) :=
Finset.map ⟨Subtype.val, Subtype.val_injective⟩
(Equiv.finsetCongr
(l.getDualInOtherEquiv l2) Finset.univ)
have hSCard : S'.card = l2.length := by
rw [Finset.card_map]
simp only [Finset.univ_eq_attach, Equiv.finsetCongr_apply, Finset.card_map, Finset.card_attach]
rw [h, ← hl]
exact Finset.card_fin l.length
have hsCardUn : S'.card = (@Finset.univ (Fin l2.length)).card := by
rw [hSCard]
exact Eq.symm (Finset.card_fin l2.length)
have hS'Eq : S' = (l2.withUniqueDualInOther l) := by
rw [@Finset.ext_iff]
intro a
simp only [S']
simp
rw [hS'Eq] at hsCardUn
exact (Finset.card_eq_iff_eq_univ (l2.withUniqueDualInOther l)).mp hsCardUn
lemma withUniqueDualInOther_eq_univ_contr_refl :
l.contrIndexList.withUniqueDualInOther l.contrIndexList = Finset.univ := by
rw [@Finset.eq_univ_iff_forall]
intro x
simp only [withUniqueDualInOther, mem_withDual_iff_isSome,
Option.isSome_none, Bool.false_eq_true, not_false_eq_true, mem_withInDualOther_iff_isSome,
getDualInOther?_self_isSome, true_and, Finset.mem_filter, Finset.mem_univ]
simp only [contrIndexList_getDual?, Option.isSome_none, Bool.false_eq_true, not_false_eq_true,
contrIndexList_getDualInOther?_self, Option.some.injEq, true_and]
intro j hj
have h1 : j = x := by
by_contra hn
have hj : l.contrIndexList.AreDualInSelf x j := by
simp [AreDualInOther] at hj
simp only [AreDualInSelf, ne_eq, contrIndexList_idMap, hj, and_true]
exact fun a => hn (id (Eq.symm a))
exact (contrIndexList_areDualInSelf_false l x j).mp hj
exact h1
lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Finset.univ)
(h' : l2.withUniqueDualInOther l3 = Finset.univ) :
l.withUniqueDualInOther l3 = Finset.univ := by
rw [Finset.eq_univ_iff_forall]
intro i
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and]
have hi : i ∈ l.withUniqueDualInOther l2 := by
rw [h]
exact Finset.mem_univ i
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and] at hi
have hi2 : ((l.getDualInOther? l2 i).get hi.2.1) ∈ l2.withUniqueDualInOther l3 := by
rw [h']
exact Finset.mem_univ ((l.getDualInOther? l2 i).get hi.right.left)
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and] at hi2
apply And.intro hi.1
apply And.intro
· rw [@getDualInOther?_isSome_iff_exists]
use (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1
simp only [AreDualInOther, getDualInOther?_id]
intro j hj
have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by
rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
simpa only [AreDualInOther, getDualInOther?_id] using hj
rw [h']
exact Finset.mem_univ ((l.getDualInOther? l2 i).get hi.right.left)
have hs : (l.getDualInOther? l3 i).isSome := by
rw [@getDualInOther?_isSome_iff_exists]
exact Exists.intro j hj
have hs' : (l.getDualInOther? l3 i).get hs = (l2.getDualInOther? l3
((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by
rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
simp only [AreDualInOther, getDualInOther?_id]
rw [h']
exact Finset.mem_univ ((l.getDualInOther? l2 i).get hi.right.left)
rw [← hj'] at hs'
rw [← hs']
exact Eq.symm (Option.eq_some_of_isSome hs)
lemma withUniqueDualInOther_eq_univ_iff_forall :
l.withUniqueDualInOther l2 = Finset.univ ↔
∀ (x : Fin l.length), l.getDual? x = none ∧ (l.getDualInOther? l2 x).isSome = true ∧
∀ (j : Fin l2.length), l.AreDualInOther l2 x j → some j = l.getDualInOther? l2 x := by
rw [Finset.eq_univ_iff_forall]
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and]
end IndexList
end IndexNotation

519
HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean
View file

@ -1,519 +0,0 @@
/-
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.AreDual
import Mathlib.Algebra.Order.Ring.Nat
/-!
# Getting dual index
Using the option-monad we define two functions:
- For a list of indices `l₁` the function `getDual?` takes in an index `i` in `l₁` and retruns
the the first index in `l₁` dual to `i`. If no such index exists, it returns `none`.
- For two lists of indices `l₁` and `l₂` the function `getDualInOther?` takes in an index `i`
in `l₁` and returns the first index in `l₂` dual to `i`. If no such index exists,
it returns `none`.
For example, given the lists `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']`, we have
- `getDual? 0 = some 2`, `getDual? 1 = none`, `getDual? 2 = some 0`, `getDual? 3 = some 0`.
Given the lists `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` and `l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']`, we have
- `l₁.getDualInOther? l₂ 0 = none`, `l₁.getDualInOther? l₂ 1 = some 1`,
`l₁.getDualInOther? l₂ 2 = none`, `l₁.getDualInOther? l₂ 3 = none`.
We prove some basic properties of `getDual?` and `getDualInOther?`. In particular,
we prove lemmas related to how `getDual?` and `getDualInOther?` behave when we appending
two index lists.
-/
namespace IndexNotation
namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 : IndexList X)
/-!
## The getDual? Function
-/
/-- 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)
/-!
## 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⟩
/-!
## Append properties of getDual?
-/
@[simp]
lemma getDual?_isSome_append_inl_iff (i : Fin l.length) :
((l ++ l2).getDual? (appendEquiv (Sum.inl i))).isSome ↔
(l.getDual? i).isSome ∨ (l.getDualInOther? l2 i).isSome := by
rw [getDual?_isSome_iff_exists, getDual?_isSome_iff_exists, getDualInOther?_isSome_iff_exists]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· obtain ⟨j, hj⟩ := h
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
exact Or.inl ⟨k, AreDualInSelf.append_inl_inl.mp hj⟩
| Sum.inr k =>
exact Or.inr ⟨k, by simpa only [AreDualInSelf.append_inl_inr] using hj⟩
· cases' h with h h <;>
obtain ⟨j, hj⟩ := h
· exact ⟨appendEquiv (Sum.inl j), AreDualInSelf.append_inl_inl.mpr hj⟩
· use appendEquiv (Sum.inr j)
simpa only [AreDualInSelf.append_inl_inr] using hj
@[simp]
lemma getDual?_isSome_append_inr_iff (i : Fin l2.length) :
((l ++ l2).getDual? (appendEquiv (Sum.inr i))).isSome ↔
(l2.getDual? i).isSome ∨ (l2.getDualInOther? l i).isSome := by
rw [getDual?_isSome_iff_exists, getDual?_isSome_iff_exists, getDualInOther?_isSome_iff_exists]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· obtain ⟨j, hj⟩ := h
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
exact Or.inr ⟨k, by simpa using hj⟩
| Sum.inr k =>
exact Or.inl ⟨k, (AreDualInSelf.append_inr_inr l l2 i k).mp hj⟩
· cases' h with h h <;>
obtain ⟨j, hj⟩ := h
· exact ⟨appendEquiv (Sum.inr j), (AreDualInSelf.append_inr_inr l l2 i j).mpr hj⟩
· use appendEquiv (Sum.inl j)
simpa only [AreDualInSelf.append_inr_inl] using hj
lemma getDual?_isSome_append_symm (i : Fin l.length) :
((l ++ l2).getDual? (appendEquiv (Sum.inl i))).isSome ↔
((l2 ++ l).getDual? (appendEquiv (Sum.inr i))).isSome := by
simp
@[simp]
lemma getDual?_eq_none_append_inl_iff (i : Fin l.length) :
(l ++ l2).getDual? (appendEquiv (Sum.inl i)) = none ↔
l.getDual? i = none ∧ l.getDualInOther? l2 i = none := by
apply Iff.intro
· intro h
have h1 := (l.getDual?_isSome_append_inl_iff l2 i).mpr.mt
simp only [not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, imp_self] at h1
exact h1 h
· intro h
have h1 := (l.getDual?_isSome_append_inl_iff l2 i).mp.mt
simp only [not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, imp_self] at h1
exact h1 h
@[simp]
lemma getDual?_eq_none_append_inr_iff (i : Fin l2.length) :
(l ++ l2).getDual? (appendEquiv (Sum.inr i)) = none ↔
(l2.getDual? i = none ∧ l2.getDualInOther? l i = none) := by
apply Iff.intro
· intro h
have h1 := (l.getDual?_isSome_append_inr_iff l2 i).mpr.mt
simp only [not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, imp_self] at h1
exact h1 h
· intro h
have h1 := (l.getDual?_isSome_append_inr_iff l2 i).mp.mt
simp only [not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, imp_self] at h1
exact h1 h
@[simp]
lemma getDual?_append_inl_of_getDual?_isSome (i : Fin l.length) (h : (l.getDual? i).isSome) :
(l ++ l2).getDual? (appendEquiv (Sum.inl i)) =
some (appendEquiv (Sum.inl ((l.getDual? i).get h))) := by
rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inl]
apply And.intro (getDual?_get_areDualInSelf l i h).symm
intro j hj
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, ge_iff_le]
rw [Fin.le_def]
have h2 : l.getDual? i = some (((l.getDual? i).get h)) := Option.eq_some_of_isSome h
nth_rewrite 1 [getDual?] at h2
rw [Fin.find_eq_some_iff] at h2
exact h2.2 k (AreDualInSelf.append_inl_inl.mp hj)
| Sum.inr k =>
simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le]
rw [Fin.le_def]
simp only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast,
Fin.coe_castAdd, Fin.coe_natAdd]
omega
@[simp]
lemma getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome (i : Fin l.length)
(hi : (l.getDual? i).isNone) (h : (l.getDualInOther? l2 i).isSome) :
(l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some
(appendEquiv (Sum.inr ((l.getDualInOther? l2 i).get h))) := by
rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inr]
apply And.intro (getDualInOther?_areDualInOther_get l l2 i h)
intro j hj
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
rw [AreDualInSelf.append_inl_inl] at hj
simp only [getDual?, Finset.mem_filter, Finset.mem_univ, true_and, Bool.not_eq_true,
Option.not_isSome, Option.isNone_iff_eq_none, Fin.find_eq_none_iff] at hi
exact False.elim (hi k hj)
| Sum.inr k =>
simp [appendEquiv]
rw [Fin.le_def]
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 only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast,
Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le]
refine h1.2 k (by simpa using hj)
lemma getDual?_append_inl (i : Fin l.length) : (l ++ l2).getDual? (appendEquiv (Sum.inl i)) =
Option.or (Option.map (appendEquiv ∘ Sum.inl) (l.getDual? i))
(Option.map (appendEquiv ∘ Sum.inr) (l.getDualInOther? l2 i)) := by
by_cases h : (l.getDual? i).isSome
· simp_all
rw [congrArg (Option.map (appendEquiv ∘ Sum.inl)) (Option.eq_some_of_isSome h)]
rfl
by_cases ho : (l.getDualInOther? l2 i).isSome
· simp_all
rw [congrArg (Option.map (appendEquiv ∘ Sum.inr)) (Option.eq_some_of_isSome ho)]
rfl
simp_all
@[simp]
lemma getDual?_append_inr_getDualInOther?_isSome (i : Fin l2.length)
(h : (l2.getDualInOther? l i).isSome) :
(l ++ l2).getDual? (appendEquiv (Sum.inr i)) =
some (appendEquiv (Sum.inl ((l2.getDualInOther? l i).get h))) := by
rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inr_inl]
apply And.intro (getDualInOther?_areDualInOther_get l2 l i h)
intro j hj
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, ge_iff_le]
rw [Fin.le_def]
have h1 : l2.getDualInOther? l i = some (((l2.getDualInOther? l i).get h)) :=
Option.eq_some_of_isSome h
nth_rewrite 1 [getDualInOther?] at h1
rw [Fin.find_eq_some_iff] at h1
simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le]
refine h1.2 k (by simpa using hj)
| Sum.inr k =>
simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le]
rw [Fin.le_def]
simp only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast,
Fin.coe_castAdd, Fin.coe_natAdd]
omega
@[simp]
lemma getDual?_inr_getDualInOther?_isNone_getDual?_isSome (i : Fin l2.length)
(h : (l2.getDualInOther? l i).isNone) (hi : (l2.getDual? i).isSome) :
(l ++ l2).getDual? (appendEquiv (Sum.inr i)) = some
(appendEquiv (Sum.inr ((l2.getDual? i).get hi))) := by
rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inr_inr]
apply And.intro (getDual?_areDualInSelf_get l2 i hi)
intro j hj
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
simp at hj
simp only [getDualInOther?, Option.isNone_iff_eq_none, Fin.find_eq_none_iff] at h
exact False.elim (h k hj)
| Sum.inr k =>
simp [appendEquiv, IndexList.length]
rw [Fin.le_def]
simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le]
have h2 : l2.getDual? i = some ((l2.getDual? i).get hi) := Option.eq_some_of_isSome hi
nth_rewrite 1 [getDual?] at h2
rw [Fin.find_eq_some_iff] at h2
simp only [AreDualInSelf.append_inr_inr] at hj
exact h2.2 k hj
lemma getDual?_append_inr (i : Fin l2.length) :
(l ++ l2).getDual? (appendEquiv (Sum.inr i)) =
Option.or (Option.map (appendEquiv ∘ Sum.inl) (l2.getDualInOther? l i))
(Option.map (appendEquiv ∘ Sum.inr) (l2.getDual? i)) := by
by_cases h : (l2.getDualInOther? l i).isSome
· simp_all
rw [congrArg (Option.map (appendEquiv ∘ Sum.inl)) (Option.eq_some_of_isSome h)]
rfl
by_cases ho : (l2.getDual? i).isSome
· simp_all
rw [congrArg (Option.map (appendEquiv ∘ Sum.inr)) (Option.eq_some_of_isSome ho)]
rfl
simp_all
/-!
## Properties of getDualInOther? and append
-/
variable (l3 : IndexList X)
@[simp]
lemma getDualInOther?_append_of_inl (i : Fin l.length) :
(l ++ l2).getDualInOther? l3 (appendEquiv (Sum.inl i)) = l.getDualInOther? l3 i := by
simp [getDualInOther?]
@[simp]
lemma getDualInOther?_append_of_inr (i : Fin l2.length) :
(l ++ l2).getDualInOther? l3 (appendEquiv (Sum.inr i)) = l2.getDualInOther? l3 i := by
simp [getDualInOther?]
@[simp]
lemma getDualInOther?_isSome_of_append_iff (i : Fin l.length) :
(l.getDualInOther? (l2 ++ l3) i).isSome ↔
(l.getDualInOther? l2 i).isSome ∨ (l.getDualInOther? l3 i).isSome := by
rw [getDualInOther?_isSome_iff_exists, getDualInOther?_isSome_iff_exists,
getDualInOther?_isSome_iff_exists]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· obtain ⟨j, hj⟩ := h
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
exact Or.inl ⟨k, by simpa using hj⟩
| Sum.inr k =>
exact Or.inr ⟨k, (AreDualInOther.of_append_inr i k).mp hj⟩
· cases' h with h h <;>
obtain ⟨j, hj⟩ := h
· use appendEquiv (Sum.inl j)
exact (AreDualInOther.of_append_inl i j).mpr hj
· use appendEquiv (Sum.inr j)
exact (AreDualInOther.of_append_inr i j).mpr hj
@[simp]
lemma getDualInOther?_eq_none_of_append_iff (i : Fin l.length) :
(l.getDualInOther? (l2 ++ l3) i) = none ↔
(l.getDualInOther? l2 i) = none ∧ (l.getDualInOther? l3 i) = none := by
apply Iff.intro
· intro h
have h1 := (l.getDualInOther?_isSome_of_append_iff l2 l3 i).mpr.mt
simp only [not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, imp_self] at h1
exact h1 h
· intro h
have h1 := (l.getDualInOther?_isSome_of_append_iff l2 l3 i).mp.mt
simp only [not_or, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, imp_self] at h1
exact h1 h
@[simp]
lemma getDualInOther?_of_append_of_isSome (i : Fin l.length)
(hi : (l.getDualInOther? l2 i).isSome) : l.getDualInOther? (l2 ++ l3) i =
some (appendEquiv (Sum.inl ((l.getDualInOther? l2 i).get hi))) := by
rw [getDualInOther?, Fin.find_eq_some_iff, AreDualInOther.of_append_inl]
apply And.intro (getDualInOther?_areDualInOther_get l l2 i hi)
intro j hj
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, ge_iff_le]
rw [Fin.le_def]
have h1 : l.getDualInOther? l2 i = some (((l.getDualInOther? l2 i).get hi)) :=
Option.eq_some_of_isSome hi
nth_rewrite 1 [getDualInOther?] at h1
rw [Fin.find_eq_some_iff] at h1
simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le, ge_iff_le]
refine h1.2 k ((AreDualInOther.of_append_inl i k).mp hj)
| Sum.inr k =>
simp only [appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left, RelIso.coe_fn_toEquiv,
Fin.castOrderIso_apply, finSumFinEquiv_apply_right, ge_iff_le]
rw [Fin.le_def]
simp only [length, append_val, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast,
Fin.coe_castAdd, Fin.coe_natAdd]
omega
@[simp]
lemma getDualInOther?_of_append_of_isNone_isSome (i : Fin l.length)
(hi : (l.getDualInOther? l2 i) = none) (h2 : (l.getDualInOther? l3 i).isSome) :
l.getDualInOther? (l2 ++ l3) i =
some (appendEquiv (Sum.inr ((l.getDualInOther? l3 i).get h2))) := by
rw [getDualInOther?, Fin.find_eq_some_iff, AreDualInOther.of_append_inr]
apply And.intro (getDualInOther?_areDualInOther_get l l3 i h2)
intro j hj
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
simp at hj
simp only [getDualInOther?, Option.isNone_iff_eq_none, Fin.find_eq_none_iff] at hi
exact False.elim (hi k hj)
| Sum.inr k =>
simp [appendEquiv, IndexList.length]
rw [Fin.le_def]
simp only [Fin.coe_cast, Fin.coe_natAdd, add_le_add_iff_left, Fin.val_fin_le]
have h1 : l.getDualInOther? l3 i = some ((l.getDualInOther? l3 i).get h2) :=
Option.eq_some_of_isSome h2
nth_rewrite 1 [getDualInOther?] at h1
rw [Fin.find_eq_some_iff] at h1
simp only [AreDualInOther.of_append_inr] at hj
exact h1.2 k hj
end IndexList
end IndexNotation

41
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Equivs.lean
View file

@ -151,6 +151,47 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ :=
lemma getDualInOtherEquiv_symm : (l.getDualInOtherEquiv l2).symm = l2.getDualInOtherEquiv l := by
rfl
/-- An equivalence casting `withUniqueDualInOther` based on an equality of the left index list. -/
def withUniqueDualCastLeft (h : l = l3) :
l.withUniqueDualInOther l2 ≃ l3.withUniqueDualInOther l2 where
toFun x := ⟨Fin.cast (by rw [h]) x.1, by subst h; exact x.prop⟩
invFun x := ⟨Fin.cast (by rw [h]) x.1, by subst h; exact x.prop⟩
left_inv x := SetCoe.ext rfl
right_inv x := SetCoe.ext rfl
/-- An equivalence casting `withUniqueDualInOther` based on an equality of the right index list. -/
def withUniqueDualCastRight (h : l2 = l3) :
l.withUniqueDualInOther l2 ≃ l.withUniqueDualInOther l3 where
toFun x := ⟨x.1, by subst h; exact x.prop⟩
invFun x := ⟨x.1, by subst h; exact x.prop⟩
left_inv x := SetCoe.ext rfl
right_inv x := SetCoe.ext rfl
/-- An equivalence casting `withUniqueDualInOther` based on an equality of both index lists. -/
def withUniqueDualCast {l1 l2 l1' l2' : IndexList X} (h : l1 = l1') (h2 : l2 = l2') :
l1.withUniqueDualInOther l2 ≃ l1'.withUniqueDualInOther l2' where
toFun x := ⟨Fin.cast (by rw [h]) x.1, by subst h h2; exact x.prop⟩
invFun x := ⟨Fin.cast (by rw [h]) x.1, by subst h h2; exact x.prop⟩
left_inv x := SetCoe.ext rfl
right_inv x := SetCoe.ext rfl
lemma getDualInOtherEquiv_cast_left (h : l = l3) :
l.getDualInOtherEquiv l2 = ((withUniqueDualCastLeft l l2 l3 h).trans
(l3.getDualInOtherEquiv l2)).trans (withUniqueDualCastRight l2 l l3 h).symm := by
subst h
rfl
lemma getDualInOtherEquiv_cast_right (h : l2 = l3) :
l.getDualInOtherEquiv l2 = ((withUniqueDualCastRight l l2 l3 h).trans
(l.getDualInOtherEquiv l3)).trans (withUniqueDualCastLeft l2 l l3 h).symm := by
subst h
rfl
lemma getDualInOtherEquiv_cast {l1 l2 l1' l2' : IndexList X} (h : l1 = l1') (h2 : l2 = l2') :
l1.getDualInOtherEquiv l2 = ((withUniqueDualCast h h2).trans
(l1'.getDualInOtherEquiv l2')).trans (withUniqueDualCast h2 h).symm := by
subst h h2
rfl
/-!

1
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Subperm.lean
View file

@ -93,7 +93,6 @@ lemma contr_refl : l.contrIndexList.Subperm l.contrIndexList := by
end Subperm
end IndexList
end IndexNotation

4
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean
View file

@ -61,7 +61,7 @@ def toCharList (s : IndexString X) : List Char := s.val.toList
/-- Takes a list of characters to the correpsonding index if it exists else to `none`. -/
def charListToOptionIndex (l : List Char) : Option (Index X) :=
if h : listCharIndex X l && l ≠ [] then
some (Index.ofCharList l (by simpa using h))
some (IndexRep.ofCharList l (by simpa using h)).toIndex
else
none
@ -97,7 +97,7 @@ open IndexNotation ColorIndexList IndexString
noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String)
(hs : listCharIsIndexString 𝓣.toTensorColor.Color s.toList = true)
(hn : n = (toIndexList' s hs).length)
(hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
(hD : IndexList.OnlyUniqueDuals (toIndexList' s hs))
(hC : IndexList.ColorCond (toIndexList' s hs))
(hd : TensorColor.ColorMap.DualMap (toIndexList' s hs).colorMap
(cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex :=

618
HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean
View file

@ -1,618 +0,0 @@
/-
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.Contraction
import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Data.Finset.Sort
/-!
# withDuals equal to withUniqueDuals
In a permissible list of indices every index which has a dual has a unique dual.
This corresponds to the condition that `l.withDual = l.withUniqueDual`.
We prove lemmas relating to this condition.
-/
namespace IndexNotation
namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 l3 : IndexList X)
/-!
## withDual equal to withUniqueDual
-/
lemma withUnqiueDual_eq_withDual_iff_unique_forall :
l.withUniqueDual = l.withDual ↔
∀ (i : l.withDual) j, l.AreDualInSelf i j → j = l.getDual? i := by
refine Iff.intro (fun h i j hj => ?_) (fun h => ?_)
· rw [@Finset.ext_iff] at h
simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and, and_iff_left_iff_imp] at h
refine h i ?_ j hj
exact withDual_isSome l i
· refine Finset.ext (fun i => ?_)
refine Iff.intro (fun hi => mem_withDual_of_mem_withUniqueDual l i hi) (fun hi => ?_)
· simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ,
true_and]
exact And.intro ((mem_withDual_iff_isSome l i).mp hi) (fun j hj => h ⟨i, hi⟩ j hj)
lemma withUnqiueDual_eq_withDual_iff :
l.withUniqueDual = l.withDual ↔
∀ i, (l.getDual? i).bind l.getDual? = Option.guard (fun i => i ∈ l.withDual) i := by
apply Iff.intro
· intro h i
by_cases hi : i ∈ l.withDual
· have hii : i ∈ l.withUniqueDual := by
simp_all only
change (l.getDual? i).bind l.getDual? = _
simp [hii]
symm
rw [Option.guard_eq_some]
exact ⟨rfl, mem_withUniqueDual_isSome l i hii⟩
· simp at hi
simp [Option.guard, hi]
· intro h
rw [withUnqiueDual_eq_withDual_iff_unique_forall]
intro i j hj
rcases l.getDual?_of_areDualInSelf hj with hi | hi | hi
· have hj' := h j
rw [hi] at hj'
simp at hj'
rw [hj']
symm
rw [Option.guard_eq_some, hi]
exact ⟨rfl, rfl⟩
· exact hi.symm
· have hj' := h j
rw [hi] at hj'
rw [h i] at hj'
have hi : Option.guard (fun i => i ∈ l.withDual) ↑i = some i := by
apply Option.guard_eq_some.mpr
simp
rw [hi] at hj'
simp at hj'
have hj'' := Option.guard_eq_some.mp hj'.symm
have hj''' := hj''.1
rw [hj'''] at hj
simp at hj
lemma withUnqiueDual_eq_withDual_iff_list_apply :
l.withUniqueDual = l.withDual ↔
(Fin.list l.length).map (fun i => (l.getDual? i).bind l.getDual?) =
(Fin.list l.length).map (fun i => Option.guard (fun i => i ∈ l.withDual) i) := by
rw [withUnqiueDual_eq_withDual_iff]
refine Iff.intro (fun h => List.map_eq_map_iff.mpr fun a _ => h a) (fun h i => ?_)
simp only [List.map_inj_left] at h
have h1 {n : ℕ} (m : Fin n) : m ∈ Fin.list n := by
have h1' : (Fin.list n)[m] = m := Fin.getElem_list _ _
exact h1' ▸ List.getElem_mem _ _ _
exact h i (h1 i)
/-- A boolean which is true for an index list `l` if for every index in `l` with a dual,
that dual is unique. -/
def withUnqiueDualEqWithDualBool : Bool :=
if (Fin.list l.length).map (fun i => (l.getDual? i).bind l.getDual?) =
(Fin.list l.length).map (fun i => Option.guard (fun i => i ∈ l.withDual) i) then
true
else
false
lemma withUnqiueDual_eq_withDual_iff_list_apply_bool :
l.withUniqueDual = l.withDual ↔ l.withUnqiueDualEqWithDualBool := by
rw [withUnqiueDual_eq_withDual_iff_list_apply]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· simp only [withUnqiueDualEqWithDualBool, h, mem_withDual_iff_isSome, ↓reduceIte]
· simpa only [mem_withDual_iff_isSome, List.map_inj_left, withUnqiueDualEqWithDualBool,
Bool.if_false_right, Bool.and_true, decide_eq_true_eq] using h
@[simp]
lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) :
l.withUniqueDual = l.withDual := by
rw [h, Finset.eq_empty_iff_forall_not_mem]
intro x
by_contra hx
have x' : l.withDual := ⟨x, l.mem_withDual_of_withUniqueDual ⟨x, hx⟩⟩
have hx' := x'.2
simp [h] at hx'
lemma withUniqueDual_eq_withDual_iff_sort_eq :
l.withUniqueDual = l.withDual ↔
l.withUniqueDual.sort (fun i j => i ≤ j) = l.withDual.sort (fun i j => i ≤ j) := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rw [h]
· have h1 := congrArg Multiset.ofList h
rw [Finset.sort_eq, Finset.sort_eq] at h1
exact Eq.symm ((fun {α} {s t} => Finset.val_inj.mp) (id (Eq.symm h1)))
/-!
# withUniqueDual equal to withDual and count conditions.
-/
lemma withUniqueDual_eq_withDual_iff_countId_leq_two :
l.withUniqueDual = l.withDual ↔ ∀ i, l.countId (l.val.get i) ≤ 2 := by
refine Iff.intro (fun h i => ?_) (fun h => ?_)
· by_cases hi : i ∈ l.withDual
· rw [← h] at hi
rw [mem_withUniqueDual_iff_countId_eq_two] at hi
rw [hi]
· rw [mem_withDual_iff_countId_gt_one] at hi
simp at hi
exact Nat.le_succ_of_le hi
· refine Finset.ext (fun i => ?_)
rw [mem_withUniqueDual_iff_countId_eq_two, mem_withDual_iff_countId_gt_one]
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
by_cases h0 : l.countId (l.val.get i)= 0
· exact Or.inl h0
· by_cases h1 : l.countId (l.val.get i) = 1
· exact Or.inr (Or.inl h1)
· have h2 : l.countId (l.val.get i) ≤ 2 := by
rw [withUniqueDual_eq_withDual_iff_countId_leq_two] at h
exact h i
omega
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
exact h1
lemma filter_id_of_countId_eq_zero' {I : Index X} (h1 : l.countId I = 0) :
l.val.filter (fun J => I.id = J.id) = [] := by
rw [countId_eq_length_filter, List.length_eq_zero] at h1
exact h1
lemma filter_id_of_countId_eq_one {i : Fin l.length} (h1 : l.countId (l.val.get i) = 1) :
l.val.filter (fun J => (l.val.get i).id = J.id) = [l.val.get i] := by
rw [countId_eq_length_filter, List.length_eq_one] at h1
obtain ⟨J, hJ⟩ := h1
have hme : (l.val.get i) ∈ List.filter (fun J => decide ((l.val.get i).id = J.id)) l.val := by
simp only [List.get_eq_getElem, List.mem_filter, decide_True, and_true]
exact List.getElem_mem l.val (↑i) i.isLt
rw [hJ] at hme
simp only [List.get_eq_getElem, List.mem_singleton] at hme
erw [hJ]
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) =
[l.val.get i, l.val.get ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))] ∨
l.val.filter (fun J => (l.val.get i).id = J.id) =
[l.val.get ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h)), l.val.get i] := by
have hc := l.countId_eq_two_of_mem_withUniqueDual i
((mem_withUniqueDual_iff_countId_eq_two l i).mpr h)
rw [countId_eq_length_filter] at hc
by_cases hi : i < ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))
· apply Or.inl
symm
apply List.Sublist.eq_of_length
· have h1 : [l.val.get i, l.val.get
((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))].filter
(fun J => (l.val.get i).id = J.id) = [l.val.get i, l.val.get
((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))] := by
simp only [List.get_eq_getElem, decide_True, List.filter_cons_of_pos, List.cons.injEq,
List.filter_eq_self, List.mem_singleton, decide_eq_true_eq, forall_eq, true_and]
change l.idMap i = l.idMap ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))
simp
rw [← h1]
refine List.Sublist.filter (fun (J : Index X) => ((l.val.get i).id = J.id)) ?_
rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq]
refine ⟨⟨⟨![i, (l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h)], ?_⟩, ?_⟩, ?_⟩
· refine List.nodup_ofFn.mp ?_
simpa using Fin.ne_of_lt hi
· intro a b
fin_cases a, b
<;> simp [hi]
exact Fin.le_of_lt hi
· intro a
fin_cases a <;> rfl
· rw [hc]
simp
· have hi' : ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h)) < i := by
have h1 := l.getDual?_get_areDualInSelf i (getDual?_isSome_of_countId_eq_two l h)
simp only [AreDualInSelf] at h1
have h2 := h1.1
omega
apply Or.inr
symm
apply List.Sublist.eq_of_length
· have h1 : [l.val.get ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h)),
l.val.get i].filter (fun J => (l.val.get i).id = J.id) = [l.val.get
((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h)), l.val.get i,] := by
simp only [List.get_eq_getElem, List.filter_eq_self, List.mem_cons, List.mem_singleton,
decide_eq_true_eq, forall_eq_or_imp, forall_eq, and_true]
apply And.intro
· change l.idMap i = l.idMap ((l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h))
simp
· simp only [List.not_mem_nil, false_implies, implies_true, and_self]
rw [← h1]
refine List.Sublist.filter (fun (J : Index X) => ((l.val.get i).id = J.id)) ?_
rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq]
refine ⟨⟨⟨![(l.getDual? i).get (l.getDual?_isSome_of_countId_eq_two h), i], ?_⟩, ?_⟩, ?_⟩
· refine List.nodup_ofFn.mp ?_
simp only [List.get_eq_getElem, List.length_singleton, Nat.succ_eq_add_one, Nat.reduceAdd,
List.length_nil, List.ofFn_succ, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_succ,
Matrix.cons_val_fin_one, List.ofFn_zero, List.nodup_cons, List.mem_singleton,
List.not_mem_nil, not_false_eq_true, List.nodup_nil, and_self, and_true]
exact Fin.ne_of_lt hi'
· intro a b
fin_cases a, b
<;> simp [hi']
exact Fin.le_of_lt hi'
· intro a
fin_cases a <;> rfl
· rw [hc]
simp
/-- Given an index `I` such that there is one index in `l` with the same `id` as `I`.
This is that index. -/
def consDual {I : Index X} (hI : l.countId I = 1) : Index X :=
(l.cons I).val.get (((l.cons I).getDual? ⟨0, by simp⟩).get
((l.cons I).getDual?_isSome_of_countId_eq_two (by simpa [countId] using hI)))
/-! TODO: Relate `consDual` to `getDualInOther?`. -/
@[simp]
lemma consDual_id {I : Index X} (hI : l.countId I = 1) :
(l.consDual hI).id = I.id := by
change (l.cons I).idMap ((((l.cons I).getDual? ⟨0, by simp⟩).get
((l.cons I).getDual?_isSome_of_countId_eq_two (by simpa [countId] using hI)))) = _
simp only [cons, Fin.zero_eta, getDual?_get_id]
simp only [idMap, List.get_eq_getElem, List.length_cons, Fin.val_zero, List.getElem_cons_zero]
@[simp]
lemma consDual_mem {I : Index X} (hI : l.countId I = 1) :
l.consDual hI ∈ l.val := by
let Di := (((l.cons I).getDual? ⟨0, by simp⟩).get (by
rw [← zero_mem_withUniqueDual_of_cons_iff_countId_one] at hI; exact
mem_withUniqueDual_isSome (l.cons I) ⟨0, _⟩ hI))
have hDiz : Di ≠ ⟨0, by simp⟩ := by
have hd : (l.cons I).AreDualInSelf ⟨0, by simp⟩ Di := by
simp [Di]
symm
exact (l.cons I).getDual?_get_areDualInSelf ⟨0, by simp⟩ (by
rw [← zero_mem_withUniqueDual_of_cons_iff_countId_one] at hI;
exact mem_withUniqueDual_isSome (l.cons I) ⟨0, _⟩ hI)
simp [AreDualInSelf] at hd
have hd2 := hd.1
exact fun a => hd2 (id (Eq.symm a))
have Dim1 : (Di.1-1) + 1 = Di.1 := by
have : Di.1 ≠ 0 := by
rw [Fin.ne_iff_vne] at hDiz
exact hDiz
omega
change (l.cons I).val.get Di ∈ l.val
simp only [cons_val, List.get_eq_getElem, List.length_cons]
have h1 : (I :: l.val).get ⟨Di.1, Di.isLt⟩ = (I :: l.val).get
⟨(Di.1-1) + 1, by rw [Dim1]; exact Di.isLt⟩ := by
apply congrArg
rw [Fin.ext_iff]
exact id (Eq.symm Dim1)
simp only [List.length_cons, cons_length, Fin.eta, List.get_eq_getElem,
List.getElem_cons_succ] at h1
rw [h1]
exact List.getElem_mem l.val _ _
lemma consDual_filter {I : Index X} (hI : l.countId I = 1) :
l.val.filter (fun J => I.id = J.id) = [l.consDual hI] := by
have h1 : (l.val.filter (fun J => I.id = J.id)).length = 1 := by
rw [← List.countP_eq_length_filter]
exact hI
rw [List.length_eq_one] at h1
obtain ⟨a, ha⟩ := h1
rw [ha]
simp only [List.cons.injEq, and_true]
have haI : l.consDual hI ∈ l.val.filter (fun J => I.id = J.id) := by
simp
rw [ha] at haI
simp at haI
exact haI.symm
lemma consDual_iff {I : Index X} (hI : l.countId I = 1)
(I' : Index X) : I' = l.consDual hI ↔ I' ∈ l.val ∧ I'.id = I.id := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· subst h
simp only [consDual_mem, consDual_id, and_self]
· have hI' : I' ∈ l.val.filter (fun J => I.id = J.id) := by
simp only [List.mem_filter, h, decide_True, and_self]
rw [l.consDual_filter hI] at hI'
simpa using hI'
lemma filter_of_constDual {I : Index X} (hI : l.countId I = 1) :
(l.cons I).val.filter (fun J => (l.consDual hI).id = J.id) = [I, l.consDual hI] := by
simp only [consDual_id, cons_val, decide_True, List.filter_cons_of_pos, List.cons.injEq, true_and]
exact consDual_filter l hI
end filterID
lemma withUniqueDual_eq_withDual_iff_countId_mem_le_two :
l.withUniqueDual = l.withDual ↔
∀ I (_ : I ∈ l.val), l.countId I ≤ 2 := by
rw [withUniqueDual_eq_withDual_iff_countId_leq_two]
refine Iff.intro (fun h I hI => ?_) (fun h i => ?_)
· let i := l.val.indexOf I
have hi : i < l.length := List.indexOf_lt_length.mpr hI
have hIi : I = l.val.get ⟨i, hi⟩ := (List.indexOf_get hi).symm
rw [hIi]
exact h ⟨i, hi⟩
· exact h (l.val.get i) (List.getElem_mem l.val (↑i) i.isLt)
lemma withUniqueDual_eq_withDual_iff_all_countId_le_two :
l.withUniqueDual = l.withDual ↔
l.val.all (fun I => l.countId I ≤ 2) := by
rw [withUniqueDual_eq_withDual_iff_countId_mem_le_two]
simp only [List.all_eq_true, decide_eq_true_eq]
/-!
## Relationship with cons
-/
lemma withUniqueDual_eq_withDual_cons_iff (I : Index X) (hl : l.withUniqueDual = l.withDual) :
(l.cons I).withUniqueDual = (l.cons I).withDual ↔ l.countId I ≤ 1 := by
rw [withUniqueDual_eq_withDual_iff_all_countId_le_two]
simp only [cons_val, countId, List.all_cons, decide_True, List.countP_cons_of_pos,
Nat.reduceLeDiff, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, and_iff_left_iff_imp]
intro h I' hI'
by_cases hII' : I'.id = I.id
· rw [List.countP_cons_of_pos]
· rw [hII']
omega
· simpa using hII'
· rw [List.countP_cons_of_neg]
· rw [withUniqueDual_eq_withDual_iff_countId_mem_le_two] at hl
exact hl I' hI'
· simpa using hII'
lemma withUniqueDual_eq_withDual_of_cons {I : Index X}
(hl : (l.cons I).withUniqueDual = (l.cons I).withDual) :
l.withUniqueDual = l.withDual := by
rw [withUniqueDual_eq_withDual_iff_countId_mem_le_two] at hl ⊢
intro I' hI'
have hImem : I' ∈ (l.cons I).val := by
simp [hI']
have h1 : List.countP (fun J => decide (I'.id = J.id)) l.val ≤
List.countP (fun J => decide (I'.id = J.id)) (I :: l.val) := by
by_cases hII' : I'.id = I.id
· rw [List.countP_cons_of_pos _ l.val]
· simp
· simpa using hII'
· rw [List.countP_cons_of_neg _ l.val]
simpa using hII'
exact Nat.le_trans h1 (hl I' hImem)
lemma withUniqueDual_eq_withDual_cons_iff' (I : Index X) :
(l.cons I).withUniqueDual = (l.cons I).withDual ↔
l.withUniqueDual = l.withDual ∧ l.countId I ≤ 1 := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· have h1 : l.withUniqueDual = l.withDual := by
exact withUniqueDual_eq_withDual_of_cons l h
apply And.intro h1 ((withUniqueDual_eq_withDual_cons_iff l I h1).mp h)
· rw [withUniqueDual_eq_withDual_cons_iff]
· exact h.2
· exact h.1
/-!
## withUniqueDualInOther equal to withDualInOther append conditions
-/
lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm'
(h : (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3) :
(l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by
rw [Finset.ext_iff] at h ⊢
intro j
obtain ⟨k, hk⟩ := appendEquiv.surjective j
subst hk
match k with
| Sum.inl k =>
rw [mem_append_withUniqueDualInOther_symm]
simpa only [mem_withInDualOther_iff_isSome, getDualInOther?_append_of_inl,
getDualInOther?_append_of_inr] using h (appendEquiv (Sum.inr k))
| Sum.inr k =>
rw [← mem_append_withUniqueDualInOther_symm]
simpa only [mem_withInDualOther_iff_isSome, getDualInOther?_append_of_inr,
getDualInOther?_append_of_inl] using h (appendEquiv (Sum.inl k))
lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm :
(l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3 ↔
(l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 :=
Iff.intro
(l.withUniqueDualInOther_eq_withDualInOther_append_of_symm' l2 l3)
(l2.withUniqueDualInOther_eq_withDualInOther_append_of_symm' l l3)
lemma withUniqueDualInOther_eq_withDualInOther_of_append_symm'
(h : l.withUniqueDualInOther (l2 ++ l3) = l.withDualInOther (l2 ++ l3)) :
l.withUniqueDualInOther (l3 ++ l2) = l.withDualInOther (l3 ++ l2) := by
rw [Finset.ext_iff] at h ⊢
intro j
rw [mem_withUniqueDualInOther_symm]
rw [h j]
simp only [mem_withInDualOther_iff_isSome, getDualInOther?_isSome_of_append_iff]
exact Or.comm
lemma withUniqueDualInOther_eq_withDualInOther_of_append_symm :
l.withUniqueDualInOther (l2 ++ l3) = l.withDualInOther (l2 ++ l3) ↔
l.withUniqueDualInOther (l3 ++ l2) = l.withDualInOther (l3 ++ l2) :=
Iff.intro
(l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l2 l3)
(l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l3 l2)
/-!
## withDual equal to withUniqueDual append conditions
-/
lemma append_withDual_eq_withUniqueDual_iff :
(l ++ l2).withUniqueDual = (l ++ l2).withDual ↔
((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2)
= l.withDual ∪ l.withDualInOther l2
∧ (l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l
= l2.withDual ∪ l2.withDualInOther l := by
rw [append_withUniqueDual_disjSum, withDual_append_eq_disjSum]
simp only [Equiv.finsetCongr_apply, Finset.map_inj]
have h (s s' : Finset (Fin l.length)) (t t' : Finset (Fin l2.length)) :
s.disjSum t = s'.disjSum t' ↔ s = s' ∧ t = t' := by
simp [Finset.ext_iff]
exact h _ _ _ _
lemma append_withDual_eq_withUniqueDual_symm :
(l ++ l2).withUniqueDual = (l ++ l2).withDual ↔
(l2 ++ l).withUniqueDual = (l2 ++ l).withDual := by
rw [append_withDual_eq_withUniqueDual_iff, append_withDual_eq_withUniqueDual_iff]
exact And.comm
@[simp]
lemma append_withDual_eq_withUniqueDual_inl (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
l.withUniqueDual = l.withDual := by
rw [Finset.ext_iff]
intro i
refine Iff.intro (fun h' => ?_) (fun h' => ?_)
· exact mem_withDual_of_mem_withUniqueDual l i h'
· have hn : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by
rw [h]
simp_all
refine l.mem_withUniqueDual_of_inl l2 i hn ?_
exact (mem_withDual_iff_isSome l i).mp h'
@[simp]
lemma append_withDual_eq_withUniqueDual_inr (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
l2.withUniqueDual = l2.withDual := by
rw [append_withDual_eq_withUniqueDual_symm] at h
exact append_withDual_eq_withUniqueDual_inl l2 l h
@[simp]
lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl
(h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
l.withUniqueDualInOther l2 = l.withDualInOther l2 := by
rw [Finset.ext_iff]
intro i
refine Iff.intro (fun h' => ?_) (fun h' => ?_)
· simp only [mem_withInDualOther_iff_isSome, h', mem_withUniqueDualInOther_isSome]
· have hn : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual := by
rw [h]
simp_all only [mem_withInDualOther_iff_isSome, mem_withDual_iff_isSome,
getDual?_isSome_append_inl_iff, or_true, mem_withUniqueDual_isSome]
refine l.mem_withUniqueDualInOther_of_inl_withDualInOther l2 i hn ?_
exact (mem_withInDualOther_iff_isSome l l2 i).mp h'
@[simp]
lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr
(h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
l2.withUniqueDualInOther l = l2.withDualInOther l := by
rw [append_withDual_eq_withUniqueDual_symm] at h
exact append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l2 l h
lemma append_withDual_eq_withUniqueDual_iff' :
(l ++ l2).withUniqueDual = (l ++ l2).withDual ↔
l.withUniqueDual = l.withDual ∧ l2.withUniqueDual = l2.withDual
∧ l.withUniqueDualInOther l2 = l.withDualInOther l2 ∧
l2.withUniqueDualInOther l = l2.withDualInOther l := by
apply Iff.intro
· intro h
exact ⟨append_withDual_eq_withUniqueDual_inl l l2 h,
append_withDual_eq_withUniqueDual_inr l l2 h,
append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l l2 h,
append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr l l2 h⟩
· intro h
rw [append_withDual_eq_withUniqueDual_iff]
rw [h.1, h.2.1, h.2.2.1, h.2.2.2]
have h1 : l.withDual ∩ (l.withDualInOther l2)ᶜ = l.withDual := by
rw [Finset.inter_eq_left, Finset.subset_iff, ← h.1, ← h.2.2.1]
intro i hi
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true,
Option.not_isSome, Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome,
Finset.compl_filter, not_and, not_forall, Finset.mem_filter, Finset.mem_univ, true_and]
intro hn
simp_all
have h2 : l2.withDual ∩ (l2.withDualInOther l)ᶜ = l2.withDual := by
rw [Finset.inter_eq_left, Finset.subset_iff, ← h.2.1, ← h.2.2.2]
intro i hi
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true,
Option.not_isSome, Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome,
Finset.compl_filter, not_and, not_forall, Finset.mem_filter, Finset.mem_univ, true_and]
intro hn
simp_all
exact ⟨congrFun (congrArg Union.union h1) (l.withDualInOther l2),
congrFun (congrArg Union.union h2) (l2.withDualInOther l)⟩
lemma append_withDual_eq_withUniqueDual_swap :
(l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual
↔ (l2 ++ l ++ l3).withUniqueDual = (l2 ++ l ++ l3).withDual := by
rw [append_withDual_eq_withUniqueDual_iff']
rw [append_withDual_eq_withUniqueDual_iff' (l2 ++ l) l3]
rw [append_withDual_eq_withUniqueDual_symm]
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

6
HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
View file

@ -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.Color
import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexList.Color
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Relations
import HepLean.SpaceTime.LorentzTensor.IndexNotation.ColorIndexList.Append
import HepLean.SpaceTime.LorentzTensor.Basic
@ -153,7 +153,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
intro x hx
have hx' : x ∈ i.withUniqueDual := by
exact Finset.mem_of_mem_filter x hx
rw [i.unique_duals] at h
rw [← i.unique_duals] at h
rw [h] at hx'
simp_all only [Finset.not_mem_empty]
erw [TensorStructure.contr_tprod_isEmpty]
@ -238,7 +238,7 @@ lemma trans {T₁ T₂ T₃ : 𝓣.TensorIndex} (h1 : Rel T₁ T₂) (h2 : Rel T
simp only [contrPermEquiv_trans, contrPermEquiv_symm]
/-- Rel forms an equivalence relation. -/
lemma isEquivalence : Equivalence (@Rel _ _ 𝓣 _) where
lemma isEquivalence : Equivalence (@Rel _ _ 𝓣 _ _) where
refl := Rel.refl
symm := Rel.symm
trans := Rel.trans

229
HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean
View file

@ -1,229 +0,0 @@
/-
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.GetDual
import Mathlib.Algebra.Order.Ring.Nat
import Mathlib.Tactic.FinCases
/-!
# Indices with duals.
In this file we define the following finite sets:
- Given an index list `l₁`, the finite set, `l₁.withDual`, of (positions in) `l₁`
corresponding to those indices which have a dual in `l₁`. This is equivalent to those indices
of `l₁` for which `getDual?` is `some`.
- Given two index lists `l₁` and `l₂`, the finite set, `l₁.withDualInOther l₂` of (positions in)
`l₁` corresponding to those indices which have a dual in `l₂`. This is equivalent to those indices
of `l₁` for which `l₁.getDualInOther? l₂` is `some`.
For example for `l₁ := ['ᵘ¹', 'ᵘ²', 'ᵤ₁', 'ᵘ¹']` and `l₂ := ['ᵘ³', 'ᵘ²', 'ᵘ⁴', 'ᵤ₂']` we have
`l₁.withDual = {0, 2, 3}` and `l₁.withDualInOther l₂ = {1}`.
We prove some properties of these finite sets. In particular, we prove properties
related to how they interact with appending two index lists.
-/
namespace IndexNotation
namespace IndexList
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
variable (l l2 l3 : IndexList X)
/-!
## Finsets on which getDual? and getDualInOther? are some.
-/
/-- 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 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
/-!
## Basic properties of withDual
-/
@[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]
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
/-!
## Relationship between membership of withDual and countP on id.
-/
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]
rw [mem_withDual_iff_exists] at h
obtain ⟨j, hj⟩ := h
simp [AreDualInSelf, idMap] at hj
by_contra hn
have hn' := l.countId_index_neq_zero i
have hl : 2 ≤ l.val.countP (fun J => (l.val.get i).id = J.id) := by
by_cases hij : i < j
· have hsub : List.Sublist [l.val.get i, l.val.get j] l.val := by
rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq]
refine ⟨⟨⟨![i, j], ?_⟩, ?_⟩, ?_⟩
· refine List.nodup_ofFn.mp ?_
simpa using Fin.ne_of_lt hij
· intro a b
fin_cases a, b
<;> simp [hij]
exact Fin.le_of_lt hij
· intro a
fin_cases a <;> rfl
simpa [hj.2] using List.Sublist.countP_le
(fun (j : Index X) => decide (l.val[i].id = j.id)) hsub
· have hij' : j < i := by omega
have hsub : List.Sublist [l.val.get j, l.val.get i] l.val := by
rw [List.sublist_iff_exists_fin_orderEmbedding_get_eq]
refine ⟨⟨⟨![j, i], ?_⟩, ?_⟩, ?_⟩
· refine List.nodup_ofFn.mp ?_
simpa using Fin.ne_of_lt hij'
· intro a b
fin_cases a, b
<;> simp [hij']
exact Fin.le_of_lt hij'
· intro a
fin_cases a <;> rfl
simpa [hj.2] using List.Sublist.countP_le
(fun (j : Index X) => decide (l.val[i].id = j.id)) hsub
omega
lemma countId_of_not_mem_withDual (i : Fin l.length)(h : i ∉ l.withDual) :
l.countId (l.val.get i) = 1 := by
rw [countId]
rw [mem_withDual_iff_exists] at h
simp [AreDualInSelf] at h
have h1 : ¬ l.val.Duplicate (l.val.get i) := by
by_contra hn
rw [List.duplicate_iff_exists_distinct_get] at hn
obtain ⟨k, j, h1, h2, h3⟩ := hn
by_cases hi : k = i
<;> by_cases hj : j = i
· subst hi hj
simp at h1
· subst hi
exact h j (fun a => hj (id (Eq.symm a))) (congrArg Index.id h3)
· subst hj
exact h k (fun a => hi (id (Eq.symm a))) (congrArg Index.id h2)
· exact h j (fun a => hj (id (Eq.symm a))) (congrArg Index.id h3)
rw [List.duplicate_iff_two_le_count] at h1
simp at h1
by_cases hx : List.count l.val[i] l.val = 0
· rw [List.count_eq_zero] at hx
refine False.elim (h i (fun _ => hx ?_) rfl)
exact List.getElem_mem l.val (↑i) (Fin.val_lt_of_le i (le_refl l.length))
· have hln : List.count l.val[i] l.val = 1 := by
rw [Nat.lt_succ, Nat.le_one_iff_eq_zero_or_eq_one] at h1
simp at hx
simpa [hx] using h1
rw [← hln, List.count]
refine (List.countP_congr (fun xt hxt => ?_))
let xid := l.val.indexOf xt
have h2 := List.indexOf_lt_length.mpr hxt
simp only [decide_eq_true_eq, Fin.getElem_fin, beq_iff_eq]
by_cases hxtx : ⟨xid, h2⟩ = i
· rw [(List.indexOf_get h2).symm, hxtx]
simp only [List.get_eq_getElem]
· refine Iff.intro (fun h' => False.elim (h i (fun _ => ?_) rfl)) (fun h' => ?_)
· exact h ⟨xid, h2⟩ (fun a => hxtx (id (Eq.symm a))) (by
rw [(List.indexOf_get h2).symm] at h'; exact h')
· rw [h']
rfl
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
/-!
## Basic properties of withDualInOther
-/
@[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]
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
/-!
## Append properties of withDual
-/
lemma withDual_append_eq_disjSum : (l ++ l2).withDual =
Equiv.finsetCongr appendEquiv
((l.withDual ∪ l.withDualInOther l2).disjSum
(l2.withDual ∪ l2.withDualInOther l)) := by
ext i
obtain ⟨k, hk⟩ := appendEquiv.surjective i
subst hk
match k with
| Sum.inl k =>
simp
| Sum.inr k =>
simp
/-!
## Append properties of withDualInOther
-/
lemma append_withDualInOther_eq :
(l ++ l2).withDualInOther l3 =
Equiv.finsetCongr appendEquiv ((l.withDualInOther l3).disjSum (l2.withDualInOther l3)) := by
rw [Finset.ext_iff]
intro i
obtain ⟨k, hk⟩ := appendEquiv.surjective i
subst hk
match k with
| Sum.inl k =>
simp
| Sum.inr k =>
simp
lemma withDualInOther_append_eq : l.withDualInOther (l2 ++ l3) =
l.withDualInOther l2 ∪ l.withDualInOther l3 := by
ext i
simp
end IndexList
end IndexNotation

1019
HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean
View file

File diff suppressed because it is too large Load diff

4
HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
View file

@ -78,7 +78,7 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
(T : (realLorentzTensor d).Tensor cn) (s : String)
(hs : listCharIsIndexString realTensorColor.Color s.toList = true)
(hn : n = (toIndexList' s hs).length)
(hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
(hD : (toIndexList' s hs).OnlyUniqueDuals)
(hC : IndexList.ColorCond.bool (toIndexList' s hs))
(hd : TensorColor.ColorMap.DualMap.boolFin
(toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) :
@ -103,7 +103,7 @@ macro "prodTactic" : tactic =>
`(tactic| {
apply (ColorIndexList.AppendCond.iff_bool _ _).mpr
change @ColorIndexList.AppendCond.bool realTensorColor
instIndexNotationColorRealTensorColor instDecidableEqColorRealTensorColor _ _
instDecidableEqColorRealTensorColor _ _
simp only [prod_toIndexList, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
toTensorColor_eq, decidableEq_eq_color]
rfl})