theorem
proved
tactic proof
secondDeriv_radialInv
show as:
view Lean formalization →
formal statement (Lean)
646theorem secondDeriv_radialInv (n : ℕ) (μ ν : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0) :
647 secondDeriv (radialInv n) μ ν x =
648 if μ = 0 ∨ ν = 0 then 0 else
649 (n : ℝ) *
650 ((n + 2 : ℝ) * x μ * x ν / (spatialRadius x) ^ (n + 4) -
651 (if μ = ν then 1 else 0) / (spatialRadius x) ^ (n + 2)) := by
proof body
Tactic-mode proof.
652 unfold secondDeriv
653 by_cases hμ : μ = 0
654 · -- μ = 0: outer function is eventually 0.
655 simp only [hμ, true_or, ↓reduceIte]
656 have h_ev : (fun s => partialDeriv_v2 (radialInv n) 0 (coordRay x ν s)) =ᶠ[𝓝 0]
657 (fun _ => (0 : ℝ)) := by
658 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
659 intro s hs
660 show partialDeriv_v2 (radialInv n) 0 (coordRay x ν s) = 0
661 rw [partialDeriv_v2_radialInv n 0 (coordRay x ν s) hs]
662 simp
663 rw [h_ev.deriv_eq]; exact deriv_const 0 _
664 · by_cases hν : ν = 0
665 · -- μ ≠ 0, ν = 0: outer function is constant in s.
666 simp only [hν, hμ, false_or, ↓reduceIte, or_true]
667 have h_const : ∀ s, partialDeriv_v2 (radialInv n) μ (coordRay x 0 s) =
668 partialDeriv_v2 (radialInv n) μ x := by
669 intro s
670 have hr_s : spatialRadius (coordRay x 0 s) = spatialRadius x :=
671 spatialRadius_coordRay_temporal x s
672 have h_coord : (coordRay x 0 s) μ = x μ := coordRay_temporal_spatial x s μ hμ
673 have hr_ne_s : spatialRadius (coordRay x 0 s) ≠ 0 := by rw [hr_s]; exact hx
674 rw [partialDeriv_v2_radialInv n μ (coordRay x 0 s) hr_ne_s,
675 partialDeriv_v2_radialInv n μ x hx]
676 simp only [hμ, ↓reduceIte]
677 rw [hr_s, h_coord]
678 simp_rw [h_const]
679 exact deriv_const 0 _
680 · -- Main case: μ ≠ 0 and ν ≠ 0.
681 simp only [hμ, hν, false_or, ↓reduceIte]
682 have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
683 have hr_ne : spatialRadius x ≠ 0 := hx
684 -- Near 0, the outer function equals the smooth formula `-n · y_μ / r(y)^(n+2)`.
685 have h_ev : (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) =ᶠ[𝓝 0]
686 (fun s => -(n : ℝ) * (coordRay x ν s) μ /
687 (spatialRadius (coordRay x ν s)) ^ (n + 2)) := by
688 apply (spatialRadius_coordRay_ne_zero_eventually hx ν).mono
689 intro s hs
690 show partialDeriv_v2 (radialInv n) μ (coordRay x ν s) =
691 -(n : ℝ) * (coordRay x ν s) μ /
692 (spatialRadius (coordRay x ν s)) ^ (n + 2)
693 rw [partialDeriv_v2_radialInv n μ (coordRay x ν s) hs]
694 simp [hμ]
695 rw [h_ev.deriv_eq]
696 -- Compute deriv via HasDerivAt.div on the smooth formula.
697 -- Numerator: c(s) = -n · (x_μ + s · δ_{μ,ν}); c(0) = -n · x_μ; c'(0) = -n · δ_{μ,ν}.
698 have h_num_hda : HasDerivAt (fun s => -(n : ℝ) * (coordRay x ν s) μ)
699 (-(n : ℝ) * basisVec ν μ) 0 := by
700 simp only [coordRay_apply]
701 have h_inner : HasDerivAt (fun s => x μ + s * basisVec ν μ) (basisVec ν μ) 0 := by
702 have := ((hasDerivAt_id (0 : ℝ)).mul_const (basisVec ν μ)).const_add (x μ)
703 simpa using this
704 exact h_inner.const_mul (-(n : ℝ))
705 -- Denominator inner: r(coordRay x ν s); deriv at 0 is `x_ν / r`.
706 have h_r_da : DifferentiableAt ℝ (fun s => spatialRadius (coordRay x ν s)) 0 :=
707 differentiableAt_coordRay_spatialRadius x ν hx
708 have h_r_deriv : deriv (fun s => spatialRadius (coordRay x ν s)) 0 =
709 x ν / spatialRadius x := by
710 have := partialDeriv_v2_spatialRadius ν x hx
711 simp only [partialDeriv_v2, hν, ↓reduceIte] at this
712 exact this
713 have h_r_hda : HasDerivAt (fun s => spatialRadius (coordRay x ν s))
714 (x ν / spatialRadius x) 0 := by
715 have := h_r_da.hasDerivAt
716 simpa [h_r_deriv] using this
717 -- Denominator: g(s) = r(coordRay x ν s)^(n+2); g(0) = r^(n+2);
718 -- g'(0) = (n+2) · r^(n+1) · (x_ν / r) (note `n + 2 - 1 = n + 1` via Nat subtraction).
719 have h_den_hda : HasDerivAt (fun s => (spatialRadius (coordRay x ν s)) ^ (n + 2))
720 ((n + 2 : ℕ) * spatialRadius x ^ (n + 2 - 1) * (x ν / spatialRadius x)) 0 := by
721 have h := h_r_hda.pow (n + 2)
722 simp only [coordRay_zero] at h
723 exact h
724 have h_den_ne : (spatialRadius (coordRay x ν 0)) ^ (n + 2) ≠ 0 := by
725 simp only [coordRay_zero]; exact pow_ne_zero (n + 2) hr_ne
726 -- Apply the quotient rule.
727 have h_quot : HasDerivAt
728 (fun s => -(n : ℝ) * (coordRay x ν s) μ /
729 (spatialRadius (coordRay x ν s)) ^ (n + 2))
730 ((-(n : ℝ) * basisVec ν μ * spatialRadius x ^ (n + 2) -
731 -(n : ℝ) * x μ *
732-- ... 38 more lines elided ...