PhysLean Documentation

PhysLean.Relativity.Tensors.RealTensor.Vector.Causality.LightLike

Properties of light like vectors #

@[simp]

Causally preceding is reflexive

For two lightlike vectors with equal time components, their spatial parts have equal Euclidean norms

theorem Lorentz.Vector.lightlike_spatial_parallel_implies_proportional {d : } {v w : Vector d} (hv : v.causalCharacter = CausalCharacter.lightLike) (hw : w.causalCharacter = CausalCharacter.lightLike) (h_spatial_parallel : ∃ (r : ), v = r w) :
∃ (r : ), |v (Sum.inl 0)| = |r| * |w (Sum.inl 0)|

If two lightlike vectors have parallel spatial components, their temporal components must also be proportional, which implies the entire vectors are proportional