Optimization

Motivation

Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.

Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy $y(b) = Pb + q$, whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.

Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of $m+1$ affinely independent points of $\mathbb R^m_+$. Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.

Setting

Let $A \in \mathbb R^{m\times n_1}$, $B \in \mathbb R^{m\times n_2}$, $c \in \mathbb R^{n_1}_+$, $d \in \mathbb R^{n_2}_+$ and let $\mathcal U \subseteq \mathbb R^m_+$ be an uncertainty set. The problem $\Pi_{\mathrm{Adapt}}(\mathcal U)$ is

$$z_{\mathrm{Adapt}}(\mathcal U)=\min\ c^{T}x+\max_{b\in\mathcal U} d^{T}y(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U .$$

Here $x$ is the first-stage decision and $y : \mathcal U \to \mathbb R^{n_2}$ is the second-stage policy; all inequalities between vectors are componentwise. The value $z_{\mathrm{Aff}}(\mathcal U)$ is the same minimum restricted to affine policies $y(b) = Pb + q$ with $P \in \mathbb R^{n_2\times m}$ and $q \in \mathbb R^{n_2}$; an affine policy must still satisfy $Pb + q \ge 0$ for every $b \in \mathcal U$. Always $z_{\mathrm{Adapt}}(\mathcal U) \le z_{\mathrm{Aff}}(\mathcal U)$.

The instance $\mathcal I$ of (6) is defined for $\delta > 0$ and an even integer $m > 200/\delta^2$. It has $n_1 = n_2 = m$, $c = 0$, $d = (1,\dots,1)^T$, $A = 0$, and

$$B_{ij}=\begin{cases}1,& i=j,\\ 1/\sqrt m,& i\ne j,\end{cases}\qquad \mathcal U=\operatorname{conv}\{b^0,b^1,\dots,b^{m+2}\},$$

where $b^0 = 0$, $b^j = e_j$ is the $j$-th unit vector for $j = 1,\dots,m$, $b^{m+1}$ has entries $1/\sqrt m$ in its first $m/2$ coordinates and $0$ in the others, and $b^{m+2}$ has $0$ in its first $m/2$ coordinates and $1/\sqrt m$ in the others. Thus $\mathcal U$ is generated by $m+2$ nonzero points. The last two are also extreme points when $m\ge 6$; for $m=2$ or $4$ they lie in the convex hull of $0,e_1,\dots,e_m$.

For a permutation $\tau$ of $\{1,\dots,m\}$, write $x^\tau = (x_{\tau(1)},\dots,x_{\tau(m)})$. A set $U$ is permutation-invariant with respect to $\tau$ if $x \in U \iff x^\tau \in U$ (Definition 2), and $\Gamma$ is the set (10) of permutations with $i \le m/2 \iff \tau(i) \le m/2$.

Formalization targets

Goal: Theorem 2

$$z_{\mathrm{Aff}}(\mathcal U)>(2-\delta)\cdot z_{\mathrm{Adapt}}(\mathcal U)\qquad\text{for the instance }\mathcal I\text{ of (6), every }\delta>0\text{ and every even }m>200/\delta^2 .$$

Milestones

1. Lemma 1. On $\mathcal I$ there is a feasible fully adaptable solution with worst-case cost $1$, so $z_{\mathrm{Adapt}}(\mathcal U) \le 1$.
2. Lemma 2. The set $\mathcal U$ of (6) is permutation-invariant with respect to every $\tau \in \Gamma$.
3. Lemma 3. There is an optimal affine solution $\hat y(b) = \hat Pb + \hat q$ whose intercept is constant: $\hat q_i = \hat q_j$ for all $i, j$.
4. First Claim of the proof of Theorem 2. For any feasible affine solution with intercept $\hat q \equiv \beta$ and worst-case cost at most $2-\delta$: $\beta \le (2-\delta)/m$.
5. Second Claim. Under the same assumption, $\hat P_{jj} \ge 1 - 2/\sqrt m - 2/m$ for every $j$.
6. Third Claim. Under the same assumption, $\hat P_{ij} \ge -(2-\delta)/m$ for all $i, j$.

Significance

Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach $2$. The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to $m^{1/2-\delta}$ for sets with polynomially many extreme points and prove a matching $O(\sqrt m)$ upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.

The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values $z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$, and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.

Difficulty

The upper bound $z_{\mathrm{Adapt}} \le 1$ requires a feasible policy, which can be written down. The lower bound on $z_{\mathrm{Aff}}$ is a statement about all affine policies, an $m^2 + m$ dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of $\Gamma$ and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most $2-\delta$ yields only $z_{\mathrm{Aff}} \ge 2-\delta$, not the strict inequality.

Formalization scope

Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, $Bx$ is B *ᵥ x and $d^Ty$ is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate $i$ is index $i - 1$, so "$i \le m/2$" is (i : ℕ) < m / 2, with natural-number division (exact since $m$ is even). $x^\tau$ is x ∘ τ for τ : Equiv.Perm (Fin m).

$z_{\mathrm{Adapt}}$ and $z_{\mathrm{Aff}}$ are the infima of the sets of real numbers $t$ for which some feasible (respectively feasible affine) solution satisfies $c^Tx + d^Ty(b) \le t$ for all $b \in \mathcal U$. This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value $0$, which is why Lemma 1 also asserts the existence of the feasible solution of cost $1$. Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on $\mathcal U$, as in (1).

The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional $\mathcal U \subseteq \mathbb R^m_+$, feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: $\delta > 0$, $m$ even and $m > 200/\delta^2$. For $\delta \ge 2$ the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most $2-\delta$, which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis $m > 200/\delta^2$. Definition 2 prints "$x \in P \iff x^\tau \in P$"; the formalization reads $P$ as the set $U$.

Replacing $z_{\mathrm{Aff}}$ by the cost of one particular affine policy, stating the goal with $\ge$, or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.

A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in $(x, P, q)$ with infinitely many constraints indexed by $\mathcal U$, reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with $\sqrt m$. Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming Ser. A (online first 2011; received 31 Oct 2009, accepted 17 Jan 2011). https://doi.org/10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Mathematics of Operations Research 35 (2010) 363–394. https://doi.org/10.1287/moor.1100.0444

Motivation

Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision $x$ is fixed before an uncertain parameter is revealed, and a second-stage decision $y(b)$ is chosen after the parameter $b$ is observed, so that the second stage may depend on $b$ arbitrarily. The objective is the worst case over an uncertainty set $\mathcal U$ of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.

Optimizing over all functions $y(\cdot)$ is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in $b$ with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) $y(b)=Pb+q$; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.

Timeline of the relevant results:

• 2004. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduce affinely adjustable robust counterparts and show that the best affine policy is tractable for many uncertainty sets (doi:10.1007/s10107-003-0454-y).
• 2010. Bertsimas, Iancu and Parrilo prove that affine policies are optimal for a class of multistage robust problems with one-dimensional uncertainty per stage and box uncertainty sets (doi:10.1287/moor.1100.0444).
• 2012. Bertsimas and Goyal, the source of this mission, prove that an affine policy is optimal for model (1) whenever $\mathcal U$ is a simplex (Theorem 1), and show that this exactness breaks down for slightly larger sets (doi:10.1007/s10107-011-0444-4).

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$ and $d\in\mathbb R^{n_2}_+$. The problem $\Pi_{Adapt}(\mathcal U)$ of model (1) is

$$z_{Adapt}(\mathcal U)=\min\ c^Tx+\max_{b\in\mathcal U}d^Ty(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U,$$

where inequalities between vectors are componentwise. A pair $(x,y)$ satisfying the constraints is feasible; its worst-case cost is $c^Tx+\max_{b\in\mathcal U}d^Ty(b)$. A feasible pair is optimal when its worst-case cost equals $z_{Adapt}(\mathcal U)$, and an affine policy is a second stage of the form $y(b)=Pb+q$ with $P\in\mathbb R^{n_2\times m}$, $q\in\mathbb R^{n_2}$, still required to be nonnegative on $\mathcal U$. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine policies.

A simplex in $\mathbb R^m$ is the convex hull

$$\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$$

of $m+1$ affinely independent points, that is, points for which $b^1-b^{m+1},\dots,b^m-b^{m+1}$ are linearly independent. The proof works with the $m\times m$ matrix $Q=[(b^1-b^{m+1})\cdots(b^m-b^{m+1})]$, the matrix $Y=[(y^*(b^1)-y^*(b^{m+1}))\cdots(y^*(b^m)-y^*(b^{m+1}))]$ of display (2), and the affine rule $\tilde y(b)=YQ^{-1}(b-b^{m+1})+y^*(b^{m+1})$. In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.

Formalization targets

Goal: Theorem 1

If $\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$ with affinely independent $b^j\in\mathbb R^m_+$ and $\Pi_{Adapt}(\mathcal U)$ is feasible, then there exist $\hat x$, $P\in\mathbb R^{n_2\times m}$ and $q\in\mathbb R^{n_2}$ such that

$$(\hat x,\ \hat y),\qquad \hat y(b)=Pb+q\ \ (b\in\mathcal U),$$

is an optimal solution of $\Pi_{Adapt}(\mathcal U)$, optimal among all (not only affine) two-stage solutions. In particular $z_{Aff}(\mathcal U)=z_{Adapt}(\mathcal U)$.

Milestones

The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:

1. $Q$ is invertible (PDF p. 6).
2. For $b=\sum_j\alpha_jb^j$ with $\sum_j\alpha_j=1$: $Q^{-1}(b-b^{m+1})=(\alpha_1,\dots,\alpha_m)^T$ (PDF p. 6).
3. $\tilde y\big(\sum_j\alpha_jb^j\big)=\sum_j\alpha_j\,y^*(b^j)$ (PDF pp. 6–7).
4. Displays (3)–(5): for any feasible $(x^*,y^*)$, the pair $(x^*,\tilde y)$ is feasible and every bound on the worst-case cost of $(x^*,y^*)$ also bounds that of $(x^*,\tilde y)$ (PDF p. 7).

Significance

The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix $A$ and $B$ and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with $m+3$ extreme points the best affine policy can already be worse by a factor $2-\delta$, and that on sets with exponentially many extreme points the gap can be $\Omega(m^{1/2-\delta})$; Section 6 uses a dominating simplex, on which affine policies are exact, to build an $O(\sqrt m)$-approximation for general $\mathcal U$. The theorem also says that on a simplex the whole adaptive problem reduces to $m+1$ scenario copies of a linear program.

Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.

Difficulty

Two steps are not routine to formalize. First, the paper starts from "an optimal solution $x^*,y^*(b)$", that is, it assumes the minimum in (1) is attained. Over arbitrary functions $y(\cdot)$ this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of $m+1$ points to invertibility of the $m\times m$ matrix $Q$, and the identity $Q^{-1}(b-b^{m+1})=\alpha$ requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing $z_{Aff}$ and $z_{Adapt}$ as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.

Formalization scope

Vectors in $\mathbb R^m$ are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at $1$, Lean's at $0$: $b^j$ is v (j-1) and $b^{m+1}$ is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of $\mathcal U$ is the hypothesis that all $m+1$ vertices are nonnegative (the page writes $j=1,\dots,m$, a slip for $m+1$). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values $z_{Adapt}$ and $z_{Aff}$ are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.

The goal must not be replaced by $z_{Aff}(\mathcal U)\le z_{Adapt}(\mathcal U)$, by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention $Q$, $Y$ or the interpolant.

A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. doi:10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. doi:10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010. doi:10.1287/moor.1100.0444
• A. Bemporad, F. Borrelli, M. Morari, Min–max control of constrained uncertain discrete-time linear systems, IEEE Trans. Autom. Control 48(9), 1600–1606, 2003. doi:10.1109/TAC.2003.816984

Motivation

Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy $\varepsilon$ after $O(L^2 R^2/\varepsilon^2)$ iterations, where $L$ and $R$ are measured in the Euclidean norm; on the simplex this hides a factor of order $n$ in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to $\ln n$.

Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance $B_\psi$. This viewpoint gives a short convergence proof, and with the entropy as $\psi$ it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.

Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a $O(\sqrt{\ln n}/\sqrt k)$ rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the $\ell_p$ potential $\tfrac12\|x\|_p^2$, $p = 1 + 1/\ln n$, whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same $\sqrt{2\ln n}\,L_f/\sqrt k$ rate with a closed-form update.

Setting

Let $E$ be $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and $\|z\|_* = \max\{\langle x, z\rangle : \|x\| \le 1\}$ the dual norm. The problem is $\min\{f(x) : x \in X\}$ under Assumption A: $X$ is closed and convex; $f$ is convex on $X$ and Lipschitz there, $|f(x) - f(y)| \le L_f\|x - y\|$; $f$ has a minimiser $x^* \in X$; and a subgradient $f'(x)$ can be computed at every $x \in X$.

Let $\psi : X \to \mathbb R$ be strongly convex with parameter $\sigma > 0$ and differentiable. The distance-like function (3.10) is

$$B_\psi(x, y) = \psi(x) - \psi(y) - \langle x - y, \nabla\psi(y)\rangle .$$

The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from $x^1$ and sets, with step sizes $t_k > 0$,

$$x^{k+1} = \operatorname*{argmin}_{x \in X}\Big\{\langle x, f'(x^k)\rangle + \tfrac{1}{t_k} B_\psi(x, x^k)\Big\}.$$

With $\psi = \tfrac12\|\cdot\|_2^2$ this is the projected subgradient method.

On the unit simplex $\Delta = \{x \in \mathbb R^n : x \ge 0,\ \sum_j x_j = 1\}$ take the entropy $\psi_e(x) = \sum_j x_j \ln x_j$ (5.27), with $0\ln0 = 0$. SANP becomes the entropic descent algorithm (EDA):

$$x^{k+1}_j = \frac{x^k_j\,e^{-t_k f'_j(x^k)}}{\sum_{i=1}^n x^k_i\,e^{-t_k f'_i(x^k)}} .$$

Formalization targets

Goal: Theorem 5.1 (p. 174)

If $f$ is convex and $L_f$-Lipschitz on $\Delta$ for $\|\cdot\|_1$, with subgradients satisfying $\|f'(x)\|_\infty \le L_f$, and the EDA is started at $x^1 = n^{-1}e$ with step $t = \sqrt{2\ln n}/(L_f\sqrt k)$ for a horizon $k \ge 1$, then

$$\min_{1 \le s \le k} f(x^s) - \min_{x \in \Delta} f(x) \le \frac{\sqrt{2\ln n}\;L_f}{\sqrt k}.$$

The general estimate: Theorems 4.1 and 4.2 (pp. 171–172)

For any norm, any $\sigma$-strongly convex $\psi$ and any SANP run,

$$\min_{1 \le s \le k} f(x^s) - \min_X f \le \frac{B_\psi(x^*, x^1) + (2\sigma)^{-1}\sum_{s=1}^k t_s^2\|f'(x^s)\|_*^2}{\sum_{s=1}^k t_s},$$

and with the optimal constant step this gives $L_f\sqrt{2B_\psi(x^*, x^1)/\sigma}/\sqrt k$.

The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound $B_\psi \ge \tfrac\sigma2\|\cdot\|^2$, the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on $B_\psi(x^*, x^1)$; then for the simplex, the 1-strong convexity of $\psi_e$ for $\|\cdot\|_1$ (Proposition 5.1(a), Remark 5.1), the bound $B_{\psi_e}(x^*, n^{-1}e) \le \ln n$ (Proposition 5.1(c)), and the identification of the EDA with SANP.

Significance

The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy $\varepsilon$ in $O(L_f^2\ln n/\varepsilon^2)$ iterations, with $L_f$ measured in the $\ell_\infty$ dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.

Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the $\ell_1$ geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.

Difficulty

The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in $\mathbb R^n$). The bound $B_\psi(u, y) \ge \tfrac\sigma2\|u - y\|^2$ must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to $\|\cdot\|_1$ is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over $\Delta$, which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from $\ell_\infty$ to $\ell_2$ and the strong convexity constant of the entropy, and loses the $\ln n$ rate.

Formalization scope

Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, $\langle u, f'(x)\rangle$ is its value at $u$, and $\|\cdot\|_*$ is the operator norm. $\nabla\psi$ is the Fréchet derivative. Iterates are indexed from $1$. A SANP run is a predicate on sequences: each step size is positive, each iterate lies in $X$, $\psi$ is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces "$X$ has nonempty interior" and "$x^1 \in \operatorname{int} X$". Section 5 works on $\mathbb R^n$ as functions $\{1, \dots, n\} \to \mathbb R$ with explicit $\ell_1$ and $\ell_\infty$ sums; $\operatorname{int}\Delta$ is the relative interior, and the entropy formula is evaluated on $\Delta$ only. "$\min_{1\le s\le k} f(x^s) - \min_X f \le R$" is stated as the existence of $s \in \{1, \dots, k\}$ with $f(x^s) - f(x^*) \le R$.

Added hypotheses, each disclosed in the item: a bound $\|f'(x)\|_* \le L_f$ on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to $X$); $D^{-1}b > 0$ in Proposition 4.1, without which the proposition as printed is false; $L_f > 0$ in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon $k$, which is what the proof chooses; Theorem 5.1 is stated with $L_f$, since the free index in the printed bound (5.28) cannot be bound, and $L_f$ is what the proof yields.

Trivializing formalizations are ruled out: $B_\psi$ is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of $\|f'(x^s)\|_\infty$ over the run, and the step is not an anytime schedule $t_s \propto 1/\sqrt s$.

A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.

Selected references

• A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Oper. Res. Lett. 31 (2003) 167–175. https://doi.org/10.1016/S0167-6377(02)00231-6
• A. Ben-Tal, T. Margalit, A. Nemirovski, The ordered subsets mirror descent optimization method with applications to tomography, SIAM J. Optim. 12 (2001) 79–108. https://doi.org/10.1137/S1052623499354564
• A. Nemirovsky, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• G. Chen, M. Teboulle, Convergence analysis of a proximal-like minimization algorithm using Bregman functions, SIAM J. Optim. 3 (1993) 538–543. https://doi.org/10.1137/0803026

Motivation

Many problems in imaging, signal processing and statistics are convex minimizations of the form

$$\min_{x\in\mathcal X}\ F(x)+G(x)+H(Lx),$$

where $F$ is smooth, $G$ and $H$ are nonsmooth but have computable proximity operators, and $L$ is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only $\nabla F$, the proximity operators of $G$ and $H^*$, and applications of $L$ and $L^*$, without ever inverting $L$ or computing the proximity operator of $H\circ L$.

Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.

Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under $\sigma\tau\|L\|^2<1$ (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term $F$, relaxation and errors (Theorem 3.1), and, for $F=0$, proved weak convergence for relaxation parameters up to $2$ (Theorem 3.2), the result of this mission.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and $L:\mathcal X\to\mathcal Y$ a bounded linear operator with adjoint $L^*$ and operator norm $\|L\|$. Write $\Gamma_0(\mathcal H)$ for the proper, lower semicontinuous, convex functions $\mathcal H\to\mathbb R\cup\{+\infty\}$. For $J\in\Gamma_0(\mathcal H)$, the conjugate is $J^*(s)=\sup_{s'}[\langle s,s'\rangle-J(s')]$, the proximity operator is $\mathrm{prox}_J(s)=\arg\min_{s'}[J(s')+\tfrac12\|s-s'\|^2]$, and the subdifferential is $\partial J(u)=\{v:\ J(u)+\langle v,u'-u\rangle\le J(u')\ \forall u'\}$.

Fix $G\in\Gamma_0(\mathcal X)$, $H\in\Gamma_0(\mathcal Y)$ and $F:\mathcal X\to\mathbb R$. The primal–dual inclusion (6) asks for $(\hat x,\hat y)$ with

$$0\in\partial G(\hat x)+L^*\hat y+\nabla F(\hat x),\qquad 0\in-L\hat x+\partial H^*(\hat y);$$

then $\hat x$ minimizes $F+G+H\circ L$ and $\hat y$ solves the dual problem. The paper assumes this inclusion has a solution.

Given $\tau,\sigma>0$, relaxation parameters $(\rho_n)$ and error terms $e_{F,n},e_{G,n}\in\mathcal X$, $e_{H,n}\in\mathcal Y$, Algorithm 3.1 iterates, from any $(x_0,y_0)$,

$$\tilde x_{n+1}=\mathrm{prox}_{\tau G}\big(x_n-\tau(\nabla F(x_n)+e_{F,n})-\tau L^*y_n\big)+e_{G,n},$$ $$\tilde y_{n+1}=\mathrm{prox}_{\sigma H^*}\big(y_n+\sigma L(2\tilde x_{n+1}-x_n)\big)+e_{H,n},$$ $$(x_{n+1},y_{n+1})=\rho_n(\tilde x_{n+1},\tilde y_{n+1})+(1-\rho_n)(x_n,y_n).$$

Algorithm 3.2 exchanges the roles: it computes $\tilde y_{n+1}$ from $y_n+\sigma Lx_n$ first, then $\tilde x_{n+1}$ using $L^*(2\tilde y_{n+1}-y_n)$.

Formalization targets

Goal: Theorem 3.2

Suppose $F=0$ and $e_{F,n}=0$, $\tau,\sigma>0$, and

$$\sigma\tau\|L\|^2<1,\qquad \rho_n\in\,]0,2[,\qquad \sum_n\rho_n(2-\rho_n)=+\infty,\qquad \sum_n\rho_n\|e_{G,n}\|<+\infty,\ \ \sum_n\rho_n\|e_{H,n}\|<+\infty.$$

Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution $(\hat x,\hat y)$ of (6) with $x_n\rightharpoonup\hat x$ and $y_n\rightharpoonup\hat y$ weakly.

Milestones

1. Lemma 4.1 (Krasnosel'skii–Mann): relaxed inexact iterates of a nonexpansive map converge weakly to a fixed point.
2. Lemma 4.2 (proximal point algorithm): for maximally monotone $M$, $s_{n+1}=s_n+\rho_n((I+M)^{-1}s_n+e_n-s_n)$ converges weakly to a zero of $M$ under the same conditions on $\rho_n$, $e_n$ as the goal.
3. $P$ bounded from below: if $\sigma\tau\|L\|^2<1$, the operators $P=\begin{pmatrix}\tau^{-1}I&-L^*\\-L&\sigma^{-1}I\end{pmatrix}$ and $P'$ (with $+L^*$, $+L$) satisfy $\langle z,Pz\rangle\ge c\|z\|^2$.
4. Inclusions (22) and (44): each error-free step satisfies $-(\nabla F(x_n),0)\in A(\tilde z_{n+1})+P(\tilde z_{n+1}-z_n)$ (resp. $P'$), where $A(x,y)=(\partial G(x)+L^*y)\times(-Lx+\partial H^*(y))$; with $F=0$ the left side is $0$.
5. $A$ is maximally monotone on $\mathcal X\times\mathcal Y$.

Further items

Remark 3.2 (the goal with $F$ affine, $\beta=0$, instead of $F=0$) and Theorem 5.2 (the version with $m\ge2$ composite terms $\sum_iH_i(L_ix)$ and condition $\sigma\tau\|\sum_iL_i^*L_i\|<1$).

Significance

The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation $\rho_n\in\,]0,2[$ and summable errors, in arbitrary real Hilbert spaces. Over-relaxation $\rho_n>1$ often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.

Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition $\sum\rho_n(2-\rho_n)=+\infty$ is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.

Difficulty

The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where $\sigma\tau\|L\|^2<1$, strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.

Formalization scope

The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in $\mathbb R\cup\{+\infty\}$ are EReal-valued, with $\Gamma_0$ the published IsProperClosedConvex. The conjugate is an EReal supremum, so $H^*$ can take the value $+\infty$. Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product $\mathcal X\times\mathcal Y$ with the inner product $\langle x,x'\rangle+\langle y,y'\rangle$ is WithLp 2 (X × Y). Weak convergence is $\langle x_n,v\rangle\to\langle\hat x,v\rangle$ for all $v$. "$\sum a_n=+\infty$" means partial sums tend to $+\infty$, and "$\sum\rho_n\|e_n\|<+\infty$" means summability of a nonnegative series.

Standing assumptions are hypotheses: $G,H\in\Gamma_0$, and (6) has a solution. With $F=0$ the smoothness assumption on $F$ is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit $(\hat x,\hat y)$ is chosen after the run.

The condition is strict, $\sigma\tau\|L\|^2<1$, and relaxation is open, $\rho_n\in\,]0,2[$. A goal quantifying over no run, assuming the limit exists, or fixing $(\hat x,\hat y)$ before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.

Selected references

• L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158(2):460–479, 2013. https://doi.org/10.1007/s10957-012-0245-9 (author's version: https://hal.science/hal-00609728)
• A. Chambolle, T. Pock, A first-order primal-dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40:120–145, 2011. https://doi.org/10.1007/s10851-010-0251-1
• B. He, X. Yuan, Convergence analysis of primal-dual algorithms for a saddle-point problem: from contraction perspective, SIAM J. Imaging Sci. 5(1):119–149, 2012. https://doi.org/10.1137/100814494
• B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38:667–681, 2013. https://doi.org/10.1007/s10444-011-9254-8
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
• P. L. Combettes, Solving monotone inclusions via compositions of nonexpansive averaged operators, Optimization 53:475–504, 2004. https://doi.org/10.1080/02331930412331327157

Motivation

Many problems in imaging, signal processing and statistics take the form

$$\min_{x\in\mathcal X}\ F(x)+G(x)+H(Lx),$$

where $G$ and $H$ are convex functions whose proximity operators can be computed cheaply, $L$ is a linear operator such as a finite-difference gradient, and $F$ is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because $H\circ L$ is generally not proximable even when $H$ is, practical methods split the problem so that each step uses only $\mathrm{prox}_{\tau G}$, $\mathrm{prox}_{\sigma H^*}$, $L$ and $L^*$, without inverting any operator.

L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With $F=0$ the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming $\tau\sigma\|L\|^2<1$, $\rho_n\equiv1$ and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation $\rho_n\equiv\rho\in\,]0,2[$ under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with $F=0$, the iterates converge under the step-size condition $\sigma\tau\|L\|^2\le1$, equality included. Equality matters in practice: one can set $\sigma=1/(\tau\|L\|^2)$ and tune a single parameter, as in the Douglas–Rachford method.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and $L:\mathcal X\to\mathcal Y$ a bounded linear operator with adjoint $L^*$ and operator norm $\|L\|$. Write $\Gamma_0(\mathcal H)$ for the proper, lower semicontinuous, convex functions $\mathcal H\to\mathbb R\cup\{+\infty\}$, and let $G\in\Gamma_0(\mathcal X)$, $H\in\Gamma_0(\mathcal Y)$. The Fenchel conjugate is $H^*(s)=\sup_{s'}[\langle s,s'\rangle-H(s')]$, the proximity operator is $\mathrm{prox}_J(s)=\operatorname{argmin}_{s'}[J(s')+\tfrac12\|s-s'\|^2]$, and the subdifferential is $\partial J(u)=\{v:\ \langle u'-u,v\rangle+J(u)\le J(u')\ \forall u'\}$.

The primal–dual inclusion (6) asks for $(\hat x,\hat y)\in\mathcal X\times\mathcal Y$ with

$$0\in\partial G(\hat x)+L^*\hat y+\nabla F(\hat x),\qquad 0\in-L\hat x+\partial H^*(\hat y).$$

A solution gives a minimiser $\hat x$ of the primal problem and a solution $\hat y$ of its dual.

Algorithm 3.1 chooses $\tau>0$, $\sigma>0$, relaxation parameters $(\rho_n)$, error terms $(e_{F,n}),(e_{G,n}),(e_{H,n})$ and an initial estimate $(x_0,y_0)$, then iterates

$$\tilde x_{n+1}=\mathrm{prox}_{\tau G}\big(x_n-\tau(\nabla F(x_n)+e_{F,n})-\tau L^*y_n\big)+e_{G,n},\qquad \tilde y_{n+1}=\mathrm{prox}_{\sigma H^*}\big(y_n+\sigma L(2\tilde x_{n+1}-x_n)\big)+e_{H,n},$$ $$(x_{n+1},y_{n+1})=\rho_n(\tilde x_{n+1},\tilde y_{n+1})+(1-\rho_n)(x_n,y_n).$$

Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses $2\tilde y_{n+1}-y_n$. Section 5 extends both to $\sum_{i=1}^mH_i(L_ix)$ (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).

Formalization targets

Goal: Theorem 3.3 (p. 6)

Let $\mathcal X$, $\mathcal Y$ be finite-dimensional, $F=0$, $e_{F,n}=0$, and assume (6) has a solution. If

$$\text{(i)}\ \sigma\tau\|L\|^2\le1,\qquad \text{(ii)}\ \rho_n\in[\varepsilon,2-\varepsilon]\ \ \forall n,\ \text{for some }\varepsilon>0,\qquad \text{(iii)}\ \textstyle\sum_n\|e_{G,n}\|<\infty,\ \sum_n\|e_{H,n}\|<\infty,$$

then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, $(x_n,y_n)$ converges to a solution $(\hat x,\hat y)$ of (6).

Milestones (from the proof, pp. 8–13)

With $P(x,y)=(\tfrac1\tau x-L^*y,\,-Lx+\tfrac1\sigma y)$ the operator (20) and $T(x,y)=(\tilde x,\tilde y)$ the error-free step of Algorithm 3.1:

• $P$ (and $P'$ of (44)) is positive under (i): $\langle z,Pz\rangle\ge0$;
• $T$ depends on $z$ only through $Pz$ (the paper's $T\circ S=T$, (32)–(33));
• on solutions of (6), $PT(z)=Pz$ ((41)–(42));
• $PT(z)=Pz$ implies that $T(z)$ solves (6) (via (35));
• $T$ is continuous;
• Lemma 4.1 (Krasnosel'skii–Mann iteration) and Lemma 4.6 (Polyak's lemma).

Further statements

Remark 3.2 (Theorem 3.3 with $F$ affine, i.e. $\beta=0$ in (2)) and Theorem 5.3 (the analogue for $m\ge2$ composite terms, with (i) replaced by $\sigma\tau\|\sum_iL_i^*L_i\|\le1$) are included as draft theorems.

Significance

Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size $\sigma\tau\|L\|^2=1$. It covers relaxation parameters up to $2-\varepsilon$ and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.

None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.

Difficulty

The usual proof treats the iteration as a proximal-point or forward–backward step in the space $\mathcal X\times\mathcal Y$ with the inner product $\langle z,Pz'\rangle$. That argument needs $P$ strictly positive, which is exactly what fails when $\sigma\tau\|L\|^2=1$: then $P$ has a nontrivial kernel, $\langle z,Pz\rangle$ is only a seminorm, and weak convergence in the $P$-geometry says nothing about the components of $z$ in $\ker P$. The proof replaces the iteration by its "shadow" $Sz_n$ on $\operatorname{ran}P$, uses that $T$ factors through $S$, and recovers the full iterates through continuity of $T$ and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.

Formalization scope

Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in $\Gamma_0$ take values in EReal and satisfy the published predicate IsProperClosedConvex (never $-\infty$, finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps $P_G$, $P_H$ satisfying the published minimisation predicate IsProx for $\tau G$ and $\sigma H^*$; such maps exist and are unique for $\Gamma_0$ functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. "$=+\infty$" for a series is divergence of its partial sums, "$<+\infty$" is summability of a nonnegative series, and convergence in the goal is norm convergence.

The standing assumptions of pp. 3–4 are hypotheses: $G,H\in\Gamma_0$, and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators $P$ and $T$ are plain maps on $\mathcal X\times\mathcal Y$. The projector $S$ is not built: "$T\circ S=T$" is stated as "$Pz=Pz'\Rightarrow T(z)=T(z')$", which is equivalent because $P$ is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.

The strict inequality $\sigma\tau\|L\|^2<1$ would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps $\le$. Weak convergence in place of norm convergence, an $\varepsilon$ chosen after $n$, or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.

Useful infrastructure includes: firm nonexpansiveness of $\mathrm{prox}$ for EReal-valued $\Gamma_0$ functions; $\Gamma_0$-ness of the conjugate and Moreau's identity; maximal monotonicity of $\partial G\times\partial H^*$ plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.

Selected references

• L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158(2):460–479, 2013. https://doi.org/10.1007/s10957-012-0245-9 (author's version: https://hal.science/hal-00609728v5)
• B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38:667–681, 2013. https://doi.org/10.1007/s10444-011-9254-8
• A. Chambolle, T. Pock, A first-order primal–dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40:120–145, 2011. https://doi.org/10.1007/s10851-010-0251-1
• P. L. Combettes, Solving monotone inclusions via compositions of nonexpansive averaged operators, Optimization 53:475–504, 2004. https://doi.org/10.1080/02331930412331327157
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
• B. T. Polyak, Introduction to Optimization, Optimization Software, New York, 1987.

Motivation

Many convex optimization models combine a smooth loss, a nonsmooth penalty whose proximity operator is easy to compute, and a second penalty applied after a linear map. Imaging models, for example, often place a data-fitting term on the image and a regularizer on its transformed coefficients. The resulting objective has the form $F(x)+G(x)+H(Lx)$. Condat's primal–dual method evaluates the smooth gradient and two proximity operators separately, without requiring a proximity operator for the composite $H\circ L$. Condat, 2013 establishes weak convergence with relaxation and summably weighted computational errors. This mission targets its main positive-smoothness theorem, Theorem 3.1, in the final author's version.

The theorem matters when a computed gradient or proximal point is inexact, as is common when a proximal subproblem is itself solved numerically. Its conditions account for these errors directly rather than treating the displayed algorithm as exact. It also gives one parameter regime for two orders of updating the primal and dual variables. These two algorithms share an objective and a solution inclusion, but have distinct recursions.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and let $L:\mathcal X\to\mathcal Y$ be bounded linear, with adjoint $L^*$. The smooth term $F:\mathcal X\to\mathbb R$ is convex and differentiable. Its gradient is $\beta$-Lipschitz when $\|\nabla F(x)-\nabla F(x')\|\le\beta\|x-x'\|$ for all $x,x'$. The nonsmooth terms $G$ and $H$ are proper, lower semicontinuous, convex functions with values in $\mathbb R\cup\{+\infty\}$. Such functions form the class $\Gamma_0$. An infinite value may encode a constraint.

For a convex function $J$, its proximity operator $\operatorname{prox}_{\gamma J}(s)$ minimizes $J(u)+\|u-s\|^2/(2\gamma)$ over $u$, where $\gamma>0$. The Fenchel conjugate is $J^*(v)=\sup_u\{\langle v,u\rangle-J(u)\}$. A subgradient $v\in\partial J(u)$ obeys $J(u)+\langle v,u'-u\rangle\le J(u')$ for every $u'$. The sought primal–dual solution $(\hat x,\hat y)$ satisfies

$$-L^*\hat y-\nabla F(\hat x)\in\partial G(\hat x),\qquad L\hat x\in\partial H^*(\hat y).$$

Algorithms 3.1 and 3.2 maintain sequences $x_n\in\mathcal X$ and $y_n\in\mathcal Y$. Algorithm 3.1 updates the primal proximity step before the dual one; Algorithm 3.2 reverses that order. Each uses positive step sizes $\tau,\sigma$, positive relaxation weights $\rho_n$, and errors $e_{F,n}$, $e_{G,n}$ and $e_{H,n}$ in the gradient and the two proximal evaluations. Their full recursions are part of the Lean setting, so a run is determined by its initial pair. The paper specifies the problem in §2 and both algorithms in §3.

Formalization targets

The goal is Theorem 3.1 on p. 5. Suppose $\beta>0$, the primal–dual solution set is nonempty, and $G,H\in\Gamma_0$. Set

$$\delta=2-\frac{\beta}{2}\left(\frac1\tau-\sigma\|L\|^2\right)^{-1}.$$

For $\tau,\sigma>0$, the theorem assumes

$$\frac1\tau-\sigma\|L\|^2\ge\frac\beta2,\qquad 0<\rho_n<\delta\quad\text{for every }n,$$ $$\sum_{n\ge0}\rho_n(\delta-\rho_n)=+\infty,\qquad\sum_{n\ge0}\rho_n\|e_{F,n}\|<\infty,\quad\sum_{n\ge0}\rho_n\|e_{G,n}\|<\infty,\quad\sum_{n\ge0}\rho_n\|e_{H,n}\|<\infty.$$

Under these conditions, both sequences of each algorithm converge weakly to the components of a primal–dual solution. The solution may depend on the initial pair and on the run. The milestone list includes Lemmas 4.1 and 4.3–4.5, the strict positivity claim for the block operator $P$, estimate (29), and the error-free optimality inclusions (22) and (44), ordered as preliminary results followed by the two algorithm-specific claims. These targets match the results stated in §4 of the source version.

Significance

The result supplies a convergence guarantee for a composite objective under an explicit coupling condition on $\tau$, $\sigma$, and $\|L\|$. It permits relaxation weights that vary with $n$ and errors that are summable only after weighting by those same relaxation values. The dual conclusion is substantive: convergence of the primal sequence alone would not give convergence of the dual certificate produced by the algorithm. The weak topology is appropriate in general Hilbert spaces; norm convergence would assert more than the paper proves.

The theorem is proved in the 2013 paper. The present formalization task is to give its statement and the selected operator lemmas machine-checked proofs in Lean. Related platform definitions for proximal maps, monotone operators, nonexpansive maps, subgradients and weak convergence already exist; the paper-specific convergence theorem and its selected milestones are new targets in this proposal. The resulting definitions and abstract Lemmas 4.1, 4.3–4.5 can be reused in later operator-splitting developments.

Difficulty

The displayed recursions involve three errors, two proximal evaluations, a linear map and its adjoint, and two different update orders. A direct estimate on $\|x_{n+1}-\hat x\|$ does not by itself control the coupled dual variable, while a bound on only the combined objective value would not establish weak convergence of either iterate. The relaxation condition permits weights without a fixed positive lower bound, so a convergence argument cannot replace the stated divergent series by a simpler constant-step assumption. The abstract lemmas must also retain the endpoints $\alpha_2=1$ and $\gamma=2\kappa$ present in the source.

Formalization scope

Lean uses complete real inner-product spaces for $\mathcal X$ and $\mathcal Y$, a continuous linear map for $L$, and EReal for $G$, $H$ and their conjugates. The conjugate supremum is taken in EReal. The paper's $\Gamma_0$ class and proximity maps use published definitions; the latter are parameters constrained to be the actual proximal minimizers. Positive step sizes and proper closed convex data ensure such maps exist and are unique. The subgradient predicate explicitly requires a finite value at the base point; this follows from the source's properness assumptions when a subgradient exists.

Both algorithms are represented by recursion predicates on every natural-number index, with all error terms present. The goal quantifies over every run and chooses its weak limit afterwards. Divergence to $+\infty$ means finite partial sums tend to atTop; a finite weighted error sum means the corresponding nonnegative real sequence is summable. These choices prevent a default value of an infinite sum from satisfying the hypotheses. The nonempty solution set is an explicit standing assumption from p. 4 and implies the earlier nonempty-primal-minimizer assumption. A condition that made all runs impossible, or one that discarded either the primal or dual conclusion, would not represent Theorem 3.1.

The block operator $P$ is represented through its quadratic form $q_P$; $P'$ is recorded for Algorithm 3.2. The complete development will need the abstract iteration lemmas, proximal optimality conditions, block-metric estimates, and the links from each algorithm's inclusion to the solution set. Contributions proving those results, or building reusable Hilbert-space operator infrastructure needed by them, are in scope. The several-composite-functions extension in Theorem 5.1 is reserved for separate work.

Selected references

• Laurent Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, Journal of Optimization Theory and Applications 158(2):460–479, 2013. DOI; final author's version, hal-00609728v5.