PhysLean Documentation

PhysLean.Relativity.LorentzGroup.Boosts.Generalized

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 #

Auxiliary Linear Maps #

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

Equations
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
      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₂_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 ν)

      Generalized Boosts #

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

      Equations
      Instances For
        @[simp]
        @[simp]
        @[simp]

        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_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)

        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.