All missions

Motivation

A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.

A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.

Setting

Fix $c, f \in \mathbb R^n$ and write a linear program in the homogeneous form (6)

$$(P)\qquad \min\{c^{T}x \mid Ax \ge 0,\ f^{T}x = 1\},$$

where $A$ is a real $m\times n$ matrix and $Ax\ge0$ is componentwise. Every linear program can be put in this form. The matrix $A$ is uncertain: it is only known to lie in an uncertainty set $\mathcal U$ of $m\times n$ matrices. Each $A\in\mathcal U$ gives an instance $(P)$ with feasible set $\{x\mid Ax\ge0,\ f^{T}x = 1\}$ and optimal value $c^*(P)$; the family of instances is $\mathcal P$. The robust counterpart (7) is

$$(P_{\mathcal U})\qquad \min\{c^{T}x \mid x \in G_{\mathcal U}\},\qquad G_{\mathcal U} = \{x\mid Ax\ge0\ \ \forall A\in\mathcal U;\ f^{T}x = 1\},$$

and its optimal value is $c^*$. Since $G_{\mathcal U}$ does not change when $\mathcal U$ is replaced by its closed convex hull, the paper assumes throughout that $\mathcal U$ is convex and closed.

Let $\mathcal U_i\subseteq\mathbb R^n$ be the set of all realizations of the $i$-th row, the projection of $\mathcal U$ onto the data of the $i$-th constraint. The uncertainty is constraint-wise if $\mathcal U = \mathcal U_1\times\dots\times\mathcal U_m$: the rows vary independently. The Boundedness Assumption asks for a convex compact set $Q\subseteq\mathbb R^n$ that contains the feasible set of every instance.

Formalization targets

Goal: Proposition 2.1 (p. 5)

If the uncertainty is constraint-wise and the Boundedness Assumption holds, then

1. $(P_{\mathcal U})$ is infeasible if and only if some instance is infeasible:

$$G_{\mathcal U} = \emptyset \iff \exists A\in\mathcal U:\ \{x\mid Ax\ge0,\ f^{T}x=1\}=\emptyset;$$

2. if $(P_{\mathcal U})$ is feasible with optimal value $c^*$, then

$$c^* = \sup\{c^*(P)\mid (P)\in\mathcal P\}. \tag{9}$$

Milestones

The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of $G_{\mathcal U}$ in every instance's feasible set; the reduction of the semi-infinite system (8) on $Q$ to a finite subsystem; the statement that the finite system (10) $A_1x\ge0,\dots,A_Nx\ge0,\ f^{T}x=1$ then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.

Companions

The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: $G_{\mathcal U}$ is unchanged under passing to the closed convex hull of $\mathcal U$ (§2.1) or to the product $\mathcal U_1\times\dots\times\mathcal U_m$ of its projections (§2.2).

Significance

Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of $G_{\mathcal U}$ under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.

The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of $\mathcal U$.

Difficulty

The robust counterpart has a continuum of constraints, one for each $A\in\mathcal U$, so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in $Q$; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in $\mathcal U$, which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and $Ax\ge0$ is 0 ≤ A *ᵥ x in the componentwise order. The $i$-th row of $A$ is A i and $a^{T}x$ is a ⬝ᵥ x. The projections $\mathcal U_i$ are the images of $\mathcal U$ under $A\mapsto A_i$, not free sets, and constraint-wise uncertainty is the inclusion $\mathcal U_1\times\dots\times\mathcal U_m\subseteq\mathcal U$ (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of $Q$, as on the page.

Optimal values are infima: $c^*$ is the greatest lower bound (IsGLB) of $c^{T}x$ over $G_{\mathcal U}$, and (9) states that $c^*$ is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.

The goal carries the paper's standing assumption that $\mathcal U$ is convex and closed, and one disclosed addition: $\mathcal U$ is nonempty. The paper takes this for granted; without it part (i) fails for $f = 0$ and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets $\mathcal U_i$ are arbitrary sets with $\mathcal U = \prod_i\mathcal U_i$, or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.

A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/s0167-6377(99)00016-4 (cited here by the pages of the authors' manuscript).
• A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154

Motivation

Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid $F_7$, and proves that no real matrix corresponds to it.

The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line $U_{2,4}$, and the regular matroids by three excluded minors, $U_{2,4}$, $F_7$ and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over $\mathbb R$.

Timeline:

• 1935. Whitney defines matroids, the circuit matrix of a matrix, and proves (§16) that the seven-element matroid $M'$ corresponds to no real matrix; in a footnote he credits Saunders MacLane with finding that $M'$ corresponds to no matrix and identifying it with a finite projective geometry. On p. 533 he exhibits a matrix of integers mod 2 for $M'$.
• 1958. Tutte characterizes binary and regular matroids by excluded minors; $F_7$ appears as an excluded minor for regularity (Tutte 1958).

Setting

Let $\mathbf M=(a_{ij})$ be an $m\times n$ matrix with columns $C_1,\dots,C_n$. For a set $N$ of columns, let $r(N)$ be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid $M$ on $\{C_1,\dots,C_n\}$ with rank function $r$: the matroid of $\mathbf M$. A matroid corresponds to $\mathbf M$ if it is the matroid of $\mathbf M$, with elements matched to columns.

A circuit of a matroid is a minimal dependent set. For a circuit $P=\{i_1,\dots,i_p\}$ of the matroid of $\mathbf M$, there are numbers $b_1,\dots,b_n$ with $\sum_j a_{ij}b_j=0$ for every row $i$, and $b_j\neq 0$ exactly for $j\in P$; the set of such vectors is written $Z_{i_1\cdots i_p}$ when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix $\mathbf M'$ of $\mathbf M$, determined up to nonzero factors on its rows.

A fundamental set of circuits of a matroid $M$ with nullity $n(M)=\rho(M)-r(M)$ ($\rho$ the number of elements) is a family of circuits $P_1,\dots,P_q$ with $q=n(M)$ such that the elements can be ordered $e_1,\dots,e_n$ with $e_{n-q+i}\in P_i$ and $e_{n-q+j}\notin P_i$ for $j>i$; it is strict if $e_{n-q+j}\notin P_i$ for every $j\neq i$.

The matroid $M'$ of §16 has elements $1,\dots,7$; its bases (maximal independent sets) are all three-element sets except

$$124,\quad 135,\quad 167,\quad 236,\quad 257,\quad 347,\quad 456. \qquad (16.1)$$

Formalization targets

Goal: §16, pp. 529–530

$$\exists\,M' \quad\text{and}\quad \forall m\ \forall\,\mathbf M\in\mathbb R^{m\times 7}:\ M' \text{ is not the matroid of } \mathbf M .$$

The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.

Milestones

1. §12. Every real matrix has a matroid: the ranks of column submatrices satisfy the rank postulates.
2. §14, (14.1). Every real matrix has a circuit matrix.
3. Theorem 29. The rows of a fundamental set of circuits form a base for the rows of the circuit matrix, so $r(\mathbf M')=q=n(\mathbf M)$.
4. Lemma 10. The support of a vector in the row space $H$ of a circuit matrix is a union of circuits.
5. Lemma 11. Two vectors of $H$ with the same circuit as support are proportional.
6. Theorem 32. For a circuit matrix normalised along a strict fundamental set, a minor $D$ vanishes iff an associated $q\times q$ minor $D'$ vanishes, iff some circuit avoids a prescribed set of columns.
7. §16, rank of $M'$. The rank of a $k$-set is $k$ for $k\le 2$, $3$ for $k\ge 4$, and for $k=3$ it is $2$ on (16.1) and $3$ otherwise.
8. p. 533. $M'$ is the matroid of an explicit $3\times 7$ matrix of integers mod 2.

Significance

The result. The theorem separates the abstract notion of matroid from linear dependence over $\mathbb R$: some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.

Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over $\mathbb R$ in Lean is known to the curators.

Difficulty

The obvious attempt is a direct search: suppose a real $m\times 7$ matrix has $M'$ as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows $m$ is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that $2\neq 0$ in $\mathbb R$, since over a field of characteristic 2 the statement is false (milestone 8).

Formalization scope

• Elements and matrices. Matroids are Mathlib Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element $k$ being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of $\mathbf M$" means: ground set everything, and the rank M.eRk N of every finite set $N$ of columns equals Matrix.rank of the column submatrix.
• Field. The goal and Lemmas 10–11, Theorems 29 and 32 are stated over $\mathbb R$, as in the paper; the predicate "matroid of a matrix" is stated over any field so that the mod-2 milestone uses the same notion.
• Circuit matrix. Rows are determined up to nonzero factors, so "circuit matrix" is a predicate on a matrix together with a bijection between its rows and the circuits; every theorem holds for every such choice.
• Nullity and indices. $q=n(M)$ is written $q+r(M)=\rho(M)$ in extended naturals, with no truncated subtraction. In Theorem 32, $n=p+q$, the complement of $i_1,\dots,i_s$ is given as an order embedding of Fin t with $s+t=q$, and determinants are of square submatrices in the paper's row and column order.
• Ruling out trivial readings. The goal includes the existence of $M'$; without it "every matroid with these bases has no real matrix" could hold vacuously. The goal quantifies over every number of rows; fixing $m=3$ would be a weaker statement.

Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the American Mathematical Society 88 (1958), 144–174. https://doi.org/10.2307/1993244
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• O. Veblen and J. W. Young, Projective Geometry, Vol. I, Ginn, 1910 (cited by Whitney for the finite projective geometry).

Motivation

Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.

Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.

Setting

A matroid $M$ on elements $e_1, \dots, e_n$ is given by its independent sets; its circuits are its minimal dependent sets, its rank $r(M)$ is the size of a base, and its nullity is $n(M) = n - r(M)$. Here $M$ is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.

Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle $\emptyset$. A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.

With $n = r + q$, a family $P_1, \dots, P_q$ is a strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$ if $q = n(M)$, each $P_i$ is a circuit, and $P_i$ contains $e_{n-q+i}$ but no other $e_{n-q+j}$.

For a matrix $\mathbf M$ over the integers mod 2 with columns $C_1, \dots, C_n$, columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to $\mathbf M$ has the column indices as elements and these independent sets.

Formalization targets

Goal: Theorem 37 (p. 533)

Let $M$ satisfy (C*), with elements $e_1, \dots, e_n$ and base $\{e_1, \dots, e_{n-q}\}$. For every matrix $\mathbf M_1$ mod 2 (any number of rows) whose $n - q$ columns are independent mod 2,

$$\exists!\ \mathbf M = (\mathbf M_1 \mid C_{n-q+1} \cdots C_n) \ \text{ whose corresponding matroid is } M.$$

Milestones

1. Theorem 9 (p. 517): if $e_1, \dots, e_{n-q}$ is a base, there is a unique strict fundamental set of circuits with respect to $e_{n-q+1}, \dots, e_n$.
2. Appendix, p. 531: (C*) implies the circuit postulate (C₂), for any family of sets.
3. Theorem 33: under (C*), the circuits are exactly the minimal non-null cycles.
4. Theorem 34: under (C*), the cycles are exactly the $2^q$ sums mod 2 of a strict fundamental set.
5. Theorem 35: two (C*)-matroids with a common strict fundamental set have the same circuits.
6. Theorem 36: any $P_1, \dots, P_q$ with $e_{n-q+i} \in P_i \subseteq \{e_1, \dots, e_{n-q}, e_{n-q+i}\}$ is the strict fundamental set of exactly one (C*)-matroid.
7. Appendix, p. 532: the matroid of a matrix mod 2 exists, satisfies (C*), and its cycles are the supports of the mod-2 dependencies among the columns.

Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).

Significance

The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by $q$ arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.

Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.

Difficulty

Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is $M$ itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.

Formalization scope

• Matroids are Mathlib Matroid (Fin (r + q)) with ground set Set.univ; Whitney's $e_k$ is k - 1, his $e_1, \dots, e_{n-q}$ is the range of Fin.castAdd q, and $e_{n-q+i}$ is Fin.natAdd r (i - 1). Writing $n = r + q$ removes natural-number subtraction; $q$ is not a free parameter, since $\{e_1, \dots, e_r\}$ is required to be a base.
• Sums mod 2 count parity of membership (sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.
• A strict fundamental set includes the nullity condition $r(M) + q = \rho(M)$, stated in $\mathbb N_\infty$.
• Matrices are Matrix (Fin m) (Fin n) (ZMod 2) with any $m$; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.
• Ruled out: the goal is not satisfied by any statement that compares only the bases of one size, by an existence-only statement without uniqueness, or by real (instead of mod-2) independence.
• Tacit hypotheses made explicit: the matroid's ground set is exactly $e_1, \dots, e_n$ ($\rho(M) = n$); the elements and matroids are finite.

Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• W. T. Tutte, A homotopy theorem for matroids, I, II, Transactions of the AMS 88 (1958), 144–174. https://doi.org/10.2307/1993244
• P. D. Seymour, The matroids with the max-flow min-cut property, Journal of Combinatorial Theory Ser. B 23 (1977), 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• P. D. Seymour, Decomposition of regular matroids, Journal of Combinatorial Theory Ser. B 28 (1980), 305–359. https://doi.org/10.1016/0095-8956(80)90075-1
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001

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

Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract rank function that behaves like the rank of a set of vectors. Part II of the paper opens with the decomposition of a matroid into components. The question it answers is basic to every later use of matroids: when does a matroid split into independent pieces, and how can the pieces be recognized?

For the matroid of a graph (elements = edges, rank = number of vertices minus number of connected pieces spanned) the components are the 2-connected blocks of the graph, and Whitney's theorem recovers the classical fact that two edges lie in a common block exactly when they lie on a common cycle. Whitney had studied separability of graphs in Non-separable and planar graphs (1932), and footnote 11 of the 1935 paper points out that the theorem identifies König's "Glieder" of a graph with components. Matroid connectivity built on this notion runs through later structure theory: Tutte's higher connectivity, Seymour's decomposition of regular matroids, and the matroid minors project all start from the separation of a matroid into components.

Setting

A matroid $M$ on a finite ground set $E$ is given here by Mathlib's Matroid structure, with rank function $r(X)$ for $X\subseteq E$ (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset $X\subseteq E$ as a matroid in its own right, a submatroid, with the rank function of $M$ restricted to subsets of $X$. For sets he writes $M_1+M_2$ for the union, $\rho(N)$ for the number of elements of $N$, and

$$n(N) = \rho(N) - r(N)$$

for the nullity of $N$.

Rank is subadditive: $r(X_1+X_2)\le r(X_1)+r(X_2)$. A submatroid $X$ is separable if it can be divided into two disjoint groups $X_1, X_2$, each containing at least one element, with

$$r(X) = r(X_1) + r(X_2),$$

and non-separable otherwise. Every single element is non-separable. A component of $M$ is a maximal non-separable part of $M$: a nonempty non-separable set $K\subseteq E$ contained in no strictly larger non-separable subset of $E$.

Formalization targets

Goal: Theorem 19

For two distinct elements $e_1\neq e_2$ of $E$,

$$\bigl(\exists K \text{ component of } M:\ e_1, e_2\in K\bigr) \iff \bigl(\exists P \text{ circuit of } M:\ e_1, e_2\in P\bigr).$$

Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.

Milestones (§10, in the paper's order)

• Theorem 11. If $r(M_1+M_2)=r(M_1)+r(M_2)$, $M_1'\subseteq M_1$ and $M_2'\subseteq M_2$, then $r(M_1'+M_2')=r(M_1')+r(M_2')$.
• Theorem 12. Under the same rank additivity, a non-separable $M'\subseteq M_1+M_2$ lies in $M_1$ or in $M_2$.
• Theorem 13. Two non-separable sets with a common element have a non-separable union.
• Theorem 14. Distinct components are disjoint.
• Theorem 15. The components cover $E$, and no other family of components does.
• Theorem 16. A set is non-separable of nullity $1$ if and only if it is a circuit.
• Lemma 9. If $M_1+M_2$ is non-separable, with $M_1, M_2$ nonempty and disjoint, some circuit inside $M_1+M_2$ meets both.
• Theorem 17. A non-separable set of nullity $n>0$ is built from a circuit by $n-1$ steps, each adding a set of elements that forms a circuit with elements already present, through non-separable sets of nullity $1,2,\dots,n$.
• Theorem 18. For distinct nonempty non-separable $M_1,\dots,M_p$ covering $E$, the following are equivalent: they are the components; they are pairwise disjoint and no circuit meets two of them; $r(E)=\sum_i r(M_i)$.

Significance

The result. Theorem 19 makes the component decomposition computable from circuits alone and shows that "lying on a common circuit" is an equivalence relation on distinct elements, a fact that is not evident from the circuit axioms. Theorem 18 adds that the decomposition is the unique one with additive rank. Together they are the starting point of matroid connectivity: the direct-sum decomposition of a matroid, the reduction of many matroid problems (representability, duality of components, Whitney's own Theorems 24–26 on duals of components) to the connected case, and the higher-connectivity theory that followed.

Formalizing it. The results are classical and proved in the paper; nothing here is open. To our knowledge Mathlib at the pinned revision has no notion of matroid connectivity or components, so this mission produces the first machine-checked development of Whitney's §10: the rank-based definition of separability, the disjoint decomposition into components, the circuit characterization, and the ear-type construction of non-separable matroids (Theorem 17). These are reusable for any later formalization of matroid connectivity, including Whitney's results on duals of components.

Difficulty

The two directions of Theorem 19 rest on different machinery. That two elements on a common circuit lie in one component follows from the rank theory (Theorems 13 and 16). The converse is the substantial direction: a component is defined by the failure of rank additivity, which only says that every division of the component is crossed by some circuit (Lemma 9). It does not directly give one circuit through two prescribed elements. Combining circuits that cross different divisions into a single circuit through both $e_1$ and $e_2$ requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from $e_1$ to $e_2$ gives a connected chain of circuits, not one circuit.

Formalization scope

• Representation. A matroid is Mathlib's Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset $X\subseteq$ M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid $M = M_1 + M_2$" are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid $M_1+M_2$.
• Ranks are Mathlib's ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in $\mathbb Z$ as the number of elements minus the rank.
• Definitions. IsSeparable M X requires two nonempty, disjoint groups with union $X$ and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds $X\subseteq$ M.E. IsComponent M K requires $K$ nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.
• Tacit hypotheses made explicit. In Theorem 19 the two elements are distinct: for $e_1=e_2$ a coloop is its own component and lies on no circuit. In Theorem 18 the sets $M_1,\dots,M_p$ are distinct and nonempty: a loop listed twice would satisfy (3) but not (2), and an empty set would satisfy (2) and (3) but not (1). In Theorems 11 and 12 the two parts need not be disjoint, as Whitney's use of $M_1+M_2$ for overlapping sets in Theorem 13 indicates; the statements hold in that generality.
• Ruled out. Components must not be defined as the classes of the relation "lie on a common circuit": that would make the goal a tautology. Here they are the rank-defined maximal non-separable sets of §10, and circuits are Mathlib's Matroid.IsCircuit.
• Infrastructure. Solvers will need submodularity of M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside $X$ (Matroid.restrict_isCircuit_iff), and finiteness arguments for maximal non-separable sets. Proofs of the milestones, alternative proofs of the goal, and lemmas relating components to Mathlib's direct sums of matroids are all welcome.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182
• 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
• D. König, Acta Litterarum ac Scientiarum Szeged, vol. 6, pp. 155–179, as cited by Whitney in footnote 11 (p. 159 for the notion of "Glied").
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011, Chapter 4 (connectivity).

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.