Metrics as real Lorentz tensors

@[reducible, inline]

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

Real contravariant Lorentz vector.

Equations

• Lorentz.Vector d = (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up]

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.

def Lorentz.Vector.toCoord {d : ℕ} : Vector d ≃ₗ[ℝ] Fin 1 ⊕ Fin d → ℝ

The coordinates of a Lorentz vector as a linear map.

Equations

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

theorem Lorentz.Vector.toCoord_apply {d : ℕ} (p : Vector d) : toCoord 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.toCoord_injective {d : ℕ} : Function.Injective ⇑toCoord

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

Equations

• Lorentz.Vector.instCoeFunForallSumFinOfNatNatReal = { coe := ⇑Lorentz.Vector.toCoord }

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

theorem Lorentz.Vector.toCoord_basis_apply {d : ℕ} (μ : Fin (1 + d)) (ν : Fin 1 ⊕ Fin d) : toCoord ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ μ) ν = (Finsupp.single (finSumFinEquiv.symm μ) 1) ν

theorem Lorentz.Vector.basis_repr_apply {d : ℕ} (p : Vector d) (b : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up]) : ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr p) b = toCoord p (finSumFinEquiv.symm (b 0))

def Lorentz.Vector.innerProduct {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.

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

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.innerProduct_toCoord {d : ℕ} (p q : Vector d) : ⟪p, q⟫ₘ = toCoord p (Sum.inl 0) * toCoord q (Sum.inl 0) - ∑ i : Fin d, toCoord p (Sum.inr i) * toCoord q (Sum.inr i)

@[simp]

theorem Lorentz.Vector.innerProduct_zero_left {d : ℕ} (q : Vector d) : ⟪0, q⟫ₘ = 0

@[simp]

theorem Lorentz.Vector.innerProduct_zero_right {d : ℕ} (p : Vector d) : ⟪p, 0⟫ₘ = 0

@[simp]

theorem Lorentz.Vector.innerProduct_invariant {d : ℕ} (p q : Vector d) (Λ : ↑(LorentzGroup d)) : ⟪Λ • p, Λ • q⟫ₘ = ⟪p, q⟫ₘ

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

## Smoothness

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

Equations

• Lorentz.Vector.isNormedAddCommGroup d = NormedAddCommGroup.induced (Lorentz.Vector d) (Fin 1 ⊕ Fin d → ℝ) Lorentz.Vector.toCoord ⋯

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

Equations

• Lorentz.Vector.isNormedSpace d = NormedSpace.induced ℝ (Lorentz.Vector d) (Fin 1 ⊕ Fin d → ℝ) Lorentz.Vector.toCoord

def Lorentz.Vector.toCoordContinuous {d : ℕ} : Vector d ≃L[ℝ] Fin 1 ⊕ Fin d → ℝ

The toCoord map as a ContinuousLinearEquiv.

Equations

• Lorentz.Vector.toCoordContinuous = Lorentz.Vector.toCoord.toContinuousLinearEquiv

theorem Lorentz.Vector.toCoord_differentiable {d : ℕ} : Differentiable ℝ ⇑toCoord

theorem Lorentz.Vector.toCoord_fderiv {d : ℕ} (x : Vector d) : ↑(fderiv ℝ (⇑toCoord) x) = ↑toCoord

def Lorentz.Vector.toCoordFull {d : ℕ} : Vector d ≃ₗ[ℝ] ((j : Fin (Nat.succ 0)) → Fin ((realLorentzTensor d).repDim (![realLorentzTensor.Color.up] j))) → ℝ

The coordinates of a Lorentz vector as a linear map.

Equations

• Lorentz.Vector.toCoordFull = ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr.toEquiv.trans Finsupp.equivFunOnFinite).toLinearEquiv ⋯

theorem Lorentz.Vector.toCoord_apply_eq_toCoordFull_apply {d : ℕ} (p : Vector d) : toCoord p = (Equiv.piCongrLeft' (fun (a : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up]) => ℝ) indexEquiv) (toCoordFull p)

def Lorentz.Vector.fromCoordFullContinuous {d : ℕ} : (((j : Fin (Nat.succ 0)) → Fin ((realLorentzTensor d).repDim (![realLorentzTensor.Color.up] j))) → ℝ) ≃L[ℝ] Vector d

The toCoordFull map as a ContinuousLinearEquiv.

Equations

• Lorentz.Vector.fromCoordFullContinuous = Lorentz.Vector.toCoordFull.symm.toContinuousLinearEquiv

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)

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)

The Lorentz action

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

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

@[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 i = Lorentz.Vector.toCoord v (Sum.inr i)

@[simp]

theorem Lorentz.Vector.spatialPart_basis_natAdd {d : ℕ} (i j : Fin d) : spatialPart ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ (Fin.natAdd 1 i)) j = (Finsupp.single (Sum.inr i) 1) (Sum.inr j)

@[simp]

theorem Lorentz.Vector.spatialPart_basis_castAdd {d : ℕ} (i : Fin d) : spatialPart ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ (Fin.castAdd d 0)) i = 0

@[reducible, inline]

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

Extract time component from a Lorentz vector

Equations

• v.timeComponent = Lorentz.Vector.toCoord v (Sum.inl 0)

@[simp]

theorem Lorentz.Vector.timeComponent_basis_natAdd {d : ℕ} (i : Fin d) : timeComponent ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ (Fin.natAdd 1 i)) = 0

@[simp]

theorem Lorentz.Vector.timeComponent_basis_castAdd {d : ℕ} : timeComponent ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ (Fin.castAdd d 0)) = 1