`secondDeriv_radialInv`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Calculus.Derivatives
domain: Relativity
line: 646 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Calculus.Derivatives on GitHub at line 646.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 643      and `field_simp` plus `ring` to clear denominators.
 644
 645    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
 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
 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]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.