spatialRadius_ne_zero_iff

formal source

 154  unfold spatialRadius
 155  rw [Real.sqrt_pos]
 156
 157theorem spatialRadius_ne_zero_iff (x : Fin 4 → ℝ) : spatialRadius x ≠ 0 ↔ spatialNormSq x ≠ 0 := by
 158  unfold spatialRadius
 159  rw [Real.sqrt_ne_zero (spatialNormSq_nonneg x)]
 160
 161/-- Nonzero spatial radius is automatically positive. -/
 162theorem spatialRadius_pos_of_ne_zero (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
 163    0 < spatialRadius x := by
 164  have h_ne : spatialNormSq x ≠ 0 := (spatialRadius_ne_zero_iff x).mp hx
 165  exact (spatialRadius_pos_iff x).2 (lt_of_le_of_ne (spatialNormSq_nonneg x) h_ne.symm)
 166
 167/-- Temporal coordinate ray doesn't change spatial components. -/
 168lemma coordRay_temporal_spatial (x : Fin 4 → ℝ) (s : ℝ) (i : Fin 4) (hi : i ≠ 0) :
 169    (coordRay x 0 s) i = x i := by
 170  simp [coordRay, basisVec, hi]
 171
 172/-- spatialNormSq is invariant under temporal coordinate ray. -/
 173lemma spatialNormSq_coordRay_temporal (x : Fin 4 → ℝ) (s : ℝ) :
 174    spatialNormSq (coordRay x 0 s) = spatialNormSq x := by
 175  unfold spatialNormSq
 176  have h1 : (coordRay x 0 s) 1 = x 1 := coordRay_temporal_spatial x s 1 (by decide)
 177  have h2 : (coordRay x 0 s) 2 = x 2 := coordRay_temporal_spatial x s 2 (by decide)
 178  have h3 : (coordRay x 0 s) 3 = x 3 := coordRay_temporal_spatial x s 3 (by decide)
 179  rw [h1, h2, h3]
 180
 181/-- spatialRadius is invariant under temporal coordinate ray. -/
 182lemma spatialRadius_coordRay_temporal (x : Fin 4 → ℝ) (s : ℝ) :
 183    spatialRadius (coordRay x 0 s) = spatialRadius x := by
 184  unfold spatialRadius
 185  rw [spatialNormSq_coordRay_temporal]
 186
 187/-- For any spatial index `i ∈ {1,2,3}`, `x_i² ≤ spatialNormSq x`. -/