Space time

This file introduce 4d Minkowski spacetime.

@[reducible, inline]

abbrev SpaceTime (d : ℕ := 3) : Type

SpaceTime d corresponds to d+1 dimensional space-time. This is equipped with an instaance of the action of a Lorentz group, corresponding to Minkowski-spacetime.

Equations

• SpaceTime d = Lorentz.Vector d

To space and time

def SpaceTime.space {d : ℕ} : SpaceTime d →ₗ[ℝ] Space d

The space part of spacetime.

Equations

• SpaceTime.space = { toFun := fun (x : SpaceTime d) => Lorentz.Vector.spatialPart x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SpaceTime.space_toCoord_symm {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) : space f = fun (i : Fin d) => f (Sum.inr i)

def SpaceTime.space_equivariant : InformalLemma

The function space is equivariant with respect to rotations.

Equations

• SpaceTime.space_equivariant = { deps := [`SpaceTime.space], tag := "7MTYX" }

def SpaceTime.time {d : ℕ} : SpaceTime d →ₗ[ℝ] Time

The time part of spacetime.

Equations

• SpaceTime.time = { toFun := fun (x : SpaceTime d) => { val := Lorentz.Vector.timeComponent x }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SpaceTime.time_val_toCoord_symm {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) : (time f).val = f (Sum.inl 0)

def SpaceTime.toTimeAndSpace {d : ℕ} : SpaceTime d ≃L[ℝ] Time × Space d

A continuous linear equivalence between SpaceTime d and Time × Space d.

Equations

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

theorem SpaceTime.toTimeAndSpace_basis_inr {d : ℕ} (i : Fin d) : toTimeAndSpace (Lorentz.Vector.basis (Sum.inr i)) = (0, Space.basis i)

theorem SpaceTime.toTimeAndSpace_basis_inl {d : ℕ} : toTimeAndSpace (Lorentz.Vector.basis (Sum.inl 0)) = (1, 0)

Coordinates

def SpaceTime.coord {d : ℕ} (μ : Fin (1 + d)) : SpaceTime d →ₗ[ℝ] ℝ

For a given μ : Fin (1 + d) coord μ p is the coordinate of p in the direction μ.

This is denoted 𝔁 μ p, where 𝔁 is typed with \MCx.

Equations

• SpaceTime.coord μ = { toFun := fun (x : SpaceTime d) => x (finSumFinEquiv.symm μ), map_add' := ⋯, map_smul' := ⋯ }

def SpaceTime.term𝔁 : Lean.ParserDescr

For a given μ : Fin (1 + d) coord μ p is the coordinate of p in the direction μ.

This is denoted 𝔁 μ p, where 𝔁 is typed with \MCx.

Equations

• SpaceTime.term𝔁 = Lean.ParserDescr.node `SpaceTime.term𝔁 1024 (Lean.ParserDescr.symbol "𝔁")

theorem SpaceTime.coord_apply {d : ℕ} (μ : Fin (1 + d)) (y : SpaceTime d) : (coord μ) y = y (finSumFinEquiv.symm μ)

Derivatives

noncomputable def SpaceTime.deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] {d : ℕ} (μ : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) : SpaceTime d → M

The derivative of a function SpaceTime d → ℝ along the μ coordinte.

Equations

• SpaceTime.deriv μ f y = (fderiv ℝ f y) (Lorentz.Vector.basis μ)

def SpaceTime.«term∂_» : Lean.ParserDescr

The derivative of a function SpaceTime d → ℝ along the μ coordinte.

Equations

• SpaceTime.«term∂_» = Lean.ParserDescr.node `SpaceTime.«term∂_» 1024 (Lean.ParserDescr.symbol "∂_")

theorem SpaceTime.deriv_eq {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] {d : ℕ} (μ : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) (y : SpaceTime d) : deriv μ f y = (fderiv ℝ f y) (Lorentz.Vector.basis μ)

@[simp]

theorem SpaceTime.deriv_zero {d : ℕ} (μ : Fin 1 ⊕ Fin d) : (deriv μ fun (x : SpaceTime d) => 0) = 0