Operations Research

Motivation

The maximum flow problem asks how much of a commodity can be shipped from a source to a sink through a network whose arcs have limited capacities. L. R. Ford, Jr. and D. R. Fulkerson's 1956 paper Maximal Flow Through a Network proved the minimal cut theorem: the largest flow value equals the smallest total capacity of a set of arcs that separates source from sink. That theorem is formalized in the companion mission Maximal Flow Through a Network I.

The second section of the same paper treats a special class of networks, those that remain planar after an arc from source to sink is added. For these networks the paper shows that one particular source–sink chain crosses every minimal separating set exactly once. This structural fact turns the minimal cut theorem into a simple computing procedure: repeatedly push as much flow as possible along such a chain and delete the arcs it saturates. The paper notes that G. Dantzig had conjectured, before the minimal cut theorem was proved, that this procedure yields a maximal flow on planar networks. The same "uppermost path" idea underlies later algorithms for maximum flow in planar graphs with source and sink on a common face (Itai and Shiloach, 1979).

The statement is short and purely combinatorial in its conclusion, but its hypothesis is topological. This mission isolates that theorem.

Setting

A network $N$ has a finite set $V$ of vertices and a finite set $E$ of arcs. Each arc $e$ joins two distinct end vertices, written $\mathrm{tail}(e)$ and $\mathrm{head}(e)$; arcs carry no direction, and two arcs may join the same pair of vertices. Two distinct vertices are distinguished, the source $a$ and the sink $b$, and each arc carries a positive capacity (capacities play no role in the target below).

A chain joining $u$ and $w$ is a set $C$ of distinct arcs that can be arranged as $\alpha_1(v_0v_1), \alpha_2(v_1v_2), \dots, \alpha_k(v_{k-1}v_k)$ with $v_0 = u$, $v_k = w$, and the vertices $v_0, \dots, v_k$ pairwise distinct; each arc may be traversed in either direction. The empty set is the null chain from $u$ to $u$.

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$. A disconnecting set none of whose proper subsets is disconnecting is a cut.

The network is ab-planar if the graph of $N$, together with one additional arc joining $a$ and $b$, can be drawn in the plane without crossings: vertices go to distinct points of $\mathbb R^2$; each arc, including the added arc $ab$, goes to an injective continuous path between the points of its end vertices; no arc passes through a vertex other than its ends; and two distinct arcs meet only at endpoints of both. In Lean the drawing is the structure ABPlaneDrawing N, and $N$ is ab-planar when Nonempty (ABPlaneDrawing N). The section's standing assumption is that no arc of $N$ already joins $a$ and $b$.

Formalization targets

Goal: Theorem 2 (p. 403)

If $N$ is ab-planar, no arc of $N$ joins $a$ and $b$, and some chain joins $a$ and $b$, then

$$\exists\, T \text{ a chain joining } a \text{ and } b \ \text{ such that }\ |T \cap D| = 1 \ \text{ for every cut } D \text{ of } N.$$

This is FordFulkerson56.Planar.ab_planar_exists_chain_meeting_each_cut_once. "Precisely once" is exact cardinality one, neither "at least once" (true of every chain) nor "at most once".

Milestone: a chain meeting a cut in one prescribed arc (proof of Theorem 2, p. 403)

For every network $N$, every cut $D$ and every arc $\alpha \in D$, there is a chain $C$ joining $a$ and $b$ with $C \cap D = \{\alpha\}$. No planarity is involved; the statement is what the minimality of a cut provides to the proof.

Further item: the Fig. 2 example (p. 403)

In the "gas, water, electricity" graph $K_{3,3}$ with the arc $ab$ removed, every chain joining $a$ and $b$ meets some cut in three arcs. This network is not ab-planar, so the example shows that the planarity hypothesis of Theorem 2 cannot be dropped.

Significance

Theorem 2 and the minimal cut theorem together give the paper's procedure for planar networks: if $T$ meets every cut once, then imposing a flow $k$ on $T$ lowers the value of every cut by exactly $k$, so the minimal cut value, and hence the maximal flow value, drops by $k$. Saturated arcs can then be deleted and the step repeated. Without the "exactly once" property the reduction could overshoot the cut structure, and the greedy step would not be justified. The theorem is also one of the earliest instances of the link between planarity and cut structure that later underlies planar duality arguments for minimum cuts.

The result has been known since 1956 and is not open. No machine-checked version is recorded on the platform, and Mathlib, at the pinned revision, has neither planar graphs nor the Jordan curve theorem. A formal proof would be the first formalized statement about source–sink planar networks in this library, and the counterexample item records, as a checkable fact, that the hypothesis is necessary.

Difficulty

The conclusion is combinatorial while the hypothesis is a drawing in $\mathbb R^2$. The paper's proof normalises the drawing (the added arc $ab$ on the outer boundary, the graph in a vertical strip with $a$ on the left line and $b$ on the right), selects the "top-most" chain from $a$ to $b$, and argues that a chain meeting a cut below the top-most chain must cross another such chain. Each of these steps rests on plane topology: the existence of the outer region, the meaning of "top-most", and the fact that two chains with interleaved endpoints on a boundary must intersect, which is a form of the Jordan curve theorem.

The naive purely combinatorial route fails: the analogous statement for arbitrary networks is false (Fig. 2), so any argument has to use the drawing somewhere. Replacing the drawing by a combinatorial embedding (rotation systems, faces) is possible but then requires proving that the two notions agree, which is again Jordan-curve territory.

Formalization scope

Conventions committed to in the Lean statements:

• Vertices and arcs are finite types V, E with decidable equality. Arcs are undirected, may be parallel, and have two distinct end vertices. Source and sink are distinct, capacities are positive (structure Network).
• A chain is a Finset E that is the arc set of some arrangement as a simple path (IsChainWalk, IsChain); the null chain is allowed.
• IsDisconnecting and IsCut quantify over all chains joining source and sink; a cut is a disconnecting set no proper subset of which is disconnecting.
• ab-planarity is a plane drawing of the graph with the extra arc indexed by none : Option E, with injective Paths in ℝ × ℝ as arcs.

Hypotheses of the goal: hno_ab, the standing assumption of §2 (no arc joins $a$ and $b$, p. 403); hconn, that some chain joins $a$ and $b$. The second is not stated in the paper; its proof starts from "the chain joining a and b which is top-most", which presupposes one, and without it the statement is false (if $a$ and $b$ are disconnected, the empty set is a cut and no chain exists).

The drawing structure is satisfiable (a three-vertex path network has an explicit drawing), so the planarity hypothesis is not vacuous; and it covers the added arc $ab$ and all crossings, so $K_{3,3}$ minus $ab$ is not ab-planar and the goal is not refuted by the paper's own example. A formalization that dropped the arc $ab$ from the drawing, or quantified over disconnecting sets instead of cuts, would state a false theorem and is ruled out.

A complete development needs basic plane topology for paths in $\mathbb R^2$ (a Jordan-curve-type separation lemma for simple closed curves, or an equivalent statement about crossing paths in a strip), together with combinatorial lemmas about chains (concatenation and shortcutting of chains at a common vertex). The topological lemmas are reusable well beyond this mission. Proofs through a combinatorial embedding are welcome, provided the equivalence with ABPlaneDrawing is proved.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• A. Itai and Y. Shiloach, Maximum flow in planar networks, SIAM Journal on Computing 8 (1979), 135–150. https://doi.org/10.1137/0208012
• H. Whitney, Planar graphs, Fundamenta Mathematicae 21 (1933), 73–84. https://doi.org/10.4064/fm-21-1-73-84

Motivation

A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model $(P_0, r_0)$. It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not $(s,a)$-rectangular.

Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for $s$-rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $\gamma\in(0,1)$ a discount factor, $P_0(s'\mid s,a)$ a transition kernel and $r_0(s,a)$ a reward. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to each state a probability distribution $\pi_s$ on $\mathcal A$. For $v\in\mathbb R^{\mathcal S}$ write $q_s(a)=r_0(s,a)+\gamma\sum_{s'}P_0(s'\mid s,a)v(s')$ and

$$[T^\pi_{(P_0,r_0)}v](s)=\sum_a\pi_s(a)\,q_s(a).$$

All norms $\|\cdot\|$ below are $\ell_2$-norms, $\|a\|=\big(\sum_z a(z)^2\big)^{1/2}$; $\|\cdot\|_\infty$ is the sup norm.

Fix nonnegative radii $\alpha^r_s,\alpha^P_s$ for each state. The R² regularizer is $\Omega_{v,\mathrm R^2}(\pi_s)=\|\pi_s\|\,(\alpha^r_s+\alpha^P_s\gamma\|v\|)$, and the R² Bellman operators are

$$[T^{\pi,\mathrm R^2}v](s)=[T^\pi_{(P_0,r_0)}v](s)-\Omega_{v,\mathrm R^2}(\pi_s),\qquad [T^{*,\mathrm R^2}v](s)=\max_{\pi\in\Delta^{\mathcal S}_{\mathcal A}}[T^{\pi,\mathrm R^2}v](s).$$

A policy $\pi$ is greedy for $v$ when $T^{\pi,\mathrm R^2}v=T^{*,\mathrm R^2}v$.

Assumption 5.1 (bounded radius). For each $s$ there is $\epsilon_s>0$ with

$$\alpha^P_s\le\min\Big(\frac{1-\gamma-\epsilon_s}{\gamma\sqrt{|\mathcal S|}}\ ;\ \min_{u\in\mathbb R^{\mathcal A}_+,\|u\|=1,\ w\in\mathbb R^{\mathcal S}_+,\|w\|=1}\ \sum_{a,s'}u(a)P_0(s'\mid s,a)w(s')\Big),$$

and $\epsilon_*=\min_s\epsilon_s$. The R² value function $v^{\pi,\mathrm R^2}$ of a policy and the R² optimal value $v^{*,\mathrm R^2}$ are the fixed points of $T^{\pi,\mathrm R^2}$ and $T^{*,\mathrm R^2}$.

Formalization targets

Goal: Theorem 5.1 (p. 8)

Under Assumption 5.1, $T^{*,\mathrm R^2}$ and every $T^{\pi,\mathrm R^2}$ have unique fixed points; a greedy policy $\pi^{*,\mathrm R^2}$ for $v^{*,\mathrm R^2}$ exists, and every such policy satisfies

$$v^{\pi^{*,\mathrm R^2},\mathrm R^2}=v^{*,\mathrm R^2}\ \ge\ v^{\pi,\mathrm R^2}\qquad\text{for all }\pi\in\Delta^{\mathcal S}_{\mathcal A};$$

every optimal policy is greedy; and when $\alpha^r_s>0$ for all $s$ the greedy policy is unique, hence the unique optimal R² policy.

Milestones

1. Proposition 2.1 (p. 3): for $\Omega$ strongly convex on the simplex, $\Omega^*(y)=\max_{a\in\Delta}\langle a,y\rangle-\Omega(a)$ is differentiable with Lipschitz gradient equal to the unique maximizer, satisfies $\Omega^*(y+c\mathbb 1)=\Omega^*(y)+c$, and is non-decreasing.
2. Proposition 5.1 (i) (p. 8): $v_1\le v_2$ implies $T^{\pi,\mathrm R^2}v_1\le T^{\pi,\mathrm R^2}v_2$ and $T^{*,\mathrm R^2}v_1\le T^{*,\mathrm R^2}v_2$.
3. Proposition 5.1 (iii) (p. 8):

$$\|T^{\pi,\mathrm R^2}v_1-T^{\pi,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty,\qquad \|T^{*,\mathrm R^2}v_1-T^{*,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty.$$

Significance

Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an $s$-rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.

The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.

Difficulty

The R² evaluation operator is not affine: the value regularizer $-\alpha^P_s\gamma\|\pi_s\|\,\|v\|$ is concave in $v$ and decreases as $\|v\|$ grows. Monotonicity therefore does not follow from the positivity of $P_0$ as in the standard case; it requires the second bound of Assumption 5.1, which compares the $\ell_2$ variation of $\|v\|$ with the minimal nonnegative bilinear form of $P_0(\cdot\mid s,\cdot)$. Likewise the contraction modulus is not $\gamma$ but $1-\epsilon_*$, because the regularizer is $\sqrt{|\mathcal S|}$-Lipschitz between the $\ell_2$ and sup norms. The optimality step of the classical proof uses linearity of $T^\pi$ when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.

Formalization scope

States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The $\ell_2$-norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for $\|\cdot\|_\infty$). $T^{*,\mathrm R^2}v(s)$ is the real supremum over the simplex $\Delta_{\mathcal A}$ (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative $\ell_2$-unit vectors; the witnesses $\epsilon_s$ are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.

Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes $\alpha^r_s>0$ for all $s$: with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes $\Omega$ continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, $P_0=1$, $r_0=0$, $\gamma=1/2$, $\alpha^r=0$, $\alpha^P=1/2$, $\epsilon=1/4$, one has $Tv=v/2-|v|/4$, and $v_1=-1$, $c=1$ give $T(v_1+c)=0>-1/4=Tv_1+\gamma c$. Remark 5.1, Algorithm 1 and the $\ell_p$ variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is $0$ whenever some $P_0(s'\mid s,a)=0$, forcing $\alpha^P_s=0$; this is the assumption as printed.

A formalization in which $\|\cdot\|$ is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of $p\mapsto\langle p,q\rangle-c\|p\|$ on the simplex.

Selected references

• E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
• M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. arXiv:1901.11275
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
• A. Mensch, M. Blondel, Differentiable dynamic programming for structured prediction and attention, ICML 2018. arXiv:1802.03676

Motivation

Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow $\dot x=-\nabla f(x)$ for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic $f$ this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value $+\infty$, by replacing $\|\nabla f\|$ with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower-$C^2$ functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).

Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to $C^1$ functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.

Setting

Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$. The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\neq x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge0$. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $x_k\to x$ and $f(x_k)\to f(x)$. The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|: x^*\in\partial f(x)\}$, equal to $+\infty$ when $\partial f(x)=\emptyset$, and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points.

The standing assumptions of Section 4 are:

• $(\mathcal H1)$ $f$ is either lower semicontinuous and convex, or lower-$C^2$ with $\operatorname{dom} f=\mathbb R^n$. Lower-$C^2$ means that near each point $f=\max_{s\in S}F(\cdot,s)$ for a compact space $S$ and a jointly continuous $F$ with jointly continuous first and second $x$-derivatives.
• $(\mathcal H2)$ $f$ is somewhere finite and bounded from below.
• $(\mathcal H3)$ $f$ is subanalytic: its graph is locally the projection of a bounded set defined by finitely many real-analytic equalities and strict inequalities.

A trajectory of the subgradient system $(\mathcal G)$ is an absolutely continuous curve $x:[0,T)\to\mathbb R^n$, $T\in(0,+\infty]$, with $\dot x(t)+\partial f(x(t))\ni0$ for almost every $t$ and $\partial f(x(t))\neq\emptyset$ for every $t$. It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around $a$ with exponent $\theta$ if $|f-f(a)|^\theta/m_f$ is bounded near $a$, with $0^0=1$ and $\infty/\infty=0/0=0$. A Łojasiewicz exponent at $a\in\operatorname{dom} f$ is any such $\theta\in[0,1)$.

Formalization targets

Goal: Theorem 4.7

Under $(\mathcal H1)$–$(\mathcal H3)$, every bounded maximal trajectory $x$ is defined on $[0,+\infty)$ and converges to a critical point $a$. For every Łojasiewicz exponent $\theta$ at $a$ there are $k,k'>0$ and $t_0\ge0$ such that for $t\ge t_0$

$$\|x(t)-a\|\le \begin{cases} k\,(t+1)^{-\frac{1-\theta}{2\theta-1}}, & \theta\in(\tfrac12,1),\\[2pt] k\,e^{-k't}, & \theta=\tfrac12,\end{cases}$$

and for $\theta\in[0,\tfrac12)$, $x(t)=a$ for all large $t$. The constants are existential, so the goal survives any later sharpening of them.

Milestones

1. Corollary 4.1(i): for almost every $t$, $\frac{d}{dt}f(x(t))=\langle\dot x(t),x^*\rangle$ for every $x^*\in\partial f(x(t))$.
2. Corollary 4.1(iii): every trajectory extends to a maximal one on $[0,+\infty)$ with $\dot x\in L^2$.
3. Corollary 4.2: $\|\dot x(t)\|=m_f(x(t))$ and $\frac{d}{dt}f(x(t))=-m_f(x(t))^2$ almost everywhere.
4. Inequality (20): the Łojasiewicz inequality holds around every point of $\operatorname{dom}\partial f$.
5. Theorem 4.5: bounded maximal trajectories have finite length $\int_0^\infty\|\dot x\|<\infty$ and converge to a critical point.
6. The tail bound $\int_t^\infty\|\dot x\|\le\frac{c}{1-\theta}(f(x(t))-f(a))^{1-\theta}$.
7. Inequality (27): $\int_t^\infty\|\dot x\|\le\frac{c^{1/\theta}}{1-\theta}\|\dot x(t)\|^{(1-\theta)/\theta}$ for almost every large $t$.

Significance

Theorem 4.5 says that for convex or lower-$C^2$ subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at $\theta=\tfrac12$, polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.

On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on $[0,T)$, a chain rule for $f\circ x$ along absolutely continuous curves, and a comparison lemma for the differential inequality $\dot\sigma\le-L\sigma^\alpha$. The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.

Difficulty

Compactness gives cluster points of a bounded trajectory, and the decrease of $f$ gives convergence of $f(x(t))$. Neither gives convergence of $x(t)$. The usual first idea, that $\int_0^\infty\|\dot x\|^2<\infty$ forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control $\int\|\dot x\|$ rather than $\int\|\dot x\|^2$. That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: $f\circ x$ is differentiable almost everywhere with derivative $\langle\dot x,x^*\rangle$ for every $x^*\in\partial f(x(t))$, which relies on $\partial f=\hat\partial f$ for convex and lower-$C^2$ functions. Global existence on $[0,+\infty)$ (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.

Formalization scope

Space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes $-\infty$. The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope $m_f$ is valued in $[0,+\infty]$. The Łojasiewicz inequality is encoded as $|f(y)-f(a)|^\theta\le C\|v\|$ for $y$ near $a$ and every $v\in\partial f(y)$, which is the bounded ratio under the paper's conventions. Times are real numbers and $T\in[0,+\infty]$. Curves are functions $\mathbb R\to\mathbb R^n$ whose values outside $[0,T)$ are irrelevant. "Absolutely continuous on $[0,T)$" means absolutely continuous on every compact $[0,b]\subseteq[0,T)$. Velocities appear only "for almost every $t$". Lengths are lower Lebesgue integrals $\int^-\|\dot x\|$ in $[0,+\infty]$, never Bochner integrals (which would vanish for a non-integrable speed).

Two trivializations are ruled out. Maximality is a hypothesis and $T=+\infty$ is a conclusion: assuming $T=+\infty$ would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on $\mathbb R_+$ with $\dot{\hat x}\in L^2$", because the printed $\hat x\in W^{1,2}(\mathbb R_+)$ would fail for any trajectory with nonzero limit.

Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower-$C^2$ functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.

Selected references

• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
• H. Brézis, Opérateurs maximaux monotones et semi-groupes de contractions dans les espaces de Hilbert, North-Holland, 1973.
• J.-P. Aubin, A. Cellina, Differential Inclusions, Springer, 1984. https://doi.org/10.1007/978-3-642-69512-4
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116 (2009) 5–16. https://doi.org/10.1007/s10107-007-0133-5

Motivation

Many estimation procedures in statistics, and most stochastic optimization models in operations research, have the same shape: a decision or parameter $x\in\mathbb R^n$ is chosen to minimize an expected loss $Ef(x)=\int f(x,\xi)\,P(d\xi)$ under a distribution $P$ that is not known. In practice $P$ is replaced by an estimate $P^\nu$ built from the information available at stage $\nu$ (an empirical measure, a smoothed or parametric fit, a Bayesian posterior), and the minimizer of the estimated problem is used in place of the true one. The basic question is whether this is justified: do the estimated solutions converge to a true solution, and the estimated optimal values to the true optimal value, as information accumulates?

For maximum likelihood this is Wald's consistency theorem (Wald 1949); Huber extended it to M-estimators under non-standard conditions (Huber 1967). Both settings are unconstrained, or constrained to an open set, and assume finite-valued criteria. Constrained least squares, $L^1$ and Huber regression with inequality constraints, variance-component models with Heywood cases, and two-stage stochastic programs with recourse all lead instead to criteria that take the value $+\infty$ off a closed feasible set and are only lower semicontinuous in $x$.

J. Dupačová and R. Wets (IIASA WP-86-41, 1986; journal version Ann. Statist. 16 (1988)) proved consistency in this generality by combining epi-convergence of functions with the theory of measurable multifunctions and normal integrands. This mission formalizes their §3.

Setting

$\Xi$ is a Polish space with its Borel $\sigma$-field and $P$ is a probability measure on it. The integrand is $f:\mathbb R^n\times\Xi\to(-\infty,\infty]$, and the true problem is to minimize

$$Ef(x)=\int_\Xi f(x,\xi)\,P(d\xi),$$

with the convention that $Ef(x)=+\infty$ whenever $\xi\mapsto f(x,\xi)$ is not bounded above by a summable function. The effective domain of a function $h:\mathbb R^n\to[-\infty,\infty]$ is $\operatorname{dom}h=\{x: h(x)<\infty\}$, and $\operatorname{argmin}h=\{x: h(x)=\inf h\}$.

Information arrives on a probability space $(Z,\mathcal F,\mu)$ with an increasing sequence of $\sigma$-fields $\mathcal F^1\subseteq\mathcal F^2\subseteq\dots\subseteq\mathcal F$. Each sample $\zeta\in Z$ yields probability measures $P^\nu(\cdot,\zeta)$ on $\Xi$, and $\zeta\mapsto P^\nu(A,\zeta)$ is $\mathcal F^\nu$-measurable for every Borel $A$: the estimate at stage $\nu$ uses only stage-$\nu$ information. The estimated problem minimizes

$$E^\nu f(x,\zeta)=\int_\Xi f(x,\xi)\,P^\nu(d\xi,\zeta).$$

A sequence $g^\nu$ epi-converges to $g$ if, at every $x$, $\liminf g^\nu(x^\nu)\ge g(x)$ along every sequence $x^\nu\to x$, and $\limsup g^\nu(x^\nu)\le g(x)$ along some sequence $x^\nu\to x$.

The standing hypotheses are Assumption 3.4: $\operatorname{dom}f=S\times\Xi$ with $S$ closed and nonempty; $f(x,\cdot)$ is continuous for $x\in S$; $f(\cdot,\xi)$ is lower semicontinuous; and $f$ is locally lower Lipschitz on $S$ with a bounded continuous modulus $\beta(\xi)$. Assumption 3.5 asks that, for $\mu$-almost every $\zeta$, $P^\nu(\cdot,\zeta)$ converge in distribution to $P$, that $|f(x,\cdot)|$ be uniformly tight along $P=P^0,P^1,\dots$ for each $x\in S$, and that $\int\inf_x f(x,\xi)\,P^\nu(d\xi,\zeta)>-\infty$ for all $\nu$.

Formalization targets

Goal: Theorem 3.9, "In particular" (pp. 21–22)

Let $D\subseteq\mathbb R^n$ be compact, suppose $(\operatorname{argmin}E^\nu f)\cap D\neq\emptyset$ $\mu$-a.s. for every $\nu$, and suppose $\{x^*\}=\operatorname{argmin}Ef\cap D$. Then there are $\mathcal F^\nu$-measurable selections $x^\nu$ of $\operatorname{argmin}E^\nu f$ with

$$x^\nu(\zeta)\to x^*\quad\text{and}\quad \inf E^\nu f(\cdot,\zeta)\to\inf Ef\qquad\text{for }\mu\text{-almost every }\zeta .$$

The goal does not assume that $Ef$ has a unique global minimizer, and it does not assume convexity.

Milestones

In attack order:

• Proposition 3.3: epi-convergence gives $\limsup(\inf g^\nu)\le\inf g$, limits of minimizers are minimizers, and the minimum is attained in the closure of a bounded $D$.
• Lemma 3.6: almost surely, $Ef$ and every $E^\nu f$ are proper and l.s.c., with domain $S$.
• Theorem 3.7: almost surely, $E^\nu f$ epi-converges and converges pointwise to $Ef$.
• Theorem 3.8: almost surely, the epigraphs of $E^\nu f$ are closed, and they depend $\mathcal F^\nu$-measurably on $\zeta$.
• Theorem 3.9:
  • (3.14) $\limsup(\inf E^\nu f)\le\inf Ef$ a.s.;
  • (i) cluster points of estimated minimizers minimize $Ef$;
  • (ii) $\zeta\mapsto\operatorname{argmin}E^\nu f(\cdot,\zeta)$ is closed-valued and $\mathcal F^\nu$-measurable.
• Proposition 3.1: the measurable selection theorem.

Significance

The result separates two things: the statistical input, which is only convergence in distribution of $P^\nu$ plus a tightness condition, and the variational output, which is convergence of optimal values and solutions. It therefore applies to any estimator $P^\nu$ that converges weakly almost surely: empirical measures, kernel estimates, parametric fits. It also covers constrained and nonsmooth problems: the feasible set enters through $f=+\infty$ off $S$, and only lower semicontinuity in $x$ is required. Asymptotic distribution results for constrained estimators, such as the second part of the same paper and the subsequent literature on sample average approximation, start from this consistency.

The theorem is proved on paper. To the best of current knowledge none of it is machine-checked. Mathlib has weak convergence of probability measures, lower semicontinuity and extended-real integrals. It does not have epi-convergence, Effros-measurable multifunctions, normal integrands or the Kuratowski–Ryll-Nardzewski selection theorem. A formal proof produces these as reusable components. It also has to supply the details that the paper's proof of Theorem 3.8 leaves as a sketch.

Difficulty

Pointwise convergence $E^\nu f(x)\to Ef(x)$ is not enough to move minimizers to the limit, and uniform convergence fails because $f$ is $+\infty$ off $S$ and need not be bounded. Epi-convergence is the right notion. Proving it needs a liminf inequality along moving points $x^\nu\to x$ under moving measures $P^\nu$. That combines Fatou's lemma, the lower Lipschitz bound and the tightness condition, and the integrands are extended-real-valued, so care is needed.

The second difficulty is measurability. The exceptional null set lies in $\mathcal F$ but not in $\mathcal F^\nu$, so "$\mathcal F^\nu$-measurable" has to be understood on a full-measure set in the trace $\sigma$-field. The paper's argument for Theorem 3.8 appeals to continuity of $P\mapsto\operatorname{epi}E_Pf$ in the epi-topology, and it remarks itself that Theorem 3.7 gives this only along sequences satisfying Assumption 3.5. A solver will have to rebuild this step, for example through the normal-integrand structure of $E^\nu f$.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Euclidean norm.
• $\Xi$ is a Polish space with its Borel $\sigma$-algebra. This is exactly a closed subset of a Polish space with the relative Borel field.
• $f$ is EReal-valued. Every expectation is the mission's expect: $+\infty$ when $\int f^+=\infty$, and $\int f^+-\int f^-$ otherwise, both computed as Lebesgue integrals of $[0,\infty]$-valued functions. A Bochner integral, which would assign $0$ to non-integrable functions, is never used for $Ef$ or $E^\nu f$.
• The sample index is shifted: Lean's Pν k and 𝔽 k are the paper's $P^{k+1}$ and $\mathcal F^{k+1}$, and $P=P^0$ is a separate argument.
• Infima, $\liminf$ and $\limsup$ are taken in $[-\infty,\infty]$.
• Measurability on the full-measure set $Z_0$ uses the trace $\sigma$-field.
• The selections in the goal are total, $\mathcal F^\nu$-measurable maps $Z\to\mathbb R^n$ that select almost surely. This is equivalent to the paper's maps $Z_0\to\mathbb R^n$.
• "Random l.s.c. function" in Theorem 3.8 is encoded by the equivalent conditions (3.4i)–(3.4ii): nonempty, closed and measurable epigraphs.
• Lower Lipschitz (3.10) is written additively.
• The hypothesis that $\Xi$ is the support of $P$ is omitted. It is unused in §3, and omitting it strengthens every statement.
• Nothing beyond the page is assumed: no convexity, no compact $S$, no bounded $f$, no unique minimizer, no i.i.d. sampling, no empirical $P^\nu$, no completeness of $\mu$ or $\mathcal F^\nu$.

The hypotheses are not vacuous. A sorry-free check verifies all of them, including those of the goal, for $f(x,\xi)=\|x\|^2$ with Dirac measures. Defining the expectation through a Bochner integral, or dropping $S\neq\emptyset$ (which makes every $\operatorname{argmin}$ all of $\mathbb R^n$), would trivialize or change the statements; the definitions above rule both out.

Contributions are welcome on any milestone. Proposition 3.1 (Kuratowski–Ryll-Nardzewski for $\mathbb R^m$-valued multifunctions) and Proposition 3.3 (deterministic epi-convergence facts) are independent of the probabilistic setting and reusable beyond this mission.

Selected references

• J. Dupačová, R. Wets, Asymptotic Behavior of Statistical Estimators and Optimal Solutions for Stochastic Optimization Problems, IIASA Working Paper WP-86-41, 1986. https://pure.iiasa.ac.at/id/eprint/2818/ — journal version: Ann. Statist. 16(4), 1517–1549, 1988. https://doi.org/10.1214/aos/1176351052
• A. Wald, Note on the consistency of the maximum likelihood estimate, Ann. Math. Statist. 20, 595–601, 1949. https://doi.org/10.1214/aoms/1177729938
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1, 221–233, 1967. https://projecteuclid.org/euclid.bsmsp/1200512988
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Ch. 7 epi-convergence; Ch. 14 measurable multifunctions and normal integrands). https://doi.org/10.1007/978-3-642-02431-3

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$. Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$, and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

$$\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}$$

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$, the derivatives $G_i'(v)$, $i\in I(v)$, are linearly independent in $V^*$.

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$, and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

$$F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,$$ $$\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.$$

Milestones, in the order of the paper's proof

1. (3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$; no regularity needed).
2. (3.16): at a regular feasible point $v$, every $h$ with $\langle G_i'(v),h\rangle=0$ ($i\le p$) and $\langle G_i'(v),h\rangle\ge0$ ($i>p$, $i\in I(v)$) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$.
3. Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$.
4. Lemma 3.3: an $\varepsilon$-Farkas–Minkowski lemma in $V^*$: if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$, then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$.

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$, $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$, then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$.

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$, but that function is not differentiable at $v_\varepsilon$, so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$; closing this gap requires the regularity assumption and completeness of $V$, and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$, must be turned into an approximate multiplier representation in $V^*$, an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

• $V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
• Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$, an equality constraint iff its index is $<p$. p ≤ m is assumed in the goal.
• $C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
• No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and "$F(v)\le\inf_{\mathcal C}F+\varepsilon^2$" is "$F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$". A real infimum over an empty or unbounded set would be a junk value.
• Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ($\inf\emptyset=+\infty$) while the conclusion asks for a feasible point.
• Lemma 3.3 is stated with $\le\varepsilon$. The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$, no constraints and $w^*=\varepsilon\,\mathrm{id}$; its proof gives $\le$, and Theorem 3.1 uses $\le$.
• Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
• Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$, so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$, and a closedness result for finitely generated cones in $V^*$.

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. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$, a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$. The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$, and $\mathcal K=\mathrm{Conv}(\mathcal C)$. An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$. In round $t$ the learner plays a random arm $v_t\in\mathcal C$, pays $\ell_t^\top v_t$, and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$. The pseudo-regret is

$$\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .$$

A Legendre function on $\bar D$, for a nonempty open convex $D$, is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$. Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$, and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$.

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$. It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$. OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

$$\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}$$

A $0$-potential is a convex, $C^1$, increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$, $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$. It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$. With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$-potential $\psi$ and non-negative unbiased estimates,

$$\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].$$

For $\psi(x)=(-x)^{-q}$ with $q>1$, the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$,

$$\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.$$

Milestones

1. Lemma 5.1: $F^{**}=F$, $\nabla F^*=(\nabla F)^{-1}$ on $D^*$, and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$.
2. Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
3. Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$.
4. Theorem 5.5, linear losses, and its corrected general form.
5. Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$.
6. Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$.

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$, with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$. Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$. A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$.

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$, so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$, and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$.

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$, and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$, sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$, which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$, $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$.

Corrections and instantiations, each labelled in the item's Formalization Note:

• Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$. The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$, which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$.
• Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$. That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$. The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$, as the proof's first inequality does. The linear-loss bound is stated as printed.
• Lemma 5.2. "For all $z\in K\cap D$" is read as "for the projection $z$", which lies in $K\cap D$.
• Hypotheses made explicit: $q>1$; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$); a subgradient selection as an explicit input.
• Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$, $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$, a Lean division $x/0=0$, or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$.

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$-potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
• J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598