MixedPartialsSymmetric
plain-language theorem explainer
Mixed partial symmetry states that second derivatives of a scalar function on four-dimensional space commute in their indices. General relativists cite it when assuming coordinate smoothness for curvature computations in the Riemann tensor. The declaration is a direct definition that equates the two orders of the secondDeriv operator without additional steps.
Claim. For a scalar function $f: (Fin 4 → ℝ) → ℝ$ and point $x ∈ Fin 4 → ℝ$, the second partial derivatives satisfy $∂_μ ∂_ν f(x) = ∂_ν ∂_μ f(x)$ for all indices $μ, ν$.
background
The RiemannSymmetries module derives algebraic identities for the Riemann curvature tensor from Christoffel symbols of a metric tensor. The secondDeriv operator, imported from the Derivatives module, computes iterated directional derivatives $∂_μ ∂_ν f$ by differentiating along coordinate rays. This definition encodes the classical commutativity of mixed partials (Schwarz theorem) specialized to four dimensions and the functions appearing in metric components.
proof idea
The declaration is a definition that directly equates secondDeriv f μ ν x with secondDeriv f ν μ x for all μ ν. It functions as a one-line wrapper that applies the secondDeriv operator in both orders and asserts their equality.
why it matters
This definition is required by the downstream MetricSmooth property, which ensures the metric tensor components admit symmetric mixed partials before the Riemann tensor symmetries (antisymmetry in first pair, first Bianchi identity, pair exchange) are derived. It supplies the smoothness hypothesis referenced in the module strategy that leads to R_ρσμν = R_μνρσ. In the broader framework it anchors the geometric layer used to reach D = 3 from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.