theorem
proved
tactic proof
differentiableAt_coordRay_partialDeriv_v2_radialInv
show as:
view Lean formalization →
formal statement (Lean)
596theorem differentiableAt_coordRay_partialDeriv_v2_radialInv
597 (n : ℕ) (x : Fin 4 → ℝ) (μ ν : Fin 4) (hx : spatialRadius x ≠ 0) :
598 DifferentiableAt ℝ (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) 0 := by
proof body
Tactic-mode proof.
599 by_cases hμ : μ = 0
600 · -- Temporal: `partialDeriv_v2 (radialInv n) 0 y = 0` for `r y ≠ 0`,
601 -- so the function is eventually 0 near `s = 0`.
602 apply (differentiableAt_const (0 : ℝ)).congr_of_eventuallyEq
603 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
604 intro s hs
605 show partialDeriv_v2 (radialInv n) μ (coordRay x ν s) = 0
606 rw [partialDeriv_v2_radialInv n μ (coordRay x ν s) hs]
607 simp [hμ]
608 · -- Spatial: smooth quotient formula `-n · x_μ / r^(n+2)` is differentiable,
609 -- and `partialDeriv_v2` agrees with it where `r ≠ 0`.
610 have h_num_diff : DifferentiableAt ℝ
611 (fun s : ℝ => -(n : ℝ) * (coordRay x ν s) μ) 0 :=
612 (differentiableAt_coordRay_i x ν μ).const_mul (-(n : ℝ))
613 have h_denom_diff : DifferentiableAt ℝ
614 (fun s : ℝ => spatialRadius (coordRay x ν s) ^ (n + 2)) 0 :=
615 (differentiableAt_coordRay_spatialRadius x ν hx).pow _
616 have h_denom_ne : spatialRadius (coordRay x ν 0) ^ (n + 2) ≠ 0 := by
617 simp only [coordRay_zero]; exact pow_ne_zero (n + 2) hx
618 have h_smooth_diff : DifferentiableAt ℝ
619 (fun s : ℝ => -(n : ℝ) * (coordRay x ν s) μ /
620 (spatialRadius (coordRay x ν s)) ^ (n + 2)) 0 :=
621 h_num_diff.div h_denom_diff h_denom_ne
622 apply h_smooth_diff.congr_of_eventuallyEq
623 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
624 intro s hs
625 show partialDeriv_v2 (radialInv n) μ (coordRay x ν s) =
626 -(n : ℝ) * (coordRay x ν s) μ / (spatialRadius (coordRay x ν s)) ^ (n + 2)
627 rw [partialDeriv_v2_radialInv n μ (coordRay x ν s) hs]
628 simp [hμ]
629
630/-- Second directional derivative of `radialInv n`:
631 `∂_ν ∂_μ (1/r^n) = n · ((n+2) x_μ x_ν / r^{n+4} - δ_{μν} / r^{n+2})` for `μ, ν ∈ {1,2,3}`,
632 and `0` whenever either index is `0` (temporal).
633
634 Proof structure:
635 - `μ = 0`: `partialDeriv_v2 (radialInv n) 0 = 0` (already proved), so the outer derivative
636 is `deriv 0 = 0`.
637 - `μ ≠ 0, ν = 0`: spatial partial derivative is invariant along the temporal ray
638 (since both `x_μ` and `r` are unchanged), so the outer derivative is `deriv const = 0`.
639 - `μ, ν ≠ 0`: apply the quotient rule `HasDerivAt.div` to the smooth formula
640 `-n · x_μ / r^{n+2}`, then simplify the resulting algebraic expression
641 `(f' g - f g') / g²` to match the target. The simplification uses
642 `r^{n+2-1} = r^{n+1}` (natural-number subtraction), `(r^{n+2})² = r^{2(n+2)} = r^{n+4} · r^n`,
643 and `field_simp` plus `ring` to clear denominators.
644
645 Closes one of the §XXIII.B′ Mathlib calculus axioms. -/