PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Coordinate covariance of the Euler-Lagrange expression under time-dependent point transformations

Statement

Let $n \geq 1$ , let $Ω \subseteq R \times R^{n}$ be open and nonempty, and let $X : Ω \to R^{n}$ be of class $C^{3}$ ( $C^{k}$ Euclidean maps and diffeomorphisms) with $X_{q} (t, q)$ invertible for every $(t, q) \in Ω$ (Invertible Euclidean linear maps, Linear map between vector spaces over the same field). Let $O_{x} \subseteq R \times R^{n} \times R^{n}$ be open and let $L : O_{x} \to R$ be of class $C^{2}$ . Put

$O : = {(t, q, v) \in Ω \times R^{n} : (t, X (t, q), X_{t} (t, q) + X_{q} (t, q) v) \in O_{x}}, \tilde{L} (t, q, v) : = L (t, X (t, q), X_{t} (t, q) + X_{q} (t, q) v) .$

Then:

$O$ is open, $O \subseteq R \times R^{n} \times R^{n}$ , and $\tilde{L}$ is of class $C^{2}$ on $O$ ;
with $w : = X_{t} (t, q) + X_{q} (t, q) v$ one has ${\tilde{L}}_{v} (t, q, v) = X_{q} (t, q)^{T} L_{v} (t, X (t, q), w)$ ;
${\tilde{L}}_{q} (t, q, v) = X_{q}^{T} L_{x} + (X_{t q} + X_{q q} [v])^{T} L_{v}$ , where $X_{t q}$ is the $t$ -derivative of $X_{q}$ and $X_{q q} [v]$ is the matrix with entries $\sum_{j} \partial_{j} \partial_{i} X_{k} (t, q) v_{j}$ , all evaluated at $(t, q)$ and $L_{x}, L_{v}$ at $(t, X (t, q), w)$ ;
(transport) let $a < b$ be reals and let $q : [a, b] \to R^{n}$ be a $C^{2}$ curve with $(t, q (t), q^{'} (t)) \in O$ for all $t \in [a, b]$ , put $x (t) : = X (t, q (t))$ , and define $P (t) : = {\tilde{L}}_{v} (t, q (t), q^{'} (t))$ and $p (t) : = L_{v} (t, x (t), x^{'} (t))$ , which are $C^{1}$ . Then

$\frac{d}{d t} P (t) - {\tilde{L}}_{q} (t, q (t), q^{'} (t)) = X_{q} (t, q (t))^{T} (\frac{d}{d t} p (t) - L_{x} (t, x (t), x^{'} (t))) (t \in [a, b]);$

consequently, since $X_{q} (t, q (t))$ is invertible, the Euler–Lagrange expression of $\tilde{L}$ vanishes along $q$ if and only if the Euler–Lagrange expression of $L$ vanishes along $x$ .

Facts & Assumptions

Given: The open sets $Ω, O_{x}$ , the $C^{3}$ map $X$ with everywhere invertible $X_{q}$ , the $C^{2}$ Lagrangian $L$ , a $C^{2}$ curve $q : [a, b] \to R^{n}$ with $(t, q (t), q^{'} (t)) \in O$ , and the shorthand $x (t) : = X (t, q (t))$ .

[F1]

Compositions and finite products of $C^{r}$ maps are $C^{r}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition, $C^{k}$ Euclidean maps and diffeomorphisms), and a map with continuous partial derivatives is totally differentiable with the Jacobian as derivative (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F2]

The chain rule for total derivatives (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ) gives the derivatives of all composites below; in particular $x^{'} (t) = X_{t} (t, q (t)) + X_{q} (t, q (t)) q^{'} (t)$ , so that $x^{'} (t) = w (t, q (t), q^{'} (t))$ , and $\frac{d}{d t} X_{q} (t, q (t)) = X_{q t} (t, q (t)) + X_{q q} (t, q (t)) [q^{'} (t)]$ as matrices.

[F3]

Mixed second partials of a $C^{2}$ function commute (Clairaut--Schwarz theorem for continuous second partial derivatives): since $X$ is $C^{3}$ , its mixed second partials are $C^{1}$ and satisfy $X_{q t} = X_{t q}$ and $\partial_{j} \partial_{i} X_{k} = \partial_{i} \partial_{j} X_{k}$ .

[F4]

If a square matrix $A$ is invertible, then $A^{T} u = 0$ implies $u = 0$ : indeed $A^{T} u = 0$ gives $u \cdot A w = 0$ for all $w$ , and surjectivity of $A$ gives $u \cdot u = 0$ , hence $u = 0$ (Invertible Euclidean linear maps, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, Linear map between vector spaces over the same field, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct; compute the transformed gradients and compare the two Euler–Lagrange expressions along a curve, using the equality of mixed partials of $X$

1.1F1F2algebra

$O$ is the preimage under the continuous map $(t, q, v) \mapsto (t, X (t, q), X_{t} (t, q) + X_{q} (t, q) v)$ of the open set $O_{x}$ , hence open; and $\tilde{L}$ is the composite of the $C^{2}$ map $L$ with that map, which is $C^{2}$ because $X$ is $C^{3}$ and $v$ enters linearly. This proves clause 1.

1.2F2algebra

Clause 2: by the chain rule and the definition of $w$ , $\frac{\partial \tilde{L}}{\partial v_{j}} = \sum_{k} L_{v_{k}} (t, X, w) \frac{\partial w_{k}}{\partial v_{j}} = \sum_{k} L_{v_{k}} (t, X, w) X_{k j} (t, q),$ which is the $j$ -th entry of $X_{q}^{T} L_{v}$ .

1.3F2F3algebra

Clause 3: differentiating $\tilde{L}$ in $q_{i}$ gives $\frac{\partial \tilde{L}}{\partial q_{i}} = \sum_{k} L_{x_{k}} \frac{\partial X_{k}}{\partial q_{i}} + \sum_{k} L_{v_{k}} (\partial_{i} X_{t, k} + \sum_{j} \partial_{i} X_{k, j} v_{j}) = (X_{q}^{T} L_{x})_{i} + ((X_{t q} + X_{q q} [v])^{T} L_{v})_{i},$ as displayed.

2.1F2F3step 1.2step 1.3algebra

Clause 4: by clause 2, $P (t) = X_{q} (t, q (t))^{T} p (t)$ . Differentiating by [F2] and using $X_{q t} = X_{t q}$ from [F3], $\frac{d}{d t} P = (X_{q t} (t, q) + X_{q q} (t, q) [q^{'}])^{T} p + X_{q}^{T} \frac{d}{d t} p = (X_{t q} (t, q) + X_{q q} (t, q) [q^{'}])^{T} p + X_{q}^{T} \frac{d}{d t} p .$ By clause 3 evaluated at $(t, q (t), q^{'} (t))$ , ${\tilde{L}}_{q} (t, q, q^{'}) = X_{q}^{T} L_{x} + (X_{t q} + X_{q q} [q^{'}])^{T} L_{v} .$ Subtracting and using $p = L_{v} (t, x, x^{'})$ cancels the bracket terms and gives the displayed transport identity.

3.1F4step 2.1given∎

Consequence: if $X_{q} (t, q (t))$ is invertible, then by [F4] the identity $X_{q}^{T} u = 0$ implies $u = 0$ ; applying this to $u = \frac{d}{d t} p - L_{x} (t, x, x^{'})$ , the vanishing of $\frac{d}{d t} P - {\tilde{L}}_{q}$ is equivalent to the vanishing of $\frac{d}{d t} p - L_{x}$ . This proves clause 4.

Remarks

The transformation is restricted to the configuration variables; no transformation of the time variable is performed here. The general point transformation that also changes time, together with the resulting Noether charge, is treated in Noether identity for point transformations with time reparametrisation: the conserved charge $p \cdot ξ - E τ - B$ .
The $C^{3}$ hypothesis makes $(t, q, v) \mapsto (t, X, X_{t} + X_{q} v)$ a $C^{2}$ map and hence ensures the transformed Lagrangian is $C^{2}$ . The mixed second derivatives used in transport already commute for $C^{2}$ $X$ ; that weaker assumption alone does not ensure the claimed $C^{2}$ transformed chart.

Coordinate covariance of the Euler-Lagrange expression under time-dependent point transformations

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources