Minkowski product on Lorentz vectors

In this module we define and create an API around the Minkowski product on Lorentz vectors.

The minkowskiProduct

def Lorentz.Vector.minkowskiProductMap {d : ℕ} (p q : Vector d) : ℝ

The Minkowski product of Lorentz vectors in the +--- convention..

Equations

• One or more equations did not get rendered due to their size.

theorem Lorentz.Vector.minkowskiProductMap_toCoord {d : ℕ} (p q : Vector d) : p.minkowskiProductMap q = p (Sum.inl 0) * q (Sum.inl 0) - ∑ i : Fin d, p (Sum.inr i) * q (Sum.inr i)

theorem Lorentz.Vector.minkowskiProductMap_symm {d : ℕ} (p q : Vector d) : p.minkowskiProductMap q = q.minkowskiProductMap p

@[simp]

theorem Lorentz.Vector.minkowskiProductMap_add_fst {d : ℕ} (p q r : Vector d) : (p + q).minkowskiProductMap r = p.minkowskiProductMap r + q.minkowskiProductMap r

@[simp]

theorem Lorentz.Vector.minkowskiProductMap_add_snd {d : ℕ} (p q r : Vector d) : p.minkowskiProductMap (q + r) = p.minkowskiProductMap q + p.minkowskiProductMap r

@[simp]

theorem Lorentz.Vector.minkowskiProductMap_smul_fst {d : ℕ} (c : ℝ) (p q : Vector d) : (c • p).minkowskiProductMap q = c * p.minkowskiProductMap q

@[simp]

theorem Lorentz.Vector.minkowskiProductMap_smul_snd {d : ℕ} (c : ℝ) (p q : Vector d) : p.minkowskiProductMap (c • q) = c * p.minkowskiProductMap q

def Lorentz.Vector.minkowskiProduct {d : ℕ} : Vector d →ₗ[ℝ] Vector d →ₗ[ℝ] ℝ

The Minkowski product of two Lorentz vectors as a linear map.

Equations

• One or more equations did not get rendered due to their size.

def Lorentz.Vector.«term⟪_,_⟫ₘ» : Lean.ParserDescr

The Minkowski product of two Lorentz vectors as a linear map.

Equations

• One or more equations did not get rendered due to their size.

theorem Lorentz.Vector.minkowskiProduct_apply {d : ℕ} (p q : Vector d) : (minkowskiProduct p) q = p.minkowskiProductMap q

theorem Lorentz.Vector.minkowskiProduct_symm {d : ℕ} (p q : Vector d) : (minkowskiProduct p) q = (minkowskiProduct q) p

theorem Lorentz.Vector.minkowskiProduct_toCoord {d : ℕ} (p q : Vector d) : (minkowskiProduct p) q = p (Sum.inl 0) * q (Sum.inl 0) - ∑ i : Fin d, p (Sum.inr i) * q (Sum.inr i)

theorem Lorentz.Vector.minkowskiProduct_toCoord_minkowskiMatrix {d : ℕ} (p q : Vector d) : (minkowskiProduct p) q = ∑ μ : Fin 1 ⊕ Fin d, minkowskiMatrix μ μ * p μ * q μ

@[simp]

theorem Lorentz.Vector.minkowskiProduct_invariant {d : ℕ} (p q : Vector d) (Λ : ↑(LorentzGroup d)) : (minkowskiProduct (Λ • p)) (Λ • q) = (minkowskiProduct p) q

theorem Lorentz.Vector.minkowskiProduct_eq_timeComponent_spatialPart {d : ℕ} (p q : Vector d) : (minkowskiProduct p) q = p.timeComponent * q.timeComponent - inner ℝ p.spatialPart q.spatialPart

theorem Lorentz.Vector.minkowskiProduct_self_eq_timeComponent_spatialPart {d : ℕ} (p : Vector d) : (minkowskiProduct p) p = ‖p.timeComponent‖ ^ 2 - ‖p.spatialPart‖ ^ 2

theorem Lorentz.Vector.minkowskiProduct_self_le_timeComponent_sq {d : ℕ} (p : Vector d) : (minkowskiProduct p) p ≤ p.timeComponent ^ 2

@[simp]

theorem Lorentz.Vector.minkowskiProduct_basis_left {d : ℕ} (μ : Fin 1 ⊕ Fin d) (p : Vector d) : (minkowskiProduct (basis μ)) p = minkowskiMatrix μ μ * p μ

@[simp]

theorem Lorentz.Vector.minkowskiProduct_basis_right {d : ℕ} (μ : Fin 1 ⊕ Fin d) (p : Vector d) : (minkowskiProduct p) (basis μ) = minkowskiMatrix μ μ * p μ

@[simp]

theorem Lorentz.Vector.minkowskiProduct_eq_zero_forall_iff {d : ℕ} (p : Vector d) : (∀ (q : Vector d), (minkowskiProduct p) q = 0) ↔ p = 0

The adjoint of a linear map

theorem Lorentz.Vector.map_minkowskiProduct_eq_self_forall_iff {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : (∀ (p q : Vector d), (minkowskiProduct (f p)) q = (minkowskiProduct p) q) ↔ f = LinearMap.id

def Lorentz.Vector.adjoint {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : Vector d →ₗ[ℝ] Vector d

The adjoint of a linear map from Vector d to itself with respect to the minkowskiProduct.

Equations

• Lorentz.Vector.adjoint f = (LinearMap.toMatrix Lorentz.Vector.basis Lorentz.Vector.basis).symm (minkowskiMatrix.dual ((LinearMap.toMatrix Lorentz.Vector.basis Lorentz.Vector.basis) f))

theorem Lorentz.Vector.map_minkowskiProduct_eq_adjoint {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p q : Vector d) : (minkowskiProduct (f p)) q = (minkowskiProduct p) ((adjoint f) q)

theorem Lorentz.Vector.minkowskiProduct_map_eq_adjoint {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p q : Vector d) : (minkowskiProduct p) (f q) = (minkowskiProduct ((adjoint f) p)) q

The property IsLorentz of linear maps

def Lorentz.Vector.IsLorentz {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : Prop

A linear map Vector d →ₗ[ℝ] Vector d satsfies IsLorentz if it preserves the minkowski product.

Equations

• Lorentz.Vector.IsLorentz f = ∀ (p q : Lorentz.Vector d), (Lorentz.Vector.minkowskiProduct (f p)) (f q) = (Lorentz.Vector.minkowskiProduct p) q

theorem Lorentz.Vector.isLorentz_iff {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : IsLorentz f ↔ ∀ (p q : Vector d), (minkowskiProduct (f p)) (f q) = (minkowskiProduct p) q

theorem Lorentz.Vector.isLorentz_iff_basis {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : IsLorentz f ↔ ∀ (μ ν : Fin 1 ⊕ Fin d), (minkowskiProduct (f (basis μ))) (f (basis ν)) = (minkowskiProduct (basis μ)) (basis ν)

theorem Lorentz.Vector.isLorentz_iff_comp_adjoint_eq_id {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : IsLorentz f ↔ adjoint f ∘ₗ f = LinearMap.id

theorem Lorentz.Vector.isLorentz_iff_toMatrix_mem_lorentzGroup {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : IsLorentz f ↔ (LinearMap.toMatrix basis basis) f ∈ LorentzGroup d