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.

def Lorentz.Vector (d : ℕ := 3) : Type

Real contravariant Lorentz vector.

Equations

• Lorentz.Vector d = (Fin 1 ⊕ Fin d → ℝ)

instance Lorentz.Vector.instAddCommMonoid {d : ℕ} : AddCommMonoid (Vector d)

Equations

• Lorentz.Vector.instAddCommMonoid = inferInstanceAs (AddCommMonoid (Fin 1 ⊕ Fin d → ℝ))

instance Lorentz.Vector.instModuleReal {d : ℕ} : Module ℝ (Vector d)

Equations

• Lorentz.Vector.instModuleReal = inferInstanceAs (Module ℝ (Fin 1 ⊕ Fin d → ℝ))

instance Lorentz.Vector.instAddCommGroup {d : ℕ} : AddCommGroup (Vector d)

Equations

• Lorentz.Vector.instAddCommGroup = inferInstanceAs (AddCommGroup (Fin 1 ⊕ Fin d → ℝ))

instance Lorentz.Vector.instFiniteDimensionalReal {d : ℕ} : FiniteDimensional ℝ (Vector d)

def Lorentz.Vector.equivEuclid (d : ℕ) : Vector d ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 1 ⊕ Fin d)

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

Equations

• Lorentz.Vector.equivEuclid d = (WithLp.linearEquiv 2 ℝ (Lorentz.Vector d)).symm

@[simp]

theorem Lorentz.Vector.equivEuclid_apply (d : ℕ) (v : Vector d) (i : Fin 1 ⊕ Fin d) : ((equivEuclid d) v).ofLp i = v i

instance Lorentz.Vector.instNorm (d : ℕ) : Norm (Vector d)

Equations

• Lorentz.Vector.instNorm d = { norm := fun (v : Lorentz.Vector d) => ‖(Lorentz.Vector.equivEuclid d) v‖ }

theorem Lorentz.Vector.norm_eq_equivEuclid (d : ℕ) (v : Vector d) : ‖v‖ = ‖(equivEuclid d) v‖

@[simp]

theorem Lorentz.Vector.abs_component_le_norm {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : |v i| ≤ ‖v‖

instance Lorentz.Vector.isNormedAddCommGroup (d : ℕ) : NormedAddCommGroup (Vector d)

Equations

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

instance Lorentz.Vector.isNormedSpace (d : ℕ) : NormedSpace ℝ (Vector d)

Equations

• Lorentz.Vector.isNormedSpace d = { toModule := Lorentz.Vector.instModuleReal, norm_smul_le := ⋯ }

instance Lorentz.Vector.instInnerReal (d : ℕ) : Inner ℝ (Vector d)

Equations

• Lorentz.Vector.instInnerReal d = { inner := fun (v w : Lorentz.Vector d) => inner ℝ ((Lorentz.Vector.equivEuclid d) v) ((Lorentz.Vector.equivEuclid d) w) }

theorem Lorentz.Vector.inner_eq_equivEuclid (d : ℕ) (v w : Vector d) : inner ℝ v w = inner ℝ ((equivEuclid d) v) ((equivEuclid d) w)

instance Lorentz.Vector.innerProductSpace (d : ℕ) : InnerProductSpace ℝ (Vector d)

The Euclidean inner product structure on CoVector.

Equations

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

instance Lorentz.Vector.instChartedSpace {d : ℕ} : ChartedSpace (Vector d) (Vector d)

The instance of a ChartedSpace on Vector d.

Equations

• Lorentz.Vector.instChartedSpace = chartedSpaceSelf (Lorentz.Vector d)

instance Lorentz.Vector.instCoeFunForallSumFinOfNatNatReal {d : ℕ} : CoeFun (Vector d) fun (x : Vector d) => Fin 1 ⊕ Fin d → ℝ

Equations

• Lorentz.Vector.instCoeFunForallSumFinOfNatNatReal = { coe := fun (v : Lorentz.Vector d) => v }

@[simp]

theorem Lorentz.Vector.apply_smul {d : ℕ} (c : ℝ) (v : Vector d) (i : Fin 1 ⊕ Fin d) : (c • v) i = c * v i

@[simp]

theorem Lorentz.Vector.apply_add {d : ℕ} (v w : Vector d) (i : Fin 1 ⊕ Fin d) : (v + w) i = v i + w i

@[simp]

theorem Lorentz.Vector.apply_sub {d : ℕ} (v w : Vector d) (i : Fin 1 ⊕ Fin d) : (v - w) i = v i - w i

theorem Lorentz.Vector.apply_sum {d : ℕ} {ι : Type} [Fintype ι] (f : ι → Vector d) (i : Fin 1 ⊕ Fin d) : (∑ j : ι, f j) i = ∑ j : ι, f j i

@[simp]

theorem Lorentz.Vector.neg_apply {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : (-v) i = -v i

@[simp]

theorem Lorentz.Vector.zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) : 0 i = 0

def Lorentz.Vector.coordCLM {d : ℕ} (i : Fin 1 ⊕ Fin d) : Vector d →L[ℝ] ℝ

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

Equations

• Lorentz.Vector.coordCLM i = LinearMap.toContinuousLinearMap { toFun := fun (v : Lorentz.Vector d) => v i, map_add' := ⋯, map_smul' := ⋯ }

theorem Lorentz.Vector.coordCLM_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) (v : Vector d) : (coordCLM i) v = v i

theorem Lorentz.Vector.coord_continuous {d : ℕ} (i : Fin 1 ⊕ Fin d) : Continuous fun (v : Vector d) => v i

theorem Lorentz.Vector.coord_contDiff {n : WithTop ℕ∞} {d : ℕ} (i : Fin 1 ⊕ Fin d) : ContDiff ℝ n fun (v : Vector d) => v i

theorem Lorentz.Vector.coord_differentiable {d : ℕ} (i : Fin 1 ⊕ Fin d) : Differentiable ℝ fun (v : Vector d) => v i

theorem Lorentz.Vector.coord_differentiableAt {d : ℕ} (i : Fin 1 ⊕ Fin d) (v : Vector d) : DifferentiableAt ℝ (fun (v : Vector d) => v i) v

def Lorentz.Vector.euclidCLE (d : ℕ) : Vector d ≃L[ℝ] EuclideanSpace ℝ (Fin 1 ⊕ Fin d)

The continous linear equivalence between Vector d and Euclidean space.

Equations

• Lorentz.Vector.euclidCLE d = (Lorentz.Vector.equivEuclid d).toContinuousLinearEquiv

def Lorentz.Vector.equivPi (d : ℕ) : Vector d ≃L[ℝ] Fin 1 ⊕ Fin d → ℝ

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

Equations

• Lorentz.Vector.equivPi d = (LinearEquiv.refl ℝ (Lorentz.Vector d)).toContinuousLinearEquiv

@[simp]

theorem Lorentz.Vector.equivPi_apply {d : ℕ} (v : Vector d) (i : Fin 1 ⊕ Fin d) : (equivPi d) v i = v i

theorem Lorentz.Vector.continuous_of_apply {d : ℕ} {α : Type u_1} [TopologicalSpace α] (f : α → Vector d) (h : ∀ (i : Fin 1 ⊕ Fin d), Continuous fun (x : α) => f x i) : Continuous f

theorem Lorentz.Vector.differentiable_apply {d : ℕ} {α : Type u_1} [NormedAddCommGroup α] [NormedSpace ℝ α] (f : α → Vector d) : (∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun (x : α) => f x i) ↔ Differentiable ℝ f

theorem Lorentz.Vector.contDiff_apply {n : WithTop ℕ∞} {d : ℕ} {α : Type u_1} [NormedAddCommGroup α] [NormedSpace ℝ α] (f : α → Vector d) : (∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun (x : α) => f x i) ↔ ContDiff ℝ n f

theorem Lorentz.Vector.fderiv_apply {d : ℕ} {α : Type u_1} [NormedAddCommGroup α] [NormedSpace ℝ α] (f : α → Vector d) (h : Differentiable ℝ f) (x dt : α) (ν : Fin 1 ⊕ Fin d) : (fderiv ℝ f x) dt ν = (fderiv ℝ (fun (y : α) => f y ν) x) dt

@[simp]

theorem Lorentz.Vector.fderiv_coord {d : ℕ} (μ : Fin 1 ⊕ Fin d) (x : Vector d) : fderiv ℝ (fun (v : Vector d) => v μ) x = coordCLM μ

Tensorial

def Lorentz.Vector.indexEquiv {d : ℕ} : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up] ≃ Fin 1 ⊕ Fin d

The equivalence between the type of indices of a Lorentz vector and Fin 1 ⊕ Fin d.

Equations

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

instance Lorentz.Vector.tensorial {d : ℕ} : (realLorentzTensor d).Tensorial ![realLorentzTensor.Color.up] (Vector d)

Equations

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

theorem Lorentz.Vector.toTensor_symm_apply {d : ℕ} (p : (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up]) : TensorSpecies.Tensorial.toTensor.symm p = (Equiv.piCongrLeft' (fun (a : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up]) => ℝ) indexEquiv) (Finsupp.equivFunOnFinite ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr p))

theorem Lorentz.Vector.toTensor_symm_pure {d : ℕ} (p : TensorSpecies.Tensor.Pure (realLorentzTensor d) ![realLorentzTensor.Color.up]) (i : Fin 1 ⊕ Fin d) : TensorSpecies.Tensorial.toTensor.symm p.toTensor i = ((contrBasisFin d).repr (p 0)) (indexEquiv.symm i 0)

Basis

def Lorentz.Vector.basis {d : ℕ} : Module.Basis (Fin 1 ⊕ Fin d) ℝ (Vector d)

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

Equations

• Lorentz.Vector.basis = Pi.basisFun ℝ (Fin 1 ⊕ Fin d)

@[simp]

theorem Lorentz.Vector.basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : basis μ ν = if μ = ν then 1 else 0

theorem Lorentz.Vector.toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : TensorSpecies.Tensorial.toTensor.symm ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) (indexEquiv.symm μ)) = basis μ

theorem Lorentz.Vector.toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : TensorSpecies.Tensorial.toTensor (basis μ) = (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) (indexEquiv.symm μ)

theorem Lorentz.Vector.basis_eq_map_tensor_basis {d : ℕ} : basis = ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).map TensorSpecies.Tensorial.toTensor.symm).reindex indexEquiv

theorem Lorentz.Vector.tensor_basis_map_eq_basis_reindex {d : ℕ} : (TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).map TensorSpecies.Tensorial.toTensor.symm = basis.reindex indexEquiv.symm

theorem Lorentz.Vector.tensor_basis_repr_toTensor_apply {d : ℕ} (p : Vector d) (μ : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up]) : ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr (TensorSpecies.Tensorial.toTensor p)) μ = p (indexEquiv μ)

theorem Lorentz.Vector.basis_repr_apply {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) : (basis.repr p) μ = p μ

theorem Lorentz.Vector.map_apply_eq_basis_mulVec {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p : Vector d) : f p = ((LinearMap.toMatrix basis basis) f).mulVec p

theorem Lorentz.Vector.sum_basis_eq_zero_iff {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) : ∑ μ : Fin 1 ⊕ Fin d, f μ • basis μ = 0 ↔ ∀ (μ : Fin 1 ⊕ Fin d), f μ = 0

theorem Lorentz.Vector.sum_inl_inr_basis_eq_zero_iff {d : ℕ} (f₀ : ℝ) (f : Fin d → ℝ) : f₀ • basis (Sum.inl 0) + ∑ i : Fin d, f i • basis (Sum.inr i) = 0 ↔ f₀ = 0 ∧ ∀ (i : Fin d), f i = 0

The action of the Lorentz group

theorem Lorentz.Vector.smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : ↑(LorentzGroup d)) (p : Vector d) : (Λ • p) i = ∑ j : Fin 1 ⊕ Fin d, ↑Λ i j * p j

theorem Lorentz.Vector.smul_eq_mulVec {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : Λ • p = (↑Λ).mulVec p

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

@[simp]

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

theorem Lorentz.Vector.smul_zero {d : ℕ} (Λ : ↑(LorentzGroup d)) : Λ • 0 = 0

theorem Lorentz.Vector.smul_neg {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : Λ • -p = -(Λ • p)

theorem Lorentz.Vector.neg_smul {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : -Λ • p = -(Λ • p)

theorem LorentzGroup.eq_of_action_vector_eq {d : ℕ} {Λ Λ' : ↑(LorentzGroup d)} (h : ∀ (p : Lorentz.Vector d), Λ • p = Λ' • p) : Λ = Λ'

B. The continuous action of the Lorentz group

def Lorentz.Vector.actionCLM {d : ℕ} (Λ : ↑(LorentzGroup d)) : Vector d →L[ℝ] Vector d

The Lorentz action on vectors as a continuous linear map.

Equations

• Lorentz.Vector.actionCLM Λ = LinearMap.toContinuousLinearMap { toFun := fun (v : Lorentz.Vector d) => Λ • v, map_add' := ⋯, map_smul' := ⋯ }

theorem Lorentz.Vector.actionCLM_apply {d : ℕ} (Λ : ↑(LorentzGroup d)) (p : Vector d) : (actionCLM Λ) p = Λ • p

theorem Lorentz.Vector.actionCLM_injective {d : ℕ} (Λ : ↑(LorentzGroup d)) : Function.Injective ⇑(actionCLM Λ)

theorem Lorentz.Vector.actionCLM_surjective {d : ℕ} (Λ : ↑(LorentzGroup d)) : Function.Surjective ⇑(actionCLM Λ)

theorem Lorentz.Vector.smul_basis {d : ℕ} (Λ : ↑(LorentzGroup d)) (μ : Fin 1 ⊕ Fin d) : Λ • basis μ = ∑ ν : Fin 1 ⊕ Fin d, ↑Λ ν μ • basis ν

C. The Spatial part

@[reducible, inline]

abbrev Lorentz.Vector.spatialPart {d : ℕ} (v : Vector d) : EuclideanSpace ℝ (Fin d)

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

Equations

• v.spatialPart = WithLp.toLp 2 fun (i : Fin d) => v (Sum.inr i)

theorem Lorentz.Vector.spatialPart_apply_eq_toCoord {d : ℕ} (v : Vector d) (i : Fin d) : v.spatialPart.ofLp i = v (Sum.inr i)

theorem Lorentz.Vector.spatialPart_basis_sum_inr {d : ℕ} (i j : Fin d) : (basis (Sum.inr i)).spatialPart.ofLp j = (Finsupp.single (Sum.inr i) 1) (Sum.inr j)

theorem Lorentz.Vector.spatialPart_basis_sum_inl {d : ℕ} (i : Fin d) : (basis (Sum.inl 0)).spatialPart.ofLp i = 0

def Lorentz.Vector.spatialCLM (d : ℕ) : Vector d →L[ℝ] EuclideanSpace ℝ (Fin d)

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

Equations

• Lorentz.Vector.spatialCLM d = { toFun := fun (v : Lorentz.Vector d) => WithLp.toLp 2 fun (i : Fin d) => v (Sum.inr i), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem Lorentz.Vector.spatialCLM_apply_eq_spatialPart {d : ℕ} (v : Vector d) (i : Fin d) : ((spatialCLM d) v).ofLp i = v.spatialPart.ofLp i

@[simp]

theorem Lorentz.Vector.spatialCLM_basis_sum_inl {d : ℕ} : (spatialCLM d) (basis (Sum.inl 0)) = 0

@[simp]

theorem Lorentz.Vector.spatialCLM_basis_sum_inr {d : ℕ} (i : Fin d) : (spatialCLM d) (basis (Sum.inr i)) = (EuclideanSpace.basisFun (Fin d) ℝ) i

The Temporal component

@[reducible, inline]

abbrev Lorentz.Vector.timeComponent {d : ℕ} (v : Vector d) : ℝ

Extract time component from a Lorentz vector

Equations

• v.timeComponent = v (Sum.inl 0)

theorem Lorentz.Vector.timeComponent_basis_sum_inr {d : ℕ} (i : Fin d) : (basis (Sum.inr i)).timeComponent = 0

theorem Lorentz.Vector.timeComponent_basis_sum_inl {d : ℕ} : (basis (Sum.inl 0)).timeComponent = 1

def Lorentz.Vector.temporalCLM (d : ℕ) : Vector d →L[ℝ] ℝ

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

Equations

• Lorentz.Vector.temporalCLM d = LinearMap.toContinuousLinearMap { toFun := fun (v : Lorentz.Vector d) => v (Sum.inl 0), map_add' := ⋯, map_smul' := ⋯ }

theorem Lorentz.Vector.temporalCLM_apply_eq_timeComponent {d : ℕ} (v : Vector d) : (temporalCLM d) v = v.timeComponent

@[simp]

theorem Lorentz.Vector.temporalCLM_basis_sum_inr {d : ℕ} (i : Fin d) : (temporalCLM d) (basis (Sum.inr i)) = 0

@[simp]

theorem Lorentz.Vector.temporalCLM_basis_sum_inl {d : ℕ} : (temporalCLM d) (basis (Sum.inl 0)) = 1

## Smoothness

def Lorentz.Vector.asSmoothManifold (d : ℕ) : ModelWithCorners ℝ (Vector d) (Vector d)

The structure of a smooth manifold on Vector .

Equations

• Lorentz.Vector.asSmoothManifold d = modelWithCornersSelf ℝ (Lorentz.Vector d)

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

theorem Lorentz.Vector.basis_inner {d : ℕ} (μ : Fin 1 ⊕ Fin d) (p : Vector d) : inner ℝ (basis μ) p = p μ

theorem Lorentz.Vector.inner_basis {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) : inner ℝ p (basis μ) = p μ