Derivative of 1 + K cos²t sin²t
ProvedExactVacuumAtlas.Deriv.one_add_mul_cos_sq_sin_sqexact-vacuum-atlasgeneral-relativitylean4mathlib
For all real K and θ: the function t ↦ 1 + K cos²t sin²t has derivative K (2 cos³θ sin θ − 2 cos θ sin³θ) at θ (HasDerivAt).
Preamble
import Mathlib open Real
Formal statement
theorem ExactVacuumAtlas.Deriv.one_add_mul_cos_sq_sin_sq (K θ : ℝ) :
HasDerivAt (fun t => 1 + K * (cos t ^ 2 * sin t ^ 2))
(K * (2 * cos θ ^ 3 * sin θ - 2 * cos θ * sin θ ^ 3)) θ := by sorrySource
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Controls/ShearDeriv.lean#L13-L19; SHA-256 289482b30b70007ed251428d9febcddfa951f51d54e87520950d81e2b8842664. Mathematical background: See mission/PHYSICS_BOUNDARY.md §A-F for registered definitions and literature references (Wald, Müller-Grave arXiv:0904.4184, Visser arXiv:0706.0622, Martel-Poisson gr-qc/0001069).
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.