Optimization

Motivation

Gradient descent needs a step size, and the classical choices each ask for something the user may not have. A constant step $1/L$ needs the Lipschitz constant $L$ of the gradient, which is rarely known and often pessimistic. Backtracking needs repeated function evaluations. The exact line search needs a one-dimensional minimization at every iteration. Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021, doi:10.1137/20M1329858) proposed a step size for the static linear-quadratic regulator (their rule (4.8), §4.3, p. 11). In §6.1 they point out that the same rule applies to any smooth unconstrained problem $\min_{x\in\mathbb{R}^n} f(x)$. The rule divides the squared gradient norm by the Hessian quadratic form along the gradient. It needs one Hessian–vector product per iteration and neither $L$ nor the strong convexity constant $\mu$. In the paper's LQR experiment (§5, Figure 8, p. 13) the algorithm built on this step converges much faster than gradient descent with a constant step tuned at the first iterations.

The paper proves the method converges linearly for strongly convex functions (Theorem 6.1, p. 13). The proof takes one page (Appendix D.4, p. 19). This mission formalizes that theorem. It is the third mission of a series on this paper; the other two concern the LQR gradient method and gradient flow, and this one uses none of their control-theoretic objects.

Setting

Let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable, with gradient $\nabla f(x)$ and Hessian $\nabla^2 f(x)$. Three constants describe it.

• $f$ is $\mu$-strongly convex, $\mu>0$: $f(ax+by)\le af(x)+bf(y)-ab\,\frac{\mu}{2}\|x-y\|^2$ for all $x,y$ and $a,b\ge0$ with $a+b=1$.
• $\nabla f$ is Lipschitz with constant $L$: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$.
• $\nabla^2 f$ is Lipschitz with constant $M$: $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ in the operator norm.

Let $x_*$ be the global minimizer of $f$. The Hessian step size at a point $x$ is

$$\gamma(x)=\frac{\|\nabla f(x)\|^2}{\langle\nabla^2 f(x)\nabla f(x),\nabla f(x)\rangle},$$

the minimizer of the second-order Taylor model of $f$ along $-\nabla f(x)$. The method (6.1) runs

$$x_{j+1}=x_j-\gamma_j\nabla f(x_j),\qquad\gamma_j=\gamma(x_j),$$

from a starting point $x_0$. The damped method with factor $\sigma>0$ runs $x_{j+1}=x_j-\sigma\gamma_j\nabla f(x_j)$. For a quadratic $f(x)=\langle Hx,x\rangle$ the method (6.1) is steepest descent with exact line search.

Formalization targets

Goal: Theorem 6.1 (p. 13), both parts

Under the hypotheses above:

1. If $\delta>0$ and $M\sqrt{2L(f(x_0)-f(x_*))}\le3\mu^2(1-\delta)$ (condition (6.2)), the iterates of (6.1) satisfy

$$f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\delta}{L}\Bigr)^j\quad\text{for all }j.\tag{6.3}$$

2. If $0<\sigma\le\mu/L$, the damped iterates from any $x_0$ satisfy

$$f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\sigma}{L}\Bigr)^j\quad\text{for all }j.\tag{6.4}$$

The constants are the paper's, stated exactly.

Milestones (Appendix D.4, p. 19)

• Cubic Taylor bound (first display): $\bigl|f(x+y)-f(x)-\langle\nabla f(x),y\rangle-\frac12\langle\nabla^2 f(x)y,y\rangle\bigr|\le\frac M6\|y\|^3$.
• One-step inequality (third display): with $\varphi_j=f(x_j)$, $\varphi_{j+1}\le\varphi_j-\frac12\gamma_j\|\nabla f(x_j)\|^2\bigl(1-\frac{M\gamma_j^2}{3}\|\nabla f(x_j)\|\bigr)$.
• (D.1): $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac{L}{2\mu}\langle\nabla^2 f(x)(y-x),y-x\rangle$.
• (D.2): one damped step gives $f(x_{j+1})\le f(x_j)-\frac{\sigma\gamma_j}{2}\|\nabla f(x_j)\|^2$.

Significance

Theorem 6.1 gives a rate for a step size computed from local second-order information alone. Part 1 says that near the minimizer the method converges at least as fast as gradient descent with step $\delta/L$, with no step-size parameter to tune. Part 2 gives convergence from every starting point, at the price of knowing a lower bound on $\mu/L$ for the damping. The same step appears in the paper's LQR method (rule (4.8)) and in gradient projection methods (p. 13, citing [37]), so the one-step inequalities are reusable beyond this theorem.

The result is proved in the paper. As of this writing none of it has a machine-checked proof. The formal work is the full development: the cubic Taylor bound from a Lipschitz second derivative on $\mathbb{R}^n$, the two one-step inequalities, and the inductions that give the rates.

Difficulty

The obvious argument for gradient descent uses the quadratic upper bound $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac L2\|y-x\|^2$ and a step no larger than $2/L$. The Hessian step can be as large as $1/\mu$, far outside that range, so the quadratic bound in the Euclidean norm gives no decrease. Two different replacements are needed. For the undamped method, the cubic Taylor error must be controlled along the whole trajectory, and condition (6.2) is imposed only on $x_0$: the proof must show the gradient stays small enough at every later iterate. For the damped method, the upper bound must be measured in the local Hessian norm (D.1), which trades the step's size for the condition number $L/\mu$.

On the Lean side, Mathlib has Taylor's theorem in one variable. The cubic bound for a function on $\mathbb{R}^n$ with a Lipschitz Fréchet second derivative must be assembled from it or from the integral form along a segment. Mathlib has no ready-made link between strong convexity and a lower bound on the Hessian either.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient f. The Hessian quadratic form $\langle\nabla^2 f(x)v,v\rangle$ is fderiv ℝ (fderiv ℝ f) x v v. Twice differentiability is differentiability of f and of fderiv ℝ f everywhere. The Lipschitz constant of the Hessian is in the operator norm of the bilinear map, not the Frobenius norm. Strong convexity is StrongConvexOn Set.univ μ f with 0 < μ; Mathlib's modulus is $\frac\mu2\|x-y\|^2$. $L$ and $M$ are real constants in the Lipschitz inequalities. The minimizer $x_*$ is a hypothesis ($f(x_*)\le f(y)$ for all $y$), not constructed.

Deviations from the page, all recorded in the items' Formalization Notes:

• The damping positivity $0<\sigma$ is added. It is implicit on the page.
• The damped claim is stated under the full hypotheses of Theorem 6.1, including the Lipschitz Hessian, although its proof does not use $M$.
• The one-step inequality for (6.1) is stated under the strong convexity of Theorem 6.1, which keeps $\gamma\ge0$. The gradient's Lipschitz constant is not assumed there.

At a stationary point the step is $0/0$; Lean evaluates it to $0$, so the method stays at the minimizer, and both rates remain true.

The iterates are those of the defined recursions (6.1) and its damped version. A statement about an arbitrary sequence satisfying a descent inequality would be a different, weaker theorem and does not discharge the goal. Condition (6.2) is imposed on $x_0$ only; a version assuming it at every iterate is also not the goal.

Contributions welcome: the multivariate cubic Taylor bound (reusable wherever a Lipschitz Hessian appears, e.g. in cubic regularization of Newton's method); the Hessian bounds $\mu I\preceq\nabla^2 f\preceq LI$ from strong convexity and a Lipschitz gradient; and the inequality $\frac12\|\nabla f(x)\|^2\le L(f(x)-f(x_*))$.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, 2020; SIAM J. Control Optim. 59(5), 2021. https://arxiv.org/abs/2004.09875 · https://doi.org/10.1137/20M1329858
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108, 2006 (the cubic Taylor bound for Lipschitz Hessians). https://doi.org/10.1007/s10107-006-0706-8
• B. T. Polyak, Introduction to Optimization, Optimization Software, 1987 (gradient methods, strong convexity).

Motivation

The gradient projection method minimizes a continuously differentiable function over a closed convex set by alternating a gradient step with a projection back onto the set. It was proposed by Goldstein (1964) and by Levitin and Polyak (1966), and it is the basic step of many algorithms for bound constrained and linearly constrained optimization, including large-scale quadratic programming codes.

The classical convergence results either need a Lipschitz constant for the gradient to choose the step (Goldstein; Levitin–Polyak), or assume a bounded sequence of iterates and conclude only that limit points are stationary (Bertsekas, 1976, for the Armijo rule on a box; Dunn, 1981). Calamai and Moré (1987) introduced a general step-size rule that contains the Armijo procedure, and proved a convergence statement that needs no boundedness of the iterates: the projected gradients tend to zero. This statement is what later results on finite identification of the active constraints use as their hypothesis, so it is the natural entry point to the paper.

Setting

Let $E$ be a finite-dimensional real inner product space with norm $\|\cdot\|$, let $\Omega \subseteq E$ be nonempty, closed and convex, and let $f : E \to \mathbb R$ be continuously differentiable on $\Omega$, with gradient $\nabla f$ taken with respect to the inner product. The problem is

$$\min\{f(x) : x \in \Omega\}. \qquad (1.1)$$

• The projection into $\Omega$ is $P(x) = \operatorname{argmin}\{\|z - x\| : z \in \Omega\}$, the unique nearest point of $\Omega$ to $x$ (Eq. (1.3)).
• A point $x^* \in \Omega$ is stationary if $\langle \nabla f(x^*), x - x^* \rangle \ge 0$ for all $x \in \Omega$ (Eq. (1.5)).
• A direction $v$ is feasible at $x \in \Omega$ if $x + \tau v \in \Omega$ for all sufficiently small $\tau > 0$; the tangent cone $T(x)$ is the closure of the set of feasible directions.
• The projected gradient is $\nabla_\Omega f(x) = \operatorname{argmin}\{\|v + \nabla f(x)\| : v \in T(x)\}$ (Eq. (3.1)), the nearest point of $T(x)$ to $-\nabla f(x)$.

A run of the gradient projection method is a pair of sequences $(x_k)_{k\ge0}$, $(\alpha_k)_{k \ge 0}$ with $x_0 \in \Omega$, $\alpha_k > 0$ and $x_{k+1} = x_k(\alpha_k)$, where $x_k(\alpha) = P(x_k - \alpha \nabla f(x_k))$. For fixed constants $\gamma_1, \gamma_2 > 0$ and $\mu_1, \mu_2 \in (0,1)$, the steps satisfy the sufficient decrease condition

$$f(x_{k+1}) \le f(x_k) + \mu_1 \langle \nabla f(x_k), x_{k+1} - x_k\rangle \qquad (2.1)$$

and the condition that the step is not too small: either $\alpha_k \ge \gamma_1$, or $\alpha_k \ge \gamma_2 \bar\alpha_k > 0$ for some $\bar\alpha_k$ at which sufficient decrease fails,

$$f(x_k(\bar\alpha_k)) > f(x_k) + \mu_2 \langle \nabla f(x_k), x_k(\bar\alpha_k) - x_k \rangle. \qquad (2.2)\text{–}(2.3)$$

In Lean these objects are proj, projGrad and IsGradientProjectionRun in the namespace CalamaiMore.Convergence, together with the shared definitions tangentCone and IsStationaryPoint in CalamaiMore.Shared.

Formalization targets

Goal: Theorem 3.2

If, in addition, the steps are bounded, $\alpha_k \le \gamma_3$ for some constant $\gamma_3$ (3.2), $f$ is bounded below on $\Omega$, and $\nabla f$ is uniformly continuous on $\Omega$, then

$$\lim_{k \to \infty} \|\nabla_\Omega f(x_k)\| = 0.$$

No boundedness of $\{x_k\}$ is assumed, and no specific step rule beyond (2.1)–(2.3).

Milestones

1. Lemma 2.1: $P$ satisfies the variational inequality $\langle P(x) - x, z - P(x)\rangle \ge 0$ for $z \in \Omega$, is monotone (strictly when $P(y) \ne P(x)$) and nonexpansive.
2. Eqs. (2.4)–(2.5): $\langle \nabla f(x_k), x_k - x_k(\alpha)\rangle \ge \|x_k(\alpha) - x_k\|^2/\alpha$ for $\alpha > 0$, and its instance at $\alpha = \alpha_k$.
3. Lemma 2.2: $\alpha \mapsto \|P(x + \alpha d) - x\|/\alpha$ is nonincreasing on $(0, \infty)$.
4. Theorem 2.3: under the hypotheses of the goal without (3.2), $\|x_{k+1} - x_k\|/\alpha_k \to 0$.
5. Lemma 3.1: $-\langle \nabla f(x), \nabla_\Omega f(x) \rangle = \|\nabla_\Omega f(x)\|^2$; $\min\{\langle \nabla f(x), v\rangle : v \in T(x), \|v\| \le 1\} = -\|\nabla_\Omega f(x)\|$; and $x$ is stationary if and only if $\nabla_\Omega f(x) = 0$.
6. Theorem 2.4: if some subsequence $\{x_k : k \in K\}$ is bounded, $\|x_{k+1} - x_k\|/\alpha_k \to 0$ along $K$, and every limit point of $\{x_k\}$ is stationary.
7. Lemma 3.3: $x \mapsto \|\nabla_\Omega f(x)\|$ is lower semicontinuous on $\Omega$.
8. Theorem 3.4: with (3.2) and a bounded subsequence $\{x_k : k \in K\}$, $\|\nabla_\Omega f(x_{k+1})\| \to 0$ along $K$.

Significance

By Lemma 3.1, $\|\nabla_\Omega f(x)\|$ vanishes exactly at stationary points, so Theorem 3.2 says that the method approaches stationarity in a quantitative sense even when the iterates are unbounded. With Lemma 3.3 it gives that every limit point is stationary. For polyhedral $\Omega$ it is the hypothesis of the paper's Theorem 4.1: any sequence with $\nabla_\Omega f(x_k) \to 0$ converging to a nondegenerate point identifies the active constraints in finitely many iterations, which is the basis of active-set methods that switch between gradient projection steps and subspace minimization.

The results are proved in the paper. To our knowledge they have no machine-checked proof. This mission produces a formal account of the gradient projection method with a general step rule, a reusable projected gradient and tangent cone on a general finite-dimensional inner product space, and the standard projection estimates of §2, which are also the starting point of the paper's other two main results.

Difficulty

The obvious argument fails at two places. First, the continuity of $\nabla_\Omega f$ cannot be used: the map $x \mapsto \nabla_\Omega f(x)$ is not continuous, and $\|\nabla_\Omega f\|$ can be bounded away from zero in every neighborhood of a stationary point, because the tangent cone changes discontinuously at the boundary of $\Omega$. So $x_k \to x^*$ with $x^*$ stationary does not by itself force $\nabla_\Omega f(x_k) \to 0$, and here the iterates need not converge at all. Second, the steps $\alpha_k$ may tend to zero along a subsequence; the step rule gives information only through a trial step $\bar\alpha_k$, at a point other than $x_{k+1}$, and comparing the two projected steps is where the argument must work.

Formalization scope

The space is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; $\nabla f$ is Mathlib's gradient f. "Continuously differentiable on $\Omega$" is ∀ x ∈ Ω, DifferentiableAt ℝ f x together with ContinuousOn (gradient f) Ω. Bounded below is BddBelow (f '' Ω), uniform continuity is UniformContinuousOn (gradient f) Ω. Sequences are ℕ → E indexed from $0$; a subsequence is an infinite K : Set ℕ with limits along atTop ⊓ 𝓟 K; a limit point is a MapClusterPt. The projection and the projected gradient are total functions through a nearest-point map that returns $0$ when no nearest point exists; every theorem assumes $\Omega$ nonempty, closed and convex, and evaluates $\nabla_\Omega f$ only at points of $\Omega$, where the nearest point exists and is unique. The step rule is a predicate on the pair of sequences, so the theorems cover every rule satisfying (2.1)–(2.3); the auxiliary condition $\mu_1 \le \mu_2$, which the paper uses only to show that an admissible step exists, is not imposed.

The run predicate is satisfiable: for a constant $f$, the constant sequence $x_k = x_0 \in \Omega$ with $\alpha_k = \gamma_1$ is a run, so the goal is not vacuous. A formalization that states the goal for an arbitrary map in place of the projection, drops the bound $\alpha_k \le \gamma_3$, or replaces $\|\nabla_\Omega f(x_k)\|$ by $\|x_{k+1} - x_k\|/\alpha_k$ proves a different theorem and is not accepted.

Contributions welcome: the projection estimates (reusable for any projection-based method), existence and uniqueness of the projected gradient, the characterization of stationarity, and the two limit theorems.

Selected references

• P. H. Calamai, J. J. Moré, Projected gradient methods for linearly constrained problems, Mathematical Programming 39 (1987) 93–116. https://doi.org/10.1007/BF02592073
• A. A. Goldstein, Convex programming in Hilbert space, Bulletin of the AMS 70 (1964) 709–710. https://doi.org/10.1090/S0002-9904-1964-11178-2
• E. S. Levitin, B. T. Polyak, Constrained minimization methods, USSR Computational Mathematics and Mathematical Physics 6 (1966) 1–50. https://doi.org/10.1016/0041-5553(66)90114-5
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Transactions on Automatic Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
• J. C. Dunn, Global and asymptotic convergence rate estimates for a class of projected gradient processes, SIAM Journal on Control and Optimization 19 (1981) 368–400. https://doi.org/10.1137/0319022
• E. M. Gafni, D. P. Bertsekas, Two-metric projection methods for constrained optimization, SIAM Journal on Control and Optimization 22 (1984) 936–964. https://doi.org/10.1137/0322061

Motivation

Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.

The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form $\max\{c^Tx : Ax\le b,\ x\in\mathbb Z^n\}$ that is feasible and bounded, every optimal LP solution $x^*$ has an optimal integer solution $z^*$ with $\|x^*-z^*\|_\infty\le n\cdot\delta$, where $\delta$ is the largest absolute value of a subdeterminant of $A$. For programs in standard form $Ax=b$ with $m$ rows this gives, via the Hadamard bound, $\|z^*-x^*\|_1\le n^2\cdot m^{m/2}\Delta^m$, which grows with the number of variables $n$.

Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on $n$ altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on $m$ and on the largest absolute value $\Delta$ of an entry of $A$, and it is the basis of their faster algorithms for integer programs with few constraints.

Setting

Fix natural numbers $m$ (rows) and $n$ (variables). The data are a matrix $A\in\mathbb Z^{m\times n}$, a right-hand side $b\in\mathbb Z^m$, an objective $c\in\mathbb Z^n$ and upper bounds $u\in\mathbb N^n$. A natural number $\Delta$ bounds the entries: $|a_{ij}|\le\Delta$ for all $i,j$. The integer program (10) is

$$\max\{c^Tx : Ax=b,\ 0\le x\le u,\ x\in\mathbb Z^n\},$$

and its LP relaxation is the same problem over $x\in\mathbb R^n$. Its feasible region $P=\{x\in\mathbb R^n: Ax=b,\ 0\le x\le u\}$ is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of $P$. An optimal integer solution is IsIPOptimal. Both are maxima.

Distances are measured in the $\ell_1$-norm $\|z-x\|_1=\sum_i|z_i-x_i|$.

A vector $y\in\mathbb Z^n$ is a cycle of $z^*-x^*$ (Eq. (14)) if $Ay=0$ and, for every $i$, $|y_i|\le|(z^*-x^*)_i|$ and $y_i(z^*-x^*)_i\ge0$: an integer kernel vector that is sign-compatible with $z^*-x^*$ and dominated by it (IsCycle).

The Steinitz lemma (Theorem 1.1) concerns vectors $x_1,\dots,x_n$ in an $m$-dimensional normed space with $\sum_i x_i=0$ and $\|x_i\|\le1$. It asserts a permutation $\pi$ with $\|\sum_{j\le k}x_{\pi(j)}\|\le c(m)$ for all $k$, and the paper uses Sevast'anov's constant $c(m)=m$.

Formalization targets

Goal: Theorem 3.3 (p. 5:8)

If (10) has an integer feasible point and $x^*$ is an optimal vertex solution of its LP relaxation, then there is an optimal solution $z^*$ of (10) with

$$\|z^*-x^*\|_1\ \le\ m\cdot(2m\Delta+1)^m .$$

The constant is the paper's. The goal holds for all $m$, $n$, $b$, $c$ and $u$; only $m$ and $\Delta$ enter the bound.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 5:8): for an LP optimum $x^*$, an integer optimum $z^*$ and a cycle $y$ of $z^*-x^*$, the vector $z^*-y$ is integer feasible, $x^*+y$ is LP feasible, and $c^Ty\le0$.
2. Lemma 3.2 (p. 5:8): if $z^*$ minimizes $\|z^*-x^*\|_1$ among the optimal integer solutions, then $z^*-x^*$ has no nonzero cycle.
3. Theorem 1.1 with $c(m)=m$ (p. 5:4): the Steinitz lemma in any $m$-dimensional real normed space.
4. Proof of Theorem 3.3 (pp. 5:8–5:9): round a vertex $x^*$ towards an integer vector and write $\{x^*\}$ for the remainder. Then $\|-A\{x^*\}\|_\infty\le\Delta m$ and $-A\{x^*\}=w_1+\dots+w_m$ with integer $w_j$, $\|w_j\|_\infty\le\Delta$.
5. Proof of Theorem 3.3, Eq. (20) (p. 5:9): a sequence of integer vectors of $\ell_\infty$-norm at most $m\Delta$ in which no value repeats $m+1$ times has length at most $m(2m\Delta+1)^m$.
6. Eq. (21) (p. 5:9), a consequence: $c^T(x^*-z^*)\le\|c\|_\infty\cdot m(2m\Delta+1)^m$ for every optimal integer solution $z^*$.

Significance

The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an $\ell_1$-ball of radius $m(2m\Delta+1)^m$ around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by $\|c\|_\infty$. The Steinitz lemma with constant $m$ is a general tool in discrepancy theory and in scheduling algorithms.

All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant $m$ for arbitrary norms is reusable well beyond integer programming.

Difficulty

Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant $m$ for an arbitrary norm: the bound must hold uniformly in the number $n$ of vectors, and the constant must be exactly $m$, because the goal's constant $(2m\Delta+1)^m$ counts integer points of $\ell_\infty$-norm at most $m\Delta$. The second is the passage from a vertex to at most $m$ fractional coordinates. The paper argues this in one sentence ("$x^*$ has at most $m$ positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound $u_i>0$ are positive. The correct fact concerns coordinates strictly between $0$ and $u_i$, and it has to be derived from the extreme-point property of $P$.

Formalization scope

• All declarations live in the namespace IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries $u_i=0$ allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. $m=0$ and $n=0$ are allowed.
• "Vertex" is Mathlib's Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.
• The $\ell_1$-distance is the explicit sum ∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has $\|\cdot\|_\infty$ (the $\|c\|_\infty$ of Eq. (21)).
• The goal adds one hypothesis the paper leaves implicit: (10) has an integer feasible point. The paper's proof begins with "Let $z^*$ be an optimal integer solution"; without this hypothesis the conclusion is false.
• Eq. (14) is formalized literally, so $y=0$ is a cycle, and Lemma 3.2 is stated for nonzero cycles, which is what its proof establishes. Dropping the vertex hypothesis would make the goal false, so the goal keeps it. The constant is exactly $m(2m\Delta+1)^m$, with no hidden existential constant.
• The Steinitz milestone is stated for any finite-dimensional real normed space of dimension $m$ with the explicit constant $m$. The goal needs only the $\ell_\infty$ case on $\mathbb R^m$.
• Out of scope: the dynamic program and the running-time theorems of Sections 2 and 4, and the refinement $\|z^*-x^*\|_1\le2\Delta$ for $m=1$.

Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.

Selected references

• F. Eisenbrand, R. Weismantel, Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma, ACM Transactions on Algorithms 16(1), Article 5, 2019. https://doi.org/10.1145/3340322
• W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34, 251–264, 1986. https://doi.org/10.1007/BF01582230
• E. Steinitz, Bedingt konvergente Reihen und konvexe Systeme, Journal für die reine und angewandte Mathematik 143, 128–176, 1913. https://doi.org/10.1515/crll.1913.143.128
• S. Sevast'janov, Approximate solution of some problems of scheduling theory (in Russian), Metody Diskretnogo Analiza 32, 66–75, 1978 (reference [31] of the paper).
• V. S. Grinberg, S. V. Sevast'yanov, Value of the Steinitz constant, Functional Analysis and Its Applications 14(2), 125–126, 1980 (reference [16] of the paper).

Motivation

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.

Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.

Setting

A network $N$ has a finite set $V$ of nodes, a source $s$ and a sink $t \neq s$, and a set of arcs, ordered pairs $(u,v)$ with $u \neq v$, at most one from each node to another. One arc is the return arc $(t,s)$; the other arcs form the set $A$, and each $(u,v) \in A$ has a capacity $c(u,v) > 0$. A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and flow conservation at every node, $s$ and $t$ included. Its value is $f(t,s)$, the flow returned along the return arc; a maximum flow has the largest value among all flows, and $f^*(t,s)$ denotes that value.

The residual network $N^f$ has an arc $(u,v)$ whenever $(u,v) \in A$ and $c(u,v) - f(u,v) > 0$, or $(v,u) \in A$ and $f(v,u) > 0$. An augmenting path is a directed path $s = u_1, \dots, u_p = t$ of distinct nodes in $N^f$. Each of its arcs $(u,v)$ has a residual amount $e(u,v)$, equal to $c(u,v) - f(u,v)$, $f(v,u)$, or $c(u,v) - f(u,v) + f(v,u)$ according to which of $(u,v)$, $(v,u)$ lie in $A$, and the path's augmentation is $\varepsilon = \min e(u_i, u_{i+1})$. Augmenting increases $f(t,s)$ by $\varepsilon$ and changes the flow on the arcs of the path accordingly, with the paper's own rule when both $(u,v)$ and $(v,u)$ are arcs. The labeling method produces flows $f^0, f^1, \dots$ by augmenting along a path relative to $f^k$ as long as one exists.

The rule studied here chooses, at every step, an augmenting path whose $\varepsilon$ is at least that of every other augmenting path relative to the current flow. The bound involves an integer $M > 1$ such that every partition of the nodes into $X \ni s$ and $\bar X \ni t$ has at most $M$ arcs of $N$ with one end on each side.

Formalization targets

Goal: Theorem 2 (p. 253)

For a network with integer capacities, $M$ as above, and a run $f^0, \dots, f^K$ of the labeling method with maximum augmentations started from an integer-valued flow,

$$K \;\le\; 1 + \log_{M/(M-1)} f^*(t,s),$$

and if no augmenting path relative to $f^K$ exists, then $f^K$ is a maximum flow.

Milestones

The milestone list follows the paper's argument:

1. augmentation produces a flow of value $f(t,s) + \varepsilon$ (§1.1, p. 249);
2. a flow is maximum if and only if it has no augmenting path (§1.1, pp. 249–250);
3. with integer capacities, $\varepsilon$ is a positive integer and the flows of the method stay integer-valued (§1.1, p. 250);
4. the cut inequality $c(X,\bar X) \ge f(X,\bar X) - f(\bar X,X) = f(t,s)$ (p. 254);
5. $f^*(t,s) - f^k(t,s) \le \varepsilon^k M$, where $\varepsilon^k = f^{k+1}(t,s) - f^k(t,s)$ (p. 254);
6. $f^*(t,s) - f^{k+1}(t,s) \le [f^*(t,s) - f^k(t,s)](1 - M^{-1})$ (p. 254);
7. $f^*(t,s) - f^k(t,s) \le f^*(t,s)(1 - M^{-1})^k$ (p. 254).

Significance

Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since $M \le n^2/2$ and $f^*(t,s)$ is at most $n^2$ times the average capacity, the bound is $O(n^2 \log(n^2 \bar c))$ in terms of the number of nodes $n$ and the average capacity $\bar c$ (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).

The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.

Difficulty

The obvious argument, that each augmentation raises the value by at least 1, gives only the bound $f^*(t,s)$, and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap $f^*(t,s) - f^k(t,s)$. The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.

Formalization scope

• Nodes form a finite type V with decidable equality. A : Finset (V × V) contains no loops and not $(t,s)$. Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of $N$, the return arc included).
• Flows are functions V → V → ℝ constrained only on the arcs of $N$. A maximum flow is the predicate IsMaxFlow, comparing $f(t,s)$ with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets $f^*(t,s) = g(t,s)$; every network has one.
• Augmenting paths are duplicate-free node lists whose consecutive pairs are arcs of $N^f$. The page prints Case (b) of the definition of $\varepsilon_i$ with the same hypothesis as Case (c); the corrected Case (b), $(u,v) \notin A$ and $(v,u) \in A$, is used, as the definition of $N^f$ (p. 251) and the list for $e(u,v)$ (p. 253) confirm.
• A run is IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum $\varepsilon$ among all augmenting paths.
• The crossing bound CrossArcsBounded N M counts the arcs of $N$, return arc included, with one end on each side of every $s$–$t$ partition. This is the literal reading of p. 253.
• Explicit constants. The bound is exactly $1 + \log_{M/(M-1)} f^*(t,s)$, written (K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with $M > 1$ a natural number. When $f^*(t,s) = 0$, Real.logb gives $0$ and the bound reads $K \le 1$. The contraction factor is 1 - (M : ℝ)⁻¹.
• A statement that bounds only runs of an unsatisfiable step predicate, drops the integrality of $f^0$ or of the capacities (the bound is false without them), or compares $\varepsilon$ only among paths of some restricted class does not formalize Theorem 2. A sorry-free check exhibits a four-node network with integer capacities and a valid maximum-augmentation step.
• Reusable beyond this mission: the return-arc network model, the augmentation step with the paper's opposite-arc rule, the integrality lemma, and the cut inequality. Proofs of any milestone are welcome, as are proofs of the converse in milestone 2 that could later be shared with mission 1.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• L. R. Ford, D. R. Fulkerson, Flows in Networks, RAND report R-375-PR, 1962; Princeton University Press, 1962. https://www.rand.org/pubs/reports/R375.html

Motivation

Infinite-horizon sequential decision problems (deterministic optimal control, Markov decision processes, minimax control) share one computational question: does the dynamic programming (DP) algorithm, which starts from a terminal cost and repeatedly applies the Bellman operator, converge to the optimal cost? For discounted problems with bounded costs the answer is yes, by the contraction mapping theorem (Blackwell 1965; Denardo 1967). Without discounting and boundedness the answer depends on the sign structure of the problem. Strauch's negative programming model (Strauch 1966) and Blackwell's positive programming model behave differently, and in the former the DP algorithm can fail to converge to the optimal cost even for simple deterministic problems.

Bertsekas (1977) recast these models in one abstract framework: a monotone mapping $H$ that encodes the one-stage problem, with no probabilistic or additive structure assumed. Two sign conditions organise the theory: uniform increase (Assumption I, containing Strauch's model) and uniform decrease (Assumption D, containing the deterministic version of Blackwell's positive model, e.g. deterministic problems with nonpositive stage costs). This mission formalizes the uniform-decrease half of Section 5: under D, the finite-horizon problems are solved by the DP algorithm, $J^*$ is the limit of the finite-horizon values, Bellman's equation holds, and the DP algorithm converges to $J^*$. The same framework became the basis of Bertsekas–Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978) and of Bertsekas's Abstract Dynamic Programming (2013, 3rd ed. 2022).

Setting

States, controls, policies. $S$ (nonempty) and $C$ are sets. Each $x\in S$ has a nonempty constraint set $U(x)\subseteq C$. $M$ is the set of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$, and a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors. The policy is stationary if $\mu_k=\mu$ for all $k$.

Functions and the mapping $H$. $F$ is the set of functions $J:S\to[-\infty,\infty]$, ordered pointwise, and $e$ is the constant function $1$. A mapping $H:S\times C\times F\to[-\infty,\infty]$ is given, and it is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for every $x$ and $u\in U(x)$. It defines

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).$$

$T^k$ is the $k$-fold composition, with $T^0$ the identity, and $(T_{\mu_0}\cdots T_{\mu_{N-1}})$ applies $T_{\mu_{N-1}}$ first.

Costs. A terminal function $\bar J\in F$ with $\bar J(x)>-\infty$ is given. The cost of a policy, the optimal cost, the $N$-stage optimal cost and the limit of the DP algorithm are

$$J_\pi=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J^*=\inf_{\pi}J_\pi,\quad J_N=\inf_{\pi}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J_\infty=\lim_{N\to\infty}T^N(\bar J),$$

all pointwise. $J_\mu$ denotes the cost of the stationary policy $\{\mu,\mu,\dots\}$.

Assumptions. D: $H(x,u,\bar J)\le\bar J(x)$ for all $x$, $u\in U(x)$. Under D every sequence above is nonincreasing, so the limits exist in $[-\infty,\infty]$. D.1: for every sequence with $J_{k+1}\le J_k\le\bar J$, $\lim_k H(x,u,J_k)=H(x,u,\lim_k J_k)$. D.2: there is $\alpha>0$ such that $H(x,u,J)-\alpha r\le H(x,u,J-re)\le H(x,u,J)$ for all $r>0$ and $J\le\bar J$.

Formalization targets

Goal: convergence of the DP algorithm (Proposition 9)

If D holds, and either D.1 holds or $J_N=T^N(\bar J)$ for every $N\ge1$, then

$$J_\infty=J^*.$$

Milestones

1. Lemma 1. Under D, $J^*(x)=\lim_{N\to\infty}J_N(x)$ for every $x$.
2. Proposition 3. Under D, and either D.1 or (D.2 and $T^N(\bar J)>-\infty$ everywhere), $J_N=T^N(\bar J)$ for a given $N\ge1$.
3. Proposition 6. Under D and D.1, $J^*=T(J^*)$, and every $J'\le\bar J$ with $J'\le T(J')$ satisfies $J'\le J^*$.
4. Corollary 6.2. Under D and D.1, $J_\mu=T_\mu(J_\mu)$ for every stationary policy, and every $J'\le\bar J$ with $J'\le T_\mu(J')$ satisfies $J'\le J_\mu$.
5. Proposition 8. Under D and D.1, a stationary policy $\{\mu^*,\mu^*,\dots\}$ is optimal if and only if $T_{\mu^*}(J_{\mu^*})=T(J_{\mu^*})$.

The goal is the paper's answer, in the uniform-decrease case, to the question it poses in the introduction: when is $\lim_N T^N(\bar J)=J^*$?

Significance

The result. Proposition 9 justifies value iteration from $\bar J$ for every problem that fits Assumption D, including deterministic and stochastic control with nonpositive costs (reward maximization with nonnegative rewards) and minimax problems satisfying D.1. Propositions 6 and 8 characterise $J^*$ as the largest solution of Bellman's equation below $\bar J$ and give a verification test for stationary policies. The hypotheses are sharp in the sense the paper documents: its Counterexamples 2 and 3 show $J_N\ne T^N(\bar J)$ when D.1 is dropped together with D.2 or with the finiteness condition $T^N(\bar J)>-\infty$. Under the mirror assumption I, $J_\infty=J^*$ can fail, so the asymmetry between the two sign conditions is part of the content.

Formalizing it. All results are proved in the 1977 paper and reappear in later monographs. No machine-checked version of this abstract framework is known. The platform's existing dynamic programming items are finite-state, real-valued and contraction-based, so this mission would add the first formal treatment of extended-real-valued, non-contractive dynamic programming, and a model definition that other results of the same theory can reuse.

Difficulty

The obvious argument for Proposition 9, "$J_N=T^N(\bar J)$ and $J_N\to J^*$", hides two separate interchanges of limits and infima. Lemma 1 interchanges $\inf_\pi$ with $\lim_N$, which works only because every sequence is monotone in the right direction under D. Proposition 3 is where the work is: the $N$-stage infimum over policies must be matched by the iterated infimum $T^N$, which requires building near-optimal selectors stage by stage and passing a limit through $H$ $N$ times, using D.1, or controlling accumulated errors through D.2. The latter breaks down when values reach $-\infty$, which is why that branch needs $T^N(\bar J)>-\infty$. All arithmetic is in $[-\infty,\infty]$, where expressions such as $\infty-\infty$ are not defined, and $J^*$, $J_N$, $T^N(\bar J)$ may equal $-\infty$ even though $\bar J$ does not.

Formalization scope

The model is a Lean structure MonotoneDP.Decrease.Model S C with fields U, U_nonempty, H, mono, Jbar, Jbar_ne_bot and S_nonempty; $F$ is S → EReal. Policies are ℕ → Selector, where a selector is a function with values in the constraint sets. $T$ is an infimum over U x only, and $J^*$, $J_N$ are infima over admissible policies. $J_\pi$ and $J_\infty$ are limUnder atTop; every theorem assumes D, under which both sequences are nonincreasing and converge, so these are the paper's limits. In D.1 both limits are limUnder. D.2 carries its scalar as a parameter, and "D.2 holds" is ∃ α, AssumptionD2 α. Only real scalars are ever subtracted from extended reals.

$J_N$ is defined for every $N$, and Propositions 3 and 9 quantify over $N\ge1$ as the paper does. In Proposition 3 the condition $T^N(\bar J)>-\infty$ belongs to the D.2 branch only. No hypothesis beyond the page is added. Nonempty constraint sets and $\bar J>-\infty$ are the paper's standing assumptions, stated in the model, not in the theorems. Without nonempty constraint sets there would be no policies, $J^*$ and $J_N$ would be $+\infty$, and several statements would hold trivially; the model rules this out.

Useful contributions: general lemmas about monotone sequences in EReal (interchanging ⨅ and limits), the monotonicity facts (25) and $T^{N+1}(\bar J)\le T^N(\bar J)$ under D, and reusable constructions of near-optimal selectors. Corollary 6.1 (the finite-state D.2 variant) is not included.

Selected references

• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699147
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. https://www.mit.edu/~dimitrib/abstractdp_MIT.html

Motivation

Many problems in convex optimization, variational inequalities and signal processing reduce to finding a zero of a sum of three monotone operators, one of which is single-valued and smooth. Davis and Yin (Set-Valued Var. Anal. 25, 2017) introduced a splitting scheme that evaluates each of the three operators separately: the two set-valued ones through their resolvents, the single-valued one through a forward step. With a fixed stepsize, their Algorithm 1 converges weakly but can be slow: the paper's Section 3.4 constructs examples where the squared distance of the iterates to the solution decays no faster than $(k+1)^{-(1+\epsilon)}$ for every $\epsilon > 0$.

When one of the operators is strongly monotone (for example the subdifferential of a strongly convex function), first-order splitting methods can be accelerated by letting the stepsize shrink like $1/k$; the paper relates its stepsizes to those of Chambolle and Pock's accelerated primal–dual method (J. Math. Imaging Vis. 40, 2011, Algorithm 2) and of Boţ, Csetnek, Heinrich and Hendrich (Math. Program. 150, 2015, Algorithm 5). Section 3.3 of Davis–Yin carries this device over to three-operator splitting and obtains an $O(1/(k+1)^2)$ rate for the squared distance. This mission formalizes that result.

Setting

Let $H$ be a real Hilbert space. A set-valued operator $A : H \to 2^H$ is monotone if $\langle x - y, u - v\rangle \ge 0$ for all $u \in Ax$, $v \in Ay$, and maximal monotone if its graph is not properly contained in the graph of another monotone operator. It is $\mu$-strongly monotone if $\langle x - y, u - v\rangle \ge \mu\|x-y\|^2$ for all such pairs. A single-valued $C : H \to H$ is $\beta$-cocoercive if $\beta\|Cx - Cy\|^2 \le \langle Cx - Cy, x - y\rangle$, and $L_C$-Lipschitz if $\|Cx - Cy\| \le L_C\|x - y\|$.

The problem is to find $x^* \in \operatorname{zer}(A + B + C)$, that is, $0 \in Ax^* + Bx^* + Cx^*$, where $A$, $B$ are maximal monotone and $C$ is monotone and single-valued. For $\gamma > 0$ the resolvent $J_{\gamma A} = (I + \gamma A)^{-1}$ is the map with $x \in J_{\gamma A}x + \gamma A(J_{\gamma A}x)$.

Algorithm 3 fixes stepsizes $(\gamma_k)_{k\ge 0} \subseteq (0,\infty)$ and an initial point $x_A^0 \in H$, sets $x_B^0 = J_{\gamma_0 B}(x_A^0)$, $u_B^0 = \gamma_0^{-1}(x_A^0 - x_B^0)$, and iterates for $k \ge 0$

$$x_B^{k+1} = J_{\gamma_k B}(x_A^k + \gamma_k u_B^k),\quad u_B^{k+1} = \tfrac{1}{\gamma_k}(x_A^k + \gamma_k u_B^k - x_B^{k+1}),\quad x_A^{k+1} = J_{\gamma_{k+1}A}(x_B^{k+1} - \gamma_{k+1}u_B^{k+1} - \gamma_{k+1}Cx_B^{k+1}).$$

The stepsize changes in the middle of an iteration. Two stepsize rules are considered, each defined recursively from $\gamma_0$:

$$\text{(3.6)}\quad \gamma_{k+1} = \frac{-2\gamma_k^2\mu_C\eta + \sqrt{(2\gamma_k^2\mu_C\eta)^2 + 4(1+2\gamma_k\mu_B)\gamma_k^2}}{2(1+2\gamma_k\mu_B)}, \qquad \text{(3.7)}\quad \gamma_{k+1} = \frac{\gamma_k}{\sqrt{1 + 2\gamma_k(\mu_B - \gamma_kL_C^2/2)}}.$$

Formalization targets

Goal: Theorem 3.3, both parts

Let $B$ be $\mu_B$-strongly monotone with $\mu_B \ge 0$.

1. If $C$ is $\beta$-cocoercive and $\mu_C$-strongly monotone ($\mu_C > 0$), $\eta \in (0,1)$, $\gamma_0 \in (0, 2\beta(1-\eta))$ and the stepsizes follow (3.6), then for every $x^* \in \operatorname{zer}(A+B+C)$

$$\exists K\ \forall k \ge 0:\quad \|x_B^k - x^*\|^2 \le \frac{K}{(k+1)^2}.$$

2. If $C$ is $L_C$-Lipschitz, $\mu_B > 0$, $\gamma_0 \in (0, 2\mu_B/L_C^2)$ and the stepsizes follow (3.7), the same conclusion holds.

The goal asserts the shape of the rate only; the constant $K$ is not fixed.

Milestones

• Proposition 3.1, Parts 1 and 2: the one-step inequalities (3.9) and (3.10) for Algorithm 3 with arbitrary admissible stepsizes.
• Stepsize facts from the proof of Theorem 3.3: the identities that make (3.9) and (3.10) telescope, the monotonicity of the stepsizes (3.6), and the limits $(k+1)\gamma_k \to 1/(\mu_C\eta + \mu_B)$ for (3.6) and $(k+1)\gamma_k \to 1/\mu_B$ for (3.7).

Significance

The theorem shows that strong monotonicity of $B$ or $C$ can be converted into a quadratically decaying distance bound without knowledge of the solution, with stepsizes that are computable from the strong monotonicity and cocoercivity (or Lipschitz) constants alone. Since the rate is established for $x_B^k$, it applies directly to splitting schemes for strongly convex composite problems $\min f + g + h$ with $h$ smooth, where $x_B^k$ is the proximal point of $g$.

The result is proved in the paper; no machine-checked version is known. The formalization adds a precise statement of the admissible parameter ranges, a check of the index conventions of a scheme whose stepsize changes mid-iteration, and a correction of the one-step inequalities at the first iteration (see Formalization scope). The stepsize limits are statements about explicit real recursions and are of independent use for other accelerated schemes.

Difficulty

The one-step inequalities (3.9) and (3.10) are long but elementary chains of inner-product identities and Young's inequality; the work lies in bookkeeping two stepsizes per iteration. The rate itself does not follow from the one-step inequality alone: telescoping gives a bound of the form $\|x_B^{k}-x^*\|^2 \lesssim \gamma_k^2$, and one must then show $\gamma_k$ decays exactly like $1/k$. The rules (3.6) and (3.7) are nonlinear recursions without closed form, so their asymptotics require a Stolz–Cesàro type argument, which is not available in Mathlib under that name. Choosing a stepsize sequence of the form $c/k$ instead is a different algorithm and not covered by the theorem.

Formalization scope

• $H$ is an arbitrary real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not a Euclidean space.
• Resolvents are not constructed. They are families JA JB : ℝ → H → H required to satisfy the resolvent inclusion $\gamma^{-1}(x - J(\gamma)x) \in A(J(\gamma)x)$ for every $\gamma > 0$; for maximal monotone operators such maps exist and are unique, so nothing is lost.
• Algorithm 3 is a single recursive definition of the triple $(x_A^k, x_B^k, u_B^k)$ from $x_A^0$, the stepsizes, the resolvent families and $C$; the paper's loop index $k = 1, 2, \dots$ matches recursion (3.8) shifted by one.
• The stepsize rules (3.6) and (3.7) are recursive real sequences, used verbatim; each theorem assumes the paper's parameter ranges.
• $O(1/(k+1)^2)$ is rendered as $\exists K\,\forall k,\ \|x_B^k - x^*\|^2 \le K/(k+1)^2$, with $K$ chosen after all data (initial point, operators, constants, $\gamma_0$, $x^*$) and before $k$. No explicit constant is stated.
• Strong monotonicity of $C$ means $\mu_C > 0$; only $\mu_B = 0$ is allowed, as on the page. With $\mu_B = \mu_C = 0$ rule (3.6) keeps $\gamma_k$ constant and the rate fails, so a formalization allowing $\mu_C = 0$ would be false. In Part 2, $L_C > 0$ is assumed so that the stepsize interval is meaningful, and $C$ is assumed monotone, as in problem (1.1) and as used in the paper's proof of (3.10).
• The paper states (3.9) and (3.10) for all $k \ge 0$; at $k = 0$ the initial point $x_A^0$ is not a resolvent output, and both inequalities fail in general. The milestones state them for $k \ge 1$. Theorem 3.3 is unaffected, since finitely many initial terms do not change an $O(\cdot)$ bound.
• The display $\gamma_k^2 - \gamma_{k+1}^2 = \gamma_k\gamma_{k+1}(2\gamma_k\mu_B + 2\gamma_{k+1}\mu_C\eta)$ on p. 845 has $\gamma_k$ and $\gamma_{k+1}$ swapped inside the bracket; the milestone states the corrected identity $\gamma_k\gamma_{k+1}(2\gamma_{k+1}\mu_B + 2\gamma_k\mu_C\eta)$.
• A trivializing formalization, such as one in which the resolvent hypothesis is unsatisfiable, the stepsize interval is empty, or the rate constant may depend on $k$, is ruled out: the hypotheses are met by $A = 0$, $B = \mu_B I$ (with resolvents $J_{\gamma A} = I$, $J_{\gamma B} = (1+\gamma\mu_B)^{-1}I$) and $C = cI$ with $c > 0$, and $K$ is quantified before $k$.

Contributions are welcome at every level: proofs of the real-sequence milestones (a general Stolz–Cesàro lemma would be reusable well beyond this mission), of the two one-step inequalities, and of the telescoping argument that assembles the goal.

Selected references

• D. Davis and W. Yin, A Three-Operator Splitting Scheme and its Optimization Applications, Set-Valued and Variational Analysis 25 (2017), 829–858. https://doi.org/10.1007/s11228-017-0421-z (preprint: https://arxiv.org/abs/1504.01032)
• R. I. Boţ, E. R. Csetnek, A. Heinrich and C. Hendrich, On the convergence rate improvement of a primal-dual splitting algorithm for solving monotone inclusion problems, Mathematical Programming 150 (2015), 251–279. https://doi.org/10.1007/s10107-014-0766-0
• A. Chambolle and T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, Journal of Mathematical Imaging and Vision 40 (2011), 120–145. https://doi.org/10.1007/s10851-010-0251-1
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5