@[reducible, inline]

abbrev CM18.Metric (n : ℕ) : Type

A metric on $(1+n)$-dimensional spacetime: a function assigning to each spacetime point $x$ a matrix of components $m_{\mu\nu}(x)$ for $\mu,\nu \in \{0,1,\dots,n\}$.

@[reducible, inline]

abbrev CM18.InverseMetric (n : ℕ) : Type

An inverse metric on $(1+n)$-dimensional spacetime: a function assigning to each spacetime point $x$ a matrix of components $(m^{-1})^{\mu\nu}(x)$ for $\mu,\nu \in \{0,1,\dots,n\}$.

def CM18.MetricLagrangian (n : ℕ) : Type

A metric Lagrangian $\mathcal{L}(\phi, \nabla\phi, m)$: a function of a scalar value, a gradient covector, and a metric matrix, returning a real number. This is the type of Lagrangian considered in CM18 Section 2 (coordinate-invariant Lagrangians).

noncomputable def CM18.MetricLagrangian.eval {n : ℕ} (L : MetricLagrangian n) (φ : ScalarField n) (m : Metric n) (x : Spacetime n) : ℝ

Evaluate a metric Lagrangian on a scalar field $\phi$ and metric $m$ at a spacetime point $x$, producing $\mathcal{L}(\phi(x), \nabla\phi(x), m(x))$.

structure CM18.FlowMap (n : ℕ) : Type

A one-parameter flow on spacetime generated by a smooth vector field $Y$. The map $F_\epsilon : \text{Spacetime} \to \text{Spacetime}$ satisfies $F_0 = \mathrm{id}$, $F_{-\epsilon} \circ F_\epsilon = \mathrm{id}$, and $\frac{d}{ds}F_s(x) = Y(F_s(x))$. This corresponds to the diffeomorphism family of CM18 Proposition 2.0.1.

• F : ℝ → Spacetime n → Spacetime n
• Y : Spacetime n → Spacetime n
• F_zero (x : Spacetime n) : self.F 0 x = x
• F_smooth_eps (x : Spacetime n) : ContDiff ℝ ⊤ fun (ε : ℝ) => self.F ε x
• F_inv (ε : ℝ) (x : Spacetime n) : self.F (-ε) (self.F ε x) = x
• F_flow (ε : ℝ) (x : Spacetime n) : deriv (fun (s : ℝ) => self.F s x) ε = self.Y (self.F ε x)
• F_smooth_joint : ContDiff ℝ ⊤ fun (p : ℝ × Spacetime n) => self.F p.1 p.2
• Y_smooth : ContDiff ℝ ⊤ self.Y

noncomputable def CM18.FlowMap.jacobian {n : ℕ} (Psi : FlowMap n) (eps : ℝ) (x : Spacetime n) (mu nu : Fin (n + 1)) : ℝ

The $(\mu,\nu)$-component of the Jacobian matrix $M^\mu_{\ \nu} = \partial \widetilde{x}^\mu / \partial x^\nu$ of the flow map $F_\epsilon$ evaluated at $x$.

noncomputable def CM18.FlowMap.invJacobian {n : ℕ} (Psi : FlowMap n) (eps : ℝ) (xt : Spacetime n) (mu nu : Fin (n + 1)) : ℝ

The $(\mu,\nu)$-component of the inverse-Jacobian matrix $(M^{-1})^\mu_{\ \nu} = \partial x^\mu / \partial \widetilde{x}^\nu$, defined as the Jacobian of $F_{-\epsilon}$ at $\widetilde{x}$.

def CM18.transformedField {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (eps : ℝ) (xt : Spacetime n) : ℝ

The transformed scalar field $\widetilde{\phi}(\widetilde{x}) := \phi(F_{-\epsilon}(\widetilde{x}))$ from CM18 Definition 2.0.6.

noncomputable def CM18.transformedGradient {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (eps : ℝ) (xt : Spacetime n) (mu : Fin (n + 1)) : ℝ

The transformed gradient $\widetilde{\nabla}_\mu \widetilde{\phi}(\widetilde{x}) := (M^{-1})^\alpha_{\ \mu} \nabla_\alpha \phi(F_{-\epsilon}(\widetilde{x}))$ from CM18 Definition 2.0.6.

noncomputable def CM18.transformedMetric {n : ℕ} (Psi : FlowMap n) (m : Metric n) (eps : ℝ) (xt : Spacetime n) (mu nu : Fin (n + 1)) : ℝ

The transformed metric components $\widetilde{m}_{\mu\nu}(\widetilde{x}) := (M^{-1})^\alpha_{\ \mu} (M^{-1})^\beta_{\ \nu} m_{\alpha\beta}(F_{-\epsilon}(\widetilde{x}))$ from CM18 Definition 2.0.6.

noncomputable def CM18.transformedInverseMetric {n : ℕ} (Psi : FlowMap n) (mInv : InverseMetric n) (eps : ℝ) (xt : Spacetime n) (mu nu : Fin (n + 1)) : ℝ

The transformed inverse metric components $(\widetilde{m}^{-1})^{\mu\nu}(\widetilde{x}) := M^\mu_{\ \alpha} M^\nu_{\ \beta} (m^{-1})^{\alpha\beta}(F_{-\epsilon}(\widetilde{x}))$ from CM18 Definition 2.0.6.

def CM18.IsCoordinateInvariant {n : ℕ} (L : MetricLagrangian n) : Prop

A metric Lagrangian $\mathcal{L}$ is coordinate invariant (CM18 Definition 2.0.7) if for every smooth flow $\Psi$ on spacetime, $\mathcal{L}(\phi(x), \nabla\phi(x), m(x)) = \mathcal{L}(\widetilde{\phi}(\widetilde{x}), \widetilde{\nabla}\widetilde{\phi}(\widetilde{x}), \widetilde{m}(\widetilde{x}))$ where the transformed fields are as in Definition 2.0.6 and $x = F_{-\epsilon}(\widetilde{x})$.

theorem CM18.chain_rule_scalar_along_inverse_flow {n : ℕ} (Psi : FlowMap n) (f : Spacetime n → ℝ) (hf : ContDiff ℝ ⊤ f) (xt : Spacetime n) : deriv (fun (eps : ℝ) => f (Psi.F (-eps) xt)) 0 = -∑ alpha : Fin (n + 1), Psi.Y xt alpha * spacetimeGradient f xt alpha

Chain rule along the inverse flow: for a smooth scalar function $f$, $\left.\partial_\epsilon\right|_{\epsilon=0} f(F_{-\epsilon}(\widetilde{x})) = -Y^\alpha(\widetilde{x}) \, \nabla_\alpha f(\widetilde{x})$. This is the scalar case of CM18 Proposition 2.0.2.

theorem CM18.flow_deriv_scalar {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (hphi : ContDiff ℝ ⊤ phi) (xt : Spacetime n) : deriv (fun (eps : ℝ) => transformedField Psi phi eps xt) 0 = -∑ alpha : Fin (n + 1), Psi.Y xt alpha * spacetimeGradient phi xt alpha

CM18 Proposition 2.0.2, scalar part: the $\epsilon$-derivative at $\epsilon=0$ of the transformed field equals $-Y^\alpha \nabla_\alpha \phi$.

theorem CM18.invJacobian_zero {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) (alpha mu : Fin (n + 1)) : Psi.invJacobian 0 xt alpha mu = if alpha = mu then 1 else 0

At $\epsilon = 0$, the inverse Jacobian reduces to the Kronecker delta $(M^{-1})^\alpha_{\ \mu}|_{\epsilon=0} = \delta^\alpha_{\ \mu}$.

theorem CM18.deriv_fderiv_swap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (G : ℝ × E → F) (hG : ContDiff ℝ ⊤ G) (t₀ : ℝ) (x₀ v : E) : deriv (fun (t : ℝ) => (fderiv ℝ (fun (x : E) => G (t, x)) x₀) v) t₀ = (fderiv ℝ (fun (x : E) => deriv (fun (t : ℝ) => G (t, x)) t₀) x₀) v

Schwarz-type swap: for a smooth $G : \mathbb{R} \times E \to F$, the time derivative of the partial space differential equals the space differential of the partial time derivative, $\partial_t \, d_x G(t, x_0)\,v = d_x (\partial_t G)(x_0)\,v$.

theorem CM18.invJacobian_differentiableAt_zero {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) (alpha mu : Fin (n + 1)) : DifferentiableAt ℝ (fun (eps : ℝ) => Psi.invJacobian eps xt alpha mu) 0

The inverse Jacobian $(M^{-1})^\alpha_{\ \mu}$ depends differentiably on $\epsilon$ at $\epsilon = 0$.

theorem CM18.hasDerivAt_invJacobian_at_zero {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) (alpha mu : Fin (n + 1)) : HasDerivAt (fun (eps : ℝ) => Psi.invJacobian eps xt alpha mu) (-(fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single mu 1)) 0

The derivative of the inverse Jacobian at $\epsilon = 0$: $\left.\partial_\epsilon\right|_{\epsilon=0} (M^{-1})^\alpha_{\ \mu} = -\nabla_\mu Y^\alpha$. This expands the expansion $(M^{-1})^\mu_{\ \nu} = \delta^\mu_\nu - \epsilon \nabla_\nu Y^\mu + O(\epsilon^2)$ from CM18 Proposition 2.0.1.

theorem CM18.hasDerivAt_scalar_along_inverse_flow {n : ℕ} (Psi : FlowMap n) (g : Spacetime n → ℝ) (hg : ContDiff ℝ ⊤ g) (xt : Spacetime n) : HasDerivAt (fun (eps : ℝ) => g (Psi.F (-eps) xt)) (-∑ alpha : Fin (n + 1), Psi.Y xt alpha * spacetimeGradient g xt alpha) 0

HasDerivAt version of chain_rule_scalar_along_inverse_flow: for a smooth scalar $g$, the function $\epsilon \mapsto g(F_{-\epsilon}(\widetilde{x}))$ has derivative $-Y^\alpha \nabla_\alpha g$ at $\epsilon = 0$.

theorem CM18.fderiv_sum_Y_spacetimeGradient {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (hphi : ContDiff ℝ ⊤ phi) (xt : Spacetime n) (mu : Fin (n + 1)) : (fderiv ℝ (fun (y : Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * spacetimeGradient phi y alpha) xt) (Pi.single mu 1) = ∑ alpha : Fin (n + 1), ((fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single mu 1) * spacetimeGradient phi xt alpha + Psi.Y xt alpha * spacetimeGradient (fun (y : Spacetime n) => spacetimeGradient phi y alpha) xt mu)

Leibniz-rule expansion of $\nabla_\mu (Y^\alpha \nabla_\alpha \phi)$ as a sum, used in proving the gradient transformation rule (CM18 Proposition 2.0.2).

theorem CM18.chain_rule_gradient_along_inverse_flow {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (hphi : ContDiff ℝ ⊤ phi) (xt : Spacetime n) (mu : Fin (n + 1)) : deriv (fun (eps : ℝ) => transformedGradient Psi phi eps xt mu) 0 = -(fderiv ℝ (fun (y : Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * spacetimeGradient phi y alpha) xt) (Pi.single mu 1)

CM18 Proposition 2.0.2, gradient part: for a smooth scalar field $\phi$, $\left.\partial_\epsilon\right|_{\epsilon=0} \widetilde{\nabla}_\mu \widetilde{\phi} = -\nabla_\mu(Y^\alpha \nabla_\alpha \phi)$.

theorem CM18.flow_deriv_gradient {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (hphi : ContDiff ℝ ⊤ phi) (xt : Spacetime n) (mu : Fin (n + 1)) : deriv (fun (eps : ℝ) => transformedGradient Psi phi eps xt mu) 0 = -(fderiv ℝ (fun (y : Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * spacetimeGradient phi y alpha) xt) (Pi.single mu 1)

Restatement of chain_rule_gradient_along_inverse_flow (CM18 Proposition 2.0.2, gradient case): the $\epsilon$-derivative of the transformed gradient at $\epsilon = 0$ equals $-\nabla_\mu(Y^\alpha \nabla_\alpha \phi)$.

theorem CM18.hasDerivAt_metric_component_along_inverse_flow {n : ℕ} (Psi : FlowMap n) (m : Metric n) (xt : Spacetime n) (alpha beta : Fin (n + 1)) (hm : ContDiff ℝ ⊤ fun (y : Spacetime n) => m y alpha beta) : HasDerivAt (fun (eps : ℝ) => m (Psi.F (-eps) xt) alpha beta) (-∑ gamma : Fin (n + 1), Psi.Y xt gamma * (fderiv ℝ (fun (y : Spacetime n) => m y alpha beta) xt) (Pi.single gamma 1)) 0

For a smooth metric component $m_{\alpha\beta}$, the derivative of $\epsilon \mapsto m_{\alpha\beta}(F_{-\epsilon}(\widetilde{x}))$ at $\epsilon = 0$ is $-Y^\gamma \nabla_\gamma m_{\alpha\beta}$.

theorem CM18.chain_rule_metric_along_inverse_flow {n : ℕ} (Psi : FlowMap n) (m : Metric n) (xt : Spacetime n) (mu nu : Fin (n + 1)) (hm : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => m y alpha beta) : deriv (fun (eps : ℝ) => transformedMetric Psi m eps xt mu nu) 0 = -(∑ alpha : Fin (n + 1), m xt alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single mu 1) + ∑ alpha : Fin (n + 1), m xt mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single nu 1) + ∑ alpha : Fin (n + 1), Psi.Y xt alpha * (fderiv ℝ (fun (y : Spacetime n) => m y mu nu) xt) (Pi.single alpha 1))

CM18 Proposition 2.0.2, metric part: $\left.\partial_\epsilon\right|_{\epsilon=0} \widetilde{m}_{\mu\nu} = -(m_{\alpha\nu} \nabla_\mu Y^\alpha + m_{\mu\alpha} \nabla_\nu Y^\alpha + Y^\alpha \nabla_\alpha m_{\mu\nu})$.

theorem CM18.flow_deriv_metric {n : ℕ} (Psi : FlowMap n) (m : Metric n) (xt : Spacetime n) (mu nu : Fin (n + 1)) (hm : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => m y alpha beta) : deriv (fun (eps : ℝ) => transformedMetric Psi m eps xt mu nu) 0 = -(∑ alpha : Fin (n + 1), m xt alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single mu 1) + ∑ alpha : Fin (n + 1), m xt mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single nu 1) + ∑ alpha : Fin (n + 1), Psi.Y xt alpha * (fderiv ℝ (fun (y : Spacetime n) => m y mu nu) xt) (Pi.single alpha 1))

Restatement of chain_rule_metric_along_inverse_flow (CM18 Proposition 2.0.2, metric case): the $\epsilon$-derivative of the transformed metric at $\epsilon=0$ equals $-(m_{\alpha\nu} \nabla_\mu Y^\alpha + m_{\mu\alpha} \nabla_\nu Y^\alpha + Y^\alpha \nabla_\alpha m_{\mu\nu})$.

theorem CM18.jacobian_zero {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) (mu alpha : Fin (n + 1)) : Psi.jacobian 0 xt mu alpha = if mu = alpha then 1 else 0

At $\epsilon = 0$, the Jacobian reduces to the Kronecker delta $M^\mu_{\ \alpha}|_{\epsilon=0} = \delta^\mu_{\ \alpha}$.

theorem CM18.hasDerivAt_jacobian_at_moving_point_zero {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) (mu alpha : Fin (n + 1)) : HasDerivAt (fun (eps : ℝ) => Psi.jacobian eps (Psi.F (-eps) xt) mu alpha) ((fderiv ℝ (fun (y : Spacetime n) => Psi.Y y mu) xt) (Pi.single alpha 1)) 0

Derivative of the Jacobian along the inverse flow at the moving point: $\left.\partial_\epsilon\right|_{\epsilon=0} M^\mu_{\ \alpha}(F_{-\epsilon}(\widetilde{x})) = \nabla_\alpha Y^\mu(\widetilde{x})$. This is the key identity for differentiating the transformed inverse metric.

theorem CM18.chain_rule_inverse_metric_along_flow {n : ℕ} (Psi : FlowMap n) (mInv : InverseMetric n) (xt : Spacetime n) (mu nu : Fin (n + 1)) (hmInv : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => mInv y alpha beta) : deriv (fun (eps : ℝ) => transformedInverseMetric Psi mInv eps xt mu nu) 0 = ∑ alpha : Fin (n + 1), mInv xt alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y mu) xt) (Pi.single alpha 1) + ∑ alpha : Fin (n + 1), mInv xt mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y nu) xt) (Pi.single alpha 1) - ∑ alpha : Fin (n + 1), Psi.Y xt alpha * (fderiv ℝ (fun (y : Spacetime n) => mInv y mu nu) xt) (Pi.single alpha 1)

CM18 Proposition 2.0.2, inverse metric part: $\left.\partial_\epsilon\right|_{\epsilon=0} (\widetilde{m}^{-1})^{\mu\nu} = (m^{-1})^{\alpha\nu} \nabla_\alpha Y^\mu + (m^{-1})^{\mu\alpha} \nabla_\alpha Y^\nu - Y^\alpha \nabla_\alpha (m^{-1})^{\mu\nu}$.

theorem CM18.flow_deriv_inverse_metric {n : ℕ} (Psi : FlowMap n) (mInv : InverseMetric n) (xt : Spacetime n) (mu nu : Fin (n + 1)) (hmInv : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => mInv y alpha beta) : deriv (fun (eps : ℝ) => transformedInverseMetric Psi mInv eps xt mu nu) 0 = ∑ alpha : Fin (n + 1), mInv xt alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y mu) xt) (Pi.single alpha 1) + ∑ alpha : Fin (n + 1), mInv xt mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y nu) xt) (Pi.single alpha 1) - ∑ alpha : Fin (n + 1), Psi.Y xt alpha * (fderiv ℝ (fun (y : Spacetime n) => mInv y mu nu) xt) (Pi.single alpha 1)

Restatement of chain_rule_inverse_metric_along_flow (CM18 Proposition 2.0.2, inverse metric case): the $\epsilon$-derivative of the transformed inverse metric at $\epsilon = 0$.

theorem CM18.exists_ne_fixed_in_erase {n : ℕ} (σ : Equiv.Perm (Fin n)) (hσ : σ ≠ 1) (i : Fin n) : ∃ j ∈ Finset.univ.erase i, σ j ≠ j

For any non-identity permutation $\sigma$ and any index $i$, there exists some $j \ne i$ that $\sigma$ does not fix. Used in the proof of the Jacobi determinant identity.

theorem CM18.det_deriv_trace_identity {n : ℕ} (f' : Fin (n + 1) → Fin (n + 1) → ℝ) : ∑ σ : Equiv.Perm (Fin (n + 1)), ↑↑(Equiv.Perm.sign σ) * ∑ k : Fin (n + 1), (∏ j ∈ Finset.univ.erase k, if σ j = j then 1 else 0) • f' (σ k) k = ∑ k : Fin (n + 1), f' k k

Jacobi-style trace identity: the permutation-sum form of the determinant derivative at the identity matrix collapses to the trace $\sum_k f'_{kk}$.

theorem CM18.jacobi_formula_flow {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) : deriv (fun (eps : ℝ) => (Matrix.of fun (mu nu : Fin (n + 1)) => Psi.invJacobian eps xt mu nu).det) 0 = -∑ alpha : Fin (n + 1), (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single alpha 1)

Jacobi's formula applied to the inverse-Jacobian flow at $\epsilon = 0$: $\left.\partial_\epsilon\right|_{\epsilon=0} \det M^{-1} = -\nabla_\alpha Y^\alpha$, matching the expansion $\det M^{-1} = 1 - \epsilon \nabla_\alpha Y^\alpha + O(\epsilon^2)$ in CM18 Proposition 2.0.1.

theorem CM18.flow_deriv_det_invJacobian {n : ℕ} (Psi : FlowMap n) (xt : Spacetime n) : deriv (fun (eps : ℝ) => (Matrix.of fun (mu nu : Fin (n + 1)) => Psi.invJacobian eps xt mu nu).det) 0 = -∑ alpha : Fin (n + 1), (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) xt) (Pi.single alpha 1)

Restatement of jacobi_formula_flow: the $\epsilon$-derivative of $\det M^{-1}$ at $\epsilon=0$ equals $-\nabla_\alpha Y^\alpha$ (CM18 Proposition 2.0.1, determinant case).

noncomputable def CM18.dL_dm {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (x : Spacetime n) (mu nu : Fin (n + 1)) : ℝ

The partial derivative $\partial \mathcal{L} / \partial m_{\mu\nu}$ of a metric Lagrangian with respect to the $(\mu,\nu)$-entry of the metric, evaluated at $(\phi(x), \nabla\phi(x), m(x))$.

theorem CM18.fderiv_prod_decomp_chain {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (h : E × F → G) (a : E) (b : F) (da : E) (db : F) (hh : DifferentiableAt ℝ h (a, b)) : (fderiv ℝ h (a, b)) (da, db) = (fderiv ℝ (fun (a' : E) => h (a', b)) a) da + (fderiv ℝ (fun (b' : F) => h (a, b')) b) db

Decomposition of the Fréchet derivative on a product: for $h : E \times F \to G$ differentiable at $(a,b)$, $dh_{(a,b)}(da, db) = dh^{(\cdot, b)}_a(da) + dh^{(a, \cdot)}_b(db)$, i.e. the total differential splits into the two partial differentials.

theorem CM18.clm_pi_decomp_chain {n : ℕ} (D : (Fin (n + 1) → ℝ) →L[ℝ] ℝ) (v : Fin (n + 1) → ℝ) : D v = ∑ μ : Fin (n + 1), D (Pi.single μ 1) * v μ

A continuous linear functional on $\mathbb{R}^{n+1}$ decomposes in the standard basis as $D(v) = \sum_\mu D(e_\mu)\, v_\mu$, where $e_\mu$ is the $\mu$-th unit vector.

theorem CM18.clm_dbl_pi_decomp_chain {n : ℕ} (D : (Fin (n + 1) → Fin (n + 1) → ℝ) →L[ℝ] ℝ) (v : Fin (n + 1) → Fin (n + 1) → ℝ) : D v = ∑ μ : Fin (n + 1), ∑ ν : Fin (n + 1), (D fun (μ' ν' : Fin (n + 1)) => if μ' = μ ∧ ν' = ν then 1 else 0) * v μ ν

Matrix version of clm_pi_decomp_chain: a continuous linear functional on the matrix space $\mathbb{R}^{(n+1) \times (n+1)}$ decomposes as $D(v) = \sum_{\mu,\nu} D(E_{\mu\nu})\, v_{\mu\nu}$, where $E_{\mu\nu}$ is the matrix with a single $1$ in position $(\mu,\nu)$.

theorem CM18.deriv_pi_comp_chain {n : ℕ} (f : ℝ → Fin (n + 1) → ℝ) (x : ℝ) (i : Fin (n + 1)) (hf : DifferentiableAt ℝ f x) : deriv f x i = deriv (fun (ε : ℝ) => f ε i) x

For a vector-valued function $f : \mathbb{R} \to \mathbb{R}^{n+1}$, taking the $i$-th component of $f'(x)$ equals the derivative of the scalar component function $\epsilon \mapsto f(\epsilon)_i$.

theorem CM18.deriv_double_pi_comp_chain {n : ℕ} (f : ℝ → Fin (n + 1) → Fin (n + 1) → ℝ) (x : ℝ) (i j : Fin (n + 1)) (hf : DifferentiableAt ℝ f x) : deriv f x i j = deriv (fun (ε : ℝ) => f ε i j) x

Matrix version of deriv_pi_comp_chain: for $f : \mathbb{R} \to \mathbb{R}^{(n+1)\times(n+1)}$, the $(i,j)$ entry of $f'(x)$ equals the derivative of the scalar component $\epsilon \mapsto f(\epsilon)_{ij}$.

theorem CM18.chain_rule_three_arg {n : ℕ} (L : ℝ → (Fin (n + 1) → ℝ) → (Fin (n + 1) → Fin (n + 1) → ℝ) → ℝ) (f₁ : ℝ → ℝ) (f₂ : ℝ → Fin (n + 1) → ℝ) (f₃ : ℝ → Fin (n + 1) → Fin (n + 1) → ℝ) (hL : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × (Fin (n + 1) → Fin (n + 1) → ℝ)) => L p.1 p.2.1 p.2.2) (hf₁ : DifferentiableAt ℝ f₁ 0) (hf₂ : DifferentiableAt ℝ f₂ 0) (hf₃ : DifferentiableAt ℝ f₃ 0) : deriv (fun (ε : ℝ) => L (f₁ ε) (f₂ ε) (f₃ ε)) 0 = deriv (fun (v : ℝ) => L v (f₂ 0) (f₃ 0)) (f₁ 0) * deriv f₁ 0 + ∑ μ : Fin (n + 1), (fderiv ℝ (fun (p : Fin (n + 1) → ℝ) => L (f₁ 0) p (f₃ 0)) (f₂ 0)) (Pi.single μ 1) * deriv (fun (ε : ℝ) => f₂ ε μ) 0 + ∑ μ : Fin (n + 1), ∑ ν : Fin (n + 1), ((fderiv ℝ (fun (m : Fin (n + 1) → Fin (n + 1) → ℝ) => L (f₁ 0) (f₂ 0) m) (f₃ 0)) fun (μ' ν' : Fin (n + 1)) => if μ' = μ ∧ ν' = ν then 1 else 0) * deriv (fun (ε : ℝ) => f₃ ε μ ν) 0

Three-argument chain rule for a Lagrangian $L(v, p, m)$ composed with three smooth families $f_1(\epsilon), f_2(\epsilon), f_3(\epsilon)$: the $\epsilon$-derivative at $0$ decomposes as $\partial_v L \cdot f_1' + \sum_\mu \partial_{p_\mu} L \cdot (f_2)_\mu'

• \sum_{\mu,\nu} \partial_{m_{\mu\nu}} L \cdot (f_3)_{\mu\nu}'$.

theorem CM18.transformedField_at_zero {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (x : Spacetime n) : transformedField Psi phi 0 x = phi x

At $\epsilon = 0$, the transformed scalar field reduces to the original: $\widetilde{\phi}|_{\epsilon=0}(x) = \phi(x)$.

theorem CM18.transformedGradient_at_zero {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (x : Spacetime n) : (fun (mu : Fin (n + 1)) => transformedGradient Psi phi 0 x mu) = spacetimeGradient phi x

At $\epsilon = 0$, the transformed gradient reduces to the original gradient $\nabla\phi(x)$.

theorem CM18.transformedMetric_at_zero {n : ℕ} (Psi : FlowMap n) (m : Metric n) (x : Spacetime n) : (fun (mu nu : Fin (n + 1)) => transformedMetric Psi m 0 x mu nu) = m x

At $\epsilon = 0$, the transformed metric reduces to the original $m(x)$.

theorem CM18.transformedField_differentiable {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (x : Spacetime n) (hphi : ContDiff ℝ ⊤ phi) : DifferentiableAt ℝ (fun (eps : ℝ) => transformedField Psi phi eps x) 0

For smooth $\phi$, the transformed field $\epsilon \mapsto \widetilde{\phi}(x)$ is differentiable at $\epsilon = 0$.

theorem CM18.transformedGradient_differentiable {n : ℕ} (Psi : FlowMap n) (phi : ScalarField n) (x : Spacetime n) (hphi : ContDiff ℝ ⊤ phi) : DifferentiableAt ℝ (fun (eps : ℝ) (mu : Fin (n + 1)) => transformedGradient Psi phi eps x mu) 0

For smooth $\phi$, the transformed gradient $\epsilon \mapsto \widetilde{\nabla}\widetilde{\phi}(x)$ is differentiable at $\epsilon = 0$.

theorem CM18.transformedMetric_differentiable {n : ℕ} (Psi : FlowMap n) (m : Metric n) (x : Spacetime n) (hm : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => m y alpha beta) : DifferentiableAt ℝ (fun (eps : ℝ) (mu nu : Fin (n + 1)) => transformedMetric Psi m eps x mu nu) 0

For a smooth metric, the transformed metric $\epsilon \mapsto \widetilde{m}(x)$ is differentiable at $\epsilon = 0$.

theorem CM18.flow_algebra_simplification {n : ℕ} (L : MetricLagrangian n) (Psi : FlowMap n) (phi : ScalarField n) (m : Metric n) (x : Spacetime n) (hL_smooth : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × (Fin (n + 1) → Fin (n + 1) → ℝ)) => L p.1 p.2.1 p.2.2) (h_scalar : deriv (fun (eps : ℝ) => transformedField Psi phi eps x) 0 = -∑ alpha : Fin (n + 1), Psi.Y x alpha * spacetimeGradient phi x alpha) (h_grad : ∀ (mu : Fin (n + 1)), deriv (fun (eps : ℝ) => transformedGradient Psi phi eps x mu) 0 = -(fderiv ℝ (fun (y : Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * spacetimeGradient phi y alpha) x) (Pi.single mu 1)) (h_metric : ∀ (mu nu : Fin (n + 1)), deriv (fun (eps : ℝ) => transformedMetric Psi m eps x mu nu) 0 = -(∑ alpha : Fin (n + 1), m x alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) x) (Pi.single mu 1) + ∑ alpha : Fin (n + 1), m x mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) x) (Pi.single nu 1) + ∑ alpha : Fin (n + 1), Psi.Y x alpha * (fderiv ℝ (fun (y : Spacetime n) => m y mu nu) x) (Pi.single alpha 1))) (hphi : ContDiff ℝ ⊤ phi) (hm : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => m y alpha beta) : deriv (fun (eps : ℝ) => L (transformedField Psi phi eps x) (fun (mu : Fin (n + 1)) => transformedGradient Psi phi eps x mu) fun (mu nu : Fin (n + 1)) => transformedMetric Psi m eps x mu nu) 0 = -deriv (fun (v : ℝ) => L v (spacetimeGradient phi x) (m x)) (phi x) * ∑ alpha : Fin (n + 1), Psi.Y x alpha * spacetimeGradient phi x alpha - ∑ mu : Fin (n + 1), (fderiv ℝ (fun (p : Fin (n + 1) → ℝ) => L (phi x) p (m x)) (spacetimeGradient phi x)) (Pi.single mu 1) * (fderiv ℝ (fun (y : Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * spacetimeGradient phi y alpha) x) (Pi.single mu 1) - ∑ mu : Fin (n + 1), ∑ nu : Fin (n + 1), dL_dm L phi m x mu nu * (∑ alpha : Fin (n + 1), m x alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) x) (Pi.single mu 1) + ∑ alpha : Fin (n + 1), m x mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) x) (Pi.single nu 1) + ∑ alpha : Fin (n + 1), Psi.Y x alpha * (fderiv ℝ (fun (y : Spacetime n) => m y mu nu) x) (Pi.single alpha 1))

Algebraic combination of the scalar, gradient, and metric variation formulas. Given the three flow-derivative identities (CM18 Proposition 2.0.2) as hypotheses, the $\epsilon$-derivative of $\mathcal{L}(\widetilde{\phi}, \widetilde{\nabla}\widetilde{\phi}, \widetilde{m})$ at $\epsilon=0$ expands by the three-argument chain rule into the explicit sum appearing in CM18 Corollary 2.0.3.

theorem CM18.corollary_deriv_L_flow {n : ℕ} (L : MetricLagrangian n) (Psi : FlowMap n) (phi : ScalarField n) (m : Metric n) (x : Spacetime n) (hL_smooth : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × (Fin (n + 1) → Fin (n + 1) → ℝ)) => L p.1 p.2.1 p.2.2) (hphi : ContDiff ℝ ⊤ phi) (hm : ∀ (alpha beta : Fin (n + 1)), ContDiff ℝ ⊤ fun (y : Spacetime n) => m y alpha beta) : deriv (fun (eps : ℝ) => L (transformedField Psi phi eps x) (fun (mu : Fin (n + 1)) => transformedGradient Psi phi eps x mu) fun (mu nu : Fin (n + 1)) => transformedMetric Psi m eps x mu nu) 0 = -deriv (fun (v : ℝ) => L v (spacetimeGradient phi x) (m x)) (phi x) * ∑ alpha : Fin (n + 1), Psi.Y x alpha * spacetimeGradient phi x alpha - ∑ mu : Fin (n + 1), (fderiv ℝ (fun (p : Fin (n + 1) → ℝ) => L (phi x) p (m x)) (spacetimeGradient phi x)) (Pi.single mu 1) * (fderiv ℝ (fun (y : Spacetime n) => ∑ alpha : Fin (n + 1), Psi.Y y alpha * spacetimeGradient phi y alpha) x) (Pi.single mu 1) - ∑ mu : Fin (n + 1), ∑ nu : Fin (n + 1), dL_dm L phi m x mu nu * (∑ alpha : Fin (n + 1), m x alpha nu * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) x) (Pi.single mu 1) + ∑ alpha : Fin (n + 1), m x mu alpha * (fderiv ℝ (fun (y : Spacetime n) => Psi.Y y alpha) x) (Pi.single nu 1) + ∑ alpha : Fin (n + 1), Psi.Y x alpha * (fderiv ℝ (fun (y : Spacetime n) => m y mu nu) x) (Pi.single alpha 1))

CM18 Corollary 2.0.3: the derivative of the Lagrangian along the flow at $\epsilon = 0$, $\left.\partial_\epsilon\right|_{\epsilon=0} \mathcal{L}(\widetilde{\phi}, \widetilde{\nabla}\widetilde{\phi}, \widetilde{m}) = -\frac{\partial \mathcal{L}}{\partial \phi} Y^\alpha \nabla_\alpha \phi - \frac{\partial \mathcal{L}}{\partial (\nabla_\mu \phi)} \nabla_\mu (Y^\alpha \nabla_\alpha \phi) - \frac{\partial \mathcal{L}}{\partial m_{\mu\nu}} (m_{\alpha\nu} \nabla_\mu Y^\alpha + m_{\mu\alpha} \nabla_\nu Y^\alpha + Y^\alpha \nabla_\alpha m_{\mu\nu})$.

noncomputable def CM18.energyMomentumTensor {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (mInv : InverseMetric n) (x : Spacetime n) (mu nu : Fin (n + 1)) : ℝ

The energy-momentum tensor associated to a metric Lagrangian: $T^{\mu\nu}(x) := 2 \frac{\partial \mathcal{L}}{\partial m_{\mu\nu}}

• (m^{-1})^{\mu\nu} \mathcal{L}(\phi, \nabla\phi, m)$. This is the canonical "Hilbert" energy-momentum tensor obtained by varying the action with respect to the metric.

noncomputable def CM18.tensorDivergence {n : ℕ} (T : Spacetime n → Fin (n + 1) → Fin (n + 1) → ℝ) (x : Spacetime n) (nu : Fin (n + 1)) : ℝ

Divergence of a tensor field $T$ at a point $x$ in the $\nu$ slot: $(\nabla \cdot T)^\nu(x) := \sum_\mu \nabla_\mu T^{\mu\nu}(x)$.

def CM18.SatisfiesEulerLagrange {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) : Prop

A scalar field $\phi$ satisfies the Euler-Lagrange equation for the Lagrangian $\mathcal{L}$ with metric $m$ if the Euler-Lagrange operator vanishes at every spacetime point.

def CM18.matTransposeLM (k : ℕ) : (Fin k → Fin k → ℝ) →ₗ[ℝ] Fin k → Fin k → ℝ

Matrix transpose viewed as an $\mathbb{R}$-linear map $\mathbb{R}^{k \times k} \to \mathbb{R}^{k \times k}$.

noncomputable def CM18.matTransposeCLM (k : ℕ) : (Fin k → Fin k → ℝ) →L[ℝ] Fin k → Fin k → ℝ

Matrix transpose as a continuous $\mathbb{R}$-linear map on $\mathbb{R}^{k \times k}$.

theorem CM18.matTranspose_symm_eq {k : ℕ} (M₀ : Fin k → Fin k → ℝ) (hM₀_symm : ∀ (mu nu : Fin k), M₀ mu nu = M₀ nu mu) : (matTransposeCLM k) M₀ = M₀

A symmetric matrix is fixed by transposition: if $M_0$ is symmetric then $M_0^\top = M_0$.

theorem CM18.fderiv_symmetric_at_symm_point {n : ℕ} (f : (Fin (n + 1) → Fin (n + 1) → ℝ) → ℝ) (M₀ : Fin (n + 1) → Fin (n + 1) → ℝ) (hf_symm : ∀ (M : Fin (n + 1) → Fin (n + 1) → ℝ), f M = f fun (i j : Fin (n + 1)) => M j i) (hM₀_symm : ∀ (mu nu : Fin (n + 1)), M₀ mu nu = M₀ nu mu) (mu nu : Fin (n + 1)) : ((fderiv ℝ f M₀) fun (mu' nu' : Fin (n + 1)) => if mu' = mu ∧ nu' = nu then 1 else 0) = (fderiv ℝ f M₀) fun (mu' nu' : Fin (n + 1)) => if mu' = nu ∧ nu' = mu then 1 else 0

If $f : \mathbb{R}^{(n+1)\times(n+1)} \to \mathbb{R}$ is invariant under transpose and $M_0$ is a symmetric matrix, then the partial derivatives of $f$ at $M_0$ with respect to the $(\mu,\nu)$ and $(\nu,\mu)$ entries coincide.

theorem CM18.dL_dm_symmetric {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (x : Spacetime n) (hm_symm : ∀ (y : Spacetime n) (mu nu : Fin (n + 1)), m y mu nu = m y nu mu) (hL_symm : ∀ (v : ℝ) (p : Fin (n + 1) → ℝ) (M : Fin (n + 1) → Fin (n + 1) → ℝ), L v p M = L v p fun (i j : Fin (n + 1)) => M j i) (mu nu : Fin (n + 1)) : dL_dm L phi m x mu nu = dL_dm L phi m x nu mu

If the Lagrangian $\mathcal{L}$ is invariant under transposing the metric argument and the metric $m$ is symmetric, then $\partial \mathcal{L} / \partial m_{\mu\nu}$ is symmetric in $(\mu,\nu)$.

theorem CM18.energyMomentumTensor_symmetric {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (mInv : InverseMetric n) (x : Spacetime n) (hm_symm : ∀ (y : Spacetime n) (mu nu : Fin (n + 1)), m y mu nu = m y nu mu) (hL_symm : ∀ (v : ℝ) (p : Fin (n + 1) → ℝ) (M : Fin (n + 1) → Fin (n + 1) → ℝ), L v p M = L v p fun (i j : Fin (n + 1)) => M j i) (hmInv_symm : ∀ (y : Spacetime n) (mu nu : Fin (n + 1)), mInv y mu nu = mInv y nu mu) (mu nu : Fin (n + 1)) : energyMomentumTensor L phi m mInv x mu nu = energyMomentumTensor L phi m mInv x nu mu

The energy-momentum tensor is symmetric in $(\mu,\nu)$ whenever the metric, inverse metric, and Lagrangian (in its metric argument) are all symmetric: $T^{\mu\nu} = T^{\nu\mu}$.

theorem CM18.noether_ibp_computation {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (mInv : InverseMetric n) (hL_inv : IsCoordinateInvariant L) (hL_smooth : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × (Fin (n + 1) → Fin (n + 1) → ℝ)) => L p.1 p.2.1 p.2.2) (hphi_smooth : ContDiff ℝ 2 phi) (hphi_EL : SatisfiesEulerLagrange L phi m) (hmInv : ∀ (x : Spacetime n), Matrix.of (mInv x) * Matrix.of (m x) = 1) (hm_symm : ∀ (y : Spacetime n) (mu nu : Fin (n + 1)), m y mu nu = m y nu mu) (K : Set (Spacetime n)) (hK : IsCompact K) (Y : Spacetime n → Spacetime n) (hY : ContDiff ℝ ⊤ Y) (hY_supp : Function.support Y ⊆ K) (nu : Fin (n + 1)) : ∫ (x : Spacetime n) in K, ∑ alpha : Fin (n + 1), tensorDivergence (energyMomentumTensor L phi m mInv) x nu * m x alpha nu * Y x alpha = 0

The integration-by-parts computation underlying Noether's theorem in CM18: for a coordinate invariant Lagrangian, a solution $\phi$ of the Euler-Lagrange equation, and a compactly supported vector field $Y$, the contracted integral $\int_K (\nabla \cdot T)_\nu \, m_{\alpha\nu} \, Y^\alpha\, d^{1+n}x = 0$ vanishes.

theorem CM18.noether_integral_identity {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (mInv : InverseMetric n) (hL_inv : IsCoordinateInvariant L) (hL_smooth : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × (Fin (n + 1) → Fin (n + 1) → ℝ)) => L p.1 p.2.1 p.2.2) (hphi_smooth : ContDiff ℝ 2 phi) (hphi_EL : SatisfiesEulerLagrange L phi m) (hmInv : ∀ (x : Spacetime n), Matrix.of (mInv x) * Matrix.of (m x) = 1) (hm_symm : ∀ (y : Spacetime n) (mu nu : Fin (n + 1)), m y mu nu = m y nu mu) (K : Set (Spacetime n)) (hK : IsCompact K) (Y : Spacetime n → Spacetime n) (hY : ContDiff ℝ ⊤ Y) (hY_supp : Function.support Y ⊆ K) (nu : Fin (n + 1)) : ∫ (x : Spacetime n) in K, ∑ alpha : Fin (n + 1), tensorDivergence (energyMomentumTensor L phi m mInv) x nu * m x alpha nu * Y x alpha = 0

Restatement of noether_ibp_computation as the Noether integral identity: for any compactly supported smooth vector field $Y$, $\int_K (\nabla \cdot T)_\nu \, m_{\alpha\nu} \, Y^\alpha\, d^{1+n}x = 0$.

theorem CM18.duBoisReymond_contracted {n : ℕ} (f : Spacetime n → ℝ) (m : Metric n) (mInv : InverseMetric n) (hmInv : ∀ (x : Spacetime n), Matrix.of (mInv x) * Matrix.of (m x) = 1) (nu : Fin (n + 1)) (hf : ∀ (K : Set (Spacetime n)), IsCompact K → ∀ (Y : Spacetime n → Spacetime n), ContDiff ℝ ⊤ Y → Function.support Y ⊆ K → ∫ (x : Spacetime n) in K, ∑ alpha : Fin (n + 1), f x * m x alpha nu * Y x alpha = 0) (x : Spacetime n) : f x = 0

A contracted du Bois-Reymond / fundamental lemma of the calculus of variations: if for every compactly supported smooth test vector field $Y$ one has $\int_K \sum_\alpha f(x) m_{\alpha\nu}(x) Y^\alpha(x)\, d^{1+n}x = 0$, then $f$ vanishes identically. Uses invertibility of $m$ via $m^{-1}$.

theorem CM18.noether_energy_momentum_divergence_free {n : ℕ} (L : MetricLagrangian n) (phi : ScalarField n) (m : Metric n) (mInv : InverseMetric n) (hL_inv : IsCoordinateInvariant L) (hL_smooth : ContDiff ℝ 2 fun (p : ℝ × (Fin (n + 1) → ℝ) × (Fin (n + 1) → Fin (n + 1) → ℝ)) => L p.1 p.2.1 p.2.2) (hphi_smooth : ContDiff ℝ 2 phi) (hphi_EL : SatisfiesEulerLagrange L phi m) (hmInv : ∀ (x : Spacetime n), Matrix.of (mInv x) * Matrix.of (m x) = 1) (hm_symm : ∀ (y : Spacetime n) (mu nu : Fin (n + 1)), m y mu nu = m y nu mu) (x : Spacetime n) (nu : Fin (n + 1)) : tensorDivergence (energyMomentumTensor L phi m mInv) x nu = 0

Noether's theorem (CM18 main result): for a coordinate-invariant Lagrangian $\mathcal{L}$ and a scalar field $\phi$ satisfying the Euler-Lagrange equation, the energy-momentum tensor is divergence-free, $\nabla_\mu T^{\mu\nu}(x) = 0$ for all $x$ and $\nu$.