Boosts of 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) (β : ℝ) (hβ : |β| < 1) (p : Vector d) : toCoord (LorentzGroup.boost i β hβ • p) (Sum.inl 0) = LorentzGroup.γ β * (toCoord p (Sum.inl 0) - β * toCoord p (Sum.inr i))

theorem Lorentz.Vector.boost_inr_self_eq {d : ℕ} (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) : toCoord (LorentzGroup.boost i β hβ • p) (Sum.inr i) = LorentzGroup.γ β * (toCoord p (Sum.inr i) - β * toCoord p (Sum.inl 0))

theorem Lorentz.Vector.boost_inr_other_eq {d : ℕ} (i j : Fin d) (hji : j ≠ i) (β : ℝ) (hβ : |β| < 1) (p : Vector d) : toCoord (LorentzGroup.boost i β hβ • p) (Sum.inr j) = toCoord p (Sum.inr j)

theorem Lorentz.Vector.boost_toCoord_eq {d : ℕ} (i : Fin d) (β : ℝ) (hβ : |β| < 1) (p : Vector d) : toCoord (LorentzGroup.boost i β hβ • p) = fun (j : Fin 1 ⊕ Fin d) => match j with | Sum.inl 0 => LorentzGroup.γ β * (toCoord p (Sum.inl 0) - β * toCoord p (Sum.inr i)) | Sum.inr j => if j = i then LorentzGroup.γ β * (toCoord p (Sum.inr i) - β * toCoord p (Sum.inl 0)) else toCoord p (Sum.inr j)