Physlib.SpaceAndTime.SpaceTime.Basic

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.SpeedOfLight
public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial
public import Physlib.SpaceAndTime.Space.Integrals.Basic
public import Physlib.SpaceAndTime.Time.Basic
public import Physlib.Meta.Informal.Basic

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

@[expose] public section

A. The definition of `SpaceTime d`

TODO "SpaceTime should be refactored into a structure, or similar, to prevent casting."

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.

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

C. Continuous linear map to coordinates

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.

def coord {d : ℕ} (μ : Fin (1 + d)) : SpaceTime d →ₗ[ℝ] ℝ where
  toFun x := x (finSumFinEquiv.symm μ)
  map_add' x1 x2 := byd:ℕμ:Fin (1 + d)x1:SpaceTime dx2:SpaceTime d⊢ (x1 + x2) (finSumFinEquiv.symm μ) = x1 (finSumFinEquiv.symm μ) + x2 (finSumFinEquiv.symm μ)
    simpAll goals completed! 🐙
  map_smul' c x := byd:ℕμ:Fin (1 + d)c:ℝx:SpaceTime d⊢ (c • x) (finSumFinEquiv.symm μ) = (RingHom.id ℝ) c • x (finSumFinEquiv.symm μ)
    simpAll goals completed! 🐙

@[inherit_doc coord]
scoped notation "𝔁" => coord

lemma coord_apply {d : ℕ} (μ : Fin (1 + d)) (y : SpaceTime d) :
    𝔁 μ y = y (finSumFinEquiv.symm μ) := byd:ℕμ:Fin (1 + d)y:SpaceTime d⊢ (𝔁 μ) y = y (finSumFinEquiv.symm μ)
  rflAll goals completed! 🐙

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

def coordCLM (μ : Fin 1 ⊕ Fin d) : SpaceTime d →L[ℝ] ℝ where
  toFun x := x μ
  map_add' x1 x2 := byd:ℕμ:Fin 1 ⊕ Fin dx1:SpaceTime dx2:SpaceTime d⊢ (x1 + x2) μ = x1 μ + x2 μ
    simpAll goals completed! 🐙
  map_smul' c x := byd:ℕμ:Fin 1 ⊕ Fin dc:ℝx:SpaceTime d⊢ (c • x) μ = (RingHom.id ℝ) c • x μ
    simpAll goals completed! 🐙
  cont := byd:ℕμ:Fin 1 ⊕ Fin d⊢ Continuous fun x => x μ
    fun_propAll goals completed! 🐙

D. Measures on `SpaceTime d`

D.1. Instance of a measurable space

instance {d : ℕ} : MeasurableSpace (SpaceTime d) := borel (SpaceTime d)

D.2. Instance of a borel space

instance {d : ℕ} : BorelSpace (SpaceTime d) where
  measurable_eq := byd:ℕ⊢ instMeasurableSpace = borel (SpaceTime d) rflAll goals completed! 🐙

D.4. Instance of a measure space

instance {d : ℕ} : MeasureSpace (SpaceTime d) where
  volume := Lorentz.Vector.basis.addHaar

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

instance {d : ℕ} : (volume (α := SpaceTime d)).IsOpenPosMeasure :=
  inferInstanceAs ((Lorentz.Vector.basis.addHaar).IsOpenPosMeasure)

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

instance {d : ℕ} : IsFiniteMeasureOnCompacts (volume (α := SpaceTime d)) :=
  inferInstanceAs (IsFiniteMeasureOnCompacts (Lorentz.Vector.basis.addHaar))

D.7. Volume measure is an additive Haar measure

instance {d : ℕ} : Measure.IsAddHaarMeasure (volume (α := SpaceTime d)) :=
  inferInstanceAs (Measure.IsAddHaarMeasure (Lorentz.Vector.basis.addHaar))

B. Maps to and from `Space` and `Time`

B.1. Linear map to `Space d`

The space part of spacetime.

def space {d : ℕ} : SpaceTime d →L[ℝ] Space d where
  toFun x := ⟨Lorentz.Vector.spatialPart x⟩
  map_add' x1 x2 := byd:ℕx1:SpaceTime dx2:SpaceTime d⊢ { val := (Lorentz.Vector.spatialPart (x1 + x2)).ofLp } =
  { val := (Lorentz.Vector.spatialPart x1).ofLp } + { val := (Lorentz.Vector.spatialPart x2).ofLp }
    ext id:ℕx1:SpaceTime dx2:SpaceTime di:Fin d⊢ { val := (Lorentz.Vector.spatialPart (x1 + x2)).ofLp }.val i =
  ({ val := (Lorentz.Vector.spatialPart x1).ofLp } + { val := (Lorentz.Vector.spatialPart x2).ofLp }).val i
    simpAll goals completed! 🐙
  map_smul' c x := byd:ℕc:ℝx:SpaceTime d⊢ { val := (Lorentz.Vector.spatialPart (c • x)).ofLp } = (RingHom.id ℝ) c • { val := (Lorentz.Vector.spatialPart x).ofLp }
    ext id:ℕc:ℝx:SpaceTime di:Fin d⊢ { val := (Lorentz.Vector.spatialPart (c • x)).ofLp }.val i =
  ((RingHom.id ℝ) c • { val := (Lorentz.Vector.spatialPart x).ofLp }).val i
    simpAll goals completed! 🐙
  cont := byd:ℕ⊢ Continuous fun x => { val := (Lorentz.Vector.spatialPart x).ofLp }
    fun_propAll goals completed! 🐙

B.1.1. Explicit expansion of map to space

lemma space_toCoord_symm {d : ℕ} (f : Fin 1 ⊕ Fin d → ℝ) :
    space f = fun i => f (Sum.inr i) := byd:ℕf:Fin 1 ⊕ Fin d → ℝ⊢ (space f).val = fun i => f (Sum.inr i)
  funext id:ℕf:Fin 1 ⊕ Fin d → ℝi:Fin d⊢ (space f).val i = f (Sum.inr i)
  simp [space]All goals completed! 🐙

B.1.2. Equivariance of the to space under rotations

The function space is equivariant with respect to rotations.

informal_lemma space_equivariant where
  deps := [``space]
  tag := "7MTYX"

B.2. Linear map to `Time`

The time part of spacetime.

def time {d : ℕ} (c : SpeedOfLight := 1) : SpaceTime d →ₗ[ℝ] Time where
  toFun x := ⟨Lorentz.Vector.timeComponent x / c⟩
  map_add' x1 x2 := byd:ℕc:SpeedOfLightx1:SpaceTime dx2:SpaceTime d⊢ { val := Lorentz.Vector.timeComponent (x1 + x2) / c.val } =
  { val := Lorentz.Vector.timeComponent x1 / c.val } + { val := Lorentz.Vector.timeComponent x2 / c.val }
    extd:ℕc:SpeedOfLightx1:SpaceTime dx2:SpaceTime d⊢ { val := Lorentz.Vector.timeComponent (x1 + x2) / c.val }.val =
  ({ val := Lorentz.Vector.timeComponent x1 / c.val } + { val := Lorentz.Vector.timeComponent x2 / c.val }).val
    simp [Lorentz.Vector.timeComponent]d:ℕc:SpeedOfLightx1:SpaceTime dx2:SpaceTime d⊢ (x1 (Sum.inl 0) + x2 (Sum.inl 0)) / c.val = x1 (Sum.inl 0) / c.val + x2 (Sum.inl 0) / c.val
    grindAll goals completed! 🐙
  map_smul' c x := byd:ℕc✝:SpeedOfLightc:ℝx:SpaceTime d⊢ { val := Lorentz.Vector.timeComponent (c • x) / c✝.val } =
  (RingHom.id ℝ) c • { val := Lorentz.Vector.timeComponent x / c✝.val }
    extd:ℕc✝:SpeedOfLightc:ℝx:SpaceTime d⊢ { val := Lorentz.Vector.timeComponent (c • x) / c✝.val }.val =
  ((RingHom.id ℝ) c • { val := Lorentz.Vector.timeComponent x / c✝.val }).val
    simp [Lorentz.Vector.timeComponent]d:ℕc✝:SpeedOfLightc:ℝx:SpaceTime d⊢ c * x (Sum.inl 0) / c✝.val = c * (x (Sum.inl 0) / c✝.val)
    grindAll goals completed! 🐙

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

@[simp]
lemma time_val_toCoord_symm {d : ℕ} (c : SpeedOfLight) (f : Fin 1 ⊕ Fin d → ℝ) :
    (time c f).val = f (Sum.inl 0) / c := byd:ℕc:SpeedOfLightf:Fin 1 ⊕ Fin d → ℝ⊢ ((time c) f).val = f (Sum.inl 0) / c.val
  simp [time, Lorentz.Vector.timeComponent]All goals completed! 🐙

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

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

def toTimeAndSpace {d : ℕ} (c : SpeedOfLight := 1) : SpaceTime d ≃L[ℝ] Time × Space d :=
  LinearEquiv.toContinuousLinearEquiv {
    toFun x := (x.time c, x.space)
    invFun tx := (fun i =>
      match i with
      | Sum.inl _ => c * tx.1.val
      | Sum.inr i => tx.2 i)
    left_inv x := byd:ℕc:SpeedOfLightx:SpaceTime d⊢ (fun tx i =>
      match i with
      | Sum.inl val => c.val * tx.1.val
      | Sum.inr i => tx.2.val i)
    ((fun x => ((time c) x, space x)) x) =
  x
      simp only [time, LinearMap.coe_mk, AddHom.coe_mk, space]d:ℕc:SpeedOfLightx:SpaceTime d⊢ (fun i =>
    match i with
    | Sum.inl val => c.val * (Lorentz.Vector.timeComponent x / c.val)
    | Sum.inr i =>
      ({ toFun := fun x => { val := fun i => x (Sum.inr i) }, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x).val i) =
  x
      funext id:ℕc:SpeedOfLightx:SpaceTime di:Fin 1 ⊕ Fin d⊢ (match i with
  | Sum.inl val => c.val * (Lorentz.Vector.timeComponent x / c.val)
  | Sum.inr i =>
    ({ toFun := fun x => { val := fun i => x (Sum.inr i) }, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x).val i) =
  x i
      match i with
      | Sum.inl 0 =>d:ℕc:SpeedOfLightx:SpaceTime di:Fin 1 ⊕ Fin d⊢ (match Sum.inl 0 with
  | Sum.inl val => c.val * (Lorentz.Vector.timeComponent x / c.val)
  | Sum.inr i =>
    ({ toFun := fun x => { val := fun i => x (Sum.inr i) }, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x).val i) =
  x (Sum.inl 0)
        simp [Lorentz.Vector.timeComponent]d:ℕc:SpeedOfLightx:SpaceTime di:Fin 1 ⊕ Fin d⊢ c.val * (x (Sum.inl 0) / c.val) = x (Sum.inl 0)
        field_simpAll goals completed! 🐙
      | Sum.inr i =>d:ℕc:SpeedOfLightx:SpaceTime di✝:Fin 1 ⊕ Fin di:Fin d⊢ (match Sum.inr i with
  | Sum.inl val => c.val * (Lorentz.Vector.timeComponent x / c.val)
  | Sum.inr i =>
    ({ toFun := fun x => { val := fun i => x (Sum.inr i) }, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x).val i) =
  x (Sum.inr i) simpAll goals completed! 🐙
    right_inv tx := byd:ℕc:SpeedOfLighttx:Time × Space d⊢ (fun x => ((time c) x, space x))
    ((fun tx i =>
        match i with
        | Sum.inl val => c.val * tx.1.val
        | Sum.inr i => tx.2.val i)
      tx) =
  tx
      simp only [time, Lorentz.Vector.timeComponent, Fin.isValue, LinearMap.coe_mk, AddHom.coe_mk,
        ne_eq, SpeedOfLight.val_ne_zero, not_false_eq_true, mul_div_cancel_left₀, space,
        ContinuousLinearMap.coe_mk']All goals completed! 🐙
    map_add' x y := byd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ ((time c) (x + y), space (x + y)) = ((time c) x, space x) + ((time c) y, space y)
      simp only [Prod.mk_add_mk, Prod.mk.injEq]d:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ (time c) (x + y) = (time c) x + (time c) y ∧ space (x + y) = space x + space y
      constructorleftd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ (time c) (x + y) = (time c) x + (time c) yrightd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ space (x + y) = space x + space y
      ·leftd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ (time c) (x + y) = (time c) x + (time c) y extleftd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ ((time c) (x + y)).val = ((time c) x + (time c) y).val
        simpAll goals completed! 🐙
      ext irightd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime di:Fin d⊢ (space (x + y)).val i = (space x + space y).val i
      simpAll goals completed! 🐙
    map_smul' := byd:ℕc:SpeedOfLight⊢ ∀ (m : ℝ) (x : SpaceTime d), ((time c) (m • x), space (m • x)) = (RingHom.id ℝ) m • ((time c) x, space x)
      simpAll goals completed! 🐙
  }

              @[simp]
lemma toTimeAndSpace_symm_apply_time_space {d : ℕ} {c : SpeedOfLight} (x : SpaceTime d) :
    (toTimeAndSpace c).symm (x.time c, x.space) = x :=
  (toTimeAndSpace c).left_inv x@[simp]
lemma space_toTimeAndSpace_symm {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) :
    ((toTimeAndSpace c).symm (t, s)).space = s := byd:ℕc:SpeedOfLightt:Times:Space d⊢ space ((toTimeAndSpace c).symm (t, s)) = s
  simp [space, toTimeAndSpace]All goals completed! 🐙@[simp]
lemma time_toTimeAndSpace_symm {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) :
    ((toTimeAndSpace c).symm (t, s)).time c = t := byd:ℕc:SpeedOfLightt:Times:Space d⊢ (time c) ((toTimeAndSpace c).symm (t, s)) = t
  simp [time, toTimeAndSpace]All goals completed! 🐙@[simp]
lemma toTimeAndSpace_symm_apply_inl {d : ℕ} {c : SpeedOfLight} (t : Time) (s : Space d) :
    (toTimeAndSpace c).symm (t, s) (Sum.inl 0) = c * t := byd:ℕc:SpeedOfLightt:Times:Space d⊢ (toTimeAndSpace c).symm (t, s) (Sum.inl 0) = c.val * t.val rflAll goals completed! 🐙@[simp]
lemma toTimeAndSpace_symm_apply_inr {d : ℕ} {c : SpeedOfLight} (t : Time) (x : Space d)
    (i : Fin d) :
    (toTimeAndSpace c).symm (t, x) (Sum.inr i) = x i := byd:ℕc:SpeedOfLightt:Timex:Space di:Fin d⊢ (toTimeAndSpace c).symm (t, x) (Sum.inr i) = x.val i rflAll goals completed! 🐙

B.3.1. Derivative of `toTimeAndSpace`



@[simp]
lemma toTimeAndSpace_fderiv {d : ℕ} {c : SpeedOfLight} (x : SpaceTime d) :
    fderiv ℝ (toTimeAndSpace c) x = (toTimeAndSpace c).toContinuousLinearMap := byd:ℕc:SpeedOfLightx:SpaceTime d⊢ fderiv ℝ (⇑(toTimeAndSpace c)) x = ↑(toTimeAndSpace c)
  rw [ContinuousLinearEquiv.fderivd:ℕc:SpeedOfLightx:SpaceTime d⊢ ↑(toTimeAndSpace c) = ↑(toTimeAndSpace c)All goals completed! 🐙]All goals completed! 🐙

B.3.2. Derivative of the inverse of `toTimeAndSpace`



@[simp]
lemma toTimeAndSpace_symm_fderiv {d : ℕ} {c : SpeedOfLight} (x : Time × Space d) :
    fderiv ℝ (toTimeAndSpace c).symm x = (toTimeAndSpace c).symm.toContinuousLinearMap := byd:ℕc:SpeedOfLightx:Time × Space d⊢ fderiv ℝ (⇑(toTimeAndSpace c).symm) x = ↑(toTimeAndSpace c).symm
  rw [ContinuousLinearEquiv.fderivd:ℕc:SpeedOfLightx:Time × Space d⊢ ↑(toTimeAndSpace c).symm = ↑(toTimeAndSpace c).symmAll goals completed! 🐙]All goals completed! 🐙

B.3.3. `toTimeAndSpace` acting on spatial basis vectors

lemma toTimeAndSpace_basis_inr {d : ℕ} {c : SpeedOfLight} (i : Fin d) :
    toTimeAndSpace c (Lorentz.Vector.basis (Sum.inr i))
    = (0, Space.basis i) := byd:ℕc:SpeedOfLighti:Fin d⊢ (toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i)) = (0, Space.basis i)
  refine Prod.ext ?_ ?_refine_1d:ℕc:SpeedOfLighti:Fin d⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))).1 = (0, Space.basis i).1refine_2d:ℕc:SpeedOfLighti:Fin d⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))).2 = (0, Space.basis i).2
  ·refine_1d:ℕc:SpeedOfLighti:Fin d⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))).1 = (0, Space.basis i).1 simp [toTimeAndSpace, time]All goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLighti:Fin d⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))).2 = (0, Space.basis i).2 ext jrefine_2d:ℕc:SpeedOfLighti:Fin dj:Fin d⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))).2.val j = (0, Space.basis i).2.val j
    simp [toTimeAndSpace, space, Space.basis_apply]All goals completed! 🐙

B.3.4. `toTimeAndSpace` acting on the temporal basis vectors

lemma toTimeAndSpace_basis_inl {d : ℕ} {c : SpeedOfLight} :
    toTimeAndSpace (d := d) c (Lorentz.Vector.basis (Sum.inl 0)) = (⟨1/c.val⟩, 0) := byd:ℕc:SpeedOfLight⊢ (toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0)) = ({ val := 1 / c.val }, 0)
  refine Prod.ext ?_ ?_refine_1d:ℕc:SpeedOfLight⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0))).1 = ({ val := 1 / c.val }, 0).1refine_2d:ℕc:SpeedOfLight⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0))).2 = ({ val := 1 / c.val }, 0).2
  ·refine_1d:ℕc:SpeedOfLight⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0))).1 = ({ val := 1 / c.val }, 0).1 simp [toTimeAndSpace, time]All goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLight⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0))).2 = ({ val := 1 / c.val }, 0).2 ext jrefine_2d:ℕc:SpeedOfLightj:Fin d⊢ ((toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0))).2.val j = ({ val := 1 / c.val }, 0).2.val j
    simp [toTimeAndSpace, space]All goals completed! 🐙



lemma toTimeAndSpace_basis_inl' {d : ℕ} {c : SpeedOfLight} :
    toTimeAndSpace (d := d) c (Lorentz.Vector.basis (Sum.inl 0)) = (1/c.val) • (1, 0) := byd:ℕc:SpeedOfLight⊢ (toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inl 0)) = (1 / c.val) • (1, 0)
  rw [toTimeAndSpace_basis_inld:ℕc:SpeedOfLight⊢ ({ val := 1 / c.val }, 0) = (1 / c.val) • (1, 0)d:ℕc:SpeedOfLight⊢ ({ val := 1 / c.val }, 0) = (1 / c.val) • (1, 0)]d:ℕc:SpeedOfLight⊢ ({ val := 1 / c.val }, 0) = (1 / c.val) • (1, 0)
  simp [Prod.ext_iff, Time.ext_iff, Time.smul_real_val, Time.one_val]All goals completed! 🐙

B.4. Time space basis

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

def timeSpaceBasis {d : ℕ} (c : SpeedOfLight := 1) :
    Module.Basis (Fin 1 ⊕ Fin d) ℝ (SpaceTime d) where
  repr := (toTimeAndSpace (d := d) c).toLinearEquiv.trans <|
      (Time.basis.toBasis.prod (Space.basis (d := d)).toBasis).repr

B.4.1. Elements of the basis

@[simp]
lemma timeSpaceBasis_apply_inl {d : ℕ} (c : SpeedOfLight) :
    timeSpaceBasis (d := d) c (Sum.inl 0) = c.val • Lorentz.Vector.basis (Sum.inl 0) := byd:ℕc:SpeedOfLight⊢ (timeSpaceBasis c) (Sum.inl 0) = c.val • Lorentz.Vector.basis (Sum.inl 0)
  simp [timeSpaceBasis]d:ℕc:SpeedOfLight⊢ (toTimeAndSpace c).symm (1, 0) = c.val • Lorentz.Vector.basis (Sum.inl 0)
  apply (toTimeAndSpace (d := d) c).injectived:ℕc:SpeedOfLight⊢ (toTimeAndSpace c) ((toTimeAndSpace c).symm (1, 0)) = (toTimeAndSpace c) (c.val • Lorentz.Vector.basis (Sum.inl 0))
  simp only [ContinuousLinearEquiv.apply_symm_apply, map_smul, toTimeAndSpace_basis_inl]d:ℕc:SpeedOfLight⊢ (1, 0) = c.val • ({ val := 1 / c.val }, 0)
  extfstd:ℕc:SpeedOfLight⊢ (1, 0).1.val = (c.val • ({ val := 1 / c.val }, 0)).1.valsndd:ℕc:SpeedOfLighti✝:Fin d⊢ (1, 0).2.val i✝ = (c.val • ({ val := 1 / c.val }, 0)).2.val i✝ <;>fstd:ℕc:SpeedOfLight⊢ (1, 0).1.val = (c.val • ({ val := 1 / c.val }, 0)).1.valsndd:ℕc:SpeedOfLighti✝:Fin d⊢ (1, 0).2.val i✝ = (c.val • ({ val := 1 / c.val }, 0)).2.val i✝ simpAll goals completed! 🐙

@[simp]
lemma timeSpaceBasis_apply_inr {d : ℕ} (c : SpeedOfLight) (i : Fin d) :
    timeSpaceBasis (d := d) c (Sum.inr i) = Lorentz.Vector.basis (Sum.inr i) := byd:ℕc:SpeedOfLighti:Fin d⊢ (timeSpaceBasis c) (Sum.inr i) = Lorentz.Vector.basis (Sum.inr i)
  simp [timeSpaceBasis]d:ℕc:SpeedOfLighti:Fin d⊢ (toTimeAndSpace c).symm (0, Space.basis i) = Lorentz.Vector.basis (Sum.inr i)
  apply (toTimeAndSpace (d := d) c).injectived:ℕc:SpeedOfLighti:Fin d⊢ (toTimeAndSpace c) ((toTimeAndSpace c).symm (0, Space.basis i)) = (toTimeAndSpace c) (Lorentz.Vector.basis (Sum.inr i))
  simp only [ContinuousLinearEquiv.apply_symm_apply, toTimeAndSpace_basis_inr]All goals completed! 🐙

B.4.2. Equivalence adjusting time basis vector

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

def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) :
    SpaceTime d ≃L[ℝ] SpaceTime d where
  toFun x := fun μ =>
    match μ with
    | Sum.inl 0 => c.val * x (Sum.inl 0)
    | Sum.inr i => x (Sum.inr i)
  invFun x := fun μ =>
    match μ with
    | Sum.inl 0 => (1 / c.val) * x (Sum.inl 0)
    | Sum.inr i => x (Sum.inr i)
  left_inv x := byd:ℕc:SpeedOfLightx:SpaceTime d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x) =
  x
    funext μd:ℕc:SpeedOfLightx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x)
    μ =
  x μ
    match μ with
    | Sum.inl 0 =>d:ℕc:SpeedOfLightx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x)
    (Sum.inl 0) =
  x (Sum.inl 0)
      field_simpAll goals completed! 🐙
    | Sum.inr i =>d:ℕc:SpeedOfLightx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x)
    (Sum.inr i) =
  x (Sum.inr i)
      rflAll goals completed! 🐙
  right_inv x := byd:ℕc:SpeedOfLightx:SpaceTime d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x) =
  x
    funext μd:ℕc:SpeedOfLightx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x)
    μ =
  x μ
    match μ with
    | Sum.inl 0 =>d:ℕc:SpeedOfLightx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x)
    (Sum.inl 0) =
  x (Sum.inl 0)
      field_simpAll goals completed! 🐙
    | Sum.inr i =>d:ℕc:SpeedOfLightx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ (fun x μ =>
      match μ with
      | Sum.inl 0 => c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    ((fun x μ =>
        match μ with
        | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i))
      x)
    (Sum.inr i) =
  x (Sum.inr i)
      rflAll goals completed! 🐙
  map_add' x y := byd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime d⊢ (fun μ =>
    match μ with
    | Sum.inl 0 => c.val * (x + y) (Sum.inl 0)
    | Sum.inr i => (x + y) (Sum.inr i)) =
  (fun μ =>
      match μ with
      | Sum.inl 0 => c.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i)) +
    fun μ =>
    match μ with
    | Sum.inl 0 => c.val * y (Sum.inl 0)
    | Sum.inr i => y (Sum.inr i)
    funext μd:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (match μ with
  | Sum.inl 0 => c.val * (x + y) (Sum.inl 0)
  | Sum.inr i => (x + y) (Sum.inr i)) =
  ((fun μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i)) +
      fun μ =>
      match μ with
      | Sum.inl 0 => c.val * y (Sum.inl 0)
      | Sum.inr i => y (Sum.inr i))
    μ
    match μ with
    | Sum.inl 0 =>d:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (match Sum.inl 0 with
  | Sum.inl 0 => c.val * (x + y) (Sum.inl 0)
  | Sum.inr i => (x + y) (Sum.inr i)) =
  ((fun μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i)) +
      fun μ =>
      match μ with
      | Sum.inl 0 => c.val * y (Sum.inl 0)
      | Sum.inr i => y (Sum.inr i))
    (Sum.inl 0)
      simp only [Fin.isValue, Lorentz.Vector.apply_add]d:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ c.val * (x (Sum.inl 0) + y (Sum.inl 0)) = c.val * x (Sum.inl 0) + c.val * y (Sum.inl 0)
      ringAll goals completed! 🐙
    | Sum.inr i =>d:ℕc:SpeedOfLightx:SpaceTime dy:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ (match Sum.inr i with
  | Sum.inl 0 => c.val * (x + y) (Sum.inl 0)
  | Sum.inr i => (x + y) (Sum.inr i)) =
  ((fun μ =>
        match μ with
        | Sum.inl 0 => c.val * x (Sum.inl 0)
        | Sum.inr i => x (Sum.inr i)) +
      fun μ =>
      match μ with
      | Sum.inl 0 => c.val * y (Sum.inl 0)
      | Sum.inr i => y (Sum.inr i))
    (Sum.inr i)
      simpAll goals completed! 🐙
  map_smul' c x := byd:ℕc✝:SpeedOfLightc:ℝx:SpaceTime d⊢ (fun μ =>
    match μ with
    | Sum.inl 0 => c✝.val * (c • x) (Sum.inl 0)
    | Sum.inr i => (c • x) (Sum.inr i)) =
  (RingHom.id ℝ) c • fun μ =>
    match μ with
    | Sum.inl 0 => c✝.val * x (Sum.inl 0)
    | Sum.inr i => x (Sum.inr i)
    funext μd:ℕc✝:SpeedOfLightc:ℝx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (match μ with
  | Sum.inl 0 => c✝.val * (c • x) (Sum.inl 0)
  | Sum.inr i => (c • x) (Sum.inr i)) =
  ((RingHom.id ℝ) c • fun μ =>
      match μ with
      | Sum.inl 0 => c✝.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    μ
    match μ with
    | Sum.inl 0 =>d:ℕc✝:SpeedOfLightc:ℝx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (match Sum.inl 0 with
  | Sum.inl 0 => c✝.val * (c • x) (Sum.inl 0)
  | Sum.inr i => (c • x) (Sum.inr i)) =
  ((RingHom.id ℝ) c • fun μ =>
      match μ with
      | Sum.inl 0 => c✝.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    (Sum.inl 0)
      simp only [Fin.isValue, Lorentz.Vector.apply_smul, RingHom.id_apply]d:ℕc✝:SpeedOfLightc:ℝx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ c✝.val * (c * x (Sum.inl 0)) = c * (c✝.val * x (Sum.inl 0))
      ringAll goals completed! 🐙
    | Sum.inr i =>d:ℕc✝:SpeedOfLightc:ℝx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ (match Sum.inr i with
  | Sum.inl 0 => c✝.val * (c • x) (Sum.inl 0)
  | Sum.inr i => (c • x) (Sum.inr i)) =
  ((RingHom.id ℝ) c • fun μ =>
      match μ with
      | Sum.inl 0 => c✝.val * x (Sum.inl 0)
      | Sum.inr i => x (Sum.inr i))
    (Sum.inr i)
      simpAll goals completed! 🐙
  continuous_invFun := byd:ℕc:SpeedOfLight⊢ Continuous fun x μ =>
  match μ with
  | Sum.inl 0 => 1 / c.val * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
    simp only [one_div, Fin.isValue]d:ℕc:SpeedOfLight⊢ Continuous fun x μ =>
  match μ with
  | Sum.inl 0 => c.val⁻¹ * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
    apply Lorentz.Vector.continuous_of_applyd:ℕc:SpeedOfLight⊢ ∀ (i : Fin 1 ⊕ Fin d),
  Continuous fun x =>
    match i with
    | Sum.inl 0 => c.val⁻¹ * x (Sum.inl 0)
    | Sum.inr i => x (Sum.inr i)
    intro μd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ Continuous fun x =>
  match μ with
  | Sum.inl 0 => c.val⁻¹ * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
    match μ with
    | Sum.inl 0 =>d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ Continuous fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => c.val⁻¹ * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
      simp only [Fin.isValue]d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ Continuous fun x => c.val⁻¹ * x (Sum.inl 0)
      fun_propAll goals completed! 🐙
    | Sum.inr i =>d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin d⊢ Continuous fun x =>
  match Sum.inr i with
  | Sum.inl 0 => c.val⁻¹ * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
      simp onlyd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin d⊢ Continuous fun x => x (Sum.inr i)
      fun_propAll goals completed! 🐙
  continuous_toFun := byd:ℕc:SpeedOfLight⊢ Continuous fun x μ =>
  match μ with
  | Sum.inl 0 => c.val * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
    apply Lorentz.Vector.continuous_of_applyd:ℕc:SpeedOfLight⊢ ∀ (i : Fin 1 ⊕ Fin d),
  Continuous fun x =>
    match i with
    | Sum.inl 0 => c.val * x (Sum.inl 0)
    | Sum.inr i => x (Sum.inr i)
    intro μd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ Continuous fun x =>
  match μ with
  | Sum.inl 0 => c.val * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
    match μ with
    | Sum.inl 0 =>d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ Continuous fun x =>
  match Sum.inl 0 with
  | Sum.inl 0 => c.val * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
      simp only [Fin.isValue]d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ Continuous fun x => c.val * x (Sum.inl 0)
      fun_propAll goals completed! 🐙
    | Sum.inr i =>d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin d⊢ Continuous fun x =>
  match Sum.inr i with
  | Sum.inl 0 => c.val * x (Sum.inl 0)
  | Sum.inr i => x (Sum.inr i)
      simp onlyd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin d⊢ Continuous fun x => x (Sum.inr i)
      fun_propAll goals completed! 🐙

B.4.3. Determinant of the equivalence



lemma det_timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) :
    (timeSpaceBasisEquiv (d := d) c).det = c.val := byd:ℕc:SpeedOfLight⊢ ↑(LinearEquiv.det ↑(timeSpaceBasisEquiv c)) = c.val
  rw [@LinearEquiv.coe_detd:ℕc:SpeedOfLight⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) = c.vald:ℕc:SpeedOfLight⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) = c.val]d:ℕc:SpeedOfLight⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) = c.val
  let e := toTimeAndSpace (d := d) cd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace c⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) = c.val
  trans LinearMap.det (e.toLinearMap ∘ₗ (timeSpaceBasisEquiv (d := d) c).toLinearMap ∘ₗ
    e.symm.toLinearMap)d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace c⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) = LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm)d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace c⊢ LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) = c.val
  ·d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace c⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) = LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) simp only [ContinuousLinearEquiv.toLinearEquiv_symm, LinearMap.det_conj]All goals completed! 🐙
  have h1 : e.toLinearMap ∘ₗ (timeSpaceBasisEquiv (d := d) c).toLinearMap ∘ₗ
    e.symm.toLinearMap = (c.val • LinearMap.id).prodMap LinearMap.id := byd:ℕc:SpeedOfLight⊢ ↑(LinearEquiv.det ↑(timeSpaceBasisEquiv c)) = c.vald:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) = c.val
    ext txhl.fstd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Time⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).1.val =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).1.valhl.sndd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Timei✝:Fin d⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).2.val i✝ =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).2.val i✝hr.fstd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Space d⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).1.val =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).1.valhr.sndd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Space di✝:Fin d⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).2.val i✝ =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).2.val i✝d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) = c.val <;>hl.fstd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Time⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).1.val =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).1.valhl.sndd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Timei✝:Fin d⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).2.val i✝ =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inl ℝ Time (Space d)) tx).2.val i✝hr.fstd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Space d⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).1.val =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).1.valhr.sndd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ctx:Space di✝:Fin d⊢ (((↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).2.val i✝ =
  (((c.val • LinearMap.id).prodMap LinearMap.id ∘ₗ LinearMap.inr ℝ Time (Space d)) tx).2.val i✝d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) = c.val simp [e, timeSpaceBasisEquiv, toTimeAndSpace, space]d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) = c.vald:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm) = c.val
  rw [h1,d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det ((c.val • LinearMap.id).prodMap LinearMap.id) = c.vald:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (c.val • LinearMap.id) * LinearMap.det LinearMap.id = c.val LinearMap.det_prodMapd:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (c.val • LinearMap.id) * LinearMap.det LinearMap.id = c.vald:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (c.val • LinearMap.id) * LinearMap.det LinearMap.id = c.val]d:ℕc:SpeedOfLighte:SpaceTime d ≃L[ℝ] Time × Space d := toTimeAndSpace ch1:↑↑e ∘ₗ ↑↑(timeSpaceBasisEquiv c) ∘ₗ ↑↑e.symm = (c.val • LinearMap.id).prodMap LinearMap.id⊢ LinearMap.det (c.val • LinearMap.id) * LinearMap.det LinearMap.id = c.val
  simpAll goals completed! 🐙

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

lemma timeSpaceBasis_eq_map_basis {d : ℕ} (c : SpeedOfLight) :
    timeSpaceBasis (d := d) c =
    Module.Basis.map (Lorentz.Vector.basis (d := d)) (timeSpaceBasisEquiv c).toLinearEquiv := byd:ℕc:SpeedOfLight⊢ timeSpaceBasis c = Lorentz.Vector.basis.map ↑(timeSpaceBasisEquiv c)
  ext1 μd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ (timeSpaceBasis c) μ = (Lorentz.Vector.basis.map ↑(timeSpaceBasisEquiv c)) μ
  match μ with
  | Sum.inl 0 =>d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ (timeSpaceBasis c) (Sum.inl 0) = (Lorentz.Vector.basis.map ↑(timeSpaceBasisEquiv c)) (Sum.inl 0)
    simp [timeSpaceBasisEquiv]d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin d⊢ c.val • Lorentz.Vector.basis (Sum.inl 0) = fun μ =>
  match μ with
  | Sum.inl 0 => c.val
  | Sum.inr i => 0
    funext νd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (c.val • Lorentz.Vector.basis (Sum.inl 0)) ν =
  match ν with
  | Sum.inl 0 => c.val
  | Sum.inr i => 0
    rcases ν with _ | jinld:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ (c.val • Lorentz.Vector.basis (Sum.inl 0)) (Sum.inl val✝) =
  match Sum.inl val✝ with
  | Sum.inl 0 => c.val
  | Sum.inr i => 0inrd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin dj:Fin d⊢ (c.val • Lorentz.Vector.basis (Sum.inl 0)) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => c.val
  | Sum.inr i => 0 <;>inld:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin dval✝:Fin 1⊢ (c.val • Lorentz.Vector.basis (Sum.inl 0)) (Sum.inl val✝) =
  match Sum.inl val✝ with
  | Sum.inl 0 => c.val
  | Sum.inr i => 0inrd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin dj:Fin d⊢ (c.val • Lorentz.Vector.basis (Sum.inl 0)) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => c.val
  | Sum.inr i => 0 simp [Fin.fin_one_eq_zero]All goals completed! 🐙
  | Sum.inr i =>d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin d⊢ (timeSpaceBasis c) (Sum.inr i) = (Lorentz.Vector.basis.map ↑(timeSpaceBasisEquiv c)) (Sum.inr i)
    simp [timeSpaceBasisEquiv]d:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin d⊢ Lorentz.Vector.basis (Sum.inr i) = fun μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i_1 => if i = i_1 then 1 else 0
    funext νd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin dν:Fin 1 ⊕ Fin d⊢ Lorentz.Vector.basis (Sum.inr i) ν =
  match ν with
  | Sum.inl 0 => 0
  | Sum.inr i_1 => if i = i_1 then 1 else 0
    rcases ν with _ | jinld:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin dval✝:Fin 1⊢ Lorentz.Vector.basis (Sum.inr i) (Sum.inl val✝) =
  match Sum.inl val✝ with
  | Sum.inl 0 => 0
  | Sum.inr i_1 => if i = i_1 then 1 else 0inrd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin dj:Fin d⊢ Lorentz.Vector.basis (Sum.inr i) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => 0
  | Sum.inr i_1 => if i = i_1 then 1 else 0 <;>inld:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin dval✝:Fin 1⊢ Lorentz.Vector.basis (Sum.inr i) (Sum.inl val✝) =
  match Sum.inl val✝ with
  | Sum.inl 0 => 0
  | Sum.inr i_1 => if i = i_1 then 1 else 0inrd:ℕc:SpeedOfLightμ:Fin 1 ⊕ Fin di:Fin dj:Fin d⊢ Lorentz.Vector.basis (Sum.inr i) (Sum.inr j) =
  match Sum.inr j with
  | Sum.inl 0 => 0
  | Sum.inr i_1 => if i = i_1 then 1 else 0 simp [Fin.fin_one_eq_zero]All goals completed! 🐙

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



lemma timeSpaceBasis_addHaar {d : ℕ} (c : SpeedOfLight := 1) :
    (timeSpaceBasis (d := d) c).addHaar = (ENNReal.ofReal (c⁻¹)) • volume := byd:ℕc:SpeedOfLight⊢ (timeSpaceBasis c).addHaar = ENNReal.ofReal c.val⁻¹ • volume
  rw [timeSpaceBasis_eq_map_basis c,d:ℕc:SpeedOfLight⊢ (Lorentz.Vector.basis.map ↑(timeSpaceBasisEquiv c)).addHaar = ENNReal.ofReal c.val⁻¹ • volumed:ℕc:SpeedOfLight⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume ← Module.Basis.map_addHaard:ℕc:SpeedOfLight⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volumed:ℕc:SpeedOfLight⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume]d:ℕc:SpeedOfLight⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume
  have h1 := MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar
    (f := (timeSpaceBasisEquiv (d := d) c).toLinearMap) (μ := Lorentz.Vector.basis.addHaar)
    (byd:ℕc:SpeedOfLight⊢ LinearMap.det ↑↑(timeSpaceBasisEquiv c) ≠ 0d:ℕc:SpeedOfLighth1:Measure.map (⇑↑↑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |(LinearMap.det ↑↑(timeSpaceBasisEquiv c))⁻¹| • Lorentz.Vector.basis.addHaar⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume simp [← LinearEquiv.coe_det, det_timeSpaceBasisEquiv]All goals completed! 🐙d:ℕc:SpeedOfLighth1:Measure.map (⇑↑↑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |(LinearMap.det ↑↑(timeSpaceBasisEquiv c))⁻¹| • Lorentz.Vector.basis.addHaar⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume)d:ℕc:SpeedOfLighth1:Measure.map (⇑↑↑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |(LinearMap.det ↑↑(timeSpaceBasisEquiv c))⁻¹| • Lorentz.Vector.basis.addHaar⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume
  simp at h1d:ℕc:SpeedOfLighth1:Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar⊢ Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar = ENNReal.ofReal c.val⁻¹ • volume
  rw [h1d:ℕc:SpeedOfLighth1:Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar⊢ ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal c.val⁻¹ • volumed:ℕc:SpeedOfLighth1:Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar⊢ ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal c.val⁻¹ • volume]d:ℕc:SpeedOfLighth1:Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar⊢ ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal c.val⁻¹ • volume
  simp [← LinearEquiv.coe_det, det_timeSpaceBasisEquiv]d:ℕc:SpeedOfLighth1:Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar⊢ (ENNReal.ofReal |c.val|)⁻¹ • Lorentz.Vector.basis.addHaar = (ENNReal.ofReal c.val)⁻¹ • volume
  congre_ad:ℕc:SpeedOfLighth1:Measure.map (⇑(timeSpaceBasisEquiv c)) Lorentz.Vector.basis.addHaar =
  ENNReal.ofReal |LinearMap.det ↑↑(timeSpaceBasisEquiv c)|⁻¹ • Lorentz.Vector.basis.addHaar⊢ |c.val| = c.val
  simpAll goals completed! 🐙

B.5. Integrals over `SpaceTime d`

B.5.1. Measure preserving property of `toTimeAndSpace.symm`


lemma toTimeAndSpace_symm_measurePreserving {d : ℕ} (c : SpeedOfLight) :
    MeasurePreserving (toTimeAndSpace c).symm (volume.prod (volume (α := Space d)))
    (ENNReal.ofReal c⁻¹ • volume) := byd:ℕc:SpeedOfLight⊢ MeasurePreserving (⇑(toTimeAndSpace c).symm) (volume.prod volume) (ENNReal.ofReal c.val⁻¹ • volume)
  refine { measurable := ?_, map_eq := ?_ }refine_1d:ℕc:SpeedOfLight⊢ Measurable ⇑(toTimeAndSpace c).symmrefine_2d:ℕc:SpeedOfLight⊢ Measure.map (⇑(toTimeAndSpace c).symm) (volume.prod volume) = ENNReal.ofReal c.val⁻¹ • volume
  ·refine_1d:ℕc:SpeedOfLight⊢ Measurable ⇑(toTimeAndSpace c).symm fun_propAll goals completed! 🐙
  rw [Space.volume_eq_addHaar,refine_2d:ℕc:SpeedOfLight⊢ Measure.map (⇑(toTimeAndSpace c).symm) (volume.prod Space.basis.toBasis.addHaar) = ENNReal.ofReal c.val⁻¹ • volumerefine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaar Time.volume_eq_basis_addHaar,refine_2d:ℕc:SpeedOfLight⊢ Measure.map (⇑(toTimeAndSpace c).symm) (Time.basis.toBasis.addHaar.prod Space.basis.toBasis.addHaar) =
  ENNReal.ofReal c.val⁻¹ • volumerefine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaar ← Module.Basis.prod_addHaar,refine_2d:ℕc:SpeedOfLight⊢ Measure.map (⇑(toTimeAndSpace c).symm) (Time.basis.toBasis.prod Space.basis.toBasis).addHaar =
  ENNReal.ofReal c.val⁻¹ • volumerefine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaar
    Module.Basis.map_addHaar,refine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = ENNReal.ofReal c.val⁻¹ • volumerefine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaar ← timeSpaceBasis_addHaar crefine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaarrefine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaar]refine_2d:ℕc:SpeedOfLight⊢ ((Time.basis.toBasis.prod Space.basis.toBasis).map ↑(toTimeAndSpace c).symm).addHaar = (timeSpaceBasis c).addHaar
  rflAll goals completed! 🐙

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

              

lemma spaceTime_integral_eq_time_space_integral {M} [NormedAddCommGroup M]
    [NormedSpace ℝ M] {d : ℕ} (c : SpeedOfLight)
    (f : SpaceTime d → M) :
    ∫ x : SpaceTime d, f x ∂(volume) =
    c.val • ∫ tx : Time × Space d, f ((toTimeAndSpace c).symm tx) ∂(volume.prod volume) := byM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ∫ (x : SpaceTime d), f x = c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume
  symmM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x
  have h1 : ∫ tx : Time × Space d, f ((toTimeAndSpace c).symm tx) ∂(volume.prod volume)
    = ∫ x : SpaceTime d, f x ∂((ENNReal.ofReal (c⁻¹)) • volume) := byM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ∫ (x : SpaceTime d), f x = c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volumeM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x
    apply MeasureTheory.MeasurePreserving.integral_comph₁M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurePreserving (⇑(toTimeAndSpace c).symm) (volume.prod volume) (ENNReal.ofReal c.val⁻¹ • volume)h₂M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurableEmbedding ⇑(toTimeAndSpace c).symmM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x
    ·h₁M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurePreserving (⇑(toTimeAndSpace c).symm) (volume.prod volume) (ENNReal.ofReal c.val⁻¹ • volume)M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x exact toTimeAndSpace_symm_measurePreserving cAll goals completed! 🐙M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x
    ·h₂M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurableEmbedding ⇑(toTimeAndSpace c).symmM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x exact (toTimeAndSpace c).symm.toHomeomorph.measurableEmbeddingM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f xM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume = ∫ (x : SpaceTime d), f x
  rw [h1M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume = ∫ (x : SpaceTime d), f xM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume = ∫ (x : SpaceTime d), f x]M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh1:∫ (tx : Time × Space d), f ((toTimeAndSpace c).symm tx) ∂volume.prod volume =
  ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume⊢ c.val • ∫ (x : SpaceTime d), f x ∂ENNReal.ofReal c.val⁻¹ • volume = ∫ (x : SpaceTime d), f x
  simpAll goals completed! 🐙

lemma spaceTime_integrable_iff_space_time_integrable {M} [NormedAddCommGroup M]
    {d : ℕ} (c : SpeedOfLight)
    (f : SpaceTime d → M) :
    Integrable f volume ↔ Integrable (f ∘ ((toTimeAndSpace c).symm)) (volume.prod volume) := byM:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable f volume ↔ Integrable (f ∘ ⇑(toTimeAndSpace c).symm) (volume.prod volume)
  symmM:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable (f ∘ ⇑(toTimeAndSpace c).symm) (volume.prod volume) ↔ Integrable f volume
  trans Integrable f (ENNReal.ofReal (c⁻¹) • volume)M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable (f ∘ ⇑(toTimeAndSpace c).symm) (volume.prod volume) ↔ Integrable f (ENNReal.ofReal c.val⁻¹ • volume)M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable f (ENNReal.ofReal c.val⁻¹ • volume) ↔ Integrable f volume; swapM:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable f (ENNReal.ofReal c.val⁻¹ • volume) ↔ Integrable f volumeM:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable (f ∘ ⇑(toTimeAndSpace c).symm) (volume.prod volume) ↔ Integrable f (ENNReal.ofReal c.val⁻¹ • volume)
  ·M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable f (ENNReal.ofReal c.val⁻¹ • volume) ↔ Integrable f volume rw [MeasureTheory.integrable_smul_measureM:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ Integrable f volume ↔ Integrable f volumeh₁M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ 0h₂M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ ⊤h₁M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ 0h₂M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ ⊤]h₁M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ 0h₂M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ ⊤
    ·h₁M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ 0 simpAll goals completed! 🐙
    ·h₂M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ ENNReal.ofReal c.val⁻¹ ≠ ⊤ simpAll goals completed! 🐙
  apply MeasureTheory.MeasurePreserving.integrable_comp_embh₁M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurePreserving (⇑(toTimeAndSpace c).symm) (volume.prod volume) (ENNReal.ofReal c.val⁻¹ • volume)h₂M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurableEmbedding ⇑(toTimeAndSpace c).symm
  ·h₁M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurePreserving (⇑(toTimeAndSpace c).symm) (volume.prod volume) (ENNReal.ofReal c.val⁻¹ • volume) exact toTimeAndSpace_symm_measurePreserving cAll goals completed! 🐙
  ·h₂M:Type u_1inst✝:NormedAddCommGroup Md:ℕc:SpeedOfLightf:SpaceTime d → M⊢ MeasurableEmbedding ⇑(toTimeAndSpace c).symm exact (toTimeAndSpace c).symm.toHomeomorph.measurableEmbeddingAll goals completed! 🐙

lemma spaceTime_integral_eq_time_integral_space_integral {M} [NormedAddCommGroup M]
    [NormedSpace ℝ M] {d : ℕ} (c : SpeedOfLight)
    (f : SpaceTime d → M)
    (h : Integrable f volume) :
    ∫ x : SpaceTime d, f x =
    c.val • ∫ t : Time, ∫ x : Space d, f ((toTimeAndSpace c).symm (t, x)) := byM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ ∫ (x : SpaceTime d), f x = c.val • ∫ (t : Time) (x : Space d), f ((toTimeAndSpace c).symm (t, x))
  rw [spaceTime_integral_eq_time_space_integral,M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLight.val ?c • ∫ (tx : Time × Space d), f ((toTimeAndSpace ?c).symm tx) ∂volume.prod volume =
  c.val • ∫ (t : Time) (x : Space d), f ((toTimeAndSpace c).symm (t, x))cM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLighthfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace c).symm tx)) (volume.prod volume) MeasureTheory.integral_prodM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLight.val ?c • ∫ (x : Time) (y : Space d), f ((toTimeAndSpace ?c).symm (x, y)) =
  c.val • ∫ (t : Time) (x : Space d), f ((toTimeAndSpace c).symm (t, x))hfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace ?c).symm tx)) (volume.prod volume)cM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLighthfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace c).symm tx)) (volume.prod volume)]hfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace c).symm tx)) (volume.prod volume)
  exact (spaceTime_integrable_iff_space_time_integrable c f).mp hAll goals completed! 🐙

lemma spaceTime_integral_eq_space_integral_time_integral {M} [NormedAddCommGroup M]
    [NormedSpace ℝ M] {d : ℕ} (c : SpeedOfLight)
    (f : SpaceTime d → M)
    (h : Integrable f volume) :
    ∫ x : SpaceTime d, f x =
    c.val • ∫ x : Space d, ∫ t : Time, f ((toTimeAndSpace c).symm (t, x)) := byM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ ∫ (x : SpaceTime d), f x = c.val • ∫ (x : Space d) (t : Time), f ((toTimeAndSpace c).symm (t, x))
  rw [spaceTime_integral_eq_time_space_integral,M:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLight.val ?c • ∫ (tx : Time × Space d), f ((toTimeAndSpace ?c).symm tx) ∂volume.prod volume =
  c.val • ∫ (x : Space d) (t : Time), f ((toTimeAndSpace c).symm (t, x))cM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLighthfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace c).symm tx)) (volume.prod volume) MeasureTheory.integral_prod_symmM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLight.val ?c • ∫ (y : Space d) (x : Time), f ((toTimeAndSpace ?c).symm (x, y)) =
  c.val • ∫ (x : Space d) (t : Time), f ((toTimeAndSpace c).symm (t, x))hfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace ?c).symm tx)) (volume.prod volume)cM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ SpeedOfLighthfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace c).symm tx)) (volume.prod volume)]hfM:Type u_1inst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕc:SpeedOfLightf:SpaceTime d → Mh:Integrable f volume⊢ Integrable (fun tx => f ((toTimeAndSpace c).symm tx)) (volume.prod volume)
  exact (spaceTime_integrable_iff_space_time_integrable c f).mp hAll goals completed! 🐙

Spacetime

i. Overview

ii. Key results

iii. Table of contents

iv. References

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

A. The definition of `SpaceTime d`

D. Measures on `SpaceTime d`

B. Maps to and from `Space` and `Time`

B.1. Linear map to `Space d`

B.2. Linear map to `Time`

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.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`