Convex Optimization

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

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

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.

Motivation

Many large convex programs have the form "minimize a strictly convex function $f$ subject to linear equations $Ax=b$". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When $A$ is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of $A$.

L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets $A_i$, in which each step replaces the current point by its $D$-projection onto one set: the minimizer of a distance-like function $D(\cdot,y)$ over that set. §2 chooses $D$ from the objective $f$ itself, $D(x,y)=f(x)-f(y)-(g(y),x-y)$ with $g$ the gradient of $f$; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes $f$ over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.

Setting

Work in the Euclidean space $E^p$ with inner product $(\cdot,\cdot)$. Let $S\subset E^p$ be a convex set with closure $\bar S$ and interior $\operatorname{int}S$. Let $f$ be strictly convex and continuously differentiable over $S$, with gradient $g(x)$ at $x\in S$, and continuous over $\bar S$. Let $A$ be an $m\times p$ matrix with nonzero rows $A_1,\dots,A_m$ and $b\in E^m$. The problem (2.1)–(2.3) is

$$\text{minimize } f(x)\quad\text{subject to}\quad Ax=b,\ x\in\bar S,$$

with feasible set $R=\{x\in E^p\mid Ax=b,\ x\in\bar S\}$, assumed nonempty. A point of $R$ minimizing $f$ over $R$ is a solution.

The function (1.4) is

$$D(x,y)=f(x)-f(y)-\bigl(g(y),x-y\bigr),$$

and $A_i$ also denotes the hyperplane $\{x\mid (A_i,x)=b_i\}$. The paper assumes that $D$ satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every $y\in S$, a $D$-projection $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$. It also assumes condition (2): if $y^n\in S$ and $y^n\to y^*\in\bar S$, then $D(y^*,y^n)\to 0$.

A relaxation sequence with control $(i_n)_{n\ge0}$ starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. The control is any sequence of row indices. Finally,

$$Z=\{x\in S\mid g(x)=uA=\textstyle\sum_i u_iA_i\ \text{for some } u\in E^m\}$$

is the set of points of $S$ at which the gradient lies in the row space of $A$.

Formalization targets

Goal: Theorem 3

Assume that the $D$-projection of every point of $\operatorname{int}S$ onto every $A_i$ lies in $\operatorname{int}S$. For every control and every relaxation sequence with $x^0\in Z\cap\operatorname{int}S$ that converges to a point $x^*\in R$,

$$f(x^*)\le f(y)\qquad\text{for every } y\in R .$$

Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.

Milestones

1. Lemma 3. If $y^*\in R\cap\bar Z$, then $y^*$ is a solution of (2.1)–(2.3).
2. (2.7)–(2.8). For $x\in\operatorname{int}S$ there is $\lambda\in\mathbb R$ with $g(P_ix)=g(x)+\lambda A_i$ and $(A_i,P_ix)=b_i$.
3. Invariance of $Z$. $P_i$ maps $Z\cap\operatorname{int}S$ into $Z\cap\operatorname{int}S$.

An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.

Significance

Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier $\lambda$ of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for $f(x)=\tfrac12\|x\|^2$.

The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.

Difficulty

The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of $A$, so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on $S$, the limit may lie on the boundary of $S$ (or outside $S$, in $\bar S$), and $g$ need not extend continuously there, so the multipliers $u^n$ need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at $y^*$. Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that $P_i$ preserves $\operatorname{int}S$; on the boundary of $S$ a minimizer over $A_i\cap S$ need not satisfy (2.7).

Formalization scope

The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and $(A_i,x)$ is the real inner product. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt f (g x) S x for $x\in S$ and continuous on $S$; $S$ is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:

• The $D$-projection is a fixed map $P$; condition II says $P_iy$ minimizes $D(\cdot,y)$ over $A_i\cap S$, and condition III is stated for that map.
• Condition IV is assumed in its one-sided directional form (implied by the paper's), so theorems under it are at least as strong as the paper's.
• "Compact" in conditions V and VI is sequential compactness. Condition V is assumed for the points of $R\cap S$.
• Condition (2) is assumed for limits $y^*\in\bar S$; the page prints $y^*\in S$, but its use at a feasible point needs $\bar S$.
• Translation slips are corrected in the statements and recorded: condition II's "$D(z,x)$" and "$i\in T$", (2.7)'s "$g(x^{n-1})$" (read $g(x^{n+1})$), and "Theorems 1 − 3" (read Theorems 1–2).
• The control is an arbitrary sequence of indices in $\{0,\dots,m-1\}$; λ is named lam.
• Note 2 is stated for candidate points $y,z\in S$, where $g$ is meaningful.

The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open $S$, or to a limit assumed to lie in $Z$: any of these would trivialize the passage to the limit that the theorem is about.

A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality $f(x)\ge f(y)+(g(y),x-y)$ for $x\in\bar S$, $y\in S$, and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. doi:10.1016/0041-5553(67)90040-7
• Y. Censor, S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997. doi:10.1093/oso/9780195100624.001.0001
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. doi:10.1007/BF00934676

Why a likelihood maximum needs a diagnostic

The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.

The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.

Choice experiments and weighted differences

There are $N\geq1$ trials. Trial $n$ offers $J_n$ alternatives, indexed by $i$ and $j$. Alternative $i$ has an attribute vector $z_{in}\in\mathbb R^K$, and $S_{in}$ counts how many times it was selected in that trial. Each trial has at least two alternatives and $R_n=\sum_iS_{in}>0$ observations. The vector $\theta\in\mathbb R^K$ is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative $i$ a probability proportional to $\exp(z_{in}\cdot\theta)$, with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).

For the test, define the weighted difference

$$w_{nij}=S_{in}(z_{jn}-z_{in})\in\mathbb R^K.$$

It is indexed by every trial and every ordered pair of alternatives, including $i=j$ and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.

Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank $K$. Equivalently, the vectors $z_{jn}-z_{in}$ span $\mathbb R^K$; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction $\gamma\in\mathbb R^K$ satisfies $w_{nij}\cdot\gamma\leq0$ for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.

Formalization targets

Lemma 4: a quadratic-programming test

Let $Q$ be the set of feasible vectors

$$Q=\left\{y=\sum_{n=1}^{N}\sum_{i,j=1}^{J_n}\alpha_{ijn}w_{nij}: \alpha_{ijn}\geq1\text{ for all }n,i,j\right\}.$$

The mission's goal is the equivalence in Lemma 4:

$$\text{Axiom 6 holds} \quad\Longleftrightarrow\quad \min_{y\in Q}y\cdot y=0.$$

The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the $w_{nij}$ gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).

What the result provides

Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.

The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.

Why the equivalence is delicate

The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints $\alpha_{ijn}\geq1$ in equation (22). Both conditions must appear in their proper places.

The full-rank condition alone does not ensure that the vectors $w_{nij}$ span the attribute space if a trial has no observed choices. The section describes $R_n$ repetitions of each trial, and the formal data require $R_n>0$. This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.

Formalization scope

Lean represents a nonempty set of trials by Fin N, alternatives in trial $n$ by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count $R_n$ is the sum of observed choice counts. The model requires $J_n\geq2$ and $R_n>0$ for each trial. There is no extra assumption that $K>0$: the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.

Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every $n,i,j$ from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.

The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.

Selected references

• Daniel McFadden, “Conditional Logit Analysis of Qualitative Choice Behavior,” in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142; especially pp. 113–117, Axioms 5–6, Lemmas 3–4, and equation (22). Book catalog search.