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

Merge branch 'master' into Tensors

Browse source
This commit is contained in:
Joseph Tooby-Smith 2024-07-19 16:27:19 -04:00 • committed by GitHub
commit 850546783c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
27 changed files with 52 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/LorentzGroup/Basic.lean
View file

@ -224,7 +224,7 @@ lemma toGL_embedding : Embedding (@toGL d).toFun where
induced := by
refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
intro s
rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s]
rw [isOpen_induced_iff, isOpen_induced_iff]
exact exists_exists_and_eq_and

2
HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
View file

@ -166,7 +166,7 @@ lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
apply Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul_sum ]
rw [Finset.sum_mul_sum]
apply Finset.sum_congr rfl (fun j _ => ?_)
apply Finset.sum_congr rfl (fun k _ => ?_)
ring

4
HepLean/SpaceTime/LorentzVector/NormOne.lean
View file

@ -160,7 +160,7 @@ variable {v w : NormOneLorentzVector d}
lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
apply le_trans (time_abs_sub_space_norm v w)
rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩ , sub_eq_add_neg, right_spaceReflection]
rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩, sub_eq_add_neg, right_spaceReflection]
apply (add_le_add_iff_left _).mpr
rw [neg_le]
apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_
@ -223,7 +223,7 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur
apply Finset.sum_congr rfl
intro i _
ring
exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩,
exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _)⟩,
by
simp only [space, Function.comp_apply, mem_iff_time_nonneg, time, Real.sqrt_pos]
exact Real.sqrt_nonneg _⟩

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

@ -102,7 +102,7 @@ lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ)
/-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/
@[simps!]
def toLorentzGroupElem (M : SL(2, ℂ)) : LorentzGroup 3 :=
⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M) ,
⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M),
by simp [repLorentzVector, iff_det_selfAdjoint]⟩
/-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/