Calculus of Variations

Motivation

A function that is bounded below need not attain its infimum: $e^x$ on $\mathbb{R}$ has infimum $0$ and no minimizer. The classical "variational principle" says that at a minimizer $\bar u$ of a differentiable functional, $F'(\bar u)=0$. Without compactness there may be no minimizer, and the principle has nothing to say. In 1974 Ivar Ekeland showed that a weaker statement survives in every complete metric space: next to any approximate minimizer lies a point that is the exact, strict minimizer of a slightly perturbed function (Ekeland 1974).

The result is now a standard tool in nonlinear analysis, optimization and the calculus of variations. It yields approximate first-order conditions ($\|F'(v)\|_*\le\varepsilon$) without existence of minimizers, approximate Lagrange multiplier rules, and approximate maximum principles in optimal control; Ekeland's survey (Ekeland 1979) collects many of these uses.

Timeline. Bishop and Phelps introduced the partial order on a Banach space times $\mathbb{R}$ that underlies the proof, in their study of support functionals of convex sets (Bishop–Phelps, The support functional of a convex set, Proc. Symp. Pure Math. 7, AMS, 1963). Brøndsted and Rockafellar used it in 1965 to obtain subdifferentiability properties of convex functions on Banach spaces (Brøndsted–Rockafellar 1965), and Browder applied it to nonconvex subsets of Banach spaces (Bull. AMS 79, 1973). Ekeland's 1974 article, formalized here, isolates the device as a principle valid in every complete metric space for lower semicontinuous functions with values in $\mathbb{R}\cup\{+\infty\}$, and applies it to Gâteaux-differentiable functions, constrained optimization, Plateau's problem, geodesics and optimal control.

Setting

Let $(V,d)$ be a complete metric space. Let $F:V\to\mathbb{R}\cup\{+\infty\}$ be lower semicontinuous (for every $c$ the set $\{F\le c\}$ is closed), not identically $+\infty$, and bounded from below:

$$\inf F > -\infty. \tag{1.1}$$

For $\varepsilon>0$, a point $u\in V$ is an $\varepsilon$-minimizer if

$$\inf F \le F(u) \le \inf F + \varepsilon. \tag{1.2}$$

For $\alpha>0$, the Bishop–Phelps order on $V\times\mathbb{R}$ is

$$(v_1,a_1)\prec(v_2,a_2)\iff (a_2-a_1)+\alpha\,d(v_1,v_2)\le 0. \tag{1.6}$$

In Lean it is EkelandVP.General.bpLE α p q, read $p\prec q$. The epigraph of $F$ is $S=\{(v,a)\mid a\ge F(v)\}\subseteq V\times\mathbb{R}$ (1.15).

In §2, $V$ is a real Banach space with dual $V^*$, and $F$ is Gâteaux-differentiable with derivative $F':V\to V^*$ (EkelandVP.General.IsGateauxDiff F F'): at every $u_0$ with $F(u_0)<+\infty$, $\frac{d}{dt}F(u_0+tv)|_{t=0}=\langle F'(u_0),v\rangle$ for every $v$ (2.1).

Formalization targets

Goal: Theorem 1.1 (p. 324)

For every $u$ satisfying (1.2) and every $\lambda>0$ there is $v\in V$ with

$$F(v)\le F(u),\qquad d(u,v)\le\lambda,\qquad \forall w\ne v:\ F(w)>F(v)-\frac{\varepsilon}{\lambda}\,d(v,w). \tag{1.3–1.5}$$

The parameters $\varepsilon$ and $\lambda$ are free; the trade-off between closeness to $u$ and the size of the perturbation is the content of the theorem.

Milestones (§1)

1. For $\alpha>0$, $\prec$ is reflexive, antisymmetric and transitive (p. 325).
2. For every $(v_1,a_1)$, the set $\{(v,a)\mid (v_1,a_1)\prec(v,a)\}$ is closed in $V\times\mathbb{R}$ (p. 325).
3. Lemma 1.2 (p. 325): if $S\subseteq V\times\mathbb{R}$ is closed and $a\ge m$ on $S$ for some $m$ (1.7), then every $(v_1,a_1)\in S$ lies below a $\prec$-maximal element of $S$.

Consequences (§2)

• Corollary 2.3 (p. 328): for $V$ Banach, $F$ l.s.c. and Gâteaux-differentiable with $-\infty<\inf F<+\infty$, and every $\varepsilon>0$, there is $v_\varepsilon$ with $F(v_\varepsilon)-\inf F\le\varepsilon^2$ and $\|F'(v_\varepsilon)\|_*\le\varepsilon$.
• Corollary 2.4 (p. 328): if moreover $F(v)\ge k\|v\|+c$ with $k>0$, then $F'(V)$ is dense in $kB^*$.
• Corollary 2.5 (p. 329): if $F(v)\ge\Phi(\|v\|)$ with $\Phi$ continuous and $\Phi(t)/t\to\infty$, then $F'(V)$ is dense in $V^*$.

Significance

The result. Theorem 1.1 replaces "a minimizer exists" by "a strict minimizer of a Lipschitz perturbation exists nearby", with explicit control of both the distance and the perturbation. With $\lambda=\sqrt{\varepsilon}$ this gives a point that is $\varepsilon$-optimal, $\sqrt{\varepsilon}$-close to $u$, and $\sqrt{\varepsilon}$-stationary in the metric sense. Corollary 2.3 is the form announced in the paper's abstract: a differentiable function with a finite lower bound has points where $F$ is almost minimal and $\|F'\|_*$ is arbitrarily small. Later sections of the same paper use Theorem 1.1 for approximate Lagrange multiplier rules (§3) and an approximate Pontryagin maximum principle (§7), which are the subjects of missions II and III of this series.

Formalizing it. The theorem is proved; this mission formalizes the paper's own route (the order (1.6), Lemma 1.2, then Theorem 1.1) and its first applications in §2. The pinned Mathlib has no statement of Ekeland's principle, of the Caristi fixed point theorem, or of the Bishop–Phelps order, and the platform has none either. A machine-checked Theorem 1.1 for extended-real-valued functions would be directly reusable by every later mission that needs approximate optimality without compactness.

Difficulty

The obvious argument — take a minimizing sequence and pass to a limit — fails because nothing makes a minimizing sequence converge: $V$ is not compact, and a minimizing sequence of $e^x$ escapes to $-\infty$. Completeness only helps for Cauchy sequences, so one must construct a sequence that is Cauchy. The limit must moreover be maximal for the order (1.6), not merely a limit point, and that maximality is what produces the strict inequality (1.5). Lemma 1.2 is where this difficulty sits. In §2, the passage from the metric statement (1.5) to a bound on $\|F'(v)\|_*$ requires $F$ to be finite near $v$ along every line, which the Gâteaux hypothesis supplies.

Formalization scope

• $V$ is a MetricSpace with CompleteSpace; $d(u,v)$ is dist u v. $V\times\mathbb{R}$ carries the product topology; only closedness of subsets of it is used.
• $F:V\to$ EReal. "Bounded from below" (1.1) is $\bot<\inf_v F(v)$; it also excludes the value $-\infty$, which the paper's codomain does not contain. "Not identically $+\infty$" is $\exists v_0,\ F(v_0)\ne\top$. Lower semicontinuity is Mathlib's LowerSemicontinuous.
• (1.2) is assumed in the form $F(u)\le\inf F+\varepsilon$ with $\varepsilon>0$ real (the left half is automatic). $\lambda$ is named lam.
• (1.5) is $F(v)-\frac{\varepsilon}{\lambda}d(v,w)<F(w)$ for all $w\ne v$, strict, with the paper's argument order $d(v,w)$. Since $F(v)$ is finite under the hypotheses, the EReal subtraction is ordinary.
• A trivializing formalization is ruled out: $F$ is not real-valued (the value $+\infty$ is what lets §3 apply the theorem to $F$ plus the indicator of a closed set), (1.5) is strict and quantified over all $w\ne v$, and the conclusion is not weakened to $d(u,v)<\infty$ or $\le$ in (1.5).
• In §2, $V$ is a real NormedSpace with CompleteSpace, $F'$ is a function $V\to(V\to_L\mathbb{R})$, and Gâteaux differentiability requires $t\mapsto F(u_0+tv)$ to be finite near $t=0$ before taking a real derivative; without this, EReal.toReal $(\pm\infty)=0$ would let an infinite function have a junk derivative. Density of $F'(V)$ is stated for derivatives taken at points where $F<+\infty$.
• Theorem 2.2 is not part of this mission: its conclusion (2.4) is printed as the strict $\|v-u\|<\lambda$, while its one-line proof from Theorem 1.1 gives only $\le\lambda$. Corollaries 2.3–2.5 do not depend on the strict form.

Contributions welcome: proofs of the milestones (the first two are short; Lemma 1.2 is the core), of Theorem 1.1, and of the §2 corollaries; a reusable Caristi fixed point theorem built on the same order would be a natural addition.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974), 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• E. Bishop, R. R. Phelps, The support functional of a convex set, in Convexity (V. Klee, ed.), Proc. Symp. Pure Math. 7, Amer. Math. Soc., 1963, 27–35. (Reference [4] of Ekeland 1974.)
• A. Brøndsted, R. T. Rockafellar, On the subdifferentiability of convex functions, Proc. Amer. Math. Soc. 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8
• F. E. Browder, Normal solvability for nonlinear mappings into Banach spaces, Bull. Amer. Math. Soc. 79 (1973), 328–350. https://doi.org/10.1090/S0002-9904-1973-13152-9

Motivation

Second-order elliptic equations in divergence form, such as $-\nabla\cdot(A\nabla u) + b\cdot\nabla u + cu = f$, model steady diffusion, electrostatics in inhomogeneous media and linear elasticity. They are also the stationary part of every parabolic and hyperbolic problem studied later in the same notes. When the coefficients are only bounded and measurable, classical solutions need not exist. The modern theory replaces them by weak solutions in the Sobolev space $H^1_0(\Omega)$ and settles existence, uniqueness and solvability by Hilbert-space methods. This mission formalizes that theory as presented in Chapter 4 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014). The chapter follows the standard development of Evans, Partial Differential Equations, Chapter 6, and of Gilbarg–Trudinger, Chapter 8.

Timeline. Riesz (1907) and Fréchet represented bounded functionals on Hilbert spaces. Fredholm (1903) proved the alternative for integral equations of the second kind, and Riesz (1918) extended it to compact operators. Lax and Milgram (1954) removed the symmetry assumption from the Riesz approach, and Gårding (1953) proved the coercivity estimate for elliptic forms. Together these give the existence and Fredholm theory for the Dirichlet problem stated here.

Setting

Let $\Omega \subseteq \mathbb{R}^n$ be open. A test function is a smooth $\phi$ with compact support in $\Omega$. The space $H^1_0(\Omega)$ is the closure of the test functions in the norm $\|u\|_{H^1_0}^2 = \int_\Omega (u^2 + |Du|^2)\,dx$; each element carries a function $u$ and a weak gradient $Du$, both square-integrable. $H^{-1}(\Omega)$ is the space of bounded linear functionals on $H^1_0(\Omega)$, and $f \in L^2(\Omega)$ acts on it by $\langle f, \phi\rangle = \int_\Omega f\phi\,dx$.

Given coefficients $a_{ij}, b_i, c \in L^\infty(\Omega)$ with $a_{ij} = a_{ji}$, the operator is

$$Lu = -\sum_{i,j=1}^n \partial_i(a_{ij}\partial_j u) + \sum_{i=1}^n \partial_i(b_i u) + cu .$$

It is uniformly elliptic if $\sum_{i,j} a_{ij}(x)\xi_i\xi_j \ge \theta|\xi|^2$ for some $\theta > 0$, almost every $x$ and every $\xi$. Its bilinear form on $H^1_0(\Omega)$ is

$$a(u,v) = \int_\Omega \Big(\sum_{i,j} a_{ij}\,\partial_i u\,\partial_j v - \sum_i b_i\,u\,\partial_i v + c\,uv\Big)dx ,$$

and the formal adjoint $L^*u = -\sum\partial_i(a_{ij}\partial_j u) - \sum b_i\partial_i u + cu$ has the form $a^*(u,v) = a(v,u)$. For $\mu \in \mathbb{R}$, $u$ is a weak solution of $Lu + \mu u = f$ with $u = 0$ on $\partial\Omega$ if $u \in H^1_0(\Omega)$ and $a(u,\phi) + \mu\int_\Omega u\phi = \langle f,\phi\rangle$ for all $\phi \in H^1_0(\Omega)$. The resolvent $K = (L+\mu I)^{-1}$ maps $f \in L^2(\Omega)$ to that solution.

A bounded operator $T$ on a Hilbert space is Fredholm if its kernel is finite-dimensional and its range is closed with finite-dimensional orthogonal complement. Its index is $\dim\ker T - \dim(\operatorname{ran}T)^\perp$.

Formalization targets

Goal: the Fredholm alternative (Theorem 4.24)

For $\Omega$ bounded, $L$ uniformly elliptic and $\lambda \in \mathbb{R}$, exactly one of the following holds:

$$\text{(1)}\quad \ker(L^*-\lambda) = 0 \ \text{ and } \ \forall f \in L^2(\Omega)\ \exists!\,u \in H^1_0(\Omega):\ Lu - \lambda u = f;$$ $$\text{(2)}\quad 0 < \dim\ker(L-\lambda) = \dim\ker(L^*-\lambda) < \infty,\quad Lu - \lambda u = f \text{ solvable} \iff f \perp_{L^2} \ker(L^*-\lambda),$$

with non-unique solutions in case (2). Every kernel and equation is meant in the weak sense on $H^1_0(\Omega)$.

Milestones

• Poincaré inequality (Theorem 4.9): $\int_\Omega u^2 \le C\int_\Omega |Du|^2$ on $H^1_0(\Omega)$ when $\Omega$ lies between two parallel hyperplanes. Unique solvability of $-\Delta u = f \in H^{-1}(\Omega)$ (Theorem 4.11).
• The Lax–Milgram theorem (Theorem 4.20).
• Energy estimates (Theorem 4.21): $C_1\|u\|_{H^1_0}^2 \le a(u,u) + \gamma\|u\|_{L^2}^2$ and $|a(u,v)| \le C_2\|u\|_{H^1_0}\|v\|_{H^1_0}$, with the explicit $\gamma = \theta - c_0$ if $b = 0$ and $\gamma = \tfrac{1}{2\theta}\sum\|b_i\|_{L^\infty}^2 + \tfrac\theta2 - c_0$ otherwise.
• Unique weak solvability of $Lu + \mu u = f$ for $\mu \ge \gamma$ (Theorem 4.22). The resolvent $K$ is bounded on $L^2(\Omega)$ with adjoint $(L^*+\mu I)^{-1}$, and it is compact when $\Omega$ is bounded (Theorem 4.23).
• The abstract Fredholm alternative for Fredholm operators of index zero (Theorem 4.50).
• The spectral theorem for symmetric $L$ (Theorem 4.25): eigenvalues $\lambda_1 \le \lambda_2 \le \dots \to \infty$ of finite multiplicity, with an orthonormal eigenbasis of $L^2(\Omega)$.

Significance

The Fredholm alternative is the complete linear solvability theory of the Dirichlet problem for general elliptic operators on bounded domains. Uniqueness for the homogeneous problem is equivalent to existence for all data. When uniqueness fails, the obstruction is a finite set of orthogonality conditions given by the adjoint problem. This feeds directly into the spectral theory of Theorem 4.25, into eigenfunction expansions, and into the existence theory for parabolic and hyperbolic equations (Galerkin approximation in later chapters). Nonlinear elliptic problems are routinely reduced to it through linearization and the implicit function theorem.

Mathlib has Lax–Milgram for continuous coercive forms, compact operators, the Riesz representation theorem and the spectral theorem for compact self-adjoint operators. It does not have Sobolev spaces with zero boundary values as used here, elliptic bilinear forms, Fredholm operators or their index. As far as a search of the platform shows, none of these results has a machine-checked statement for elliptic operators with $L^\infty$ coefficients. The mission would give formal statements, and eventually proofs, of textbook results that are fully proved on paper.

Difficulty

The abstract functional analysis is close to the library. The difficulty lies in connecting it to the PDE objects. Gårding's inequality needs pointwise uniform ellipticity turned into an integral bound on the weak gradient, with the non-symmetric first-order term controlled explicitly enough to reach the stated $\gamma$. Compactness of the resolvent needs the Rellich–Kondrachov theorem: $H^1_0(\Omega)$ embeds compactly in $L^2(\Omega)$ for bounded $\Omega$, which is not in Mathlib in this form. The goal then relates the weak problem on $H^1_0(\Omega)$ to operator statements on $L^2(\Omega)$ in both directions, including the solution spaces and the adjoint's kernel. A proof that argues only on $L^2(\Omega)$, without tracking that the solutions lie in $H^1_0(\Omega)$ and satisfy the weak identity for every $H^1_0$ test function, does not reach the stated result.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. Coordinates are 0-based.
• $H^1_0(\Omega)$ (H10 n Ω) is modelled by jets. It is the closure, in $L^2(\Omega;\mathbb{R}\times\mathbb{R}^n)$, of the pairs $(\phi,\nabla\phi)$ for smooth compactly supported $\phi$ with support in $\Omega$. Its norm is exactly the standard $H^1$ norm, and it is a Hilbert space. $H^{-1}(\Omega)$ is StrongDual ℝ (H10 n Ω).
• Coefficients are bundled in Coeffs n. Admissible is $L^\infty(\Omega)$ membership plus a.e. symmetry. Uniform ellipticity carries $\theta > 0$.
• Weak solutions are tested against every $\phi \in H^1_0(\Omega)$, not only test functions. $f \in L^2(\Omega)$ is an element of Lp ℝ 2 on $\Omega$.
• The printed display (4.21) of the adjoint form has $+\sum b_i(\partial_i u)v$. That contradicts both $a^*(u,v) = a(v,u)$ and the stated $L^*$. The formalization uses $a^*(u,v) = a(v,u)$.
• Theorem 4.22's printed equation "$Lu + \mu f = 0$" is read as $Lu + \mu u = f$, as in Definition 4.19 and the proof.
• Theorem 4.25's printed $\lambda_1 < \lambda_2$ is stated as $\lambda_1 \le \lambda_2$, since the strict inequality fails for disconnected $\Omega$. $\Omega \neq \emptyset$ and $n \ge 1$ are assumed there.
• In Theorem 4.21 the explicit $\gamma$ is asserted for every a.e. lower bound $c_0$ of $c$, which is equivalent to the book's $c_0 = \inf c$.
• The Fredholm index is an integer computed from Module.finrank and is only used for Fredholm operators.
• Solution spaces are subspaces of $H^1_0(\Omega)$. Their finite-dimensionality is asserted separately from the equality of dimensions, so a finrank equality between two infinite-dimensional spaces (both $0$ in Lean) cannot stand in for the book's claim.
• A resolvent defined by an arbitrary choice with junk value $0$ is only used for $\mu \ge \gamma$, where the weak solution exists and is unique. The theorem asserts that this function is a continuous linear map, so it cannot be satisfied vacuously.

Needed infrastructure, reusable beyond this mission: the jet model of $H^1_0$ and its Poincaré inequality, Gårding-type estimates, a Rellich–Kondrachov compactness theorem for $H^1_0(\Omega) \hookrightarrow L^2(\Omega)$, and Fredholm operators with index on Hilbert spaces. Contributions of any of these as separate lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, Chapter 4. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, Chapter 6. https://doi.org/10.1090/gsm/019
• P. D. Lax and A. N. Milgram, "Parabolic equations", Contributions to the Theory of Partial Differential Equations, Annals of Mathematics Studies 33, 1954, 167–190. https://doi.org/10.1515/9781400882182-010
• L. Gårding, "Dirichlet's problem for linear elliptic partial differential equations", Mathematica Scandinavica 1 (1953), 55–72. https://doi.org/10.7146/math.scand.a-10364
• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer Classics in Mathematics, 2001, Chapter 8. https://doi.org/10.1007/978-3-642-61798-0

Motivation

Introductory physics is normally taught as a sequence of unrelated chapters — kinematics, dynamics, energy, optics, gravitation — each with its own rules. A recurring proposal in physics education is to teach instead from a single organising statement: among all conceivable histories of a system, the one realised in nature is the one that makes a certain integral, the action, stationary. Edwin Taylor's editorial A Call to Action (American Journal of Physics, 2003) argued for building the first-year curriculum on it; Lachlan McGinness and Craig Savage reported classroom results for such a course at the Australian National University (Action physics, American Journal of Physics, 2016); Massimiliano Malgieri tested a sum-over-paths treatment in an Italian secondary school (2017).

The source monograph for this mission, Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio (Trabalho de Conclusão de Curso, Universidade Federal do Ceará, 2025), develops this programme for secondary education. Its Chapters 2 and 3 are quantitative: they follow the historical line from antiquity to the nineteenth century and carry out every calculation in full. This mission formalises that quantitative core, and nothing of the pedagogical Chapter 4.

The historical line the monograph reconstructs, and which the milestone list follows:

• Heron of Alexandria (c. 60 AD), Catoptrics: the law of reflection derived from the shortest reflected path (§2.2).
• Galileo (1638), Two New Sciences: uniformly accelerated descent on an inclined plane, and the law of chords — descent from rest along any chord of a vertical circle takes the same time (§2.3).
• Fermat (1657–1662): the method of maxima and minima, and the law of refraction obtained by minimising travel time, with the velocities entering inversely to Descartes' version (§2.4, §2.4.1).
• Maupertuis (1744, 1746): the quantity of action $mvl$, the refraction law, and the equilibrium of a lever obtained by minimising action (§2.6).
• Euler (1744), Methodus inveniendi, including Additamentum II: the discretise–vary–pass-to-the-limit method, the resulting differential equation, and Keplerian orbits from Maupertuis' principle under conservation of total energy (§2.7).
• Lagrange (1760, 1788) and Hamilton (1834–1835): the general variational derivation and the principle of stationary action $\delta\int (T-U)\,dt = 0$ (Chapter 3, §3.1).

Setting

Fix real endpoints $x_1 < x_2$ and an integrand $f(y, y', x)$, a real-valued function of three real arguments. A path is a function $y : \mathbb{R} \to \mathbb{R}$, and its action over $[x_1,x_2]$ is

$$S[y] \;=\; \int_{x_1}^{x_2} f\bigl(y(x),\, y'(x),\, x\bigr)\, dx .$$

Neighbouring paths are produced by an admissible variation: a twice continuously differentiable $\eta$ with $\eta(x_1) = \eta(x_2) = 0$, giving the family $y(x,\alpha) = y(x) + \alpha\,\eta(x)$. The path $y$ is stationary when

$$\left.\frac{d}{d\alpha}\, S[\,y + \alpha\eta\,]\right|_{\alpha = 0} = 0 \qquad \text{for every admissible } \eta .$$

Writing $\partial f/\partial y$ and $\partial f/\partial y'$ for the partial derivatives of $f$ in its first and second slots, the Euler–Lagrange expression along $y$ is

$$E_f[y](x) \;=\; \frac{\partial f}{\partial y}\bigl(y(x), y'(x), x\bigr) \;-\; \frac{d}{dx}\left[\frac{\partial f}{\partial y'}\bigl(y(x), y'(x), x\bigr)\right].$$

In mechanics one takes $x = t$, $y = q$ and $f = L = T - U$, so that stationarity of $\int (T-U)\,dt$ is Hamilton's principle and $E_L[q] = 0$ is the Lagrange equation of motion.

Formalization targets

Goal — the Euler–Lagrange equation from stationary action

For $x_1 < x_2$, $f$ twice continuously differentiable in all three arguments and $y$ twice continuously differentiable, if $y$ is stationary for $S$ then

$$\frac{\partial f}{\partial y} - \frac{d}{dx}\,\frac{\partial f}{\partial y'} \;=\; 0 \qquad \text{at every } x \in [x_1, x_2].$$

This is equation (3.9) of the monograph, and — through the substitution $x \mapsto t$, $y \mapsto q_i$, $f \mapsto L$ — equation (3.17). It is stated as the weakest stable form: stationarity, not minimality, and an arbitrary admissible integrand rather than a particular Lagrangian.

Milestones

The supporting statements are the analytic ingredients of that derivation (the fundamental lemma, the first variation formula, the first integral for a cyclic coordinate), its two mechanical applications worked out in the monograph (harmonic oscillator, plane pendulum), its geometric application (shortest path), and the historical minimisation problems of Chapter 2 (Heron, Galileo, Fermat, Maupertuis).

Significance

The Euler–Lagrange equation is the bridge the whole unification argument rests on: once it is available, Newton's second law, the pendulum equation, Snell's law, geodesics and conservation laws all become consequences of one statement about an integral, which is exactly the claim the monograph makes to justify teaching physics this way. The Chapter 2 statements are the historically prior special cases, each obtained by a one-variable minimisation rather than by the general machinery, and together they exhibit how far elementary optimisation alone reaches before the calculus of variations is needed.

What this mission adds beyond the source is a machine-checked version of an argument that, in every textbook presentation including this one, is carried out at the level of rigour of formal manipulation: the interchange of differentiation and integration is performed without justification, the passage from a vanishing integral to a vanishing integrand is asserted, and the regularity needed for $\frac{d}{dx}\,\partial f/\partial y'$ to exist is left implicit. All of it is true under the stated hypotheses; none of it is proved in the source. Mathlib has the analytic infrastructure (interval integrals, differentiation under the integral sign, smooth bump functions) but, at the environment pinned for this mission, no Euler–Lagrange equation and no calculus-of-variations layer built on it. The definitions published here — action, admissible variation, stationary path, Euler–Lagrange expression — are reusable by any later variational mission.

Difficulty

The obvious argument is three lines: differentiate under the integral sign, integrate by parts, and conclude that the integrand vanishes because $\eta$ is arbitrary. Each line is where the work is.

Differentiating under the integral sign needs a dominating bound valid uniformly for $\alpha$ near $0$; it is available here because the data are $C^2$ and the interval is compact, but it has to be produced. The integration by parts needs $x \mapsto \partial f/\partial y'(y(x), y'(x), x)$ to be differentiable, which is where the second derivative of $y$ and the second derivatives of $f$ are consumed — a $C^1$ path is not enough for this formulation. The final step needs test functions: a $C^2$ bump supported in a small interval around a point where the continuous coefficient is nonzero, which is why the fundamental lemma is a separate milestone rather than a step.

A standing trap in the Lean formulation is that deriv returns $0$ at points where a function is not differentiable, so a statement about $\frac{d}{dx}\,\partial f/\partial y'$ can be accidentally true for the wrong reason unless the regularity hypotheses are genuinely strong enough. Every statement here carries the hypotheses that make each derivative a real derivative.

Formalization scope

The development is one-dimensional and real: paths are $\mathbb{R} \to \mathbb{R}$, the integrand is a curried $f : \mathbb{R} \to \mathbb{R} \to \mathbb{R} \to \mathbb{R}$ with argument order $(y, y', x)$ matching the source's $f(y(x), y'(x), x)$, and all integrals are interval integrals over $[x_1, x_2]$. Partial derivatives are one-dimensional derivatives in the frozen remaining arguments; smoothness of $f$ is stated for its uncurried form on $\mathbb{R} \times \mathbb{R} \times \mathbb{R}$. Regularity is $C^2$ throughout — for the integrand, for the path, and for the variations — matching the monograph's requirement that $\eta$ have continuous first and second derivatives.

Stationarity is a hypothesis quantified over all admissible variations, so the goal cannot be satisfied by exhibiting one convenient $\eta$; and the conclusion is an equation at every point of the closed interval, not almost everywhere, so it cannot be weakened to a null-set statement. The mechanical milestones are stated as equivalences between the Euler–Lagrange equation for the explicit Lagrangian and the classical equation of motion, which rules out a one-directional reading that would be vacuous for a path that never satisfies either.

Physical constants ($m$, $k$, $g$, $\ell$, the speeds $v_1, v_2$) are free real parameters, with positivity or non-vanishing assumed only where the source's conclusion requires it — the pendulum equivalence divides by $m\ell^2$, so $m \neq 0$ and $\ell \neq 0$ appear, while the oscillator equivalence needs no such assumption. Angles never appear as primitive objects in the optics milestones: the sines of the incidence and refraction angles are written as the ratios $x/\sqrt{a^2+x^2}$ that the figures define them by, so no convention about angle ranges is smuggled in.

Contributions welcome: proofs of any milestone, and reusable infrastructure for differentiation under the interval integral sign and for $C^k$ bump functions with prescribed support, both of which are of use well beyond this mission.

Selected references

• Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio, Trabalho de Conclusão de Curso (Licenciatura em Física), Universidade Federal do Ceará, Fortaleza, 2025, 60 pp. (the source of every statement in this mission; Chapters 2–3).
• Alberto Rojo and Anthony Bloch, The Principle of Least Action: History and Physics, Cambridge University Press, 2018 (the historical reconstruction the monograph follows for Chapter 2).
• Edwin F. Taylor, A call to action, American Journal of Physics 71 (2003), guest editorial.
• Lachlan P. McGinness and Craig M. Savage, Action physics, American Journal of Physics 84 (2016).
• Massimiliano Malgieri, Test on the effectiveness of the sum over paths approach in favoring the construction of an integrated knowledge of quantum physics in high school, 2017.
• Leonhard Euler, Methodus inveniendi lineas curvas maximi minimive proprietate gaudentes, Lausanne, 1744, in particular Additamentum II.

Motivation

A firm that sells a product line of different qualities cannot see how much each customer values quality. It can only post a price for every quality and let customers choose. Mussa and Rosen's 1978 paper solves the monopolist's problem in this setting and compares the result with the competitive outcome. Their model is, together with Mirrlees' optimal income tax and Maskin and Riley's later treatment of nonlinear pricing, one of the founding examples of screening: the seller designs a menu so that customers sort themselves. The model's main qualitative prediction, that a monopolist degrades the quality sold to every customer except the one who values quality most, is the origin of the phrase "no distortion at the top". Textbooks on contract theory and mechanism design still teach it in this form.

Timeline. Mussa and Rosen (1978) give the first-order analysis, including "bunching" of customers at a common quality when marginal revenue is not monotone. Maskin and Riley (1984) treat the same problem for nonlinear quantity pricing. Myerson (1981) introduced the "ironing" procedure for non-monotone virtual valuations in auction design, which later became the standard way of describing the bunching conditions of this paper.

Setting

Consumer types are numbers $\theta\in[\underline\theta,\bar\theta]$ with $0\le\underline\theta<\bar\theta$, distributed with a density $f$ that is positive and differentiable on the whole interval; $F(\theta)=\int_{\underline\theta}^{\theta}f(s)\,ds$. A consumer of type $\theta$ buys at most one unit, and from quality $q$ at price $p$ gets utility $\theta q-p$. Producing one unit of quality $q\ge0$ costs $C(q)$, where $C(0)=0$, $C$ is twice differentiable, and $C'(q)>0$, $C''(q)>0$ for $q\ge0$.

Under competition, price equals unit cost and type $\theta$ buys the quality $J(\theta)$ with $C'(J(\theta))=\theta$, or nothing when $\theta\le C'(0)$.

The monopolist chooses an assignment $q(\theta)$, the quality bought by type $\theta$. It must be nondecreasing, nonnegative and piecewise differentiable on $[\underline\theta,\bar\theta]$; such assignments are called admissible. Incentive compatibility and participation fix the consumer surplus at $z(\theta)=\int_{\underline\theta}^{\theta}q(s)\,ds$, so the monopolist maximizes

$$\Pi(q)=\int_{\underline\theta}^{\bar\theta}\bigl[\theta\,q(\theta)-z(\theta)-C(q(\theta))\bigr]f(\theta)\,d\theta .$$

An assignment is optimal if it is admissible and maximizes $\Pi$ among admissible assignments. The marginal revenue of quality sold to type $\theta$ is

$$MR(\theta)=\theta-\frac{1-F(\theta)}{f(\theta)} .$$

The paper's analysis runs through the marginal profit of a uniform quality increase for all types $\theta\ge t$,

$$\mu(t)=\int_t^{\bar\theta}\Bigl[\theta-\int_t^\theta ds-C'(q(\theta))\Bigr]f(\theta)\,d\theta .$$

Formalization targets

Goal: quality distortion below the top

For every optimal assignment $q$:

$$C'(q(\theta))<\theta\quad\text{for }\underline\theta\le\theta<\bar\theta,\ \theta>C'(0);\qquad q(\theta)=0\quad\text{for }\underline\theta\le\theta<\bar\theta,\ \theta\le C'(0);$$

and, if $C'(0)<\bar\theta$, the limit $L=\lim_{\theta\uparrow\bar\theta}q(\theta)$ exists and satisfies $C'(L)=\bar\theta$ (if $\bar\theta\le C'(0)$, then $q(\theta)\to0$). In words: $q^m(\theta)<J(\theta)$ for every type below the top that buys under competition, types that do not buy under competition do not buy from the monopolist, and $q^m(\bar\theta)=J(\bar\theta)$.

Milestones

The paper's own chain of claims, in order: $MR(\theta)<\theta$ except at $\bar\theta$ (p. 308); the first-order condition (9), $\Lambda(h;q)\le0$ for every admissible deformation; the identity (10) = (12), $\mu(t)=\int_t^{\bar\theta}[MR-C'(q)]f$; condition (13), $\mu\le0$; condition (15), $\mu=0$ where $\dot q>0$; $\mu=0$ at a jump; the absence of jumps; (17), $C'(q)=MR$ where $\dot q>0$; the bunching conditions (18)–(19); and the absence of a bunch at the top. Companion items state the two-type case of footnote 4, the uniform–quadratic example of §5, and the loss of consumer surplus (§6, "Second").

Significance

The result. The goal says how the monopolist differs from competition: it lowers every quality except the top one, and it never serves a type that competition leaves out. The distortion comes from the gap $\theta-MR(\theta)=(1-F(\theta))/f(\theta)>0$, which closes only at $\bar\theta$. The same comparison underlies results on second-degree price discrimination, regulation of product lines, and versioning of information goods. The bunching conditions (18)–(19) are an early statement of what is now called ironing.

Formalizing it. The result has been proved since 1978 in the economic literature, under the paper's smoothness assumptions and by a variational argument. As far as is known, it has not been machine-checked: no formal library contains the monopoly quality problem, its first-order conditions or the bunching conditions. The mission produces a checked version with the hypotheses made explicit, including the conventions at the endpoints that the paper leaves implicit. The uniform–quadratic example gives a concrete optimum that certifies the hypotheses are satisfiable.

Difficulty

The obvious argument sets $C'(q(\theta))=MR(\theta)$ pointwise and compares with $C'(J(\theta))=\theta$. This fails when $MR$ is not increasing: the pointwise solution is then decreasing somewhere and not admissible. The optimal assignment is constant on some intervals, and on such a bunch $C'(q)\ne MR$ pointwise. The comparison with $J$ there needs the boundary conditions (18)–(19) and the fact that no bunch reaches $\bar\theta$. All of these come from one-sided deformations that respect monotonicity, so the first-order conditions are inequalities and need a separate argument for equality. The paper also asserts without a separate step that optimal assignments have no jumps, and later steps use continuity.

Formalization scope

Types and assignments are real functions on $\mathbb R$; only their values on $[\underline\theta,\bar\theta]$ matter. The type distribution and $MR$ are the published MechanismDesign.Screening.TypeDistribution and virtualValuation. The standing assumptions are hypotheses of every main statement: $f$ is differentiable on $[\underline\theta,\bar\theta]$ (positivity and total mass 1 are part of the distribution), $C(0)=0$, $C$ and $C'$ are differentiable on $\mathbb R$, and $C'>0$, $C''>0$ on $[0,\infty)$. $C(0)=0$ is an added normalization: quality 0 means not buying. "Piecewise differentiable" means differentiable on $(\underline\theta,\bar\theta)$ outside a finite set. The competitive assignment $J=C'^{-1}$ is never formed; every comparison with $J$ is written through $C'$. Admissible deformations $h$ in (9) are required to keep $q+h\ge0$.

The value $q(\bar\theta)$ does not affect $\Pi$, so a statement about $q(\bar\theta)$ itself would be false; the top-type claim is stated as a left limit. Optimality ranges over admissible assignments only. Any reading under which no optimal assignment exists makes the goal vacuous; the §5 companion rules this out, since its optimal assignment has a kink and uses the same notion of optimality.

Needed infrastructure: interval integrals of monotone functions, first variations under monotonicity constraints, and fundamental-theorem-of-calculus arguments for $F$. The incentive-compatibility reduction (monotonicity and the envelope formula) is not posed here, because it is posed on the platform in Börgers' screening chapter. Related platform item: Börgers' Proposition 2.6 (MechanismDesign.Screening.nonlinear_pricing_optimal) treats a linear-cost, concave-valuation model under regularity, which is a different statement. Contributions to any milestone, and reusable lemmas about monotone deformations, are welcome.

Selected references

• M. Mussa and S. Rosen, Monopoly and product quality, Journal of Economic Theory 18 (1978), 301–317. https://doi.org/10.1016/0022-0531(78)90085-6
• E. Maskin and J. Riley, Monopoly with incomplete information, RAND Journal of Economics 15 (1984), 171–196. https://doi.org/10.2307/2555674
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6 (1981), 58–73. https://doi.org/10.1287/moor.6.1.58
• J. A. Mirrlees, An exploration in the theory of optimum income taxation, Review of Economic Studies 38 (1971), 175–208. https://doi.org/10.2307/2296779
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 2. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

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 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