All missions

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

The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.

Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to $O(\log n)$ dimensions, and the projected vectors are obtained from $O(\log n)$ calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.

Setting

Let $G=(V,E,w)$ be a connected, simple, weighted undirected graph with $n=|V|$ vertices, edge set $E$ and edge weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix $B\in\mathbb R^{E\times V}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise. With $W$ the diagonal matrix of weights, the Laplacian is $L=B^{\mathsf T}WB$, a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when $G$ is connected. Its Moore–Penrose pseudoinverse is $L^+=\sum_{\lambda_i\neq 0}\lambda_i^{-1}u_iu_i^{\mathsf T}$, where $u_i$ are orthonormal eigenvectors of $L$ with nonzero eigenvalues $\lambda_i$.

For a vertex $u$ let $\chi_u$ be its indicator vector. The effective resistance between $u$ and $v$ is

$$R_{uv}=(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v),$$

and $R_e=R_{ab}$ for an edge $e$ with endpoints $a,b$. The $L$-norm of $y\in\mathbb R^V$ is $\|y\|_L=\sqrt{y^{\mathsf T}Ly}$. Let $w_{\min}$ and $w_{\max}$ be the smallest and largest edge weights.

A resistance sketch is a $k\times n$ matrix $Z$ (columns indexed by $V$) with

$$(1-\varepsilon)R_{uv}\le\|Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)R_{uv}\quad\text{for all }u,v,$$

where $\|\cdot\|$ is the Euclidean norm. In the paper, $Z=QW^{1/2}BL^+$ for a random $\pm1/\sqrt k$ matrix $Q$ with $k=O(\log n/\varepsilon^2)$, and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write $z_i$ and $\tilde z_i$ for the $i$-th rows of $Z$ and of an approximation $\widetilde Z$, as vectors in $\mathbb R^V$.

Formalization targets

Goal: Lemma 9 (p. 11)

Let $0<\varepsilon<1$. If $Z$ is a resistance sketch, if every row satisfies

$$\|z_i-\tilde z_i\|_L\le\delta\|z_i\|_L,\tag{4}$$

and if

$$\delta\le\frac{\varepsilon}{3}\sqrt{\frac{2(1-\varepsilon)w_{\min}}{(1+\varepsilon)n^3w_{\max}}},\tag{5}$$

then for every pair $u,v$

$$(1-\varepsilon)^2R_{uv}\le\|\widetilde Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)^2R_{uv}.$$

The lemma is stated for arbitrary $k$, $Z$ and $\widetilde Z$: nothing about the random projection or the solver enters beyond (4) and the sketch property.

Milestones

• Trace identity (§3, p. 8): $\sum_{e}w_eR_e=n-1$ for a connected graph.
• Proposition 10 (p. 12): $R_{uv}\ge 2/(nw_{\max})$ for distinct vertices $u\neq v$ of a connected simple graph.

Significance

Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in $\widetilde O(m\log r/\varepsilon^2)$ time, that returns any effective resistance to within a factor $(1\pm\varepsilon)^2$ in $O(\log n/\varepsilon^2)$ time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.

The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity $\sum_e w_eR_e=n-1$ (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative $L$-norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.

Difficulty

The hypothesis (4) controls the error row by row, in the $L$-norm on $\mathbb R^V$, while the conclusion concerns the columns of $\widetilde Z$ applied to $\chi_u-\chi_v$, in the Euclidean norm on $\mathbb R^k$, and it is a relative bound for every pair at once. A relative bound cannot hold unless $R_{uv}$ is bounded below uniformly over all pairs of distinct vertices, which is where the factors $n^3$, $w_{\min}$ and $w_{\max}$ of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make $R_{uv}$ arbitrarily small, and the relation between the $L$-norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between $u$ and $v$.

Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from $(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v)$; no theorem relating the two is available.

Formalization scope

The graph is a structure WGraph V E over finite types $V$ (vertices, $n=$ Fintype.card V) and $E$ (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes $V\neq\emptyset$); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by $E$ and $V$. $L^+$ is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on the Euclidean space $\mathbb R^V$, converted back to a matrix; for symmetric $L$ this is the spectral pseudoinverse of §2.2. $\|Z x\|^2$ is the sum of squares of the coordinates, not Lean's sup norm. $n^3$ is the real number $n^3$.

Choices committed to, relative to the page:

• $w_{\min}$, $w_{\max}$ are any reals with $0<w_{\min}\le w_e\le w_{\max}$ for all edges; the exact extremes are an instance, and looser bounds only make (5) and Proposition 10 weaker.
• $\varepsilon$ is assumed to satisfy $0<\varepsilon<1$; the paper gives no range, and for $\varepsilon\ge1$ the square root in (5) has a non-positive argument.
• The graph is assumed simple in Lemma 9 and Proposition 10. Proposition 10 is false for multigraphs (two parallel unit edges give $R=1/2<1=2/(nw_{\max})$), and the proof of Lemma 9 uses it.
• Proposition 10 is stated for $u\neq v$. As printed it claims all $u,v$, which fails at $u=v$ since $R_{uu}=0$.
• The trace identity requires connectivity only.

A trivializing formalization is ruled out: the goal does not assume the intermediate inequality $|\|Zx\|-\|\widetilde Zx\||\le(\varepsilon/3)\|Zx\|$ of the proof, nor a stronger condition on $\delta$ than (5); its hypotheses are satisfiable (for example $\widetilde Z=Z$ with $Z=W^{1/2}BL^+$ and $\delta=0$), and its conclusion is not vacuous for $n\ge2$.

Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity $L^+LL^+=L^+$ and $LL^+$ as the projection onto $\mathbf 1^\perp$ for a connected Laplacian; the trace identity; Loewner-order monotonicity of $R_{uv}$ in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems, arXiv:cs/0607105. https://arxiv.org/abs/cs/0607105
• D. Achlioptas, Database-friendly random projections: Johnson–Lindenstrauss with binary coins, J. Comput. Syst. Sci. 66(4), 2003. https://doi.org/10.1016/S0022-0000(03)00025-4
• P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057

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