The OR Formalization Drive

Motivation

Many problems in signal processing, statistics and machine learning minimise a sum of three convex terms: a smooth data-fit term and two nonsmooth regularisers or constraints, each of which is easy to handle on its own (through its proximal map) but not in combination. Examples are constrained sparse regression, matrix completion with a nuclear-norm penalty and box constraints, and support-vector machines with a norm penalty. Davis and Yin (Set-Valued Var. Anal. 25 (2017)) introduced a three-operator splitting scheme that evaluates each proximal map and the gradient of the smooth term once per iteration and reduces to Douglas–Rachford splitting (Lions and Mercier 1979) and forward–backward splitting as special cases. Section 3 of that paper gives the objective-error rates of the scheme on convex problems. This mission formalizes those rates for general convex problems.

Setting

Let $H$ be a real Hilbert space. The problem is

$$\min_{x \in H}\; f(x) + g(x) + h(x), \tag{3.1}$$

where $f, g : H \to (-\infty, +\infty]$ are closed, proper, convex functions (lower semicontinuous, never $-\infty$, finite somewhere, with convex epigraph) and $h : H \to \mathbb R$ is convex and differentiable with $\beta^{-1}$-Lipschitz gradient $\nabla h$, $\beta > 0$.

For $\gamma > 0$ the proximal map $\operatorname{prox}_{\gamma f}(x)$ is the unique minimiser of $y \mapsto f(y) + \frac{1}{2\gamma}\|y - x\|^2$. Algorithm 2 of the paper picks $z^0 \in H$ and $\gamma \in (0, 2\beta)$ and iterates, with relaxation $\lambda_k \equiv 1$,

$$x^k_g = \operatorname{prox}_{\gamma g}(z^k),\qquad x^k_f = \operatorname{prox}_{\gamma f}\big(2x^k_g - z^k - \gamma\nabla h(x^k_g)\big),\qquad z^{k+1} = z^k + x^k_f - x^k_g .$$

Equivalently $z^{k+1} = T z^k$ for the three-operator map

$$T z = \operatorname{prox}_{\gamma f}\big(2\operatorname{prox}_{\gamma g}(z) - z - \gamma\nabla h(\operatorname{prox}_{\gamma g}(z))\big) + z - \operatorname{prox}_{\gamma g}(z).$$

If $z^*$ is a fixed point of $T$, then $x^* = \operatorname{prox}_{\gamma g}(z^*)$ minimises (3.1). The weighted ergodic iterate is

$$\bar x^k_g = \frac{2}{(k+1)(k+2)}\sum_{i=0}^{k} (i+1)\,x^i_g ,$$

and $\bar x^k_f$ is defined the same way from $(x^i_f)$.

Formalization targets

Goal: Theorem 3.2 (p. 840)

Let $z^*$ be a fixed point of $T$, $x^* = \operatorname{prox}_{\gamma g}(z^*)$, and suppose $f$ is $L$-Lipschitz continuous on the closed ball $B\big(x^*, (1+\gamma/\beta)\|z^0 - z^*\|\big)$. Then there is a constant $C$, independent of $k$, with

$$(f+g+h)(\bar x^k_g) - (f+g+h)(x^*) \le \frac{C}{k+1}\qquad (k \ge 0).$$

The goal asserts the order $O(1/(k+1))$ and leaves the constant free, so it is not invalidated by a sharper constant.

Milestones

1. Corollary 2.1, Part 1 (p. 834): $\|z^j - z^*\|$ is nonincreasing.
2. Lemma 3.1 (p. 838): $x^j_f, x^j_g \in B\big(x^*, (1+\gamma/\beta)\|z^0 - z^*\|\big)$ for all $j$.
3. Eq. (3.2) (p. 839): for all $k \ge 0$,

$$2\gamma\big(f(x^k_f) + g(x^k_g) + h(x^k_g) - (f+g+h)(x^*)\big) \le \|z^k - x^*\|^2 - \|z^{k+1} - x^*\|^2 - \|z^k - z^{k+1}\|^2 + 2\gamma\langle z^k - z^{k+1}, \nabla h(x^k_g)\rangle .$$

4. Theorem 3.1 (p. 838): the last-iterate rate $(f+g+h)(x^k_g) - (f+g+h)(x^*) = o\big(1/\sqrt{k+1}\big)$.
5. Eq. (2.7) (p. 836), with $\lambda_k \equiv 1$: for $\gamma/(2\beta) < \varepsilon < 1$,

$$\sum_{i=k}^\infty \|\nabla h(x^i_g) - \nabla h(x^*)\|^2 \le \frac{\|z^k - z^*\|^2}{\gamma(2\beta - \gamma/\varepsilon)} .$$

6. Eq. (3.4) (p. 840): $\|\bar x^k_f - \bar x^k_g\| \le 5\|z^0 - z^*\|/(k+1)$.

Significance

The result. Theorem 3.1 gives the last iterate an objective error of $o(1/\sqrt{k+1})$. Theorem 3.2 shows that averaging with linearly increasing weights improves this to $O(1/(k+1))$, the rate of the standard uniform ergodic average, while putting more weight on recent iterates. The paper notes that this matters when the iterates $x^k_g$ are sparse vectors or low-rank matrices and the average should stay close to them. The rates hold under a local Lipschitz condition on one of the two nonsmooth terms only, so $g$ may be the indicator function of a constraint set. They therefore cover the constrained applications of Section 4 of the paper.

Formalizing it. The results are proved in the paper. No machine-checked version of this scheme or its rates exists on the platform or, as far as is known, in Mathlib. A formalization produces a checked proof in an arbitrary real Hilbert space with extended-valued $f, g$. It also produces infrastructure that Mathlib lacks: proximal maps characterised by minimisation, the prox-subgradient inclusion, Fejér monotonicity of an averaged-operator iteration, and a weighted Jensen inequality for extended-valued convex functions. All of these can be reused by other splitting and proximal-gradient missions. The formalization also checks the constants: the last display of the published proof of Theorem 3.2 drops a factor $2\gamma$ in front of the Lipschitz term, and the printed ball in both theorems is centred at $0$ where the proof needs $x^*$.

Difficulty

The obvious argument sums the one-step inequality (3.2). That controls the objective at the two different points $x^k_f$ and $x^k_g$, and only $f(x^k_f)$ appears, never $f(x^k_g)$. Moving from one point to the other needs the Lipschitz hypothesis on $f$, and so it needs every iterate, and every weighted average, to stay in the ball on which that hypothesis holds. For the weighted average there is a further obstacle: the cross term $2\gamma\langle z^k - z^{k+1}, \nabla h(x^k_g)\rangle$ does not telescope under the weights $(i+1)$. Controlling it requires the summability of the gradient differences (2.7), which is inherited from the averagedness analysis of Section 2 and not from convexity alone. Uniform averaging with the same argument does not give the weighted statement, and the weights must not be replaced.

Formalization scope

• $H$ is an arbitrary real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$.
• $f, g : H \to$ EReal. They are proper (never $\bot$, somewhere $\ne \top$), lower semicontinuous, and have a convex epigraph in $H \times \mathbb R$. $h : H \to \mathbb R$ is convex and differentiable, and Mathlib's gradient h is $\beta^{-1}$-Lipschitz.
• Proximal maps are not constructed. A map $P$ is assumed to minimise $f(y) + \|y - x\|^2/(2\gamma)$ for every $x$. Such a map exists and is unique for closed proper convex $f$, so nothing is lost.
• Algorithm 2 is fixed with $\lambda_k \equiv 1$, the only case of Theorems 3.1 and 3.2. Iterates are indexed from $0$. The fixed point $z^*$ is a hypothesis, $T z^* = z^*$, and $x^* := \operatorname{prox}_{\gamma g}(z^*)$. Assumption 1 of the paper follows from this and is not assumed separately.
• Ball centre. The theorems print $B(0, (1+\gamma/\beta)\|z^0 - z^*\|)$. The proofs use Lemma 3.1, whose ball is centred at $x^*$, so the ball here is centred at $x^*$. "$f$ is $L$-Lipschitz on the ball" is stated as: $f$ is finite on the ball, and its real-valued restriction is $L$-Lipschitz there.
• O(·) and o(·). $O(1/(k+1))$ is $\exists C \in \mathbb R,\ \forall k,\ (f+g+h)(\bar x^k_g) \le (f+g+h)(x^*) + C/(k+1)$, with $C$ chosen after all data. $o(1/\sqrt{k+1})$ is $\sqrt{k+1}\,\big((f+g+h)(x^k_g) - (f+g+h)(x^*)\big) \to 0$, together with finiteness of the objective values as part of the conclusion. No explicit constant from the proof is stated, because the published constant drops a factor.
• Corollary 2.1 Part 1 and Eq. (2.7) are stated for Algorithm 2 with $\lambda_k \equiv 1$, $\gamma \in (0, 2\beta)$ and $\varepsilon \in (\gamma/(2\beta), 1)$. As printed, Corollary 2.1's condition on $\tau_k$ excludes $\lambda_k \equiv 1$, but Section 3 uses Part 1 in exactly this case. Summability in (2.7) is part of the conclusion.
• Trivialization ruled out. Objective values are extended reals, and the goal compares them without subtraction. The value $(f+g+h)(x^*)$ is proved finite as part of the conclusion. So the goal cannot hold through $\infty - \infty$ or through an infinite right-hand side.

Welcome contributions: the prox–subgradient inclusion for EReal-valued convex functions, averagedness and Fejér monotonicity of $T$ (the companion mission on Section 2 treats the general operator case), a weighted Jensen inequality in EReal, and proofs of the milestones in the listed order.

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
• 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
• P.-L. Lions and B. Mercier, Splitting Algorithms for the Sum of Two Nonlinear Operators, SIAM J. Numer. Anal. 16 (1979) 964–979. https://doi.org/10.1137/0716071
• D. Davis and W. Yin, Convergence Rate Analysis of Several Splitting Schemes, in Splitting Methods in Communication, Imaging, Science, and Engineering, Springer, 2016. https://doi.org/10.1007/978-3-319-41589-5_4

Motivation

Infinite-horizon optimal control problems with nonnegative costs (Strauch's negative dynamic programming, the positive-cost counterpart of Blackwell's positive model) are among the settings where the standard tools of discounted dynamic programming fail: there is no contraction, costs may be infinite, and the value-iteration algorithm started from zero may converge to the wrong limit. Strauch showed in 1966 that under these assumptions the limit of value iteration can lie strictly below the optimal cost (Strauch 1966). Bertsekas (1977) recast the deterministic, stochastic and minimax versions of these problems as one abstract problem about a monotone mapping $H$, and proved Bellman's equation, optimality criteria for stationary policies, and conditions for convergence of the dynamic programming algorithm at that level of generality (Bertsekas 1977). This framework became the basis of the "abstract dynamic programming" theory developed later in Bertsekas and Shreve (1978) and Bertsekas (2013, 2022).

This mission formalizes the part of the paper that works under the uniform increase assumption, culminating in the paper's compactness condition for convergence of value iteration.

Setting

A model consists of a nonempty state space $S$, a control space $C$, for each $x\in S$ a nonempty constraint set $U(x)\subseteq C$, a mapping $H:S\times C\times F\to[-\infty,+\infty]$, where $F$ is the set of functions $J:S\to[-\infty,\infty]$ ordered pointwise, and a terminal function $\bar J\in F$ with $\bar J(x)>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for $u\in U(x)$.

A selector is $\mu:S\to C$ with $\mu(x)\in U(x)$; a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors, and $\{\mu,\mu,\dots\}$ is stationary. Define

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$ $$J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J)(x),\qquad J^*(x)=\inf_\pi J_\pi(x),\qquad J_\infty(x)=\lim_{N\to\infty}T^N(\bar J)(x).$$

$J^*$ is the optimal value function and $J_\infty$ the limit of the dynamic programming algorithm. A policy is optimal if $J_\pi=J^*$.

Assumption I is $\bar J(x)\le H(x,u,\bar J)$ for all $x$ and $u\in U(x)$. Assumption I.1 says that $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $\bar J$. Assumption I.2 says there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+re)\le H(x,u,J)+\alpha r$ for $r>0$ and $J\ge\bar J$, where $e\equiv1$. For the convergence analysis the paper introduces, for $k\ge1$, the sets $C_k=\{(x,u,\lambda)\mid u\in U(x),\ H[x,u,T^{k-1}(\bar J)]\le\lambda\}$ with $\lambda$ real, their projections $P(C_k)$ on $(x,\lambda)$ through admissible $u$, and the closure $\overline{P(C_k)}$ obtained by adding limits of real sequences $\lambda_n$ at fixed $x$.

Formalization targets

Goal: Proposition 12

Let I, I.1, I.2 hold, let $C$ be a Hausdorff topological space, and suppose there is $\bar k$ such that $U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ is compact for every $x$, real $\lambda$ and $k\ge\bar k$. Then

$$P\Bigl(\bigcap_{k\ge1}C_k\Bigr)=\bigcap_{k\ge1}\overline{P(C_k)},\qquad J_\infty=T(J_\infty)=T(J^*)=J^*,$$

and there exists an optimal stationary policy.

Milestones

In attack order: Proposition 2 ($J_N=T^N(\bar J)$ for the $N$-stage problem); Proposition 4 ($\varepsilon$-optimal policies, stationary when $\alpha<1$); Proposition 5 (Bellman's equation $J^*=T(J^*)$ and minimality of $J^*$ among $T$-excessive functions above $\bar J$); Corollary 5.1 (the same for $J_\mu$); Proposition 7 ($\{\mu^*,\mu^*,\dots\}$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$); Proposition 10 ($J_\infty\le T(J_\infty)\le T(J^*)=J^*$, with equality throughout iff $J_\infty=T(J_\infty)$); Lemma 2 ($\overline{P(C_k)}=E[T^k(\bar J)]$, the epigraph); Proposition 11 (convergence of value iteration is equivalent to interchanging projection and intersection); Lemma 3 (a function with compact real sublevel sets attains its minimum).

Significance

The result. Proposition 12 gives a checkable condition, compactness of sublevel sets of the one-stage costs, under which value iteration started at $\bar J$ converges to the optimal cost and an optimal stationary policy exists, in any model covered by the abstract framework: deterministic and stochastic control with nonnegative costs, minimax control, and problems with state constraints encoded by infinite costs. Without such a condition the algorithm can stall below $J^*$ even in one-dimensional deterministic problems. Propositions 5 and 7 are the abstract form of the classical Bellman equation and optimality criterion for positive-cost problems.

Formalizing it. The results are proved in the paper. The platform's existing dynamic programming results are finite-state, real-valued and contraction-based; none covers extended-real costs, general state spaces, or the uniform increase regime. This mission would produce a machine-checked abstract DP layer over EReal in which the Bellman equation, the stationary-policy criterion and the convergence conditions are proved once for every model satisfying the assumptions. No machine-checked proof of these results is known.

Difficulty

The obvious argument for $J_\infty=J^*$ interchanges a limit in $N$ with an infimum over policies. Under Assumption I the iterates increase, and a limit of infima of an increasing family can be strictly smaller than the infimum of the limits; the paper's own example in Section 1 shows it. Monotone convergence arguments therefore do not apply. The paper converts the interchange into a statement about projections of the sets $C_k$ and closes the gap with a compactness argument, which requires handling infinite values carefully: epigraphs are taken over real $\lambda$ only, and states where the value is $+\infty$ are treated separately. Proposition 4, on which Bellman's equation rests, needs a selection of nearly optimal policies state by state and a geometric control of the errors through I.2.

Formalization scope

Functions in $F$ are S → EReal. Policies are sequences ℕ → Selector, where a selector is a function with $\mu(x)\in U(x)$ for all $x$. The composition $T_{\mu_0}\cdots T_{\mu_{N-1}}$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ and $J_\infty$ are limUnder atTop of their defining sequences. Every statement assumes Assumption I, under which these sequences are nondecreasing and the limits exist. $T$ takes the infimum over $U(x)$ only and $J^*$ over admissible policies only. Both $S$ and each $U(x)$ are nonempty. $\lambda$ ranges over $\mathbb R$, and the closure $\overline{\,\cdot\,}$ is the sequential closure in $\lambda$ at fixed $x$, not a topological closure on $S\times\mathbb R$. The sets $C_k$ are used only for $k\ge1$. I.2 is parameterized by its scalar $\alpha$. Proposition 4's second part refers to the $\alpha$ for which I.2 is assumed.

Repairs of the page. Lemma 3 is false as printed. On $\mathbb N$ with the cofinite topology every subset is compact, yet $f(n)=-n$ has no minimum. It also fails for $U=\emptyset$. The mission states Lemma 3 for a Hausdorff space $C$ and nonempty $U$, and Proposition 12 for a Hausdorff control space. Proposition 12 is also false as printed: with $S=\{0\}$, $C=U(0)=\mathbb N$ cofinite, $\bar J(0)=0$ and $H(0,u,J)=J(0)+1/(u+1)$, all hypotheses hold but no stationary policy is optimal and (70) fails. Proposition 11(b)'s parenthetical "(equivalently there exists an optimal stationary policy)" holds only together with $J_\infty=J^*$ (the paper cites an example with an optimal stationary policy and $J_\infty\neq J^*$). It is stated in that joint form, never as an equivalence between condition (68) and the bare existence of an optimal stationary policy.

Trivializing readings ruled out. An empty constraint set would make $T\equiv+\infty$ and the policy set empty, so every Bellman identity would hold trivially. The model therefore requires $U(x)\neq\emptyset$. The goal's three conclusions, (70), the chain of equalities and the optimal stationary policy, are all required, so a formalization that states only one of them is not the goal.

Needed infrastructure: monotone limits in EReal, infima over sets, and compactness in Hausdorff spaces (Mathlib's Cantor intersection theorem). The definitions (model, assumptions, epigraph sets) can be reused for the companion mission under Assumption D and for later abstract DP developments. Proofs of any milestone are welcome, as are reusable lemmas on monotone EReal sequences.

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
• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699369
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. http://web.mit.edu/dimitrib/www/abstractdp.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

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

The Steiner problem in graphs asks for the cheapest way to connect a prescribed set of nodes of a network, where intermediate nodes may be used freely. It is the network version of the classical Euclidean Steiner tree problem surveyed by Gilbert and Pollak (SIAM J. Appl. Math. 16, 1968), and it arises wherever a few sites must be joined through an existing network at minimum total cost: communication and pipeline layout, VLSI routing, and phylogenetics. With two terminals it is the shortest-path problem; with all nodes as terminals it is the minimum spanning tree problem; in between it is NP-hard.

Dreyfus and Wagner (Networks 1(3):195–207, 1971) gave the first exact algorithm whose running time is exponential only in the number $k$ of terminals and polynomial in the number $n$ of nodes. The paper states it, as Algorithm A, together with its proof of correctness and an exact count of its elementary operations.

Timeline. 1968: Gilbert and Pollak survey Steiner minimal trees. 1971: Dreyfus and Wagner, a dynamic program over subsets of terminals running in time proportional to $n^3/2 + n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$. 1987: Erickson, Monma and Veinott give the same subset recursion for general network flow problems. 2007: Björklund, Husfeldt, Kaski and Koivisto (STOC 2007) improve the exponential dependence on $k$ for small integer weights. The Dreyfus–Wagner recursion remains the standard exact method and the basis of the fixed-parameter tractability of the problem in $k$.

Setting

A graph $G = (N, A)$ has a finite set $N$ of nodes and a set $A$ of undirected arcs, each arc $a$ having a positive length $|a|$; $G$ is connected. For a set $S \subseteq A$ of arcs, $|S| = \sum_{s \in S} |s|$. A set $S$ connects a node set $X$ if all members of $X$ are joined by paths composed only of arcs in $S$.

Given $Y \subseteq N$, a Steiner path (or Steiner tree) connecting $Y$ is a set $S \subseteq A$ that connects $Y$ with $|S|$ minimum. Its length is the Steiner length $\operatorname{St}(Y)$. For nodes $i, j$, $D(i,j)$ is the length of a shortest path from $i$ to $j$; $D(i,j) = \operatorname{St}(\{i,j\})$.

Algorithm A fixes a linear order of $N$ (so that each nonempty set $D$ has a first element $D[1]$), picks $q \in Y$, sets $C = Y - \{q\}$, and fills a table $S[D, I]$ for nonempty $D \subsetneq C$ and $I \in N$:

$$S[\{t\}, I] = D(t, I), \qquad S[D, I] = \min_{J \in N}\Big(D(I,J) + \min_{D[1] \in E \subsetneq D}\big(S[E,J] + S[D-E,J]\big)\Big),$$

and returns

$$v = \min_{J \in N}\Big(D(q,J) + \min_{C[1] \in E \subsetneq C}\big(S[E,J] + S[C-E,J]\big)\Big).$$

A minimum over an empty set is $+\infty$. In the Lean development these objects are steinerLength, pathDist, tableA and algorithmA in the namespace DreyfusWagner.Steiner.

Formalization targets

Goal: Algorithm A is exact

For every finite connected graph with positive arc lengths, every linear order on its nodes, every $Y$ with $\|Y\| \ge 3$ and every $q \in Y$,

$$v = \operatorname{St}(Y).$$

This is the caption of Algorithm A ("Computes the length of the Steiner tree connecting $Y$", p. 203). The statement is an equality, not a bound.

Milestones

In the order the proof uses them:

1. A Steiner path is a tree (§1, p. 197): a minimum connecting arc set contains no cycle.
2. The two-node case (Appendix A, p. 205): $\operatorname{St}(\{i,j\}) = D(i,j)$.
3. Theorem 1 (Appendix A, p. 206): for a Steiner tree $S$, a node $x$ on it, and a set $C$ of arcs of $S$ at $x$, the arcs of $S$ connecting $x$ to the terminals reached through $C$ form a Steiner tree for those terminals together with $x$.
4. Optimal Decomposition Theorem (Appendix A, p. 206): if $\|Y\| \ge 3$ and $q \in Y$, a Steiner tree for $Y$ splits into three disjoint Steiner paths, for $\{p,q\}$, $\{p\} \cup D$ and $\{p\} \cup (Y - D - \{q\})$, where $p \in N$ and $\emptyset \ne D \subsetneq Y - \{q\}$.
5. The recurrence (§2, pp. 199–200): for $\|D\| \ge 2$ and any node $m$,

$$\operatorname{St}(\{m\} \cup D) = \min_{k \in N}\Big(D(m,k) + \min_{\emptyset \ne E \subsetneq D}\big(\operatorname{St}(\{k\} \cup E) + \operatorname{St}(\{k\} \cup (D - E))\big)\Big).$$

6. The table invariant (§2, p. 200): $S[D, I] = \operatorname{St}(\{I\} \cup D)$ for every nonempty $D$ and every $I$.

Two companion items accompany the goal: the numerical illustration of §3 (seven nodes, $\operatorname{St}(Y) = 5$, Algorithm A returns $5$), and the exact count of elementary statements of §5, $n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$.

Significance

The result turns the Steiner problem with few terminals into a polynomial computation in the size of the network: for fixed $k$ the running time is $O(n^3)$ including all-pairs shortest paths. It is the reference exact algorithm against which heuristics and approximation algorithms for Steiner trees are evaluated, a standard example of dynamic programming over subsets, and the origin of the fixed-parameter tractability of the Steiner tree problem parameterized by the number of terminals. The subset recurrence reappears in group Steiner, prize-collecting and directed Steiner variants.

The paper's proof is complete and the result is classical; it has not, to our knowledge, been machine-checked. This mission produces a checked account of the exactness of the recursion: the structural facts about minimum connecting arc sets (acyclicity, optimality of branches, the three-way decomposition) and the passage from these to the algorithm's table. These facts about weighted graphs, minimum connecting arc sets and shortest paths are reusable well beyond this paper.

Difficulty

The upper bound $v \ge \operatorname{St}(Y)$ is routine: each term of each minimum is the length of some connecting arc set, so no term can beat the optimum. The content is the reverse inequality, which needs the Optimal Decomposition Theorem: one must show that some optimal tree actually splits at a single node $p$ into a shortest path to $q$ and two optimal subtrees whose terminal sets partition $Y - \{q\}$ into two nonempty parts. The naive choice $p = q$ fails when $q$ is a leaf, and the choice of the first branching node fails when the path from $q$ meets another terminal first; the paper handles these as separate cases. A second difficulty is the passage from arc sets to trees: minimum connecting sets are forests only because lengths are positive, and "the arcs of $S$ involved in connecting" a set of terminals must be identified with a subtree. Finally the table recursion must be matched with the recurrence, including the restriction $D[1] \in E$ that enumerates each splitting once.

Formalization scope

Nodes are a finite type V with a LinearOrder (the paper's "(ordered) set"; the goal holds for every order). The graph is a SimpleGraph V with decidable adjacency, arcs are unordered pairs Sym2 V, and lengths are ℓ : Sym2 V → ℝ. Every theorem assumes the paper's standing hypotheses of p. 195: all arcs of $G$ have positive length (∀ e ∈ G.edgeSet, 0 < ℓ e) and $G$ is connected. The paper allows several arcs between the same two nodes; the simple-graph model keeps one, which does not change any Steiner length since an optimal set uses only the shortest of parallel arcs. Connecting means reachability in the graph formed by the arcs of $S$. Steiner lengths, $D(i,j)$ and all minima of the algorithm take values in WithTop ℝ, where ⊤ is $+\infty$, ⊤ + x = ⊤ and an empty minimum is ⊤; no real-valued infimum with a junk value is used. $D(i,j)$ is a minimum over paths of $G$.

The goal assumes $\|Y\| \ge 3$, the paper's own hypothesis (Appendix A, p. 205). For $\|Y\| = 2$ Algorithm A as printed returns $+\infty$ because line (18) admits no set $E$; the two-node case is covered by milestone 2. The algorithm is defined from $D(i,j)$, addition and minima only: a formalization in which tableA or algorithmA refers to Steiner lengths, or in which the goal only asserts $v \ge \operatorname{St}(Y)$, would be trivial and is ruled out. The loop order of lines (4)–(14) is replaced by recursion on $\|D\|$, which the paper states is immaterial (p. 203).

Useful infrastructure: sums of lengths along walks and paths, reachability in edge-subgraphs, acyclicity of minimum connecting sets, and splitting a tree at a node. Contributions of these as reusable lemmas are welcome, as are proofs of individual milestones in any order. Tree reconstruction (§2, p. 200) and the empirical running times (p. 205) are out of scope.

Selected references

• S. E. Dreyfus, R. A. Wagner, The Steiner Problem in Graphs, Networks 1(3):195–207, 1971. https://doi.org/10.1002/net.3230010302
• E. N. Gilbert, H. O. Pollak, Steiner Minimal Trees, SIAM Journal on Applied Mathematics 16(1):1–29, 1968. https://doi.org/10.1137/0116001
• R. W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6):345, 1962. https://doi.org/10.1145/367766.368168
• R. E. Erickson, C. L. Monma, A. F. Veinott Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4):634–664, 1987. https://doi.org/10.1287/moor.12.4.634
• A. Björklund, T. Husfeldt, P. Kaski, M. Koivisto, Fourier Meets Möbius: Fast Subset Convolution, STOC 2007, 67–74. https://doi.org/10.1145/1250790.1250801

Motivation

Von Neumann's minimax theorem says that in a zero-sum game with real payoffs, Player I can guarantee an expected gain of at least the value $v$ and Player II can hold it to at most $v$. In a long series of plays, the law of large numbers turns this into a statement about the average payoff: I can make it exceed $v-\varepsilon$, II can keep it below $v+\varepsilon$, with probability approaching one.

Blackwell's 1956 paper asks the same question when the payoff of each play is a vector in $\mathbb R^N$ rather than a number. A single player then cannot optimize "the" payoff, and the natural question becomes geometric: can a player force the running average of the payoff vectors to converge to a prescribed set $S$, whatever the opponent does? The resulting notion, approachability, became a basic tool in repeated games with incomplete information (Aumann–Maschler), in the theory of calibration and regret minimization (Foster–Vohra; Hart–Mas-Colell), and in online learning, where no-regret algorithms and Blackwell approachability are known to be equivalent (Abernethy–Bartlett–Hazan 2011).

Timeline.

• 1928: von Neumann's minimax theorem for matrix games.
• 1954: Blackwell's maximal inequality for sums with negative conditional drift (On optimal systems, Ann. Math. Statist.), quoted in this paper as THEOREM 2.
• 1956: this paper. A sufficient condition for approachability (THEOREM 1), a complete characterization for closed convex sets (THEOREM 3) and for $N=1$, an example of a set that is neither approachable nor excludable, and a conjecture on weak approachability.
• 1992: Vieille proved Blackwell's conjecture that every set is weakly approachable or weakly excludable.

Setting

Fix integers $N\ge0$ and $r,s\ge1$, and a closed, bounded, convex set $X\subseteq\mathbb R^N$. The game is an $r\times s$ matrix $M=\|m(i,j)\|$ whose entries are probability distributions concentrated on $X$. Write $\bar m(i,j)$ for the mean of $m(i,j)$, $P$ for the simplex of mixed actions $p=(p_1,\dots,p_r)$ of Player I, and $Q$ for that of Player II.

A strategy $f=\{f_n\}_{n\ge0}$ of I is a sequence of measurable maps from the $n$-tuples $(x_1,\dots,x_n)$ of past outcomes to $P$; $f_0$ is a point of $P$. Strategies $g=\{g_n\}$ of II take values in $Q$. A play of $(f,g)$ is a sequence of random vectors $x_1,x_2,\dots$ such that, given $x_1,\dots,x_n$, the players draw $i$ and $j$ independently from $f_n(x_1,\dots,x_n)$ and $g_n(x_1,\dots,x_n)$, and $x_{n+1}$ is drawn from $m(i,j)$. The average payoff is $\bar x_n=\frac1n\sum_{i=1}^n x_i$, and $\delta_n$ is its distance from $S$.

A set $S\subseteq\mathbb R^N$ is approachable with $f^*$ if for every $\varepsilon>0$ there is $N_0$ such that for every strategy $g$ of II,

$$\mathrm{Prob}\{\delta_n\ge\varepsilon\text{ for some }n\ge N_0\}<\varepsilon .$$

It is excludable with $g^*$ if there is $d>0$ such that for every $\varepsilon>0$ there is $N_0$ such that for every strategy $f$ of I,

$$\mathrm{Prob}\{\delta_n\ge d\text{ for all }n\ge N_0\}>1-\varepsilon .$$

$S$ is approachable (excludable) if some strategy approaches (excludes) it. Finally, for $p\in P$ and $q\in Q$,

$$R(p)=\operatorname{conv}\Big\{\textstyle\sum_i p_i\bar m(i,j)\Big\}_{j=1}^{s},\qquad T(q)=\operatorname{conv}\Big\{\textstyle\sum_j q_j\bar m(i,j)\Big\}_{i=1}^{r}:$$

$R(p)$ is the set of expected payoffs I can guarantee to stay in by playing $p$, and $T(q)$ the set II can confine them to by playing $q$.

Formalization targets

Goal: THEOREM 3

For a closed convex set $S\subseteq\mathbb R^N$,

$$S\text{ is approachable}\iff S\cap T(q)\neq\emptyset\ \text{ for every }q\in Q,$$

and if $S\cap T(q_0)=\emptyset$ then $S$ is excludable with the stationary strategy $g_n\equiv q_0$. In particular every closed convex set is either approachable or excludable. Both sentences are part of the goal.

Milestones, in the paper's order

1. THEOREM 2: for $|z_k|\le1$ with $E(z_k\mid z_1,\dots,z_{k-1})\le-u\,E(|z_k|\mid z_1,\dots,z_{k-1})$ and $0<u<1$,

$$\mathrm{Prob}\{z_1+\dots+z_k\ge t\text{ for some }k\}\le\Big(\tfrac{1-u}{1+u}\Big)^t .$$

2. The LEMMA: a sequence satisfying the almost-supermartingale conditions (5), (6), (7) converges to $0$ at a rate depending only on the constants $a,b,c$.
3. In the proof of THEOREM 1, the squared distances $\delta_n^2$ satisfy (5)–(7) uniformly in II's strategy.
4. THEOREM 1: if every $x\notin S$ admits $p(x)\in P$ such that the hyperplane through a closest point $y\in S$, perpendicular to $xy$, separates $x$ from $R(p(x))$, then $S$ is approachable with any strategy playing $p(\bar x_n)$ when $\bar x_n\notin S$.
5. No set is both approachable and excludable.
6. If a closed $S$ is approachable in the transpose $M'$ with $f$, then every closed $T$ disjoint from $S$ is excludable in $M$ with $f$.
7. A closed convex $S$ meeting every $T(q)$ satisfies THEOREM 1's hypothesis.
8. Every $T(q_0)$ is approachable in $M'$ with $f_n\equiv q_0$.

Significance

The result. THEOREM 3 is the vector analogue of the minimax theorem. For a closed convex target it reduces an infinite-horizon stochastic question, about every strategy of the opponent over all histories, to a finite family of one-shot conditions on the mean matrix $\bar M$, and it shows that the game is determined for convex targets: one of the two players always wins. Its sufficient condition, THEOREM 1, is the origin of the "Blackwell strategy", which steers the average toward the target by playing, at each step, a mixed action that pushes the expected next payoff across the supporting hyperplane. Regret-matching, calibration algorithms and the reductions between online linear optimization and approachability are instances of this construction.

Formalizing it. The result is proved in the paper; to the best of available knowledge no machine-checked proof of it exists. This mission produces one: the stochastic model of a repeated game with vector payoffs, the probabilistic estimates (THEOREM 2 and the LEMMA) with the uniform rate the paper claims, and the minimax reduction for convex sets. A related platform mission, Introduction to Online Convex Optimization XIII, states a deterministic, sufficiency-only textbook variant for bounded sets; the present mission covers the stochastic model, unbounded convex targets, and the excludability half.

Difficulty

The obvious argument shows that the expected squared distance $E\delta_n^2$ decreases like $1/n$. That is not approachability: the definition asks for the probability that the average is ever again $\varepsilon$-far after time $N_0$, uniformly over the opponent's strategies. Controlling the whole tail of the path, with a threshold $N_0$ that does not depend on the opponent, is the step that fails for a naive expectation bound and is why the paper needs a maximal inequality for sums with negative conditional drift. On the geometric side, the "only if" direction is not automatic: it requires that approachability and excludability be incompatible, which in turn requires that a play of every pair of strategies exists.

Formalization scope

Points live in EuclideanSpace ℝ (Fin N); pure actions are Fin r and Fin s; mixed actions are elements of stdSimplex. The game is a structure carrying $X$ (closed, bounded, convex) and the distributions $m(i,j)$ (probability measures with $m(i,j)(X^{c})=0$). A play is described by the conditional law of the next outcome given the past, and approachability and excludability quantify over every probability space in Type carrying such a play. Distances are extended (Metric.infEDist), equal to $+\infty$ to the empty set.

Conventions and disclosed additions:

• $r,s\ge1$ where a statement needs both players to have strategies;
• strategies are measurable in the history;
• outcomes are indexed from $1$; (5) and (7) start at $n=2$, (6) at $n=1$;
• "the closest point" in THEOREM 1 is some closest point, and "separates" is weak separation;
• THEOREM 2 is stated with $E(|z_k|\mid\cdot)$ in place of the printed "max" (the weaker hypothesis, as in the cited source), and with $u<1$ so that $((1-u)/(1+u))^t$ is a real power.

$S$ is not assumed bounded or nonempty. With the real-valued distance, the empty set would be approachable with every strategy and THEOREM 3 would be false; the extended distance rules this out. Stating only the sufficiency direction, fixing the approaching strategy in the hypotheses, or assuming a play exists would each trivialize the goal, and none is done.

A complete development needs: conditional laws of the next outcome from a strategy pair (Ionescu–Tulcea, Kernel.traj in Mathlib), a nonnegative-supermartingale maximal inequality, the metric projection onto closed convex sets, and the minimax theorem (Mathlib's Sion theorem). The maximal inequality of THEOREM 2 and the LEMMA are reusable beyond this mission. Contributions to any milestone, and to a construction of plays, are welcome.

Selected references

• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific J. Math. 6(1):1–8, 1956. https://doi.org/10.2140/pjm.1956.6.1
• D. Blackwell, On optimal systems, Ann. Math. Statist. 25(2):394–397, 1954. https://doi.org/10.1214/aoms/1177728796
• N. Vieille, Weak approachability, Math. Oper. Res. 17(4):781–791, 1992. https://doi.org/10.1287/moor.17.4.781
• J. Abernethy, P. Bartlett, E. Hazan, Blackwell approachability and no-regret learning are equivalent, COLT 2011. https://arxiv.org/abs/1011.1936
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5):1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153