differentiableAt_coordRay_radialInv

formal source

 425  apply DifferentiableAt.sqrt (differentiableAt_coordRay_spatialNormSq x μ) h_sn_ne_zero
 426
 427/-- Differentiability of radialInv along a coordinate ray. -/
 428theorem differentiableAt_coordRay_radialInv (n : ℕ) (x : Fin 4 → ℝ) (μ : Fin 4) (hx : spatialRadius x ≠ 0) :
 429    DifferentiableAt ℝ (fun t => radialInv n (coordRay x μ t)) 0 := by
 430  unfold radialInv
 431  apply DifferentiableAt.div (differentiableAt_const (1 : ℝ))
 432  · apply DifferentiableAt.pow (differentiableAt_coordRay_spatialRadius x μ hx)
 433  · have h_pos : 0 < spatialRadius x := by
 434      unfold spatialRadius
 435      apply Real.sqrt_pos.mpr
 436      have h_nonneg := spatialNormSq_nonneg x
 437      have h_ne_zero := (spatialRadius_ne_zero_iff x).mp hx
 438      exact lt_of_le_of_ne h_nonneg h_ne_zero.symm
 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. -/