Chain rule for the slice derivative
ProvedExactVacuumAtlas.pd_compexact-vacuum-atlasgeneral-relativitylean4mathlib
Let V be open, f C^∞ on V, Φ a map with Φ y ∈ V whose slices have genuine derivatives J y k i at y. Then for every i: pd i (z ↦ f (Φ z)) y = Σ_e pd e f (Φ y) · J y e i.
Preamble
import Mathlib
import Definitions.Def_Atlas_Core_Basic
open Filter Topology
open scoped ContDiff
open ExactVacuumAtlas
variable {n : ℕ}
Formal statement
theorem ExactVacuumAtlas.pd_comp {V : Set (Pt n)} (hV : IsOpen V) {f : Pt n → ℝ} (hf : ContDiffOn ℝ ∞ f V)
{Φ : Pt n → Pt n} {J : Pt n → Matrix (Fin n) (Fin n) ℝ} {y : Pt n} (hy : Φ y ∈ V)
(hJ : ∀ k i : Fin n, HasDerivAt (fun u : ℝ => Φ (Function.update y i u) k) (J y k i) (y i))
(i : Fin n) : pd i (fun z => f (Φ z)) y = ∑ e, pd e f (Φ y) * J y e i := by sorrySource
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Transport/Calculus.lean#L69-L87; SHA-256 0f59ac6cfdfd6b539a70914c2743635b3775f0848016a2490e7a5b20efd22759. 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.