spatialNormSq_coordRay_spatial_3

formal source

 215      if_neg (by decide : (3 : Fin 4) ≠ 2)]
 216  ring
 217
 218private lemma spatialNormSq_coordRay_spatial_3 (x : Fin 4 → ℝ) (s : ℝ) :
 219    spatialNormSq (coordRay x 3 s) = x 1 ^ 2 + x 2 ^ 2 + (x 3 + s) ^ 2 := by
 220  unfold spatialNormSq coordRay basisVec
 221  rw [if_neg (by decide : (1 : Fin 4) ≠ 3),
 222      if_neg (by decide : (2 : Fin 4) ≠ 3),
 223      if_pos (rfl : (3 : Fin 4) = 3)]
 224  ring
 225
 226/-- `spatialRadius` stays nonzero under sufficiently small coordinate perturbations.
 227
 228    Quantitative version: if `r = spatialRadius x ≠ 0` and `|s| < r/2`, then the
 229    perturbed point `coordRay x ν s = x + s · e_ν` still has nonzero spatial radius.
 230
 231    Proof: case-split on `ν ∈ {0,1,2,3}`.
 232    - `ν = 0`: temporal direction, `spatialRadius (coordRay x 0 s) = spatialRadius x` (proved).
 233    - `ν ∈ {1,2,3}`: only the `ν`-th spatial component changes by `s`, so
 234      `spatialNormSq (coordRay x ν s) = ‖x‖² + 2 s · x_ν + s²`. Using `|x_ν| ≤ r`
 235      and `|s| < r/2`, the polynomial lower bound `(r - |s|)² ≤ ‖x‖² + 2 s x_ν + s²`
 236      gives `spatialNormSq > 0` and hence `spatialRadius ≠ 0`.
 237
 238    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
 239theorem spatialRadius_coordRay_ne_zero (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
 240    (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2) :
 241    spatialRadius (coordRay x ν s) ≠ 0 := by
 242  rw [spatialRadius_ne_zero_iff]
 243  have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
 244  have hr_sq : spatialRadius x ^ 2 = spatialNormSq x := by
 245    unfold spatialRadius; rw [Real.sq_sqrt (spatialNormSq_nonneg x)]
 246  have h_s_lo : -(spatialRadius x / 2) < s := (abs_lt.mp hs).1
 247  have h_s_hi : s < spatialRadius x / 2 := (abs_lt.mp hs).2
 248  have h_x1_le : x 1 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_1 x