lemma
proved
term proof
spatialNormSq_coordRay_spatial_3
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/