Derivative of $-(1-K/u)$ at a nonzero point

Proved

ExactVacuumAtlas.Deriv.neg_one_sub_div

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

coordinate-geometryderivativeexact-vacuum-atlasgeneral-relativityreal-analysis

Let $K,r$ be real numbers with $r\neq0$ . The function $u\mapsto-(1-K/u)$ has, at $u=r$ , the derivative

\frac{d}{du}\Big(-\big(1-\tfrac{K}{u}\big)\Big)\Big|_{u=r}=-\frac{K}{r^2}.

The radial derivative of the coefficient $g_{tt}=-(1-2M/r)$ shared by the standard Schwarzschild and Eddington–Finkelstein metrics ( $K=2M$ ).

Formalization Note Stated with Mathlib's HasDerivAt.

Preamble

import Mathlib
open Real

Formal statement

theorem ExactVacuumAtlas.Deriv.neg_one_sub_div (K r : ℝ) (hr : r ≠ 0) :
    HasDerivAt (fun u => -(1 - K / u)) (-K / r ^ 2) 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#L21-L27 (module Atlas.Core.Deriv, file sha256 dc49ec3a0b39ea3e075312c79b8b14e378ffdc0688d2931d08c6421ec4264e95; uploaded stub = platform_mirror/Theorems/Thm_ExactVacuumAtlas_Deriv_neg_one_sub_div.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 −(1−K/u)-(1-K/u)−(1−K/u) at a nonzero point

Derivative of $-(1-K/u)$ at a nonzero point