Properties of time like vectors

@[simp]

theorem Lorentz.Vector.timelike_neg_time_component_product {d : ℕ} (v w : Vector d) (hv_neg : toCoord v (Sum.inl 0) < 0) (hw_neg : toCoord w (Sum.inl 0) < 0) : toCoord v (Sum.inl 0) * toCoord w (Sum.inl 0) > 0

For timelike vectors with negative time components, their time components multiply to give a positive number

theorem Lorentz.Vector.timeLike_iff_norm_sq_pos {d : ℕ} (p : Vector d) : p.causalCharacter = CausalCharacter.timeLike ↔ 0 < ⟪p, p⟫ₘ

For timelike vectors, the Minkowski inner product is positive

theorem Lorentz.Vector.timelike_time_dominates_space {d : ℕ} {v : Vector d} (hv : v.causalCharacter = CausalCharacter.timeLike) : inner v.spatialPart v.spatialPart < v.timeComponent * v.timeComponent

For timeLike vectors in Minkowski space, the inner product of the spatial part is less than the square of the time component

@[simp]

theorem Lorentz.Vector.time_component_ne_zero_of_timelike {d : ℕ} {v : Vector d} (hv : v.causalCharacter = CausalCharacter.timeLike) : toCoord v (Sum.inl 0) ≠ 0

For nonzero timelike vectors, the time component is nonzero

@[simp]

theorem Lorentz.Vector.timelike_time_component_ne_zero {d : ℕ} {v : Vector d} (hv : v.causalCharacter = CausalCharacter.timeLike) : v.timeComponent ≠ 0

For timelike vectors, the time component is nonzero

theorem Lorentz.Vector.timeLike_iff_time_lt_space {d : ℕ} {v : Vector d} : v.causalCharacter = CausalCharacter.timeLike ↔ inner v.spatialPart v.spatialPart < toCoord v (Sum.inl 0) * toCoord v (Sum.inl 0)

A vector is timelike if and only if its time component squared is less than the sum of its spatial components squared

@[simp]

theorem Lorentz.Vector.timeComponent_squared_pos_of_timelike {d : ℕ} {v : Vector d} (hv : v.causalCharacter = CausalCharacter.timeLike) : 0 < v.timeComponent ^ 2

Time component squared is positive for timelike vectors

theorem Lorentz.Vector.timelike_spatial_lt_time_squared {d : ℕ} {v : Vector d} (hv : v.causalCharacter = CausalCharacter.timeLike) : inner v.spatialPart v.spatialPart < v.timeComponent ^ 2

For timelike vectors, the spatial norm squared is strictly less than the time component squared