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

def LorentzGroup.genBoostAux₁ {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : Lorentz.Vector d →ₗ[ℝ] Lorentz.Vector d

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' := ⋯ }

def LorentzGroup.genBoostAux₂ {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : Lorentz.Vector d →ₗ[ℝ] Lorentz.Vector 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.Velocity d)) : genBoostAux₂ u u = -genBoostAux₁ u u

def LorentzGroup.genBoost {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : Lorentz.Vector d →ₗ[ℝ] Lorentz.Vector 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.genBoost_mul_one_plus_contr {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (x : Lorentz.Vector d) : (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v) • (genBoost u v) x = (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v) • x + (2 * (Lorentz.Vector.minkowskiProduct x) ↑u * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)) • ↑v - (Lorentz.Vector.minkowskiProduct x) (↑u + ↑v) • (↑u + ↑v)

theorem LorentzGroup.genBoost.self {d : ℕ} (u : ↑(Lorentz.Velocity 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.

theorem LorentzGroup.genBoost.genBoostAux₁_apply_basis {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ : Fin 1 ⊕ Fin d) : (genBoostAux₁ u v) (Lorentz.Vector.basis μ) = (2 * minkowskiMatrix μ μ * Lorentz.Vector.toCoord (↑u) μ) • ↑v

theorem LorentzGroup.genBoost.genBoostAux₂_apply_basis {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ : Fin 1 ⊕ Fin d) : (genBoostAux₂ u v) (Lorentz.Vector.basis μ) = -(minkowskiMatrix μ μ * (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)

theorem LorentzGroup.genBoost.genBoost_apply_basis {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ : Fin 1 ⊕ Fin d) : (genBoost u v) (Lorentz.Vector.basis μ) = Lorentz.Vector.basis μ + (2 * minkowskiMatrix μ μ * Lorentz.Vector.toCoord (↑u) μ) • ↑v - (minkowskiMatrix μ μ * (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)

To Matrix

def LorentzGroup.genBoost.toMatrix {d : ℕ} (u v : ↑(Lorentz.Velocity 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.Vector.basis Lorentz.Vector.basis) (LorentzGroup.genBoost u v)

theorem LorentzGroup.genBoost.toMatrix_mulVec {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (x : Lorentz.Vector d) : (toMatrix u v).mulVec (Lorentz.Vector.toCoord x) = Lorentz.Vector.toCoord ((genBoost u v) x)

theorem LorentzGroup.genBoost.genBoostAux₁_toMatrix_apply {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (LinearMap.toMatrix Lorentz.Vector.basis Lorentz.Vector.basis) (genBoostAux₁ u v) μ ν = minkowskiMatrix ν ν * (2 * Lorentz.Vector.toCoord (↑u) ν * Lorentz.Vector.toCoord (↑v) μ)

theorem LorentzGroup.genBoost.genBoostAux₂_toMatrix_apply {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (LinearMap.toMatrix Lorentz.Vector.basis Lorentz.Vector.basis) (genBoostAux₂ u v) μ ν = minkowskiMatrix ν ν * (-(Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v))

theorem LorentzGroup.genBoost.toMatrix_apply_eq_minkowskiProduct {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : toMatrix u v μ ν = minkowskiMatrix μ μ * ((Lorentz.Vector.minkowskiProduct (Lorentz.Vector.basis μ)) (Lorentz.Vector.basis ν) + 2 * (Lorentz.Vector.minkowskiProduct (Lorentz.Vector.basis ν)) ↑u * (Lorentz.Vector.minkowskiProduct (Lorentz.Vector.basis μ)) ↑v - (Lorentz.Vector.minkowskiProduct (Lorentz.Vector.basis μ)) (↑u + ↑v) * (Lorentz.Vector.minkowskiProduct (Lorentz.Vector.basis ν)) (↑u + ↑v) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v))

theorem LorentzGroup.genBoost.toMatrix_apply_eq_toCoord {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : toMatrix u v μ ν = 1 μ ν + 2 * minkowskiMatrix ν ν * Lorentz.Vector.toCoord (↑u) ν * Lorentz.Vector.toCoord (↑v) μ - minkowskiMatrix ν ν * (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)

theorem LorentzGroup.genBoost.toMatrix_continuous_snd {d : ℕ} (u : ↑(Lorentz.Velocity d)) : Continuous (toMatrix u)

theorem LorentzGroup.genBoost.toMatrix_continuous_fst {d : ℕ} (u : ↑(Lorentz.Velocity d)) : Continuous fun (x : ↑(Lorentz.Velocity d)) => toMatrix x u

Proving that toMatrix is in the Lorentz group

theorem LorentzGroup.genBoost.genBoostAux₁_basis_minkowskiProduct {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (Lorentz.Vector.minkowskiProduct ((genBoostAux₁ u v) (Lorentz.Vector.basis μ))) ((genBoostAux₁ u v) (Lorentz.Vector.basis ν)) = 4 * minkowskiMatrix μ μ * minkowskiMatrix ν ν * Lorentz.Vector.toCoord (↑u) μ * Lorentz.Vector.toCoord (↑u) ν

theorem LorentzGroup.genBoost.genBoostAux₂_basis_minkowskiProduct {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (Lorentz.Vector.minkowskiProduct ((genBoostAux₂ u v) (Lorentz.Vector.basis μ))) ((genBoostAux₂ u v) (Lorentz.Vector.basis ν)) = 2 * minkowskiMatrix μ μ * minkowskiMatrix ν ν * (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν) * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)⁻¹

theorem LorentzGroup.genBoost.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (Lorentz.Vector.minkowskiProduct ((genBoostAux₁ u v) (Lorentz.Vector.basis μ))) ((genBoostAux₂ u v) (Lorentz.Vector.basis ν)) = -2 * minkowskiMatrix μ μ * minkowskiMatrix ν ν * Lorentz.Vector.toCoord (↑u) μ * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν)

theorem LorentzGroup.genBoost.genBoostAux₁_add_genBoostAux₂_minkowskiProduct {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (Lorentz.Vector.minkowskiProduct ((genBoostAux₁ u v) (Lorentz.Vector.basis μ) + (genBoostAux₂ u v) (Lorentz.Vector.basis μ))) ((genBoostAux₁ u v) (Lorentz.Vector.basis ν) + (genBoostAux₂ u v) (Lorentz.Vector.basis ν)) = 2 * minkowskiMatrix μ μ * minkowskiMatrix ν ν * (-Lorentz.Vector.toCoord (↑u) μ * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν) - Lorentz.Vector.toCoord (↑u) ν * (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) + (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν) * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)⁻¹ + 2 * Lorentz.Vector.toCoord (↑u) μ * Lorentz.Vector.toCoord (↑u) ν)

theorem LorentzGroup.genBoost.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂ {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : (Lorentz.Vector.minkowskiProduct (Lorentz.Vector.basis μ)) ((genBoostAux₁ u v) (Lorentz.Vector.basis ν) + (genBoostAux₂ u v) (Lorentz.Vector.basis ν)) = minkowskiMatrix μ μ * minkowskiMatrix ν ν * (2 * Lorentz.Vector.toCoord (↑u) ν * Lorentz.Vector.toCoord (↑v) μ - (Lorentz.Vector.toCoord (↑u) μ + Lorentz.Vector.toCoord (↑v) μ) * (Lorentz.Vector.toCoord (↑u) ν + Lorentz.Vector.toCoord (↑v) ν) * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)⁻¹)

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

To Lorentz group

def LorentzGroup.genBoost.toLorentz {d : ℕ} (u v : ↑(Lorentz.Velocity 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.Velocity d)) : Continuous (toLorentz u)

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

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

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

theorem LorentzGroup.genBoost.isOrthochronous {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : IsOrthochronous (toLorentz u v)

theorem LorentzGroup.genBoost.toLorentz_mem_restricted {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : toLorentz u v ∈ restricted d