spatialRadius_coordRay_ne_zero_eventually

formal source

 439    simp only [coordRay_zero]
 440    exact (pow_pos h_pos n).ne'
 441
 442theorem spatialRadius_coordRay_ne_zero_eventually {x : Fin 4 → ℝ} (hx : spatialRadius x ≠ 0) (μ : Fin 4) :
 443    ∀ᶠ t in 𝓝 0, spatialRadius (coordRay x μ t) ≠ 0 := by
 444  have h_cont : Continuous (fun t => spatialRadius (coordRay x μ t)) := by
 445    unfold spatialRadius spatialNormSq coordRay basisVec
 446    fun_prop
 447  apply h_cont.continuousAt.eventually_ne
 448  simp [coordRay_zero, hx]
 449
 450/-- Directional derivative of `spatialRadius` in coordinates.
 451
 452    For temporal direction (μ = 0), the spatial radius is invariant along the
 453    coordinate ray, so the derivative is 0. For a spatial direction (μ ≠ 0),
 454    we compose the chain rule for `Real.sqrt` (Mathlib `HasDerivAt.sqrt`)
 455    with the derivative `∂_μ ‖x‖² = 2 x_μ` (lifted from
 456    `partialDeriv_v2_spatialNormSq`), giving `(2 x_μ) / (2 √‖x‖²) = x_μ / r`.
 457
 458    Closes one of the seven §XXIII.B′ Mathlib calculus axioms. -/
 459theorem partialDeriv_v2_spatialRadius (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
 460    partialDeriv_v2 spatialRadius μ x =
 461    if μ = 0 then 0 else x μ / spatialRadius x := by
 462  by_cases hμ : μ = 0
 463  · -- Temporal direction: `spatialRadius` is invariant along `coordRay x 0 _`.
 464    simp only [hμ, ↓reduceIte]
 465    unfold partialDeriv_v2
 466    have h : ∀ t, spatialRadius (coordRay x 0 t) = spatialRadius x :=
 467      spatialRadius_coordRay_temporal x
 468    simp_rw [h]
 469    exact deriv_const 0 _
 470  · -- Spatial direction: chain rule for `Real.sqrt`.
 471    simp only [hμ, ↓reduceIte]
 472    unfold partialDeriv_v2 spatialRadius