partialDeriv_v2_spatialRadius_proved

formal source

 126
 127/-- The directional derivative of `spatialRadius` in the spatial directions equals
 128    `x μ / spatialRadius x`. -/
 129theorem partialDeriv_v2_spatialRadius_proved
 130    (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
 131    partialDeriv_v2 spatialRadius μ x =
 132    if μ = 0 then 0 else x μ / spatialRadius x := by
 133  unfold partialDeriv_v2 spatialRadius
 134  by_cases hμ : μ = 0
 135  · -- Temporal direction: spatialNormSq is constant along t ↦ coordRay x 0 t
 136    simp only [hμ, ↓reduceIte]
 137    have h : ∀ t, spatialNormSq (coordRay x 0 t) = spatialNormSq x :=
 138      spatialNormSq_coordRay_temporal x
 139    simp_rw [h]
 140    exact deriv_const 0 _
 141  · -- Spatial direction: apply HasDerivAt.sqrt + chain rule
 142    simp only [hμ, ↓reduceIte]
 143    have h_sn_pos : 0 < spatialNormSq x := by
 144      have := (spatialRadius_ne_zero_iff x).mp hx
 145      exact lt_of_le_of_ne (spatialNormSq_nonneg x) this.symm
 146    -- spatialNormSq along the ray is differentiable with derivative 2 * x μ
 147    have h_sn_da : DifferentiableAt ℝ (fun t => spatialNormSq (coordRay x μ t)) 0 :=
 148      differentiableAt_coordRay_spatialNormSq x μ
 149    have h_sn_deriv : deriv (fun t => spatialNormSq (coordRay x μ t)) 0 = 2 * x μ := by
 150      have := partialDeriv_v2_spatialNormSq μ x
 151      simp only [hμ, ↓reduceIte] at this
 152      exact this
 153    -- HasDerivAt for spatialNormSq ∘ coordRay
 154    have h_sn_hda : HasDerivAt (fun t => spatialNormSq (coordRay x μ t)) (2 * x μ) 0 :=
 155      h_sn_deriv ▸ h_sn_da.hasDerivAt
 156    -- Chain rule for sqrt: HasDerivAt √f
 157    have h_sqrt_hda : HasDerivAt (fun t => Real.sqrt (spatialNormSq (coordRay x μ t)))
 158        ((2 * x μ) / (2 * Real.sqrt (spatialNormSq x))) 0 := by
 159      have h0 : spatialNormSq (coordRay x μ 0) = spatialNormSq x := by