spatialRadius_coordRay_temporal

formal source

 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
 204  unfold spatialNormSq coordRay basisVec
 205  rw [if_pos (rfl : (1 : Fin 4) = 1),
 206      if_neg (by decide : (2 : Fin 4) ≠ 1),
 207      if_neg (by decide : (3 : Fin 4) ≠ 1)]
 208  ring
 209
 210private lemma spatialNormSq_coordRay_spatial_2 (x : Fin 4 → ℝ) (s : ℝ) :
 211    spatialNormSq (coordRay x 2 s) = x 1 ^ 2 + (x 2 + s) ^ 2 + x 3 ^ 2 := by
 212  unfold spatialNormSq coordRay basisVec