spatialNormSq_coordRay_temporal

formal source

 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`. -/
 188private lemma sq_le_spatialNormSq_1 (x : Fin 4 → ℝ) :
 189    x 1 ^ 2 ≤ spatialNormSq x := by
 190  unfold spatialNormSq; nlinarith [sq_nonneg (x 2), sq_nonneg (x 3)]
 191
 192private lemma sq_le_spatialNormSq_2 (x : Fin 4 → ℝ) :
 193    x 2 ^ 2 ≤ spatialNormSq x := by
 194  unfold spatialNormSq; nlinarith [sq_nonneg (x 1), sq_nonneg (x 3)]
 195
 196private lemma sq_le_spatialNormSq_3 (x : Fin 4 → ℝ) :
 197    x 3 ^ 2 ≤ spatialNormSq x := by
 198  unfold spatialNormSq; nlinarith [sq_nonneg (x 1), sq_nonneg (x 2)]
 199
 200/-- Helper: closed form of `spatialNormSq (coordRay x j s)` when `j` is a fixed
 201    spatial index. The sum changes only at index `j`, where `x j` becomes `x j + s`. -/
 202private lemma spatialNormSq_coordRay_spatial_1 (x : Fin 4 → ℝ) (s : ℝ) :
 203    spatialNormSq (coordRay x 1 s) = (x 1 + s) ^ 2 + x 2 ^ 2 + x 3 ^ 2 := by