Atlas_Transport_MatrixCalc
Definitionexact-vacuum-atlasgeneral-relativitylean4mathlib
pdM i A y = Matrix.of (a, b ↦ pd i (z ↦ A z a b) y): the entrywise slice derivative of a matrix-valued field A : ℝⁿ → Matrix (Fin n) (Fin n) ℝ (a notation wrapper over the registered pd; pdM_apply is rfl). SmoothOn A U := ∀ a b, ContDiffOn ℝ ∞ (y ↦ A y a b) U: every entry is C^∞ on U. The rules (product, linearity, inverse ∂K = −K ∂J K, chain rule, symmetry of mixed derivatives, smoothness of a right inverse by Cramer) are theorems of the source module, not part of the bundle.
中文导读。 矩阵场的逐项切片导数 pdM（对登记 pd 的记号包装）与逐项 C^∞ 的 SmoothOn；微积分规则是模块定理，不在包内。
Definition code
-- Generated by scripts/release01/gen_platform_tree.py (ATLAS-RELEASE-01) by skeleton subtraction from Atlas/Transport/MatrixCalc.lean
-- definition bundle: kept ExactVacuumAtlas.SmoothOn, ExactVacuumAtlas.pdM
import Mathlib
import Definitions.Def_Atlas_Core_Basic
/-!
# Transport layer II.b: entrywise calculus of matrix-valued fields (ATLAS-II)
`pdM i A y` is the matrix of slice derivatives `pd i (A · a b) y` of a matrix field `A : Pt n → Matrix`
(B3 class B: a notation wrapper over `pd`, bridge `pdM_apply` is `rfl`). `SmoothOn A U` says every entry
is `C^∞` on `U`. On an open set all the usual rules hold with genuine derivatives:
* product rule `pdM i (A·B) = (pdM i A)·B + A·(pdM i B)`, linearity, finite sums, scalar multiples;
* derivative of an inverse: `K·J = 1` on `U` ⇒ `pdM i K = −K·(pdM i J)·K`;
* chain rule `pdM i (B ∘ Φ) y = Σ_e J y e i • pdM e B (Φ y)`;
* symmetry `pdM c (pdM d A) = pdM d (pdM c A)`;
* smoothness of a right inverse `K` of a smooth `J` (`K = det(J)⁻¹ • adjugate J`), and of the genuine
Jacobian of a `C^∞` map (`smoothOn_jacobian`).
Nothing here mentions a metric or a connection.
-/
open scoped ContDiff
namespace ExactVacuumAtlas
variable {n : ℕ}
/-- Entrywise slice derivative of a matrix-valued field. -/
noncomputable def pdM (i : Fin n) (A : Pt n → Matrix (Fin n) (Fin n) ℝ) (y : Pt n) :
Matrix (Fin n) (Fin n) ℝ :=
Matrix.of fun a b => pd i (fun z => A z a b) y
/-- Every entry is `C^∞` on `U`. -/
def SmoothOn (A : Pt n → Matrix (Fin n) (Fin n) ℝ) (U : Set (Pt n)) : Prop :=
∀ a b, ContDiffOn ℝ ∞ (fun y => A y a b) U
namespace SmoothOn
variable {U V : Set (Pt n)} {A B : Pt n → Matrix (Fin n) (Fin n) ℝ}
end SmoothOn
/-! ### Rules for `pdM` on an open set -/
section rules
variable {U : Set (Pt n)} (hU : IsOpen U) {y : Pt n} (hy : y ∈ U) (i : Fin n)
{A B : Pt n → Matrix (Fin n) (Fin n) ℝ}
include hU hy
end rules
/-! ### Smoothness of Jacobians and of their inverses -/
end ExactVacuumAtlas
Source
He Wang, Exact Vacuum Atlas II, local source snapshot (public Git repository not yet available), commit 11fb317259353b71a41d6daed466c495cffd7db4; Atlas/Transport/MatrixCalc.lean; SHA-256 994bf6c8664b9c7b2def61b44cb0205ed97883699045a73e41d873029c259310. 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.