Convex Optimization

Motivation

Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than $\mathbb R^n$.

A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).

Timeline.

• 1959: Cheney and Goldstein study proximity maps (metric projections) onto convex sets and a fixed-point construction for the distance between two convex sets (Cheney–Goldstein 1959, cited by the note as [1]).
• 1964: Goldstein, this note: the gradient projection method in Hilbert space with steps in $[\sigma, 2\rho_0 - \sigma]$.
• 1966: Levitin and Polyak give the same method and convergence rates for constrained minimization.
• 1987: Calamai and Moré extend the analysis to Armijo-type step rules and identification of the active constraints in $\mathbb R^n$ (Calamai–Moré 1987).

Setting

Let $H$ be a real Hilbert space with inner product $[x, y]$ and norm $\|x\|$. Let $C \subseteq H$ be closed and convex, and let $P : H \to H$ be the projection onto $C$: $P(x)$ is the point of $C$ closest to $x$. In Lean, IsProjection C P says that $P(x) \in C$ and $\|x - P(x)\| \le \|x - y\|$ for all $y \in C$.

Let $f : H \to \mathbb R$, $x_0 \in C$, and let

$$S = \{x \in C : f(x) \le f(x_0)\}$$

be the level set (levelSet f C x0). Let $\hat S$ be an open set containing the convex hull of $S$. Write $f'(x, h)$ for the Fréchet derivative of $f$ at $x$ applied to $h$, $\nabla f(x)$ for the gradient (so $f'(x, h) = [\nabla f(x), h]$), and

$$f''(x, h, h) = \frac{d}{dt}\Big|_{t=0} f'(x + th, h)$$

for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some $\rho_0 > 0$, at every $x \in \hat S$ and for every $h \in H$, these derivatives exist and

$$|f''(x, h, h)| \le \frac{\|h\|^2}{\rho_0}.$$

Choose $0 < \sigma \le \rho_0$ and step sizes $\sigma \le \rho_k \le 2\rho_0 - \sigma$. The method is

$$x_{k+1} = P\big(x_k - \rho_k \nabla f(x_k)\big), \qquad k \ge 0.$$

A point $z \in C$ is stationary if $P(z - \rho \nabla f(z)) = z$ for every $\rho > 0$.

Formalization targets

Goal: the THEOREM, parts (i)–(v)

Assume $f$ is bounded below and continuous on $C$. There is $L \in \mathbb R$ such that

1. (i) $x_k \in S$ for all $k$, $x_{k+1} - x_k \to 0$, and $f(x_k)$ decreases to $L$;
2. (ii) if $S$ is compact, every cluster point $z$ of $(x_k)$ near which $\nabla f$ is continuous is stationary, and a unique cluster point is the limit of $(x_k)$;
3. (iii) if $S$ is convex and $f''(x, h, h) \ge \mu \|h\|^2$ on $S$ for some $\mu \ge 0$, then

$$L = \inf\{f(x) : x \in C\};$$

4. (iv) under (iii) with $S$ bounded, every weak cluster point of $(x_k)$ minimizes $f$ on $C$;
5. (v) under (iii) with $\mu > 0$ and $\nabla f$ bounded on $S$, there is $z \in S$ with $f(z) = L$, $x_k \to z$ in norm, and $z$ is the unique minimizer of $f$ on $C$.

The goal is the whole theorem, because its five parts share one limit $L$ and one standing setting.

Milestones

The projection inequality $[x - y, P(x) - y] \ge \|P(x) - y\|^2$ for $y \in C$; the Lipschitz property of $P$; the characterization of stationarity for convex $f$ at a differentiability point; the one-step Taylor estimate; the step lemma (for $\sigma \le \rho \le 2\rho_0 - \sigma$ the new point stays in $S$ and the decrease is at least $\|x_{k+1} - x_k\|^2 \sigma / 4\rho_0^2$); parts (i) and (ii); the strong-convexity bound $f(x) \ge f(y) + [\nabla f(y), x - y] + \frac12\mu\|x - y\|^2$ on $S$; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of $f$ on $C$.

Significance

The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.

Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.

Difficulty

The obvious argument for (i) applies a quadratic upper bound for $f$ along the segment from $x_k$ to $x_{k+1}$. That bound is only available where the curvature hypothesis holds, on $\hat S$, and nothing guarantees in advance that $x_{k+1}$, or the segment, lies in $\hat S$. Ruling this out requires control of $f$ up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.

Formalization scope

• $H$ is a real Hilbert space: [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product $[x, y]$ is ⟪x, y⟫_ℝ, and $\nabla f$ is Mathlib's gradient f.
• $P$ is any map with IsProjection C P; there is no chosen projection and no junk value.
• $f''(x, h, h)$ is the derivative at $t = 0$ of $t \mapsto f'(x + th, h)$. The hypothesis on $\hat S$ (SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.
• The run starts at $x_0$, and $0 < \sigma \le \rho_0$ makes the step window nonempty.
• "$L = \inf$" is IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.
• Added hypothesis: $f$ is continuous on $C$. Part (i) as printed is false without it: on $H = C = \mathbb R$ with $P = \mathrm{id}$, $f(x) = (x - 2)^2$ for $x < 1$ and $f(x) = 100$ for $x \ge 1$, $x_0 = 0$, $\hat S = (-1, 1)$, $\rho_0 = 1/2$, $\sigma = 1/4$, $\rho_k = 1/2$, the first step lands at $x_1 = 2$ with $f(x_1) = 100 > f(x_0)$.
• Moved clause. The last clause of (ii), "$z$ minimizes $f$ on $C$", is false for nonconvex $f$ (a unique cluster point can be a stationary point that is not a minimizer). The goal omits it, and a companion item states it under convexity of $f$ on $C$.
• The goal assumes nothing about the step decrease, the step size $\hat\rho$ of the proof, or the iterates beyond the run's definition. A formalization that adds such facts as hypotheses, or that proves only one of the five parts, does not count as closing the goal.

Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).

Selected references

• A. A. Goldstein, Convex programming in Hilbert space, Bull. Amer. Math. Soc. 70 (1964), 709–710. https://doi.org/10.1090/s0002-9904-1964-11178-2
• E. W. Cheney and A. A. Goldstein, Proximity maps for convex sets, Proc. Amer. Math. Soc. 10 (1959), 448–450.
• A. V. Balakrishnan, An operator theoretic formulation of a class of control problems and a steepest descent method of solution, J. SIAM Control Ser. A 1 (1963), 109–127.
• E. S. Levitin and B. T. Polyak, Constrained minimization methods, USSR Comput. Math. Math. Phys. 6(5) (1966), 1–50.
• P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), 93–116. https://doi.org/10.1007/BF02592073

Why closed-form ADMM updates for ℓ1 problems

Many estimation problems in statistics, machine learning and signal processing minimize a smooth loss plus a nonsmooth ℓ1-type regularizer: the lasso, basis pursuit, least absolute deviations, Huber fitting, the group lasso, and ℓ1-penalized maximum likelihood for Gaussian graphical models. Chapter 6 of Boyd, Parikh, Chu, Peleato and Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Found. Trends Mach. Learn. 3(1), 2011), shows that the alternating direction method of multipliers (ADMM) splits each of these problems into a step that touches only the loss and a step that touches only the regularizer, and that each step has a closed form. The practical value of ADMM on these problems rests entirely on those closed forms: an iteration is one cached linear solve, one projection, or one thresholding.

The capstone is sparse inverse covariance selection (§6.5), the ℓ1-penalized Gaussian maximum-likelihood problem of Banerjee, El Ghaoui and d'Aspremont (2008), also solved by the graphical lasso of Friedman, Hastie and Tibshirani (2008). Its ADMM X-update minimizes a log-determinant objective over positive definite matrices, and the book shows that it is solved exactly by one symmetric eigenvalue decomposition.

Setting

All vectors are real and $\|\cdot\|_2$ is the Euclidean norm. For $\kappa\in\mathbb R$ the soft thresholding operator is $S_\kappa(a)=a-\kappa$ if $a>\kappa$, $0$ if $|a|\le\kappa$, and $a+\kappa$ if $a<-\kappa$, applied componentwise to vectors and entrywise to matrices. The vector soft thresholding operator on $\mathbb R^m$ is $\mathcal S_\kappa(a)=(1-\kappa/\|a\|_2)_+a$, with $\mathcal S_\kappa(0)=0$. The Huber penalty is $g^{\mathrm{hub}}(a)=a^2/2$ for $|a|\le1$ and $|a|-1/2$ for $|a|>1$, summed over components for vectors.

In scaled-form ADMM for minimizing $f(x)+g(z)$ subject to $Ax+Bz=c$, with penalty $\rho>0$ and scaled dual variable $u$, the updates are

$$x^{k+1}=\operatorname*{argmin}_x\bigl(f(x)+\tfrac\rho2\|Ax+Bz^k-c+u^k\|_2^2\bigr),\quad z^{k+1}=\operatorname*{argmin}_z\bigl(g(z)+\tfrac\rho2\|Ax^{k+1}+Bz-c+u^k\|_2^2\bigr),$$

followed by $u^{k+1}=u^k+Ax^{k+1}+Bz^{k+1}-c$. "The update is given by formula $F$" means $F$ is the unique minimizer of the corresponding subproblem.

For sparse inverse covariance selection, $S\in\mathbb R^{n\times n}$ is symmetric (the empirical covariance), $\lambda>0$ is the regularization weight, $\|M\|_F^2=\sum_{ij}M_{ij}^2$, $\|M\|_1=\sum_{ij}|M_{ij}|$, and $\mathbb S^n_{++}$ is the set of symmetric positive definite matrices, the domain of $\log\det$. ADMM alternates

$$X^{k+1}=\operatorname*{argmin}_{X\in\mathbb S^n_{++}}\Bigl(\operatorname{Tr}(SX)-\log\det X+\tfrac\rho2\|X-Z^k+U^k\|_F^2\Bigr),\qquad Z^{k+1}=\operatorname*{argmin}_Z\Bigl(\lambda\|Z\|_1+\tfrac\rho2\|X^{k+1}-Z+U^k\|_F^2\Bigr),$$

and $U^{k+1}=U^k+X^{k+1}-Z^{k+1}$.

Formalization targets

Goal: the X-update in closed form (§6.5, p. 47)

Let $S$ and $Z-U$ be symmetric, $\rho>0$, and $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu_1,\dots,\mu_n)\,Q^T$ with $Q^TQ=QQ^T=I$. Then

$$X=Q\,\mathrm{diag}\Bigl(\frac{\mu_i+\sqrt{\mu_i^2+4\rho}}{2\rho}\Bigr)Q^T$$

is positive definite and is the unique minimizer of $\operatorname{Tr}(SX')-\log\det X'+\frac\rho2\|X'-Z+U\|_F^2$ over $X'\in\mathbb S^n_{++}$.

Milestones

1. Scalar root (p. 47): for $\rho>0$, $t=(\mu+\sqrt{\mu^2+4\rho})/(2\rho)$ is positive and $\rho t-1/t=\mu$.
2. Equation (6.5) (p. 47): the matrix $X$ above is positive definite and $\rho X-X^{-1}=\rho(Z-U)-S$.
3. First-order condition (p. 47): a positive definite $X$ minimizes the X-objective over $\mathbb S^n_{++}$ if and only if $S-X^{-1}+\rho(X-Z+U)=0$.
4. Z-update (p. 47): $Z_{ij}=S_{\lambda/\rho}(X_{ij}+U_{ij})$ is the unique minimizer of $\lambda\|Z\|_1+\frac\rho2\|X-Z+U\|_F^2$.
5. Huber z-update (§6.1.1, p. 40): with $v=Ax-b+u$, $z=\frac{\rho}{1+\rho}v+\frac1{1+\rho}S_{1+1/\rho}(v)$ minimizes $g^{\mathrm{hub}}(z)+\frac\rho2\|Ax-z-b+u\|_2^2$.
6. Basis pursuit (§6.2, p. 41): if $AA^T$ is invertible, $(I-A^T(AA^T)^{-1}A)(z-u)+A^T(AA^T)^{-1}b$ is the projection of $z-u$ onto $\{x\mid Ax=b\}$.
7. Lasso (§6.4, p. 43): $(A^TA+\rho I)^{-1}(A^Tb+\rho(z-u))$ minimizes $\frac12\|Ax-b\|_2^2+\frac\rho2\|x-z+u\|_2^2$, and $S_{\lambda/\rho}(x+u)$ minimizes $\lambda\|z\|_1+\frac\rho2\|x-z+u\|_2^2$.
8. Group lasso (§6.4.2, p. 45): blockwise $\mathcal S_{\lambda/\rho}(x_i+u_i)$ minimizes $\lambda\sum_i\|z_i\|_2+\frac\rho2\sum_i\|x_i-z_i+u_i\|_2^2$.

Significance

The closed forms are what make ADMM competitive on these problems. For the lasso the x-update is a ridge regression whose factorization is computed once; for basis pursuit it is a cached projection; the ℓ1 step is a componentwise threshold. For covariance selection the X-update costs one eigenvalue decomposition, and the book (p. 46) cites Scheinberg, Ma and Goldfarb (2010) as showing that ADMM outperforms state-of-the-art methods on this problem. The goal also yields that $X^{k+1}$ is always positive definite, so the iterates remain in the domain of $\log\det$ without a line search.

All statements here are classical and their proofs are elementary convex analysis and linear algebra. A search of the platform found no machine-checked version of any of them. Formalizing them produces verified proximity operators (soft thresholding, vector soft thresholding, Huber, projection onto an affine set) and a verified matrix-function argument for $\log\det$ that later missions on ADMM, proximal methods and Gaussian graphical models can import.

Difficulty

The vector updates reduce to separable one-dimensional problems or to a normal equation, and the difficulty there is bookkeeping: uniqueness, the case $a=0$ of vector soft thresholding, and the three regimes of the Huber prox.

The goal is harder. The book's argument says that $X$ satisfies the gradient equation "and thus minimizes the X-minimization objective". Checking the equation is algebra; the claim to be proved is minimality over the open cone $\mathbb S^n_{++}$, which needs the convexity (indeed strict convexity, for uniqueness) of $-\log\det$ on positive definite matrices and the identification of its gradient with $-X^{-1}$ along symmetric directions. Mathlib has determinants and positive definiteness; a usable convexity statement for $\log\det$ on $\mathbb S^n_{++}$ is not among the platform's published results. Showing that $X$ satisfies (6.5) alone does not establish the goal.

Formalization scope

• Carriers. Vectors are EuclideanSpace ℝ (Fin n), matrices Matrix (Fin m) (Fin n) ℝ acting by Matrix.toEuclideanLin. The Frobenius norm and the entrywise ℓ1 norm are written as explicit sums, not through Mathlib's matrix norm instances. The vector ℓ1 norm is the platform definition HighDimStat.SparseLinear.l1Norm.
• Updates as unique minimizers. Each update is stated as: the book's formula is the unique minimizer of the subproblem (IsUniqueMinimizerOn). Iterates are not defined; the subproblem's data ($z^k$, $u^k$, $x^{k+1}$) are arbitrary.
• Domain of log det. The X-objective is minimized over Matrix.PosDef only. Singular or indefinite matrices are never competitors, so Real.log of a nonpositive determinant plays no role.
• Explicit hypotheses. $S$ and $Z-U$ are assumed symmetric in the goal and the first-order condition; $S$ need not be positive semidefinite. $\rho>0$ everywhere. Basis pursuit assumes $\det(AA^T)\ne0$, which the book uses without stating. The book's $\lambda>0$ is relaxed to $\lambda\ge0$ in the thresholding statements, which contain the book's case.
• Eigendecomposition. The goal holds for every orthogonal $Q$ and real $\mu$ with $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu)Q^T$, not for one decomposition chosen by Mathlib.
• Names. The book uses $\lambda$ for both the regularization weight and the eigenvalues; Lean calls them lam and μ.
• Typo. The book prints $u^k$ in the group-lasso block update; the block $u_i^k$ is stated.
• Ruled out. A goal that only asserts that $X$ satisfies (6.5), or that minimizes over a set extended by Real.log of nonpositive determinants, is not the book's claim; the goal states unique minimality over $\mathbb S^n_{++}$.
• Not stated. Least absolute deviations and the generalized lasso updates (same pattern as milestones 5 and 7), the overlapping group lasso, and the two-step termination claim for Huber fitting on p. 40 (whose formula $x^{\mathrm{ls}}=(A^TA)^{-1}b$ is misprinted).

Contributions welcome: convexity and strict convexity of $-\log\det$ on $\mathbb S^n_{++}$ and its derivative; a general "prox of a separable function is componentwise" lemma; and the projection onto an affine set.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
• O. Banerjee, L. El Ghaoui, A. d'Aspremont, Model Selection Through Sparse Maximum Likelihood Estimation for Multivariate Gaussian or Binary Data, Journal of Machine Learning Research 9, 2008, pp. 485–516. https://jmlr.org/papers/v9/banerjee08a.html
• J. Friedman, T. Hastie, R. Tibshirani, Sparse Inverse Covariance Estimation with the Graphical Lasso, Biostatistics 9(3), 2008, pp. 432–441. https://doi.org/10.1093/biostatistics/kxm045
• K. Scheinberg, S. Ma, D. Goldfarb, Sparse Inverse Covariance Selection via Alternating Linearization Methods, Advances in Neural Information Processing Systems 23, 2010 (reference [148] of the book).
• R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society B 58(1), 1996, pp. 267–288. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• M. Yuan, Y. Lin, Model Selection and Estimation in Regression with Grouped Variables, Journal of the Royal Statistical Society B 68(1), 2006, pp. 49–67. https://doi.org/10.1111/j.1467-9868.2005.00532.x

Why consensus and sharing

Many large optimization problems arising in statistics, machine learning, signal processing and resource allocation have an objective that is a sum of terms, each depending on data held by a different processor, or a coupling term that depends on the sum of the agents' decisions. Chapter 7 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) introduces two templates that turn such problems into distributed algorithms: consensus and sharing. Nearly every distributed application in the rest of the monograph (distributed lasso, distributed logistic regression, splitting across examples and across features in Chapter 8) is an instance of one of the two. Consensus problems in the context of ADMM go back to Bertsekas and Tsitsiklis (Parallel and Distributed Computation, 1989).

The value of the templates lies in a handful of exact algebraic facts about the ADMM subproblems: the global update is an average, the dual variables average to zero, and the sharing update, which looks like a problem in $Nn$ variables, is really a problem in $n$ variables. These facts are what this mission formalizes.

Setting

There are $N\ge1$ agents. Vectors live in $\mathbb R^n$ with the Euclidean inner product, and an overline denotes an average over agents, $\bar v=\frac1N\sum_{i=1}^N v_i$. Each local cost $f_i$ and the shared cost $g$ are functions into $\mathbb R\cup\{+\infty\}$. The penalty parameter is $\rho>0$.

Global variable consensus (§7.1) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)\quad\text{subject to } x_i-z=0,\ i=1,\dots,N,$$

with local variables $x_i\in\mathbb R^n$ and a global variable $z$. ADMM alternates a parallel $x_i$-update, an averaging $z$-update and a dual update of the multipliers $y_i$. With a regularizer $g(z)$ added (7.2), the $z$-update (7.4) becomes a minimization involving $g$.

General form consensus (§7.2) lets local variable $x_i\in\mathbb R^{n_i}$ copy only some entries of $z$: entry $j$ of $x_i$ corresponds to entry $z_{\mathcal G(i,j)}$, and $\tilde z_i\in\mathbb R^{n_i}$ is defined by $(\tilde z_i)_j=z_{\mathcal G(i,j)}$. The number of local entries copying $z_g$ is $k_g$.

Sharing (§7.3) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)+g\Big(\sum_{i=1}^N x_i\Big),\tag{7.11}$$

written for ADMM with copies $z_i$ of the $x_i$ (7.12). In scaled form, with $a_i=u_i^k+x_i^{k+1}$, its $z$-update is

$$(z_1^{k+1},\dots,z_N^{k+1})\in\operatorname*{argmin}_{z_1,\dots,z_N}\ g\Big(\sum_{i=1}^N z_i\Big)+(\rho/2)\sum_{i=1}^N\|z_i-a_i\|_2^2,$$

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z_i^{k+1}$.

Formalization targets

Goal: the sharing $z$-update reduction (§7.3, p. 57)

For every $a_1,\dots,a_N$: $(z_1,\dots,z_N)$ solves the $Nn$-variable $z$-update iff $\bar z$ solves

$$\operatorname*{minimize}_{\bar z\in\mathbb R^n}\ g(N\bar z)+(\rho/2)\sum_{i=1}^N\|\bar z-\bar a\|_2^2$$

and

$$z_i=a_i+\bar z-\bar a\quad (7.13);$$

and along every run of sharing ADMM,

$$u_i^{k+1}=\bar u^k+\bar x^{k+1}-\bar z^{k+1}\quad(7.14),$$

so all scaled dual variables agree after one step.

Milestones

• §7.1: the consensus $z$-update is $z^{k+1}=\bar x^{k+1}+(1/\rho)\bar y^k$; then $\bar y^{k+1}=0$, $z^k=\bar x^k$ and the simplified iteration.
• (7.4), §7.1.1: with a regularizer, the $z$-update is averaging followed by a proximal step with weight $N\rho$; the soft-threshold ($g=\lambda\|\cdot\|_1$) and positive-part ($g$ the indicator of $\mathbb R^n_+$) examples.
• §7.2: the general form $z$-update is local averaging, and the dual entries attached to each global index sum to zero after the first iteration.
• (7.13): with $\bar z$ fixed, $z_i=a_i+\bar z-\bar a$ is the unique minimizer.

Significance

The reduction is what makes sharing ADMM scale: the central step needs only the averages $\bar x^{k+1}$, $\bar u^k$ and one $n$-dimensional proximal problem, regardless of the number of agents, and the dual state collapses to a single vector. The same reduction underlies exchange ADMM (§7.3.2) and the splitting-across-features algorithms of §8.3. The consensus facts explain why the fusion center only averages and why the dual variables can be dropped from its update.

All results of the chapter are proved, informally, in the monograph; they are elementary. To our knowledge none has a machine-checked proof. The mission produces checked statements of the update formulas that later chapters of the series and distributed-optimization developments can cite instead of re-deriving.

Difficulty

The statements are exact identities between minimizer sets of nonsmooth problems in which $g$ may be any extended-real-valued function: there is no first-order condition to use, so each step must be argued by comparing objective values, and the iff requires producing, for an arbitrary competitor, a competitor of the reduced problem with no larger value. The index bookkeeping is the other half: averages of sums of sequences indexed by agents and by iterations, the off-by-one in "after the first iteration", and in §7.2 sums over the fibres $\{(i,j):\mathcal G(i,j)=g\}$ of an index map between local vectors of different dimensions.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n); agents are indexed by Fin N, so the book's $i=1,\dots,N$ is Lean's $i-1$; components are 0-based as well.
• An extended-real-valued function is encoded by its effective domain (a set) and its finite values; every minimization is over the domain. Convexity is not assumed: none of the stated identities needs it, so the statements are slightly more general than the chapter's standing assumption that each $f_i$ is convex.
• Iterates are hypotheses: a run is any sequence satisfying the update rules (argmin properties, not chosen minimizers). The consensus run uses the averaging formula exactly as printed on p. 49; the general form and sharing runs use the argmin form printed on pp. 55–56.
• Explicit hypotheses that the book leaves implicit: $N\ge1$, $\rho>0$, $\lambda>0$ (named lam), $k_g\ge1$ for every global index $g$ in §7.2, and the index ranges $k\ge1$ for $\bar y^{k}=0$ and $k\ge2$ for $z^k=\bar x^k$ (the starting $y^0$ is arbitrary).
• Corrected misprints: p. 52 prints $\bar x^{k+1}-(1/\rho)\bar y^k$ in the soft-threshold and positive-part examples, while the proximal form gives $\bar x^{k+1}+(1/\rho)\bar y^k$; p. 55 prints $\sum_{i=1}^m$ for $\sum_{i=1}^N$; p. 57 writes $u\in\mathbf R^m$ for a vector of $\mathbb R^n$.
• The goal is about minimizers of the $Nn$-variable $z$-subproblem, not the algebraic identity (7.13) alone, and (7.14) is derived for every run rather than built into a single-dual-variable definition; either shortcut would make the goal trivial.
• Not included: the consensus residual norms (p. 51), the duality discussion of §7.3.1 and exchange ADMM (§7.3.2). Contributions formalizing them on top of these definitions are welcome.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 1–122, 2011. https://doi.org/10.1561/2200000016
• D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://web.mit.edu/dimitrib/www/pdc.html

Motivation

In data-driven stochastic optimization a decision maker knows the distribution of an uncertain parameter $\xi$ only through $N$ samples $\hat\xi_1,\dots,\hat\xi_N$. Wasserstein distributionally robust optimization hedges against this ignorance by evaluating a loss $\ell$ under the worst distribution in a ball, measured in the Wasserstein metric, around the empirical distribution of the samples. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) showed that for piecewise concave losses the worst-case expectation is the optimal value of a finite convex program (their Theorem 4.2), which made the approach computationally practical.

Knowing the worst-case value is often not enough. Stress tests of a candidate decision require the extremal distributions themselves: the distributions inside the ball that (nearly) achieve the worst case. Section 4.2 of the paper answers this question. Its Theorem 4.4 shows that the worst case is approached by discrete distributions with at most $NK$ atoms, read off from near-optimal solutions of a second finite convex program, and its Example 2 shows that a worst-case distribution need not exist at all. This mission formalizes that section. The source is the arXiv preprint version 3 (13 June 2017); all numbering below refers to it.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbb R^m$), equipped with its Borel $\sigma$-algebra. Linear functionals $z$ on $E$ act by $\langle z,\xi\rangle$, and the dual norm is $\|z\|_* = \sup_{\|\xi\|\le 1}\langle z,\xi\rangle$. Extended reals $\overline{\mathbb R} = [-\infty,+\infty]$ follow the paper's conventions $0\cdot\infty = 0/0 = 0$ and $\infty - \infty = \infty$.

• Samples and empirical distribution. $\hat\xi_1,\dots,\hat\xi_N$ lie in a set $\Xi\subseteq E$, and $\widehat{\mathbb P}_N = \frac1N\sum_i\delta_{\hat\xi_i}$.
• Wasserstein ball. $d_W(\mathbb Q_1,\mathbb Q_2)$ is the infimum of $\int\|\xi_1-\xi_2\|\,\Pi(d\xi_1,d\xi_2)$ over couplings $\Pi$ of $\mathbb Q_1$ and $\mathbb Q_2$, and $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ is the set of probability distributions supported on $\Xi$ within distance $\varepsilon$ of $\widehat{\mathbb P}_N$.
• Loss. $\ell(\xi) = \max_{k\le K}\ell_k(\xi)$ for measurable pieces $\ell_k : E\to\overline{\mathbb R}$, and $\mathbb E^{\mathbb Q}[\ell(\xi)] = \mathbb E^{\mathbb Q}[\max\{\ell,0\}] + \mathbb E^{\mathbb Q}[\min\{\ell,0\}]$.
• Worst-case expectation (10). $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)]$.
• Assumption 4.1. $\Xi$ is convex and closed; every $-\ell_k$ is proper, convex and lower semicontinuous; and no $\ell_k$ is identically $-\infty$ on $\Xi$.
• Program (13). Over weights $\alpha_{ik}\ge 0$ and displacements $q_{ik}\in E$,

$$\sup_{\alpha_{ik},q_{ik}}\ \frac1N\sum_{i=1}^N\sum_{k=1}^K\alpha_{ik}\,\ell_k\Big(\hat\xi_i-\frac{q_{ik}}{\alpha_{ik}}\Big)\quad\text{s.t.}\quad\frac1N\sum_{i,k}\|q_{ik}\|\le\varepsilon,\ \ \sum_k\alpha_{ik}=1,\ \ \hat\xi_i-\frac{q_{ik}}{\alpha_{ik}}\in\Xi .$$

When $\alpha_{ik}=0$ the last constraint forces $q_{ik}=0$ and the $ik$-th objective term is $0$.

• Candidate distributions. $\mathbb Q = \frac1N\sum_{i,k}\alpha_{ik}\,\delta_{\xi_{ik}}$ with $\xi_{ik} = \hat\xi_i - q_{ik}/\alpha_{ik}$.

Formalization targets

Goal: Theorem 4.4 (worst-case distributions)

Under Assumption 4.1 and for every $\varepsilon\ge 0$,

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)] = \text{optimal value of (13)},$$

and for every feasible sequence $(\alpha_{ik}(r),q_{ik}(r))_r$ of (13) whose objective values converge to that optimal value, the distributions $\mathbb Q_r$ lie in $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ and

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)] = \lim_{r\to\infty}\mathbb E^{\mathbb Q_r}[\ell(\xi)] = \lim_{r\to\infty}\frac1N\sum_{i,k}\alpha_{ik}(r)\,\ell(\xi_{ik}(r)).$$

The limits may be $+\infty$; no finiteness is assumed.

Milestones, in the order of the proof

The proof starts from (10) = (12f) (proof of Theorem 4.2, p. 13), which is posed in mission I of this series, Wasserstein Worst-Case Expectations as Finite Convex Programs, and is not restated here; it will be linked as a milestone once that mission is live.

1. Lemma 4.5: $\inf_z\langle z,q-\alpha\hat\xi\rangle+\alpha f^*(z)$ is the extended perspective of $q\mapsto -f(\hat\xi-q)$ for proper, convex, lower semicontinuous $f$.
2. (14d)–(14f): the $ik$-th dual term equals $\alpha\ell_k(\hat\xi-q/\alpha)-\chi_\Xi(\hat\xi-q/\alpha)$ under the extended-arithmetic conventions.
3. (12f) = (13), the first part of the proof of Theorem 4.4.
4. $\mathbb Q_r\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ for every feasible point of (13).
5. $\mathbb E^{\mathbb Q_r}[\ell(\xi)]$ equals $\frac1N\sum_{i,k}\alpha_{ik}\ell(\xi_{ik})$ and is at least the objective of (13) for every feasible point.

Companion results

Corollary 4.6: if $\Xi$ is compact or $K=1$, the sequence has an accumulation point that defines a worst-case distribution. Example 2: for $\Xi=\mathbb R$, $N=1$, $\hat\xi_1=0$, $\ell=\max\{0,\xi-1\}$, the worst-case expectation is $\varepsilon$ and, for $\varepsilon>0$, is attained by no distribution in the ball.

Significance

Theorem 4.4 turns the abstract supremum over an infinite-dimensional ball of distributions into a finite-dimensional convex program whose near-optimal solutions are near-worst-case distributions. The atoms $\xi_{ik}$ sit within total weighted distance $\sum_{i,k}\alpha_{ik}\|\xi_{ik}-\hat\xi_i\|\le N\varepsilon$ of the data, and they may lie off the data, which distinguishes Wasserstein balls from ambiguity sets based on the total variation distance or the Kullback–Leibler divergence. Example 2 marks the boundary: the theorem cannot be upgraded to the existence of a maximizer in general, while Corollary 4.6 names two cases where it can.

The results are proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a precise account of the extended-arithmetic conventions the paper relies on ($0\cdot\infty=0$, $q/0\notin E$, $\infty-\infty=\infty$), each of which is made explicit in the definitions, and a reusable Lean treatment of extended-valued conjugates and perspective functions on a normed space with an arbitrary norm.

Difficulty

The first claim goes through Lagrangian duality for program (12f), whose constraints involve conjugates that may take the value $+\infty$; the strong duality and the minimax interchange (14c) must be justified for extended-valued convex functions, not just finite ones. Lemma 4.5 needs the Fenchel–Moreau theorem $f^{**}=f$ for proper, convex, lower semicontinuous $\overline{\mathbb R}$-valued functions on a finite-dimensional normed space, together with its degenerate case $\alpha=0$. The second claim is a squeeze argument, but it rests on computing an extended expectation of an $\overline{\mathbb R}$-valued function under a discrete measure and on an explicit coupling for the Wasserstein distance. A tempting shortcut, attaining the supremum by a limit distribution, fails: Example 2 shows the maximizing atoms can escape to infinity.

Formalization scope

• The space is a finite-dimensional real normed space E with [BorelSpace E]; the dual space is StrongDual ℝ E, and the dual norm is the operator norm. All values are in EReal.
• The Wasserstein distance, the ball (6) and $\widehat{\mathbb P}_N$ are the published WassersteinDRO.Duality.wassersteinDistance, ambiguitySet (with $p=1$) and empiricalDistribution.
• The extended expectation is the published DupacovaWets.Consistency.expect; it integrates the positive and negative parts separately and returns $+\infty$ when the positive part is infinite; there is no integrability guard, so a distribution with infinite expected loss pushes (10) to $+\infty$ as in the paper.
• Program values are infima or suprema over feasibility predicates, so an empty feasible set gives $\pm\infty$, never a junk $0$. Program (13) encodes $\alpha_{ik}=0$ by the clauses "$q_{ik}=0$" and "objective term $=0$" (p. 14).
• Standing assumptions carried as hypotheses: $N\ge1$, $K\ge1$, $\hat\xi_i\in\Xi$ (§2), measurability of each $\ell_k$ (p. 11).
• A trivializing formalization is ruled out: dropping the clause $\alpha_{ik}=0\Rightarrow q_{ik}=0$ or the hypothesis $\hat\xi_i\in\Xi$ would change program (13) or make the ball empty, and both are kept explicitly.
• The objects shared with mission I (extended expectation, worst-case expectation, conjugate, Assumption 4.1, program (12f)) are restated verbatim in this mission's namespace; they will be merged with mission I's copies. Contributions to the convex-analysis groundwork (extended-valued Fenchel–Moreau, perspective functions) are welcome and reusable beyond this mission.

Selected references

• P. Mohajerin Esfahani and D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric: Performance Guarantees and Tractable Reformulations, Mathematical Programming 171, 2018. Version formalized: arXiv:1505.05116v3.
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (Propositions 1.6.1 and 5.5.4, used in the proofs).
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Motivation

A decision maker who must minimize an expected cost $\mathbb E^{\mathbb P}[h(x,\xi)]$ rarely knows the distribution $\mathbb P$ of the uncertain parameter $\xi$; usually only $N$ samples $\hat\xi_1,\dots,\hat\xi_N$ are available. Replacing $\mathbb P$ by the empirical distribution (sample average approximation) tends to produce decisions that perform poorly out of sample when $N$ is small. Distributionally robust optimization instead minimizes the worst expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take that set to be a ball in the Wasserstein metric around the empirical distribution. Such balls give finite-sample and asymptotic guarantees, but each evaluation of the robust objective is an optimization over infinitely many probability distributions. Section 4.1 of the paper shows that, for a large class of losses, this inner problem is a finite convex program. That result, Theorem 4.2, is the subject of this mission.

Timeline. Wasserstein ambiguity sets for portfolio selection were proposed by Pflug and Wozabal (2007); before this paper, robust problems over such sets were solved with global optimization algorithms (Pflug and Pichler 2014). Strong duality for conic linear and moment problems (Shapiro 2001) underlies the reduction. Mohajerin Esfahani and Kuhn (preprint 2015, journal 2018) proved the convex reduction for piecewise concave losses; Gao and Kleywegt (arXiv:1604.02199) and Blanchet and Murthy (arXiv:1604.01446) proved strong duality for general transport costs in 2016.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbb R^m$) and its Borel σ-algebra. Its dual norm is $\|z\|_* = \sup_{\|\xi\|\le 1}\langle z,\xi\rangle$, where $\langle z,\xi\rangle$ is the value of the linear functional $z$ at $\xi$. Let $\Xi\subseteq E$ be the support set and $\hat\xi_1,\dots,\hat\xi_N\in\Xi$ the samples, with empirical distribution $\widehat{\mathbb P}_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$.

The 1-Wasserstein distance between two distributions is the least transport cost $\int\|\xi-\xi'\|\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ with the given marginals. The Wasserstein ball $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ is the set of probability distributions on $\Xi$ within distance $\varepsilon\ge 0$ of $\widehat{\mathbb P}_N$.

The loss is a pointwise maximum $\ell(\xi)=\max_{k\le K}\ell_k(\xi)$ of measurable functions $\ell_k:E\to\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$. Its expectation is $\mathbb E^{\mathbb Q}[\ell]=\mathbb E^{\mathbb Q}[\max\{\ell,0\}]+\mathbb E^{\mathbb Q}[\min\{\ell,0\}]$ with $\infty-\infty=\infty$. The worst-case expectation is

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)].\tag{10}$$

The conjugate of $f:E\to\overline{\mathbb R}$ is $f^*(z)=\sup_\xi\langle z,\xi\rangle-f(\xi)$, the characteristic function $\chi_\Xi$ is $0$ on $\Xi$ and $+\infty$ off it, and the support function is $\sigma_\Xi(z)=\sup_{\xi\in\Xi}\langle z,\xi\rangle$. Assumption 4.1 requires $\Xi$ to be convex and closed, each $-\ell_k$ to be proper, convex and lower semicontinuous, and no $\ell_k$ to be identically $-\infty$ on $\Xi$.

Formalization targets

Goal: Theorem 4.2 (convex reduction)

Under Assumption 4.1, for every $\varepsilon\ge0$, (10) equals

$$\inf_{\lambda,s_i,z_{ik},\nu_{ik}}\ \lambda\varepsilon+\frac1N\sum_{i=1}^N s_i\quad\text{s.t.}\quad [-\ell_k]^*(z_{ik}-\nu_{ik})+\sigma_\Xi(\nu_{ik})-\langle z_{ik},\hat\xi_i\rangle\le s_i,\ \ \|z_{ik}\|_*\le\lambda\quad\forall i,k.\tag{11}$$

Milestones, in the order of the paper's proof

1. (12a)–(12c). Without any convexity, (10) is at most the value of (12c): $\inf\{\lambda\varepsilon+\frac1N\sum_i s_i:\ \sup_{\xi\in\Xi}(\ell(\xi)-\lambda\|\xi-\hat\xi_i\|)\le s_i,\ \lambda\ge0\}$.
2. Corollary 4.3. Without Assumption 4.1, (10) is at most the value of (12f), the program with constraints $[-\ell_k+\chi_\Xi]^*(z_{ik})-\langle z_{ik},\hat\xi_i\rangle\le s_i$ and $\|z_{ik}\|_*\le\lambda$.
3. (12a) is an equality for $\varepsilon>0$ under Assumption 4.1.
4. The case $\varepsilon=0$. (10) is the sample average $\frac1N\sum_i\ell(\hat\xi_i)$, the objective of (12b) converges to it as $\lambda\to\infty$, and (12a) is again an equality.
5. (12e) is an equality. For each constraint, $\sup_{\xi\in\Xi}(\ell_k(\xi)-\lambda\|\xi-\hat\xi_i\|)=\min_{\|z\|_*\le\lambda}\sup_{\xi\in\Xi}(\ell_k(\xi)-\langle z,\xi-\hat\xi_i\rangle)$.
6. (10) equals (12f) under Assumption 4.1.
7. (12f) equals (11) under Assumption 4.1, as optimal values.

Significance

Theorem 4.2 is what makes Wasserstein distributionally robust optimization computable. Once the worst-case expectation is a convex program in $(\lambda,s,z,\nu)$, minimizing over the decision $x$ becomes one larger convex program. Section 5 of the paper derives linear and conic programs from it for piecewise affine losses, uncertainty quantification and two-stage problems. Theorem 4.4 of the same paper (mission II of this series) builds worst-case distributions from the same program. Corollary 4.3 gives a conservative convex bound for losses that are not piecewise concave.

The result is proved on paper; no machine-checked proof of it is known. A formal development needs a working theory of extended-valued conjugates, support functions and inf-convolution in a normed space, Kantorovich-type couplings of an empirical measure, and a minimax theorem over a compact dual ball. Each of these is reusable well beyond this paper.

Difficulty

The weak inequality, (10) $\le$ (12f), is the elementary direction: integrate a pointwise bound against a near-optimal coupling. The difficulty lies in the two equalities. Equality in (12a) is strong duality for an infinite-dimensional moment problem whose loss may take the values $\pm\infty$ and may be unbounded on an unbounded $\Xi$. A Slater point exists only for $\varepsilon>0$, so $\varepsilon=0$ needs a separate limit argument. The equality (12f) $=$ (11) is subtle as well. The conjugate of $-\ell_k+\chi_\Xi$ is only the closure of the inf-convolution of $[-\ell_k]^*$ and $\sigma_\Xi$, so the two constraint sets differ and only the optimal values agree. The paper's sentence "cl$[f]\le 0$ iff $f\le0$" is false pointwise and cannot be formalized as written.

Formalization scope

• Space. $E$ is a finite-dimensional real normed space with its Borel σ-algebra. The pairing $\langle z,\xi\rangle$ is application of a continuous linear functional $z$, and $\|z\|_*$ is the operator norm. These choices keep the paper's arbitrary norm; §5 of the paper uses the 1- and ∞-norms.
• Extended reals. Values are in EReal. Mathlib's EReal has $\top+\bot=\bot$, whereas the paper has $\infty-\infty=\infty$, so the expectation treats an infinite positive part separately, and $[-\ell_k+\chi_\Xi]^*(z)$ is written as $\sup_{\xi\in\Xi}(\langle z,\xi\rangle+\ell_k(\xi))$, with no addition at all. The one EReal sum, $[-\ell_k]^*+\sigma_\Xi$ in (11), never meets $\top+\bot$ under Assumption 4.1.
• Programs. Each optimal value is an infimum over a feasibility predicate with real epigraph variables, so an infeasible program has value $+\infty$.
• Ball. The ball is the published WassersteinDRO.Duality.ambiguitySet with $p=1$ around empiricalDistribution. Its condition $\mathbb Q(\Xi^{\mathrm c})=0$ encodes $\mathbb Q\in\mathcal M(\Xi)$. The finite first moment is automatic at finite distance from $\widehat{\mathbb P}_N$.
• Standing assumptions. Every statement carries $N\ge1$, $K\ge1$, $\hat\xi_i\in\Xi$ (§2, p. 5) and measurability of each $\ell_k$ (p. 11). The radius condition is $\varepsilon\ge0$, or $\varepsilon>0$ in milestone 3.
• Assumption 4.1. Convexity of $-\ell_k$ is stated through its real epigraph, because ConvexOn cannot take an EReal codomain.
• Not trivializable. The statements cannot be made vacuous by an empty ball, because the samples lie in $\Xi$. They cannot be trivialized by a junk expectation either: the expectation is not guarded by integrability, so a distribution with infinite expected loss makes (10) infinite, exactly as in the paper.

Welcome contributions are reusable lemmas on EReal-valued conjugates and support functions, the decomposition of a coupling with an empirical marginal into conditional distributions, the dual-norm identity $\max_{\|z\|_*\le\lambda}\langle z,v\rangle=\lambda\|v\|$, and a Sion-type minimax theorem.

Selected references

• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, arXiv:1505.05116v3, 2017; Math. Program. 171 (2018) 115–166. https://arxiv.org/abs/1505.05116v3
• A. Shapiro, On duality theory of conic linear problems, in M. A. Goberna, M. A. López (eds.), Semi-Infinite Programming, Kluwer, 2001.
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2010 (Theorem 11.23(a), p. 493).
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (Proposition 5.5.4).
• G. Ch. Pflug, A. Pichler, Multistage Stochastic Optimization, Springer, 2014.
• G. Ch. Pflug, D. Wozabal, Ambiguity in portfolio selection, Quantitative Finance 7 (2007) 435–442.
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, arXiv:1604.01446, 2016. https://arxiv.org/abs/1604.01446

Motivation

Convex minimization often has a simple objective but no useful closed form for its minimizer. A proximal method replaces one difficult minimization by a sequence of regularized minimizations. The familiar quadratic regularizer treats all directions through a Euclidean norm. In applications with nonnegative variables, entropy-like geometry can be more natural: a step can be penalized by a Bregman distance generated by a strictly convex function. Chen and Teboulle studied a proximal minimization algorithm with this geometry and established a rate in objective values together with convergence of the iterates under the paper's assumptions. Their analysis also removed a bounded-below assumption used in an earlier treatment and allowed step sizes whose sum diverges even if individual steps approach zero (Chen and Teboulle, 1993, pp. 539–540).

This mission records the complete theorem of that paper, rather than only its rate when a minimizer is known to exist. The distinction matters because a proper convex objective can have an infimum of $-\infty$ or a finite infimum that it never attains. The rate against each comparison point remains meaningful in those cases, and the theorem's value convergence does not presuppose a minimizer.

Setting

Let $E$ be a finite-dimensional real normed space, $C\subseteq E$ the nonempty effective domain of a proper lower semicontinuous convex objective, and $f:C\to\mathbb R$ its finite restriction. Its value outside $C$ is $+\infty$. Thus $f_* = \inf_{u\in C}f(u)$ is an extended-real number that may equal $-\infty$, and $X_* = \{u\in C: f(u)\le f(v)\text{ for every }v\in C\}$ is the set of minimizers, possibly empty.

A Bregman function with zone $S$ is a function $\psi$ on the closure $\bar S$ of an open set $S$. It is continuously differentiable on $S$, strictly convex and continuous on $\bar S$, and satisfies the bounded partial-level-set and two sequential conditions of Definition 2.1 (Chen and Teboulle, 1993, p. 539). Its distance-like expression is

$$D_\psi(u,y)=\psi(u)-\psi(y)-\langle u-y,\nabla\psi(y)\rangle, \qquad u\in\bar S,\ y\in S.$$

It is nonnegative and zero exactly when $u=y$, but need not be symmetric or satisfy a triangle inequality. The zone contains the relative interior of $C$. Starting from $x^0\in S$ and positive steps $\lambda_k$, a PMD run selects $x^k\in S\cap C$ minimizing $f(u)+\lambda_k^{-1}D_\psi(u,x^{k-1})$ over $u\in C\cap\bar S$, for $k\ge1$. Write $\sigma_n=\sum_{k=1}^n\lambda_k$. The paper calls this proximal minimization with D-functions (Chen and Teboulle, 1993, pp. 539–540).

Formalization targets

Rate and value convergence

For every $n\ge1$ and every finite comparison point $u\in C\cap\bar S$, the goal includes

$$f(x^n)-f(u)\le\sigma_n^{-1}D_\psi(u,x^0).$$

If $\sigma_n\to+\infty$, then $f(x^n)\to f_*$ in the extended reals, including when $f_*=-\infty$. This is Theorem 3.4's inequality (20) and its ensuing value-convergence claim (Chen and Teboulle, 1993, p. 542).

Minimizer bound and iterate convergence

For every $x^*\in X_*$, the same rate gives

$$f(x^n)-f(x^*)\le\sigma_n^{-1}D_\psi(x^*,x^0),\qquad n\ge1.$$

When $X_*\ne\varnothing$ and $\sigma_n\to+\infty$, the entire sequence $x^n$ converges to a point of $X_*$. The displayed bound is (21), and convergence of the iterates is the final clause of Theorem 3.4. The milestone list follows the authors' statements: the three-point identity, nonnegativity of the distance, Lemma 3.2, and the three parts of Lemma 3.3. Display (17) is an additional supporting theorem item (Chen and Teboulle, 1993, pp. 539–542).

Significance

The rate compares a PMD iterate with any admissible point, so it gives a finite-horizon certificate even before an optimal point is identified. If a minimizer exists, substituting it gives an explicit objective-gap bound. With divergent cumulative steps, the theorem identifies the limiting objective value without assuming that value is finite. Its final clause goes further: when the optimum is attained, the points themselves converge, not merely their objective values (Chen and Teboulle, 1993, p. 542).

The mathematical result was proved in 1993. The formalization task is to state and prove it in Lean with the extended objective, full Bregman-function conditions, and sequence limits visible to later developments. The three-point identity is already posed as a separate public platform theorem from a later mirror-descent treatment; this mission reuses that statement. The remaining statements here are proof obligations, not claims of completed machine-checked proofs. Their definition layer can also support analyses of other nonquadratic proximal algorithms.

Difficulty

The direct one-step minimization comparison alone does not yield the global estimate with $\sigma_n$ and the exact weighted distance terms of Lemma 3.3(iii). It also does not settle convergence of the points: decreasing objective values can coexist with several cluster points. The Bregman function's bounded partial level sets and sequential conditions are needed to rule out that behavior. A further issue appears when $f_*=-\infty$: replacing the infimum by a real number, or assuming a minimizer to define it, removes a case that Theorem 3.4 explicitly covers. The original paper separates these issues across Lemmas 3.2–3.3 and Theorem 3.4 (Chen and Teboulle, 1993, pp. 540–542).

Formalization scope

Lean uses a finite-dimensional real normed space in place of $\mathbb R^n$; none of the statements depends on a chosen Euclidean inner product. A derivative is a continuous linear functional, and its value on a vector represents the paper's gradient pairing. The Bregman distance is the already-published definition with the derivative at its second argument. The paper's $\psi:\bar S\to\mathbb R$ is represented by a total function whose values outside $\bar S$ are unused. Strict convexity on $\bar S$ includes convexity of $\bar S$. The last sequential condition explicitly requires its first arguments to lie in $\bar S$, the domain where the paper defines $D_\psi$.

The extended objective is a nonempty convex domain $C$, a real-valued restriction $f$, and an extended-real function equal to $+\infty$ off $C$. Lower semicontinuity applies to that extended function. The infimum $f_*$ is taken in the extended reals; it cannot silently become zero when the values are unbounded below. A PMD run is a predicate on an existing sequence, recording a minimizer in $S\cap C$ at each step. This makes explicit the existence consequence for which the paper assumes the gradient of $\psi$ has full range; it does not define iterates by a choice operator. Every Bregman distance differentiates at a point of $S$, where $\psi$ is $C^1$. The rate starts at $n=1$, so $\sigma_n>0$ and no finite value is demanded of $x^0$. No lower bound on $f$ is imposed. Contributions proving the milestone inequalities, the extended-real value limit, the Bregman-function examples, and the compactness step for iterate convergence are within scope.

Selected references

• Gong Chen and Marc Teboulle, Convergence analysis of a proximal-like minimization algorithm using Bregman functions, SIAM Journal on Optimization 3(3), 538–543, 1993. DOI: 10.1137/0803026.