Motivation

In 1918 Emmy Noether published Invariante Variationsprobleme (Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-phys. Klasse, 235–257), answering a question raised by Hilbert and Klein about the status of energy conservation in the general theory of relativity. The paper proves two theorems that tie the symmetries of a variational integral to structural properties of its Euler–Lagrange equations: continuous symmetries depending on finitely many parameters produce divergence identities ("conservation laws"), while symmetries depending on arbitrary functions produce identities among the Euler–Lagrange expressions themselves, so that some of the field equations are consequences of the others. The first theorem is the source of the correspondence between time translation and energy, space translation and momentum, rotation and angular momentum; the second underlies the Bianchi-type identities of generally covariant theories and the gauge identities of field theory.

This mission formalizes the two theorems of §1 of the paper, together with the chain of identities of §2 and §3 by which Noether derives them, in the case of first-order Lagrangians.

Setting

Fix integers $n$ (independent variables), $m$ (dependent variables). Points of the base are $x = (x_1,\dots,x_n) \in \mathbb{R}^n$, and a field is a map $u : \mathbb{R}^n \to \mathbb{R}^m$, written componentwise $u_i(x)$. Write $\partial_l g$ for the derivative of a scalar function $g$ on $\mathbb{R}^n$ along the $l$-th coordinate direction, and

$$\operatorname{Div} A \;=\; \sum_{l=1}^{n} \partial_l A_l$$

for the divergence of a vector field $A = (A_1,\dots,A_n)$ on $\mathbb{R}^n$.

A Lagrangian is a function $f(x, q, v)$ of the point $x \in \mathbb{R}^n$, of the field value $q \in \mathbb{R}^m$, and of the array of first derivatives $v = (v_{l i}) \in \mathbb{R}^{n \times m}$. Along a field $u$ one writes $f[u](x) = f\bigl(x, u(x), (\partial_l u_i(x))_{l,i}\bigr)$, and the integral under study is $I = \int f[u]\,dx$. The momenta are

$$p_{l i}[u](x) \;=\; \frac{\partial f}{\partial v_{l i}}\bigl(x, u(x), (\partial u)(x)\bigr),$$

and the Lagrange expressions — the left-hand sides of the Euler–Lagrange equations — are

$$\psi_i[u](x) \;=\; \frac{\partial f}{\partial q_i}\bigl(x, u(x), (\partial u)(x)\bigr) \;-\; \sum_{l=1}^{n} \partial_l\, p_{l i}[u](x).$$

An infinitesimal transformation is given by generators $\Delta x = (\Delta x_l)$ on the independent variables and $\Delta u = (\Delta u_i)$ on the dependent ones. Noether's equation (9) replaces them by the variation at fixed $x$,

$$\delta u_i \;=\; \Delta u_i \;-\; \sum_{l=1}^{n} \frac{\partial u_i}{\partial x_l}\,\Delta x_l ,$$

and the corresponding variation of the Lagrangian is

$$\delta f \;=\; \sum_{i=1}^{m}\Bigl( \frac{\partial f}{\partial q_i}\,\delta u_i + \sum_{l=1}^{n} \frac{\partial f}{\partial v_{l i}}\, \partial_l \delta u_i \Bigr).$$

Two vector fields organise the boundary terms: the partial-integration vector $A_l = -\sum_i p_{l i}\,\delta u_i$ of equation (3), and Noether's

$$B_l \;=\; A_l \;-\; f[u]\,\Delta x_l \qquad\text{(equation (12))}.$$

Invariance of $I$ enters through Noether's equation (11), the pointwise identity

$$\delta f \;+\; \operatorname{Div}\bigl(f[u]\,\Delta x\bigr) \;=\; 0 ,$$

which the paper derives in §2 from the vanishing of $\Delta I$ over every region.

Target

The goal theorem is Theorem I of the paper, in the first-order case, in the form Noether states as equation (13). Given $\rho$ generators $\bigl(\Delta x^{(r)}, \Delta u^{(r)}\bigr)$, $r = 1,\dots,\rho$, each satisfying the invariance identity (11) with its own $\delta u^{(r)}$ from (9), one has for every $r$ and every $x$

$$\sum_{i=1}^{m} \psi_i[u]\;\delta u^{(r)}_i \;=\; \operatorname{Div} B^{(r)}, \qquad B^{(r)}_l \;=\; -\sum_{i=1}^m p_{l i}\,\delta u^{(r)}_i \;-\; f[u]\,\Delta x^{(r)}_l .$$

The milestones are the intermediate statements of the paper, in the order in which it proves them: the central identity (3), the passage from the invariance of the integral to the pointwise identity (11), the single-generator divergence identity (12), the conservation law $\operatorname{Div} B = 0$ on solutions of the Euler–Lagrange equations (§3), the converse of Theorem I (§3), and Theorem II in the form of the dependency relations (16) for a group depending on arbitrary functions entering to first order.

Significance

Theorem I is the general statement behind every "first integral from a symmetry" argument in mechanics and field theory; Theorem II is the statement that a variational theory invariant under a group of arbitrary functions has field equations that are not independent — $\rho$ of them follow from the rest — which is the group-theoretic form of the failure of a proper energy conservation law in general relativity that Hilbert had asserted. The two theorems are used constantly and stated loosely; a formal version fixes exactly which hypotheses are needed and what the conclusion says.

Mathlib contains the differential-calculus and measure-theoretic infrastructure used here (Fréchet derivatives, integration on $\mathbb{R}^n$, compactly supported test functions, and the standard vanishing lemma for locally integrable functions tested against smooth compactly supported functions), but no calculus of variations: there is no Euler–Lagrange operator, no first-variation formula, and no Noether theorem. This mission supplies the first-order, finite-dimensional-base version of that material, with definitions that later missions (higher-order Lagrangians, the $\kappa$-th order identity (6), mixed groups) can extend.

Difficulty

The algebraic core — the central identity (3) and the passage to (12) — is a product rule plus a reindexing, and the real work is elsewhere.

Two steps are genuinely analytic. First, Noether's inference from "the integral of the integrand vanishes over every region" to "the integrand vanishes pointwise" (equations (10)–(11)) requires the regularity of the integrand to be used explicitly. Second, Theorem II's equation (16) requires integrating by parts against an arbitrary function and then applying the fundamental lemma of the calculus of variations in $\mathbb{R}^n$: the arbitrary functions of the group must be specialized to compactly supported test functions before the boundary terms can be discarded.

The remaining difficulty is bookkeeping: every statement must carry the differentiability hypotheses that make each derivative in it meaningful, since in Lean an undefined derivative silently evaluates to zero rather than failing.

Formalization scope

The formalization is in the first-order setting: the Lagrangian depends on $x$, on $u$, and on the first derivatives of $u$ only. The base is $\mathbb{R}^n$ with $n$ fixed but arbitrary, and fields are globally defined maps $\mathbb{R}^n \to \mathbb{R}^m$; no boundary conditions, no manifolds, and no jet bundles are used. The group is not formalized as a group: as in §2 of the paper, only its infinitesimal generators $\Delta x$, $\Delta u$ enter, and the invariance hypothesis is Noether's identity (11). The linear independence of the $\rho$ divergence relations, which Noether argues from the essentiality of the parameters, is not part of the formal statements.

Derivatives are Fréchet derivatives: $\partial_l g(x)$ is the derivative of $g$ at $x$ applied to the $l$-th standard basis vector, and partial derivatives of the Lagrangian are derivatives of the corresponding partially applied function. Because Lean's derivative operator returns $0$ at points of non-differentiability, each statement carries explicit differentiability hypotheses for exactly the functions whose derivatives it mentions; a solver may not assume more.

The statements are not vacuous: the hypotheses of every milestone are satisfied, for instance, by smooth Lagrangians and smooth fields, and the invariance hypothesis (11) is satisfied by the classical examples (a Lagrangian independent of $x_l$ with $\Delta x = e_l$, $\Delta u = 0$). Degenerate parameter values are admitted and behave as expected: for $m = 0$ or $n = 0$ the sums are empty and the identities reduce to $0 = 0$, and for $\rho = 0$ the goal quantifies over an empty index set.

Contributions of independent interest that this mission would welcome: a reusable statement of the fundamental lemma of the calculus of variations on $\mathbb{R}^n$ in the form needed for (16), and the higher-order analogue of the central identity, Noether's equation (6).

Selected references

• E. Noether, Invariante Variationsprobleme, Nachr. d. König. Gesellsch. d. Wiss. zu Göttingen, Math-phys. Klasse (1918), 235–257. English translation by M. A. Tavel, Invariant Variation Problems, Transport Theory and Statistical Physics 1 (3) (1971), 183–207; arXiv:physics/0503066.
• Y. Kosmann-Schwarzbach, The Noether Theorems: Invariance and Conservation Laws in the Twentieth Century, Springer (2011), DOI:10.1007/978-0-387-87868-3.
• P. J. Olver, Applications of Lie Groups to Differential Equations, 2nd ed., Springer (1993), DOI:10.1007/978-1-4612-4350-2.