Boosts

This file defines those Lorentz which are boosts.

We first define generalised boosts, which are restricted lorentz transformations taking a four velocity u to a four velocity v.

A boost is the special case of a generalised boost when u = stdBasis 0.

References

• The main argument follows: Guillem Cobos, The Lorentz Group, 2015: https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf

def LorentzGroup.genBoostAux₁ {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Lorentz.ContrMod d →ₗ[ℝ] Lorentz.ContrMod d

An auxiliary linear map used in the definition of a generalised boost.

Equations

• LorentzGroup.genBoostAux₁ u v = { toFun := fun (x : Lorentz.ContrMod d) => (2 * Lorentz.contrContrContractField (x ⊗ₜ[ℝ] ↑↑u)) • ↑↑v, map_add' := ⋯, map_smul' := ⋯ }

def LorentzGroup.genBoostAux₂ {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Lorentz.ContrMod d →ₗ[ℝ] Lorentz.ContrMod d

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.

theorem LorentzGroup.genBoostAux₂_self {d : ℕ} (u : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : genBoostAux₂ u u = -genBoostAux₁ u u

def LorentzGroup.genBoost {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Lorentz.ContrMod d →ₗ[ℝ] Lorentz.ContrMod d

An generalised boost. This is a Lorentz transformation which takes the four velocity u to v.

Equations

• LorentzGroup.genBoost u v = LinearMap.id + LorentzGroup.genBoostAux₁ u v + LorentzGroup.genBoostAux₂ u v

theorem LorentzGroup.genBoost_mul_one_plus_contr {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) (x : ↑(Lorentz.Contr d).V) : (1 + Lorentz.contrContrContractField (↑↑u ⊗ₜ[ℝ] ↑↑v)) • (genBoost u v) x = (1 + Lorentz.contrContrContractField (↑↑u ⊗ₜ[ℝ] ↑↑v)) • x + (2 * Lorentz.contrContrContractField (x ⊗ₜ[ℝ] ↑↑u) * (1 + Lorentz.contrContrContractField (↑↑u ⊗ₜ[ℝ] ↑↑v))) • ↑↑v - Lorentz.contrContrContractField (x ⊗ₜ[ℝ] (↑↑u + ↑↑v)) • (↑↑u + ↑↑v)

theorem LorentzGroup.genBoost.self {d : ℕ} (u : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : genBoost u u = LinearMap.id

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.

def LorentzGroup.genBoost.toMatrix {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ

A generalised boost as a matrix.

Equations

• LorentzGroup.genBoost.toMatrix u v = (LinearMap.toMatrix Lorentz.ContrMod.stdBasis Lorentz.ContrMod.stdBasis) (LorentzGroup.genBoost u v)

theorem LorentzGroup.genBoost.toMatrix_mulVec {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) (x : ↑(Lorentz.Contr d).V) : Lorentz.ContrMod.mulVec (toMatrix u v) x = (genBoost u v) x

@[simp]

theorem LorentzGroup.genBoost.toMatrix_apply {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) (μ ν : Fin 1 ⊕ Fin d) : toMatrix u v μ ν = minkowskiMatrix μ μ * (Lorentz.contrContrContractField (Lorentz.ContrMod.stdBasis μ ⊗ₜ[ℝ] Lorentz.ContrMod.stdBasis ν) + 2 * Lorentz.contrContrContractField (Lorentz.ContrMod.stdBasis ν ⊗ₜ[ℝ] ↑↑u) * Lorentz.contrContrContractField (Lorentz.ContrMod.stdBasis μ ⊗ₜ[ℝ] ↑↑v) - Lorentz.contrContrContractField (Lorentz.ContrMod.stdBasis μ ⊗ₜ[ℝ] (↑↑u + ↑↑v)) * Lorentz.contrContrContractField (Lorentz.ContrMod.stdBasis ν ⊗ₜ[ℝ] (↑↑u + ↑↑v)) / (1 + Lorentz.contrContrContractField (↑↑u ⊗ₜ[ℝ] ↑↑v)))

theorem LorentzGroup.genBoost.toMatrix_continuous {d : ℕ} (u : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Continuous (toMatrix u)

theorem LorentzGroup.genBoost.toMatrix_in_lorentzGroup {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : toMatrix u v ∈ LorentzGroup d

def LorentzGroup.genBoost.toLorentz {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : ↑(LorentzGroup d)

A generalised boost as an element of the Lorentz Group.

Equations

• LorentzGroup.genBoost.toLorentz u v = ⟨LorentzGroup.genBoost.toMatrix u v, ⋯⟩

theorem LorentzGroup.genBoost.toLorentz_continuous {d : ℕ} (u : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Continuous (toLorentz u)

theorem LorentzGroup.genBoost.toLorentz_joined_to_1 {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : Joined 1 (toLorentz u v)

theorem LorentzGroup.genBoost.toLorentz_in_connected_component_1 {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : toLorentz u v ∈ connectedComponent 1

theorem LorentzGroup.genBoost.isProper {d : ℕ} (u v : ↑(Lorentz.Contr.NormOne.FuturePointing d)) : IsProper (toLorentz u v)