Convex Optimization

Motivation

A conic quadratic program minimizes a linear objective subject to constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy $\varepsilon$ using $O(k\ln(2/\varepsilon))$ variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral $\varepsilon$-approximation needs $\Omega(k\ln(1/\varepsilon))$ inequalities.

The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.

Setting

For $y\in\mathbb R^k$ write $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The Lorentz cone is

Let $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ such that

1. if $(y,t)\in L^k$, then $\Pi(y,t,u)\ge0$ for some $u\in\mathbb R^p$;
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Here $\ge0$ is componentwise, $p$ is the number of auxiliary variables and $q$ the number of homogeneous linear inequalities. Equivalently, the polyhedral cone $K=\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone $\widehat L^k$ of the $(y,t)$-space with $L^k\subseteq\widehat L^k\subseteq\{(y,t)\mid\|y\|_2\le(1+\varepsilon)t\}$. The slice of $\widehat L^k$ at height one is $G=\{y\mid(y,1)\in\widehat L^k\}$, and $B=\{y\mid\|y\|_2\le1\}$ denotes the closed unit ball.

Formalization targets

Goal: Proposition 3.1, Eq. (13)

The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.

Milestones (claims of the proof, in order)

1. Reduction. For $\varepsilon>0$ one may replace $\Pi$ by an approximation with the same $q$, at most $p$ auxiliary variables and the same projection, whose cone $K$ contains no line.
2. Extreme rays. A line-free cone $\{z\mid Az\ge0\}$ defined by $q$ inequalities is the conic hull of at most $2^q$ extreme rays.
3. Sandwich. $B\subseteq G\subseteq(1+\varepsilon)B$.
4. Vertices. If $K$ has no line, $G$ is the convex hull of $N\le2^q$ points.
5. Covering. If $\operatorname{conv}\{y_1,\dots,y_N\}\supseteq B$ and all $\|y_i\|_2\le1+\varepsilon$, the closed balls of radius $\sqrt{2\varepsilon(1+\varepsilon)}$ about the $y_i$ cover the sphere $\{\|y\|_2=1+\varepsilon\}$.
6. Counting. For $k\ge2$ and $\varepsilon\le\tfrac12$ such a covering needs $N\ge\exp\{c\,k\ln(1/\varepsilon)\}$ balls.

Significance

The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension $k$ to relative accuracy $\varepsilon$ by linear inequalities costs $\Theta(k\ln(1/\varepsilon))$ inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on $1/\varepsilon$, from what it cannot buy, a sub-linear dependence on $k$ or on $\ln(1/\varepsilon)$. Without auxiliary variables a polytope approximating the ball needs $\varepsilon^{-\Omega(k)}$ facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.

Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).

Difficulty

The obvious argument counts vertices of $G$: at most $2^q$ of them, and a polytope between $B$ and $(1+\varepsilon)B$ needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of $G$ with $B$ gives nothing, since $G$ may have the volume of $(1+\varepsilon)B$. The argument needs the transfer from "the convex hull of the points contains $B$" to "the points are $\sqrt{2\varepsilon(1+\varepsilon)}$-dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to $k=2$ and up to $\varepsilon=\tfrac12$, where $\ln(1/\varepsilon)$ is only $\ln2$ and the radius $\sqrt{2\varepsilon(1+\varepsilon)}$ is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: $K$ itself may contain lines in the $u$-directions, in which case it has no extreme rays at all.

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which $L^k$ is polyhedral and the goal is false. A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and $p$, $q$ are the dimensions of its types; with arbitrary (nonlinear) maps, $\Pi(y,t)=t-\|y\|_2$ would give $q=1$, so linearity is what makes the statement non-trivial. "Extreme ray" means a ray $\{sr\mid s\ge0\}$, $r\ne0$, that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.

Corrections of the printed statement. Proposition 3.1 is printed for every positive integer $k$. It is false for $k=1$: $L^1=\{|y|\le t\}$ is polyhedral, and $\Pi(y,t)=(t-y,t+y)$ is a polyhedral $\varepsilon$-approximation with $q=2$ for every $\varepsilon$, so $q\ge c\ln(1/\varepsilon)$ fails for small $\varepsilon$. The goal and the counting milestone are therefore stated for $k\ge2$, which is the case the proof covers. The phrase "polyhedral $\alpha$ approximation" in the proof is read as $\varepsilon$. The paper's $O(1)$ constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.

A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

Motivation

Monotone operators from a Banach space $E$ to its dual $E^*$ are the abstract framework for nonlinear equations, variational inequalities and evolution equations, and for the convergence theory of proximal-point and splitting algorithms in infinite dimensions. Within that framework, the class that behaves well — for surjectivity results, for resolvents, for sums — is the class of maximal monotone operators. The most important source of such operators is convex analysis: the subdifferential of a convex function. Whether every subdifferential of a closed proper convex function is maximal monotone, in an arbitrary Banach space, is therefore a basic question for convex optimization in function spaces.

Timeline:

• 1964. G. J. Minty proves maximality of the subdifferential for convex functions that are finite and continuous everywhere (Minty, Pacific J. Math. 14 (1964)).
• 1965. A. Brøndsted and R. T. Rockafellar show that subgradients exist on a dense set and approximate ε-subgradients (Brøndsted–Rockafellar, Proc. AMS 16 (1965)). J.-J. Moreau develops proximal maps and conjugate duality for convex functions in Hilbert space (Moreau, Bull. SMF 93 (1965)); his later lecture notes Fonctionnelles convexes (Collège de France, 1967) are the paper's reference for conjugates in locally convex spaces.
• 1966. R. T. Rockafellar announces the general Banach-space result, for every lower semicontinuous proper convex function (Rockafellar, Pacific J. Math. 17 (1966)). H. Brézis later points out a gap in that proof: a subgradient chosen in the argument may grow without bound.
• 1970. Rockafellar gives a complete proof by a different route, valid in nonreflexive spaces, in the paper formalized here (Rockafellar, Pacific J. Math. 33 (1970)).

Setting

Let $E$ be a real Banach space with dual $E^*$ and bidual $E^{**}$, and write $\langle x, x^*\rangle = x^*(x)$. $E$ sits in $E^{**}$ through the canonical embedding.

A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$, not identically $+\infty$, such that $f((1-\lambda)x + \lambda y) \le (1-\lambda) f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$. It is lower semicontinuous for the norm topology.

The subdifferential of $f$ is the multivalued map $\partial f : E \to E^*$,

A multivalued map $T : E \to E^*$ is monotone if $\langle x_0 - x_1, x_0^* - x_1^* \rangle \ge 0$ whenever $x_0^* \in T(x_0)$ and $x_1^* \in T(x_1)$. It is maximal monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other monotone map $T' : E \to E^*$.

The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} \{\langle x, x^*\rangle - f(x)\}$, a function on $E^*$; its subdifferential $\partial f^*$ maps $E^*$ into $E^{**}$. Finally $j(x) = \tfrac12 \|x\|^2$.

In Lean these are ProperConvex f, subdiff f, IsMonotoneOp T, IsMaximalMonotone T, conj f and halfSqNorm, all stated over an arbitrary real normed space V so that they apply equally to $E$ and to $E^*$.

Formalization targets

Goal: Theorem A (p. 210)

No reflexivity, inner product or finite dimension is assumed.

Milestones, in attack order

1. (2.2) Fenchel–Young: $f(x) + f^*(x^*) \ge \langle x, x^* \rangle$, with equality iff $x^* \in \partial f(x)$.
2. §2, p. 210. $f^*$ is a weak* lower semicontinuous (hence strongly lower semicontinuous) proper convex function on $E^*$.
3. §2, p. 211. The restriction of $f^{**}$ to $E$ is $f$.
4. Proposition 1. $x^{**} \in \partial f^*(x^*)$ iff there are a net $x_i^* \to x^*$ in norm and a bounded net $x_i \to x^{**}$ weak**, on one directed index set, with $x_i^* \in \partial f(x_i)$.
5. (3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for all $x \in E$.
6. §3, p. 213. $(f + j)^*$ is finite and continuous throughout $E^*$.
7. §3, p. 213 (Minty). On any real Banach space, a convex function that is finite and continuous everywhere has a maximal monotone subdifferential.

Significance

Theorem A places every closed proper convex function in the maximal monotone class, in every real Banach space. Downstream, it is what allows convex minimization problems to be treated by the general theory: surjectivity of $\partial f + \lambda J$ (with $J$ the duality map) in reflexive spaces, existence for evolution equations governed by subdifferentials, the definition of resolvents and proximal maps, and the convergence of proximal-point and splitting methods for convex problems. Proposition 1 is of independent interest: in a nonreflexive space $\partial f^*$ is not the inverse of $\partial f$, but it is still completely determined by $\partial f$ through bounded weak** nets.

The theorem is classical and fully proved in the literature. What this mission adds is a machine-checked proof of the nonreflexive Banach-space statement, together with the infrastructure it needs: extended-real-valued proper convex functions, the subdifferential and the conjugate on a normed space and its dual, monotone and maximal monotone operators, and the Fenchel–Moreau identity $f^{**}|_E = f$. None of these exists in Mathlib at the pinned revision, and Mathlib contains no statement of Theorem A, in Hilbert or in Banach spaces.

Difficulty

Monotonicity of $\partial f$ follows in two lines from the definition; the whole difficulty is maximality. In a Hilbert space the standard argument solves $x + \partial f(x) \ni y$ by minimizing $f + \tfrac12\|\cdot - y\|^2$ and uses the identification of $E$ with $E^*$; in a general Banach space there is no such identification, and minimizers need not exist without reflexivity. The 1966 argument tried to approximate subgradients of $f$ at nearby points, and it failed because those subgradients could become unbounded as the approximation was refined. Any argument that passes through the dual meets a second obstacle: $\partial f^*$ takes values in the bidual $E^{**}$, which is strictly larger than $E$ when $E$ is not reflexive, so $\partial f^*$ is not the inverse of $\partial f$. Relating the two is the content of Proposition 1, and its necessity half requires approximation results well beyond the definitions.

Formalization scope

Lean representation and committed conventions:

• $E$ is a real Banach space: NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E. $E^*$ is StrongDual ℝ E with the operator norm; the pairing $\langle x, x^*\rangle$ is x' x; $E^{**}$ is StrongDual ℝ (StrongDual ℝ E) and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual ℝ E.
• The value set $(-\infty,+\infty]$ is EReal with the clause "never $\bot$". Properness also requires some value $\ne \top$. Convexity is the paper's inequality for $0 < \lambda < 1$, computed in EReal.
• Multivalued maps are V → Set (StrongDual ℝ V). Maximality is graph inclusion, quantified over every monotone T', not only over subdifferentials.
• The conjugate is an EReal supremum over all of $V$; the biconjugate is conj (conj f) on the bidual.
• (2.2) is stated as $\langle x, x^*\rangle \le f(x) + f^*(x^*)$ with the equality case, avoiding EReal subtraction.
• Weak* lower semicontinuity of $f^*$ is lower semicontinuity on WeakDual ℝ E.
• In Proposition 1 a net is a map from a nonempty, directed, partially ordered index type (in the universe of $E$), with convergence along atTop. Weak** convergence is pointwise convergence on $E^*$ of the canonical images, which is convergence in the weak topology induced on $E^{**}$ by $E^*$. Boundedness is a uniform norm bound.
• (3.1) reads the printed $\partial(f+j)$ as $\partial(f+j)(x)$; the right side is the pointwise (Minkowski) set sum.
• "Finite and continuous" for $(f+j)^*$ is the existence of a continuous real-valued $h$ on $E^*$ equal to it everywhere.
• Minty's case is stated for an arbitrary real Banach space $V$, because the proof applies it on $E^*$.

A trivializing formalization is ruled out: properness excludes $f \equiv +\infty$ (whose empty subdifferential is monotone but not maximal) and $-\infty$ values, maximality ranges over all monotone operators, and the index set in Proposition 1 is nonempty and directed so that no convergence statement holds vacuously.

Infrastructure needed and reusable beyond this mission: extended-real convex analysis on normed spaces (conjugates, the Fenchel–Moreau theorem via Hahn–Banach separation, lower semicontinuity in the weak and weak* topologies), subdifferential calculus for a sum with a continuous function, nets and weak** approximation in the bidual (Goldstine-type arguments), and the Brøndsted–Rockafellar approximation of ε-subgradients. Contributions are welcome at every milestone; the definitions layer and milestones 1–3 are the natural starting points.

Selected references

• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific Journal of Mathematics 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific Journal of Mathematics 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
• G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific Journal of Mathematics 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• A. Brøndsted and R. T. Rockafellar, On the subdifferentiability of convex functions, Proceedings of the American Mathematical Society 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8

Motivation

Many problems in signal processing, statistics and operations research ask to minimize a sum $\Theta = \Phi + \Psi$ of a nonsmooth convex term $\Phi$ (a constraint indicator, an $\ell^1$ penalty) and a smooth term $\Psi$. The standard method is the forward-backward (proximal-gradient) algorithm: an explicit gradient step on $\Psi$ followed by a proximal step on $\Phi$. Its classical convergence theory requires $\Psi$ to be convex and the step size to stay below $2/L_\Psi$, where $L_\Psi$ is the Lipschitz constant of $\nabla\Psi$.

Attouch, Peypouquet and Redont (authors' manuscript of SIAM J. Optim. 24 (2014)) derive an inertial forward-backward algorithm (IFB) as a time discretization of a second-order dissipative dynamical system with Hessian-driven damping. The added inertial terms cost essentially nothing to compute, yet they allow step sizes beyond $2/L_\Psi$ and a smooth part $\Psi$ that is not convex, provided the sum $\Theta$ is.

Timeline of the relevant results:

• Heavy-ball-with-friction methods, the inertial discretizations of $\ddot u + \alpha\dot u + \nabla\Phi(u) = 0$, were introduced by Polyak (1964) and developed by Alvarez and Attouch (2001) for proximal schemes.
• Hessian-driven damping for one potential: Alvarez, Attouch, Bolte and Redont (2002); for a nonsmooth potential plus a smooth one, the continuous dynamics underlying (IFB): Attouch, Maingé and Redont (2012).
• The discrete algorithm (IFB) and its weak convergence in Hilbert spaces: Attouch, Peypouquet and Redont (2014), the paper of this mission.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. Let $\Phi : H \to \mathbb R\cup\{+\infty\}$ and $\Psi : H \to \mathbb R$, and write $\Theta = \Phi + \Psi$ and $\mathcal S = \operatorname{Argmin}\Theta$. A vector $g$ is a subgradient of $\Phi$ at $u$, written $g \in \partial\Phi(u)$, if $\Phi(u) < +\infty$ and $\Phi(u) + \langle g, v - u\rangle \le \Phi(v)$ for all $v$.

Hypothesis H fixes positive constants $L_\Psi$, $a$, $b$ and a step size $\lambda$ with:

• $H_\Phi$: $\Phi$ is proper, lower semicontinuous and convex;
• $H_\Psi$: $\Psi$ is differentiable and $\nabla\Psi$ is $L_\Psi$-Lipschitz;
• $H_\lambda$: $0 < \lambda < \Lambda = \min\{1/a,\ 2(a+b)/(bL_\Psi)\}$;
• $H_\Theta$: $\Theta$ is convex and bounded from below.

Algorithm (IFB). From any $(u_0, y_0) \in H \times H$, compute for $k \ge 0$

A sequence $u_k$ converges weakly to $p$, written $u_k \rightharpoonup p$, if $\langle u_k, v\rangle \to \langle p, v\rangle$ for every $v \in H$. The analysis uses the velocity $\xi_k = u_k - u_{k-1}$, the energy $E_k = \Theta(u_k) + \gamma\|\xi_k\|^2$ with $\gamma = (1-a\lambda)/(2b\lambda^2)$, and two auxiliary real sequences $G_k(q)$ and $F_k(q)$, defined from $u$, $y$ and a reference point $q$ by (17) and (18) of the paper.

Formalization targets

Goal: Theorem 1

Under Hypothesis H, for every sequence generated by (IFB),

if $\mathcal S \ne \emptyset$ and one of (i) $\mathcal S$ is a singleton, (ii) $\Phi$ is differentiable with weak-to-weak sequentially continuous gradient, (iii) $\nabla\Psi$ is weak-to-weak sequentially continuous, (iv) $\Psi$ is convex, holds, then

and if $\mathcal S = \emptyset$, then $\|u_k\| \to +\infty$.

Milestones

In the order of the paper's argument: Proposition 2 (energy decrease, $\sum\|\xi_k\|^2 < \infty$); Proposition 3 (the identity and inequality (19) for $F_k(q)$); Proposition 4 ($G_k(q)$ is bounded above for $q\in\operatorname{dom}\Phi$); the lower bound (28) on $F_k(q)$; Lemma 5 (a real-sequence lemma); Proposition 6 ($\Theta(u_k)\to\inf\Theta$, weak cluster points lie in $\mathcal S$); Lemma 7 (a boundedness lemma); Proposition 8 (boundedness of $(u_k)$ and convergence of $F_k(q)$ when $\mathcal S \ne\emptyset$).

Significance

The result gives convergence of a forward-backward type method under a step-size bound $\Lambda$ that can be made arbitrarily large by choosing $a$ small, and for a smooth term $\Psi$ that need not be convex. The special case $\Phi = \delta_C$ (indicator of a closed convex set) yields an inertial gradient-projection method, and the paper applies the theorem to feasibility problems, the CQ algorithm, Pareto fronts and $\ell^1$ signal recovery.

The theorem is proved in the paper; to our knowledge it is not formalized anywhere. A complete formalization would provide a machine-checked Liapunov analysis of an inertial proximal method in an infinite-dimensional Hilbert space, including the passage from a minimizing sequence to weak convergence. The milestones Proposition 2, 3 and 8 are energy estimates that also underlie other inertial and proximal schemes.

Difficulty

The energy $E_k$ controls the values $\Theta(u_k)$ and the velocities $\xi_k$, but not the iterates themselves. The first idea, proving that $\|u_k - q\|$ is nonincreasing for every $q \in \mathcal S$ (Fejér monotonicity, the standard route for the classical forward-backward method), does not come out of the energy estimates for (IFB): the inertial variable $y_k$ couples consecutive steps, and the distance to a minimizer is not a Liapunov function. The paper's replacement, the sequence $F_k(q)$, carries the auxiliary sum $G_k(q)$, whose upper bound already requires the full Hypothesis H. Because $H$ is infinite-dimensional, bounded sequences have only weakly convergent subsequences, so the minimizing property has to pass through weak lower semicontinuity of $\Theta$, and the final step, uniqueness of the weak cluster point, needs a separate argument in each of the cases (i)–(iv) together with Opial's lemma, which is not in Mathlib.

Formalization scope

• $H$ is a general real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); nothing is specialized to finite dimension.
• $\Phi$ and $\Theta$ take values in EReal. Properness excludes $-\infty$. Convexity of an extended-valued function is convexity of its epigraph in $H\times\mathbb R$, because Mathlib's ConvexOn needs a scalar action that EReal lacks. The subgradient predicate requires $\Phi(u) < +\infty$, so $\partial\Phi(u) = \emptyset$ off $\operatorname{dom}\Phi$.
• (IFB) is encoded as the subgradient inclusion, not through the proximity operator. Weak convergence is convergence of all inner products $\langle u_k, v\rangle$; weak cluster points are weak limits along strictly increasing subsequences.
• $L_\Psi > 0$ is assumed (harmless: a Lipschitz gradient is Lipschitz with every larger constant). The step size $\lambda$ is written lam.
• $\xi_k$, $z_k$, $E_k$, $G_k$, $F_k$ are defined on all natural indices, and each statement quantifies $k \ge 1$ (or $k \ge 2$ for $G_k$) as the paper does. Energies and values are never truncated to real numbers, so no statement becomes true through the convention EReal.toReal ⊤ = 0.
• Deviation from the printed text: Proposition 4 is printed under $H_\Phi$ and $H_\Psi$ only, but its proof invokes Proposition 2, which needs all of Hypothesis H, and the printed statement is false for step sizes above $\Lambda$ (e.g. $H=\mathbb R$, $\Phi = x^2/2$, $\Psi = 3x^2/2$, $a=2$, $b=0.02$, $\lambda = 10$). The milestone is stated under the full Hypothesis H.
• A formalization in which $\partial\Phi(u)$ is nonempty at points of infinite value, in which the energy is converted to a real number, or in which Hypothesis H cannot be satisfied, would make these statements trivial or vacuous, and is ruled out by the definitions above.

A complete development needs Opial's lemma, weak sequential compactness of bounded sets in Hilbert space, weak lower semicontinuity of lower semicontinuous convex functions, the descent lemma for functions with Lipschitz gradient, and monotonicity of the subdifferential. These are reusable well beyond this mission; contributions of any of them, and of the milestones in any order, are welcome.

Selected references

• H. Attouch, J. Peypouquet, P. Redont, A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization, SIAM J. Optim. 24(1), 2014 (statements cited from the authors' manuscript of Aug 2013). https://doi.org/10.1137/130910294
• H. Attouch, P.-E. Maingé, P. Redont, A second-order differential system with Hessian-driven damping; application to non-elastic shock laws, Differential Equations and Applications 4(1), 2012. https://doi.org/10.7153/dea-04-02
• F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Analysis 9, 2001. https://doi.org/10.1023/A:1011253113155
• F. Alvarez, H. Attouch, J. Bolte, P. Redont, A second-order gradient-like dissipative dynamical system with Hessian-driven damping, J. Math. Pures Appl. 81(8), 2002. https://doi.org/10.1016/S0021-7824(01)01253-3
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0

Motivation

A robust Markov decision process replaces the unknown transition probabilities of an MDP by sets of plausible values and optimises against the worst case. Nilim and El Ghaoui (Oper. Res. 53 (2005)) showed that, when the uncertainty is rectangular (each row of each transition matrix varies independently in its own set), the robust problem is solved by a Bellman-type recursion. Each step of that recursion needs, for every state and action, the value of an inner problem: the largest expectation of the next-stage value vector over the uncertainty set of one transition row. The recursion is only as tractable as this inner problem.

The paper studies several uncertainty models built from statistical estimates of the transition rows. In the entropy model the uncertain row is any distribution within a prescribed Kullback–Leibler divergence of a nominal distribution. For this model the paper reduces the inner problem to the minimisation of a scalar convex function, which is then solved by bisection. Iyengar (Math. Oper. Res. 30 (2005)) obtained the same robust recursion independently, and the same scalar reduction is the basic computation in later KL-constrained distributionally robust optimisation. This mission formalizes that reduction and the properties of the scalar function that the paper derives from it.

Setting

Let $n\ge 1$ and let $\Delta_n=\{p\in\mathbb R^n : p\ge 0,\ \sum_j p(j)=1\}$ be the probability simplex. For $p,q\in\mathbb R^n$ the Kullback–Leibler divergence is

with $0\log 0=0$. Fix a nominal distribution $q\in\Delta_n$ with $q(j)>0$ for every $j$, and a level $\beta>0$. The entropy uncertainty set is

For a vector $v\in\mathbb R^n$ (in the MDP, the value function of the next stage), the inner problem (17) is

The paper's scalar dual function (47) is, for $\lambda>0$,

Write $v_{\max}=\max_j v(j)$ and $Q(v)=\sum_{j:\,v(j)=v_{\max}}q(j)$, the $q$-mass of the maximisers of $v$. The tilted distribution at $\lambda>0$ is $p^*(j)=q(j)e^{v(j)/\lambda}/\sum_i q(i)e^{v(i)/\lambda}$.

In Lean, vectors are Fin n → ℝ, $\Delta_n$ is stdSimplex ℝ (Fin n), and $D$, $\mathcal P$, $\sigma$, $p^*$, $v_{\max}$, $Q(v)$ are klDiv, klBall, dualFn, tiltedDist, vmax, maxMass in the namespace RobustMDP.EntropyInner.

Formalization targets

Goal: the dual of the inner problem (§6.2, Eq. (47), p. 791)

with the maximum attained. This is kl_ball_inner_problem_dual. It holds for every $n$, every $v$, every $q>0$ in $\Delta_n$ and every $\beta>0$.

Milestones

1. §6.1: $\max_{p\in\Delta_n}D(p\|q)=\max_i(-\log q_i)$, and for $\beta\ge\max_i(-\log q_i)$ the set $\mathcal P$ is all of $\Delta_n$ and the inner value is $v_{\max}$.
2. Eq. (48): $q^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambda$ for $\lambda>0$.
3. §6.2, the optimal distribution: $p^{\mathsf T}v-\lambda D(p\|q)\le\lambda\log\sum_j q(j)e^{v(j)/\lambda}$ on $\Delta_n$, with equality at $p^*$.
4. §6.2, elimination of $\mu$: $\min_{\mu}\big[\mu+\beta\lambda+\lambda\sum_j q(j)e^{(v(j)-\mu)/\lambda-1}\big]=\sigma(\lambda)$.
5. Eq. (49): $\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)$ as $\lambda\to0^+$.
6. Eq. (50): $\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)$ as $\lambda\to\infty$.
7. §6.3: if $\beta\ge-\log Q(v)$, then $\inf_{\lambda>0}\sigma=v_{\max}$ and the inner value is $v_{\max}$.

Significance

The goal turns an $n$-dimensional optimisation over a nonpolyhedral convex set into a one-dimensional convex minimisation whose objective costs $O(n)$ to evaluate. Combined with the bisection bracket from (48) and the behaviour at $0$ from (49), it gives the paper's $O(n\log(v_{\max}/\delta))$ cost per inner problem (§6.4), and hence the per-step cost of the robust Bellman recursion under entropy uncertainty. Milestone 7 identifies exactly when the uncertainty set is large enough that the robust step ignores the nominal model; unlike the cruder threshold of milestone 1, it depends on $v$.

The result is proved in the paper modulo "standard duality arguments". The paper gives no proof of the duality step itself, and its expansions (49)–(50) are proved only in outline in Appendix C. No formal proof of any of these statements is known to exist; Mathlib has the measure-theoretic Donsker–Varadhan ingredients but not the finite, constrained dual stated here. The mission produces a machine-checked version of the whole chain, with the attainment questions (which side is a max, which is only an infimum) settled explicitly.

Difficulty

The inequality $\max_{\mathcal P}p^{\mathsf T}v\le\sigma(\lambda)$ for every $\lambda>0$ is the routine half. The obstacle is the reverse inequality. The paper appeals to Lagrangian strong duality under a Slater condition, but the Lagrangian dual function equals $\sigma(\lambda)$ only for $\lambda>0$; at $\lambda=0$ it is $v_{\max}$, and the dual infimum may be approached only as $\lambda\to0^+$. A proof that looks for a minimiser $\lambda^*>0$ and a matching primal point $p^*$ fails in precisely the regime $\beta\ge-\log Q(v)$ of milestone 7, where no such $\lambda^*$ exists and the primal optimum sits on the face of the simplex spanned by the maximisers of $v$. The strong-duality argument must also handle the boundary of $\Delta_n$, where $D(\cdot\|q)$ is not differentiable.

Formalization scope

• Vectors are Fin n → ℝ; $\Delta_n$ is stdSimplex ℝ (Fin n). $D(p\|q)$ is a local finite sum with Lean's $\log 0=0$, which gives $0\log0=0$; Mathlib's measure-valued InformationTheory.klDiv is not used.
• Standing hypotheses in every theorem: $q\in\Delta_n$, $q(j)>0$ for all $j$, and $\beta>0$, as in §6.1. No restriction on $v$ is imposed; the "without loss of generality $v\ge0$" of the paper's §5 is not assumed here.
• The primal "max" is stated with IsGreatest (attained, since the KL ball is compact). The paper's "$\min_{\lambda>0}\sigma(\lambda)$" is an infimum, stated with IsGLB over $\{\sigma(\lambda):\lambda>0\}$: it is not attained when $\beta\ge-\log Q(v)$.
• dualFn is total in $\lambda$ and equals $0$ at $\lambda=0$ (division by zero), not the paper's $\sigma(0)=v_{\max}$. Every statement uses $\lambda>0$; the value at $0$ appears as the one-sided limit of (49). Accordingly (48) is stated for $\lambda>0$.
• $v_{\max}$ is ⨆ j, v j, the attained maximum over the finite nonempty index set; $\max_i(-\log q_i)$ likewise.
• (49) is stated as a limit along 𝓝[>] 0 together with a little-o remainder; (50) as a limit along atTop.
• Milestone 7 uses the non-strict condition $\beta\ge-\log Q(v)$ of the paper's first sentence, which contains the strict version of its second.
• Trivializing formalizations are excluded: the statements quantify over all $n$, $v$ and $q$, so a constant $v$, $n=1$, or the whole-simplex case of milestone 1 does not discharge the goal.

Useful infrastructure: a finite Gibbs variational inequality, compactness of the KL ball, and convexity and one-sided asymptotics of the log-sum-exp function in the temperature parameter. These are reusable for any KL-constrained robust optimisation mission. Proofs of the milestones, alternative proofs of the goal that avoid a general strong-duality theorem, and the sharper $O(\lambda e^{-t/\lambda})$ remainder of Appendix C are all welcome.

Selected references

• A. Nilim and L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• M. D. Donsker and S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, I, Communications on Pure and Applied Mathematics 28(1):1–47, 1975. https://doi.org/10.1002/cpa.3160280102

Motivation

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$, impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$. The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$: iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$, and polytopes are replaced by the convex cones they generate.

• A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$, $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$.
• The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$.
• A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$. The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$; it is the cone over the unit cube.
• For a convex cone $K$, $K^\circ$ is the cone spanned by the 0–1 vectors in $K$. For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$, the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

1. $Y$ is symmetric;
2. $y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
3. $u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$.

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$, where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$, and its iterates are $N^0(K) = K$, $N^t(K) = N(N^{t-1}(K))$.

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$, the hyperplanes through the two opposite facets of $Q$ in direction $i$.

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$,

The statement is uniform in $n$ and in $K$: no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

1. Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$: $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$.
2. Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$,