Generalized Boosts #
This module defines a generalization of the tradiational boosts.
They are define given two elocities u
and v
, as an input an take
the velocity u
to the velocity v
.
We show that these generalised boosts are Lorentz transformations, and furthermore sit in the restricted Lorentz group.
A boost is the special case of a generalised boost when u = basis 0
.
References #
- The main argument follows: Guillem Cobos, The Lorentz Group, 2015: https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
Auxiliary Linear Maps #
An auxiliary linear map used in the definition of a generalised boost.
Equations
- LorentzGroup.genBoostAux₁ u v = { toFun := fun (x : Lorentz.Vector d) => (2 * (Lorentz.Vector.minkowskiProduct x) ↑u) • ↑v, map_add' := ⋯, map_smul' := ⋯ }
Instances For
An auxiliary linear map used in the definition of a generalised boost.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generalized Boosts #
An generalised boost. This is a Lorentz transformation which takes the Lorentz velocity u
to v
.
Equations
Instances For
This lemma states that for a given four-velocity u
, the general boost
transformation genBoost u u
is equal to the identity linear map LinearMap.id
.
The time component of a generalised boost is equal to
1 +
‖u.1.timeComponent • v.1.spatialPart - v.1.timeComponent • u.1.spatialPart‖ / (1 + ⟪u.1, v.1⟫ₘ)
A proof of this result can be found at the below link: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Lorentz.20group/near/523249684
Note that the decleration of this semiformal result will be similar once
the TODO item FXQ45
is completed.