Optimization

Motivation

Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).

The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).

Setting

Let $E$ be a nonempty finite set of states. Each $i\in E$ has a nonempty finite action set $A(i)$. Taking $a\in A(i)$ earns a real reward $r_{ia}$ and moves to $j$ with probability $p_{iaj}\ge 0$. A row may sum to less than one; the missing probability is termination. A policy $R$ specifies a probability distribution over $A(i)$ after every finite history ending in $i$. A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action $f(i)$ in each state. These are the classes $C$, $C_M$, $C_S$, and $C_D$ of §2.2 (Kallenberg 1983, pp. 19–21).

The standing contraction assumption supplies weights $\mu_i>0$ and $0\le\alpha<1$ with

$$\sum_{j\in E}p_{iaj}\mu_j\le\alpha\mu_i \qquad(i\in E,\ a\in A(i)).$$

It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).

For an initial probability distribution $\beta$, with $\beta_i\ge0$ and $\sum_i\beta_i=1$, write $x_{ja}(R)$ for the expected total number of visits to state $j$ at which action $a$ is chosen, averaged over the initial state. Let $K$, $K(M)$, $K(S)$, and $K(D)$ collect these frequency vectors for the four policy classes. The frequency polytope $P$ consists of nonnegative vectors $x$ satisfying conservation of expected flow at each state:

$$\sum_{a\in A(j)}x_{ja} -\sum_{i\in E}\sum_{a\in A(i)}p_{iaj}x_{ia}=\beta_j \qquad(j\in E).$$

These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).

Formalization targets

The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every $\beta_i>0$, and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).

The mission goal allows zero entries in the initial distribution and compares all four policy classes:

$$\overline{K(D)}=K(S)=K(M)=K=P.$$

The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, $K(D)$ is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).

Significance

The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over $P$ without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).

The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.

Difficulty

For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of $K$ with $P$ therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When $\beta_j=0$, different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).

Formalization scope

States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index $n=0$ represents the book's period $t=1$. The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.

The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository copy.

Motivation

Many problems in mechanics and optimal control are posed as the minimization of a convex functional of the form $f(Av)-\langle b,v\rangle$, where $A$ is a differential operator and $f$ is non-smooth: an obstacle, a friction term, a plasticity threshold. Splitting the variable, $y=Av$, separates the linear operator from the non-smooth function, and a Lagrange multiplier for the constraint $Av-y=0$ turns the problem into a sequence of two simpler ones: a linear system in $v$ and a pointwise nonlinear problem in $y$. The scheme that alternates between the two and then updates the multiplier is now called the alternating direction method of multipliers (ADMM). It is one of the standard algorithms of large-scale convex optimization, statistics and imaging (Boyd, Parikh, Chu, Peleato and Eckstein, 2011).

Gabay and Mercier (IRIA report RR-126, 1975; Comput. Math. Appl., 1976) gave a convergence proof of this method in Hilbert space, for a stepsize $\rho$ anywhere in $(0,2r)$, where $r$ is the penalty parameter of the augmented Lagrangian.

Timeline.

• 1969: Hestenes and Powell introduce the augmented Lagrangian (method of multipliers).
• 1975: Glowinski and Marrocco propose the alternating scheme for nonlinear Dirichlet problems.
• 1975–76: Gabay and Mercier prove strong convergence of the primal iterates for $0<\rho<2r$ under strong monotonicity of $f_1'$ (this mission).
• 1983: Gabay identifies ADMM with Douglas–Rachford splitting applied to the dual.
• 1992: Eckstein and Bertsekas extend convergence to maximal monotone operators, without strong monotonicity, for $\rho=r$.

Setting

$V$ and $Y$ are real Hilbert spaces; $(\cdot,\cdot)$ and $|\cdot|$ are the inner product and norm of $Y$, $\|\cdot\|$ the norm of $V$. $A:V\to Y$ is a continuous linear operator and $b$ is a continuous linear functional on $V$, with value $\langle b,v\rangle$ at $v$. The dual of $Y$ is identified with $Y$. The function $f:Y\to(-\infty,+\infty]$ is a sum $f=f_1+f_2$ where

1. $f_1:Y\to\mathbb R$ is convex and continuously differentiable, and its gradient is strongly monotone: $(f_1'(y)-f_1'(z),y-z)\ge\gamma|y-z|^2$ for some $\gamma>0$ (2.3);
2. $f_2$ is proper (never $-\infty$, somewhere finite), convex and lower semicontinuous;
3. $|Av|^2\ge\alpha^2\|v\|^2$ for some $\alpha>0$ (2.5);
4. some $Av_0$ lies in the interior of $\operatorname{dom}f_2=\{y:f_2(y)<+\infty\}$ (qualification).

The problem is

$$(\mathcal P)\qquad \inf_{v\in V}\ f(Av)-\langle b,v\rangle ,$$

and a solution $v^*$ is a point where this value is finite and minimal. The Lagrangian and augmented Lagrangian are, for $\lambda\in Y$ and $r>0$,

$$\mathcal L(v,y;\lambda)=f(y)+(\lambda,Av-y)-\langle b,v\rangle,\qquad \mathcal L_r=\mathcal L+\frac r2|Av-y|^2 .$$

The modified dual algorithm (3.4) starts from any $(y^0,\lambda^0)\in Y\times Y$ and, for $n\ge0$,

1. finds $v^{n+1}$ with $r(Av^{n+1},Aw)=(ry^n-\lambda^n,Aw)+\langle b,w\rangle$ for all $w\in V$ (minimization of $\mathcal L_r$ in $v$);
2. finds $y^{n+1}$ with $\lambda^n+rAv^{n+1}-ry^{n+1}-f_1'(y^{n+1})\in\partial f_2(y^{n+1})$ (minimization of $\mathcal L_r$ in $y$);
3. sets $\lambda^{n+1}=\lambda^n+\rho(Av^{n+1}-y^{n+1})$.

$P$ denotes the orthogonal projection of $Y$ onto the range $R(A)$, which is closed by (2.5).

Formalization targets

Goal: Theorem 3.1

For $r>0$ and every stepsize with

$$0<\rho<2r,$$

every run of the algorithm satisfies

$$\|v^n-v^*\|\to0,\qquad |y^n-Av^*|\to0,\qquad \sup_n|\lambda^n|<\infty,$$

where $v^*$ is the unique solution of $(\mathcal P)$. The multipliers need not converge.

Milestones

1. Proposition 2.1: $(\mathcal P)$ has a unique solution.
2. Theorem 2.1: a saddle point $(v^*,y^*;\lambda^*)$ of $\mathcal L$ consists of the solution $v^*$, $y^*=Av^*$ and $\lambda^*\in\partial f(Av^*)$ with $A'\lambda^*=b$; and a saddle point exists.
3. Theorem 2.2: for $r>0$, $\mathcal L_r$ and $\mathcal L$ have the same saddle points.
4. (3.8)–(3.10): a saddle point is a fixed point of Steps 1–2.
5. (3.11)–(3.12): $A(v^{n+1}-v^*)=P(y^n-y^*)-\frac1rP(\lambda^n-\lambda^*)$.
6. (3.19)–(3.20): the energy estimate

$$\gamma|y^{n+1}-y^*|^2+\Bigl(r-\frac\rho2\Bigr)|(I-P)(y^{n+1}-y^*)|^2+\frac r2|P(y^{n+1}-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^{n+1}-\lambda^*)|^2\le\frac r2|P(y^n-y^*)|^2+\frac1{2\rho}|(I-P)(\lambda^n-\lambda^*)|^2$$

and its sum over $n=0,\dots,N$. 7. $y^n\to y^*$ for $0<\rho\le2r$. 8. (3.22)–(3.23): a contraction-plus-summable-forcing recursion for $|P(\lambda^n-\lambda^*)|^2$, and the scalar lemma that such recursions tend to $0$. 9. $P(\lambda^n-\lambda^*)\to0$ and $v^n\to v^*$ for $0<\rho<2r$.

Significance

The theorem says that ADMM converges without any step-size tuning beyond $\rho<2r$, and that the primal iterates converge in norm in infinite dimension, which is what makes the method usable for finite element discretizations of variational problems (the companion mission on internal approximations treats the discretization). It covers obstacle problems, Bingham fluids and elasto-plastic torsion, where $f_2$ is an indicator or a non-differentiable norm.

The result is proved in the 1975 report. To our knowledge it has no machine-checked proof. Formalizing it adds a library-level convergence theorem for ADMM in Hilbert space with $\mathrm{EReal}$-valued convex functions, a saddle-point existence theorem for linearly constrained convex problems, and the energy estimate (3.19) as a reusable lemma. The formalization also fixes two defects of the printed text (see Formalization scope): a sign in Step 1 and a qualification hypothesis that is too weak.

Difficulty

The energy estimate (3.19) only controls the multiplier through its component in $R(A)^\perp$, and only the $y$-error through $\gamma>0$. The natural first idea, a Lyapunov function in $|\lambda^n-\lambda^*|^2$ alone that decreases at each step, does not work for $\rho\ne r$: the component $P(\lambda^n-\lambda^*)$ obeys a separate recursion whose contraction factor $|1-\rho/r|$ is below one only for $0<\rho<2r$, and whose forcing term must be shown summable from the $y$-estimate. The existence of a multiplier, i.e. of a saddle point, is a separate difficulty: it needs the subdifferential chain rule $\partial(f\circ A)=A'\partial f(A\,\cdot)$ in infinite dimension, under a constraint qualification.

Formalization scope

Lean conventions:

• $V$, $Y$ are InnerProductSpace ℝ with CompleteSpace; multipliers are elements of $Y$; $b$ is a StrongDual ℝ V.
• $f_1:Y\to\mathbb R$ (a Gateaux-differentiable function is finite), with a gradient f₁' at every point (HasGradientAt) that is continuous; "weakly continuous on finite-dimensional subspaces" is then automatic.
• $f_2:Y\to$ EReal, with IsProperFn, IsConvexFn, IsSubgradient from the published InertialFB.IFB.ConvexAnalysis and Mathlib's LowerSemicontinuous. No subtraction in EReal occurs: the variational inequalities (3.6), (3.9) are stated as subgradient inclusions, and the Lagrangians as a real part plus $f_2(y)$.
• A solution of $(\mathcal P)$ has finite value. A run is any triple of sequences indexed by $\mathbb N$ satisfying Steps 1–3 for every $n$; the start is arbitrary, and the well-posedness of the steps is not assumed or used.
• $P$ is the orthogonal projection onto the closure of $R(A)$, equal to $R(A)$ under (2.5).
• Strong convergence is convergence in norm; "bounded" is Bornology.IsBounded (Set.range λ).

Corrections to the printed text, each explained in the item's statement:

• Step 1 (3.5) and (3.8) carry $+\langle b,v\rangle$. The paper prints $-\langle b,v\rangle$ there and in Remark 1 of p. 15, which is inconsistent with $\mathcal L$ and $(\mathcal P)$: with the printed sign the iteration solves the problem with $-b$.
• The qualification (2.4), "$\operatorname{int}\operatorname{dom}f_2\ne\emptyset$", is strengthened to $\operatorname{int}\operatorname{dom}f_2\cap R(A)\ne\emptyset$. With (2.4) alone, Theorem 2.1's saddle point need not exist and the multipliers of Theorem 3.1 need not be bounded: $V=\mathbb R$, $Y=\mathbb R^2$, $Av=(v,0)$, $f_1=|\cdot|^2/2$, $f_2$ the indicator of the disc of centre $(0,1)$ and radius $1$, $\langle b,v\rangle=v$.
• Proposition 2.1 assumes that $f_2\circ A$ is somewhere finite, which its proof requires.

Ruled out: the solution $v^*$ is a hypothesis of the goal, so the hypotheses must not be contradictory. They are met by $V=Y=\mathbb R$, $A=\mathrm{id}$, $f_1(y)=y^2/2$, $f_2=0$, $b=0$, and a proper $f_2$ excludes the degenerate reading in which every point "solves" $(\mathcal P)$ with value $+\infty$.

A complete development needs: existence of minimizers of coercive convex l.s.c. functions on a Hilbert space; the subdifferential sum and chain rules under a continuity qualification; orthogonal projections onto closed ranges; and elementary facts about summable sequences. The saddle-point theory (Theorems 2.1–2.2) and the scalar lemma (3.23) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal by a different route.

Selected references

• D. Gabay and B. Mercier, A dual algorithm for the solution of non linear variational problems via finite element approximation, IRIA Rapport de Recherche 126, 1975. https://hal.science/hal-04716124v1 ; journal version: Computers & Mathematics with Applications 2 (1976) 17–40, https://doi.org/10.1016/0898-1221(76)90003-1
• R. Glowinski and A. Marrocco, Sur l'approximation, par éléments finis d'ordre un, et la résolution, par pénalisation-dualité, d'une classe de problèmes de Dirichlet non linéaires, RAIRO Analyse Numérique 9 (1975) 41–76. https://doi.org/10.1051/m2an/197509R200411
• M. R. Hestenes, Multiplier and gradient methods, J. Optim. Theory Appl. 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• I. Ekeland and R. Temam, Analyse convexe et problèmes variationnels, Dunod, 1974 (the paper's [E]).
• J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Math. Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
• S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3 (2011) 1–122. https://doi.org/10.1561/2200000016

Motivation

Newton's method for a nonlinear system $F(x) = 0$, with $F:\mathbb R^n\to\mathbb R^n$, solves the linear system $F'(x_k)s_k = -F(x_k)$ at every step. For large systems that solve is itself iterative (a Krylov method such as GMRES), and it is stopped early. The resulting inexact Newton methods, introduced by Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19 (1982)), accept any step with $\|F(x_k)+F'(x_k)s_k\|\le\eta_k\|F(x_k)\|$, where the forcing term $\eta_k\in[0,1)$ controls how accurately the linear system is solved. Their theory is local: it applies once the iterates are near a solution with invertible derivative.

Practical solvers (Newton–Krylov codes in large-scale simulation, nonlinear solver libraries such as PETSc's SNES and SUNDIALS' KINSOL) combine such inexact steps with a globalization, most often backtracking along the step. Eisenstat and Walker (SIAM J. Optim. 4 (1994)) gave the global convergence theory for this combination: what can be said about the iterates from an arbitrary starting point, with no assumption that a solution exists or that $F'$ is invertible anywhere.

Timeline. Dembo, Eisenstat and Steihaug (1982) proved local convergence of inexact Newton methods. Dembo and Steihaug (Math. Program. 26 (1983)) studied truncated Newton methods for unconstrained minimization. Brown and Saad (1990) studied globalized Newton–Krylov methods with line searches and model trust regions, under the inner-product norm. Eisenstat and Walker (1994) gave the general framework treated here, for an arbitrary norm. Their 1996 paper (SIAM J. Sci. Comput. 17) proposed the forcing-term choices that are now standard.

Setting

Let $E$ be $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let $F:E\to E$ be continuously differentiable with derivative $F'(x)$. A point $x_*$ is a limit point of $(x_k)$ if every ball $N_\delta(x_*)=\{y:\|y-x_*\|<\delta\}$ contains $x_k$ for infinitely many $k$.

Algorithm GIN (global inexact Newton method). Fix $t\in(0,1)$. At each $k$, find a level $\eta_k\in[0,1)$ and a step $s_k$ with

$$\|F(x_k)+F'(x_k)s_k\|\le\eta_k\|F(x_k)\| \quad (2.1),\qquad \|F(x_k+s_k)\|\le[1-t(1-\eta_k)]\,\|F(x_k)\| \quad (2.2),$$

and set $x_{k+1}=x_k+s_k$. Condition (2.1) says that $s_k$ reduces the norm of the local linear model by the factor $\eta_k$. Condition (2.2) asks that $\|F\|$ itself decrease by a fixed fraction $t$ of that predicted reduction.

Algorithm MR (minimum reduction method). Fix $\eta_{\max}\in[0,1)$ and $0<\theta_{\min}<\theta_{\max}<1$. At step $k$, choose $\bar\eta_k\in[0,\eta_{\max}]$ and a curve $\sigma_k$ with $\|F(x_k)+F'(x_k)\sigma_k(\eta)\|\le\eta\|F(x_k)\|$ for $\bar\eta_k\le\eta\le1$ (5.1). Start at $\eta_k=\bar\eta_k$. While (2.2) fails for $s_k=\sigma_k(\eta_k)$, replace $\eta_k$ by $1-\theta(1-\eta_k)$ for some $\theta\in[\theta_{\min},\theta_{\max}]$. Then set $x_{k+1}=x_k+\sigma_k(\eta_k)$.

Algorithm INB (inexact Newton backtracking). Choose $\bar\eta_k\in[0,\eta_{\max}]$ and an inexact Newton step $\bar s_k$ at level $\bar\eta_k$. While (2.2) fails, shorten the step, $s_k\leftarrow\theta s_k$, and raise the level, $\eta_k\leftarrow1-\theta(1-\eta_k)$. INB is MR with the backtracking curve $\sigma_k(\eta)=\frac{1-\eta}{1-\bar\eta_k}\bar s_k$ (6.1).

An algorithm does not break down if it produces an infinite sequence of iterates, in particular if every while-loop exits.

Formalization targets

Goal: Theorem 6.1 (global convergence of Algorithm INB)

If Algorithm INB does not break down and $x_*$ is a limit point of $(x_k)$ at which $F'(x_*)$ is invertible, then

$$F(x_*)=0,\qquad x_k\to x_*,\qquad s_k=\bar s_k\ \text{and}\ \eta_k=\bar\eta_k\ \text{for all sufficiently large }k.$$

The statement assumes no solution, bounded level set, Lipschitz derivative or particular norm. The last clause says that backtracking eventually stops, so the local rate is governed by the forcing terms $\bar\eta_k$.

Milestones

In attack order:

1. Lemmas 1.1 and 1.2. Continuity of $y\mapsto F'(y)^{-1}$ at an invertible point, and a uniform linearization error $\|F(z)-F(y)-F'(y)(z-y)\|\le\varepsilon\|z-y\|$ near $x$.
2. Theorem 3.3. If $F(x_k)\to0$, the steps satisfy (2.1) with a fixed $\eta$, and $\|F(x_k)\|$ is nonincreasing, then an invertible limit point is a zero and the limit.
3. Theorem 3.4. A GIN run with $\sum_k(1-\eta_k)=\infty$ has $F(x_k)\to0$, plus the conclusion of Theorem 3.3 at invertible limit points.
4. Theorem 3.5. A GIN run converges to a limit point near which $\|s_k\|\le\Gamma(1-\eta_k)\|F(x_k)\|$ (3.2).
5. Lemma 5.1. The while-loop terminates, with $1-\eta_k\ge\min\{1-\bar\eta_k,\theta_{\min}\delta/(\Gamma\|F(x_k)\|)\}$.
6. MR runs are GIN runs (§5).
7. Theorem 5.2 for MR. Under $\|\sigma_k(\eta)\|\le\Gamma(1-\eta)\|F(x_k)\|$ near a limit point $x_*$ (5.6): $F(x_*)=0$, $x_k\to x_*$, and $\eta_k=\bar\eta_k$ eventually.
8. INB runs are MR runs with the curve (6.1), and $s_k=\sigma_k(\eta_k)$ throughout the loop (§6).

Further items, which are not milestones: Corollary 6.2 (exact Newton with backtracking takes full Newton steps eventually), Theorem 5.2 for Algorithm TL, Lemma 3.1 (existence of acceptable GIN steps), and Proposition 2.1 (the Goldstein–Armijo alpha condition implies (2.2) in the Euclidean norm).

Significance

The result. Theorem 6.1 is the global convergence guarantee for the inexact Newton backtracking method that Newton–Krylov solvers implement. It separates three outcomes: the iterates diverge, they accumulate only at points where $F'$ is singular, or they converge to a solution with invertible derivative and eventually take the unmodified inexact Newton steps. In the third case the local theory of Dembo, Eisenstat and Steihaug applies from some iteration on, so the forcing terms alone set the convergence rate. Theorem 5.2 is the template: §§6–8 of the paper derive the convergence of backtracking, equality-curve and dogleg-type methods from it by verifying (5.6).

Formalizing it. The results are proved on paper and none of them has a machine-checked proof that we know of. The mission produces a library of algorithm-run predicates with explicit while-loops for inexact Newton methods. It also checks the paper's reduction chain (INB is a run of MR, MR is a run of GIN) and the global convergence theorems in an arbitrary finite-dimensional norm.

Difficulty

The obvious argument fails at both ends. Sufficient decrease (2.2) alone gives monotonicity of $\|F(x_k)\|$, but not convergence of the iterates. On the page, $F(x)=x^2-1$ admits sequences satisfying (2.2) with both $\pm1$ as limit points. Convergence of $\|F(x_k)\|$ to $0$ needs $\sum(1-\eta_k)=\infty$, and nothing in the algorithm states this. In Theorem 5.2 it has to be derived from the exit level of the while-loop, which depends on a neighbourhood of $x_*$ where the linearization error is uniformly controlled. A solver must combine a limit-point argument (only infinitely many iterates are near $x_*$, not all of them) with the loop's worst-case backtracking factor $\theta_{\min}$. The invertibility of $F'(x_*)$ enters only through the bound (5.6) for the backtracking curve, which must be established uniformly in $k$.

Formalization scope

• Space and norm. $E$ is a finite-dimensional real normed space ([NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]). This is exactly "$\mathbb R^n$ with an arbitrary norm". Fin n → ℝ (sup norm) and EuclideanSpace would each fix one norm. Only Proposition 2.1 assumes an inner product space, as the page does.
• Derivative. $F'$ is fderiv ℝ F, with ContDiff ℝ 1 F (the paper's standing assumption). Invertibility is ContinuousLinearMap.IsInvertible, and $F'(x)^{-1}$ is ContinuousLinearMap.inverse.
• Runs. An algorithm that does not break down is a predicate on infinite sequences (IsGINRun, IsMRRun, IsINBRun, plus IsTLRun, IsENBRun). The steps and levels the algorithm says to "find" or "choose" are data constrained only by the stated conditions. A while-loop is recorded by its number of passes $m_k$ and factors $\theta_{k,j}\in[\theta_{\min},\theta_{\max}]$. Every trial before the last fails the loop's test and the last one passes it. Termination is part of the run.
• Limit point is MapClusterPt xstar atTop x. "For all sufficiently large $k$" is ∀ᶠ k in atTop. The paper's "whenever $x_k$ is sufficiently near $x_*$ [and $k$ is sufficiently large]" is ∃ Γ, ∃ δ > 0, [∃ K,] ∀ k [≥ K], x k ∈ ball xstar δ → …. $\Gamma$ precedes $k$ ("independent of $k$"), and the "$k$ large" clause appears only in (3.2), where the page has it.
• Hypotheses as printed. Theorems 3.5 and 5.2 do not assume $F'(x_*)$ invertible. Theorem 5.2 does not assume $\sum(1-\eta_k)=\infty$. Lemma 5.1 is stated for one iteration of the loop shared by MR and TL, for every choice of factors.
• Trivializing readings ruled out. A run predicate without the "rejected" clause would allow needless backtracking, and one without the "accepted" clause would drop (2.2). Both clauses are present. A sorry-free check (F = id on $\mathbb R$) confirms that the INB, GIN and ENB run predicates and the goal's hypotheses are satisfiable, so the goal is not vacuous.
• Infrastructure. Continuity of operator inversion and uniform differentiability on neighbourhoods are in Mathlib. The run predicates and trial-level recursions are reusable for any line-search or backtracking analysis. Each milestone is stated independently; contributions in any order are welcome.

Selected references

• S. C. Eisenstat and H. F. Walker, Globally Convergent Inexact Newton Methods, SIAM J. Optim. 4(2) (1994) 393–422. https://doi.org/10.1137/0804022
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton Methods, SIAM J. Numer. Anal. 19(2) (1982) 400–408. https://doi.org/10.1137/0719025
• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Math. Program. 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
• P. N. Brown and Y. Saad, Hybrid Krylov Methods for Nonlinear Systems of Equations, SIAM J. Sci. Stat. Comput. 11(3) (1990) 450–481. https://doi.org/10.1137/0911026
• S. C. Eisenstat and H. F. Walker, Choosing the Forcing Terms in an Inexact Newton Method, SIAM J. Sci. Comput. 17(1) (1996) 16–32. https://doi.org/10.1137/0917003
• J. E. Dennis and R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, SIAM Classics in Applied Mathematics 16 (1996). https://doi.org/10.1137/1.9781611971200

Motivation

Iterative methods for a system of linear inequalities $Ax\le b$ stop at a vector $\bar x$ that only almost satisfies the system: the violation $(A\bar x-b)^+$ is small but not zero. A user then needs to know that $\bar x$ is close to an actual solution. Hoffman's 1952 paper (J. Res. Nat. Bur. Standards 49) gives the first quantitative form of this fact: the distance from $\bar x$ to the solution set is at most a fixed multiple of the violation. The paper itself names one application: in Brown's method for solving games, the computed strategy vector approaches the set of optimal strategy vectors.

The result is now known as Hoffman's error bound and the constant as the Hoffman constant. It is a standard tool in convergence analysis, sensitivity analysis of linear programs, and the theory of error bounds.

Timeline.

• 1952: S. Agmon (The relaxation method for linear inequalities, NAML Report 52-27, NBS; later Canad. J. Math. 6, 1954, doi:10.4153/CJM-1954-037-2) proves the two geometric lemmas on which Hoffman's proof rests, and a bound in the Euclidean/max norm setting.
• 1952: A. J. Hoffman proves the bound for arbitrary positive homogeneous size functions $F_n$, $F_m$, and gives explicit constants in the max and sum norms by way of matrix games.
• Later work (Robinson 1973; Güler, Hoffman and Rothblum 1995; Peña, Vera and Zuluaga 2021) extends the bound to perturbed systems, characterises the sharp constant, and studies its computation.

Setting

Let $A=(a_{ij})$ be a real $m\times n$ matrix with rows $A_1,\dots,A_m$ and let $b\in\mathbb R^m$. The system (1) is $A_i\cdot x\le b_i$ for $i=1,\dots,m$, briefly $Ax\le b$; its solution set is $\Omega=\{x : Ax\le b\}$, and the system is consistent if $\Omega\ne\emptyset$. The $i$th half space is $\{x : A_i\cdot x\le b_i\}$.

For a real number $a$, $a^+=a$ if $a\ge0$ and $a^+=0$ otherwise; for a vector, $y^+$ is taken coordinatewise. So $(Ax-b)^+$ records by how much $x$ violates each inequality.

Hoffman measures sizes with a positive homogeneous function $F_k$ on $\mathbb R^k$: a continuous real function with (i) $F_k(x)\ge0$ and $F_k(x)=0$ only for $x=0$, and (ii) $F_k(\alpha x)=\alpha F_k(x)$ for $\alpha\ge0$. Norms are examples, but $F_k$ need not be symmetric, subadditive or convex.

For a set $S$ of rows, $M$ is the $m\times n$ matrix obtained from $A$ by replacing the rows outside $S$ by $0$, and $\bar y$ keeps the coordinates of $y\in\mathbb R^m$ in $S$ and zeroes the others. "Nearest" always refers to Euclidean distance. The set $E$ consists of the points $x$ outside the cone $\{z : Mz\le0\}$ whose nearest point in that cone is the origin; $K'$ is the cone spanned by the rows of $M$ with the origin removed.

Section 3 uses three norms: $|x|$ (largest absolute coordinate), $\|x\|$ (sum of absolute coordinates) and the Euclidean norm. With $g_{ij}=A_i\cdot A_j$, $a_S$ is the largest absolute coordinate of a row in $S$, and $v_S=\min_\lambda\max_{i\in S}\sum_{j\in S}g_{ij}\lambda_j$ over probability vectors $\lambda$ on $S$, the value of the matrix game $(g_{ij})_{i,j\in S}$.

Formalization targets

Goal: Hoffman's theorem (Section 2, p. 263)

If $Ax\le b$ is consistent and $F_n$, $F_m$ are positive homogeneous, there is $c>0$ such that for every $x$ some solution $x_0$ satisfies

$$F_n(x-x_0)\le c\,F_m\bigl((Ax-b)^+\bigr).$$

The constant is existential and fixed before $x$; no value is asserted. This is the weakest statement that carries the content and survives any later improvement of the constant.

Milestones: the proof's lemmas (pp. 263–264)

• Lemma 2: if $y$ is the point of $\Omega$ nearest to $x\notin\Omega$, then $x$ lies outside the intersection $\Omega_S$ of the half spaces active at $y$, and $y$ is also the point of $\Omega_S$ nearest to $x$.
• Lemma 3: for every set $S$ of rows there is $d_S>0$ with $F_m((Mx)^+)\ge d_S F_n(x)$ for all $x\in E$.
• Lemma 1: there is $e>0$ with $F_m(\bar y)\le e\,F_m(y)$ for all $y$ and all $S$.
• Lemma 4: $K'=E$.

Milestones: explicit constants (pp. 264–265)

$$\text{(9)}\quad |x-x_0|\le\frac{a}{v}\,|(Ax-b)^+|\quad\text{if all }A_i\cdot A_j>0,\ v=\min_{i,j}A_i\cdot A_j,\ a=\max_{i,j}|a_{ij}|;$$ $$\text{(10)}\quad |x-x_0|\le\frac{a}{w}\,\|(Ax-b)^+\|\quad\text{if } w=\min_i\Bigl(g_{ii}+\sum_{j:\,g_{ij}<0}g_{ij}\Bigr)>0;$$ $$\text{(8)}\quad |x-x_0|\le c\,|(Ax-b)^+|,\qquad c=\max_{v_S>0}\frac{a_S}{v_S}.$$

Each is stated as in the theorem: for every $x$ there is a solution $x_0$ with the bound.

Significance

The result. The theorem converts a residual estimate into a distance estimate. Any scheme that drives $(Ax-b)^+$ to zero brings its iterates to the solution set at a linear rate in the residual. Linear convergence proofs for projection and first-order methods on polyhedral problems and stability results for LP solution sets build on it. Formulas (8)–(10) show that in the max and sum norms the constant can be read off the rows of $A$ through a matrix game.

Formalizing it. The theorem has been proved since 1952, and later papers give several alternative proofs. The mission formalizes Hoffman's own proof route, Lemmas 1–4, in Lean and Mathlib, and the explicit constants (8)–(10). Mathlib has Farkas-type results and projections onto closed convex sets in inner product spaces, but no error bound for linear inequality systems, and the Prove2Me library has no statement of Hoffman's theorem.

Difficulty

For a single $x$, a bound is trivial: take $x_0$ the nearest solution and choose $c$ accordingly. The whole content is that one $c$ works for all $x$, including $x$ far from $\Omega$ and $x$ approaching $\Omega$ along every direction. A compactness argument on $\{x : F_n(x)=1\}$ alone fails, because the ratio $F_n(x-x_0)/F_m((Ax-b)^+)$ is not a continuous function of $x$ on a compact set: the nearest solution and the set of active constraints jump as $x$ moves. Lemma 3 needs a positive lower bound on a set $E$ that is not obviously closed away from the origin; its closedness comes from Lemma 4, i.e. from Farkas' lemma. Since $F_n$, $F_m$ are not norms, no argument using the triangle inequality or symmetry is available. For (8), a set $S$ can arise in Lemma 2 with $v_S=0$ (e.g. $x_1\le0$, $-x_1\le0$ in $\mathbb R^2$ with $x=(1,0)$), contrary to an unnumbered remark on p. 265; the bound (8) is still true, but that remark cannot be used.

Formalization scope

• Vectors are Fin k → ℝ, $A$ is Matrix (Fin m) (Fin n) ℝ, the system is A *ᵥ x ≤ b (componentwise), and $y^+$ is posPartVec y = fun i => max (y i) 0.
• $F_n$, $F_m$ are arbitrary functions satisfying IsPosHomogeneous (continuity, nonnegativity, vanishing exactly at $0$, positive homogeneity); they are never specialised to norms in the goal or Lemmas 1, 3.
• "Nearest" is Euclidean and written with the dot product: $y$ is nearest to $x$ in $\Omega$ if $(x-y)\cdot(x-y)\le(x-z)\cdot(x-z)$ for all $z\in\Omega$. (Mathlib's dist on Fin n → ℝ is the sup distance and is not used.) Lemmas 2 and 3 take "a nearest point" as hypothesis; since the Euclidean nearest point of a closed convex set is unique, this is the page's "the nearest point".
• A "subset $S$ of the half spaces" is a Finset (Fin m) of row indices; $M$ keeps all $m$ rows, with zero rows outside $S$.
• In (8)–(10), $|x|$ is ⨆ i, |x i| and $\|x\|$ is ∑ i, |x i|; minima and maxima over finite index sets are ⨅/⨆ in ℝ, equal to the attained min/max on nonempty sets. $v_S$ is defined directly by (7) as a min over the simplex of a max, for nonempty $S$, so no minimax theorem is needed. In (8), $c$ is the maximum over nonempty $S$ with $v_S>0$ and is $0$ when there is none (only when $A=0$). In $w$, the page's summation range "$j=1,\dots,n$" is read as ranging over the $m$ rows, since $g$ is indexed by rows.
• Consistency is a hypothesis of the goal and of (8)–(10).

The quantifier order $\exists c>0,\ \forall x,\ \exists x_0$ is part of the statement: a version with $c$ chosen after $x$ is trivially true and is not this theorem; likewise $e$ precedes $y$ and $S$ in Lemma 1 and $d_S$ precedes $x$ in Lemma 3.

Infrastructure a complete development needs: existence and the variational characterisation of the Euclidean projection onto a polyhedron in Fin n → ℝ; Farkas' lemma in cone form (published as LinearOptimization.farkas_cone_corollary); compactness of level sets of positive homogeneous functions. The projection and polyhedral-cone lemmas are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal, and sharper or equivalent forms of the constants are welcome.

Selected references

• A. J. Hoffman, On Approximate Solutions of Systems of Linear Inequalities, J. Res. Nat. Bur. Standards 49(4) (1952), 263–265. https://doi.org/10.6028/jres.049.027
• S. Agmon, The Relaxation Method for Linear Inequalities, Canad. J. Math. 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
• S. M. Robinson, Bounds for error in the solution set of a perturbed linear program, Linear Algebra Appl. 6 (1973), 69–81. https://doi.org/10.1016/0024-3795(73)90007-4
• O. Güler, A. J. Hoffman, U. G. Rothblum, Approximations to solutions to systems of linear inequalities, SIAM J. Matrix Anal. Appl. 16(2) (1995), 688–696. https://doi.org/10.1137/S0895479892237744
• J. Peña, J. C. Vera, L. F. Zuluaga, New characterizations of Hoffman constants for systems of linear constraints, Math. Program. 187 (2021), 79–109. https://doi.org/10.1007/s10107-020-01473-6

Motivation

The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.

Timeline.

• 1966–1985. Practical exact methods and pseudopolynomial dynamic programs (Joksch 1966; Lawler 1976; Handler and Zang 1980; Aneja, Aggarwal and Nair 1983; Henig 1985).
• 1987. Warburton gives the first fully polynomial approximation scheme (FPAS) for this problem on acyclic graphs, based on rounding and scaling (Warburton, Oper. Res. 35, 1987).
• 1992. Hassin gives two faster FPASs: a rounding-and-scaling scheme driven by an approximate decision test (§3–§4), and a strongly polynomial scheme (§5–§6) (Hassin, Math. Oper. Res. 17, 1992).
• 2001. Lorenz and Raz give a simpler and faster scheme built on the same test-and-search pattern (Lorenz–Raz, Oper. Res. Lett. 28, 2001).

Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.

Setting

A directed graph has vertex set $\{1,\dots,n\}$, $n\ge 2$, and edge set $E$. Following the paper, the vertices are numbered so that every edge $(i,j)\in E$ has $i<j$; in particular the graph is acyclic. Each edge carries a positive integer length $c_{ij}$ and a positive integer transition time $t_{ij}$. A path $p=(v_0,\dots,v_m)$ has length $c(p)=\sum_r c_{v_{r-1}v_r}$ and transition time $t(p)=\sum_r t_{v_{r-1}v_r}$. For a nonnegative integer $T$, a $T$-path is a path from $1$ to $n$ with $t(p)\le T$, and $\mathrm{OPT}$ is the length of a shortest $T$-path.

Fix $0<\varepsilon<1$. For a real $V$, the rounded lengths are

$$\tilde c^V_{ij}=\Big\lfloor \frac{c_{ij}(n-1)}{V\varepsilon}\Big\rfloor .$$

Procedure TEST(V) deletes the edges with $c_{ij}>V$ and answers NO if, for some integer $c<(n-1)/\varepsilon$, some $1$–$n$ path in the remaining graph has transition time at most $T$ and rounded length at most $c$; otherwise it answers YES.

The Rounding Algorithm keeps bounds $(LB,UB)$ on OPT. Starting from initial bounds $(LB_0,UB_0)$, Step 1 repeats while $UB>2LB$: with $V=(LB\cdot UB)^{1/2}$ it sets $LB\leftarrow V$ if TEST(V) = YES and $UB\leftarrow V(1+\varepsilon)$ if TEST(V) = NO. Step 2 outputs a $T$-path that is shortest for the rounded lengths $\tilde c^{LB}_{ij}=\lfloor c_{ij}(n-1)/(\varepsilon LB)\rfloor$. The bounds after $k$ passes are written $(LB_k,UB_k)$.

Formalization targets

Goal: the approximation guarantee of the Rounding Algorithm

If $LB_0>0$ is a lower bound on the length of every $T$-path, $N$ is a stage at which $UB_N\le 2LB_N$, and $p$ is a Step 2 output at $LB_N$, then

$$c(p)\le (1+\varepsilon)\,c(q)\qquad\text{for every }T\text{-path }q,$$

that is, $c(p)\le(1+\varepsilon)\,\mathrm{OPT}$. The initial upper bound $UB_0$ is arbitrary.

Milestones (§3–§4)

1. Rounding error (§3, p. 38): with $\delta=V\varepsilon/(n-1)$, $0\le c_{ij}-\delta\tilde c^V_{ij}\le\delta$ for every edge, and $0\le c(p)-\delta\tilde c^V(p)\le V\varepsilon$ for every path.
2. TEST(V) = NO (§3, p. 38): some $T$-path has length $<V(1+\varepsilon)$, so $\mathrm{OPT}<V(1+\varepsilon)$.
3. TEST(V) = YES (§3, p. 38): every $T$-path has length $\ge V$, so $\mathrm{OPT}\ge V$.
4. Bound update (§4, p. 39): along the run, $LB_k>0$ and $LB_k$ is a lower bound on every $T$-path; if some $T$-path has length at most $UB_0$, some $T$-path has length at most $UB_k$.
5. Scaled-optimum error (§4, p. 39): a Step 2 output $p$ at any $LB>0$ satisfies $c(p)\le c(q)+\varepsilon LB$ for every $T$-path $q$.

Companion statements

• Termination when $(1+\varepsilon)^2<2$: some stage $N$ has $UB_N\le 2LB_N$; and an explicit instance with $\varepsilon=9/10$ on which Step 1 never stops.
• Initial bounds (Step 0, p. 39): every $1$–$n$ path has length between $1$ and the sum of the $n-1$ longest edge-lengths.
• Algorithms A and B (§2, pp. 37–38): their recursions compute $f_j(t)$ and $g_j(c)$, with $\mathrm{OPT}=f_n(T)=\min\{c\mid g_n(c)\le T\}$.

Significance

The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a $(1+\varepsilon)$-approximate $T$-path is computed in time polynomial in the input size and $1/\varepsilon$. The two ingredients, an approximate decision test that answers "OPT $\ge V$" or "OPT $<V(1+\varepsilon)$", and a geometric search on the ratio $UB/LB$, are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.

The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when $\varepsilon>\sqrt2-1$, and proves termination under $(1+\varepsilon)^2<2$.

Difficulty

The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most $V\varepsilon$ only because a $1$–$n$ path has at most $n-1$ edges, which follows from the numbering $i<j$ and must be derived for list-encoded paths. The YES case must cover $T$-paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that $(LB\cdot UB)^{1/2}$ is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for $LB_0$.

Formalization scope

• Representation. Vertices are natural numbers; an instance is a structure with $n$, a finite edge set of pairs, and length and time functions, with a well-formedness predicate: $n\ge 2$, every edge $(i,j)$ has $1\le i<j\le n$, and lengths and times are positive. The requirement $n\ge2$ is not printed: a $1$–$n$ path and the divisions by $n-1$ presuppose it. Paths are nonempty vertex lists.
• Arithmetic. $n-1$ is taken in the reals; $\lfloor\cdot\rfloor$ is the natural-number floor of a nonnegative real; $(LB\cdot UB)^{1/2}$ is the real square root. Bounds and $\varepsilon$ are reals, $T$ is a natural number.
• OPT. OPT is never a number in the formal statements, because it is $\infty$ when no $T$-path exists. "OPT $\ge V$" is a bound on every $T$-path, "OPT $<V(1+\varepsilon)$" is the existence of a $T$-path, and the goal compares the output with every $T$-path. Algorithms A and B use values in $\mathbb N\cup\{\infty\}$.
• TEST(V) is defined by the answer the procedure reaches, not through Algorithm B's printed recursion, whose initial condition $g_j(0)=\infty$ is wrong for rounded lengths $0$; for $n\ge2$ and $\varepsilon<1$ the answers agree.
• The run is the iterate of one pass of Step 1; a stopped state is a fixed point. Step 2 outputs any $T$-path optimal for the rounded lengths, without pruning edges, as printed.
• Added hypothesis. The termination statement assumes $(1+\varepsilon)^2<2$, which the page does not state; without it the printed loop can run forever, and an explicit instance is included.
• Not a trivialization. The goal assumes nothing about TEST's correctness, the rounding error or the lower-bound invariant along the run, and the termination companion shows that its stopping hypothesis is reachable.
• Out of scope. The second, strongly polynomial scheme of §5–§6 is not included, because as printed its Partitioning Algorithm can report infeasibility on a feasible instance and formalizing it would require a corrected algorithm that is not the author's. All running-time claims, stated as $O(\cdot)$ bounds under an informal operation count, are also excluded, as are the $V'$ variant of the test points and the scheduling application of §7.
• Reusable parts. The list-based path layer with two additive weights, and the correctness of the pseudopolynomial recursions of Algorithms A and B, are independent of the approximation scheme. Contributions of proofs for any milestone or companion are welcome.

Selected references

• R. Hassin, Approximation schemes for the restricted shortest path problem, Mathematics of Operations Research 17(1):36–42, 1992. https://doi.org/10.1287/moor.17.1.36
• A. Warburton, Approximation of Pareto optima in multiple-objective, shortest-path problems, Operations Research 35(1):70–79, 1987. https://doi.org/10.1287/opre.35.1.70
• D. H. Lorenz and D. Raz, A simple efficient approximation scheme for the restricted shortest path problem, Operations Research Letters 28(5):213–219, 2001. https://doi.org/10.1016/S0167-6377(01)00069-4
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Motivation

The proximal point algorithm is a way to find a zero of a set-valued monotone operator by repeatedly solving a regularized version of that operator equation. Its classical regularizer is quadratic, so the distance from one iterate to the next is Euclidean. In convex optimization, that geometry can be poorly matched to the domain: the natural iterates may be constrained to a positive orthant, a simplex, or an open set with a meaningful boundary. Eckstein's 1993 paper studies what happens when a Bregman function supplies the regularization instead. The convergence question matters because the later multiplier methods in the same paper are instances of this general iteration. Eckstein (1993) develops the general result before applying it to convex programs.

The result considered here is Theorem 1 of that paper. It concerns an existing infinite run: it states what such a run does, while Theorems 4 and 5 address conditions under which a run can be generated. This separation keeps the convergence assertion precise. The result is known mathematically; the mission asks for a Lean proof of its stated generality, including its alternative when the operator has no zero.

Setting

Work in a finite-dimensional real inner-product space $H$, representing the paper's $\mathbb R^n$. A monotone operator $T:H\to 2^H$ associates a set $T(x)$ of vectors with each point. It is monotone when $\langle x-y,u-v\rangle\ge0$ for every $u\in T(x)$ and $v\in T(y)$, and maximal monotone when its graph has no proper monotone extension. Its domain is $\operatorname{dom}T=\{x:T(x)\ne\varnothing\}$; a zero is a point $z$ with $0\in T(z)$.

Let $S\subseteq H$ be open and $h$ a real function on $\overline S$. At $y\in S$, define the Bregman distance

$$D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle,\qquad x\in\overline S.$$

It need not be symmetric and is generally not a metric. Definition 1 requires $h$ to be continuously differentiable on $S$, strictly convex and continuous on $\overline S$, and to satisfy boundedness of both kinds of partial $D_h$ sublevel sets. Two sequential conditions connect convergence in $H$ to convergence of Bregman distances, including sequences approaching the boundary of $S$. These six requirements together define a Bregman function with zone $S$.

A Bregman proximal-point run uses positive parameters $c_k$ and a sequence $x^k\in S$ satisfying

$$\frac{\nabla h(x^k)-\nabla h(x^{k+1})}{c_k}\in T(x^{k+1}),\qquad k=0,1,\ldots.$$

This is the inclusion form (4) of the paper's recursion (3). It permits set-valued $T$ and does not assert that a next iterate exists for arbitrary starting data. The model also uses the paper's standing domain condition $\operatorname{dom}T\subseteq\overline S$.

Formalization targets

The main target is Theorem 1. Assume that the positive parameters have a common positive lower bound and that one of the following conditions holds: (C1) $\overline{\operatorname{dom}T}\subseteq S$, or (C2) $T=\partial f$ for a proper lower semicontinuous convex extended-valued function $f$. Then

$$\begin{aligned} T^{-1}(0)\ne\varnothing &\quad\Longrightarrow\quad x^k\longrightarrow z\text{ for some }z\in T^{-1}(0),\\ T^{-1}(0)=\varnothing\text{ and (C1)} &\quad\Longrightarrow\quad \{x^k:k\ge0\}\text{ is unbounded}. \end{aligned}$$

The second line retains the paper's extra (C1) requirement. The standing inclusion $\operatorname{dom}T\subseteq\overline S$ has a different direction and role. The milestone list follows Lemma 1 and the three labelled steps of Theorem 1's convergence proof: the resolvent inequality, boundedness of the run when a zero exists, identification of every limit point as a zero, and convergence of the full run. The no-zero alternative remains in the goal because restating that conjunct as a separate milestone would add no independent target.

Significance

Theorem 1 says that the nonlinear iteration cannot remain bounded without approaching a zero under (C1), and that when a zero exists the whole sequence converges under either (C1) or (C2). This is stronger than saying only that accumulation points solve the operator equation. It supplies a common convergence result for the paper's later proximal minimization and multiplier algorithms, where the operator is often a subdifferential and the geometry comes from a nonquadratic $h$. Eckstein (1993) gives those applications after the general theorem.

A formalization would add a reusable interface for Bregman functions with open zones, including their boundary behavior, and for proximal-point runs of set-valued maximal monotone operators. The published platform definitions of monotone operators and extended-valued convex analysis are reused. The new proof work is the Bregman resolvent estimate and the convergence alternative at Theorem 1's level of generality. No machine-checked proof of this specific theorem is claimed here.

Difficulty

The usual Euclidean proximal-point theorem does not apply directly after changing coordinates by $y=\nabla h(x)$: the transformed operator need not remain monotone, as the paper observes after Theorem 1. A proof must account for the nonsymmetric $D_h$, the possible boundary of $S$, and two distinct ways to identify a limit point as a zero. Under (C1), the point lies where the gradient is continuous; under (C2), the argument uses the subdifferential structure instead. The no-zero case has its own difficulty because boundedness would have to contradict maximal monotonicity without first assuming that a zero exists. The proof cites a closed-graph result for maximal monotone operators and a zero-existence fact for operators with bounded domain; those external facts are groundwork for solvers, not invented milestones.

Formalization scope

Lean uses a finite-dimensional real inner-product space rather than a coordinate-fixed $\mathbb R^n$. The total function $h:H\to\mathbb R$ is constrained only on $\overline S$; its gradient is evaluated only on the open zone $S$. The Bregman distance is used on $\overline S\times S$. Definition 1's condition (vi) explicitly places its first sequence in $\overline S$, the natural domain stated immediately after the definition. The run explicitly keeps every $x^k$ in $S$ and encodes recursion (3) using the equivalent inclusion (4). A positive lower bound on $c_k$ is expressed by one $\varepsilon>0$ with $c_k\ge\varepsilon$ for every $k$.

The operator $T$ is a published set-valued operator object, with its published notions of monotonicity, maximality, domain, and zeros. The proper and convex extended-valued function in (C2) uses the published epigraph and subgradient definitions, with EReal able to express $+\infty$. Subdifferentials are built from those definitions. A limit point means a limit along a strictly increasing subsequence, and unboundedness means that the full set of iterates is not bounded. The proof step on p. 207 prints $T^{-1}(0)\subseteq S$; the formal Step 1 uses the standing condition $T^{-1}(0)\subseteq\overline S$, which is sufficient for the Bregman distance and also covers (C2).

The run relation cannot be satisfied by an arbitrary constant sequence: its inclusion must hold at every step, and a zero-free operator under (C1) triggers the unbounded conclusion. Nor does the theorem replace convergence by existence of one convergent subsequence. Reusable contributions include properties of the Bregman resolvent and maximal-monotone graph limits. Theorem 5's separate existence and minimization claims are outside this mission's core.

Selected references

• Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI: 10.1287/moor.18.1.202.