partialDeriv_v2_radialInv

formal source

 506    the derivative `∂_μ r = x_μ / r` (lifted from `partialDeriv_v2_spatialRadius`).
 507
 508    Closes one of the six remaining §XXIII.B′ Mathlib calculus axioms. -/
 509theorem partialDeriv_v2_radialInv (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
 510    partialDeriv_v2 (radialInv n) μ x =
 511    if μ = 0 then 0 else - (n : ℝ) * x μ / (spatialRadius x) ^ (n + 2) := by
 512  unfold partialDeriv_v2 radialInv
 513  by_cases hμ : μ = 0
 514  · simp only [hμ, ↓reduceIte]
 515    have h : ∀ t, spatialRadius (coordRay x 0 t) = spatialRadius x :=
 516      spatialRadius_coordRay_temporal x
 517    have h2 : (fun t => 1 / spatialRadius (coordRay x 0 t) ^ n) =
 518              (fun _ => 1 / spatialRadius x ^ n) := by
 519      funext t; rw [h]
 520    simp_rw [h2]; exact deriv_const 0 _
 521  · simp only [hμ, ↓reduceIte]
 522    cases n with
 523    | zero => simp
 524    | succ k =>
 525      have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
 526      have h_r_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t)) 0 :=
 527        differentiableAt_coordRay_spatialRadius x μ hx
 528      have h_r_pow_da : DifferentiableAt ℝ (fun t => spatialRadius (coordRay x μ t) ^ (k + 1)) 0 :=
 529        h_r_da.pow (k + 1)
 530      have h_r_pow_ne : spatialRadius (coordRay x μ 0) ^ (k + 1) ≠ 0 := by
 531        simp only [coordRay_zero]
 532        exact pow_ne_zero (k + 1) hx
 533      have h_r_deriv : deriv (fun t => spatialRadius (coordRay x μ t)) 0 = x μ / spatialRadius x := by
 534        have := partialDeriv_v2_spatialRadius μ x hx
 535        simp only [partialDeriv_v2, hμ, ↓reduceIte] at this
 536        exact this
 537      have h_r_hda : HasDerivAt (fun t => spatialRadius (coordRay x μ t)) (x μ / spatialRadius x) 0 := by
 538        have : HasDerivAt (fun t => spatialRadius (coordRay x μ t))
 539            (deriv (fun t => spatialRadius (coordRay x μ t)) 0) 0 := h_r_da.hasDerivAt