Operations Research

Motivation

Augmented Lagrangian methods are among the standard ways to solve smooth nonlinear programs. They replace a constrained problem by a sequence of subproblems in which some constraints are moved into the objective through a penalty term and multiplier estimates. The method of Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18(4), 2007) is the theory behind the ALGENCAN solver. It moves only the "upper-level" constraints into the objective, keeps arbitrary "lower-level" constraints in the subproblems, and requires the subproblems to be solved only approximately.

A convergence theory for such a method has to say what the limit points of the iterates are. This mission is about the second half of that theory (Theorem 4.2): a limit point that is feasible is a KKT point of the original problem, provided it satisfies a weak constraint qualification, the constant positive linear dependence condition (CPLD) of Qi and Wei (SIAM J. Optim. 10(4), 2000). Earlier global convergence results for augmented Lagrangian methods, such as Conn, Gould and Toint's, assumed linear independence of the active gradients (LICQ) at all limit points. CPLD is implied by MFCQ and by LICQ, holds automatically for linear constraints, and is required only at feasible points.

Timeline of the relevant notions:

• 1967: Mangasarian and Fromovitz introduce MFCQ.
• 2000: Qi and Wei introduce CPLD for SQP methods.
• 2005: Andreani, Martínez and Schuverdt show that CPLD is a genuine constraint qualification.
• 2007: this paper proves Theorem 4.2 for augmented Lagrangian methods with general lower-level constraints.

Setting

The problem (2.1) is

$$\text{minimize } f(x)\quad\text{subject to}\quad h_1(x)=0,\ g_1(x)\le 0,\ h_2(x)=0,\ g_2(x)\le 0,$$

with $f:\mathbb R^n\to\mathbb R$ and constraint maps $h_1,g_1,h_2,g_2$ into $\mathbb R^{m_1},\mathbb R^{p_1},\mathbb R^{m_2},\mathbb R^{p_2}$, all continuously differentiable. $\Omega_1=\{h_1=0,\ g_1\le 0\}$ and $\Omega_2=\{h_2=0,\ g_2\le 0\}$.

The augmented Lagrangian with respect to $\Omega_1$ (2.2) is

$$L(x,\lambda,\mu,\rho)=f(x)+\frac{\rho}{2}\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}{\rho}\Big)^2+\frac{\rho}{2}\sum_{i=1}^{p_1}\Big(\Big[[g_1(x)]_i+\frac{\mu_i}{\rho}\Big]_+\Big)^2 .$$

Algorithm 3.1 works in outer iterations $k=1,2,\dots$ with a penalty parameter $\rho_k$ and safeguarded multipliers $\bar\lambda_k$, $\bar\mu_k$ that stay in fixed boxes. At iteration $k$ it finds $x_k$ and lower-level multipliers $v_k$, $u_k\ge 0$ that satisfy the KKT conditions of "minimize $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ on $\Omega_2$" up to a tolerance $\varepsilon_k\to 0$. It then computes the first-order estimates $\lambda_{k+1}=\bar\lambda_k+\rho_k h_1(x_k)$ and $\mu_{k+1}=\max\{0,\bar\mu_k+\rho_k g_1(x_k)\}$. Finally it increases $\rho_k$ by a factor $\gamma>1$ unless a feasibility-complementarity measure has decreased by the factor $\tau<1$.

A point $x$ satisfies CPLD if, whenever some gradients of constraints active at $x$ have a nontrivial vanishing linear combination with nonnegative coefficients on the inequalities, those gradients remain linearly dependent at every point of a neighbourhood of $x$.

Formalization targets

Goal: Theorem 4.2

If $x_*\in\Omega_1\cap\Omega_2$ is a limit point of $\{x_k\}$ and satisfies CPLD with respect to all constraints of (2.1), then $x_*$ is a KKT point of (2.1). If moreover $x_*$ satisfies MFCQ and $\{x_k\}_{k\in K}\to x_*$, then

$$\{\|\lambda_{k+1}\|,\ \|\mu_{k+1}\|,\ \|v_k\|,\ \|u_k\|\}_{k\in K}\ \text{is bounded.}\tag{4.8}$$

Milestones

1. (4.9). At every outer iteration, the gradient of the Lagrangian of (2.1) at $x_k$ with multipliers $(\lambda_{k+1},\mu_{k+1},v_k,u_k)$ has norm at most $\varepsilon_k$.
2. (4.10). Along a subsequence converging to $x_*$, the multipliers of inequality constraints that are inactive at $x_*$ eventually vanish.
3. (4.11)–(4.15). For a general $C^1$ program: if $y_k\to x_*$, $x_*$ is feasible and satisfies CPLD, and the residuals $\nabla F(y_k)+\sum a_{k,i}\nabla H_i(y_k)+\sum b_{k,j}\nabla G_j(y_k)$ tend to zero with $b_k\ge 0$ supported on the constraints active at $x_*$, then $x_*$ is a KKT point.
4. (4.8) under MFCQ. In the same setting with MFCQ instead of CPLD, the coefficients $a_k$, $b_k$ are bounded.

Significance

The theorem says that the algorithm has the right limit points: a feasible limit point is stationary under a constraint qualification weaker than MFCQ and LICQ, with no assumption on the penalty parameters. Milestone 3 is a result of independent interest: an "approximate KKT" sequence converges to a KKT point under CPLD. This sequential argument was later developed into the theory of approximate KKT conditions (Andreani, Haeser & Martínez 2011), and it applies to any algorithm that produces approximate KKT points, not only to this one. Milestone 4 gives the classical fact that MFCQ bounds the multipliers of such sequences.

All results are proved in the paper. As far as is known, none has a machine-checked proof. Neither CPLD nor the augmented Lagrangian method of this paper is formalized in Mathlib or on the platform. The companion missions of this series formalize Theorem 4.1 (feasibility of limit points) and Theorem 5.4 (boundedness of the penalty parameters).

Difficulty

The obvious argument divides the approximate KKT relation by the size of the multipliers, passes to the limit and obtains a contradiction with the constraint qualification. Under CPLD this argument fails, because CPLD does not bound the multipliers: they may diverge along the sequence even though the limit is a KKT point, and the limit of the normalized relation need not contradict anything at $x_*$ itself. CPLD speaks about linear dependence on a whole neighbourhood of $x_*$, while the relation holds only at the iterates, so the information has to be transferred from $x_*$ to nearby points. A pointwise version of CPLD (dependence at $x_*$ only) is plain positive linear dependence, and with it the statement is false.

A second difficulty is complementarity (milestone 2). The safeguarded multipliers $\bar\mu_k$ do not vanish on inactive constraints. Whether $\mu_{k+1}$ does depends on whether the penalty parameters are bounded, which needs the update rule of Step 4.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\nabla$ is Mathlib's gradient. The problem is a structure of component functions indexed by Fin m. The standing assumption "continuous first derivatives on a sufficiently large and open domain" is read as ContDiff ℝ 1 on all of $\mathbb R^n$.

A run of Algorithm 3.1 is a predicate on sequences (IsRun), not a computed object:

• $x_0$ is the initial point and the outer iterations are $k\ge 1$;
• every outer iteration succeeds, which is the paper's standing assumption of §4;
• the three tolerances $\varepsilon_{k,1},\varepsilon_{k,2},\varepsilon_{k,3}$ of Step 2 are separate, as on the page;
• $\nabla L$ is the true gradient of the defined function (2.2);
• (3.1) uses the Euclidean norm, and (3.4) and Step 4 use the sup norm. The paper's norm is arbitrary, and only $\varepsilon_k\to 0$ enters.

KKT, CPLD and MFCQ are defined once for an abstract program with finite index types. The constraints of (2.1) enter as the families $h_1\oplus h_2$ and $g_1\oplus g_2$:

• the KKT definition includes feasibility, nonnegative inequality multipliers and complementarity;
• CPLD quantifies over subsets of equality indices and of active inequality indices, and requires linear dependence on a neighbourhood;
• gradient families are indexed by sum types, so repeated gradients count as dependent.

"Limit point" is MapClusterPt. (4.8) is required for every strictly increasing reindexing converging to $x_*$, and it bounds the unsafeguarded estimates $\lambda_{k+1}$, $\mu_{k+1}$; the safeguarded ones are bounded by construction and would make (4.8) trivial.

Trivializing formalizations are ruled out:

• a run is satisfiable (a sorry-free sanity check exhibits one, with a feasible CPLD limit point);
• KKT fails for a nonzero linear objective, so it is not automatic;
• the gradient is never applied to a function that is not differentiable under the hypotheses;
• gradient families are never collapsed into sets;
• the tolerances of Step 2 are not merged into $\varepsilon_k$.

Contributions welcome: proofs of the four milestones and of the goal, and in particular a reusable conic Carathéodory lemma and a library-level "approximate KKT + CPLD ⇒ KKT" theorem (milestone 3), which is useful well beyond this paper.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4):1286–1309, 2007. https://doi.org/10.1137/060654797 (HAL preprint hal-01295437v1 used here: https://hal.science/hal-01295437)
• L. Qi, Z. Wei, On the constant positive linear dependence condition and its application to SQP methods, SIAM J. Optim. 10(4):963–981, 2000. https://doi.org/10.1137/S1052623497326629
• R. Andreani, J. M. Martínez, M. L. Schuverdt, On the relation between constant positive linear dependence condition and quasinormality constraint qualification, J. Optim. Theory Appl. 125(2):473–485, 2005. https://doi.org/10.1007/s10957-004-1861-9
• O. L. Mangasarian, S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, J. Math. Anal. Appl. 17:37–47, 1967. https://doi.org/10.1016/0022-247X(67)90163-1
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60(5):627–641, 2011. https://doi.org/10.1080/02331930903578700
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999 (Carathéodory's theorem for cones, p. 689).

Why the penalty parameter matters

Augmented Lagrangian methods solve a constrained problem by minimizing a sequence of penalized subproblems while updating estimates of the Lagrange multipliers. Each subproblem carries a penalty parameter $\rho_k$. When $\rho_k$ grows without bound the subproblems become ill-conditioned and hard to solve, and the method behaves like a plain external penalty method. Avoiding that growth is one of the main reasons for using multiplier updates at all, so conditions under which $\rho_k$ stays bounded matter both in theory and in practice (Bertsekas 1982; Conn, Gould, Toint 1991).

Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); HAL hal-01295437) propose an augmented Lagrangian method, Algorithm 3.1, in which only some of the constraints are penalized. Their §5 shows that, under classical local hypotheses at the limit point and a subproblem tolerance tied to the current infeasibility, the penalty parameters remain bounded. This mission formalizes that result for equality-constrained problems (Theorem 5.4), together with the general case (Theorem 5.5) as a companion statement.

Setting

Let $f:\mathbb R^n\to\mathbb R$, $h_1:\mathbb R^n\to\mathbb R^{m_1}$, $g_1:\mathbb R^n\to\mathbb R^{p_1}$, $h_2:\mathbb R^n\to\mathbb R^{m_2}$, $g_2:\mathbb R^n\to\mathbb R^{p_2}$ be continuously differentiable. Problem (2.1) is

$$\text{Minimize } f(x)\ \text{ subject to } h_1(x)=0,\ g_1(x)\le0,\ h_2(x)=0,\ g_2(x)\le0 .$$

The upper-level constraints $h_1,g_1$ are penalized by the PHR augmented Lagrangian

$$L(x,\lambda,\mu,\rho)=f(x)+\frac\rho2\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}\rho\Big)^2+\frac\rho2\sum_{i=1}^{p_1}\Big([g_1(x)]_i+\frac{\mu_i}\rho\Big)_+^2,$$

while the lower-level constraints $h_2,g_2$ stay in the subproblems.

Algorithm 3.1 fixes $\tau\in[0,1)$, $\gamma>1$, $\rho_1>0$, a box $[\bar\lambda_{\min},\bar\lambda_{\max}]$, a bound $\bar\mu_{\max}\ge0$ and tolerances $\varepsilon_k\to0$. At outer iteration $k\ge1$ it finds $x_k$ and lower-level multipliers $v_k,u_k$ such that $x_k$ is an $\varepsilon_k$-approximate KKT point of minimizing $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ over the lower-level set, in the sense of (3.1)–(3.4). It then forms the first-order multiplier estimates

$$\lambda_{k+1}=\bar\lambda_k+\rho_k h_1(x_k),\qquad \mu_{k+1}=\max\{0,\bar\mu_k+\rho_k g_1(x_k)\},$$

and safeguarded estimates $\bar\lambda_{k+1},\bar\mu_{k+1}$, which in §5 are the projections of $\lambda_{k+1},\mu_{k+1}$ on their boxes. Finally it updates the penalty parameter: with $[\sigma_k]_i=\max\{[g_1(x_k)]_i,-[\bar\mu_k]_i/\rho_k\}$,

$$\rho_{k+1}=\begin{cases}\rho_k & \text{if } \max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}\le\tau\max\{\|h_1(x_{k-1})\|_\infty,\|\sigma_{k-1}\|_\infty\},\\ \gamma\rho_k & \text{otherwise.}\end{cases}$$

In §5.1 there are no inequality constraints ($p_1=p_2=0$): problem (5.1), with Lagrangian $L_0(x,\lambda,v)=f(x)+\langle h_1(x),\lambda\rangle+\langle h_2(x),v\rangle$. Assumptions 1–6 at the limit $x_*$ of $\{x_k\}$ are: convergence, feasibility, linear independence of all constraint gradients, $C^2$ near $x_*$, the second-order sufficient condition with multipliers $\lambda_*,v_*$, and $\lambda_*$ in the interior of the safeguard box.

Formalization targets

Goal: Theorem 5.4

Under Assumptions 1–6, $\tau>0$, and $\varepsilon_k\le\eta_k\|h_1(x_k)\|_\infty$ for a sequence $\eta_k\to0$,

$$\sup_k\rho_k<\infty .$$

Milestones, in attack order

1. Proposition 5.1: $\lambda_k\to\lambda_*$, $v_k\to v_*$, and $\bar\lambda_k=\lambda_k$ for $k$ large.
2. Lemma 5.2: there is $\bar\rho>0$ such that for all $\pi\in[0,1/\bar\rho]$

$$\begin{pmatrix}\nabla^2_{xx}L_0(x_*,\lambda_*,v_*)&\nabla h_1(x_*)&\nabla h_2(x_*)\\ \nabla h_1(x_*)^T&-\pi I&0\\ \nabla h_2(x_*)^T&0&0\end{pmatrix}\ \text{is nonsingular.}$$

3. Lemma 5.3: if $\rho_k\ge\bar\rho$ eventually, then for $k$ large

$$\|x_k-x_*\|,\ \|\lambda_{k+1}-\lambda_*\|\le M\max\Big\{\tfrac{\|\bar\lambda_k-\lambda_*\|_\infty}{\rho_k},\|\alpha_k\|,\|\beta_k\|\Big\},$$

with $\alpha_k=\nabla L(x_k,\bar\lambda_k,\rho_k)+\nabla h_2(x_k)v_k$ and $\beta_k=h_2(x_k)$. 4. (5.10): if $\rho_k\to\infty$, then $\|h_1(x_k)\|_\infty\le C\|\lambda_k-\lambda_*\|_\infty/\rho_k$ for $k$ large. 5. Contraction: if $\rho_k\to\infty$, then $\|h_1(x_k)\|_\infty\le (C/\rho_k)\|h_1(x_{k-1})\|_\infty$ for $k$ large.

Companion statements

Theorem 5.5, the general problem (2.1) under Assumptions 7–13 (LICQ, $C^2$, a second-order condition on the tangent subspace of all active constraints, multipliers inside the safeguard boxes, strict complementarity for the active upper-level inequalities), with $\varepsilon_k\le\eta_k\max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}$; and two steps of its proof, (5.13) and (5.14).

Significance

Theorem 5.4 tells a user of the method when it does not degenerate: if the safeguard box contains the true multipliers and the subproblems are solved to a precision proportional to the current infeasibility, then the penalty parameter is eventually constant. The Remark after Theorem 5.5 draws the practical conclusion that the box should be large enough to contain the true multipliers. The result underlies the analysis of the ALGENCAN solver built on Algorithm 3.1.

The results are proved on paper. To our knowledge none of them, nor the PHR augmented Lagrangian method itself, has a machine-checked formalization. A formal proof would also pin down two gaps in the printed statements, recorded under Formalization scope: the case $\tau=0$ and the early iterations in Lemma 5.3. The local analysis (a uniformly nonsingular KKT matrix and implicit-function error bounds for multiplier estimates) is reusable for other augmented Lagrangian and SQP methods.

Difficulty

Without the second-order structure there is no reason for $\rho_k$ to stay bounded: the update test compares consecutive infeasibilities, and nothing in the global theory forces them to decrease geometrically. The local argument has to show that $\|h_1(x_k)\|_\infty$ contracts by a factor of order $1/\rho_k$, which requires error bounds for both $x_k$ and $\lambda_{k+1}$ that hold uniformly as $1/\rho_k$ varies in an interval containing $0$. The uniformity in the perturbation parameter $\pi=1/\rho_k$, around the singular-looking limit $\pi=0$, is the central difficulty. Applying the implicit function theorem at each fixed $\rho$ does not give it.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Constraint maps are families of real functions indexed by Fin m, and problem (5.1) is (2.1) with $p_1=p_2=0$. The norm in (3.1), on $x$ and on $\alpha_k$ is Euclidean. Every $\|\cdot\|_\infty$, and the norms in (3.4), on $\lambda$ and on $\beta_k$, are the sup norm. The paper's norm is arbitrary and the constants absorb the change. A run of Algorithm 3.1 is a predicate on sequences: x 0 is $x_0$, the outer iterations are $k\ge1$, and the three tolerances of Step 2 are kept separate. The gradient in (3.1) is the true gradient of the defined augmented Lagrangian. "Continuous first derivatives" is $C^1$ on $\mathbb R^n$; "continuous second derivatives near $x_*$" is ContDiffAt ℝ 2. Hessians are derivatives of gradients. Every statement that uses a Hessian assumes $C^2$ at $x_*$, so it cannot be a junk value. Assumption 5 is pinned to Fletcher's equality-constrained second-order sufficient condition. Linear independence is that of a family indexed by a sum type, so equal gradients count as dependent.

Added hypotheses, each stated in the item's Formalization Note:

• $\tau>0$ in Theorems 5.4 and 5.5. With $\tau=0$ the theorem is false.
• Lemma 5.3 holds for $k\ge k_1$ instead of every $k$. It is false at early iterations.
• In Proposition 5.1, $\lambda_*,v_*$ are Lagrange multipliers at $x_*$.
• In Theorem 5.5, the multipliers are KKT multipliers of (2.1), and strict complementarity holds for the active lower-level inequalities. Without it the theorem fails when $\tau\gamma<1$.

Statements that would trivialize the goal are excluded. These include a run predicate that no sequence satisfies, merging the three tolerances into $\varepsilon_k$, collapsing gradient families into sets, a junk Hessian, and assuming $\rho_k\to\infty$ or $\rho_k\ge\bar\rho$ in the goal. The last two appear only as milestone hypotheses.

A complete development needs the PHR gradient formula, uniform invertibility of a continuous family of matrices on a compact interval, a quantitative inverse function estimate for $C^1$ maps, and the convergence of multiplier estimates under LICQ. Proofs of any milestone, and reusable lemmas for these pieces, are welcome.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4), 2007, 1286–1309. https://doi.org/10.1137/060654797 (HAL hal-01295437v1: https://hal.science/hal-01295437)
• R. Fletcher, Practical Methods of Optimization, 2nd ed., Wiley, 1987. https://doi.org/10.1002/9781118723203
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982. https://doi.org/10.1016/C2013-0-10366-2
• A. R. Conn, N. I. M. Gould, Ph. L. Toint, A globally convergent augmented Lagrangian algorithm for optimization with general constraints and simple bounds, SIAM J. Numer. Anal. 28(2), 1991, 545–572. https://doi.org/10.1137/0728030

Motivation

Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.

A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.

Setting

The problem is (2.1):

$$\text{Minimize } f(x)\ \text{ subject to }\ h_1(x)=0,\ g_1(x)\le0,\ h_2(x)=0,\ g_2(x)\le0,$$

with $f:\mathbb R^n\to\mathbb R$, $h_1:\mathbb R^n\to\mathbb R^{m_1}$, $g_1:\mathbb R^n\to\mathbb R^{p_1}$, $h_2:\mathbb R^n\to\mathbb R^{m_2}$, $g_2:\mathbb R^n\to\mathbb R^{p_2}$, all continuously differentiable. Write $\Omega_1=\{x: h_1(x)=0,\ g_1(x)\le0\}$ and $\Omega_2=\{x: h_2(x)=0,\ g_2(x)\le0\}$.

The PHR augmented Lagrangian (2.2) with respect to $\Omega_1$ is, for $\rho>0$, $\lambda\in\mathbb R^{m_1}$, $\mu\in\mathbb R^{p_1}_+$,

$$L(x,\lambda,\mu,\rho)=f(x)+\frac\rho2\sum_{i=1}^{m_1}\Big([h_1(x)]_i+\frac{\lambda_i}\rho\Big)^2+\frac\rho2\sum_{i=1}^{p_1}\Big([g_1(x)]_i+\frac{\mu_i}\rho\Big)_+^2 .$$

Algorithm 3.1 has parameters $\tau\in[0,1)$, $\gamma>1$, $\rho_1>0$, boxes $[\bar\lambda_{\min},\bar\lambda_{\max}]$ and $[0,\bar\mu_{\max}]$, and tolerances $\varepsilon_k\ge0$ with $\varepsilon_k\to0$. At outer iteration $k=1,2,\dots$ it finds $x_k$ and lower-level multipliers $v_k$, $u_k\ge0$ satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing $L(\cdot,\bar\lambda_k,\bar\mu_k,\rho_k)$ over $\Omega_2$ to tolerance $\varepsilon_k$; it chooses new safeguarded multipliers $\bar\lambda_{k+1}$, $\bar\mu_{k+1}$ in the boxes; and it keeps $\rho_{k+1}=\rho_k$ when

$$\max\{\|h_1(x_k)\|_\infty,\|\sigma_k\|_\infty\}\le\tau\max\{\|h_1(x_{k-1})\|_\infty,\|\sigma_{k-1}\|_\infty\},\qquad[\sigma_k]_i=\max\Big\{[g_1(x_k)]_i,-\frac{[\bar\mu_k]_i}{\rho_k}\Big\},$$

and sets $\rho_{k+1}=\gamma\rho_k$ otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.

A point $x$ is a KKT point of a problem with objective $F$, equalities $H_i$ and inequalities $G_j$ if it is feasible and $\nabla F(x)+\sum_i a_i\nabla H_i(x)+\sum_j b_j\nabla G_j(x)=0$ for some $a$ and some $b\ge0$ vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at $x$ if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near $x$. CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.

Formalization targets

Goal: Theorem 4.1

Let $\{x_k\}$ be a run and $x_*$ a limit point of it. If $\{\rho_k\}$ is bounded, then $x_*\in\Omega_1\cap\Omega_2$. Otherwise at least one of the following holds:

1. $x_*$ is a KKT point of

$$\text{Minimize }\frac12\Big[\sum_{i=1}^{m_1}[h_1(x)]_i^2+\sum_{i=1}^{p_1}\max\{0,[g_1(x)]_i\}^2\Big]\ \text{ subject to } x\in\Omega_2; \tag{4.1}$$

2. $x_*$ does not satisfy CPLD with respect to the constraints $h_2,g_2$ defining $\Omega_2$.

Milestones

1. Every limit point lies in $\Omega_2$.
2. If $\{\rho_k\}$ is bounded, $\|h_1(x_k)\|_\infty\to0$ and $\|\sigma_k\|_\infty\to0$.
3. If $\{\rho_k\}$ is bounded, every limit point is feasible (the first half of the goal).
4. (4.2): the residual $\delta_k$ of (3.1), with $\nabla L$ written out from (2.2), satisfies $\|\delta_k\|\le\varepsilon_k$ and $\delta_k\to0$.
5. Carathéodory's theorem for cones with free and nonnegative generators, with a linearly independent support, as used for (4.3).

Significance

Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.

The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.

Difficulty

The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by $\rho_k$ removes the objective and the multiplier estimates, but the lower-level multipliers $v_k,u_k$ divided by $\rho_k$ need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at $x_*$ whose gradients are independent at points arbitrarily close to $x_*$. Taking limits of the original multipliers without this reduction does not work.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as $C^1$ on all of $\mathbb R^n$. The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors $h_1(x_k)$, $\sigma_k$ use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by $\mathbb N$: x 0 is the initial point $x_0$, the outer iterations are $k\ge1$, the three subproblem tolerances $\varepsilon_{k,1},\varepsilon_{k,2},\varepsilon_{k,3}$ are kept separate, and $\nabla L$ is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of $\{\rho_k\}$. KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.

No hypothesis is added to Theorem 4.1 beyond the $C^1$ reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and $\sigma_k$ only at $\rho_k\ge\rho_1>0$; the gradients are taken of $C^1$ functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.

Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.

Selected references

• R. Andreani, E. G. Birgin, J. M. Martínez, M. L. Schuverdt, On augmented Lagrangian methods with general lower-level constraints, SIAM J. Optim. 18(4), 1286–1309, 2007. https://doi.org/10.1137/060654797 (preprint: https://hal.science/hal-01295437)
• L. Qi, Z. Wei, On the constant positive linear dependence condition and its application to SQP methods, SIAM J. Optim. 10(4), 963–981, 2000. https://doi.org/10.1137/S1052623497326629
• R. Andreani, J. M. Martínez, M. L. Schuverdt, On the relation between constant positive linear dependence condition and quasinormality constraint qualification, J. Optim. Theory Appl. 125, 473–483, 2005. https://doi.org/10.1007/s10957-004-1861-9
• D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999 (Carathéodory's theorem for cones, p. 689).

Motivation

Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.

Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data $(c_t, A_t, B_t, b_t)$ random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.

Setting

There are $T\ge 2$ stages. The decision $x_t\in\mathbb R^{n_t}$ satisfies $x_t\ge 0$ and, at the first stage, $A_1x_1=b_1$ with deterministic data $(c_1,A_1,b_1)$. For $t=2,\dots,T$ the data are replaced by a sample $\tilde\xi_t^j=(\tilde c_{tj},\tilde A_{tj},\tilde B_{tj},\tilde b_{tj})$, $j=1,\dots,N_t$, each with probability $1/N_t$, independently across stages, and the stage-$t$ constraint is $\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}$. The SAA cost-to-go functions are defined backwards from $\widetilde{\mathcal Q}_{T+1}\equiv 0$:

$$\widetilde Q_{tj}(x_{t-1})=\inf_{x_t\ge0}\big\{\tilde c_{tj}^\top x_t+\widetilde{\mathcal Q}_{t+1}(x_t):\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}\big\},\qquad \widetilde{\mathcal Q}_t=\frac1{N_t}\sum_{j=1}^{N_t}\widetilde Q_{tj}.$$

A scenario is a choice $(j_2,\dots,j_T)$; there are $N=\prod_t N_t$ of them, each of probability $1/N$. A policy $\bar x_t=\bar x_t(\tilde\xi_{[t]})$ depends only on the outcomes up to stage $t$; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost $\frac1N\sum_{\text{scenarios}}\sum_t\tilde c_t^\top\bar x_t$ is minimal.

SDDP keeps, for each stage, a finite set of cuts $\alpha+\beta^\top x$ whose maximum $\mathfrak Q_{t+1}$ lies below $\widetilde{\mathcal Q}_{t+1}$. An iteration has a forward step: $M$ scenarios are sampled, and along each of them the decisions $\bar x_t$ solve the stage problems with $\mathfrak Q_{t+1}$ in place of $\widetilde{\mathcal Q}_{t+1}$, (3.13)–(3.14). It also has a backward step: from $t=T-1$ down to $1$, at each trial point $\bar x_t$ the stage-$(t+1)$ problems with the current cuts are solved for all $N_{t+1}$ outcomes, and the cut (3.17) $\ell(x)=\underline{\widetilde{\mathcal Q}}_{t+1}(\bar x_t)+\tilde g^\top(x-\bar x_t)$ is added, where $\tilde g$ averages $-\tilde B^\top\pi$ over basic optimal (extreme-point) dual solutions $\pi$.

Formalization targets

Goal: Proposition 3.1

Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then

$$P\Big(\exists K\ \forall k\ge K:\ \text{the forward policy defined by }\mathfrak Q^k_2,\dots,\mathfrak Q^k_{T}\text{ is optimal for the SAA problem}\Big)=1 .$$

The goal fixes no iteration count, no rate and no number of forward scenarios $M\ge1$.

Milestones, in attack order

1. Attainment: an LP of the form (3.13)/(3.14) with finite optimal value has an optimal solution.
2. Cut validity: every cut lies below $\widetilde{\mathcal Q}_{t+1}$ on reachable decisions, and $\underline{\widetilde Q}_{tj}\le\widetilde Q_{tj}$.
3. Lower bound: the optimal value $\underline\vartheta_k$ of (3.13) is at most the SAA optimal value.
4. Finitely many cutting planes (3.17) for a fixed next-stage cut set, uniformly in the trial point.
5. Finitely many realizations of the $\mathfrak Q_t$ and of first-stage solutions; along each run the cut sets are eventually constant.
6. A policy is optimal for the SAA problem if and only if it satisfies the dynamic programming conditions (3.18) on every scenario.
7. With probability one every SAA scenario is drawn at infinitely many iterations.

Significance

The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound $\underline\vartheta_k$ eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.

The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.

Difficulty

Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from $T$ down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases $\mathfrak Q$", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.

Formalization scope

The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered $1,\dots,T$; the data of stage $t+1$ are stored under index $t$ (the coupling matrix is indexed by the decision it multiplies); V t is $\widetilde{\mathcal Q}_{t+1}$, with V t ≡ 0 for $t\ge T$. Cost-to-go values are real infima, used only on reachable decisions. The explicit readings are:

• cost-to-go functions finite valued on reachable decisions (the paper: everywhere; weaker);
• initial cut sets: a parameter, nonempty and valid on reachable decisions, with $\{(0,0)\}$ at stage $T$;
• forward solutions from a deterministic oracle that reads the cut set and returns an optimal solution whenever one exists; the goal holds for every such oracle;
• basic optimal duals: extreme points of the dual feasible region, chosen arbitrarily; the goal holds for every run;
• (A1) as a hypothesis on the run; $M\ge1$ forward scenarios per iteration, i.i.d. uniform (independence via iIndepFun);
• forward step before backward step within an iteration, with cuts at that iteration's trial points.

Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of $c,A,B,b$ depend on the outcome. If some $\tilde A_{tj}$ lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.

Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality, LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on LPs with cut epigraphs, are welcome.

Selected references

• A. Shapiro, Analysis of Stochastic Dual Dynamic Programming Method, Optimization Online preprint 2009/12/2509; European Journal of Operational Research 209(1):63–72, 2011. https://optimization-online.org/2009/12/2509/ · https://doi.org/10.1016/j.ejor.2010.08.007
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52:359–375, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4):450–455, 2008. https://doi.org/10.1016/j.orl.2008.01.013
• J. E. Kelley, The cutting-plane method for solving convex programs, J. SIAM 8(4):703–712, 1960. https://doi.org/10.1137/0108053
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

Motivation

In shop scheduling, jobs consist of chains of operations, each to be processed on a prescribed machine, and the goal is to minimize the makespan, the time at which the last operation finishes. Almost every approximation algorithm for job shops, acyclic job shops and flow shops is analysed against one quantity: the trivial lower bound $\mathrm{lb}=\max(C,D)$, where the congestion $C$ is the largest total processing time requested on one machine and the dilation $D$ is the largest total processing time of one job. Any schedule has makespan at least $\mathrm{lb}$.

How weak can this bound be? Leighton, Maggs and Rao (1994) showed that for acyclic job shops with unit-length operations the optimum is $O(\mathrm{lb})$. For operations of arbitrary length, Feige and Scheideler (2002) proved an upper bound of $O(\mathrm{lb}\cdot\log\mathrm{lb}\cdot\log\log\mathrm{lb})$ for acyclic job shops, and gave acyclic job shop instances whose optimum is $\Omega(\mathrm{lb}\cdot\log\mathrm{lb}/\log\log\mathrm{lb})$. Flow shops, in which every job visits every machine in one common order, are much more structured, and no flow shop instance with optimum $\omega(\mathrm{lb})$ was known. Feige and Scheideler asked whether flow shops admit a significantly better upper bound. Mastrolilli and Svensson (J. ACM 2011, Theorem 1.1) answered this negatively by constructing flow shops whose optimal makespan is a factor $\Omega(\log\mathrm{lb}/\log\log\mathrm{lb})$ above $\mathrm{lb}$.

Timeline:

• 1994 — Leighton, Maggs, Rao: unit-time acyclic job shops have optimum $O(\mathrm{lb})$ (packet routing).
• 2002 — Feige, Scheideler: upper bound $O(\mathrm{lb}\log\mathrm{lb}\log\log\mathrm{lb})$ for acyclic job shops, a nearly matching lower-bound family for acyclic job shops, and the open question for flow shops.
• 2011 — Mastrolilli, Svensson: flow shops with optimum $\Omega(\mathrm{lb}\log\mathrm{lb}/\log\log\mathrm{lb})$.

Setting

A job shop instance has machines and jobs; job $j$ is a sequence of operations $O_{1j},\dots,O_{\mu_j j}$, operation $O_{ij}$ needs $p_{ij}\ge0$ time units without interruption on machine $m_{ij}$. A feasible schedule assigns a start time $s\ge0$ to every operation so that each operation starts after the previous operation of its job has completed, and no two operations on one machine overlap. A zero-length operation therefore still occupies an instant on its machine: it cannot be performed strictly inside another operation there. The makespan $C_{\max}(s)$ is the largest completion time.

The instance $F(r,d)$, for natural numbers $r,d$:

• Machines. $r^{2d}$ groups $M_1,\dots,M_{r^{2d}}$; group $M_g$ has machines $m_{g,1},\dots,m_{g,d}$, one per frequency. The machines are ordered $m_{1,d},\dots,m_{1,1},m_{2,d},\dots,m_{2,1},\dots$: by group, and inside a group by decreasing frequency.
• Jobs. For each frequency $f=1,\dots,d$ there are $r^{2(d-f)}$ job groups $J^f_g$, each of $r^{2f}$ identical jobs. Such a job runs for $r^{2(d-f)}$ time units on each of the machines $m_{a+1,f},\dots,m_{a+r^{2f},f}$, $a=(g-1)r^{2f}$, and for $0$ time units on every other machine. Every job visits every machine in the common order, so $F(r,d)$ is a flow shop.

Operations of positive length are long-operations, the others short-operations. For a schedule, the $i$-th long-operation of a job $j$ of frequency $f$ is good if the delay $d_j(i)$ from its end to the start of the next long-operation of $j$ is at most $\frac{r^2}{4}r^{2(d-f)}$; the last long-operation of a job is never good. $T_{g,f}$ is the set of first halves $[s,s+p/2)$ of the good long-operations on machine $m_{g,f}$, and $L(T_{g,f})$ the total time they cover.

Formalization targets

Goal: Theorem 1.1, explicit form

For all natural numbers $r\ge8$ and $d$: every job of $F(r,d)$ has length $r^{2d}$, every machine has load $r^{2d}$ (so $\mathrm{lb}=r^{2d}$), and every feasible schedule $s$ satisfies

$$C_{\max}(s)\ \ge\ r^{2d}\cdot\min\Bigl(r,\ \frac d4\Bigr).$$

With $r=d$ this gives the paper's statement, an optimal makespan of $\Omega(\mathrm{lb}\cdot\log\mathrm{lb}/\log\log\mathrm{lb})$.

Milestones

• §2.2.1, p. 20:10: every job length and machine load equals $r^{2d}$.
• Lemma 2.2: if $C_{\max}(s)<r\cdot\mathrm{lb}$, every job has at least a $(1-4/r)$ fraction of good long-operations.
• Lemma 2.3: for $1\le k<\ell\le d$, the intervals of $T_{g,k}$ and $T_{g,\ell}$ are pairwise disjoint.
• Lemma 2.4: if $C_{\max}(s)<r\cdot\mathrm{lb}$, some group $g$ has $\sum_{f=1}^d L(T_{g,f})\ge\frac{\mathrm{lb}}4\cdot d$.

Significance

The theorem shows that the lower bound $\mathrm{lb}$, against which all known flow shop algorithms are analysed, can be off by a factor growing with $\mathrm{lb}$. Any flow shop algorithm with guarantee $o(\log\mathrm{lb}/\log\log\mathrm{lb})$ relative to the optimum must therefore use a stronger lower bound than $\max(C,D)$. The same frequency construction is the gap gadget behind the paper's inapproximability results for generalized flow shops and job shops (Theorems 1.2 and 1.3).

The result has been proved since 2011; as far as is known it has no machine-checked proof. The mission produces a formal model of the instance $F(r,d)$, a formal proof of the explicit bound for every $r\ge8$, $d$, and reusable statements about delays and first-half intervals in the published job shop model JobShopLTAS.Core.Instance.

Difficulty

The bound must hold for every feasible schedule, with no structural restriction such as a permutation or non-delay schedule. The obvious approach, comparing each machine's load with the makespan, only gives $C_{\max}\ge\mathrm{lb}$, since every machine carries exactly $\mathrm{lb}$. The gain comes from interaction between machines of different frequencies in one group: a high-frequency job running in parallel with a low-frequency long-operation is held back by its zero-length operation on the low-frequency machine. Turning this into a quantitative bound requires controlling, for every job at once, how long it waits between consecutive long-operations, and that waiting is only bounded when the makespan is already small. Encoding the index arithmetic of $F(r,d)$ (groups, frequencies, copies, positions of the long-operations) and the zero-length operations faithfully is a substantial part of the work.

Formalization scope

• Model. The published definition JobShopLTAS.Core.Instance: machines Fin m, jobs Fin n, real processing times and start times, IsFeasibleSchedule Finset.univ s (nonnegative starts, chain precedence, disjunctive machine constraint s o + p o ≤ s o' ∨ s o' + p o' ≤ s o) and makespan Finset.univ s. Under that constraint a zero-length operation cannot sit strictly inside another operation on its machine, which the paper's argument needs.
• Encoding. $F(r,d)$ has $r^{2d}d$ machines and $r^{2d}d$ jobs. Machine position $p$ is $m_{g,i}$ with $p=(g-1)d+(d-i)$, so position order is the paper's machine order. Job $q$ is $j^f_{g,a}$ with $q=(f-1)r^{2d}+(g-1)r^{2f}+(a-1)$. Every job has one operation per machine, the $i$-th on position $i$; frequencies, groups and copies are 1-based.
• Good operations. The next long-operation of a job is the next operation of positive length in its chain; a last long-operation is never good. $L(T)$ is the Lebesgue measure of the union of the intervals of $T$.
• Explicit constants replacing asymptotics. The paper's $\Omega(\mathrm{lb}\cdot\log\mathrm{lb}/\log\log\mathrm{lb})$ is replaced by the bound $r^{2d}\min(r,d/4)$ that §2.2.2 proves; the specialization $r=d$ and the asymptotic estimate $d=\Theta(\log\mathrm{lb}/\log\log\mathrm{lb})$ are not formalized. "Sufficiently large $r$" becomes $r\ge8$ (Lemma 2.4 and the goal: $1-4/r\ge1/2$) and $r\ge3$ (Lemma 2.3: $r^2/2-1>r^2/4$); Lemma 2.2 holds for every $r\ge1$. The standing assumption $C_{\max}<r\cdot\mathrm{lb}$ of §2.2.2 is an explicit hypothesis of Lemmas 2.2 and 2.4. "Optimal makespan" is stated as a bound on every feasible schedule.
• Ruled out. The goal quantifies over all feasible schedules of $F(r,d)$ as constructed; assuming the good-fraction or disjointness properties, restricting to permutation schedules, or a model in which zero-length operations occupy no machine time would trivialize or falsify it.
• Not in scope. The job shop warm-up of §2.1 (Lemma 2.1) and the reductions of §3–§4.

Welcome contributions: proofs of the counting facts about the encoding, of the milestones, and general lemmas about feasible schedules in JobShopLTAS.Core.Instance (completion time of a job bounds its delays; disjoint intervals in $[0,C_{\max}]$ have total length at most $C_{\max}$).

Selected references

• M. Mastrolilli, O. Svensson, Hardness of Approximating Flow and Job Shop Scheduling Problems, J. ACM 58(5), Article 20, 2011. https://doi.org/10.1145/2027216.2027218
• U. Feige, C. Scheideler, Improved Bounds for Acyclic Job Shop Scheduling, Combinatorica 22(3), 361–399, 2002. https://doi.org/10.1007/s004930200018
• F. T. Leighton, B. M. Maggs, S. B. Rao, Packet Routing and Job-Shop Scheduling in O(Congestion + Dilation) Steps, Combinatorica 14(2), 167–186, 1994. https://doi.org/10.1007/BF01215349
• P. Schuurman, G. J. Woeginger, Polynomial Time Approximation Algorithms for Machine Scheduling: Ten Open Problems, J. Scheduling 2(5), 203–213, 1999. https://doi.org/10.1002/(SICI)1099-1425(199909/10)2:5<203::AID-JOS26>3.0.CO;2-5

Motivation

Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.

Timeline:

• 1968, 1973. Satia (PhD thesis) and Satia and Lave (Operations Research 21) treat finite-state, finite-action Markov decision processes with uncertain transition probabilities. They state the max–min optimality equation and the optimality of stationary policies, assuming convex uncertainty sets, and do not prove that the solution of the equation is the robust value function.
• 2001. Bagnell, Ng and Schneider analyse robust policies when the decision maker is restricted to stationary policies.
• 2002–2005. Iyengar (this paper) and Nilim and El Ghaoui (Operations Research 53, 2005) give the rectangular theory. Iyengar proves the discounted robust Bellman equation for countable state spaces, against history-dependent randomized policies and an adversary that may change the law at every visit.

Setting

A discounted ambiguous Markov decision process has a countable state set $\mathcal S$, for each state $s$ a nonempty set $\mathcal A(s)$ of admissible actions, for each admissible pair $(s,a)$ a nonempty set $\mathcal P(s,a)$ of probability measures on $\mathcal S$ (the ambiguity set), a bounded reward $r(s,a,s')$ and a discount factor $\lambda\in(0,1)$. Decisions are made at epochs $t=0,1,2,\dots$.

A policy $\pi=(d_0,d_1,\dots)$ maps each history $h_t=(s_0,a_0,\dots,s_t)$ to a probability measure on $\mathcal A(s_t)$. $\Pi$ is the set of all such policies. A deterministic Markov policy plays $d_t(s_t)$ for maps $d_t:\mathcal S\to\mathcal A$ with $d_t(s)\in\mathcal A(s)$. A stationary policy uses one such rule $d$ at every epoch.

Under Rectangularity, the adversary picks a law $p\in\mathcal P(s_t,a_t)$ separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is $\mathcal T^\pi$. In the static model the adversary fixes one $\bar p_{sa}\in\mathcal P(s,a)$ per pair. The robust value of a policy and the robust value function are

$$V^\pi_\lambda(s)=\inf_{\mathbf P\in\mathcal T^\pi}\mathbf E^{\mathbf P}\Big[\sum_{t=0}^\infty\lambda^t r(s_t,d_t(h_t),s_{t+1})\Big],\qquad V^*_\lambda(s)=\sup_{\pi\in\Pi}V^\pi_\lambda(s).$$

Let $\mathbf V$ be the bounded functions on $\mathcal S$ with $\|V\|=\sup_s|V(s)|$. For a set $\mathcal D$ of deterministic Markov rules, the robust Bellman operator is

$$\mathcal L_{\mathcal D}V(s)=\sup_{d\in\mathcal D}\ \inf_{p\in\mathcal P(s,d(s))}\mathbf E^p\big[r(s,d(s),s')+\lambda V(s')\big].$$

Formalization targets

Goal: Corollary 2(b)

$$V^*_\lambda(s)=\sup_{a\in\mathcal A(s)}\ \inf_{p\in\mathcal P(s,a)}\mathbf E^p\big[r(s,a,s')+\lambda V^*_\lambda(s')\big],\qquad s\in\mathcal S,$$

$V^*_\lambda$ is the only bounded solution of this equation, and for every $\epsilon>0$ some stationary deterministic policy $\pi^\epsilon$ has $V^{\pi^\epsilon}_\lambda\ge V^*_\lambda-\epsilon$.

Milestones

1. Theorem 5(a). $\mathcal L_{\mathcal D}$ maps $\mathbf V$ to $\mathbf V$ and $\|\mathcal L_{\mathcal D}U-\mathcal L_{\mathcal D}V\|\le\lambda\|U-V\|$.
2. Theorem 5(b). For $\mathcal D=\prod_s\mathcal D(s)$, the equation $\mathcal L_{\mathcal D}V=V$ has a unique bounded solution, equal to the robust value over deterministic Markov policies with rules in $\mathcal D$.
3. Corollary 2(a). The robust value of a stationary policy $(d,d,\dots)$ is the unique bounded solution of $V(s)=\inf_{p\in\mathcal P(s,d(s))}\mathbf E^p[r(s,d(s),s')+\lambda V(s')]$.
4. Theorem 4. $V^*_\lambda(s)=\sup_{\pi\in\Pi_{MD}}V^\pi_\lambda(s)$.
5. Lemma 3. For a stationary policy, the dynamic and static models give the same value.
6. Lemma 2. The value of a stationary policy is the optimal solution of the robust program (31).
7. Lemma 1, first claim. The output of robust value iteration is within $\epsilon/4$ of $V^*_\lambda$.

Significance

Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most $\epsilon$ by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.

The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.

Difficulty

The contraction property is a state-by-state $\epsilon$-argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an $\epsilon$ slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.

Formalization scope

States and actions are countable Lean types; $\mathcal A(s)$ and $\mathcal P(s,a)$ are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and $\mathbf E^p[f]=\sum_x p(x)f(x)$ as a tsum. The rewards satisfy $|r(s,a,s')|\le R$ on admissible actions. This is the reading of the page's "$\sup r=R<\infty$", which its bounds $\pm R/(1-\lambda)$ require. The discount factor satisfies $0<\lambda<1$. Epochs start at $0$, so the first reward is undiscounted.

A policy maps $(n, h_n)$ to a PMF supported on $\mathcal A(s_n)$. The dynamic adversary maps $(n,h_n,a)$ to a law in $\mathcal P(s_n,a)$. The path law is built by PMF.bind, and the discounted reward is $\sum_t\lambda^t\mathbf E[r(s_t,a_t,s_{t+1})]$, which converges absolutely. Values are real infima and suprema over nonempty families bounded by $R/(1-\lambda)$, so no junk value arises. $\mathbf V$ is the predicate "bounded", and $\|\cdot\|$ is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.

$V^*_\lambda$ is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in $V^\pi_\lambda$ is the dynamic one; the static adversary appears only in Lemma 3.

The mission deviates from the page in three places:

• Theorem 5(b) is stated for product sets $\mathcal D=\prod_s\mathcal D(s)$. For an arbitrary $\mathcal D$ the printed statement fails, because its proof pastes $\epsilon$-greedy actions state by state. Both uses in Corollary 2 are products.
• Lemma 3 is stated for randomized Markov rules, which is the page's "any decision rule". The page proves it for deterministic rules.
• Lemma 2 adds $\sum_s\alpha(s)<\infty$ and restricts the program to bounded $V$.

Only the first claim of Lemma 1 is posed. Its second claim, that an $\epsilon/2$-greedy rule is $\epsilon$-optimal, is false as printed.

A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform $\epsilon$-optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.

Selected references

• G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, 2002 (rev. May 4, 2004); published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. A. Bagnell, A. Y. Ng and J. Schneider, Solving uncertain Markov decision problems, Tech. Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-problems/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887