Space time

This file introduce 4d Minkowski spacetime.

@[reducible, inline]

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

The space-time

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 (Lorentz.Vector.toCoord.symm 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) => Lorentz.Vector.timeComponent x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem SpaceTime.time_toCoord_symm {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) : time (Lorentz.Vector.toCoord.symm f) = 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_natAdd {d : ℕ} (i : Fin d) : toTimeAndSpace ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ (Fin.natAdd 1 i)) = (0, Space.basis i)

theorem SpaceTime.toTimeAndSpace_basis_castAdd {d : ℕ} : toTimeAndSpace ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ (Fin.castAdd d 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 := flip (⇑Lorentz.Vector.toCoord) (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 = Lorentz.Vector.toCoord y (finSumFinEquiv.symm μ)

theorem SpaceTime.coord_on_repr {d : ℕ} (μ : Fin (1 + d)) (y : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up] → ℝ) : (coord μ) ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr.symm (Finsupp.equivFunOnFinite.symm y)) = y fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ μ

Derivatives

noncomputable def SpaceTime.deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] {d : ℕ} (μ : Fin (1 + 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) ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ μ)

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 + d)) (f : SpaceTime d → M) (y : SpaceTime d) : deriv μ f y = (fderiv ℝ f y) ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ μ)

@[simp]

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

theorem SpaceTime.deriv_eq_deriv_on_coord {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → ℝ) (y : SpaceTime d) : deriv μ f y = (fderiv ℝ (fun (y : TensorSpecies.Tensor.ComponentIdx ![realLorentzTensor.Color.up] → ℝ) => f ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr.symm (Finsupp.equivFunOnFinite.symm y))) ⇑((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]).repr y)) ⇑(Finsupp.single (fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ μ) 1)

theorem SpaceTime.neg_deriv {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → ℝ) : -deriv μ f = deriv μ fun (y : SpaceTime d) => -f y

theorem SpaceTime.neg_deriv_apply {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → ℝ) (y : SpaceTime d) : -deriv μ f y = deriv μ (fun (y : SpaceTime d) => -f y) y

theorem SpaceTime.coord_differentiable {d : ℕ} (μ : Fin (1 + d)) : Differentiable ℝ ⇑(coord μ)

theorem SpaceTime.deriv_coord_same {d : ℕ} (μ : Fin (1 + d)) (y : SpaceTime d) : deriv μ (⇑(coord μ)) y = 1

theorem SpaceTime.deriv_coord_diff {d : ℕ} (μ ν : Fin (1 + d)) (h : μ ≠ ν) (y : SpaceTime d) : deriv μ (⇑(coord ν)) y = 0

theorem SpaceTime.deriv_coord_eq_if {d : ℕ} (μ ν : Fin (1 + d)) (y : SpaceTime d) : deriv μ (⇑(coord ν)) y = if μ = ν then 1 else 0

@[simp]

theorem SpaceTime.deriv_toTimeAndSpace {d : ℕ} (μ : Fin (1 + d)) (y : SpaceTime d) : deriv μ (⇑toTimeAndSpace) y = toTimeAndSpace ((TensorSpecies.Tensor.basis ![realLorentzTensor.Color.up]) fun (x : Fin (Nat.succ 0)) => Fin.cast ⋯ μ)

theorem SpaceTime.deriv_comp_toTimeAndSpace_natAdd {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d) (f : Time × Space d → M) (y : SpaceTime d) : deriv (Fin.natAdd 1 i) (f ∘ ⇑toTimeAndSpace) y = (fderiv ℝ f (toTimeAndSpace y)) (0, Space.basis i)

theorem SpaceTime.deriv_comp_toTimeAndSpace_castAdd {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (f : Time × Space d → M) (y : SpaceTime d) : deriv (Fin.castAdd d 0) (f ∘ ⇑toTimeAndSpace) y = (fderiv ℝ f (toTimeAndSpace y)) (1, 0)