Prove2Me

Radial derivative of 1/Σ1/\Sigma for Kerr

Proved
ExactVacuumAtlas.Kerr.In.hasDerivAt_Ui_r

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

coordinate-geometryderivativeexact-vacuum-atlasgeneral-relativitykerr-metricreal-analysis

Let a,θ,ra,\theta,r be real numbers with r2+a2cos⁡2θ≠0r^2+a^2\cos^2\theta\neq0 and write U(r,θ)=(r2+a2cos⁡2θ)−1=1/ΣU(r,\theta)=\big(r^2+a^2\cos^2\theta\big)^{-1}=1/\Sigma (the atom Ui of bundle Atlas_Kerr_InAtoms). Then u↦U(u,θ)u\mapsto U(u,\theta) has at u=ru=r the derivative

∂r(1Σ)=−2rΣ2=−2r U(r,θ)2.\partial_r\Big(\frac1\Sigma\Big)=-\frac{2r}{\Sigma^2}=-2r\,U(r,\theta)^2.

One of the two key derivative rules for the atom 1/Σ1/\Sigma used by the ingoing-Kerr tables, whose entries are polynomials in r,sin⁡θ,cos⁡θ,1/Σ,1/sin⁡θr,\sin\theta,\cos\theta,1/\Sigma,1/\sin\theta. Differentiating the tables also uses the usual product and chain rules, trigonometric derivatives, the derivative of 1/sin⁡θ1/\sin\theta, and locality arguments.

Formalization Note Ui a r θ is Mathlib's inverse of a real number; the hypothesis Σ≠0\Sigma\neq0 excludes the junk value of 0−1=00^{-1}=0.

Preamble
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_Core_Lift
import Definitions.Def_Atlas_Kerr_InAtoms
import Definitions.Def_Atlas_Kerr_InDefs
open Real
Formal statement
theorem ExactVacuumAtlas.Kerr.In.hasDerivAt_Ui_r (a θ r : ℝ) (h : r ^ 2 + a ^ 2 * cos θ ^ 2 ≠ 0) :
    HasDerivAt (fun u => Ui a u θ) (-2 * r * Ui a 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/Kerr/InAtoms.lean#L28-L35 (module Atlas.Kerr.InAtoms, file sha256 30e14f9094cc6659a7670a18a03040eb71977f1710ab1a059d8f086edad7527a; uploaded stub = platform_mirror/Theorems/Thm_ExactVacuumAtlas_Kerr_In_hasDerivAt_Ui_r.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