1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. Vector
  6. Basic
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Geometry.Manifold.IsManifold.Basic

Lorentz Vectors

In this module we define Lorentz vectors as real Lorentz tensors with a single up index. We create an API around Lorentz vectors to make working with them as easy as possible.

@[expose] public section

Real contravariant Lorentz vector.

def Vector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ
instance {d} : AddCommMonoid (Vector d) := inferInstanceAs (AddCommMonoid (Fin 1 ⊕ Fin d → ℝ))instance {d} : Module ℝ (Vector d) := inferInstanceAs (Module ℝ (Fin 1 ⊕ Fin d → ℝ))instance {d} : AddCommGroup (Vector d) := inferInstanceAs (AddCommGroup (Fin 1 ⊕ Fin d → ℝ))instance {d} : FiniteDimensional ℝ (Vector d) := inferInstanceAs (FiniteDimensional ℝ (Fin 1 ⊕ Fin d → ℝ))

The equivalence between Vector d and EuclideanSpace ℝ (Fin 1 ⊕ Fin d).

def equivEuclid (d : ℕ) : Vector d ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1 ⊕ Fin d) := (WithLp.linearEquiv _ _ _).symm
@[simp] lemma equivEuclid_apply (d : ℕ) (v : Vector d) (i : Fin 1 ⊕ Fin d) : equivEuclid d v i = v i := rfl@[ext] lemma eq_of_apply_eq {d : ℕ} {v w : Vector d} (h : ∀ i, v i = w i) : v = w := d:ℕv:Vector dw:Vector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w i⊢ v = w d:ℕv:Vector dw:Vector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w i⊢ (equivEuclid d) v = (equivEuclid d) w d:ℕv:Vector dw:Vector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w ii:Fin 1 ⊕ Fin d⊢ ((equivEuclid d) v).ofLp i = ((equivEuclid d) w).ofLp i All goals completed! 🐙instance (d : ℕ) : Norm (Vector d) where norm := fun v => ‖equivEuclid d v‖lemma norm_eq_equivEuclid (d : ℕ) (v : Vector d) : ‖v‖ = ‖equivEuclid d v‖ := rfl@[simp] lemma abs_component_le_norm {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : |v i| ≤ ‖v‖ := d:ℕv:Vector di:Fin 1 ⊕ Fin d⊢ |v i| ≤ ‖v‖ d:ℕv:Vector di:Fin 1 ⊕ Fin d⊢ |v i| ≤ √(∑ x, v x ^ 2) d:ℕv:Vector di:Fin 1 ⊕ Fin d⊢ v i ^ 2 ≤ ∑ x, v x ^ 2 d:ℕv:Vector di:Fin 1 ⊕ Fin d⊢ v i ^ 2 ≤ ∑ j ∈ {i}, v j ^ 2d:ℕv:Vector di:Fin 1 ⊕ Fin d⊢ ∑ j ∈ {i}, v j ^ 2 ≤ ∑ x, v x ^ 2 d:ℕv:Vector di:Fin 1 ⊕ Fin d⊢ v i ^ 2 ≤ ∑ j ∈ {i}, v j ^ 2 All goals completed! 🐙 refine Finset.sum_le_univ_sum_of_nonneg (fun i => d:ℕv:Vector di✝:Fin 1 ⊕ Fin di:Fin 1 ⊕ Fin d⊢ 0 ≤ v i ^ 2 All goals completed! 🐙)All goals completed! 🐙instance isNormedSpace (d : ℕ) : NormedSpace ℝ (Vector d) where norm_smul_le c v := d:ℕc:ℝv:Vector d⊢ ‖c • v‖ ≤ ‖c‖ * ‖v‖ d:ℕc:ℝv:Vector d⊢ ‖c • (equivEuclid d) v‖ ≤ ‖c‖ * ‖(equivEuclid d) v‖ All goals completed! 🐙instance (d : ℕ) : Inner ℝ (Vector d) where inner := fun v w => ⟪equivEuclid d v, equivEuclid d w⟫_ℝlemma inner_eq_equivEuclid (d : ℕ) (v w : Vector d) : ⟪v, w⟫_ℝ = ⟪equivEuclid d v, equivEuclid d w⟫_ℝ := rfl

The Euclidean inner product structure on CoVector.

instance innerProductSpace (d : ℕ) : InnerProductSpace ℝ (Vector d) where norm_sq_eq_re_inner v := d:ℕv:Vector d⊢ ‖v‖ ^ 2 = RCLike.re ⟪v, v⟫_ℝ d:ℕv:Vector d⊢ ‖(equivEuclid d) v‖ ^ 2 = RCLike.re ⟪(equivEuclid d) v, (equivEuclid d) v⟫_ℝ All goals completed! 🐙 conj_inner_symm x y := d:ℕx:Vector dy:Vector d⊢ (starRingEnd ℝ) ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ d:ℕx:Vector dy:Vector d⊢ (starRingEnd ℝ) ⟪(equivEuclid d) y, (equivEuclid d) x⟫_ℝ = ⟪(equivEuclid d) x, (equivEuclid d) y⟫_ℝ All goals completed! 🐙 add_left x y z := d:ℕx:Vector dy:Vector dz:Vector d⊢ ⟪x + y, z⟫_ℝ = ⟪x, z⟫_ℝ + ⟪y, z⟫_ℝ d:ℕx:Vector dy:Vector dz:Vector d⊢ ⟪(equivEuclid d) x + (equivEuclid d) y, (equivEuclid d) z⟫_ℝ = ⟪(equivEuclid d) x, (equivEuclid d) z⟫_ℝ + ⟪(equivEuclid d) y, (equivEuclid d) z⟫_ℝ All goals completed! 🐙 smul_left x y r := d:ℕx:Vector dy:Vector dr:ℝ⊢ ⟪r • x, y⟫_ℝ = (starRingEnd ℝ) r * ⟪x, y⟫_ℝ d:ℕx:Vector dy:Vector dr:ℝ⊢ ⟪r • (equivEuclid d) x, (equivEuclid d) y⟫_ℝ = (starRingEnd ℝ) r * ⟪(equivEuclid d) x, (equivEuclid d) y⟫_ℝ All goals completed! 🐙

The instance of a ChartedSpace on Vector d.

instance : ChartedSpace (Vector d) (Vector d) := chartedSpaceSelf (Vector d)
instance {d} : CoeFun (Vector d) (fun _ => Fin 1 ⊕ Fin d → ℝ) where coe := fun v => vlemma ext_of_apply {d} {v w : Vector d} (h : ∀ i, v i = w i) : v = w := d:ℕv:Vector dw:Vector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w i⊢ v = w d:ℕv:Vector dw:Vector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w i⊢ (equivEuclid d) v = (equivEuclid d) w d:ℕv:Vector dw:Vector dh:∀ (i : Fin 1 ⊕ Fin d), v i = w ii:Fin 1 ⊕ Fin d⊢ ((equivEuclid d) v).ofLp i = ((equivEuclid d) w).ofLp i All goals completed! 🐙@[simp] lemma apply_smul {d : ℕ} (c : ℝ) (v : Vector d) (i : Fin 1 ⊕ Fin d) : (c • v) i = c * v i := rfl@[simp] lemma apply_add {d : ℕ} (v w : Vector d) (i : Fin 1 ⊕ Fin d) : (v + w) i = v i + w i := rfl@[simp] lemma apply_sub {d : ℕ} (v w : Vector d) (i : Fin 1 ⊕ Fin d) : (v - w) i = v i - w i := d:ℕv:Vector dw:Vector di:Fin 1 ⊕ Fin d⊢ (v - w) i = v i - w i All goals completed! 🐙All goals completed! 🐙@[simp] lemma neg_apply {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : (-v) i = - v i := rfl@[simp] lemma zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) : (0 : Vector d) i = 0 := rfl

The continuous linear map from a Lorentz vector to one of its coordinates.

def coordCLM {d : ℕ} (i : Fin 1 ⊕ Fin d) : Vector d →L[ℝ] ℝ := LinearMap.toContinuousLinearMap { toFun v := v i map_add' := d:ℕi:Fin 1 ⊕ Fin d⊢ ∀ (x y : Vector d), (x + y) i = x i + y i All goals completed! 🐙 map_smul' := d:ℕi:Fin 1 ⊕ Fin d⊢ ∀ (m : ℝ) (x : Vector d), (m • x) i = (RingHom.id ℝ) m • x i All goals completed! 🐙}
lemma coordCLM_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) (v : Vector d) : coordCLM i v = v i := rfl@[fun_prop] lemma coord_continuous {d : ℕ} (i : Fin 1 ⊕ Fin d) : Continuous (fun v : Vector d => v i) := (coordCLM i).continuous@[fun_prop] lemma coord_contDiff {n} {d : ℕ} (i : Fin 1 ⊕ Fin d) : ContDiff ℝ n (fun v : Vector d => v i) := (coordCLM i).contDiff@[fun_prop] lemma coord_differentiable {d : ℕ} (i : Fin 1 ⊕ Fin d) : Differentiable ℝ (fun v : Vector d => v i) := (coordCLM i).differentiable@[fun_prop] lemma coord_differentiableAt {d : ℕ} (i : Fin 1 ⊕ Fin d) (v : Vector d) : DifferentiableAt ℝ (fun v : Vector d => v i) v := (coordCLM i).differentiableAt

The continuous linear equivalence between Vector d and Euclidean space.

def euclidCLE (d : ℕ) : Vector d ≃L[ℝ] EuclideanSpace ℝ (Fin 1 ⊕ Fin d) := LinearEquiv.toContinuousLinearEquiv (equivEuclid d)

The continuous linear equivalence between Vector d and the corresponding Pi type.

def equivPi (d : ℕ) : Vector d ≃L[ℝ] Π (_ : Fin 1 ⊕ Fin d), ℝ := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl _ _)
@[simp] lemma equivPi_apply {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : equivPi d v i = v i := rfld:ℕα:Type u_1inst✝:TopologicalSpace αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), Continuous fun x => f x i⊢ Continuous (⇑(equivPi d) ∘ f) d:ℕα:Type u_1inst✝:TopologicalSpace αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), Continuous fun x => f x i⊢ ∀ (i : Fin 1 ⊕ Fin d), Continuous fun a => (⇑(equivPi d) ∘ f) a i d:ℕα:Type u_1inst✝:TopologicalSpace αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), Continuous fun x => f x ii:Fin 1 ⊕ Fin d⊢ Continuous fun a => (⇑(equivPi d) ∘ f) a i d:ℕα:Type u_1inst✝:TopologicalSpace αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), Continuous fun x => f x ii:Fin 1 ⊕ Fin d⊢ Continuous fun a => f a i All goals completed! 🐙d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => f x i⊢ Differentiable ℝ (⇑(equivPi d) ∘ f) All goals completed! 🐙 d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector d⊢ Differentiable ℝ f → ∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => f x i d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ fun x => f x ν d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ (⇑(coordCLM ν) ∘ f) d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ ⇑(coordCLM ν)d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ f d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ ⇑(coordCLM ν) All goals completed! 🐙 d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fν:Fin 1 ⊕ Fin d⊢ Differentiable ℝ f All goals completed! 🐙n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => f x i⊢ ContDiff ℝ n (⇑(equivPi d) ∘ f) n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => f x i⊢ ∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => (⇑(equivPi d) ∘ f) x i n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => f x iν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => (⇑(equivPi d) ∘ f) x ν All goals completed! 🐙 n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector d⊢ ContDiff ℝ n f → ∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => f x i n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:ContDiff ℝ n fν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => f x ν n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:ContDiff ℝ n fν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n (⇑(coordCLM ν) ∘ f) n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:ContDiff ℝ n fν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n ⇑(coordCLM ν)n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:ContDiff ℝ n fν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n f n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:ContDiff ℝ n fν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n ⇑(coordCLM ν) All goals completed! 🐙 n:WithTop ℕ∞d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:ContDiff ℝ n fν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n f All goals completed! 🐙d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fx:αdt:αν:Fin 1 ⊕ Fin d⊢ (fderiv ℝ f x) dt ν = (fderiv ℝ (⇑(coordCLM ν)) (f x) ∘SL fderiv ℝ f x) dt d:ℕα:Type u_1inst✝¹:NormedAddCommGroup αinst✝:NormedSpace ℝ αf:α → Vector dh:Differentiable ℝ fx:αdt:αν:Fin 1 ⊕ Fin d⊢ (fderiv ℝ f x) dt ν = (coordCLM ν) ((fderiv ℝ f x) dt) All goals completed! 🐙@[simp] lemma fderiv_coord {d : ℕ} (μ : Fin 1 ⊕ Fin d) (x : Vector d) : fderiv ℝ (fun v : Vector d => v μ) x = coordCLM μ := d:ℕμ:Fin 1 ⊕ Fin dx:Vector d⊢ fderiv ℝ (fun v => v μ) x = coordCLM μ d:ℕμ:Fin 1 ⊕ Fin dx:Vector d⊢ fderiv ℝ (⇑(coordCLM μ)) x = coordCLM μ All goals completed! 🐙

Basis

The basis on Vector d indexed by Fin 1 ⊕ Fin d.

def basis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (Vector d) := Pi.basisFun ℝ _
@[simp] lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : basis μ ν = if μ = ν then 1 else 0 := d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ basis μ ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (Pi.basisFun ℝ (Fin 1 ⊕ Fin d)) μ ν = if μ = ν then 1 else 0 erw [d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Pi.single μ 1 ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (if ν = μ then 1 else 0) = if μ = ν then 1 else 0d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (if ν = μ then 1 else 0) = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (ν = μ) = (μ = ν) All goals completed! 🐙lemma basis_repr_apply {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) : basis.repr p μ = p μ := d:ℕp:Vector dμ:Fin 1 ⊕ Fin d⊢ (basis.repr p) μ = p μ d:ℕp:Vector dμ:Fin 1 ⊕ Fin d⊢ ((Pi.basisFun ℝ (Fin 1 ⊕ Fin d)).repr p) μ = p μ erw [d:ℕp:Vector dμ:Fin 1 ⊕ Fin d⊢ p μ = p μAll goals completed! 🐙lemma map_apply_eq_basis_mulVec {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p : Vector d) : (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := d:ℕf:Vector d →ₗ[ℝ] Vector dp:Vector d⊢ f p = (LinearMap.toMatrix basis basis) f *ᵥ p All goals completed! 🐙lemma sum_basis_eq_zero_iff {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) : (∑ μ, f μ • basis μ) = 0 ↔ ∀ μ, f μ = 0 := d:ℕf:Fin 1 ⊕ Fin d → ℝ⊢ ∑ μ, f μ • basis μ = 0 ↔ ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0 d:ℕf:Fin 1 ⊕ Fin d → ℝ⊢ ∑ μ, f μ • basis μ = 0 → ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0d:ℕf:Fin 1 ⊕ Fin d → ℝ⊢ (∀ (μ : Fin 1 ⊕ Fin d), f μ = 0) → ∑ μ, f μ • basis μ = 0 d:ℕf:Fin 1 ⊕ Fin d → ℝ⊢ ∑ μ, f μ • basis μ = 0 → ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0 d:ℕf:Fin 1 ⊕ Fin d → ℝh:∑ μ, f μ • basis μ = 0⊢ ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0 d:ℕf:Fin 1 ⊕ Fin d → ℝh:∑ μ, f μ • basis μ = 0h1:∀ i ∈ Finset.univ, f i = 0⊢ ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0 d:ℕf:Fin 1 ⊕ Fin d → ℝh:∑ μ, f μ • basis μ = 0h1:∀ i ∈ Finset.univ, f i = 0μ:Fin 1 ⊕ Fin d⊢ f μ = 0 exact h1 μ (d:ℕf:Fin 1 ⊕ Fin d → ℝh:∑ μ, f μ • basis μ = 0h1:∀ i ∈ Finset.univ, f i = 0μ:Fin 1 ⊕ Fin d⊢ μ ∈ Finset.univ All goals completed! 🐙) d:ℕf:Fin 1 ⊕ Fin d → ℝ⊢ (∀ (μ : Fin 1 ⊕ Fin d), f μ = 0) → ∑ μ, f μ • basis μ = 0 d:ℕf:Fin 1 ⊕ Fin d → ℝh:∀ (μ : Fin 1 ⊕ Fin d), f μ = 0⊢ ∑ μ, f μ • basis μ = 0 All goals completed! 🐙d:ℕf₀:ℝf:Fin d → ℝf':Fin 1 ⊕ Fin d → ℝ := fun μ => match μ with | Sum.inl 0 => f₀ | Sum.inr i => f ih1:f₀ • basis (Sum.inl 0) + ∑ i, f i • basis (Sum.inr i) = ∑ μ, f' μ • basis μ⊢ (∀ (μ : Fin 1 ⊕ Fin d), f' μ = 0) ↔ f₀ = 0 ∧ ∀ (i : Fin d), f i = 0 All goals completed! 🐙

C. The Spatial part

Extract spatial components from a Lorentz vector, returning them as a vector in Euclidean space.

abbrev spatialPart {d : ℕ} (v : Vector d) : EuclideanSpace ℝ (Fin d) := WithLp.toLp 2 fun i => v (Sum.inr i)
lemma spatialPart_apply_eq_toCoord {d : ℕ} (v : Vector d) (i : Fin d) : spatialPart v i = v (Sum.inr i) := rfld:ℕi:Fin dj:Fin d⊢ (if i = j then 1 else 0) = if Sum.inr i = Sum.inr j then 1 else 0 All goals completed! 🐙lemma spatialPart_basis_sum_inl {d : ℕ} (i : Fin d) : spatialPart (basis (Sum.inl 0)) i = 0 := d:ℕi:Fin d⊢ (basis (Sum.inl 0)).spatialPart.ofLp i = 0 All goals completed! 🐙

The spatial part of a Lorentz vector as a continuous linear map.

def spatialCLM (d : ℕ) : Vector d →L[ℝ] EuclideanSpace ℝ (Fin d) where toFun v := WithLp.toLp 2 fun i => v (Sum.inr i) map_add' v1 v2 := d:ℕv1:Vector dv2:Vector d⊢ (WithLp.toLp 2 fun i => (v1 + v2) (Sum.inr i)) = (WithLp.toLp 2 fun i => v1 (Sum.inr i)) + WithLp.toLp 2 fun i => v2 (Sum.inr i) All goals completed! 🐙 map_smul' c v := d:ℕc:ℝv:Vector d⊢ (WithLp.toLp 2 fun i => (c • v) (Sum.inr i)) = (RingHom.id ℝ) c • WithLp.toLp 2 fun i => v (Sum.inr i) All goals completed! 🐙 cont := d:ℕ⊢ Continuous fun v => WithLp.toLp 2 fun i => v (Sum.inr i) All goals completed! 🐙
lemma spatialCLM_apply_eq_spatialPart {d : ℕ} (v : Vector d) (i : Fin d) : spatialCLM d v i = spatialPart v i := rfl@[simp] lemma spatialCLM_basis_sum_inl {d : ℕ} : spatialCLM d (basis (Sum.inl 0)) = 0 := d:ℕ⊢ (spatialCLM d) (basis (Sum.inl 0)) = 0 d:ℕi:Fin d⊢ ((spatialCLM d) (basis (Sum.inl 0))).ofLp i = WithLp.ofLp 0 i All goals completed! 🐙d:ℕi:Fin dj:Fin d⊢ (Finsupp.single (Sum.inr i) 1) (Sum.inr j) = ((EuclideanSpace.basisFun (Fin d) ℝ) i).ofLp j d:ℕi:Fin dj:Fin d⊢ (if i = j then 1 else 0) = if j = i then 1 else 0 d:ℕi:Fin dj:Fin d⊢ (i = j) = (j = i) All goals completed! 🐙

The Temporal component

Extract time component from a Lorentz vector

abbrev timeComponent {d : ℕ} (v : Vector d) : ℝ := v (Sum.inl 0)
lemma timeComponent_basis_sum_inr {d : ℕ} (i : Fin d) : timeComponent (basis (Sum.inr i)) = 0 := d:ℕi:Fin d⊢ (basis (Sum.inr i)).timeComponent = 0 All goals completed! 🐙lemma timeComponent_basis_sum_inl {d : ℕ} : timeComponent (d := d) (basis (Sum.inl 0)) = 1 := d:ℕ⊢ (basis (Sum.inl 0)).timeComponent = 1 All goals completed! 🐙

The temporal part of a Lorentz vector as a continuous linear map.

def temporalCLM (d : ℕ) : Vector d →L[ℝ] ℝ := LinearMap.toContinuousLinearMap { toFun := fun v => v (Sum.inl 0) map_add' := d:ℕ⊢ ∀ (x y : Vector d), (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) All goals completed! 🐙 map_smul' := d:ℕ⊢ ∀ (m : ℝ) (x : Vector d), (m • x) (Sum.inl 0) = (RingHom.id ℝ) m • x (Sum.inl 0) All goals completed! 🐙}
lemma temporalCLM_apply_eq_timeComponent {d : ℕ} (v : Vector d) : temporalCLM d v = timeComponent v := rfl@[simp] lemma temporalCLM_basis_sum_inr {d : ℕ} (i : Fin d) : temporalCLM d (basis (Sum.inr i)) = 0 := d:ℕi:Fin d⊢ (temporalCLM d) (basis (Sum.inr i)) = 0 All goals completed! 🐙@[simp] lemma temporalCLM_basis_sum_inl {d : ℕ} : temporalCLM d (basis (Sum.inl 0)) = 1 := d:ℕ⊢ (temporalCLM d) (basis (Sum.inl 0)) = 1 All goals completed! 🐙

The continuous linear map corresponding to the creation of a Lorentz Vector with only a non-zero temporal component.

def ofTemporalComponent {d : ℕ} : ℝ →L[ℝ] Vector d where toFun xt := xt • basis (Sum.inl 0) map_add' := d:ℕ⊢ ∀ (x y : ℝ), (x + y) • basis (Sum.inl 0) = x • basis (Sum.inl 0) + y • basis (Sum.inl 0) All goals completed! 🐙 map_smul' := d:ℕ⊢ ∀ (m x : ℝ), (m • x) • basis (Sum.inl 0) = (RingHom.id ℝ) m • x • basis (Sum.inl 0) All goals completed! 🐙

The continuous linear map corresponding to the creation of a Lorentz Vector with only non-zero spatial components.

def ofSpatialComponent {d : ℕ} : EuclideanSpace ℝ (Fin d) →L[ℝ] Vector d where toFun xs := ∑ i, xs i • basis (Sum.inr i) map_add' xs ys := d:ℕxs:EuclideanSpace ℝ (Fin d)ys:EuclideanSpace ℝ (Fin d)⊢ ∑ i, (xs + ys).ofLp i • basis (Sum.inr i) = ∑ i, xs.ofLp i • basis (Sum.inr i) + ∑ i, ys.ofLp i • basis (Sum.inr i) All goals completed! 🐙 map_smul' c xs := d:ℕc:ℝxs:EuclideanSpace ℝ (Fin d)⊢ ∑ i, (c • xs).ofLp i • basis (Sum.inr i) = (RingHom.id ℝ) c • ∑ i, xs.ofLp i • basis (Sum.inr i) All goals completed! 🐙

## Smoothness

Properties of the inner product (note not the Minkowski product)

d:ℕμ:Fin 1 ⊕ Fin dp:Vector d⊢ ∑ i, ⟪((equivEuclid d) (basis μ)).ofLp i, ((equivEuclid d) p).ofLp i⟫_ℝ = p μ All goals completed! 🐙d:ℕp:Vector dμ:Fin 1 ⊕ Fin d⊢ ∑ i, ⟪((equivEuclid d) p).ofLp i, ((equivEuclid d) (basis μ)).ofLp i⟫_ℝ = p μ All goals completed! 🐙