Derivative of $K/u^2+L/u^3$ at a nonzero point

Proved

ExactVacuumAtlas.Deriv.div_sq_add_div_cube

by He Wang · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

coordinate-geometryderivativeexact-vacuum-atlasgeneral-relativityreal-analysis

Let $K,L,r$ be real numbers with $r\neq0$ . The function $u\mapsto K/u^2+L/u^3$ has, at $u=r$ , the derivative

\frac{d}{du}\Big(\frac{K}{u^2}+\frac{L}{u^3}\Big)\Big|_{u=r}=-\frac{2K}{r^3}-\frac{3L}{r^4}.

Elementary derivative rule shared by the Schwarzschild and Eddington–Finkelstein tables, where the coefficients of the Christoffel symbols are rational functions of $r$ .

Formalization Note Stated with Mathlib's HasDerivAt (an actual derivative, not a default value); division by $u$ is Mathlib's total real division, harmless because $r\neq0$ .

Preamble

import Mathlib
open Real

Formal statement

theorem ExactVacuumAtlas.Deriv.div_sq_add_div_cube (K L r : ℝ) (hr : r ≠ 0) :
    HasDerivAt (fun u => K / u ^ 2 + L / u ^ 3) (-2 * K / r ^ 3 - 3 * L / r ^ 4) r := by sorry

Source

elementary one-variable calculus (standard); Lean source: repository ExactVacuumAtlas (private repository, not publicly accessible; GitHub remote pending (no GitHub identity on the build server)), commit 35f26e6a22f5d72380094fa94edc72dea667df53, Atlas/Core/Deriv.lean#L41-L49 (module Atlas.Core.Deriv, file sha256 dc49ec3a0b39ea3e075312c79b8b14e378ffdc0688d2931d08c6421ec4264e95; uploaded stub = platform_mirror/Theorems/Thm_ExactVacuumAtlas_Deriv_div_sq_add_div_cube.lean)

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by He Wang · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Derivative of K/u2+L/u3K/u^2+L/u^3K/u2+L/u3 at a nonzero point

Derivative of $K/u^2+L/u^3$ at a nonzero point