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

feat: Improved todo list

Browse source
This commit is contained in:
jstoobysmith 2025-01-22 10:32:39 +00:00
parent 1b2cc5338f
commit ca044d3786
37 changed files with 180 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/Lorentz/Algebra/Basis.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Algebra.Basic
import HepLean.Meta.TODO.Basic
/-!
# Basis of the Lorentz Algebra
@ -15,4 +16,4 @@ This file is waiting for Lorentz Tensors to be done formally, before
it can be completed.
-/
/-! TODO: Define the standard basis of the Lorentz algebra. -/
TODO "Define the standard basis of the Lorentz algebra."

3
HepLean/Lorentz/ComplexTensor/Basis.lean
View file

@ -8,6 +8,7 @@ import HepLean.Tensors.Tree.NodeIdentities.PermContr
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
import HepLean.Meta.TODO.Basic
/-!
## Basis vectors associated with complex Lorentz tensors
@ -47,7 +48,7 @@ lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
simp only [Functor.const_obj_obj, OverColor.mk_hom] at h1
rw [h1]
/-! TODO: Generalize `basis_eq_FD`. -/
TODO "Generalize `basis_eq_FD`."
lemma basis_eq_FD {n : ℕ} (c : Fin n → complexLorentzTensor.C)
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) (i : Fin n)
(h : { as := c i } = { as := c1 }) :

2
HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean
View file

@ -388,7 +388,7 @@ lemma pauliMatrix_contr_lower_3_1_1 :
· congr 2
decide
/-! TODO: Work out why `pauliCo_prod_basis_expand'` is needed. -/
TODO "Work out why `pauliCo_prod_basis_expand'` is needed."
/-- This lemma is exactly the same as `pauliCo_prod_basis_expand`.
It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why
`pauliMatrix_lower_basis_expand_prod` does not work. -/

5
HepLean/Lorentz/ComplexVector/Basic.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.ComplexVector.Modules
import HepLean.Meta.TODO.Basic
/-!
# Complex Lorentz vectors
@ -128,7 +129,7 @@ lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
rw [LorentzGroup.toComplex_mulVec_ofReal]
rfl
/-! TODO: Rename. -/
TODO "Rename."
lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
(complexContr.ρ M) (complexContrBasis i) =
∑ j, (SL2C.toLorentzGroup M).1 j i •
@ -140,6 +141,6 @@ lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]
rw [complexContrBasis_of_real]
/-! TODO: Include relation to real Lorentz vectors. -/
TODO "Include relation to real Lorentz vectors."
end Lorentz
end

3
HepLean/Lorentz/Group/Basic.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.MinkowskiMatrix
import HepLean.Meta.TODO.Basic
/-!
# The Lorentz Group
@ -14,7 +15,7 @@ We define the Lorentz group.
- http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
-/
/-! TODO: Show that the Lorentz is a Lie group. -/
TODO "Show that the Lorentz group is a Lie group."
noncomputable section

2
HepLean/Lorentz/Group/Boosts.lean
View file

@ -21,7 +21,7 @@ A boost is the special case of a generalised boost when `u = stdBasis 0`.
https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
-/
/-! TODO: Show that generalised boosts are in the restricted Lorentz group. -/
TODO "Show that generalised boosts are in the restricted Lorentz group."
noncomputable section
namespace LorentzGroup

2
HepLean/Lorentz/Group/Orthochronous.lean
View file

@ -12,7 +12,7 @@ We define the give a series of lemmas related to the orthochronous property of l
matrices.
-/
/-! TODO: Prove topological properties of the Orthochronous Lorentz Group. -/
TODO "Prove topological properties of the Orthochronous Lorentz Group."
noncomputable section

6
HepLean/Lorentz/Group/Restricted.lean
View file

@ -10,9 +10,9 @@ import HepLean.Lorentz.Group.Orthochronous
This file is currently a stub.
-/
/-! TODO: Add definition of the restricted Lorentz group. -/
/-! TODO: Prove member of the restricted Lorentz group is combo of boost and rotation. -/
/-! TODO: Prove restricted Lorentz group equivalent to connected component of identity. -/
TODO "Add definition of the restricted Lorentz group."
TODO "Prove member of the restricted Lorentz group is combo of boost and rotation."
TODO "Prove restricted Lorentz group equivalent to connected component of identity."
noncomputable section

2
HepLean/Lorentz/Group/Rotations.lean
View file

@ -11,7 +11,7 @@ import HepLean.Mathematics.SO3.Basic
This file describes the embedding of `SO(3)` into `LorentzGroup 3`.
-/
/-! TODO: Generalize the inclusion of rotations into LorentzGroup to abitary dimension. -/
TODO "Generalize the inclusion of rotations into LorentzGroup to abitary dimension."
noncomputable section
namespace LorentzGroup

2
HepLean/Lorentz/SL2C/Basic.lean
View file

@ -312,7 +312,7 @@ informal_lemma toRestrictedLorentzGroup where
deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_isOrthochronous,
``LorentzGroup.Restricted]
/-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/
TODO "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
end
end SL2C