Proper Time

This file introduces 4d Minkowski spacetime.

def SpaceTime.properTime {d : ℕ} (q p : SpaceTime d) : ℝ

The proper time from q to p. Defaults to zero if p and q have a space-like separation.

Equations

• q.properTime p = √((Lorentz.Vector.minkowskiProduct (p - q)) (p - q))

theorem SpaceTime.properTime_pos_ofTimeLike {d : ℕ} (q p : SpaceTime d) (h : Lorentz.Vector.causalCharacter (p - q) = Lorentz.Vector.CausalCharacter.timeLike) : 0 < q.properTime p

theorem SpaceTime.properTime_zero_ofLightLike {d : ℕ} (q p : SpaceTime d) (h : Lorentz.Vector.causalCharacter (p - q) = Lorentz.Vector.CausalCharacter.lightLike) : q.properTime p = 0

theorem SpaceTime.properTime_zero_ofSpaceLike {d : ℕ} (q p : SpaceTime d) (h : Lorentz.Vector.causalCharacter (p - q) = Lorentz.Vector.CausalCharacter.spaceLike) : q.properTime p = 0