Calculus of Variations

Motivation

Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an order, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of Breiner--Dees.

The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.

Setting

A Euclidean Coxeter complex consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group $W$. A Euclidean building of type $W$ is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.

The domain is a connected open subset $D$ of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map $u:D\to X$ is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For $x_0\in D$ and small radii $r$, the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order $\operatorname{Ord}_u(x_0)$.

Formalization targets

Main classification

For a nonconstant energy-minimizing harmonic map $u:D\to X$ and any $x_0\in D$, prove that the order is defined and that there are positive integers $m,k$ such that

$$\operatorname{Ord}_u(x_0)=\frac{m}{k}, \qquad k\mid |W|.$$

If the building has rank one, prove the sharper form

$$\operatorname{Ord}_u(x_0)=\frac{m}{2} \qquad\text{for some integer }m\ge 2.$$

The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.

Significance

The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an $\mathbb R$-tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.

Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single sorry in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.

Difficulty

The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.

The rank-one clause is not obtained by substituting $|W|=2$ into the general statement alone: it also asserts $m\ge2$. The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.

Formalization scope

The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group $W$ is the image of the affine group under taking linear parts, so $|W|$ is not an arbitrary external number. The domain carries a point $x_0$ and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.

Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.

Selected references

• Christine Breiner and Ben K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, Calculus of Variations and Partial Differential Equations, 2026, Theorem 1.1 and Sections 2--4. DOI
• Mikhail Gromov and Richard Schoen, Harmonic Maps into Singular Spaces and p-adic Superrigidity for Lattices in Groups of Rank One, Publications Mathématiques de l'IHÉS 76 (1992), 165--246. EuDML

Motivation

Chapter IX of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) recasts problems of the calculus of variations with constraints as dynamic programming processes. A variational problem with an inequality constraint on the control, such as $0 \le y \le x$, is awkward for the classical Euler–Lagrange theory: the optimal control switches between the constraint boundary and the interior, and the number and location of the switches are unknown in advance. Bellman's proposal is to replace the continuous problem by a discrete-time one and to solve that by the recurrence relations of dynamic programming, a procedure he describes as the more reliable computational one "in cases treated to date" (§ 11, p. 260).

That proposal is sound only if the discrete values converge to the continuous value as the time step goes to zero. Chapter IX states one such convergence result, Theorem 2 of § 12, and proves it through an Euler-scheme error estimate. The same chapter works through an example (§§ 10–11) whose discrete version is described by Theorem 1. Both are the subject of this mission. The convergence of time-discretized dynamic programming to the continuous value function has since become a standard topic of numerical optimal control (for example the semi-Lagrangian schemes analysed by Capuzzo-Dolcetta and Falcone), and Bellman's § 12 is an early rigorous instance of it.

Setting

A state $x(t) \ge 0$ evolves on a horizon $[0, T]$ under a control $y(t)$ with $0 \le y \le x$, a running reward $F(x, y)$ and dynamics

$$\frac{dx}{dt} = G(x, y), \qquad x(0) = c .$$

Writing $y = \varphi x$ with a fractional control $0 \le \varphi \le 1$ turns $F$ and $G$ into $\tilde F(x, \varphi) = F(x, \varphi x)$ and $\tilde G(x, \varphi) = G(x, \varphi x)$ (phiForm). The continuous value is

$$f(c, T) = \sup_{\varphi} \int_0^T \tilde F(x(t), \varphi(t))\, dt,$$

over measurable $\varphi$ with values in $[0, 1]$, where $x$ solves $x(t) = c + \int_0^t \tilde G(x(s), \varphi(s))\,ds$ on $[0, T]$ (IsTrajectory, contValue).

For $n = 1, 2, \dots$ the discrete problem uses step $1/n$ and $N = \lfloor Tn \rfloor$ steps (horizonSteps): for $\varphi_0, \dots, \varphi_N \in [0, 1]$,

$$x_0 = c, \quad x_{k+1} = x_k + \frac{\tilde G(x_k, \varphi_k)}{n}, \qquad J_N(\{\varphi_k\}, n) = \sum_{k=0}^{N} \frac{\tilde F(x_k, \varphi_k)}{n},$$

and $f(c, T, n) = \max J_N$ (eulerTraj, discretePayoff, discreteValue). A discrete control defines the step control $\varphi(t) = \varphi_k$ on $k/n \le t < (k+1)/n$ (stepControl).

The example of §§ 10–11 has a gain function $b$ with $b(0) = 0$, $b'(0) = \infty$, $b' > 0$, $b'(y) \to 0$ as $y \to \infty$, $b'' < 0$ (IsGainFunction; $b(y) = y^{1/2}$ is one), and value functions (uSeq)

$$u_0(c) = c, \qquad u_{N+1}(c) = \max_{0 \le v \le c}\,\bigl[c - v + u_N(c + b(v))\bigr].$$

Formalization targets

Goal: Chapter IX, Theorem 2 (corrected)

Assume (11): (a) $F$ and $G$ have continuous second partial derivatives; (b) $px \le G(x, y) \le qx + r$ for $x > 0$, $0 \le y \le x$; (c) $G_y > 0$ throughout that region, or $G_y < 0$ throughout. Then for all $c \ge 0$, $T > 0$, the set of continuous payoffs is nonempty and bounded above, and

$$\lim_{n \to \infty} f(c, T, n) = f(c, T).$$

Milestones

1. Chapter IX, Theorem 1: the structure of $u_N$. There are $v_N(c)$ and thresholds $c_N$ with $v_N$ decreasing in $c$, $v_{N+1} > v_N$, $c_N$ the unique fixed point of $v_N$ with $c_{N+1} > c_N$, $u_N(c) = u_{N-1}(c + b(c))$ for $c \le c_N$, $u_N(c) = c - v_N(c) + u_{N-1}(c + b(v_N(c)))$ for $c \ge c_N$, and $u_N' \ge u_{N-1}'$.
2. § 12, Lemma (corrected): for $G$ Lipschitz on $[m, M] \times [0, 1]$, the Euler states with a step control are within $\kappa / n$ of the exact solution on $[0, T]$.
3. Eq. (12.13): $|J(\varphi) - J_N(\{\varphi_k\}, n)| \le B'/n$ for step controls.
4. Eq. (12.14): $f(c, T, n) \le f(c, T) + B'/n$ for all $n \ge 1$.
5. Eq. (12.17): $f(c, T) \le \liminf_{n \to \infty} f(c, T, n)$.

Milestones 3–5 are stated for $c > 0$, as in the book's proof ("Given $c > 0$ and $T > 0$"); the goal is stated for $c \ge 0$, as in the theorem.

Significance

Theorem 2 says that the value of a constrained continuous-time control problem can be computed, to any accuracy, by the finite recurrence of dynamic programming on a time grid. Its upper half (12.14) gives a rate: the discrete value never exceeds the continuous one by more than $B'/n$. The lower half (12.17) needs no rate and holds because measurable controls are approximated by step controls. Theorem 1 is a discrete counterpart of the transition curve computed in § 10: below the threshold $c_N$ the whole state is invested, above it an interior amount, and the thresholds increase with the number of remaining stages.

As far as the mission's author could establish, none of these results has a machine-checked proof. The Euler error estimate is classical and has a Gronwall-type proof; Mathlib contains Gronwall's inequality (Analysis/ODE/Gronwall) and Picard–Lindelöf for continuous right-hand sides, but no convergence theory for the value of discretized control problems. The book leaves the proof of Theorem 1 to the reader.

Difficulty

The upper bound (12.14) follows from the Lemma once the continuous and the discrete trajectories are known to stay in a common bounded strip $m \le x \le M$; that uniform bound is what assumption (11b) provides and must be established first. The lower bound is where the obvious argument fails: an arbitrary measurable control is not a step control on the grid $k/n$, and passing to a step control changes the trajectory, so the payoff must be shown continuous under almost-everywhere convergence of controls. This uses the trajectory's dependence on the control in $L^1$, not only on the initial value. Solutions exist in the Carathéodory sense only, so the integral form of the equation is required. For Theorem 1 the induction must carry concavity of $u_N$ and a strict comparison of marginal values across $N$, and $u_N$ is not differentiable at $c = 0$, where $b'(0) = \infty$.

Formalization scope

States, controls and rewards are real; $F, G, b : \mathbb R \to \mathbb R$ (or $\mathbb R \to \mathbb R \to \mathbb R$), with the hypotheses imposed where the book imposes them. The conventions:

• Misprint in (12.5). The print sets $N = [T/n]$ while using the step $1/n$ in (12.6) and the intervals $k/n \le t < (k+1)/n$ in the Lemma. Under the literal reading the discrete horizon $N/n$ tends to $0$ and Theorem 2 is false: for $F \equiv 1$, $G(x, y) = y$ (which satisfies (11) with $p = 0$, $q = 1$, $r = 0$, $G_y = 1$) and $T = 1$, $f(c, 1) = 1$ but $f(c, 1, n) = 1/n$ for $n \ge 2$. The mission uses $N = \lfloor Tn \rfloor$ and keeps the book's sum $\sum_{k=0}^{N}$; the range "$k = 0, \dots, n - 1$" in (12.6) is read as $k = 0, \dots, N - 1$.
• Lemma. Its range "$0 \le t \le N$" is read as $0 \le t \le T$. The bounds $m \le x \le M$ are required of the solution $x(t)$ as well as of the sequence $x_k$, since a Lipschitz condition on the strip says nothing about $G$ outside it; the proof of Theorem 2 supplies both bounds. The constant may depend on $m$, $M$ and the Lipschitz constant.
• Assumptions (11) are on the original $F(x, y)$, $G(x, y)$, with (11a) read as $C^2$ on $\mathbb R^2$; the problem is posed through $y = \varphi x$.
• "Max" over measurable controls is a supremum (the proof picks $\varepsilon$-optimal controls). The goal asserts that the set of payoffs is nonempty and bounded above, so the Lean supremum cannot take its default value $0$. Trajectories satisfy the integral equation with integrable right-hand side, and the reward is required integrable, so the Bochner integral's default $0$ cannot enter either.
• Theorem 1. (5a) is read as non-strict monotonicity: for $N = 1$ the interior optimum solves $b'(v) = 1$ and is constant in $c$. $v_N(c) \ge 0$ is required for $c \ge c_N$, so that $v_N(c)$ is a feasible choice. (5f) presupposes differentiability and is stated where both derivatives exist.

A trivializing formalization is ruled out: the discrete and continuous values are defined from $F$ and $G$ by the book's recursions and integrals, not assumed as hypotheses, and the corrected step count is not a free parameter.

Needed infrastructure: Carathéodory existence and uniqueness for Lipschitz right-hand sides with measurable controls, Gronwall estimates for the Euler scheme, and approximation of measurable controls by step functions. All three are reusable beyond this mission, and contributions of any of them are welcome.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter IX, §§ 10–12, pp. 256–263. DOI 10.2307/j.ctv1nxcw0f
• I. Capuzzo-Dolcetta, On a discrete approximation of the Hamilton–Jacobi equation of dynamic programming, Applied Mathematics and Optimization 10 (1983) 367–377. DOI 10.1007/BF01448394
• M. Bardi and I. Capuzzo-Dolcetta, Optimal Control and Viscosity Solutions of Hamilton–Jacobi–Bellman Equations, Birkhäuser, 1997. DOI 10.1007/978-0-8176-4755-1

Motivation

Hemivariational inequalities were introduced by Panagiotopoulos in the 1980s to model mechanical problems whose energy functional is neither convex nor smooth: nonmonotone friction, adhesion, delamination and unilateral contact with nonmonotone multivalued laws. Where a variational inequality expresses the optimality condition of a convex energy, a hemivariational inequality expresses a stationarity condition of a locally Lipschitz energy through Clarke's generalized directional derivative. When in addition the admissible set depends on the unknown state, as in contact problems with a solution-dependent gap or in Nash-type equilibrium problems with coupled constraints, the problem becomes a quasi-hemivariational inequality.

Zeng, Migórski and Khan (SIAM J. Control Optim. 59 (2021)) treat a general form of this problem that contains a multivalued operator $T$, a bifunction $\varphi$ and a constraint map $K$ at once. Their existence theorem for it, Theorem 3.8, is the base of an optimal control result (Section 4) and of an application to a frictional contact problem in elasticity (Section 5). This mission formalizes the existence part, Sections 2 and 3 of the paper.

Setting

Let $V$ be a real reflexive Banach space with dual $V^*$ and pairing $\langle\cdot,\cdot\rangle$, and let $X$, $Y$ be real Banach spaces. The data are: a nonempty closed convex set $C\subseteq V$; a multivalued constraint map $K:C\to2^C$; a multivalued operator $T:C\to2^{V^*}$; a function $\varphi:V\times V\to\mathbb R$; a locally Lipschitz functional $J:X\to\mathbb R$; bounded linear operators $\gamma:V\to X$ and $\pi:V\to Y$; a functional $f\in Y^*$; and an auxiliary function $h:V\to\mathbb R$.

For a locally Lipschitz $J$, the Clarke generalized directional derivative and the generalized gradient are

$$J^0(u;v)=\limsup_{\lambda\to0^+,\ w\to u}\frac{J(w+\lambda v)-J(w)}{\lambda},\qquad \partial J(u)=\{\xi\in X^*:\ J^0(u;v)\ge\langle\xi,v\rangle\ \forall v\in X\}.$$

Problem 1.1 asks for $u\in C$ and $u^*\in T(u)$ such that $u\in K(u)$ and

$$\langle u^*,v-u\rangle+\varphi(v,u)+J^0(\gamma u;\gamma(v-u))\ge\langle f,\pi(v-u)\rangle_{Y^*\times Y}\quad\text{for all }v\in K(u).$$

Its solution set is $\Gamma(f)$. Fixing the constraint set gives Problem 3.3: find $u\in C$ and $u^*\in T(u)$ with the same inequality for all $v\in C$; its solution set is $\mathrm{SOL}(C;T,J,\varphi,f)$. The variational selection $S:C\to2^C$ maps $w\in C$ to the solution set of Problem 3.3 with $C$ replaced by $K(w)$; its fixed points are exactly the solutions of Problem 1.1.

The hypotheses of the paper (p. 1250) are: $T$ has nonempty, compact, convex values and is upper semicontinuous; $T(\cdot)+\gamma^*\partial J(\gamma\,\cdot)$ is $(\varphi,h)$-stably pseudomonotone with respect to $\pi^*f$, where $\limsup_{t\to0^+}h(tu)/t\ge0$ and $h$ is weakly sequentially upper semicontinuous in the limsup sense (3.1); $\varphi$ is convex and l.s.c. in its first argument, concave and u.s.c. in its second, and vanishes on the diagonal; $K$ has nonempty closed convex values and satisfies two Mosco-type conditions (HK); a bounded set $C_0$ meets every $K(u)$ and, if $C$ is unbounded, a coercivity condition (3.2) holds at each point of $C_0$. Theorem 3.8 adds that $\gamma$ is compact, $h$ is convex, and $\limsup_n\varphi(v_n,u_n)\le\varphi(v,u)$ whenever $v_n\to v$ strongly and $u_n\rightharpoonup u$ weakly (3.19).

Formalization targets

Goal: Theorem 3.8 (ii)

Under all hypotheses of Theorem 3.8,

$$\Gamma(f)\neq\emptyset,\qquad \Gamma(f)\ \text{is bounded},\qquad \Gamma(f)\ \text{is weakly closed in }V.$$

Milestones

1. Proposition 2.5 (i)–(iii): $J^0(x;\cdot)$ is sublinear, $J^0(x;v)=\max\{\langle\xi,v\rangle:\xi\in\partial J(x)\}$, and $(u,v)\mapsto J^0(u;v)$ is upper semicontinuous.
2. Theorem 2.7 (Kluge): a multivalued self-map of a nonempty closed convex subset of a reflexive Banach space, with nonempty closed convex values and a sequentially weakly closed graph, has a fixed point if its domain or its range is bounded.
3. Theorem 3.4 (i)–(iii): for Problem 3.3, the Minty-type characterization

$$\langle v^*,v-u\rangle+\varphi(v,u)+\langle\eta_v,\gamma(v-u)\rangle\ge\langle f,\pi(v-u)\rangle+h(v-u)\quad\forall v\in C,\ v^*\in T(v),\ \eta_v\in\partial J(\gamma v);$$

nonemptiness, boundedness and weak closedness of $\mathrm{SOL}(C;T,J,\varphi,f)$; and its convexity when $h$ is convex. 4. Theorem 3.8 (i): the same characterization for Problem 1.1, with $C$ replaced by $K(u)$. 5. Two claims from the proof of Theorem 3.8 (ii): the graph of $S$ is sequentially weakly closed, and $S(C)=\bigcup_{w\in C}S(w)$ is bounded.

Significance

Theorem 3.8 is the existence result on which the rest of the paper rests: the optimal control problem of Section 4 minimizes $F(f)=\inf_{u\in\Gamma(f)}g(u,f)$ over $f\in Y^*$, and Section 5 casts an approximate static elastic contact model, with a multivalued normal compliance condition and a frictional law with slip-dependent friction coefficient, in the form of Problem 1.1 on a space of displacements. The theorem unifies several existence results for variational, hemivariational and quasi-variational inequalities: for single-valued $T$, $J=0$, $\pi=\mathrm{id}$, $h=0$ and $\varphi(v,u)=\phi(v)-\phi(u)$, its Corollary 3.9 reduces to an earlier existence result for quasi-variational inequalities (Remark 3.10), and Theorem 3.4 removes the compactness of $\gamma$ required in earlier work (Remark 3.6).

The results are proved in the paper. None of them, nor Clarke's calculus on a Banach space, nor Kluge's fixed point theorem, has a machine-checked proof to our knowledge. A formalization adds a checked version of a proof that combines a KKM-type fixed point theorem, Minty's trick for pseudomonotone multivalued operators, and a fixed point argument for the variational selection.

Difficulty

The obvious route to Problem 1.1 is to fix $w$, solve the inequality on $K(w)$, and take a fixed point of the solution map. Two steps resist. First, the solution map is multivalued and its values are only weakly closed, so a Schauder- or Kakutani-type theorem in the norm topology does not apply; the fixed point theorem must work with sequentially weakly closed graphs, and the graph closedness of $S$ has to be proved by passing to the limit in inequalities in which $u_n$ converges only weakly while the test points $v_n\in K(w_n)$ must converge strongly. That passage uses the compactness of $\gamma$, the upper semicontinuity of $J^0$, condition (3.19) and the Mosco-type conditions together. Second, in the "there exists $u^*\in T(u)$" form of the problem the inequality is not stable under weak limits in $u$, which is why the Minty reformulation and the stable pseudomonotonicity with the auxiliary function $h$ are needed.

Formalization scope

All spaces are real normed spaces with CompleteSpace; $V^*$ is V →L[ℝ] ℝ with the operator-norm topology; reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ V. No inner product and no finite dimension is assumed. Multivalued maps are total functions V → Set _, constrained on $C$ only. Weak convergence $x_n\rightharpoonup x$ means $\ell(x_n)\to\ell(x)$ for every $\ell\in V^*$; "weakly closed" is sequential weak closedness, which for the bounded sets $\Gamma(f)$ and $\mathrm{SOL}$ in a reflexive space agrees with weak closedness. Adjoints are composition: $\langle\gamma^*\eta,w\rangle=\eta(\gamma w)$, $\langle\pi^*f,w\rangle=f(\pi w)$. $J^0$ is a real Filter.limsup and is used only under LocallyLipschitz J. Every $\limsup$, infimum and limit in the hypotheses ($\limsup_{t\to0^+}h(tu)/t\ge0$, (3.1), (3.2), (3.19)) is written with explicit $\varepsilon$–$N$ quantifiers, so no default value of a real $\limsup$ or $\inf$ can make a hypothesis vacuous.

Four corrections to the printed hypotheses are built in and stated in each item's note: the pairing in (3.2) is $\langle\eta_u,\gamma(u-v_0)\rangle$ (the page's $\langle\eta_u,u-v_0\rangle$ does not typecheck); $T(u)$ is nonempty for $u\in C$; the condition (3.2) assumed in Theorem 3.4 refers to a bounded set $C_0$ that meets $C$; and for Theorem 3.8 (ii) and the boundedness of $S(C)$, (3.2) in (HC0) holds uniformly in $v_0\in C_0$ (one $R$ for each $M$), which is what the proof on pp. 1260–1261 uses. With (3.2) only at each fixed $v_0\in C_0$, as printed, $\Gamma(f)$ can be unbounded; the counterexample is in the note of Theorem 3.8 (ii). Theorem 3.8 (i) and the graph-closedness of $S$ keep (HC0) as printed. A formalization in which $T$ may have empty values, $C_0$ may be empty or disjoint from $C$, $V$ is a Hilbert or finite-dimensional space, a real $\limsup$ default value makes the conditions on $h$ or (3.19) vacuous, or "bounded" or "weakly closed" is dropped from the conclusion, would be a different and weaker theorem.

The development needs Clarke's calculus on a Banach space (Proposition 2.5, which relies on the Hahn–Banach theorem), Eberlein–Šmulian or Kakutani's theorem on weak compactness of bounded closed convex sets in reflexive spaces, Mazur's lemma, a KKM-type fixed point theorem in Hausdorff topological vector spaces, and Kluge's fixed point theorem. These pieces are reusable beyond this mission: Clarke's calculus for every nonsmooth optimization statement on Banach spaces, and the fixed point theorems for variational and quasi-variational inequalities in general. Contributions of any of them, of alternative proofs, and of proofs of the milestones in any order are welcome.

Selected references

• S. Zeng, S. Migórski, A. A. Khan, Nonlinear quasi-hemivariational inequalities: existence and optimal control, SIAM J. Control Optim. 59(2) (2021) 1246–1274. https://doi.org/10.1137/19M1282210
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; reprinted SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309
• R. Kluge, Nichtlineare Variationsungleichungen und Extremalaufgaben, VEB Deutscher Verlag der Wissenschaften, Berlin, 1979.
• S. Migórski, A. Ochal, M. Sofonea, Nonlinear Inclusions and Hemivariational Inequalities, Springer, 2013. https://doi.org/10.1007/978-1-4614-4232-5
• P. D. Panagiotopoulos, Hemivariational Inequalities: Applications in Mechanics and Engineering, Springer, 1993. https://doi.org/10.1007/978-3-642-51677-1

Motivation

Homogeneous minimizers model possible free-boundary singularities. A nonflat example in seven dimensions supplies one side of the claimed critical-dimension threshold. The pinned manuscript supplies the research context.

Setting

The one-phase Bernoulli energy on a ball is the integral of squared weak gradient plus the indicator of positivity. Competitors are nonnegative Sobolev functions with the prescribed H1-zero-boundary difference.

Formalization target

The selected goal is OAI.Bernoulli.nonflat_in_seven. Its central assertion is

$$\exists u:\mathbb R^7\to\mathbb R,\quad u(rx)=ru(x)\ (r>0,\ \text{a.e. }x),\quad u\text{ minimizes }E,\quad u\text{ is not flat}.$$

The theorem states that there exists a function u: ℝ⁷ → ℝ that is nonnegative almost everywhere, belongs locally to H¹, and is a global minimizer of the one-phase Bernoulli energy E_B(u) = ∫B (|∇u|² + 1{u>0}) dx. Here ∇u is a distributional gradient, and global minimality means that, for every open ball B of positive radius and every nonnegative almost-everywhere Sobolev competitor v ∈ H¹(B) with v − u ∈ H¹₀(B), one has E_B(u) ≤ E_B(v). Membership in H¹₀(B) requires approximation by smooth functions compactly supported in B, with both the functions and their gradients converging in L². The function is nonzero in the sense that it is not equal to zero almost everywhere, and it is homogeneous of degree one: for each real r > 0, u(rx) = r u(x) for almost every x. Nevertheless, it is not flat: there is no unit vector e ∈ ℝ⁷ for which u(x) = max(⟨x,e⟩, 0) almost everywhere. All almost-everywhere statements and integrals use Lebesgue measure.

Significance and status

The selected goal is existence of a nonzero nonflat one-homogeneous global minimizer in dimension seven. Flatness in dimensions at most six and singular-set dimension bounds are not attached conclusions. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

A stationary cone is insufficient: the example must minimize against all admissible ball competitors and fail every half-space profile.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, The critical dimension for one-phase Bernoulli minimizers, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Sharp filling inequalities compare the mass of a cycle with the least mass needed to fill it. The selected formulation extends a Euclidean coefficient to proper CAT(0) metric spaces. The pinned manuscript supplies the research context.

Setting

Integral currents are encoded metric currents with integer-multiplicity chart decompositions and integral boundary. The input is a compactly supported n-cycle for n at least two. In the displayed coefficient, σ_n=(n+1)ω_{n+1}, where ω_{n+1} is the Euclidean volume of the unit ball in dimension n+1; this is the published sphereArea convention.

Formalization target

The selected goal is OAI.CAT0Fillings.sharp_integral_filling. Its central assertion is

$$\partial S=T,\qquad\mathbf M(S)\leq\frac{\mathbf M(T)^{(n+1)/n}}{(n+1)\sigma_n^{1/n}}.$$

The theorem states that, for a proper metric space X with its Borel σ-algebra that is CAT(0), meaning there is a choice of geodesic parametrization segment(x,y,t) from x to y (with segment(x,y,0)=x, segment(x,y,1)=y, and dist(segment(x,y,s),segment(x,y,t))=|s−t|·dist(x,y) for s,t in [0,1]) satisfying the comparison inequality dist(segment(o,x,s),segment(o,y,t))² ≤ (s·d(o,x) − t·d(o,y))² + s·t·(d(x,y)² − (d(o,x) − d(o,y))²), the following filling property holds for every integer n ≥ 2. Let T be an integral n-current on X, that is, a metric current (a multilinear functional on a bounded Lipschitz function and n Lipschitz functions, with locality, continuity and finite mass) that is a countable sum of disjointly supported integer-multiplicity bi-Lipschitz chart pieces and whose boundary has the same properties, and suppose T is compactly supported and a cycle, meaning its boundary is zero. Then there exists a compactly supported integral (n+1)-current S on X whose boundary is T and whose mass satisfies mass(S) ≤ c_n · mass(T)^((n+1)/n), where c_n = 1/((n+1)·(σ_n)^(1/n)), σ_n = (n+1)·ω_{n+1} is the area of the unit n-sphere and ω_{n+1} is the volume of the unit ball in Euclidean (n+1)-space. This is an admitted theorem statement, not a verified proof.

Significance and status

The goal is the CAT(0) integral-current filling inequality. Euclidean coefficient optimality is an additional reference. The manifold perimeter comparison and equality-rigidity statements in the manuscript are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The sharp coefficient must hold without a smooth manifold model, while preserving integrality, compact support and the exact boundary.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.SharpIntegralFillings.coefficient_optimal (Open).

Selected references

• OpenAI, Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

The isoperimetric problem asks, for each prescribed volume, for the regions of least boundary area. In Euclidean space the answer is the round ball. In a compact space with topology the answer changes with the volume: small regions still look like balls, but larger regions can save area by wrapping around the space. The unit cubic flat three-torus $\mathbb R^3/\mathbb Z^3$ is the simplest compact example in three dimensions, and the periodic isoperimetric problem on it is equivalent, by reflection, to the relative isoperimetric problem in a cube. It is a standard test case for how local Euclidean geometry interacts with global topology, and it has been studied in connection with periodic minimal and constant-mean-curvature surfaces (Hauswirth–Pérez–Romon–Ros 2004; Ros 2005).

The conjectured answer is a sequence of three phases: balls, solid circular tubes around shortest closed geodesics, and slabs between parallel coordinate tori, followed by their complements. This mission asks for a machine-checked proof of that conjecture, including the classification of every minimizer, as claimed in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

• 1972 — Hadwiger proves that a coordinate cut minimizes at half volume for the cube (Monatsh. Math. 1972).
• 1992–1996 — Ritoré and Ros develop stability and structure results for constant-mean-curvature surfaces in flat three-manifolds (Comment. Math. Helv. 1992; Trans. AMS 1996); Ritoré's thesis records Hsiang's coordinate reflection symmetry (1994).
• 2000 — Barthe and Maurey recover Hadwiger's half-volume result by Gaussian comparison (Ann. IHP 2000). Morgan and Johnson's small-volume comparison implies that balls minimize for sufficiently small volume on compact flat manifolds (Indiana Univ. Math. J. 2000, Theorem 4.4).
• 2004 — Hauswirth, Pérez, Romon and Ros state the ball–tube–slab prediction and prove that a nonstandard minimizing boundary is connected of genus $2$, $3$ or $4$, with curvature–area bounds (Trans. AMS 2004).
• 2005 — Ros's survey records the conjecture for the cubic torus and cube (Clay Math. Proc. 2, 2005, Section 1.6).
• 2013 — Acerbi, Fusco and Morini prove that slabs are the only minimizers near half volume (Comm. Math. Phys. 2013, Theorem 5.3), without effective ranges.
• 2026 — Milman obtains effective ranges for the phases, including the ball phase up to volume fraction $0.120582\ldots$, and reduces the profile conjecture to the two transition volumes $4\pi/81$ and $1/\pi$ (Comm. Pure Appl. Math. 2026, Theorems 1.2–1.3).
• September 2026 — The OpenAI preprint claims the full conjecture with all equality cases (Theorem 1.1, p. 1).

Setting

Let $\mathbb T=\mathbb R^3/\mathbb Z^3$ with its flat metric and volume measure $|\cdot|$ (total volume $1$). For a measurable $E\subseteq\mathbb T$, its perimeter is the De Giorgi perimeter

$$P(E)=\sup\Bigl\{\int_E \operatorname{div}F : F \text{ a smooth vector field on }\mathbb T,\ |F|\le1\Bigr\}\in[0,\infty],$$

which equals the boundary area when $\partial E$ is smooth, and is insensitive to null-set changes. $E$ has finite perimeter if $P(E)<\infty$. A minimizer at volume $V$ is a finite-perimeter $E$ with $|E|=V$ and $P(E)\le P(F)$ for all finite-perimeter $F$ with $|F|=V$.

For $0<V<1$ put $v=\min(V,1-V)$ and

$$I(V)=\min\Bigl\{(36\pi)^{1/3}v^{2/3},\;2\sqrt{\pi v},\;2\Bigr\}.$$

The three expressions are the perimeters of a ball of volume $v$, a solid circular tube of volume $v$ around a shortest closed geodesic (a coordinate circle of length $1$), and a slab of width $v$ between two coordinate tori. The branches cross at $V_1=4\pi/81$ and $V_2=1/\pi$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every $V\in(0,1)$:

1. a minimizer at volume $V$ exists;
2. every minimizer has perimeter exactly $I(V)$;
3. a set $E$ is a minimizer at volume $V\le 1/2$ if and only if, up to an isometry of $\mathbb T$ and a null set, it is a ball of radius $(3V/(4\pi))^{1/3}$ when $V\le 4\pi/81$, a solid tube of radius $\sqrt{V/\pi}$ about a shortest closed geodesic when $4\pi/81\le V\le1/\pi$, or a slab of width $V$ between coordinate tori when $1/\pi\le V$; for $V>1/2$ the minimizers are exactly the complements of those at volume $1-V$.

The ranges are closed, so at each transition volume both adjacent types are minimizers and there are no others. This is OAI.CubicTorus.unit_cubic_isoperimetric.

Significance

The result itself. It determines the isoperimetric profile of the cubic three-torus and the reflected relative profile of the unit cube at every volume, settling a conjecture explicitly posed by Hauswirth–Pérez–Romon–Ros and Ros. The equality classification at the transitions is new even granting Milman's reduction, which classifies minimizers on the open branches once the endpoint values are known but leaves extra co-minimizers at $4\pi/81$ and $1/\pi$ to be excluded.

Formalizing it. The proof combines geometric measure theory (existence and regularity of minimizers), structure theorems for stable CMC surfaces, a differential inequality for the profile, and certified one-variable numerics. A formal proof would certify the whole chain; existence and regularity of isoperimetric regions in a flat torus are themselves substantial missing library pieces. No machine-checked version of the result, or of the Euclidean isoperimetric inequality for finite-perimeter sets in this generality, is known to exist.

Difficulty

The main obstruction is to rule out minimizers whose boundary is a connected surface of genus $2$, $3$ or $4$ (Theorem 2.1, p. 3, quoting Hauswirth–Pérez–Romon–Ros). The general curvature–area bound and the profile differential inequality (Lemma 2.3, p. 4) exclude such surfaces away from the transitions but not at $V_1,V_2$ themselves. At the cylinder–slab transition $V_2=1/\pi$, the planar isoperimetric inequality applied to horizontal sections leaves a deficit in a central curvature range; the preprint closes it with a calibration of a corner section, a nesting argument for planar sections, and a Jensen estimate (Section 6, Proposition 6.7, p. 19), supplemented by certified numerical bounds (Appendix B).

Formalization scope

• The torus is PiLp 2 (fun _ : Fin 3 => AddCircle 1), whose metric is the flat torus metric; volume is the pushforward of Lebesgue measure on the half-open unit cube.
• Perimeter is the De Giorgi supremum over $C^\infty$ $\mathbb Z^3$-periodic vector fields on $\mathbb R^3$ with $|F|\le1$, valued in ℝ≥0∞; no regularity of $E$ is assumed. Finite perimeter also requires null-measurability.
• Minimizers are global: the comparison ranges over all finite-perimeter sets of the same volume.
• The canonical ball is the metric ball about $0$; the tube is $\{x:\|x_1\|^2+\|x_2\|^2<V/\pi\}$ around the $x_0$-direction geodesic; the slab is $\{x:\|x_0\|<V/2\}$. CongruentAE allows any isometry of $\mathbb T$ followed by a null-set change.
• The phase ranges are closed, so both types are included at ties, matching the source. The statement is not vacuous: existence is part of the conclusion, and the profile value is a concrete real number.

Useful reusable infrastructure: sets of finite perimeter on flat tori, compactness and lower semicontinuity of perimeter, and the Euclidean isoperimetric inequality.

Selected references

• OpenAI, The Isoperimetric Conjecture for the Cubic Flat Three-Torus, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026/article.pdf
• L. Hauswirth, J. Pérez, P. Romon, A. Ros, The periodic isoperimetric problem, Trans. Amer. Math. Soc. 356 (2004), 2025–2047. https://doi.org/10.1090/S0002-9947-03-03362-2
• A. Ros, The isoperimetric problem, in Global Theory of Minimal Surfaces, Clay Math. Proc. 2 (2005), 175–209. https://www.claymath.org/wp-content/uploads/2022/03/cmip02.pdf
• E. Milman, Isoperimetric inequalities on slabs with applications to cubes and Gaussian slabs, Comm. Pure Appl. Math. 79 (2026), 1012–1072. https://doi.org/10.1002/cpa.70020
• E. Acerbi, N. Fusco, M. Morini, Minimality via second variation for a nonlocal isoperimetric problem, Comm. Math. Phys. 322 (2013), 515–557. https://doi.org/10.1007/s00220-013-1733-y
• H. Hadwiger, Gitterperiodische Punktmengen und Isoperimetrie, Monatsh. Math. 76 (1972), 410–418. https://doi.org/10.1007/BF01297304
• F. Morgan, D. L. Johnson, Some sharp isoperimetric theorems for Riemannian manifolds, Indiana Univ. Math. J. 49 (2000), 1017–1041. https://www.lehigh.edu/~dlj0/papers/morgan-johnson.pdf
• M. Ritoré, A. Ros, Stable constant mean curvature tori and the isoperimetric problem in three space forms, Comment. Math. Helv. 67 (1992), 293–305. https://doi.org/10.1007/BF02566501

Motivation

The Pontryagin maximum principle is the basic first-order necessary condition of optimal control: along an optimal control, the control value at almost every time extremizes a Hamiltonian built from the dynamics and an adjoint vector. The classical statement presupposes that an optimal control exists. For many problems none does: the set of trajectories is not closed, or the cost does not attain its infimum, and the classical principle then says nothing.

Ekeland's 1974 paper On the Variational Principle (DOI 10.1016/0022-247X(74)90025-0) proves a general result about lower semicontinuous functions on complete metric spaces (its Theorem 1.1, now called Ekeland's variational principle) and closes with an application to control theory in §7 (pp. 348–351): for every terminal-cost problem satisfying mild regularity and growth conditions, there are ε-optimal controls that satisfy the maximum principle up to ε, whether or not an optimal control exists. The argument equips the measurable controls with the metric "measure of the set where two controls differ", which has since become a standard device in nonsmooth and approximate optimal control. For the classical theory, Ekeland refers to the treatise of Pallu de la Barrière (Optimal Control Theory, Saunders, 1967).

Setting

Fix $n \ge 0$, a horizon $T > 0$, an initial state $x_0 \in \mathbb R^n$, and a nonempty compact metrizable space $K$ of control values, with its Borel σ-algebra. A control is a measurable map $u : [0, T] \to K$. The dynamics are a map $f : \mathbb R^n \times K \times [0, T] \to \mathbb R^n$, and the state obeys

$$\frac{dx}{dt}(t) = f(x(t), u(t), t) \ \text{ a.e.}, \qquad x(0) = x_0. \qquad (7.1)$$

A trajectory of $u$ (Lean: IsTrajectory f x₀ T u x) is a function $x$ continuous on $[0, T]$ with $x(t) = x_0 + \int_0^t f(x(s), u(s), s)\,ds$ for all $t \in [0, T]$. The standing hypotheses are:

• (a) $f$ and its state Jacobian $f_x' = (\partial f/\partial x_1, \dots, \partial f/\partial x_n)$ (Lean: fx) are continuous on $\mathbb R^n \times K \times [0, T]$;
• (b) $\langle x, f(x, u, t)\rangle \le c\,(1 + \|x\|^2)$ for some constant $c$.

The terminal cost is given by a $C^1$ function $g : \mathbb R^n \to \mathbb R$, and the problem is to minimize $g(x(T))$ over all controls. The adjoint vector $p$ along a pair $(u, x)$ (Lean: IsAdjoint fx g T u x p) solves the linear equation

$$\frac{dp}{dt}(t) = -{}^t f_x'(x(t), u(t), t)\, p(t), \qquad p(T) = g'(x(T)),$$

where ${}^t A$ is the transpose. The control distance (Lean: ctrlDist T u₁ u₂) is

$$\delta(u_1, u_2) = \operatorname{meas}\{t \in [0, T] \mid u_1(t) \neq u_2(t)\},$$

and the needle variation $v_\tau$ of a control $u_\varepsilon$ at $t_0$ with value $u_0 \in K$ (Lean: needle T uε u₀ t₀ τ) equals $u_0$ on $[0, T] \cap\, ]t_0 - \tau, t_0[$ and $u_\varepsilon$ elsewhere.

Formalization targets

Goal: Theorem 7.1

For every $\varepsilon > 0$ there is a control $u_\varepsilon$ with trajectory $x_\varepsilon$ and adjoint vector $p_\varepsilon$ such that

$$g(x_\varepsilon(T)) \le \inf_u g(x(T)) + \varepsilon, \qquad \langle f(x_\varepsilon(t), u_\varepsilon(t), t), p_\varepsilon(t)\rangle \le \min_{w \in K} \langle f(x_\varepsilon(t), w, t), p_\varepsilon(t)\rangle + \varepsilon \ \text{ a.e. on } [0, T].$$

Milestones

1. (7.2), a priori bound: every trajectory satisfies $\|x(t)\|^2 \le (\|x_0\|^2 + 2cT)e^{2cT}$.
2. Well-posedness (p. 348): every control has exactly one trajectory on $[0, T]$.
3. Lemma 7.2: $(\mathcal U, \delta)$ is a complete metric space (on almost-everywhere classes).
4. Lemma 7.3: $u \mapsto g(x(T))$ is continuous on $(\mathcal U, \delta)$.
5. (7.15)–(7.16): a control $u_\varepsilon$ with $F(u_\varepsilon) \le \inf F + \varepsilon^2$ and $F(u) \ge F(u_\varepsilon) - \varepsilon\,\delta(u, u_\varepsilon)$ for all $u$, where $F(u) = g(x(T))$.
6. Lemma 7.4: the right derivative of $\tau \mapsto g(x_\tau(T))$ at $\tau = 0$, for the needle variations $v_\tau$, equals $\langle f(x_\varepsilon(t_0), u_0, t_0) - f(x_\varepsilon(t_0), u_\varepsilon(t_0), t_0), p_\varepsilon(t_0)\rangle$.

Significance

The result. Theorem 7.1 decouples the maximum principle from existence of optimal controls. Any minimizing sequence can be replaced by one consisting of controls that satisfy the necessary condition up to a vanishing error, so approximate extremals are available for numerical schemes and for limiting arguments (relaxation, convergence of extremals) in problems without compactness or convexity of the velocity sets. The same scheme, a complete metric on controls plus Ekeland's principle plus needle variations, underlies later proofs of the maximum principle with state constraints and in nonsmooth settings.

Formalizing it. The theorem has a published proof, which the paper sketches in four pages and partly defers to classical results (local existence for measurable controls, differentiability of trajectories with respect to needle variations). Neither Mathlib nor the platform contains this theorem or a maximum principle for measurable controls with time-dependent dynamics; the nearest platform items assume an exact optimum, a running cost and globally Lipschitz autonomous dynamics. A formalization requires a Carathéodory theory of ODEs in Lean, the complete metric space of controls, and a rigorous version of the classical first-variation computation. Each of these is useful well beyond this paper.

Difficulty

The obvious argument fails at its first step: a minimizing sequence of controls has no convergent subsequence in any useful sense, because measurable controls with values in $K$ are not compact in the metric $\delta$ and their weak limits are relaxed controls, which are not controls. Ekeland's principle avoids compactness, but it needs a complete metric space on which the cost is lower semicontinuous. Completeness of $(\mathcal U, \delta)$ (Lemma 7.2) and continuity of the cost (Lemma 7.3) both require care. Continuity must hold for trajectories driven by merely measurable controls, which converge only in measure. The needle derivative (Lemma 7.4) holds only at times where the trajectory satisfies the state equation in the classical sense, which is almost every time but not every time.

Formalization scope

• Controls are functions ℝ → K with Measurable u; only values on $[0, T]$ matter. Trajectories and adjoint vectors are functions ℝ → EuclideanSpace ℝ (Fin n), continuous on $[0, T]$ and solving the integral form of their equation. The paper uses the same form in (7.13). A definition that asks for a derivative at every time would be unsatisfiable for discontinuous controls and would make the goal vacuous; the integral form avoids this.
• Hypothesis (a) is stated as joint continuity of f and fx on univ ×ˢ univ ×ˢ Icc 0 T together with HasFDerivAt (fun y => f y u t) (fx x u t) x. Hypothesis (b) is ∃ c, … with the order of arguments $f(x, u, t)$; the page prints $f(t, x, u)$ in (b), a slip.
• The transpose ${}^t f_x'$ is ContinuousLinearMap.adjoint, and $g'(x)$ is gradient g x.
• Infima over controls are never taken as real ⨅; (7.4) and (7.15) are stated as "for every control $u$ with trajectory $x$".
• (7.5) is printed with "$\times\,\varepsilon$". The proof's last line (7.21) gives "$+\,\varepsilon$", which is what is stated. The minimum over the compact $K$ is replaced by the equivalent "for every $w \in K$", with one null set for all $w$.
• Added hypothesis: [Nonempty K] in the goal and milestone 5. With $K$ empty no control exists and the existential statements would be false.
• Lemma 7.2 is stated as the triangle inequality, "$\delta = 0$ iff almost-everywhere equality on $[0, T]$", and sequential completeness for measurable controls. Lemma 7.3 is sequential continuity. Lemma 7.4 is a one-sided derivative within $[0, t_0]$ at $0$, stated for an arbitrary measurable $u_\varepsilon$.
• Theorem 1.1 (Ekeland's principle) is a separate mission of this series and still a draft, so milestone 5 states the instance used here directly.
• Out of scope: the uniform bound (7.3) and the remark after Theorem 7.1 that one may take $\varepsilon = 0$ in (7.5) when (7.4) holds with $\varepsilon = 0$.

Welcome contributions include Carathéodory existence and uniqueness for ODEs with measurable time dependence, Gronwall-type estimates for absolutely continuous functions, the complete metric space of measurable maps under the disagreement measure, and differentiability of flows with respect to initial data.

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
• R. Pallu de la Barrière, Optimal Control Theory, Saunders, Philadelphia, 1967.
• L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, New York, 1962.