Derivative of −(1 − K/u + L/u²)
ProvedExactVacuumAtlas.RNDeriv.neg_one_sub_div_add_div_sqeinstein-maxwellexact-spacetime-atlas-ivexact-vacuum-atlasgeneral-relativity
Derivative of −(1 − K/u + L/u²)
HasDerivAt (u ↦ −(1 − K/u + L/u²)) (−K/r² + 2L/r³) at r ≠ 0 (the RN g_vv profile).
Scope. Exactly the hypotheses printed in the formal statement.
中文摘要 RN g_vv 剖面的导数。
Preamble
import Mathlib open Real
Formal statement
theorem ExactVacuumAtlas.RNDeriv.neg_one_sub_div_add_div_sq (K L r : ℝ) (hr : r ≠ 0) :
HasDerivAt (fun u => -(1 - K / u + L / u ^ 2)) (-K / r ^ 2 + 2 * L / r ^ 3) r := by sorrySource
He Wang, Exact Spacetime Atlas IV: Certified Einstein–Maxwell Backgrounds and First Variations. Local source, no public repository; commit 543904bfcfa3bb169f43fc4d9dbd569999b71886; Atlas/EinsteinMaxwell/RN/Deriv.lean#L13-L21; SHA-256 be20df290bc44eba3b516e6dedbe84a8c4ef45320f639ac84cfcf286cdcdfb5b. Registered definitions and literature: mission/PHYSICS_BOUNDARY.md (§H–§J); Müller–Grave arXiv:0904.4184; Newman et al., J. Math. Phys. 6 (1965) 918.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.