`differentiableAt_coordRay_partialDeriv_v2_radialInv`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Calculus.Derivatives
domain: Relativity
line: 596 · 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 596.

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

 593    - denominator is nonzero at `s = 0` since `r(x) ≠ 0`.
 594
 595    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
 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
 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)

papers checked against this theorem

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