Spacetime

i. Overview

In this file we define the type SpaceTime d which corresponds to d+1 dimensional spacetime. This is equipped with an instance of the action of a Lorentz group, corresponding to Minkowski-spacetime.

It is defined through Lorentz.Vector d, and carries the tensorial instance, allowing it to be used in tensorial expressions.

ii. Key results

• SpaceTime d : The type corresponding to d+1 dimensional spacetime.
• toTimeAndSpace : A continuous linear equivalence between SpaceTime d and Time × Space d.

iii. Table of contents

• A. The definition of SpaceTime d
• C. Continuous linear map to coordinates
• D. Measures on SpaceTime d
  • D.1. Instance of a measurable space
  • D.2. Instance of a borel space
  • D.4. Instance of a measure space
  • D.5. Volume measure is positive on non-empty open sets
  • D.6. Volume measure is a finite measure on compact sets
  • D.7. Volume measure is an additive Haar measure
• B. Maps to and from Space and Time
  • B.1. Linear map to Space d
    • B.1.1. Explicit expansion of map to space
    • B.1.2. Equivariance of the to space under rotations
  • B.2. Linear map to Time
    • B.2.1. Explicit expansion of map to time in terms of coordinates
  • B.3. toTimeAndSpace: Continuous linear equivalence to Time × Space d
    • B.3.1. Derivative of toTimeAndSpace
    • B.3.2. Derivative of the inverse of toTimeAndSpace
    • B.3.3. toTimeAndSpace acting on spatial basis vectors
    • B.3.4. toTimeAndSpace acting on the temporal basis vectors
  • B.4. Time space basis
    • B.4.1. Elements of the basis
    • B.4.2. Equivalence adjusting time basis vector
    • B.4.3. Determinant of the equivalence
    • B.4.4. Time space basis expressed in terms of the Lorentz basis
    • B.4.5. The additive Haar measure associated to the time space basis
  • B.5. Integrals over SpaceTime d
    • B.5.1. Measure preserving property of toTimeAndSpace.symm
    • B.5.2. Integrals over SpaceTime d expressed as integrals over Time and Space d

iv. References

A. The definition of SpaceTime d

@[reducible, inline]

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

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

Equations

• SpaceTime d = Lorentz.Vector d

C. Continuous linear map to 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 μ)

def SpaceTime.coordCLM {d : ℕ} (μ : Fin 1 ⊕ Fin d) : SpaceTime d →L[ℝ] ℝ

The continuous linear map from a point in space time to one of its coordinates.

Equations

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

D. Measures on SpaceTime d

D.1. Instance of a measurable space

instance SpaceTime.instMeasurableSpace {d : ℕ} : MeasurableSpace (SpaceTime d)

Equations

• SpaceTime.instMeasurableSpace = borel (SpaceTime d)

D.2. Instance of a borel space

instance SpaceTime.instBorelSpace {d : ℕ} : BorelSpace (SpaceTime d)

D.4. Instance of a measure space

instance SpaceTime.instMeasureSpace {d : ℕ} : MeasureTheory.MeasureSpace (SpaceTime d)

Equations

• SpaceTime.instMeasureSpace = { toMeasurableSpace := SpaceTime.instMeasurableSpace, volume := Lorentz.Vector.basis.addHaar }

D.5. Volume measure is positive on non-empty open sets

instance SpaceTime.instIsOpenPosMeasureVolume {d : ℕ} : MeasureTheory.volume.IsOpenPosMeasure

D.6. Volume measure is a finite measure on compact sets

instance SpaceTime.instIsFiniteMeasureOnCompactsVolume {d : ℕ} : MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume

D.7. Volume measure is an additive Haar measure

instance SpaceTime.instIsAddHaarMeasureVolume {d : ℕ} : MeasureTheory.volume.IsAddHaarMeasure

B. Maps to and from Space and Time

B.1. Linear map to Space d

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

The space part of spacetime.

Equations

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

B.1.1. Explicit expansion of map to space

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

B.1.2. Equivariance of the to space under rotations

def SpaceTime.space_equivariant : InformalLemma

The function space is equivariant with respect to rotations.

Equations

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

B.2. Linear map to Time

def SpaceTime.time {d : ℕ} (c : SpeedOfLight := 1) : SpaceTime d →ₗ[ℝ] Time

The time part of spacetime.

Equations

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

B.2.1. Explicit expansion of map to time in terms of coordinates

@[simp]

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

B.3. toTimeAndSpace: Continuous linear equivalence to Time × Space d

def SpaceTime.toTimeAndSpace {d : ℕ} (c : SpeedOfLight := 1) : 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.

@[simp]

theorem SpaceTime.toTimeAndSpace_symm_apply_time_space {d : ℕ} {c : SpeedOfLight} (x : SpaceTime d) : (toTimeAndSpace c).symm ((time c) x, space x) = x

@[simp]

theorem SpaceTime.space_toTimeAndSpace_symm {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) : space ((toTimeAndSpace c).symm (t, s)) = s

@[simp]

theorem SpaceTime.time_toTimeAndSpace_symm {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) : (time c) ((toTimeAndSpace c).symm (t, s)) = t

@[simp]

theorem SpaceTime.toTimeAndSpace_symm_apply_inl {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) : (toTimeAndSpace c).symm (t, s) (Sum.inl 0) = c.val * t.val

@[simp]

theorem SpaceTime.toTimeAndSpace_symm_apply_inr {d : ℕ} {c : SpeedOfLight} (t : Time) (x : Space d) (i : Fin d) : (toTimeAndSpace c).symm (t, x) (Sum.inr i) = x.val i

B.3.1. Derivative of toTimeAndSpace

@[simp]

theorem SpaceTime.toTimeAndSpace_fderiv {d : ℕ} {c : SpeedOfLight} (x : SpaceTime d) : fderiv ℝ (⇑(toTimeAndSpace c)) x = ↑(toTimeAndSpace c)

B.3.2. Derivative of the inverse of toTimeAndSpace

@[simp]

theorem SpaceTime.toTimeAndSpace_symm_fderiv {d : ℕ} {c : SpeedOfLight} (x : Time × Space d) : fderiv ℝ (⇑(toTimeAndSpace c).symm) x = ↑(toTimeAndSpace c).symm

B.3.3. toTimeAndSpace acting on spatial basis vectors

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

B.3.4. toTimeAndSpace acting on the temporal basis vectors

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

theorem SpaceTime.toTimeAndSpace_basis_inl' {d : ℕ} {c : SpeedOfLight} : (toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0)) = (1 / c.val) • (1, 0)

B.4. Time space basis

def SpaceTime.timeSpaceBasis {d : ℕ} (c : SpeedOfLight := 1) : Module.Basis (Fin 1 ⊕ Fin d) ℝ (SpaceTime d)

The basis of SpaceTime where the first component is (c, 0, 0, ...) instead of (1, 0, 0, ....).

Equations

• SpaceTime.timeSpaceBasis c = { repr := (SpaceTime.toTimeAndSpace c).trans (Time.basis.toBasis.prod Space.basis.toBasis).repr }

B.4.1. Elements of the basis

@[simp]

theorem SpaceTime.timeSpaceBasis_apply_inl {d : ℕ} (c : SpeedOfLight) : (timeSpaceBasis c) (Sum.inl 0) = c.val • Lorentz.Vector.basis (Sum.inl 0)

@[simp]

theorem SpaceTime.timeSpaceBasis_apply_inr {d : ℕ} (c : SpeedOfLight) (i : Fin d) : (timeSpaceBasis c) (Sum.inr i) = Lorentz.Vector.basis (Sum.inr i)

B.4.2. Equivalence adjusting time basis vector

def SpaceTime.timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) : SpaceTime d ≃L[ℝ] SpaceTime d

The equivalence on of SpaceTime taking (1, 0, 0, ...) to of (c, 0, 0, ....) and keeping all other components the same.

Equations

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

B.4.3. Determinant of the equivalence

theorem SpaceTime.det_timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) : ↑(LinearEquiv.det (timeSpaceBasisEquiv c).toLinearEquiv) = c.val

B.4.4. Time space basis expressed in terms of the Lorentz basis

theorem SpaceTime.timeSpaceBasis_eq_map_basis {d : ℕ} (c : SpeedOfLight) : timeSpaceBasis c = Lorentz.Vector.basis.map (timeSpaceBasisEquiv c).toLinearEquiv

B.4.5. The additive Haar measure associated to the time space basis

theorem SpaceTime.timeSpaceBasis_addHaar {d : ℕ} (c : SpeedOfLight := 1) : (timeSpaceBasis c).addHaar = ENNReal.ofReal c.val⁻¹ • MeasureTheory.volume

B.5. Integrals over SpaceTime d

B.5.1. Measure preserving property of toTimeAndSpace.symm

theorem SpaceTime.toTimeAndSpace_symm_measurePreserving {d : ℕ} (c : SpeedOfLight) : MeasureTheory.MeasurePreserving (⇑(toTimeAndSpace c).symm) (MeasureTheory.volume.prod MeasureTheory.volume) (ENNReal.ofReal c.val⁻¹ • MeasureTheory.volume)

B.5.2. Integrals over SpaceTime d expressed as integrals over Time and Space d

theorem SpaceTime.spaceTime_integral_eq_time_space_integral {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (c : SpeedOfLight) (f : SpaceTime d → M) : ∫ (x : SpaceTime d), f x = c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂MeasureTheory.volume.prod MeasureTheory.volume

theorem SpaceTime.spaceTime_integrable_iff_space_time_integrable {M : Type u_1} [NormedAddCommGroup M] {d : ℕ} (c : SpeedOfLight) (f : SpaceTime d → M) : MeasureTheory.Integrable f MeasureTheory.volume ↔ MeasureTheory.Integrable (f ∘ ⇑(toTimeAndSpace c).symm) (MeasureTheory.volume.prod MeasureTheory.volume)

theorem SpaceTime.spaceTime_integral_eq_time_integral_space_integral {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (c : SpeedOfLight) (f : SpaceTime d → M) (h : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : SpaceTime d), f x = c.val • ∫ (t : Time) (x : Space d), f ((toTimeAndSpace c).symm (t, x))

theorem SpaceTime.spaceTime_integral_eq_space_integral_time_integral {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (c : SpeedOfLight) (f : SpaceTime d → M) (h : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : SpaceTime d), f x = c.val • ∫ (x : Space d) (t : Time), f ((toTimeAndSpace c).symm (t, x))