Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Relativity.LorentzGroup.Restricted.BasicGeneralized 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
@[expose] public sectionAuxiliary Linear Maps
An auxiliary linear map used in the definition of a generalised boost.
def genBoostAux₁ (u v : Velocity d) : Vector d →ₗ[ℝ] Vector d where
toFun x := (2 * ⟪x, u⟫ₘ) • v
map_add' x y := d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dy:Lorentz.Vector d⊢ (2 * (minkowskiProduct (x + y)) ↑u) • ↑v = (2 * (minkowskiProduct x) ↑u) • ↑v + (2 * (minkowskiProduct y) ↑u) • ↑v
All goals completed! 🐙
map_smul' c x := d:ℕu:↑(Velocity d)v:↑(Velocity d)c:ℝx:Lorentz.Vector d⊢ (2 * (minkowskiProduct (c • x)) ↑u) • ↑v = (RingHom.id ℝ) c • (2 * (minkowskiProduct x) ↑u) • ↑v
d:ℕu:↑(Velocity d)v:↑(Velocity d)c:ℝx:Lorentz.Vector d⊢ (2 * (c • minkowskiProduct x) ↑u) • ↑v = (c * (2 * (minkowskiProduct x) ↑u)) • ↑v
d:ℕu:↑(Velocity d)v:↑(Velocity d)c:ℝx:Lorentz.Vector d⊢ (2 * (c * (minkowskiProduct x) ↑u)) • ↑v = (c * (2 * (minkowskiProduct x) ↑u)) • ↑v
d:ℕu:↑(Velocity d)v:↑(Velocity d)c:ℝx:Lorentz.Vector d⊢ 2 * (c * (minkowskiProduct x) ↑u) = c * (2 * (minkowskiProduct x) ↑u)
All goals completed! 🐙An auxiliary linear map used in the definition of a generalised boost.
All goals completed! 🐙lemma genBoostAux₂_self (u : Velocity d) : genBoostAux₂ u u = - genBoostAux₁ u u := d:ℕu:↑(Velocity d)⊢ genBoostAux₂ u u = -genBoostAux₁ u u
d:ℕu:↑(Velocity d)x:Lorentz.Vector d⊢ (genBoostAux₂ u u) x = (-genBoostAux₁ u u) x
d:ℕu:↑(Velocity d)x:Lorentz.Vector d⊢ -(((minkowskiProduct x) ↑u + (minkowskiProduct x) ↑u) / (1 + 1)) • (↑u + ↑u) = -((2 * (minkowskiProduct x) ↑u) • ↑u)
d:ℕu:↑(Velocity d)x:Lorentz.Vector d⊢ -(((minkowskiProduct x) ↑u + (minkowskiProduct x) ↑u) / (1 + 1)) * (1 + 1) = -(2 * (minkowskiProduct x) ↑u * 1)
All goals completed! 🐙lemma genBoostAux₁_apply_basis (u v : Velocity d) (μ : Fin 1 ⊕ Fin d) :
(genBoostAux₁ u v) (Vector.basis μ) = (2 * η μ μ * u.1 μ) • v := d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin d⊢ (genBoostAux₁ u v) (basis μ) = (2 * η μ μ * ↑u μ) • ↑v
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin d⊢ (2 * (η μ μ * ↑u μ)) • ↑v = (2 * η μ μ * ↑u μ) • ↑v
All goals completed! 🐙lemma genBoostAux₂_apply_basis (u v : Velocity d) (μ : Fin 1 ⊕ Fin d) :
(genBoostAux₂ u v) (Vector.basis μ) =
- (η μ μ * (u.1 μ + v.1 μ) / (1 + ⟪u.1, v.1⟫ₘ)) • (u.1 + v.1) := d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin d⊢ (genBoostAux₂ u v) (basis μ) = -(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin d⊢ -(((η μ μ * ↑u μ + η μ μ * ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • ↑u) +
-(((η μ μ * ↑u μ + η μ μ * ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • ↑v) =
-((η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • ↑u) +
-((η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • ↑v)
All goals completed! 🐙lemma genBoostAux₁_basis_minkowskiProduct (u v : Velocity d) (μ ν : Fin 1 ⊕ Fin d) :
⟪genBoostAux₁ u v (Vector.basis μ), genBoostAux₁ u v (Vector.basis ν)⟫ₘ =
4 * η μ μ * η ν ν * u.1 μ * u.1 ν := d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (minkowskiProduct ((genBoostAux₁ u v) (basis μ))) ((genBoostAux₁ u v) (basis ν)) = 4 * η μ μ * η ν ν * ↑u μ * ↑u ν
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ 2 * (η ν ν * ↑u ν) * (2 * (η μ μ * ↑u μ)) = 4 * η μ μ * η ν ν * ↑u μ * ↑u ν
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (genBoostAux₁ u v) (basis ν) μ = η ν ν * (2 * ↑u ν * ↑v μ)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ 2 * (η ν ν * ↑u ν) * ↑v μ = η ν ν * (2 * ↑u ν * ↑v μ)
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:(minkowskiProduct (↑u + ↑v)) (↑u + ↑v) = 2 * (1 + (minkowskiProduct ↑u) ↑v)h2✝:1 + (minkowskiProduct ↑u) ↑v ≠ 0h2:(minkowskiProduct ↑v) ↑u = (minkowskiProduct ↑u) ↑v⊢ -(η ν ν * (↑u ν + ↑v ν) *
(-(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • minkowskiProduct (↑u + ↑v)) (↑u + ↑v)) =
η ν ν * (↑u ν + ↑v ν) * η μ μ * (↑u μ + ↑v μ) * 2
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:(minkowskiProduct (↑u + ↑v)) (↑u + ↑v) = 2 * (1 + (minkowskiProduct ↑u) ↑v)h2✝:1 + (minkowskiProduct ↑u) ↑v ≠ 0h2:(minkowskiProduct ↑v) ↑u = (minkowskiProduct ↑u) ↑v⊢ -(η ν ν * (↑u ν + ↑v ν) *
(-(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v) * 1) +
-(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v) * (minkowskiProduct ↑u) ↑v) +
(-(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v) * (minkowskiProduct ↑u) ↑v) +
-(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v) * 1)))) =
η ν ν * (↑u ν + ↑v ν) * η μ μ * (↑u μ + ↑v μ) * 2
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:(minkowskiProduct (↑u + ↑v)) (↑u + ↑v) = 2 * (1 + (minkowskiProduct ↑u) ↑v)h2✝:1 + (minkowskiProduct ↑u) ↑v ≠ 0h2:(minkowskiProduct ↑v) ↑u = (minkowskiProduct ↑u) ↑v⊢ -(η ν ν * (↑u ν + ↑v ν) * η μ μ * (↑u μ + ↑v μ) * (-1 + -(minkowskiProduct ↑u) ↑v + (-(minkowskiProduct ↑u) ↑v + -1))) =
η ν ν * (↑u ν + ↑v ν) * η μ μ * (↑u μ + ↑v μ) * (1 + (minkowskiProduct ↑u) ↑v) * 2
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:(minkowskiProduct ↑v) (↑u + ↑v) = 1 + (minkowskiProduct ↑u) ↑vh2:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ η ν ν * (↑u ν + ↑v ν) * η μ μ * ↑u μ * ((minkowskiProduct ↑u) ↑v + 1) =
η ν ν * (↑u ν + ↑v ν) * (1 + (minkowskiProduct ↑u) ↑v) * η μ μ * ↑u μ
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (genBoostAux₂ u v) (basis ν) μ = η ν ν * (-(↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (-(η ν ν * (↑u + ↑v) ν / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)) μ =
η ν ν * (-(↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (-(η ν ν * (↑u + ↑v) ν / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)) μ =
η ν ν * (-(↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ -(η ν ν * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v) * (↑u μ + ↑v μ)) =
η ν ν * ((-↑v μ + -↑u μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ -(η ν ν * (↑u ν + ↑v ν) * (↑u μ + ↑v μ)) = η ν ν * (↑u ν + ↑v ν) * (-↑v μ + -↑u μ)
All goals completed! 🐙lemma genBoostAux₁_add_genBoostAux₂_minkowskiProduct (u v : Velocity d) (μ ν : Fin 1 ⊕ Fin d) :
⟪genBoostAux₁ u v (Vector.basis μ) + genBoostAux₂ u v (Vector.basis μ),
genBoostAux₁ u v (Vector.basis ν) + genBoostAux₂ u v (Vector.basis ν)⟫ₘ =
2 * η μ μ * η ν ν * (- u.1 μ * (u.1 ν + v.1 ν)
- u.1 ν * (u.1 μ + v.1 μ)
+ (u.1 μ + v.1 μ) * (u.1 ν + v.1 ν) * (1 + ⟪u, v.1⟫ₘ)⁻¹ +
2 * u.1 μ * u.1 ν) := d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ)))
((genBoostAux₁ u v) (basis ν) + (genBoostAux₂ u v) (basis ν)) =
2 * η μ μ * η ν ν *
(-↑u μ * (↑u ν + ↑v ν) - ↑u ν * (↑u μ + ↑v μ) + (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ +
2 * ↑u μ * ↑u ν)
conv_lhs =>
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct ((genBoostAux₁ u v) (basis μ))) ((genBoostAux₁ u v) (basis ν)) +
(minkowskiProduct ((genBoostAux₂ u v) (basis μ))) ((genBoostAux₁ u v) (basis ν)) +
((minkowskiProduct ((genBoostAux₁ u v) (basis μ))) ((genBoostAux₂ u v) (basis ν)) +
(minkowskiProduct ((genBoostAux₂ u v) (basis μ))) ((genBoostAux₂ u v) (basis ν)))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| 4 * η μ μ * η ν ν * ↑u μ * ↑u ν + -2 * η ν ν * η μ μ * ↑u ν * (↑u μ + ↑v μ) +
(-2 * η μ μ * η ν ν * ↑u μ * (↑u ν + ↑v ν) +
2 * η μ μ * η ν ν * (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (minkowskiProduct ↑u) ↑v)⁻¹)
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh2:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 2 * η ν ν * ↑u ν * (η μ μ * ↑v μ) +
-(η ν ν * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v) * (η μ μ * (↑u μ + ↑v μ))) =
η μ μ * η ν ν * (2 * ↑u ν * ↑v μ - (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (minkowskiProduct ↑u) ↑v)⁻¹)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh2:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ η ν ν * η μ μ * (2 * ↑u ν * ↑v μ * (1 + (minkowskiProduct ↑u) ↑v) + -((↑u ν + ↑v ν) * (↑u μ + ↑v μ))) =
η ν ν * η μ μ * (2 * ↑u ν * ↑v μ * (1 + (minkowskiProduct ↑u) ↑v) - (↑u ν + ↑v ν) * (↑u μ + ↑v μ))
All goals completed! 🐙Generalized Boosts
An generalised boost. This is a Lorentz transformation which takes the Lorentz velocity u
to v.
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (minkowskiProduct (basis μ + ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ)))) (basis ν) +
(minkowskiProduct (basis μ + ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ))))
((genBoostAux₁ u v) (basis ν) + (genBoostAux₂ u v) (basis ν)) =
(minkowskiProduct (basis μ)) (basis ν)
conv_lhs =>
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct (basis μ + ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ)))) (basis ν)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct (basis μ) + minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ))) (basis ν)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct (basis μ)) (basis ν) +
(minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ))) (basis ν)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ))) (basis ν)
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| η ν ν * η μ μ * (2 * ↑u μ * ↑v ν - (↑u ν + ↑v ν) * (↑u μ + ↑v μ) * (1 + (minkowskiProduct ↑u) ↑v)⁻¹)
conv_lhs =>
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| minkowskiProduct (basis μ + ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ)))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| minkowskiProduct (basis μ) + minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ))
conv_lhs =>
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct (basis μ) + minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ)))
((genBoostAux₁ u v) (basis ν) + (genBoostAux₂ u v) (basis ν))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (minkowskiProduct (basis μ)) ((genBoostAux₁ u v) (basis ν) + (genBoostAux₂ u v) (basis ν)) +
(minkowskiProduct ((genBoostAux₁ u v) (basis μ) + (genBoostAux₂ u v) (basis μ)))
((genBoostAux₁ u v) (basis ν) + (genBoostAux₂ u v) (basis ν))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| η μ μ * η ν ν * (2 * ↑u ν * ↑v μ - (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (minkowskiProduct ↑u) ↑v)⁻¹) +
2 * η μ μ * η ν ν *
(-↑u μ * (↑u ν + ↑v ν) - ↑u ν * (↑u μ + ↑v μ) + (↑u μ + ↑v μ) * (↑u ν + ↑v ν) * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ +
2 * ↑u μ * ↑u ν)
All goals completed! 🐙⟩All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector d⊢ (1 + (minkowskiProduct ↑u) ↑v) • x + (2 * (minkowskiProduct x) ↑u * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v +
-((minkowskiProduct x) (↑u + ↑v) • (↑u + ↑v)) =
(1 + (minkowskiProduct ↑u) ↑v) • x + (2 * (minkowskiProduct x) ↑u * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v -
(minkowskiProduct x) (↑u + ↑v) • (↑u + ↑v)
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (1 + (minkowskiProduct ↑u) ↑v) • x + (2 * (minkowskiProduct x) ↑u * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v -
(minkowskiProduct x) (↑u + ↑v) • (↑u + ↑v) =
(1 + (minkowskiProduct ↑u) ↑v) •
(x + (2 * (minkowskiProduct x) ↑u) • ↑v -
((minkowskiProduct x) (↑u + ↑v) / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v))
d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (1 + (minkowskiProduct ↑u) ↑v) * 1 = (1 + (minkowskiProduct ↑u) ↑v) * 1d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 2 * (minkowskiProduct x) ↑u * (1 + (minkowskiProduct ↑u) ↑v) * 1 - (minkowskiProduct x) (↑u + ↑v) * 1 =
(1 + (minkowskiProduct ↑u) ↑v) *
(2 * (minkowskiProduct x) ↑u * 1 - (minkowskiProduct x) (↑u + ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1)d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ -((minkowskiProduct x) (↑u + ↑v) * 1) =
(1 + (minkowskiProduct ↑u) ↑v) * -((minkowskiProduct x) (↑u + ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1) d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (1 + (minkowskiProduct ↑u) ↑v) * 1 = (1 + (minkowskiProduct ↑u) ↑v) * 1d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 2 * (minkowskiProduct x) ↑u * (1 + (minkowskiProduct ↑u) ↑v) * 1 - (minkowskiProduct x) (↑u + ↑v) * 1 =
(1 + (minkowskiProduct ↑u) ↑v) *
(2 * (minkowskiProduct x) ↑u * 1 - (minkowskiProduct x) (↑u + ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1)d:ℕu:↑(Velocity d)v:↑(Velocity d)x:Lorentz.Vector dh:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ -((minkowskiProduct x) (↑u + ↑v) * 1) =
(1 + (minkowskiProduct ↑u) ↑v) * -((minkowskiProduct x) (↑u + ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1) All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) • ↑u + (2 * (minkowskiProduct ↑u) ↑u * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v -
(minkowskiProduct ↑u) (↑u + ↑v) • (↑u + ↑v) =
(1 + (minkowskiProduct ↑u) ↑v) • ↑v
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) • ↑u + (2 * 1 * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v -
(1 + (minkowskiProduct ↑u) ↑v) • (↑u + ↑v) =
(1 + (minkowskiProduct ↑u) ↑v) • ↑v
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) * 1 - (1 + (minkowskiProduct ↑u) ↑v) * 1 = 0d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ 2 * 1 * (1 + (minkowskiProduct ↑u) ↑v) * 1 - (1 + (minkowskiProduct ↑u) ↑v) * 1 = (1 + (minkowskiProduct ↑u) ↑v) * 1 d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) * 1 - (1 + (minkowskiProduct ↑u) ↑v) * 1 = 0d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ 2 * 1 * (1 + (minkowskiProduct ↑u) ↑v) * 1 - (1 + (minkowskiProduct ↑u) ↑v) * 1 = (1 + (minkowskiProduct ↑u) ↑v) * 1 All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) • ↑v + (2 * (minkowskiProduct ↑v) ↑u * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v -
(minkowskiProduct ↑v) (↑u + ↑v) • (↑u + ↑v) =
(1 + (minkowskiProduct ↑u) ↑v) • ((2 * (minkowskiProduct ↑u) ↑v) • ↑v - ↑u)
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) • ↑v + (2 * (minkowskiProduct ↑u) ↑v * (1 + (minkowskiProduct ↑u) ↑v)) • ↑v -
((minkowskiProduct ↑u) ↑v + 1) • (↑u + ↑v) =
(1 + (minkowskiProduct ↑u) ↑v) • ((2 * (minkowskiProduct ↑u) ↑v) • ↑v - ↑u)
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) * 1 + 2 * (minkowskiProduct ↑u) ↑v * (1 + (minkowskiProduct ↑u) ↑v) * 1 -
((minkowskiProduct ↑u) ↑v + 1) * 1 =
(1 + (minkowskiProduct ↑u) ↑v) * (2 * (minkowskiProduct ↑u) ↑v * 1)d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ -(((minkowskiProduct ↑u) ↑v + 1) * 1) = (1 + (minkowskiProduct ↑u) ↑v) * -1 d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ (1 + (minkowskiProduct ↑u) ↑v) * 1 + 2 * (minkowskiProduct ↑u) ↑v * (1 + (minkowskiProduct ↑u) ↑v) * 1 -
((minkowskiProduct ↑u) ↑v + 1) * 1 =
(1 + (minkowskiProduct ↑u) ↑v) * (2 * (minkowskiProduct ↑u) ↑v * 1)d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ -(((minkowskiProduct ↑u) ↑v + 1) * 1) = (1 + (minkowskiProduct ↑u) ↑v) * -1 All goals completed! 🐙
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.
@[simp]
lemma generalizedBoost_self (u : Velocity d) :
generalizedBoost u u = 1 := d:ℕu:↑(Velocity d)⊢ generalizedBoost u u = 1
d:ℕu:↑(Velocity d)⊢ ↑(generalizedBoost u u) = ↑1
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin d⊢ basis μ + (2 * η μ μ * ↑u μ) • ↑v + -(η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v) =
basis μ + (2 * η μ μ * ↑u μ) • ↑v - (η μ μ * (↑u μ + ↑v μ) / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v)
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ η ν ν * (-(↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v)) =
-(η μ μ *
((minkowskiProduct (basis μ)) (↑u + ↑v) * (minkowskiProduct (basis ν)) (↑u + ↑v) /
(1 + (minkowskiProduct ↑u) ↑v)))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ η ν ν * ((-↑v μ + -↑u μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v)) =
-(η μ μ * ((η μ μ * ↑u μ + η μ μ * ↑v μ) * (η ν ν * ↑u ν + η ν ν * ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v)))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ -(η ν ν * ↑v μ * ↑u ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹) - η ν ν * ↑v μ * ↑v ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ -
η ν ν * ↑u μ * ↑u ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ -
η ν ν * ↑u μ * ↑v ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ =
-(η ν ν * ↑v μ * ↑u ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ * η μ μ ^ 2) -
η ν ν * ↑v μ * ↑v ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ * η μ μ ^ 2 -
η ν ν * ↑u μ * ↑u ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ * η μ μ ^ 2 -
η ν ν * ↑u μ * ↑v ν * (1 + (minkowskiProduct ↑u) ↑v)⁻¹ * η μ μ ^ 2
All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ η ν ν * (-(↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v)) =
-(η ν ν * (↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v))
d:ℕu:↑(Velocity d)v:↑(Velocity d)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ η ν ν * ((-↑v μ + -↑u μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v)) =
-(η ν ν * (↑u μ + ↑v μ) * (↑u ν + ↑v ν) / (1 + (minkowskiProduct ↑u) ↑v))
All goals completed! 🐙d:ℕu:↑(Velocity d)this:Continuous fun v => ↑(generalizedBoost u v)⊢ Continuous (generalizedBoost u)
All goals completed! 🐙d:ℕu:↑(Velocity d)this:Continuous fun v => ↑(generalizedBoost v u)⊢ Continuous fun x => generalizedBoost x u
All goals completed! 🐙lemma id_joined_generalizedBoost (u v : Velocity d) : Joined 1 (generalizedBoost u v) := d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ Joined 1 (generalizedBoost u v)
d:ℕu:↑(Velocity d)v:↑(Velocity d)f:Path u vh✝:∀ (t : ↑unitInterval), f t ∈ Set.univ⊢ Joined 1 (generalizedBoost u v)
use ContinuousMap.comp ⟨generalizedBoost u, d:ℕu:↑(Velocity d)v:↑(Velocity d)f:Path u vh✝:∀ (t : ↑unitInterval), f t ∈ Set.univ⊢ Continuous (generalizedBoost u) All goals completed! 🐙⟩ f
d:ℕu:↑(Velocity d)v:↑(Velocity d)f:Path u vh✝:∀ (t : ↑unitInterval), f t ∈ Set.univ⊢ ({ toFun := generalizedBoost u, continuous_toFun := ⋯ }.comp ↑f).toFun 0 = 1 All goals completed! 🐙
d:ℕu:↑(Velocity d)v:↑(Velocity d)f:Path u vh✝:∀ (t : ↑unitInterval), f t ∈ Set.univ⊢ ({ toFun := generalizedBoost u, continuous_toFun := ⋯ }.comp ↑f).toFun 1 = generalizedBoost u v All goals completed! 🐙lemma generalizedBoost_in_connected_component_of_id (u v : Velocity d) :
generalizedBoost u v ∈ connectedComponent 1 :=
pathComponent_subset_component _ (id_joined_generalizedBoost u v)lemma generalizedBoost_isProper (u v : Velocity d) : IsProper (generalizedBoost u v) :=
(isProper_on_connected_component
(generalizedBoost_in_connected_component_of_id u v)).mp isProper_idlemma generalizedBoost_isOrthochronous (u v : Velocity d) :
IsOrthochronous (generalizedBoost u v) :=
(isOrthochronous_on_connected_component (generalizedBoost_in_connected_component_of_id u v)).mp
id_isOrthochronousd:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ generalizedBoost u v ∈ { carrier := {Λ | IsProper Λ ∧ IsOrthochronous Λ}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ IsProper (generalizedBoost u v)d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ IsOrthochronous (generalizedBoost u v)
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ IsProper (generalizedBoost u v) All goals completed! 🐙
d:ℕu:↑(Velocity d)v:↑(Velocity d)⊢ IsOrthochronous (generalizedBoost u v) All goals completed! 🐙d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ generalizedBoost v u • generalizedBoost u v • p = 1 • p
d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ p + (2 * (minkowskiProduct p) ↑u) • ↑v -
(((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v)) • (↑u + ↑v) +
(2 *
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1))) •
↑u -
(((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1) +
((minkowskiProduct p) ↑u + 2 * (minkowskiProduct p) ↑u * (minkowskiProduct ↑u) ↑v -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
(1 + (minkowskiProduct ↑u) ↑v))) /
(1 + (minkowskiProduct ↑u) ↑v)) •
(↑v + ↑u) =
p
d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 1 = 1d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1 -
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1) +
((minkowskiProduct p) ↑u + 2 * (minkowskiProduct p) ↑u * (minkowskiProduct ↑u) ↑v -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
(1 + (minkowskiProduct ↑u) ↑v))) /
(1 + (minkowskiProduct ↑u) ↑v) *
1 =
0d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ -(((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1) +
2 *
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1)) *
1 -
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1) +
((minkowskiProduct p) ↑u + 2 * (minkowskiProduct p) ↑u * (minkowskiProduct ↑u) ↑v -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
(1 + (minkowskiProduct ↑u) ↑v))) /
(1 + (minkowskiProduct ↑u) ↑v) *
1 =
0 d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 1 = 1d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1 -
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1) +
((minkowskiProduct p) ↑u + 2 * (minkowskiProduct p) ↑u * (minkowskiProduct ↑u) ↑v -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
(1 + (minkowskiProduct ↑u) ↑v))) /
(1 + (minkowskiProduct ↑u) ↑v) *
1 =
0d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ -(((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) * 1) +
2 *
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1)) *
1 -
((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u * 1 -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct ↑u) ↑v + 1) +
((minkowskiProduct p) ↑u + 2 * (minkowskiProduct p) ↑u * (minkowskiProduct ↑u) ↑v -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) / (1 + (minkowskiProduct ↑u) ↑v) *
(1 + (minkowskiProduct ↑u) ↑v))) /
(1 + (minkowskiProduct ↑u) ↑v) *
1 =
0 d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (1 + (minkowskiProduct ↑u) ↑v) *
(-((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) +
2 *
((1 + (minkowskiProduct ↑u) ↑v) * ((minkowskiProduct p) ↑v + (minkowskiProduct p) ↑u * 2) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) * ((minkowskiProduct ↑u) ↑v + 1))) -
((1 + (minkowskiProduct ↑u) ↑v) * ((minkowskiProduct p) ↑v + (minkowskiProduct p) ↑u * 2) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) * ((minkowskiProduct ↑u) ↑v + 1) +
(1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct p) ↑u * (1 + (minkowskiProduct ↑u) ↑v * 2) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v))) =
(1 + (minkowskiProduct ↑u) ↑v) ^ 2 * 0 d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (1 + (minkowskiProduct ↑u) ↑v) *
(2 * (minkowskiProduct p) ↑u * (1 + (minkowskiProduct ↑u) ↑v) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v)) -
((1 + (minkowskiProduct ↑u) ↑v) * ((minkowskiProduct p) ↑v + 2 * (minkowskiProduct p) ↑u) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) * ((minkowskiProduct ↑u) ↑v + 1) +
(1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct p) ↑u * (1 + 2 * (minkowskiProduct ↑u) ↑v) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v))) =
(1 + (minkowskiProduct ↑u) ↑v) ^ 2 * 0d:ℕu:↑(Velocity d)v:↑(Velocity d)p:Lorentz.Vector dh1:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ (1 + (minkowskiProduct ↑u) ↑v) *
(-((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) +
2 *
((1 + (minkowskiProduct ↑u) ↑v) * ((minkowskiProduct p) ↑v + (minkowskiProduct p) ↑u * 2) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) * ((minkowskiProduct ↑u) ↑v + 1))) -
((1 + (minkowskiProduct ↑u) ↑v) * ((minkowskiProduct p) ↑v + (minkowskiProduct p) ↑u * 2) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v) * ((minkowskiProduct ↑u) ↑v + 1) +
(1 + (minkowskiProduct ↑u) ↑v) *
((minkowskiProduct p) ↑u * (1 + (minkowskiProduct ↑u) ↑v * 2) -
((minkowskiProduct p) ↑u + (minkowskiProduct p) ↑v))) =
(1 + (minkowskiProduct ↑u) ↑v) ^ 2 * 0 All goals completed! 🐙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-Physlib/topic/Lorentz.20group/near/523249684
d:ℕu:↑(Velocity d)v:↑(Velocity d)h:1 + (minkowskiProduct ↑u) ↑v ≠ 0⊢ 1 + 2 * 1 * ↑u (Sum.inl 0) * ↑v (Sum.inl 0) -
(↑u (Sum.inl 0) + ↑v (Sum.inl 0)) * (↑u (Sum.inl 0) + ↑v (Sum.inl 0)) / (1 + (minkowskiProduct ↑u) ↑v) =
1 +
(((↑u).timeComponent * ‖(↑v).spatialPart‖) ^ 2 -
2 * ((↑u).timeComponent * ((↑v).timeComponent * inner ℝ (↑v).spatialPart (↑u).spatialPart)) +
((↑v).timeComponent * ‖(↑u).spatialPart‖) ^ 2) /
(1 + (minkowskiProduct ↑u) ↑v)
d:ℕu:↑(Velocity d)v:↑(Velocity d)h:1 + (↑u (Sum.inl 0) * ↑v (Sum.inl 0) - inner ℝ (↑u).spatialPart (↑v).spatialPart) ≠ 0⊢ 1 + 2 * 1 * ↑u (Sum.inl 0) * ↑v (Sum.inl 0) -
(↑u (Sum.inl 0) + ↑v (Sum.inl 0)) * (↑u (Sum.inl 0) + ↑v (Sum.inl 0)) /
(1 + (↑u (Sum.inl 0) * ↑v (Sum.inl 0) - inner ℝ (↑u).spatialPart (↑v).spatialPart)) =
1 +
((↑u (Sum.inl 0) * ‖(↑v).spatialPart‖) ^ 2 -
2 * (↑u (Sum.inl 0) * (↑v (Sum.inl 0) * inner ℝ (↑v).spatialPart (↑u).spatialPart)) +
(↑v (Sum.inl 0) * ‖(↑u).spatialPart‖) ^ 2) /
(1 + (↑u (Sum.inl 0) * ↑v (Sum.inl 0) - inner ℝ (↑u).spatialPart (↑v).spatialPart))
d:ℕu:↑(Velocity d)v:↑(Velocity d)h:1 + (↑u (Sum.inl 0) * ↑v (Sum.inl 0) - inner ℝ (↑u).spatialPart (↑v).spatialPart) ≠ 0⊢ (1 + 2 * ↑u (Sum.inl 0) * ↑v (Sum.inl 0)) *
(1 + (↑u (Sum.inl 0) * ↑v (Sum.inl 0) - inner ℝ (↑u).spatialPart (↑v).spatialPart)) -
(↑u (Sum.inl 0) + ↑v (Sum.inl 0)) ^ 2 =
1 + (↑u (Sum.inl 0) * ↑v (Sum.inl 0) - inner ℝ (↑u).spatialPart (↑v).spatialPart) +
(↑u (Sum.inl 0) *
(↑u (Sum.inl 0) * ‖(↑v).spatialPart‖ ^ 2 - 2 * ↑v (Sum.inl 0) * inner ℝ (↑v).spatialPart (↑u).spatialPart) +
↑v (Sum.inl 0) ^ 2 * ‖(↑u).spatialPart‖ ^ 2)
All goals completed! 🐙