PhysLean Documentation

PhysLean.Relativity.LorentzGroup.Boosts.Apply

Boosts applied to Lorentz vectors #

These recover what one would describe as the ordinary Lorentz transformations of Lorentz vectors.

theorem Lorentz.Vector.boost_time_eq {d : } (i : Fin d) (β : ) ( : |β| < 1) (p : Vector d) :
(LorentzGroup.boost i β p) (Sum.inl 0) = LorentzGroup.γ β * (p (Sum.inl 0) - β * p (Sum.inr i))
theorem Lorentz.Vector.boost_inr_self_eq {d : } (i : Fin d) (β : ) ( : |β| < 1) (p : Vector d) :
(LorentzGroup.boost i β p) (Sum.inr i) = LorentzGroup.γ β * (p (Sum.inr i) - β * p (Sum.inl 0))
theorem Lorentz.Vector.boost_inr_other_eq {d : } (i j : Fin d) (hji : j i) (β : ) ( : |β| < 1) (p : Vector d) :
(LorentzGroup.boost i β p) (Sum.inr j) = p (Sum.inr j)
theorem Lorentz.Vector.boost_toCoord_eq {d : } (i : Fin d) (β : ) ( : |β| < 1) (p : Vector d) :
LorentzGroup.boost i β p = fun (j : Fin 1 Fin d) => match j with | Sum.inl 0 => LorentzGroup.γ β * (p (Sum.inl 0) - β * p (Sum.inr i)) | Sum.inr j => if j = i then LorentzGroup.γ β * (p (Sum.inr i) - β * p (Sum.inl 0)) else p (Sum.inr j)