V-02 complex matrix calculus
DefinitionAtlas_EinsteinMaxwell_NP_CCalceinstein-maxwellexact-spacetime-atlas-vexact-vacuum-atlasgeneral-relativitynewman-penrose
V-02 complex matrix calculus
pdMC (entrywise cpdC of complex matrix fields), SmoothOnC (entrywise C^∞).
中文摘要 V-02 复矩阵演算。
Registry: PHYSICS_BOUNDARY §L (V-02) L9.
Definition code
-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/CCalc.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.SmoothOnC, ExactVacuumAtlas.EinsteinMaxwell.NP.pdMC
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_NP_Basic
import Definitions.Def_Atlas_Transport_MatrixCalc
/-!
# Atlas V-02: calculus of complex-valued fields and complex matrix fields
Complex-valued analogue (real variables, values in `ℂ`, no holomorphy) of `Atlas/Transport/{Calculus,MatrixCalc}`
for the V-01 slice derivative `cpdC` (`Atlas/EinsteinMaxwell/NP/Basic.lean`, unchanged). Every rule is stated for
`C^∞` (order `∞ = ((⊤ : ℕ∞) : WithTop ℕ∞)`, not `ω`) fields on an **open** set, so each `cpdC` is a genuine
derivative (`hasDerivAt_cpdC`):
* `cpdC` rules: constants, locality, sums, products, mixed partials (`cpdC_cpdC_symm`), smoothness of `cpdC`;
* `pdMC i A y` (B3 class B notation): entrywise `cpdC` of a complex matrix field; `SmoothOnC A U`: every entry `C^∞`;
* product rule, sums, scalar multiples, derivative of an inverse, symmetry of mixed partials, and the bridge
`pdMC_map_ofReal`: the derivative of a complexified real matrix field is the complexified `pdM`.
Nothing here mentions a metric, a frame or a connection.
-/
open Filter Topology Complex
open scoped ContDiff Matrix
namespace ExactVacuumAtlas.EinsteinMaxwell.NP
variable {n : ℕ}
/-! ### `cpdC` -/
section rules
variable {U : Set (Pt n)} (hU : IsOpen U) {y : Pt n} (hy : y ∈ U) (i : Fin n)
include hU hy
end rules
/-! ### Complex matrix fields -/
/-- Entrywise complex slice derivative of a complex matrix field (class B notation over `cpdC`). -/
noncomputable def pdMC (i : Fin n) (A : Pt n → Matrix (Fin n) (Fin n) ℂ) (y : Pt n) :
Matrix (Fin n) (Fin n) ℂ :=
Matrix.of fun a b => cpdC i (fun z => A z a b) y
/-- Every entry is `C^∞` on `U`. -/
def SmoothOnC (A : Pt n → Matrix (Fin n) (Fin n) ℂ) (U : Set (Pt n)) : Prop :=
∀ a b, ContDiffOn ℝ ∞ (fun y => A y a b) U
namespace SmoothOnC
variable {U : Set (Pt n)} {A B : Pt n → Matrix (Fin n) (Fin n) ℂ}
end SmoothOnC
section mrules
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 mrules
end ExactVacuumAtlas.EinsteinMaxwell.NP
Source
He Wang, Exact Spacetime Atlas V: From Linearized Einstein–Maxwell Equations to Kerr–Newman Radiation Systems. Local source, no public repository; commit b8cd107a558e153ed41fb4972ac5315499d14778; Atlas/EinsteinMaxwell/NP/CCalc.lean; SHA-256 6a1dbda6630d0b67e95115c8579f4f49424d8f95815411a6dc9614b2ab747a93. Registered definitions: mission/PHYSICS_BOUNDARY.md (§K–§M); literature: P. Hintz, arXiv:2609.33661 (v1); Mark–Yang–Zimmerman–Chen, arXiv:1409.5800 (v1).
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.