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 tod+1
dimensional spacetime.toTimeAndSpace
: A continuous linear equivalence betweenSpaceTime d
andTime × Space d
.deriv
: The derivative of a functionSpaceTime d → M
along theμ
coordinte.deriv_sum_inr
: The derivative along a spatial coordinate in terms of the derivative onSpace d
.deriv_sum_inl
: The derivative along the temporal coordinate in terms of the derivative onTime
.innerProductSpace
: The Euclidean inner product structure onSpaceTime d
.
iii. Table of contents #
- A. The definition of
SpaceTime d
- B. Maps to and from
Space
andTime
- 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 toTime × 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 temperal basis vectors
- B.3.1. Derivative of
- B.1. Linear map to
- C. Continous linear map to coordinates
- D. Derivatives of functions on
SpaceTime d
- D.1. The definition of the derivative
- D.2. Basic equality lemmas
- D.3. Derivative of the zero function
- D.4. The derivative of a function composed with a Lorentz transformation
- D.5. Spacetime derivatives in terms of time and space derivatives
- E. Measures on
SpaceTime d
- E.1. Instance of a measureable space
- E.2. Instance of a borel space
- E.3. Definition of an inner product space structure on
SpaceTime d
- E.4. Instance of a measure space
- E.5. Volume measure is positive on non-empty open sets
- E.6. Volume measure is a finite measure on compact sets
- E.7. Volume measure is an additive Haar measure
iv. References #
The space part of spacetime.
Equations
- SpaceTime.space = { toFun := fun (x : SpaceTime d) => Lorentz.Vector.spatialPart x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
B.1.1. Explicit expansion of map to space #
B.1.2. Equivariance of the to space under rotations #
The function space
is equivariant with respect to rotations.
Instances For
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 temperal basis vectors #
C. Continous 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
.
Equations
- SpaceTime.coord μ = { toFun := fun (x : SpaceTime d) => x (finSumFinEquiv.symm μ), map_add' := ⋯, map_smul' := ⋯ }
Instances For
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 "𝔁")
Instances For
D.1. The definition of the derivative #
The derivative of a function SpaceTime d → ℝ
along the μ
coordinte.
Equations
- SpaceTime.deriv μ f y = (fderiv ℝ f y) (Lorentz.Vector.basis μ)
Instances For
The derivative of a function SpaceTime d → ℝ
along the μ
coordinte.
Equations
- SpaceTime.«term∂_» = Lean.ParserDescr.node `SpaceTime.«term∂_» 1024 (Lean.ParserDescr.symbol "∂_")
Instances For
D.2. Basic equality lemmas #
D.3. Derivative of the zero function #
D.4. The derivative of a function composed with a Lorentz transformation #
D.5. Spacetime derivatives in terms of time and space derivatives #
E.1. Instance of a measureable space #
Equations
E.2. Instance of a borel space #
The Euclidean inner product structure on SpaceTime
.
Equations
- SpaceTime.innerProductSpace d = inferInstanceAs (InnerProductSpace ℝ (EuclideanSpace ℝ (Fin 1 ⊕ Fin d)))
E.4. Instance of a measure space #
Equations
- SpaceTime.instMeasureSpace = { toMeasurableSpace := SpaceTime.instMeasurableSpace, volume := Lorentz.Vector.basis.addHaar }