Boosts of space time

i. Overview

In this module we consider boosts acting on points in space time,and recover simple formulae for such applications.

Note that the material here currently assumes that the speed of light c = 1.

ii. Key results

• boost_x_smul : The action of a boost in the x-direction on a point in space time.

iii. Table of contents

• A. The action of a boost in the x-direction

iv. References

See e.g.

• https://en.wikipedia.org/wiki/Lorentz_transformation

A. The action of a boost in the x-direction

We show that boosting in the x-direction takes (t, x, y, z) to (γ (t - β x), γ (x - β t), y, z).

theorem SpaceTime.boost_x_smul (β : ℝ) (hβ : |β| < 1) (x : SpaceTime) : LorentzGroup.boost 0 β hβ • x = fun (x_1 : Fin 1 ⊕ Fin 3) => match x_1 with | Sum.inl 0 => LorentzGroup.γ β * (x (Sum.inl 0) - β * x (Sum.inr 0)) | Sum.inr 0 => LorentzGroup.γ β * (x (Sum.inr 0) - β * x (Sum.inl 0)) | Sum.inr 1 => x (Sum.inr 1) | Sum.inr 2 => x (Sum.inr 2)

theorem SpaceTime.boost_zero_apply_time_space {d : ℕ} {β : ℝ} (hβ : |β| < 1) (c : SpeedOfLight) (t : Time) (x : Space d.succ) : (LorentzGroup.boost 0 β hβ)⁻¹ • (toTimeAndSpace c).symm (t, x) = (toTimeAndSpace c).symm ({ val := LorentzGroup.γ β * (t.val + β / c.val * x.val 0) }, { val := fun (x_1 : Fin d.succ) => match x_1 with | ⟨0, ⋯⟩ => LorentzGroup.γ β * (x.val 0 + c.val * β * t.val) | ⟨n.succ, ih⟩ => x.val ⟨n.succ, ih⟩ })