pith. machine review for the scientific record. sign in
theorem proved tactic proof

partialDeriv_v2_spatialRadius

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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
 490      simp [coordRay_zero]
 491    -- Apply Mathlib's chain rule for sqrt.
 492    have h_sqrt_hda : HasDerivAt (fun t => Real.sqrt (spatialNormSq (coordRay x μ t)))
 493        (2 * x μ / (2 * Real.sqrt (spatialNormSq (coordRay x μ 0)))) 0 :=
 494      h_sn_hda.sqrt (by rw [h_sn_eq_at_0]; exact h_sn_ne)
 495    rw [h_sqrt_hda.deriv, h_sn_eq_at_0]
 496    -- Goal: `2 x_μ / (2 √‖x‖²) = x_μ / √‖x‖²`.
 497    have hr_ne : Real.sqrt (spatialNormSq x) ≠ 0 :=
 498      fun h => h_sn_ne (Real.sqrt_eq_zero (spatialNormSq_nonneg x) |>.mp h)
 499    field_simp
 500
 501/-- Directional derivative of `radialInv` in coordinates.
 502
 503    For temporal direction (μ = 0), `radialInv` is invariant along the ray,
 504    so the derivative is 0. For a spatial direction (μ ≠ 0), we use the quotient
 505    rule `HasDerivAt.div` on `1 / r^n`, composing with `HasDerivAt.pow` and
 506    the derivative `∂_μ r = x_μ / r` (lifted from `partialDeriv_v2_spatialRadius`).
 507
 508    Closes one of the six remaining §XXIII.B′ Mathlib calculus axioms. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (30)

Lean names referenced from this declaration's body.