Generalized Boosts

This module defines a generalization of the traditional boosts. They are define given two velocities 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

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

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

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

theorem LorentzGroup.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 ν ν * ↑u μ * ↑u ν

theorem LorentzGroup.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 * ↑u ν * ↑v μ)

theorem LorentzGroup.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 ν ν * (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)⁻¹

theorem LorentzGroup.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 ν ν * ↑u μ * (↑u ν + ↑v ν)

theorem LorentzGroup.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 ν ν * (-(↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v))

theorem LorentzGroup.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 ν ν * (-↑u μ * (↑u ν + ↑v ν) - ↑u ν * (↑u μ + ↑v μ) + (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)⁻¹ + 2 * ↑u μ * ↑u ν)

theorem LorentzGroup.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 * ↑u ν * ↑v μ - (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)⁻¹)

Generalized Boosts

def LorentzGroup.generalizedBoost {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : ↑(LorentzGroup d)

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

Equations

• LorentzGroup.generalizedBoost u v = ⟨(LinearMap.toMatrix Lorentz.Vector.basis Lorentz.Vector.basis) (LinearMap.id + LorentzGroup.genBoostAux₁ u v + LorentzGroup.genBoostAux₂ u v), ⋯⟩

theorem LorentzGroup.generalizedBoost_apply {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (x : Lorentz.Vector d) : generalizedBoost u v • x = x + (genBoostAux₁ u v) x + (genBoostAux₂ u v) x

theorem LorentzGroup.generalizedBoost_apply_mul_one_plus_contr {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (x : Lorentz.Vector d) : (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v) • generalizedBoost 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.generalizedBoost_apply_expand {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (x : Lorentz.Vector d) : generalizedBoost u v • x = x + (2 * (Lorentz.Vector.minkowskiProduct x) ↑u) • ↑v - ((Lorentz.Vector.minkowskiProduct x) (↑u + ↑v) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)

@[simp]

theorem LorentzGroup.generalizedBoost_apply_fst {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : generalizedBoost u v • ↑u = ↑v

@[simp]

theorem LorentzGroup.generalizedBoost_apply_snd {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : generalizedBoost u v • ↑v = (2 * (Lorentz.Vector.minkowskiProduct ↑u) ↑v) • ↑v - ↑u

@[simp]

theorem LorentzGroup.generalizedBoost_self {d : ℕ} (u : ↑(Lorentz.Velocity d)) : generalizedBoost u u = 1

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.genearlizedBoost_apply_basis {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ : Fin 1 ⊕ Fin d) : generalizedBoost u v • Lorentz.Vector.basis μ = Lorentz.Vector.basis μ + (2 * minkowskiMatrix μ μ * ↑u μ) • ↑v - (minkowskiMatrix μ μ * (↑u μ + ↑v μ) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)

theorem LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : ↑(generalizedBoost 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.generalizedBoost_apply_eq_toCoord {d : ℕ} (u v : ↑(Lorentz.Velocity d)) (μ ν : Fin 1 ⊕ Fin d) : ↑(generalizedBoost u v) μ ν = 1 μ ν + 2 * minkowskiMatrix ν ν * ↑u ν * ↑v μ - minkowskiMatrix ν ν * (↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)

theorem LorentzGroup.generalizedBoost_continuous_snd {d : ℕ} (u : ↑(Lorentz.Velocity d)) : Continuous (generalizedBoost u)

theorem LorentzGroup.generalizedBoost_continuous_fst {d : ℕ} (u : ↑(Lorentz.Velocity d)) : Continuous fun (x : ↑(Lorentz.Velocity d)) => generalizedBoost x u

theorem LorentzGroup.id_joined_generalizedBoost {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : Joined 1 (generalizedBoost u v)

theorem LorentzGroup.generalizedBoost_in_connected_component_of_id {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : generalizedBoost u v ∈ connectedComponent 1

theorem LorentzGroup.generalizedBoost_isProper {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : IsProper (generalizedBoost u v)

theorem LorentzGroup.generalizedBoost_isOrthochronous {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : IsOrthochronous (generalizedBoost u v)

theorem LorentzGroup.generalizedBoost_mem_restricted {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : generalizedBoost u v ∈ restricted d

theorem LorentzGroup.generalizedBoost_inv {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : (generalizedBoost u v)⁻¹ = generalizedBoost v u

theorem LorentzGroup.generalizedBoost_timeComponent_eq {d : ℕ} (u v : ↑(Lorentz.Velocity d)) : ↑(generalizedBoost u v) (Sum.inl 0) (Sum.inl 0) = 1 + ‖(↑u).timeComponent • (↑v).spatialPart - (↑v).timeComponent • (↑u).spatialPart‖ ^ 2 / (1 + (Lorentz.Vector.minkowskiProduct ↑u) ↑v)

The time component of a generalised boost.

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