Vector Space Methods VII: Euler–Lagrange EquationsTextbook
## Motivation The calculus of variations replaces optimization over finitely many coordinates by optimization over paths. Its necessary conditions underlie geodesics, minimum-energy curves, classical mechanics, and many optimal-control models. Chapter 7 of David G. Luenberger's [*Optimization by Vector Space Methods*](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods) presents this transition as an application of differentiation in normed vector spaces: a local extremum first forces every directional derivative to vanish, and the resulting integral identity forces a differential equation along the optimizing path. This mission formalizes the scalar, fixed-endpoint version in §§7.4–7.5. The target is intentionally the theorem actually isolated by the source, not a stronger modern Sobolev-space variant. ## Setting Fix real numbers $a<b$. A **$C^1$ path on the segment** is represented in Lean by two functions, $x,\dot x:\mathbb R\to\mathbb R$. Both are continuous on $[a,b]$, and $x$ has derivative $\dot x(t)$ at every $t\in(a,b)$. Ordinary two-sided derivatives are not demanded at $a$ or $b$; this makes the formal endpoint convention match the one-sided role of endpoints in a closed interval. Let $L(y,v,t)$ be a scalar Lagrangian. Along a candidate path, write $$ L_x(t)=\frac{\partial L}{\partial y}(x(t),\dot x(t),t),\qquad L_v(t)=\frac{\partial L}{\partial v}(x(t),\dot x(t),t). $$ The Lean statement records these partial derivatives with `HasDerivAt` and assumes that $L_x$ and $L_v$ are continuous on $[a,b]$. A **fixed-endpoint variation** is another $C^1$ pair $(h,\dot h)$ with $h(a)=h(b)=0$. The first variation already computed from the action is $$ \delta J(x;h)=\int_a^b\bigl(L_x(t)h(t)+L_v(t)\dot h(t)\bigr)\,dt. $$ The main theorem begins from the stationarity identity $\delta J(x;h)=0$ for every such variation. It does not claim that the complete passage from a local extremum in Luenberger's $C^1$ norm to this integral formula has already been bundled into the root statement. ## Formalization targets ### Main goal: Euler–Lagrange equation From the computed first-variation identity, prove that $$ \frac{d}{dt}L_v(t)=L_x(t)\qquad(t\in(a,b)). $$ The conclusion is expressed as `HasDerivAt Lv (Lx t) t`, so it asserts both differentiability of $L_v$ and the equality of its derivative with $L_x$. This is equation (2) and the conclusion reached on printed pages 180–181. ### Milestones The first milestone formalizes §7.4, Theorem 1: a local minimum or maximum of a real functional has zero derivative along every direction whenever that scalar directional derivative exists. The remaining milestones are the three fixed-endpoint fundamental lemmas from §7.5. They respectively show that a continuous coefficient annihilating all variations is zero, that a continuous coefficient annihilating all variation derivatives is constant, and that an identity involving both $h$ and $\dot h$ forces the second coefficient to have derivative equal to the first. These are stated with the same $C^1$ variation class used by the goal. ## Significance The result turns an infinite family of scalar integral equalities into a pointwise differential equation. Once available, the same interface can support standard variational examples by supplying a concrete $L$, its two partial derivatives, and a stationary path. It also provides the analytic core needed before treating natural boundary conditions, vector-valued paths, higher derivatives, or weak Euler–Lagrange equations. The formalization adds reusable interval-sensitive infrastructure. In particular, `IsC1OnSegment` separates a path from its chosen continuous derivative and avoids silently imposing derivatives outside the optimization interval. The three fundamental lemmas are useful independently of the named Euler–Lagrange theorem: they are test-function principles for interval integrals and can serve later missions involving integration by parts or weak formulations. The mathematics is classical and proved in the cited text; the open work is a machine-checked Lean development of these exact statements in the pinned Mathlib environment. ## Difficulty The source argument uses informal phrases such as “arbitrary $C^1$ function vanishing at the endpoints” and treats endpoint differentiation according to standard calculus convention. In Lean, those phrases must determine a precise domain, derivative witness, continuity requirement, and interval-integral orientation. Replacing $C^1$ variations by merely continuous functions would change Lemmas 2 and 3, while requiring `HasDerivAt` at the endpoints would add a hypothesis not present in the book. Another tempting shortcut is to assume from the outset that $L_v$ is differentiable and then use integration by parts. That would trivialize the central regularity conclusion of Lemma 3: the book derives differentiability of $L_v$ from stationarity and continuity. The root therefore assumes only continuity of the two coefficient functions and concludes a `HasDerivAt` assertion on the open interval. Conversely, constructing the first variation from a local extremum of the action requires a separate differentiation-under-the-integral development and a topology on bundled $C^1$ paths; it is not hidden inside the main goal. ## Formalization scope The scalar field, path values, time variable, and action values are all real. The interval is nondegenerate through the explicit hypothesis $a<b$. Integrals use Mathlib's oriented interval integral, but all principal statements are made in the forward orientation. Paths and variations are total functions on $\mathbb R$ whose relevant regularity is restricted to $[a,b]$. The Lagrangian is finite-valued. No measurability or integrability premise is omitted: continuity of the coefficient and variation factors on the compact interval supplies the intended finite integrals. The goal starts from an already computed first-variation identity. Contributions connecting a genuine local extremum of the action in the norm $\max|x|+\max|\dot x|$ to that identity are welcome as a strengthening, but they must not be advertised as part of the present root theorem. Other welcome contributions include reusable continuous test-function constructions and endpoint-aware interval integration lemmas. Sobolev paths, vector-valued state spaces, free endpoints, and weak derivatives are outside this mission and should be proposed separately rather than obtained by weakening the stated hypotheses until the result becomes vacuous. ## Selected references - David G. Luenberger, *Optimization by Vector Space Methods*, John Wiley & Sons, 1969, Chapter 7, §§7.4–7.5, pp. 178–181; definition of $D[a,b]$ on p. 23. [Open Library record](https://openlibrary.org/books/OL7612943M/Optimization_by_Vector_Space_Methods)