PhysLean Documentation

PhysLean.Relativity.SpaceTime.ProperTime

Proper Time #

This file introduces 4d Minkowski spacetime.

source
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
Instances For
    source
    theorem SpaceTime.properTime_pos_ofTimeLike {d : ℕ} (q p : SpaceTime d) (h : Lorentz.Vector.causalCharacter (p - q) = Lorentz.Vector.CausalCharacter.timeLike) :
    0 < q.properTime p
    source
    theorem SpaceTime.properTime_zero_ofLightLike {d : ℕ} (q p : SpaceTime d) (h : Lorentz.Vector.causalCharacter (p - q) = Lorentz.Vector.CausalCharacter.lightLike) :
    q.properTime p = 0
    source
    theorem SpaceTime.properTime_zero_ofSpaceLike {d : ℕ} (q p : SpaceTime d) (h : Lorentz.Vector.causalCharacter (p - q) = Lorentz.Vector.CausalCharacter.spaceLike) :
    q.properTime p = 0