Operations Research

Why a threshold rule matters

In a finite stopping problem, a decision maker observes rewards one at a time and must accept one without seeing the future. A fully informed observer takes the maximum. This comparison is often called a prophet inequality. The abstract bound that an optimal stopping rule can secure at least half the expected maximum does not say how to choose a simple rule. Samuel-Cahn showed that a threshold chosen from a median of the maximum already gives this guarantee, even when the rewards are independent but differently distributed. The rule requires one number fixed before observations begin. Samuel-Cahn, 1984

The paper builds on earlier comparisons between the maximum and the best stopping value, then narrows attention to rules that accept an observation when it crosses a fixed threshold. This mission isolates its first main result, Theorem 1, and the two cases that determine whether the crossing test is strict or weak. The paper's second main result, concerning the sharpness of the constant for identically distributed rewards, belongs to the next mission in this series. Samuel-Cahn, 1984, pp. 1213–1215

Observations and threshold rules

Let $n\ge1$, and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables. Write $X_n^*=\max(X_1,\ldots,X_n)$. For a threshold $c\ge0$, the weak threshold rule $t(c)$ takes the first $X_i$ with $i<n$ and $X_i\ge c$; the strict threshold rule $s(c)$ uses $X_i>c$. If no earlier observation qualifies, either rule takes $X_n$, even when $X_n$ is below the threshold. Hence every rule returns exactly one observed reward.

The paper distinguishes the full stopped reward from its positive threshold reward. In its notation,

$$E^+X_{t(c)}=E[X_{t(c)}\mathbf1_{\{X_{t(c)}\ge c\}}], \qquad E^+X_{s(c)}=E[X_{s(c)}\mathbf1_{\{X_{s(c)}>c\}}].$$

The last forced observation may contribute to $E X_{t(c)}$ or $E X_{s(c)}$ while contributing zero to $E^+X_{t(c)}$ or $E^+X_{s(c)}$. This difference is essential to the theorem's middle bounds. A median $m$ of $X_n^*$ means both $P(X_n^*<m)\le\tfrac12$ and $P(X_n^*>m)\le\tfrac12$. Define the excess sum $\beta=\sum_{i=1}^n E(X_i-m)^+$, where $x^+=\max(x,0)$. The two median inequalities allow an atom at $m$, and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)

Formalization targets

Theorem 1: a median threshold

For every median $m$, the goal retains both of the paper's conditional conclusions:

$$\begin{aligned} \beta\ge m&\Longrightarrow E X_n^*\le2E^+X_{s(m)}\le2E X_{s(m)},\\ \beta\le m&\Longrightarrow E X_n^*\le2E^+X_{t(m)}\le2E X_{t(m)}. \end{aligned}$$

At equality $\beta=m$, both conclusions apply. The attack path follows the expected maximum bound (1.3), the displayed identities and probability bound in (1.4), and the companion weak threshold display. Each milestone points to an actual line of the paper. The NOTE and ASSERTION give a further interval of working thresholds: if $a^*=E(X_n^*-a^*)^+$ and $b^*=\sum_iE(X_i-b^*)^+$, then every $a^*\le c\le b^*$ satisfies the same chain with $t(c)$. Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215

What the result gives

Theorem 1 replaces the unspecified best stopping policy with a specific threshold chosen from the distribution of the maximum. It also shows that the thresholded part of the stopped reward alone meets the factor two bound. That stronger middle statement distinguishes the theorem from an outer comparison $E X_n^*\le2E X_\tau$. For a reward distribution with atoms, the theorem says exactly when to use $>$ and when to use $\ge$. Its companion ASSERTION shows that a median is not the only useful threshold choice. Samuel-Cahn, 1984, p. 1214

The result is proved in the paper; the work here is to express its assumptions, boundary behavior, and all displayed inequalities as Lean statements that solvers can prove. The milestones expose reusable facts about positive parts, forced stopping, and independence of a current observation from the event that the rule has survived earlier ones. No machine checked proof of these drafted statements is claimed. The second mission can use the completed theorem to formalize why the factor two cannot be improved uniformly over threshold rules, even for identically distributed observations.

Where the formal proof is delicate

The event that a rule reaches index $i$ depends on the observations before $i$. Establishing its independence from the excess of $X_i$ requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at $n$ also makes the positive threshold reward smaller than the full stopped reward whenever the last observation misses the threshold. Ignoring that last case would erase one of the theorem's conclusions. Finally, atoms at the median prevent the strict and weak crossing events from being interchanged. Samuel-Cahn, 1984, (1.1)–(1.4)

Formalization scope

Lean indexes the $n$ observations by Fin $n$ with $n>0$. Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop $n$. The rules are the least qualifying index or that final index. The paper's $s(m)>i-1$ and $t(m)>i-1$ therefore become $i\le s(m)$ and $i\le t(m)$. Observations are measurable, nonnegative almost surely, and mutually independent under a probability measure.

Expectations use the extended nonnegative integral of the positive part, taking values in $[0,\infty]$. This keeps infinite expected rewards visible without imposing an integrability assumption absent from Theorem 1. The median has both strict tail inequalities from (1.1). The identities for positive stopped rewards state $m\ge0$ directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds $a^*$ and $b^*$ are parameters satisfying the paper's defining equations, with no extra uniqueness hypothesis in statements that do not use it.

The goal cannot be satisfied by replacing $E^+X_\tau$ with $E X_\tau$, by permitting a rule to return no observation, or by making the median predicate empty. Useful contributions include the measurable threshold rule interface, the pathwise excess decomposition, the factorization under mutual independence, and the remaining extended nonnegative arithmetic. Those pieces can also support other finite prophet inequality developments.

Selected references

• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, The Annals of Probability 12(4), 1213–1216, 1984. DOI: 10.1214/aop/1176993150

Motivation

A two-stage stochastic program with recourse models a decision taken in two steps: a first-stage decision is fixed before a random outcome is observed, and a second-stage (recourse) decision is chosen after the outcome is known, both subject to constraints and both incurring costs. The model is the standard framework for planning under uncertainty in operations research: capacity planning, production and inventory, energy dispatch, finance.

For linear recourse problems, duality was developed in the 1960s and early 1970s by Wets and others, partly under integrability restrictions on the random data. R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality (Pacific J. Math. 62 (1976), doi:10.2140/pjm.1976.62.173), treat the convex case, where every cost and constraint function is convex, by embedding the problem in a family of perturbed problems and applying the perturbational theory of convex duality (Rockafellar, Conjugate Duality and Optimization, SIAM 1974) together with the theory of convex integral functionals. The paper's dual variables are integrable price systems, interpreted as equilibrium prices for perturbations of the constraints; it is the starting point of a series of papers by the same authors on stochastic convex programming (relatively complete recourse, Kuhn–Tucker conditions, singular multipliers).

Setting

Let $(S,\Sigma,\sigma)$ be a probability space. A vector $x_1\in\mathbb R^{n_1}$ is chosen subject to $x_1\in C_1$ and $f_{1i}(x_1)\le 0$ ($i=1,\dots,m_1$), at cost $f_{10}(x_1)$. Then $s\in S$ is observed and $x_2(s)\in\mathbb R^{n_2}$ is chosen subject to $x_2(s)\in C_2$ and $f_{2i}(s,x_1,x_2(s))\le 0$ ($i=1,\dots,m_2$), at cost $f_{20}(s,x_1,x_2(s))$. The aim is to minimize the expected cost

$$f_{10}(x_1)+\int_S f_{20}(s,x_1,x_2(s))\,\sigma(ds).$$

The standing assumptions are: $C_1$, $C_2$ convex, closed and nonempty; $f_{1i}$ and $f_{2i}(s,\cdot,\cdot)$ convex and finite everywhere; $s\mapsto f_{2i}(s,x_1,x_2)$ measurable, summable for $i=0$ and bounded for $i\ge 1$.

Decisions live in $X=\mathbb R^{n_1}\times\mathcal L^\infty_{n_2}$ and perturbations in $U=\mathbb R^{m_1}\times\mathcal L^\infty_{m_2}$. The perturbation functional $F(x,u)$ is the expected cost if $x$ satisfies the constraints with right-hand sides $u_1$ and, almost surely, $u_2(s)$, and $+\infty$ otherwise. The problem $\mathbf P$ minimizes $F(x,0)$.

The space $Y=\mathbb R^{m_1}\times\mathcal L^1_{m_2}$ is paired with $U$ by $\langle u,y\rangle=u_1\cdot y_1+\int_S u_2(s)\cdot y_2(s)\,\sigma(ds)$, and $V=\mathbb R^{n_1}\times\mathcal L^1_{n_2}$ with $X$ in the same way. The Lagrangian is $L(x,y)=\inf_{u\in U}\{\langle u,y\rangle+F(x,u)\}$, the dual $\mathbf D$ maximizes $g(y)=\inf_{x\in X}L(x,y)$ over $y\in Y$, and the perturbation function is $\varphi(u)=\inf_{x\in X}F(x,u)$. Conjugates $\varphi^*$, $\varphi^{**}$ are taken with respect to the pairing of $U$ with $Y$.

Formalization targets

Goal: Theorem 3

If $C_1$ and $C_2$ are bounded, then

$$\min\mathbf P=\sup\mathbf D>-\infty,$$

and in fact $\varphi$ is a proper convex function on $U$, lower semicontinuous for the weak topology $\sigma(U,Y)$, the infimum defining $\varphi(u)$ is attained for every $u\in U$, and $\varphi^{**}=\varphi$. The goal is the theorem exactly as printed, all conclusions included.

Milestones

1. p. 174: for bounded measurable $x_1(\cdot)$, $x_2(\cdot)$, the functions $s\mapsto f_{2i}(s,x_1(s),x_2(s))$ are measurable, summable for $i=0$ and essentially bounded for $i\ge1$.
2. Proposition 3: $F$ is convex, not identically $+\infty$, and lower semicontinuous on $X\times U$ for the norm topology and for the weak topology induced by $V\times Y$.
3. (4.9): with $C_1,C_2$ bounded, $X_0=\{x: x_1\in C_1,\ x_2(s)\in C_2\text{ a.s.}\}$ is weakly compact in $X$, and $X_0'=\{x_2\in\mathcal L^\infty_{n_2}: x_2(s)\in C_2\text{ a.s.}\}$ is compact in $\sigma(\mathcal L^\infty_{n_2},\mathcal L^1_{n_2})$.
4. (4.1): $g(y)=\inf_{u}\{\langle u,y\rangle+\varphi(u)\}=-\varphi^*(-y)$.
5. (4.2): $\varphi^{**}(0)=\sup\mathbf D$.

The mission also poses the explicit form (1.8) of the Lagrangian and Corollary 1 (dual solutions are the negatives of subgradients of $\varphi$ at $0$; saddle-point characterization of primal solutions when $\partial\varphi(0)\ne\emptyset$).

Significance

Theorem 3 gives, for bounded constraint sets, the absence of a duality gap between a convex recourse problem with essentially bounded decisions and its Lagrangian dual over integrable multipliers, together with existence of an optimal decision. Through Corollary 1 it reduces the necessity of the Kuhn–Tucker (saddle-point) optimality conditions to the single question whether $\partial\varphi(0)$ is nonempty, and through the paper's later results it describes the directional derivatives of the optimal value with respect to perturbations of the constraints.

The result has been proved since 1976; it has not been machine-checked. A formal development produces the problem model on $\mathcal L^\infty$ and $\mathcal L^1$ spaces, the weak topologies of the pairings, and conjugate duality for extended-real-valued functions on such paired spaces, none of which is currently available as a ready-made Lean statement on this platform.

Difficulty

The obvious argument fails at two points. First, $\inf\mathbf P=\sup\mathbf D$ is $\varphi(0)=\varphi^{**}(0)$, and the biconjugate equals $\varphi$ only for a lower semicontinuous proper convex function in a topology compatible with the pairing. Lower semicontinuity of $\varphi$ in the norm topology of $U$ is not enough: the pairing is with $\mathcal L^1$, not with the norm dual of $\mathcal L^\infty$, so the relevant topology is the weak topology $\sigma(U,Y)$, and an infimum of lower semicontinuous functions is in general not lower semicontinuous. Second, the lower semicontinuity of $F$ itself, in the weak topology, is a statement about convex integral functionals on $\mathcal L^\infty$ that rests on measurability of the integrands in $s$ jointly with continuity in the decision variables. Boundedness of $C_1$, $C_2$ is what supplies the compactness that is otherwise missing.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ and the products $u_1\cdot y_1$, $u_2(s)\cdot y_2(s)$ are dot products. Constraint indices $i=1,\dots,m$ are Fin m.
• $\mathcal L^\infty_n$ and $\mathcal L^1_n$ are Mathlib's Lp (Fin n → ℝ) ⊤ σ and Lp (Fin n → ℝ) 1 σ, spaces of almost-everywhere classes; all second-stage conditions are stated almost surely. $\sigma$ is a probability measure (IsProbabilityMeasure).
• Values in $\mathbb R\cup\{\pm\infty\}$ are EReal; infima and suprema are lattice operations in EReal, so there are no junk values for empty or unbounded sets. Every sum has a real first summand, so no $\infty-\infty$ convention enters.
• The expected cost is a real Bochner integral; its integrand is summable for $x_2\in\mathcal L^\infty$ (milestone 1), so it is the true expected cost. No extended-real-valued function is ever integrated.
• A weak topology "induced by the pairing" is the coarsest topology making every functional of the pairing continuous; the product weak topology on $X\times U$ is the product of the two. These are passed explicitly. Replacing them by the norm topologies would make the lower semicontinuity statements strictly weaker and the compactness statement false; such a formalization does not count.
• An extended-real function is convex when its epigraph is convex, and proper when it never takes $-\infty$ and is somewhere finite.
• Boundedness of $C_1$, $C_2$ is assumed exactly where the paper assumes it: Theorem 3, (4.9) and Corollary 1.

A complete development needs the identification of $\mathcal L^\infty$ with the dual of $\mathcal L^1$ on a probability space (for weak-* compactness), lower semicontinuity of convex integral functionals, and conjugate duality on paired locally convex spaces. These are reusable well beyond this mission. Proofs of milestones, and of auxiliary lemmas of this kind as separate theorems, are welcome. The mission Stochastic Convex Programming: Basic Duality 2 formalizes the paper's other main result, on the first-stage problem and attainment of the recourse.

Selected references

• R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality, Pacific Journal of Mathematics 62(1) (1976) 173–195. https://doi.org/10.2140/pjm.1976.62.173
• R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• R. T. Rockafellar, Integrals which are convex functionals, Pacific Journal of Mathematics 24(3) (1968) 525–539. https://doi.org/10.2140/pjm.1968.24.525
• R. T. Rockafellar, Integrals which are convex functionals, II, Pacific Journal of Mathematics 39(2) (1971) 439–469. https://doi.org/10.2140/pjm.1971.39.439
• R. J.-B. Wets, Stochastic programs with fixed recourse: the equivalent deterministic program, SIAM Review 16(3) (1974) 309–339. https://doi.org/10.1137/1016053

Motivation

A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.

The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.

Setting

Let $r,s$ be positive integers and give $\mathbb R^{r+s}$ its Euclidean norm. Write $w=(w_1,w_2)$, with $w_1\in\mathbb R^r$ and $w_2\in\mathbb R^s$. Let $K\subseteq\mathbb R^s$ be nonempty, closed, and convex, and put $D=\mathbb R^r\times K$. For $w\in D$, the normal cone is

$$N_D(w)=\{v\in\mathbb R^{r+s}:\langle v,c-w\rangle\leq0\text{ for every }c\in D\}.$$

For $w\notin D$, $N_D(w)$ is empty. Thus the inclusion $y\in Aw+N_D(w)$ itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.

Partition the real square matrix $A$ into blocks $A_{11}$, $A_{12}$, $A_{21}$, and $A_{22}$, where $A_{11}$ is $r\times r$. When $A_{11}$ is nonsingular, its Schur complement in $A$ is

$$A/A_{11}=A_{22}-A_{21}A_{11}^{-1}A_{12}.$$

A real matrix $M$ is positive definite in the theorem's sense when $v^\top Mv>0$ for every nonzero $v$. Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write $\mathbb R^s_+$ for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.

Formalization targets

General closed convex set

For $T_K(w)=Aw+N_{\mathbb R^r\times K}(w)$, the first target is the sufficient condition

$$\det A_{11}\ne0\quad\text{and}\quad v^\top(A/A_{11})v>0\;(v\ne0) \quad\Longrightarrow\quad T_K^{-1}:\mathbb R^{r+s}\to\mathbb R^{r+s}\text{ is Lipschitz}.$$

Here “is Lipschitz” includes that exactly one inverse value exists at every $y$. The assertion holds for every nonempty closed convex $K$; it is not restricted to polyhedral sets.

Nonnegative orthant

When $K=\mathbb R^s_+$, the second target is an equivalence:

$$T_{\mathbb R^s_+}^{-1}\text{ is everywhere defined, single-valued and Lipschitz} \quad\Longleftrightarrow\quad \det A_{11}\ne0\text{ and }A/A_{11}\text{ is a P-matrix}.$$

The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.

Significance

The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.

A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.

Difficulty

Nonsingularity of the full matrix $A$ alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as $w_2$ reaches different faces of $K$. A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of $\mathbb R^{r+s}$. For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.

Formalization scope

Lean represents $\mathbb R^{r+s}$ as a Euclidean space indexed by the disjoint union of $\mathrm{Fin}(r)$ and $\mathrm{Fin}(s)$. This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular $A_{11}$ in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains $r,s>0$ as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.

The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex $K$, matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.

Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.

Selected references

• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 43–62, 1980. DOI 10.1287/moor.5.1.43.

Motivation

Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point $x$ has to satisfy $0 \in f(x) + \partial\psi_C(x)$. In applications the data $f$ depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation $f(p, x) = 0$ the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.

S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.

This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.

Setting

Let $X$ be a real normed linear space and $X'$ its topological dual, the continuous linear functionals on $X$. Let $C \subseteq X$ be closed and convex. The normal-cone operator of $C$ is

$$\partial\psi_C(x) = \begin{cases} \{y \in X' : y(c - x) \le 0 \text{ for all } c \in C\}, & x \in C, \\ \emptyset, & x \notin C. \end{cases}$$

A generalized equation is the inclusion $0 \in f(x) + \partial\psi_C(x)$, for a function $f$ from an open set $\Omega \subseteq X$ to $X'$. For $C = X$ it is the equation $f(x) = 0$. For $C$ the nonnegative orthant of $\mathbb R^n$ it is the nonlinear complementarity problem. For a general closed convex $C$ it is the variational inequality over $C$.

Let $x_0 \in \Omega$ solve the generalized equation, and let $f$ be Fréchet differentiable at $x_0$. Linearising $f$ gives the multifunction

$$T x = f(x_0) + f'(x_0)(x - x_0) + \partial\psi_C(x).$$

The generalized equation is strongly regular at $x_0$ with associated Lipschitz constant $\lambda$ if there are neighbourhoods $U$ of $0$ in $X'$ and $V$ of $x_0$ with the following property: for every $y \in U$ the inclusion $y \in Tx$ has exactly one solution $s(y)$ in $V$, and $\|s(y_1) - s(y_2)\| \le \lambda \|y_1 - y_2\|$ on $U$. The condition depends only on $f(x_0)$, $f'(x_0)$ and $C$.

In the parametric problem the function is $f(p, x)$, with $p$ in a topological space $P$ and base point $p_0$. Its partial derivative in $x$ is $f'(p, x)$.

Formalization targets

Goal: Theorem 2.1 (p. 45)

Assume that $f'$ exists on $P \times \Omega$, that $f$ and $f'$ are continuous at $(p_0, x_0)$, and that $x_0$ solves $0 \in f(p_0, x) + \partial\psi_C(x)$, strongly regularly with constant $\lambda$. Then for every $\varepsilon > 0$ there are neighbourhoods $N_\varepsilon$ of $p_0$ and $W_\varepsilon$ of $x_0$, and a function $x : N_\varepsilon \to W_\varepsilon$, with two properties. First, $x(p)$ is the unique solution in $W_\varepsilon$ of $0 \in f(p, x) + \partial\psi_C(x)$. Second,

$$\|x(p) - x(q)\| \le (\lambda + \varepsilon)\,\|f(p, x(q)) - f(q, x(q))\| \qquad (p, q \in N_\varepsilon).$$

Milestones: the steps of the proof (p. 46)

Write $L$ for the linearisation at $(p_0, x_0)$, $r(p, x) = f(p_0, x_0) + f'(p_0, x_0)(x - x_0) - f(p, x)$ for the residual, and $\Phi_p(x) = V \cap L^{-1}[r(p, x)]$. The milestones are four claims of the proof:

1. On the closed ball $V_\varepsilon$, the fixed points of $\Phi_p$ are exactly the solutions of the perturbed inclusion.
2. $\|\Phi_p(x_1) - \Phi_p(x_2)\| \le \lambda\delta \|x_1 - x_2\|$ on $V_\varepsilon$.
3. $\Phi_p$ maps $V_\varepsilon$ into itself.
4. The contraction principle on $V_\varepsilon$, with the bound $\|x(p) - x\| \le (1 - \lambda\delta)^{-1} \|\Phi_p(x) - x\|$ (2.5).

Companion results

• Corollary 2.2 (pp. 46–47). If $P$ lies in a normed space and $\|f(p, x) - f(q, x)\| \le \nu \|p - q\|$, then $x(\cdot)$ is Lipschitzian with modulus $\nu(\lambda + \varepsilon)$.
• Theorem 2.3 (p. 47). Let $\Phi_p(x_0)$ be the unique local solution of the linear generalized equation $0 \in f(p, x_0) + f'(p_0, x_0)(x - x_0) + \partial\psi_C(x)$. Then $\|x(p) - \Phi_p(x_0)\| \le \alpha_\varepsilon(p)\|p - p_0\|$, with $\alpha_\varepsilon(p) \to 0$.
• Theorem 2.4 (p. 48). This is a perturbation lemma for linear generalized equations $0 \in Ax + a + \partial\psi_C(x)$. Near $(A_0, a_0)$ the localised inverse stays single-valued, and it is Lipschitzian with modulus $\lambda(1 - \lambda\|A - A_0\|)^{-1}$.
• The case $C = X$ (remark on p. 45). There strong regularity is equivalent to $f'(x_0)$ having a continuous linear inverse.
• Strong regularity is the weakest possible condition (remark on p. 47). For the canonical perturbation $f(p,x) = f(x_0) + f'(x_0)(x - x_0) - p$, $p \in X'$, locally unique solvability with a Lipschitzian solution map $x(\cdot)$ near $p_0 = 0$ is exactly strong regularity at $x_0$.

Significance

Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at $x_0$, the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.

The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for $C^1$ maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of $X$.

Difficulty

The obvious approach is to apply the classical implicit-function theorem. It fails because $x \mapsto f(x) + \partial\psi_C(x)$ is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood $V$ and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: $\delta$ from $\varepsilon$, then $U$ and $V$, then the ball radius $\rho$, then the parameter neighbourhood. The estimate (2.4) has to come out with the constant $\lambda + \varepsilon$ and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of $X$, for example through the completeness of $X'$.

Formalization scope

• $X'$ is StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off $C$, and an inclusion $0 \in f(x) + \partial\psi_C(x)$ is written $-f(x) \in \partial\psi_C(x)$.
• Strong regularity is a predicate on $(C, f(x_0), f'(x_0), x_0, \lambda)$ with real $\lambda$. It requires existence, uniqueness in $V$ and the Lipschitz bound.
• $f$ is a total function $P \times X \to X'$ whose values off $P \times \Omega$ carry no hypothesis. The conclusion therefore asserts $W_\varepsilon \subseteq \Omega$.
• Differentiability is HasFDerivAt at every point of $\Omega$, for every $p$. Continuity of $f'$ at $(p_0, x_0)$ is joint and in operator norm.
• Uniqueness is uniqueness within $W_\varepsilon$, never global. Global uniqueness is false in general. Dropping uniqueness, or quantifying $\varepsilon$ after the neighbourhoods, would trivialize the goal, and the statements are written to exclude both.
• Theorem 2.1, Corollary 2.2 and Theorem 2.3 do not assume completeness, as printed. Theorem 2.4 assumes a Banach space, as printed.
• The contraction-principle milestone assumes completeness, under which the principle as invoked holds.
• Corollary 2.2 asks for its Lipschitz hypothesis on $N_\varepsilon \times V_\varepsilon$, sets that Theorem 2.1 produces. It is therefore stated on fixed neighbourhoods given in advance.
• Theorem 2.4 also asserts $\lambda\|A - A_0\| < 1$, which its proof secures.

A complete development needs the following:

• the mean-value inequality for Fréchet-differentiable maps on convex sets;
• the contraction principle on a closed ball;
• a fixed-point argument that obtains the fixed point through the complete space $X'$.

The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1):43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3

Motivation

Routing several commodities through one capacitated network at the same time is a basic problem of network optimization, with applications to communication networks, VLSI layout and divide-and-conquer graph algorithms. Its optimum is the value of a linear program, but the natural certificates of an upper bound are combinatorial: every cut of the network limits how much can be routed across it. For a single commodity the max-flow min-cut theorem says that the best cut certificate is exact. With many commodities it is not, and the size of the gap between the best flow and the best cut is the question of this mission.

• 1988–1999, Leighton and Rao proved that for uniform demands (one unit between every pair of vertices) the gap is $O(\log n)$ on an $n$-vertex network, and that the bound is attained on expanders (Leighton–Rao, JACM 1999; FOCS 1988).
• 1990–1995, Klein, Rao, Agrawal and Ravi extended a polylogarithmic bound to arbitrary demands, $O(\log C \log D)$ in the total capacity $C$ and total demand $D$ (Combinatorica 15, 1995); Plotkin and Tardos improved it to $O(\log^2 k)$ in the number of commodities $k$ (Combinatorica 15, 1995).
• 1995, Linial, London and Rabinovich (Combinatorica 15, 1995), and independently Aumann and Rabani (SIAM J. Comput. 1998), showed that the gap is bounded by the least distortion of embedding a metric derived from the network into $\ell_1$, and obtained the bound $O(\log k)$ from Bourgain's embedding theorem. This mission formalizes that theorem, Theorem 4.1 of the Linial–London–Rabinovich paper.

Setting

A multicommodity flow network has a finite vertex set $V$, capacities $C_{i,j} = C_{j,i} \ge 0$ (zero for non-edges and on the diagonal), and $k$ commodities: commodity $\mu$ has a source $s_\mu$, a sink $t_\mu$ and a demand $D_\mu \ge 0$.

A feasible concurrent flow of value $\lambda$ sends, for every $\mu$, $\lambda D_\mu$ units of commodity $\mu$ from $s_\mu$ to $t_\mu$: arc flows $f_\mu(i,j) \ge 0$ satisfy conservation of matter, with net outflow $\lambda D_\mu$ at $s_\mu$, $-\lambda D_\mu$ at $t_\mu$ and $0$ elsewhere, and the total flow of all commodities through each undirected edge $\{i,j\}$, in both directions, is at most $C_{i,j}$. The maxflow of the network is the largest such $\lambda$.

For $S \subseteq V$, $\mathrm{Cap}(S) = \sum_{i \in S}\sum_{j \notin S} C_{i,j}$ is the capacity of the edges leaving $S$, and $\mathrm{Dem}(S)$ is the total demand of the pairs that $S$ separates, i.e. with $|S \cap \{s_\mu,t_\mu\}| = 1$. Every flow of value $\lambda$ has to push $\lambda\,\mathrm{Dem}(S)$ units across the cut, so

$$\mathrm{maxflow} \le \frac{\mathrm{Cap}(S)}{\mathrm{Dem}(S)} \quad\text{for every } S \text{ with } \mathrm{Dem}(S) > 0.$$

A semi-metric on $V$ is a function $d \ge 0$ with $d(i,i) = 0$, symmetry and the triangle inequality; distinct points may be at distance $0$, as in the paper.

Formalization targets

Goal: Theorem 4.1

There is an absolute constant $C_0 > 0$ such that every network in which some commodity has $D_\mu > 0$ and $s_\mu \ne t_\mu$ has a set $S \subseteq V$ with $\mathrm{Dem}(S) > 0$ and

$$\frac{\mathrm{Cap}(S)}{\mathrm{Dem}(S)} \le C_0 \log(\max(k,2)) \cdot \mathrm{maxflow}.$$

The constant is not fixed; only the shape $O(\log k)$ in the number of commodities is asserted.

Milestones, in the order the proof uses them

1. Weak duality (§4, p. 226): $\lambda\,\mathrm{Dem}(S) \le \mathrm{Cap}(S)$ for every feasible $\lambda \ge 0$ and every $S$.
2. LP duality display (p. 227): $\mathrm{maxflow} = \min_d \dfrac{\sum_{\{i,j\}} C_{i,j} d_{i,j}}{\sum_\mu D_\mu d_{s_\mu,t_\mu}}$ over semi-metrics $d$.
3. Corollary 3.4, Claim 2 (p. 223): every finite semi-metric space with $k$ marked pairs has a non-expanding map into some $\ell_1^m$ that shrinks each marked pair by at most $C_1 \log(\max(k,2))$.
4. Coordinate minimum (p. 227): for points of $\ell_1^m$, the cost-to-demand ratio is at least its value on the best single coordinate.
5. 0/1 rounding (pp. 227–228): for symmetric real weights $a$ and nonnegative symmetric weights $b$, the minimum of $\sum a_{ij}|z_i - z_j| / \sum b_{ij}|z_i - z_j|$ over real vectors $z$ is attained at a 0/1 vector.

Significance

The theorem bounds the flow–cut gap: the integrality gap of the linear relaxation of the sparsest cut problem is $O(\log k)$, so solving one linear program and rounding gives an $O(\log k)$-approximation to the sparsest cut. Sparsest-cut approximations are the engine of approximation algorithms for minimum bisection, graph partitioning, crossing number and VLSI layout. The dependence on $k$ rather than on the number of vertices matters when few pairs carry demand. The bound is tight up to the constant: on constant-degree expanders with all-pairs unit demands the gap is $\Omega(\log n)$ (Leighton–Rao).

The result has been proved since 1995 and is textbook material (Williamson–Shmoys, Ch. 15). It has no machine-checked proof. A formalization adds a verified bridge between concurrent flows, LP duality on networks and $\ell_1$ embeddings of finite metrics; each piece is reusable on its own. Corollary 3.4, Claim 2 in particular is a terminal version of Bourgain's theorem, of which no formal proof exists either.

Difficulty

Two steps carry the weight. The first is the duality between concurrent flows and metrics: Mathlib has no linear programming duality theorem in a form that applies directly, and the dual of the arc-flow program has to be identified with a minimum over semi-metrics, which needs a shortest-path argument on top of LP duality. The second is the embedding: Claim 2 of Corollary 3.4 must achieve distortion $O(\log k)$ on the $k$ marked pairs, independent of $|X|$. A direct application of Bourgain's theorem to the whole space gives $O(\log |X|)$, which is not enough when $k$ is much smaller than the number of vertices, and the paper's proof is a one-line reference to an earlier argument.

Formalization scope

• Vertex sets are finite types V with [Fintype V] [DecidableEq V]; capacities are a function C : V → V → ℝ with symmetry, nonnegativity and zero diagonal as fields of a Network structure. Commodities are indexed by Fin k; coincident or repeated pairs are allowed.
• Flows are arc flows; the capacity bounds the total over all commodities and both directions. maxflow is the supremum of feasible values; Lean's sSup returns $0$ on an unbounded set, which only happens without a commodity of positive demand and distinct endpoints, and the goal assumes one.
• Sums over edges are over unordered pairs: the page's $\sum_{i \ne j}$ in the LP-duality and coordinate displays counts each edge twice, while $\mathrm{Cap}$ counts it once; the statements use $\tfrac12\sum_i\sum_j$ in both places, which removes the factor-2 slip without changing the proof.
• Explicit constants. The paper's $O(\log k)$ in Theorem 4.1 is $C_0 \log(\max(k,2))$ with $C_0$ quantified before the network; the $\Omega(1/\log k)$ of Corollary 3.4 is $1/(C_1\log(\max(k,2)))$ with $C_1$ quantified before the metric space. The $\max(k,2)$ keeps $k = 1$ in scope, where $\log k = 0$.
• Out of scope. The deterministic polynomial-time algorithms of Theorem 4.1 and Corollary 3.4, and the target dimension $\ell_1^{O(n^2)}$ of the latter, are not stated; the statements assert the existence of the cut and of the embedding.
• The 0/1 rounding step adds $b \ge 0$, which the page omits but its argument needs.
• A trivializing formalization is ruled out: the constant $C_0$ is quantified before the network, so it cannot depend on the instance, and maxflow is defined from flows, not as the metric minimum.
• Contributions welcome: an LP duality theorem for finite-dimensional linear programs in the form needed here, a formal Bourgain-type embedding with terminal distortion, and the max-flow min-cut theorem for undirected capacities.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995) 215–245. https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27 (1998) 291–301. https://doi.org/10.1137/S0097539794285983
• T. Leighton, S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46 (1999) 787–832. https://doi.org/10.1145/331524.331526
• J. Bourgain, On Lipschitz embedding of finite metric spaces in Hilbert space, Israel J. Math. 52 (1985) 46–52. https://doi.org/10.1007/BF02776078
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, Chapter 15. https://doi.org/10.1017/CBO9780511921735

Motivation

Discounted Markov decision problems are solved in practice by two classical schemes. Value iteration (successive approximations) is cheap per step but contracts the error only by the discount factor $\lambda$ per step, which is slow when $\lambda$ is close to $1$. Policy iteration (Howard, 1960) converges in few steps, but each step solves a linear system for the value of the current policy. Puterman and Brumelle (Mathematics of Operations Research, 1979) showed that policy iteration is Newton's method applied to the optimality equation.

Puterman and Shin (Management Science 24, 1978) interpolated between the two schemes: replace the exact policy evaluation by $k+1$ steps of successive approximation. This is modified policy iteration of order $k$. For $k=0$ it is value iteration; as $k\to\infty$ it approaches policy iteration. The paper proves that every order converges and bounds its rate. The scheme remains a standard algorithm in dynamic programming (Puterman, Markov Decision Processes, Wiley 1994, §6.5), and it appears in reinforcement learning as "optimistic" or "generalized" policy iteration.

Timeline. Howard (1960): policy iteration for finite problems. Puterman–Brumelle (1979, circulated earlier): policy iteration as Newton–Kantorovich iteration, and the support inequality for the optimality operator. van Nunen (1976) and van Nunen–Wessels: convergence of related value-oriented methods in a different framework. Puterman–Shin (1978): convergence of modified policy iteration of every order from a starting point with $Bv_0\ge 0$, and the rate bound formalized here.

Setting

$S$ is a set of states with a $\sigma$-algebra. A family $\mathcal P$ of policies is given. Each $P\in\mathcal P$ is a transition operator: a Markov kernel assigning to each state $s$ a probability distribution $P(s,\cdot)$ on $S$. Each policy also has a one-period reward $c_P:S\to\mathbb R$, and the rewards are uniformly bounded: $\sup_P\sup_s|c_P(s)|\le M<\infty$. The discount rate satisfies $0\le\lambda<1$.

$V$ is the Banach space of bounded measurable functions $v:S\to\mathbb R$ with $\|v\|=\sup_s|v(s)|$. A kernel acts on $V$ by $(Pv)(s)=\int v(t)\,P(s,dt)$. For linear $A$ on $V$, $\|A\|=\sup_{\|x\|\le 1}\|Ax\|$.

The optimality equation is

$$Bv\equiv\max_{P\in\mathcal P}\{c_P+(\lambda P-I)v\}=0. \tag{1}$$

The paper assumes throughout that the maximum in (1) is attained for every $v\in V$, by a single policy $P_v$ at every state.

For $k\ge 0$, the truncated Neumann series is $A^k_P=\sum_{i=0}^k(\lambda P)^i$. Modified policy iteration of order $k$ runs the recursion

$$v_{n+1}=v_n+A^k_{P_n}Bv_n, \tag{4}$$

where $P_n$ attains the maximum in (1) at $v_n$. A solution $v^*\in V$ of $Bv^*=0$ exists and is unique. $P^*=P_{v^*}$ denotes a policy attaining the maximum at $v^*$. The proofs also use the operators $U^kv=\max_P\{\sum_{i=0}^k(\lambda P)^ic_P+(\lambda P)^{k+1}v\}$ and the set $V_B=\{v\in V:Bv\ge 0\}$.

Formalization targets

Goal: Theorem 2, bound (8)

If $v_0\in V$ and $Bv_0\ge 0$, then for every $n$

$$\|v^*-v_{n+1}\|\ \le\ \min\Big\{\lambda,\ \frac{\lambda[1-\lambda^k]}{1-\lambda}\,\|P_n-P^*\|+\lambda^{k+1}\Big\}\,\|v_n-v^*\|. \tag{8}$$

Milestones

1. The support inequality (7): $Bw\ge Bv+(\lambda P_v-I)(w-v)$ for all $v,w\in V$.
2. Lemma 1: $U^k$ is a contraction with constant $\lambda^{k+1}$.
3. Lemma 2: $U^k$-iteration converges geometrically to the unique fixed point of $U^k$, and this fixed point solves $Bu=0$.
4. Lemma 3: $U^ku\ge(I+A^kB)v$ for $u\ge v$, and $(I+A^kB)u\ge U^0v$ if in addition $Bu\ge 0$.
5. Lemma 4: $V_B$ is invariant under $I+A^kB$.
6. Theorem 1: from $Bv_0\ge 0$, $\{v_n\}$ converges monotonically and in norm to $v^*$.
7. Corollary 1: $(U^0)^nv_0\le v_n\le (U^k)^nv_0$.
8. The two halves of (8): inequality (9), $\|v^*-v_{n+1}\|\le(\tfrac{\lambda[1-\lambda^k]}{1-\lambda}\|P_n-P^*\|+\lambda^{k+1})\|v^*-v_n\|$, and $\|v^*-v_{n+1}\|\le\lambda\|v^*-v_n\|$.

The mission also contains four further theorems that are not milestones: Corollary 2 (asymptotic rate at most $\lambda^{k+1}$ when $\|P_n-P^*\|\to 0$), Proposition 2 (monotonicity in the order $k$), the representation (6) $v_{n+1}=T_n^{k+1}v_n$, and Proposition 1 (policy iteration as Newton's method).

Significance

The result. Bound (8) gives two guarantees. Every order of modified policy iteration converges at least as fast as value iteration, with factor $\lambda$ per step. Once the improving policies stabilize near an optimal one, the factor approaches $\lambda^{k+1}$, the factor of $k+1$ value-iteration steps. This justifies spending $k$ cheap evaluation sweeps per policy improvement instead of solving a linear system. It also underlies the analysis of the many later variants: action elimination, asynchronous and approximate versions, and optimistic policy iteration in reinforcement learning.

Formalizing it. The theorems are proved on paper. As far as the platform's library shows, none of them is machine-checked: existing items cover value iteration and exact policy iteration for finite state spaces. This mission formalizes the whole chain on general measurable state spaces with Markov kernels, including the support inequality and the comparison operators $U^k$. Corollary 2 is stated as an upper bound only, because the equality printed on the page fails in degenerate runs (see the item's note).

Difficulty

The obvious route to a rate is the contraction argument for value iteration: $U^0$ is monotone and a $\lambda$-contraction, so its iterates converge geometrically. For $k\ge1$ that argument does not transfer to the map $v_n\mapsto v_n+A^k_{P_n}Bv_n$. The truncated series is taken for the policy chosen at the current point, so the map changes with $v_n$, and it is not monotone in general. The van der Wal–van Nunen example on p. 1133 of the paper shows that iterates of a higher order need not dominate those of a lower order from the same start. Moreover, without the condition $Bv_0\ge0$ the iterates need not even increase. A rate for (4) is therefore not a corollary of a fixed-point theorem for a single operator.

Formally, a second layer of difficulty is the setting itself. Everything happens in the space of bounded measurable functions on a general measurable space. So every operator applied to an iterate must be shown to preserve boundedness and measurability, and the maxima over policies are suprema over an arbitrary index set.

Formalization scope

The Lean development (namespace ModPolicyIter.Conv) represents:

• the policies as an index type $\iota$, policy $i$ being a Markov kernel P i : Kernel S S with a measurable reward c i, $|c_i|\le M$;
• $V$ by the predicate IsBM (measurable and bounded), with supNorm v = ⨆ s, |v s|;
• $P_iv$ as the Bochner integral against $P_i(s,\cdot)$;
• $B$ and $U^k$ as pointwise real suprema over $\iota$;
• $\|P_i-P_j\|$ as the supremum of $\|(P_i-P_j)x\|$ over the unit ball of $V$.

The standing assumptions of §2 are carried by the model fields; items using a maximizer assume either global attainment (MaxAttained) or an explicit maximizing policy. A run of (4) is a sequence of functions paired with a sequence of policies, each policy a maximizer at the current iterate. Only $v_0\in V$ is assumed; that later iterates lie in $V$ is part of the proofs.

Deviations from the page, all disclosed in the items:

1. Theorem 2 and its companions assume $Bv_0\ge0$, the hypothesis of Theorem 1, which the proof of Theorem 2 invokes.
2. Lemmas 1–2 and Corollary 1 assume that $U^k$ maps $V$ into $V$. This is implicit on the page, and for $k=0$ it follows from attainment. Lemma 1 states this mapping property alongside the contraction inequality.
3. The paper's $\mathcal P=\prod_s\mathcal P_s$ is generalized to an arbitrary index set.
4. Corollary 2 is stated as an upper bound.

The goal must not be trivialized by assuming $v_n\le v^*$, the support inequality, the sandwich of Corollary 1, or anything about $U^k$. These are milestones to be proved, and none of them is a hypothesis of the goal.

Reusable infrastructure includes Markov kernels as operators on bounded measurable functions (positivity, $\|P\|\le1$, measurability of $Pv$), completeness of $V$, and the Banach fixed point theorem on $V$. The first of these serves any discounted dynamic-programming mission on general state spaces. Contributions of any milestone, or of helper lemmas about these operators, are welcome.

Selected references

• M. L. Puterman and M. C. Shin, Modified policy iteration algorithms for discounted Markov decision problems, Management Science 24(11):1127–1137, 1978. https://doi.org/10.1287/mnsc.24.11.1127
• M. L. Puterman and S. L. Brumelle, On the convergence of policy iteration in stationary dynamic programming, Mathematics of Operations Research 4(1):60–69, 1979. https://doi.org/10.1287/moor.4.1.60
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. A. E. E. van Nunen, A set of successive approximation methods for discounted Markovian decision problems, Zeitschrift für Operations Research 20:203–208, 1976.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Maximum likelihood estimates, least-squares fits and sample-average approximations of stochastic programs solve $0 = \bar f^\nu(x)$, where $\bar f^\nu$ averages a random integrand over $\nu$ observations. Their classical asymptotic theory rests on the implicit function theorem and needs a smooth, unconstrained problem.

When the estimate is constrained to a set, for example a nonnegativity constraint, a simplex or a polyhedron, the first-order conditions become a generalized equation

$$0 \in f(z, x) + N(x),$$

where $N$ is a multifunction such as the normal cone of the constraint set. The same form describes optimality conditions of stochastic programs and variational inequalities. Aitchison and Silvey (1958) treated equality-constrained maximum likelihood. Huber (1967) allowed nonsmooth estimating functions but required an open parameter domain. Dupačová and Wets (1988) and Shapiro (1989) derived limit laws for solutions of stochastic programs under smoothness of the expected gradient. King and Rockafellar (1993) gave a general theory that needs neither smoothness of the expected map nor single-valuedness of $N$: the limit law of the normalized error is the image of a Gaussian under a contingent derivative, a positively homogeneous and generally nonlinear map, so the limit is generally not normal.

Setting

Let $Z$ be a separable Banach space with norm $\|\cdot\|$, and let $|\cdot|$ be the Euclidean norm on $\mathbb R^n$ and $\mathbb R^m$. A multifunction $G : Z \rightrightarrows \mathbb R^n$ assigns a set $G(z) \subseteq \mathbb R^n$ to each $z$. Its graph is $\operatorname{gph} G$ and its inverse is $G^{-1}(x) = \{z \mid x \in G(z)\}$.

For sets $A_t$ indexed by $t \downarrow 0$, the upper limit $\limsup A_t$ consists of the points $x$ with $x = \lim x_k$, $x_k \in A_{t_k}$ for some $t_k \downarrow 0$, and the lower limit of the points reachable along every such sequence. The contingent derivative of $G$ at $(z, x) \in \operatorname{gph} G$ is the multifunction $DG(z|x)$ with

$$\operatorname{gph} DG(z|x) = \limsup_{t \downarrow 0} t^{-1}\big[\operatorname{gph} G - (z,x)\big].$$

$G$ is proto-differentiable when this upper limit equals the lower limit, and semi-differentiable when $t^{-1}[G(z + t w') - x] \to DG(z|x)(w)$ as $t \downarrow 0$ and $w' \to w$. A single-valued $g$ is B-differentiable at $z$ when $t^{-1}[g(z + tw') - g(z)] \to Dg(z)(w)$ in the same sense.

The deterministic problem is $0 \in f(z, x) + N(x)$ with $f : Z \times \mathbb R^n \to \mathbb R^m$, data $z$ and solution map $J(z)$. At a reference pair $(z^*, x^*)$ set $F = f(z^*, \cdot) + N$. The analytical assumptions M.1–M.4 are as follows. $f$ is jointly continuous and B-differentiable in each variable, with the $z$-derivative $D_z f(z^*, x^*)$ strong (uniform in $x$ near $x^*$). $N$ is closed and proto-differentiable. $F$ is subinvertible: $0 \in F(x^*)$, and a closed-graph, convex-valued selection of $F^{-1}$ near $0$ passes through $x^*$. The contingent derivative $DF^{-1}(0|x^*)$ is at most single-valued.

The statistical problem has i.i.d. random elements $s_1, s_2, \dots$ of a measurable space $S$ and an integrand $f : U \times S \to \mathbb R^m$ on a compact neighborhood $U$ of $x^*$. It satisfies the probabilistic assumptions P.1–P.4: continuity in $x$, measurability in $s$, a finite second moment at one point, and a Lipschitz bound $|f(x_1,s) - f(x_2,s)| \le a(s)|x_1 - x_2|$ with $E a(s_1)^2 < \infty$. The M-estimate $x^\nu$ is a measurable solution of

$$0 \in \bar f^\nu(x) + N(x), \qquad \bar f^\nu(x) = \frac1\nu\sum_{i=1}^\nu f(x, s_i),$$

and the true equation is $0 \in Ef(x) + N(x)$ with $F = Ef + N$.

Formalization targets

Goal: Theorem 2.7 (asymptotic distribution of M-estimates)

Under P.1–P.4 on a compact neighborhood $U$ of $x^*$, B-differentiability of $Ef$ at $x^*$, and M.2–M.4 for $F = Ef + N$, every sequence of measurable solutions $x^\nu$ of (2.5) with $x^\nu \to x^*$ almost surely satisfies

$$\sqrt\nu\,[x^\nu - x^*] \xrightarrow{\ \mathcal D\ } DF^{-1}(0|x^*)(-w^*), \qquad w^* \sim \mathcal N\big(0, \operatorname{cov} f(x^*, s_1)\big).$$

The goal fixes the limit law completely: the map is the contingent derivative of $F^{-1}$, and the Gaussian has the covariance of the integrand at $x^*$.

Milestones

• Theorem 2.4 gives bounds in probability, $P\{|x^\nu - x^*| > \delta\} \le P\{\alpha\lambda\|z^\nu - z^*\| > \delta\}$. Its proof uses the upper-Lipschitz property $U \cap F^{-1}(y) \subseteq x^* + \lambda|y|B$ (a display of the proof).
• Theorem 2.6 is the abstract limit theorem: if $\tau_\nu^{-1}[z^\nu - z^*] \to_{\mathcal D} w$, then $\tau_\nu^{-1}[x^\nu - x^*] \to_{\mathcal D} DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$. Its proof uses two displays: semi-differentiability of the localized solution map, with $DJ(z^*|x^*)(w) = DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$, and a Lipschitz bound $|x - x^*| \le \lambda\|z - z^*\|$ on $U \cap J(z)$.
• Proposition A1, Corollary A2 and Theorem A3 concern the space $C_m(U)$ under P.1–P.4. The integrand and the empirical means are random elements of $C_m(U)$, and $\sqrt\nu(\bar f^\nu - Ef)$ converges in distribution to a Gaussian element of $C_m(U)$.

The three displays (Theorem 2.4's upper-Lipschitz inclusion, and Theorem 2.6's semi-differentiability and Lipschitz bound) are statements the paper cites from King and Rockafellar, Sensitivity analysis for nonsmooth generalized equations ([12]: Proposition 2.1, Theorem 4.1, Remark 4.3). They are cited results, not this paper's own, and are milestones because the proofs of Theorems 2.4 and 2.6 rest on them.

Significance

Theorem 2.7 gives the limit law of constrained and nonsmooth M-estimates in a form that can be computed. When $N$ is the normal cone of a polyhedron, $DF^{-1}(0|x^*)$ is piecewise linear, and the limit is the solution of a random linear complementarity or quadratic problem driven by a Gaussian vector. This underlies the asymptotic theory of sample-average approximation in stochastic programming, where the paper applies it to stochastic programs (§3) and to piecewise linear-quadratic tracking problems (§4). Theorem 2.6 separates the deterministic sensitivity analysis from the probability, so any data sequence with a known limit law yields a limit law for the solutions.

The result is proved in the paper modulo the cited theorems of [12] and [11], but none of it is machine-checked. Mathlib has the real-valued i.i.d. central limit theorem, Gaussian measures on Banach spaces and convergence in distribution. It has no multivariate or Banach-space central limit theorem, no contingent derivatives and no set-valued implicit function theorem. Formalizing the mission produces these, along with a checked version of the cited sensitivity results.

Difficulty

The classical argument linearizes $F$ at $x^*$, inverts the Jacobian and applies the delta method. Here $F$ is set-valued and its derivative is only positively homogeneous. There is no Jacobian to invert, and the solution map need not be differentiable or even single-valued away from $x^*$. The replacement for the implicit function theorem is the semi-differentiability of the localized solution map under M.1–M.4. Proving it means controlling both the upper and the lower set limits of difference quotients of solution sets, and subinvertibility is what supplies existence of nearby solutions.

The probabilistic side cannot work coordinate by coordinate either. The estimate solves an equation in the whole function $\bar f^\nu$, so convergence of $\bar f^\nu$ at finitely many points is not enough. The central limit theorem must hold in the sup norm on $C_m(U)$, which requires tightness of the empirical process, and only then can the deterministic sensitivity result be composed with it.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), and $Z$ is a real normed space with [CompleteSpace Z] [SeparableSpace Z] where the paper says "separable Banach". Set limits are Kuratowski limits along filters ($t \downarrow 0$ is 𝓝[>] 0, and $(t,w') \to (0^+,w)$ is the product filter). The contingent derivative is defined by (2.2) alone. M.4's printed sum formula equals it under M.1, and this is not assumed. "B-differentiable" is read as the limit (2.4). Products carry Lean's max norm. $s_1$ is s 0, empirical means sum over Finset.range ν, and (2.5) is required for $\nu \ge 1$. $F = Ef + N$ is empty off $U$. Convergence in distribution is Mathlib's TendstoInDistribution, with the limit on its own probability space. The law of $w^*$ is fixed through linear functionals: $\langle\ell, w^*\rangle \sim \mathcal N(0, \operatorname{Var}\langle\ell, f(x^*,s_1)\rangle)$. In Appendix A1–A3 the integrand is S → C(↥U, Rn m) with the Borel σ-algebra, and "Gaussian" is IsGaussian.

Explicit choices relative to the printed text:

1. The paper states that an almost surely convergent sequence of solutions "converges to the point $x^*$" (Theorems 2.6 and 2.7). This is false when the true equation has a second solution: $f(z,x) = x^2 - x - z$, $N \equiv \{0\}$, $z^* = x^* = 0$ satisfies M.1–M.4 with $J(0) = \{0, 1\}$. The formalization assumes $x^\nu \to x^*$ almost surely instead.
2. $0 \in F(x^*)$ (presupposed by $DF^{-1}(0|x^*)$) is explicit in Theorem 2.4 and the upper-Lipschitz display.
3. The threshold for "all sufficiently small $\delta$" in Theorem 2.4 is chosen with $U$ and $\lambda$, before the random elements.
4. Proposition A1 and Corollary A2 carry P.1–P.4, as stated or inherited on the Appendix page, though their measurability conclusions use only P.1.
5. In the limit theorems, the single-valued map $DF^{-1}(0|x^*)$ is a function $L$ whose values lie in the contingent derivative at every point.

The conclusion of the goal names its limit: the image of the stated Gaussian under a map $L$ whose values lie in the contingent derivative of $F^{-1}$. A statement asserting only that $\sqrt\nu(x^\nu - x^*)$ converges in distribution to some limit, or replacing $DF^{-1}(0|x^*)$ by a linear map, is a different and weaker theorem. A sorry-free check confirms that the goal's hypotheses can all be met (a degenerate instance with $f(x,s) = x$, $N \equiv \{0\}$).

A complete development needs Kuratowski set convergence and contingent derivatives (reusable across set-valued analysis), a central limit theorem in $C(K)$ for Lipschitz-indexed processes (reusable for empirical-process theory), and a continuous-mapping argument for random closed sets. Contributions to any of these layers are welcome, as are proofs of the cited [12] statements.

Selected references

• A. J. King and R. T. Rockafellar, Asymptotic theory for solutions in statistical estimation and stochastic programming, Mathematics of Operations Research 18(1) (1993). https://doi.org/10.1287/moor.18.1.148
• A. J. King and R. T. Rockafellar, Sensitivity analysis for nonsmooth generalized equations, Mathematical Programming 55 (1992) 193–212. https://doi.org/10.1007/BF01581199
• A. J. King, Generalized delta theorems for multivalued mappings and measurable selections, Mathematics of Operations Research 14(4) (1989) 720–736. https://doi.org/10.1287/moor.14.4.720
• J. Dupačová and R. J.-B. Wets, Asymptotic behavior of statistical estimators and of optimal solutions of stochastic optimization problems, Annals of Statistics 16(4) (1988) 1517–1549. https://doi.org/10.1214/aos/1176351052
• A. Shapiro, Asymptotic properties of statistical estimators in stochastic programming, Annals of Statistics 17(2) (1989) 841–858. https://doi.org/10.1214/aos/1176347146
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 221–233. https://projecteuclid.org/euclid.bsmsp/1200512988
• A. Araujo and E. Giné, The Central Limit Theorem for Real and Banach Valued Random Variables, Wiley, 1980.