partialDeriv_v2_spatialRadius

formal source

 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
 473    -- `spatialNormSq x ≠ 0` since `spatialRadius x ≠ 0`.
 474    have h_sn_ne : spatialNormSq x ≠ 0 := (spatialRadius_ne_zero_iff x).mp hx
 475    -- Differentiability of `t ↦ ‖coordRay x μ t‖²` at 0.
 476    have h_sn_da : DifferentiableAt ℝ (fun t => spatialNormSq (coordRay x μ t)) 0 :=
 477      differentiableAt_coordRay_spatialNormSq x μ
 478    -- Its derivative at 0 is `2 x_μ` (from `partialDeriv_v2_spatialNormSq`).
 479    have h_sn_deriv : deriv (fun t => spatialNormSq (coordRay x μ t)) 0 = 2 * x μ := by
 480      have := partialDeriv_v2_spatialNormSq μ x
 481      simp only [partialDeriv_v2, hμ, ↓reduceIte] at this
 482      exact this
 483    -- Lift to `HasDerivAt`.
 484    have h_sn_hda : HasDerivAt (fun t => spatialNormSq (coordRay x μ t)) (2 * x μ) 0 := by
 485      have : HasDerivAt (fun t => spatialNormSq (coordRay x μ t))
 486          (deriv (fun t => spatialNormSq (coordRay x μ t)) 0) 0 := h_sn_da.hasDerivAt
 487      simpa [h_sn_deriv] using this
 488    -- Value at 0 needed for `HasDerivAt.sqrt`.
 489    have h_sn_eq_at_0 : spatialNormSq (coordRay x μ 0) = spatialNormSq x := by