Operations Research

Motivation

Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.

Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least $A_v$. Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in $[A_v-1,\,B_v+1]$.

Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most $\Delta^*+1$ in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most $B_v+2$. Singh and Lau (STOC 2007) improved this to $B_v+1$, which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.

Setting

Let $G=(V,E)$ be a finite simple graph with edge costs $c_e\in\mathbb R$; no sign or triangle inequality is assumed. Let $F$ be a forest on $V$ with no edge in common with $E$. A set $H\subseteq E$ is an $F$-tree if $H\cup F$ is a spanning tree of $V$, and $d_H(v)$ is the number of edges of $H$ at $v$. Integer lower bounds $A_v$ are given on $U\subseteq V$ and integer upper bounds $B_v$ on $W\subseteq V$. The minimum bounded degree connecting tree problem asks for a cheapest $F$-tree with $A_v\le d_H(v)$ on $U$ and $d_H(v)\le B_v$ on $W$; with $F=\varnothing$ it is the spanning-tree problem.

The supernodes are the vertex sets of the components of $(V,F)$, isolated vertices included, and $\mathcal I(F)$ is the family of unions of supernodes. For $S\subseteq V$, $E(S)$ and $F(S)$ are the edges with both endpoints in $S$, $\delta(S)$ the edges with exactly one endpoint in $S$, and $x(D)=\sum_{e\in D}x_e$. The linear relaxation LP-MBDCT$(G,\mathcal A,\mathcal B,U,W,F)$ minimizes $\sum_e c_ex_e$ subject to

$$x(E(V))=|V|-|F(V)|-1,\quad x(E(S))\le|S|-|F(S)|-1\ (S\in\mathcal I(F)),\quad A_v\le x(\delta(v))\ (v\in U),\quad x(\delta(v))\le B_v\ (v\in W),\quad x\ge0.$$

MBDCT Algorithm2 (Figure 5 of the paper) repeats: if $F$ is a spanning tree, stop; otherwise take a basic optimal solution $x^*$, delete the edges with $x^*_e=0$, move one edge with $x^*_e=1$ (if any) into $F$ and lower $A$ and $B$ by one at its endpoints, and otherwise remove from $U$ and $W$ one vertex whose support degree is at most two.

Formalization targets

Goal: Theorem 5.2

For every well-formed instance whose LP is feasible, MBDCT Algorithm2

1. has a terminating run;
2. makes at most $|V|-|F|-1+|U\cup W|$ iterations on every run;
3. returns only $F$-trees $H\subseteq E$ with

$$c(H)\le\sum_{e\in E}c_ex_e\ \text{for every feasible }x,\qquad A_v-1\le d_H(v)\ (v\in U),\qquad d_H(v)\le B_v+1\ (v\in W).$$

The statement fixes no constants beyond the paper's $\pm1$, and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.

Milestones

In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with $|E^*|=|\mathcal L|+|T_U|+|T_W|$); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value $x^*(D(S))=r-1$ on the edges between the $r$ members of $S$, and when a set is special); Lemma 5.6 (every set of $\mathcal L$ keeps at least three tokens, exactly three only if it is special or $V$); and Lemma 5.1 (a basic solution has an edge with $x^*_e=1$ or a vertex of $U\cup W$ with support degree two).

Significance

The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the $(1,B_v+1)$ guarantee, which cannot be improved to $B_v$ unless P = NP, since a Hamiltonian path is the case $B_v\equiv 2$. With lower bounds it also covers prescribed minimum degrees.

The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.

Difficulty

The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound $|E^*|=|\mathcal L|+|T_U|+|T_W|$ from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of $A$, $B$, $U$, $W$ and $F$ along the run.

Formalization scope

Vertices form a Fintype; edges are elements of Sym2 V with no loops, and $E$, $F$ are finite sets of edges with $F$ acyclic and disjoint from $E$. LP vectors are functions on Sym2 V that vanish off $E$. Right-hand sides are computed in $\mathbb R$, degree bounds are integers, and the subtour rows range over nonempty $S\in\mathcal I(F)$ (at $S=\varnothing$ the literal row $0\le-1$ would make the LP empty). A basic solution is a feasible $x$ that is the only vector on $E$ satisfying with equality every constraint tight at $x$, including the tight rows $x_e=0$. Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.

The paper's loose phrases are made explicit as follows.

• "Polynomial time" becomes the iteration bound; the LP is solved by an oracle that returns any basic optimal solution. The ellipsoid method and the separation oracle are out of scope.
• "The algorithm returns" becomes three claims: a run exists, every run is bounded, and every returned set satisfies the guarantee. The guarantee alone would hold vacuously for a relation that can get stuck.
• "Cost at most the cost of the optimal LP solution" becomes $c(H)\le c\cdot x$ for every feasible $x$.
• "Distribute the tokens" (Lemma 5.6) becomes a counting inequality on the surplus of tokens.
• Claim 5.9's "contains exactly three special members" means that $S$ has exactly three members, all of them special.
• Figure 5's Step 4 is guarded by "no edge was picked in Step 3", as the paper's text under Lemma 5.1 states.
• "$F$ is not a spanning tree" and LP feasibility are explicit hypotheses where the paper leaves them implicit.

Two trivializations are ruled out. Existence of a cheap tree with degrees in $[A_v-1,B_v+1]$ is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.

Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.

Selected references

• M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, STOC 2007, pp. 661–670. https://doi.org/10.1145/1250790.1250887
• M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, J. ACM 62(1), 2015. https://doi.org/10.1145/2629366
• M. X. Goemans, Minimum bounded degree spanning trees, FOCS 2006, pp. 273–282. https://doi.org/10.1109/FOCS.2006.48
• M. Fürer, B. Raghavachari, Approximating the minimum-degree Steiner tree to within one of optimal, J. Algorithms 17(3), 1994, pp. 409–423. https://doi.org/10.1006/jagm.1994.1042

Motivation

Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with $\ell_1$-regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.

Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.

The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.

Setting

Let $\Re^n$ carry the Euclidean norm $\|\cdot\|$, let $\mathcal N=\{1,\dots,n\}$, and for $\mathcal J\subseteq\mathcal N$ let $x_{\mathcal J}$ be the subvector of coordinates in $\mathcal J$. The problem (1) is

$$\min_x\ F_c(x)=f(x)+cP(x),$$

where $c>0$, $P:\Re^n\to(-\infty,\infty]$ is proper, convex and lower semicontinuous, and $f$ is continuously differentiable on an open set containing $\operatorname{dom}P$.

Given $x\in\operatorname{dom}P$, a nonempty block $\mathcal J$ and a symmetric positive definite matrix $H$, the direction (6) is

$$d_H(x;\mathcal J)=\arg\min_d\Big\{\nabla f(x)^Td+\tfrac12d^THd+cP(x+d)\ \Big|\ d_j=0\ \forall j\notin\mathcal J\Big\}.$$

The CGD method starts at $x^0\in\operatorname{dom}P$, chooses at each iteration $k$ a block $\mathcal J^k$ and a matrix $H^k$, computes $d^k=d_{H^k}(x^k;\mathcal J^k)$, and sets $x^{k+1}=x^k+\alpha^kd^k$. The Armijo rule takes $\alpha^k$ as the largest element of $\{\alpha^k_{\rm init}\beta^j\}_{j\ge0}$ with

$$F_c(x^k+\alpha^kd^k)\le F_c(x^k)+\alpha^k\sigma\Delta^k,\qquad \Delta^k=\nabla f(x^k)^Td^k+\gamma\,d^{kT}H^kd^k+cP(x^k+d^k)-cP(x^k),$$

with $0<\beta,\sigma<1$ and $0\le\gamma<1$. The restricted Gauss–Seidel rule (12) asks for indices $0=t_0<t_1<\cdots$ (the set $\mathcal T$) such that the blocks used during each cycle $t_i\le k<t_{i+1}$ are pairwise disjoint and cover $\mathcal N$. $P$ is block-separable with respect to $\mathcal J$ if $P(x)=P_{\mathcal J}(x_{\mathcal J})+P_{\mathcal J^C}(x_{\mathcal J^C})$.

The analysis uses three assumptions: $\nabla f$ is $L$-Lipschitz on $\operatorname{dom}P$ (22); Assumption 1, $\bar\lambda I\succeq H^k\succeq\underline\lambda I$ with $0<\underline\lambda\le\bar\lambda$; and Assumption 2. Writing $\bar X$ for the set of stationary points of $F_c$ and $d_I(x)$ for the full direction with $H=I$, Assumption 2 says (a) $\bar X\ne\emptyset$ and the local Lipschitzian error bound $\operatorname{dist}(x,\bar X)\le\tau\|d_I(x)\|$ holds on every level set $\{F_c\le\zeta\}$ wherever $\|d_I(x)\|\le\epsilon$; (b) stationary points with different objective values are at least a fixed distance $\delta>0$ apart.

Formalization targets

Goal: Theorem 2(b)

Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of $P$ with respect to every $\mathcal J^k$, and Armijo steps with $\sup_k\alpha^k_{\rm init}\le1$ and $\inf_k\alpha^k_{\rm init}>0$:

$$\{F_c(x^k)\}\downarrow-\infty\quad\text{or}\quad\big(\{F_c(x^k)\}_{\mathcal T}\ \text{Q-linear}\ \text{and}\ \{x^k\}_{\mathcal T}\ \text{R-linear}\big).$$

No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.

Milestones

Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, $\Delta^k\to0$, $d^k\to0$), and Theorem 2(a) (the residual $\|d_I(x^k)\|$ at the start of a cycle is bounded by the step lengths of the cycle).

Significance

Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).

The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.

Difficulty

The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives $F_c(x^{k+1})-\bar\upsilon\le\tau'\|x^{k+1}-x^k\|^2$ from the error bound, where $\bar\upsilon$ is the limit value. With a nonsmooth $P$ this inequality is not available: the authors say so on p. 405, and work with $-\Delta^k$ in place of the quadratic term. A second obstacle is that the error bound controls the full residual $d_I(x^k)$, while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of $P$. Neither the global analysis nor the error bound alone gives the rate.

Formalization scope

$\Re^n$ is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued $P$ is encoded as a pair: its effective domain $D=\operatorname{dom}P$ and its finite values on $D$, with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; $F_c$ is never evaluated off $D$, and every statement carries membership in $D$ explicitly. The direction $d_H(x;\mathcal J)$ is the unique minimizer of (6) when $x\in D$ and $H\succ0$ (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent $j$. $\mathcal T$ is a strictly increasing map $t$ with $t_0=0$. Stationarity is $F_c'(x;d)\ge0$ for all $d$, in liminf form. In Assumption 2, $\operatorname{dist}$ is the infimum distance and "for any $\zeta\ge\min F_c$" is "for every real $\zeta$" (equivalent, since the condition is empty below $\inf F_c$). Q-linear convergence includes convergence of the sequence; R-linear convergence is $\|x^{t_i}-\bar x\|\le Cq^i$ with $q<1$. The rates in the goal are along $\mathcal T$, as the paper states.

Explicit choices relative to the printed text:

• Theorem 2(a) is corrected. As printed, $\|d_I(x^k)\|\le\sup_j\alpha^j\,C\,r^k$ fails for small constant stepsizes and fails without block-separability (counterexamples in the item's statement). The milestone states $\|d_I(x^k)\|\le\max\{1,\sup_j\alpha^j\}\,C\,r^k$ under block-separability of $P$ with respect to every $\mathcal J^k$ (both are what the paper's proof gives and what Theorem 2(b) supplies), with the iterates in $\operatorname{dom}P$, and with $C$ quantified before the problem data, so it depends only on $n,L,\underline\lambda,\bar\lambda$.
• Lemma 5(b)'s range $0\le\alpha\le\min\{1,2\underline\lambda(1-\sigma+\sigma\gamma)/L\}$ is stated as $0\le\alpha\le1$ and $\alpha L\le2\underline\lambda(1-\sigma+\sigma\gamma)$, so that $L=0$ gives $[0,1]$ as on paper rather than $\{0\}$.
• Lemma 5(a) holds for every decomposition of $P$ in (20), and $\bar x$ ranges over $\operatorname{dom}P_{\mathcal J}$ (outside it the left side is $-\infty$).
• "$\lim F_c(x^k)>-\infty$" is "the values $F_c(x^k)$ are bounded below"; "$\{F_c(x^k)\}\downarrow-\infty$" is "nonincreasing and tending to $-\infty$"; suprema and infima of stepsizes are explicit bounds.

A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along $\mathcal T$, or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.

Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of $d_H(x;\mathcal J)$, optimality conditions) that the milestones rely on.

Selected references

• P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming Ser. B 117 (2009) 387–423. https://doi.org/10.1007/s10107-007-0170-0
• Z.-Q. Luo and P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970, Chap. 9 (Q- and R-linear convergence). https://doi.org/10.1137/1.9780898719468
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

A G/GI/N queue has $N$ identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution $F$ of mean $1$. In the Halfin–Whitt regime the number of servers grows while the traffic intensity $\rho^N$ approaches $1$ at rate $\sqrt N(1-\rho^N)\to\beta\in\mathbb R$; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.

Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against $F$ is replaced by a convolution against the renewal function of $F$. With exponential service the renewal function is $M(t)=t$, and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.

Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.

Setting

Let $\mu$ be a probability measure on $[0,\infty)$ with mean $\int x\,d\mu(x)=1$ (the service-time law), $F(t)=\mu((-\infty,t])$ its distribution function and $G=1-F$ its tail. The equilibrium distribution is

$$F_e(x)=\int_0^x G(u)\,du,\qquad x\ge0.\tag{5.4}$$

Let $\mu^{*n}$ be the $n$-fold convolution of $\mu$ (the law of the $n$th renewal epoch $S_n$). The renewal measure is $dM=\sum_{n\ge1}\mu^{*n}$ and the renewal function is $M(t)=\sum_{n\ge1}F^{*n}(t)$, the expected number of renewals by time $t$.

A path $x:\mathbb R\to\mathbb R$ is càdlàg on $[0,\infty)$ if it is right continuous at every $t\ge0$ with finite left limits at every $t>0$; only its values on $[0,\infty)$ matter. Fix a càdlàg driving path $\zeta$ (in the paper $\tilde\zeta=\tilde M_Q+\tilde Q_I$, (5.40)) and $\beta\in\mathbb R$. Write $y^+=\max(y,0)$ and $y^-=\min(y,0)\le0$. The two equations are

$$q(t)=\zeta(t)-\beta F_e(t)+\int_0^t q^+(t-s)\,dF(s),\qquad t\ge0,\tag{5.33}$$ $$q(t)=\zeta(t)+\int_0^t\zeta(t-u)\,dM(u)-\beta t-\int_0^t q^-(t-u)\,dM(u),\qquad t\ge0.\tag{5.41}$$

All Stieltjes integrals are over the closed interval $[0,t]$.

Formalization targets

Goal: Corollary 5.2 (p. 29)

For every service law $\mu$, every càdlàg $\zeta$ and every $\beta$:

$$\forall q\ \text{càdlàg}:\quad q\ \text{solves (5.33)}\iff q\ \text{solves (5.41)},$$

and (5.41) has a càdlàg solution that is unique on $[0,\infty)$ among càdlàg paths.

Milestones, in proof order

1. (5.39): $M$ is finite, solves $M(t)=F(t)+\int_0^tM(t-u)\,dF(u)$, and is its unique locally bounded measurable solution.
2. (5.42)–(5.43): for locally bounded measurable $H$, $r=H+\int_0^tH(t-u)\,dM(u)$ is the unique locally bounded solution of $r(t)=H(t)+\int_0^tr(t-u)\,dF(u)$.
3. The identity $F_e(t)+\int_0^tF_e(t-s)\,dM(s)=t$ for $t\ge0$ (p. 30).
4. (5.44): every càdlàg solution of (5.33) satisfies (5.41) with $-\beta t$ replaced by $-\beta\bigl(F_e(t)+\int_0^tF_e(t-s)\,dM(s)\bigr)$.
5. (5.46) (further): for exponential service of rate $1$, $M(t)=t$ and (5.41) becomes $q(t)=\zeta(t)+\int_0^t\zeta(s)\,ds-\beta t-\int_0^tq^-(s)\,ds$.

Significance

The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process $\zeta$ and whose only nonlinearity is the idle-server term $\int_0^tq^-(t-u)\,dM(u)$. This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that $\tilde Q^N\Rightarrow\tilde Q_M$, the solution of (5.41).

The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on $[0,\infty)$ with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity $F_e+F_e*dM=t$; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.

Difficulty

The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when $F$ may have an atom at $0$, and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at $0$. The converse direction, (5.41) $\Rightarrow$ (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in $q$. The uniqueness of (5.41) is not a contraction argument either: the atom of $dM$ at $0$ has mass $F(0)/(1-F(0))$, which may exceed $1$, so a naive Picard estimate on $[0,\delta]$ fails.

Formalization scope

• Paths are functions $\mathbb R\to\mathbb R$; every equation is asserted for $t\ge0$ and every uniqueness is equality on $[0,\infty)$. Values at negative times are never read.
• The service law is a probability measure $\mu$ on $\mathbb R$ with $\mu((-\infty,0))=0$, integrable identity and mean $1$. The paper places "no additional restrictions on $F$ beyond a first moment".
• The renewal measure is defined as $\sum_{n\ge1}\mu^{*n}$ (Mathlib's additive convolution of measures), not through an i.i.d. sequence; the paper's "expected number of renewals" equals it by Tonelli.
• Stieltjes integrals are Lebesgue integrals over the closed $[0,t]$, so atoms at $0$ of $dF$ and $dM$ are included. $q^-$ is $\min(q,0)$, not Mathlib's negPart.
• Explicit readings: "unique strong solution" is existence and uniqueness among càdlàg paths, pathwise for each fixed $\zeta$. The paper's random statement follows by applying it to each sample path, which lies in $D[0,\infty)$ almost surely (p. 30). "Locally bounded" is bounded on every $[0,T]$, with measurability added for the functions in (5.39) and (5.42).
• Corrected slip: (5.42) prints $\int_0^tr(t)\,dF(t-u)$; the stated equation is $\int_0^tr(t-u)\,dF(u)$. Milestone (5.42)–(5.43) assumes $F$ carried by $[0,\infty)$ with $F(0)<1$, under which the cited result holds.
• Ruled out: the solution of (5.33) is not assumed to exist (it exists by the paper's Proposition 3.1 with $a=0$, $B=F$, which the solver must supply). $M$ is the renewal measure of the same $F$, never an arbitrary measure assumed to satisfy (5.39). Uniqueness is among càdlàg paths on $[0,\infty)$, so no non-measurable path makes an integral vanish.
• Not in the mission: Theorems 4.1 and 5.1 (weak convergence in the Skorohod space), whose limit this corollary rewrites, and the Brownian-motion claim after (5.46).
• Related platform items, credited but not the same object: BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below $1$); ChenWhitt93.Reflection.Basic (càdlàg paths on $[0,T]$). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.

Selected references

• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6), 2009, 2211–2269. https://arxiv.org/abs/0912.2837 (v1), https://doi.org/10.1214/09-AAP609
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Oper. Res. 29(3), 1981, 567–588. https://doi.org/10.1287/opre.29.3.567
• S. Karlin and H. M. Taylor, A First Course in Stochastic Processes, 2nd ed., Academic Press, 1975 (reference [11] of the paper).
• S. M. Ross, Stochastic Processes, Wiley, 1983 (reference [19] of the paper, Exercise 3.4).

Motivation

A dynamic programming problem in Blackwell's sense describes a controller who observes the state of a system, picks an action, collects a return, and watches the system move at random to a new state, forever. Blackwell treated the discounted case, with a bounded return and a discount factor below one (Blackwell 1965), and the positive bounded case. Strauch's paper (Strauch 1966) studies the third case, the negative case: the return is non-positive and there is no discounting. Equivalently, a non-negative cost is minimized over an infinite horizon. This is the setting of stochastic shortest-path, optimal stopping with costs, and many inventory and search problems in which the total cost may be infinite.

In the negative case two standard tools of the discounted theory break down. An optimal policy need not exist, and the natural algorithm, value iteration from the zero function, need not converge to the optimal return. Strauch's §9 gives a condition on the action sets, essential finiteness, under which both are restored. The introduction (p. 872) summarizes the finite case: "In the negative case, … if A is finite, there is an optimal policy (Section 9)." In the later terminology of Bertsekas and Shreve (1978), Strauch's negative case is their positive-cost model, for which value iteration from zero is known to require such finiteness or compactness conditions.

Setting

The state space $S$ and the action space $A$ are non-empty Borel sets. The law of motion $q(\cdot\mid s,a)$ is a probability measure on $S$ depending measurably on $(s,a)$. The return $r(s,a,t)$, collected when action $a$ is taken in state $s$ and the next state is $t$, is a Borel function with $-\infty<r\le 0$ and $\int r(s,a,t)\,dq(t\mid s,a)>-\infty$ for every $(s,a)$.

A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the $n$th action at random, with a law depending measurably on the whole history $(s_1,a_1,\dots,s_n)$. A Markov policy $(f_1,f_2,\dots)$ is a sequence of measurable maps $S\to A$; the stationary policy $f^{(\infty)}$ uses one map $f$ at every stage. The expected return from the initial state $s$ is

$$I(\pi)(s)=\sum_{n=1}^\infty \pi_1q\cdots\pi_nq\,r\,(s)\in[-\infty,0],$$

the sum of the expected stage returns. The optimal return is $v^*=\sup_\pi I(\pi)$, over all policies, and $\pi^*$ is optimal if $I(\pi^*)\ge v^*$ at every state.

For a measurable $f:S\to A$ and a non-positive Borel $u$, the operator $T$ of $f$ is

$$Tu(s)=\int\big[r(s,f(s),t)+u(t)\big]\,dq(t\mid s,f(s)),$$

and the operator of a Markov policy $\pi^*=(f_1,f_2,\dots)$ is $Uu=\sup_nT_nu$, with $T_n$ the operator of $f_n$. Value iteration is the sequence $U^n0$.

Actions $a$ and $b$ are equivalent at $s$ if $r(s,a,\cdot)=r(s,b,\cdot)$ and $q(\cdot\mid s,a)=q(\cdot\mid s,b)$. $A$ is essentially finite by $\pi^*$ if there is a partition of $S$ into Borel sets $S_1,S_2,\dots$ such that for $s\in S_n$ every action is equivalent at $s$ to one of $f_1(s),\dots,f_n(s)$. A finite $A$ is essentially finite by any Markov policy whose first $|A|$ rules are the constant rules.

Formalization targets

Goal: Theorem 9.1 (N), p. 887

If $A$ is essentially finite by $\pi^*$ and $U$ is the operator of $\pi^*$, then

$$U^n0(s)\xrightarrow[n\to\infty]{}v^*(s)=\sup_\pi I(\pi)(s)\quad\text{for every } s,\qquad\text{and}\qquad \exists f:\ I(f^{(\infty)})\ge v^*.$$

Both parts are kept together, as printed. The goal fixes no constants and no rate.

Milestones

1. Lemma 6.1 (N), p. 880. For every Markov policy $\hat\pi$ with operator $U$, $\lim_nU^n0$ exists and

$$\lim_nU^n0\ \ge\ \sup_{\pi\in G(\hat\pi)}I(\pi)\ \ge\ \sup_{f^{(\infty)}\in G(\hat\pi)}I(f^{(\infty)}),$$

where $G(\hat\pi)$ is the set of $\hat\pi$-generated policies (each rule equal to $f_n$ on the $n$th piece of a Borel partition). 2. Proof of Theorem 8.4, p. 887. $\sup_\pi I(\pi)=\sup\{I(\hat\pi)\mid\hat\pi\text{ Markov}\}$ pointwise. 3. Proof of Theorem 9.1, p. 887, first step. Under essential finiteness, $U^n0$ is non-increasing and $I(\pi)\le v^\infty:=\lim_nU^n0$ for every policy $\pi$. 4. Proof of Theorem 9.1, p. 887, second step. Under essential finiteness, $Uv^\infty\ge v^\infty$.

Inside the proof of Theorem 9.1 the paper writes $v^*$ for $\lim_nU^n0$; the mission writes $v^\infty$ for it and reserves $v^*$ for $\sup_\pi I(\pi)$.

An optional extra item states the introduction's special case: if $A$ is finite, an optimal policy exists (§1, p. 872).

Significance

Theorem 9.1 gives, in the negative case, both a computational and an existential conclusion. Value iteration from zero computes the optimal return, so the optimal total cost of an essentially finite problem is the limit of the optimal finite-horizon costs. An optimal policy exists and can be taken stationary, so the controller needs only a single measurable decision rule. Without a hypothesis of this kind neither conclusion holds in the negative case; Example 6.1 of the paper exhibits a problem where the limit of value iteration, the best return among generated policies, and the best stationary return all differ.

The result is proved in the paper. What the mission adds is a machine-checked statement and, eventually, proof of it on general Borel spaces, with the return allowed to equal $-\infty$. Blackwell's discounted analogue already has a published statement on Prove2Me (DiscountedDP.Stationary.theorem7b_optimal_stationary), in a bounded-return model; the negative case is a separate statement in a separate model. No formalization of the negative case is known to exist.

Difficulty

The discounted proof rests on the contraction property of $U$ in the supremum norm, and in the negative case that property is missing: returns are unbounded below and there is no discount. The obvious argument, "$U^n0$ decreases to some $v^\infty$, and $v^\infty$ is the optimal return because finite-horizon play approximates infinite play", fails at the second step. The finite-horizon optimum can stay strictly above the infinite-horizon optimum, because a policy can postpone a cost beyond every fixed horizon; this is exactly the gap Example 6.1 exhibits. Closing it needs the essential finiteness of the actions together with the reduction of arbitrary policies to Markov ones (milestone 2), whose proof in the paper passes through the measurable-selection results of §7–§8.

Formalization scope

• The state and action spaces are non-empty standard Borel types; "Baire function" means Borel measurable.
• The law of motion is a Markov kernel; the return is real-valued, non-positive, Borel, and integrable against every $q(\cdot\mid s,a)$ (the paper's $r>-\infty$ and $qr>-\infty$).
• Returns live in EReal and are computed as minus the lintegral of the loss $-r$, which keeps the value $-\infty$. $I(\pi)$ is the sum over stages of the expected stage loss, which equals the paper's integral over futures by monotone convergence.
• $v^*$ is the supremum over every randomized history-dependent plan, never over Markov or stationary policies only, and it is not defined through $U$. Defining $v^*$ as $\lim_nU^n0$ would make part (a) of the goal hold by unfolding; this trivializing formalization is excluded.
• Optimality is against every plan, at every state.
• $U$ is the operator of the fixed $\pi^*$ of the hypothesis, applied from the zero function; convergence is pointwise in EReal.
• Stages are numbered from $0$ in Lean. Essential finiteness is zero-based: Lean's piece $n$ is the paper's $S_{n+1}$ and allows the rules $f_1,\dots,f_{n+1}$. The pieces are measurable, pairwise disjoint and cover $S$; empty pieces are allowed, as in the paper.
• Explicit choices: the existence of $\lim U^n0$ in Lemma 6.1 is part of the statement; the limit in the steps of Theorem 9.1 is written as the infimum of the non-increasing sequence.
• Only the negative case is formalized; the paper's discounted and positive parts are not.

Policies, Markov policies, stationary policies and $\hat\pi$-generated rules come from the published definitions DiscountedDP.Stationary.Model, .Return and .Operators; the negative model is defined locally because the published Problem has a bounded return and a discount factor below one. A complete development needs the Ionescu-Tulcea construction of the history laws (already encoded as iterated composition products), monotone convergence for kernels, the measurable-selection step behind milestone 2, and a pigeonhole argument over the essentially finite action classes. The model and the Markov-reduction milestone are reusable by the other missions of this series. Proofs of any milestone, and alternative routes to milestone 2, are welcome.

Selected references

• R. E. Strauch, Negative Dynamic Programming, The Annals of Mathematical Statistics 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, Discounted Dynamic Programming, The Annals of Mathematical Statistics 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. http://web.mit.edu/dimitrib/www/soc.html

Why market entry and exit matter

Adding a firm changes the offers available to workers; removing a worker changes the pool from which firms hire. In markets with salary bargaining, those changes can alter both assignments and pay. Kelso and Crawford asked whether the direction of the change can nevertheless be predicted at the outcome selected by their salary-adjustment process. Their 1982 paper studies firms that may hire groups of workers whose joint product need not be the sum of individual products. Theorem 5 gives two comparative-statics conclusions for that setting: a new firm leaves each worker at least as well off, and retaining a worker leaves each firm at least as well off.

The result follows the paper's finite-termination and firm-optimality results for the salary-adjustment process. Its comparison is specific to the process equilibrium under the no-ties conditions of Section 5; the paper does not claim that every core allocation moves in the same direction. This mission is the fifth of seven on the paper. Mission 1 concerns termination and the discrete core, mission 2 the continuous strict core, mission 3 a one-sided market, mission 4 firm optimality, mission 6 returns to workers and gross substitutes, and mission 7 the example without a core. The statements here are drafted independently of the other missions' unpublished declarations. None of this paper's statements was previously available on Prove2Me when the series was planned.

The market and the adjustment process

A market has a finite set $W$ of workers and a finite, nonempty set $F$ of firms. Worker $i$'s utility from employment at firm $j$ for salary $s$ is $u_i(j;s)$. Firm $j$ produces $y^j(C)$ from a set $C\subseteq W$ and earns profit $\pi^j(C;s)=y^j(C)-\sum_{i\in C}s_i$. Workers care about their own firm and salary; the firm's product may depend on the whole set it hires. Every worker–firm pair has a starting salary $\sigma_{ij}$, and permitted salaries increase by a common unit $\delta>0$: $\sigma_{ij}+k\delta$ for $k\in\mathbb N$.

Each round of the salary-adjustment process records permitted salaries, offers from firms, and one tentatively accepted offer for each worker who receives any. Firms choose profit-maximizing sets of workers at current permitted salaries and repeat offers that were not rejected. A worker keeps a favorite available offer. A rejected worker–firm offer causes that pair's permitted salary to rise by $\delta$ next round. The process stops when no offer is rejected. An allocation assigns each worker one firm and a salary at that firm; an outcome is the allocation read from a stopping round. The paper calls this a process equilibrium.

An allocation is in the discrete strict core when each worker's salary is permitted and meets the starting salary, each firm's profit is nonnegative, and no firm together with a set of workers can make every participant weakly better off and at least one strictly better off using permitted salaries. The weaker discrete core excludes coalitions that make everyone strictly better off. The paper assumes workers' utilities are continuous and strictly increasing in salary; marginal product (MP) makes hiring an additional worker at the starting salary weakly profitable; no free lunch (NFL) sets the product of the empty set to zero; and gross substitutes (GS) lets a firm keep workers whose salaries did not rise when other workers' salaries increase. Section 5 adds no-ties conditions (NTW) for workers and (NTF) for firms relative to discrete-core allocations. These assumptions and their domains come from Sections 2 and 5.

Formalization targets

The preliminary target is the paper's Corollary to Theorem 4: under these assumptions, all legal runs that stop have the same outcome. A second target is the new-firm-on-the-block process claim stated in the proof of Theorem 5: starting from the original market's final salaries, its outcome is a firm-optimal discrete strict core allocation of the augmented market.

The goal is Theorem 5. Write $A$, $A^+$ and $A^-$ for stopping outcomes in the original market, the market augmented by one firm, and the market without one named worker. The two conclusions are

$$\forall i\in W,\quad u_i(A)\leq u_i(A^+),\qquad \forall j\in F,\quad \pi^j(A^-)\leq\pi^j(A).$$

The first comparison concerns every original worker's utility. The second concerns every original firm's profit. The augmented market retains the original firms' technologies, utilities and starting salaries, and the diminished market restricts those data to workers other than the removed one. All three markets use the same $\delta$ and satisfy the conditions of Theorem 4.

What the result establishes

The theorem gives a direction for the effects of entry and worker exit even though assignments and salaries may both change and a firm's product may depend on its entire workforce. The comparisons are individual: every worker is covered by the entry conclusion and every firm by the exit conclusion. Process uniqueness makes these comparisons well-defined despite the choices of favorite sets and favorite offers that a legal run may make.

The mathematical claims were proved in the 1982 paper; the Lean statements in this mission are open proof obligations. The formal development would give reusable finite-market definitions of demand, gross substitutes, core blocking, and an explicit adjustment run. It would also make precise how outcomes in markets with different agent sets are compared. The Corollary and the new-firm process result are separate proof targets. Completing them would support the goal while keeping the paper's two comparative-statics conclusions together.

The main difficulty

Firm entry changes which firm can make the best offer, and worker exit changes which subsets of workers a firm can hire profitably. A direct pointwise comparison of old and new assignments has no fixed correspondence: a worker may switch firms and a firm may hire a different group. Comparing arbitrary strict-core allocations is also insufficient, because Theorem 5 concerns the specific outcome chosen by the adjustment process. The formal proof must account for all legal tie choices and show that the identified stopping outcomes have the required utility and profit order. The paper's proof uses two modified processes; its take-my-marbles process raises the removed worker's salary to a value that need not belong to the discrete salary grid on which (GS) was assumed. This is a genuine modeling boundary for that intermediate statement.

Formalization scope

Workers and firms are finite Lean types, with at least one firm. Salaries, utilities and products are real-valued; $\delta$ is positive. An allocation assigns every worker to a firm, as the paper's $f:\{1,\ldots,m\}\to\{1,\ldots,n\}$ does. Option F represents firm entry: some j is an original firm and none is the entrant. The diminished worker set is the subtype of workers unequal to the removed worker. Gross substitutes is imposed only on the grid vectors each market permits, and (NTW) and (NTF) quantify over discrete-core allocations. Each theorem's assumptions explicitly include utility regularity, MP, NFL, GS, NTW and NTF wherever the paper says “the conditions of Theorem 4.” Section 5 allows starting salaries to vary independently of unemployment utility, so the reservation-salary equation from Section 2 is not imposed.

“The equilibrium” is represented by the outcome at any stopping round of any legal run; the Corollary states why this does not depend on those choices. “Converges in finite time” in the new-firm milestone means that each legal continuation has some stopping round. NFB's initial offers are fixed to the old firms' final offers and an offer from the new firm to every worker, a reading of the first round that NFB1 leaves implicit. The take-my-marbles convergence claim is not drafted because its off-grid starting salary requires a separate convention or a stronger GS assumption. These commitments exclude a vacuous market condition, a continuous-price substitution for the discrete theorem, and a comparison of unrelated markets. Contributions that establish the Corollary, the NFB claim, or the three-market comparison under these definitions are welcome; lemmas about demand and core allocation can be reused across the series.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.

Motivation

A backward stochastic differential equation (BSDE) prescribes the terminal value of an adapted process instead of its initial value. Pardoux and Peng (1990) proved existence and uniqueness for Lipschitz coefficients, and BSDEs have since become a standard tool in stochastic control, mathematical finance and the probabilistic treatment of semilinear PDEs. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE, whose solution is constrained to stay above a given obstacle process. Reflected BSDEs describe the price of American options in nonlinear markets (El Karoui, Pardoux and Quenez 1997), Dynkin games (Cvitanić and Karatzas 1996), and obstacle problems for parabolic PDEs.

In §7 of the 1997 paper the coefficient is assumed concave. Then the solution of the reflected BSDE is the value of a game: one player chooses a stopping time, the other chooses a control that sets the discount rate and the change of measure, and the value does not depend on which player moves first. This mission formalizes that statement (Theorem 7.2) and the results its proof uses.

Setting

Let $(\Omega,\mathcal F,P)$ carry a $d$-dimensional standard Brownian motion $B$, fix a horizon $T\ge0$, and let $\mathcal F_t$ be the natural filtration of $B$ augmented by the $P$-null sets. Write $\mathbb L^2$ for the square-integrable $\mathcal F_T$-measurable random variables, $\mathbb H^2$ for the progressively measurable processes $\varphi$ with $E\int_0^T|\varphi_t|^2dt<\infty$, and $\mathcal S^2$ for those with $E\sup_{t\le T}|\varphi_t|^2<\infty$.

The data are a terminal value $\xi\in\mathbb L^2$; a coefficient $f(\omega,t,y,z)$, $y\in\mathbb R$, $z\in\mathbb R^d$, with $f(\cdot,y,z)\in\mathbb H^2$ for every $(y,z)$ and Lipschitz in $(y,z)$ with a constant $K$; and a continuous progressively measurable obstacle $S$ with $E\sup_t(S_t^+)^2<\infty$ and $S_T\le\xi$. A solution of the reflected BSDE is a triple $(Y,Z,K)$ of progressively measurable processes with $Z\in\mathbb H^2$, $Y\in\mathcal S^2$, $K_T\in\mathbb L^2$, and

$$Y_t=\xi+\int_t^Tf(s,Y_s,Z_s)\,ds+K_T-K_t-\int_t^T(Z_s,dB_s),\qquad Y_t\ge S_t,$$

where $K$ is continuous, nondecreasing, $K_0=0$ and $\int_0^T(Y_t-S_t)\,dK_t=0$: $K$ pushes $Y$ up only when $Y$ touches $S$.

For $t\le T$, $\mathcal T_t$ is the set of stopping times $v$ with $t\le v\le T$. When $f(\omega,t,\cdot,\cdot)$ is concave, its conjugate is

$$F(\omega,t,\beta,\gamma)=\sup_{(y,z)}\big[f(\omega,t,y,z)-\beta y-\langle\gamma,z\rangle\big]\in(-\infty,+\infty].$$

The admissible controls $\mathcal A$ are the bounded progressively measurable $(\beta_t,\gamma_t)$ with $E\int_0^TF(t,\beta_t,\gamma_t)^2dt<\infty$. Each $(\beta,\gamma)\in\mathcal A$ gives the affine coefficient $f^{\beta,\gamma}(t,y,z)=F(t,\beta_t,\gamma_t)+\beta_ty+\langle\gamma_t,z\rangle$, its reflected BSDE solution $Y^{\beta,\gamma}$, the process $\Gamma^{\beta,\gamma}_{t,s}$ solving $d\Gamma_{t,s}=\Gamma_{t,s}(\beta_sds+(\gamma_s,dB_s))$, $\Gamma_{t,t}=1$, and the payoff

$$\Phi(t,v,\beta,\gamma)=\Gamma^{\beta,\gamma}_{t,v}\big[S_v1_{\{v<T\}}+\xi1_{\{v=T\}}\big]+\int_t^v\Gamma^{\beta,\gamma}_{t,s}F(s,\beta_s,\gamma_s)\,ds.$$

Formalization targets

Goal: Theorem 7.2 (p. 725)

For every $t\in[0,T]$ and $(\beta,\gamma)\in\mathcal A$, $Y^{\beta,\gamma}_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Phi(t,v,\beta,\gamma)\mid\mathcal F_t]$, and

$$Y_t=\operatorname*{ess\,inf}_{\mathcal A}Y^{\beta,\gamma}_t=\operatorname*{ess\,inf}_{\mathcal A}\operatorname*{ess\,sup}_{v\in\mathcal T_t}E[\Phi\mid\mathcal F_t]=\operatorname*{ess\,sup}_{v\in\mathcal T_t}\operatorname*{ess\,inf}_{\mathcal A}E[\Phi\mid\mathcal F_t].$$

The last equality, the interchange of the two essential extrema, is the minimax content.

Milestones

1. Theorem 4.1 (p. 712): comparison. If $\xi\le\xi'$, $f\le f'$ and $S\le S'$, and one of $f,f'$ is Lipschitz, then $Y\le Y'$.
2. §7 conjugacy (p. 724): a concave Lipschitz $f$ equals $\min_{(\beta,\gamma)\in D^F_t}\{F(t,\beta,\gamma)+\beta y+\langle\gamma,z\rangle\}$, the minimum is attained, and the domain $D^F_t$ of $F$ is a.s. bounded.
3. Proposition 7.1 (p. 724): for an affine coefficient $\delta_t+\beta_ty+\langle\gamma_t,z\rangle$, $\Gamma_tY_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Gamma_v\xi1_{\{v=T\}}+\Gamma_vS_v1_{\{v<T\}}+\int_t^v\Gamma_s\delta_sds\mid\mathcal F_t]$.
4. §7 optimal control (p. 725): some $(\beta^*,\gamma^*)\in\mathcal A$ satisfies $f(t,Y_t,Z_t)=F(t,\beta^*_t,\gamma^*_t)+\beta^*_tY_t+\langle\gamma^*_t,Z_t\rangle$ $dt\times dP$-a.e., so $(Y,Z,K)$ solves the reflected BSDE with coefficient $f^{\beta^*,\gamma^*}$.

Significance

Theorem 7.2 identifies the solution of a nonlinear reflected BSDE with the value of a zero-sum game between a stopper and a controller. In finance, with $f$ the driver of a pricing rule under constraints or ambiguity, it says that the nonlinear price of an American claim is the worst case, over a family of discount rates and changes of measure, of linear American prices; and the stopper may announce the stopping rule first without changing the value. Concave drivers include the hedging equations with different borrowing and lending rates. The representation reduces questions about the nonlinear equation to a family of linear ones, which is how monotonicity, convexity and stability properties of nonlinear American prices are usually derived.

All four results and the goal are proved in the paper, with references to standard convex analysis and a measurable section theorem for two steps. None of them has a machine-checked proof. Mathlib has Brownian motion, filtrations, stopping times and conditional expectation, but no stochastic integral; the mission uses the Itô integral of the published Peng1990.SMP.Stochastic layer. A formal proof would give, beyond the theorem, a reusable comparison theorem for reflected BSDEs, a Snell-envelope representation for linear reflected BSDEs, and a measurable selection of supergradients along a process.

Difficulty

The inequality $Y_t\le Y^{\beta,\gamma}_t$ for each control is a direct consequence of comparison, since $f\le f^{\beta,\gamma}$. The difficulty is the reverse inequality, which needs a single admissible control that attains the conjugate representation along the solution $(Y,Z)$ for almost every $(t,\omega)$. Choosing a supergradient pointwise is easy; choosing it progressively measurable, bounded, and with $F(t,\beta^*_t,\gamma^*_t)$ square integrable is a measurable-selection problem. The interchange of ess inf and ess sup does not follow from a general minimax theorem: the family $\mathcal A$ is not compact and the payoff is not convex–concave in any usable topology. It uses a specific stopping time, the first time $Y$ touches $S$, together with comparison on the random interval before it. Proposition 7.1 requires the linear change of variables $\Gamma_tY_t$, whose transformed equation lacks the square integrability of the original one, so the Snell-envelope argument has to be rerun with weaker moments.

Formalization scope

• Time and spaces. Time is $\mathbb R_{\ge0}$ with $T:\mathbb R_{\ge0}$, and time integrals run over $[t,T]\subset\mathbb R$. $\mathbb H^2$ is the published L2F (progressive in place of predictable); $\mathcal S^2$ and the obstacle condition are lower Lebesgue integrals in $[0,\infty]$.
• Filtration. The natural filtration of $B$ joined with the σ-algebra of $P$-null sets.
• Norms. $|z|$ is the Euclidean norm and $\langle\gamma,z\rangle=\sum_j\gamma_jz_j$.
• Lipschitz condition. Read as: almost surely, for all $t\le T$ and all $y,y',z,z'$.
• Solutions. Solutions are in the square-integrable class (v)–(viii). $Y$ has continuous paths. Equation (vi) holds for each $t$ almost surely, and $Y\ge S$ holds almost surely for all $t$. $K$ is continuous and nondecreasing on every path. $\int_0^T(Y-S)\,dK=0$ is taken against the Lebesgue–Stieltjes measure of the path of $K$.
• Extended values. $F$ takes values in the extended reals. $F^2$ in the definition of $\mathcal A$ is taken in $[0,\infty]$, so admissibility forces $F<\infty$ almost everywhere along the control.
• Stochastic exponential. $\Gamma^{\beta,\gamma}_{t,s}$ is the Doléans-Dade exponential, built from Itô integrals of $\gamma$ with continuous paths.
• Essential extrema. They are predicates relative to $\mathcal F_t$, real valued: the essential infimum is the published MultiperiodRisk.Bellman.EssInf, and the essential supremum is its mirror image.
• Added hypothesis. $S\in\mathcal S^2$ is assumed wherever a conditional expectation of the payoff appears (Remark 3.2: without loss of generality). Otherwise the payoff may fail to be integrable, and Lean's conditional expectation of a non-integrable function is $0$.
• Hypothesized families. The solutions $Y^{\beta,\gamma}$ and the Itô integrals defining $\Gamma^{\beta,\gamma}$ are hypotheses indexed by $\mathcal A$. They exist by the existence theorem of the first mission of this series and by continuity of Itô integrals.

Several formalizations of the goal would make it trivial, and each is ruled out. The conjugate is not a real-valued supremum, which takes a junk value when unbounded. The essential infimum over $\mathcal A$ is not a pointwise infimum. The interchange of ess inf and ess sup is not dropped. The coefficient is a random field $f(\omega,t,y,z)$, not a deterministic or Markovian one.

The closing gloss of Theorem 7.2, that the triple $(\beta^*,\gamma^*,D_t)$ is optimal, is not stated separately; milestone 4 is its control half. Contributions are welcome on a continuous version of the Itô integral, Itô's formula for products with $\Gamma$, the Snell envelope in continuous time, and measurable selection of supergradients; all of these are reusable beyond this mission.

Selected references

• N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng, M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, Ann. Probab. 25(2), 1997, 702–737. https://doi.org/10.1214/aop/1024404416
• É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14, 1990, 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
• N. El Karoui, S. Peng, M.-C. Quenez, Backward stochastic differential equations in finance, Math. Finance 7(1), 1997, 1–71. https://doi.org/10.1111/1467-9965.00022
• J. Cvitanić, I. Karatzas, Backward stochastic differential equations with reflection and Dynkin games, Ann. Probab. 24(4), 1996, 2024–2056. https://doi.org/10.1214/aop/1041903216
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990, 966–979. https://doi.org/10.1137/0328054

Motivation

A steady-state simulation produces a single long output path $Y=\{Y(t):t\ge0\}$, and the quantity of interest is its long-run mean $\mu$. The central difficulty of simulation output analysis is that the observations are correlated, so the classical confidence interval $\bar Y_n(1)\pm z\,\hat\sigma/\sqrt n$ needs a consistent estimate of the time-average variance constant $\sigma^2$, which is hard to obtain. The method of standardized time series (STS), introduced by Schruben (1983) and put on a general footing by Glynn and Iglehart (Math. Oper. Res. 15 (1990)), avoids estimating $\sigma$: it divides the centred sample mean by a functional $g$ of the whole sample path that scales like $\sigma$, so that $\sigma$ cancels in the limit. Batch means, the area estimator and other procedures used in simulation software are all instances of this construction.

Cancelling $\sigma$ has a price. Glynn and Iglehart show (their Corollary 4.16) that every STS interval has asymptotic expected length at least $2\sigma\Phi^{-1}(1-\delta/2)/\sqrt n$, the length of the interval that knows $\sigma$, and (4.23) that this bound is the infimum over all admissible $g$. This mission formalizes the next question the paper asks and answers: is the infimum attained? Proposition 4.26 says it is not, and the companion results quantify the residual randomness of the interval length.

Setting

$C[0,1]$ is the space of continuous real functions on $[0,1]$ with the uniform metric $\rho(x,y)=\sup_t|x(t)-y(t)|$ and its Borel $\sigma$-algebra; $k(t)=t$, and $C_0[0,1]=\{x\in C[0,1]:x(0)=0\}$. For $g:C[0,1]\to\mathbb R$, $D(g)$ is the set of points at which $g$ is not continuous. On a probability space $(\Omega,\mathcal F,P)$, $B$ is a standard Brownian motion, viewed as a random element of $C[0,1]$.

Assumption (2.1). There are finite constants $\mu$ and $\sigma>0$ such that $X_n\Rightarrow\sigma B$ in $C[0,1]$, where

$$X_n(t)=n^{1/2}\big(\bar Y_n(t)-\mu t\big),\qquad \bar Y_n(t)=\frac1n\int_0^{nt}Y(s)\,ds,\quad 0\le t\le1 .$$

The class $\mathcal M$ (2.3) consists of the measurable $g:C[0,1]\to\mathbb R$ with

1. $g(ax)=a\,g(x)$ for $a>0$;
2. $g(x-\beta k)=g(x)$ for $\beta\in\mathbb R$;
3. $P\{g(B)>0\}=1$;
4. $P\{B\in D(g)\}=0$.

With $H(x)=P\{B(1)/g(B)\le x\}$ and $\alpha,\beta$ chosen so that $H(\beta)-H(\alpha)=1-\delta$, the interval $[\bar Y_n(1)-g(\bar Y_n)\beta,\ \bar Y_n(1)-g(\bar Y_n)\alpha]$ (2.10) is an asymptotic $100(1-\delta)\%$ confidence interval for $\mu$, of width $L_n=g(\bar Y_n)(\beta-\alpha)$.

Formalization targets

Goal: Proposition 4.26

For every $\sigma>0$ there is no $g\in\mathcal M$ such that, for some $\alpha>0$,

$$P\{g(\sigma B)=\alpha\sigma\}=1. \qquad (4.25)$$

By the paper's discussion before (4.25), attaining the lower bound of Corollary 4.16 with some $g\in\mathcal M$ requires (4.25); the goal therefore says that the bound is attained by no $g\in\mathcal M$. The goal is stated in terms of (4.25) and not of the limit (4.24), so it does not depend on the expected-length machinery of Corollary 4.16.

Milestones (the steps of the proof, pp. 13–14)

1. For $|z|<\eta$: $P\{|B(t)-z|<\eta,\ \max_{0\le s\le t}|B(s)|<2\eta\}>0$.
2. (4.27): $P\{\rho(\sigma B,x)<\varepsilon\}>0$ for every $x\in C_0[0,1]$ and $\varepsilon>0$.
3. If the range of $g$ over every $\varepsilon$-neighbourhood of $x$ contains $\{\alpha\sigma:\sigma>0\}$, then $x\in D(g)$.
4. Under (2.3i) and (4.25), $C_0[0,1]\subseteq D(g)$.

Companions

• $g(B)$ is nondegenerate for every $g\in\mathcal M$ (p. 14).
• Proposition 4.32: if $\{g^2(X_n)\}$ is uniformly integrable, then

$$\lim_{n\to\infty}nE(L_n-EL_n)^2=\sigma^2E\big(g(B)-Eg(B)\big)^2(\beta-\alpha)^2>0 .$$

Significance

The result closes the expected-length analysis of STS intervals: the bound $2\sigma\Phi^{-1}(1-\delta/2)$ is the exact infimum over $\mathcal M$ but no single standardization reaches it, so every STS procedure is strictly worse, in expected length, than the interval with known $\sigma$. The companion results explain why: $g(B)$ is never degenerate, so $n^{1/2}L_n$ converges to a nondegenerate random limit and the interval length fluctuates at order $n^{-1/2}$, while intervals built on a consistent estimator of $\sigma$ (the regenerative method, Proposition 4.34) fluctuate only at order $n^{-1}$. This is the quantitative trade-off a practitioner faces when choosing between STS and variance-estimation methods.

The paper's results are proved; none of them is formalized. The mission produces machine-checked versions of a support property of Wiener measure on $C[0,1]$ (every path started at $0$ is in the support), which is reusable well beyond simulation, and of the deterministic step that turns such a support property into everywhere-discontinuity of a functional.

Difficulty

The goal's statement is elementary, but its proof needs a quantitative fact about Brownian paths: the law of $\sigma B$ charges every uniform ball around every path in $C_0[0,1]$. The natural first attempt, using that $g$ is continuous $P$-almost everywhere and constant almost surely on $\sigma B$, fails without this fact, because almost-sure statements say nothing about any particular path $x$. Mathlib provides Brownian finite-dimensional laws and independent increments, but no small-ball or support estimate for Brownian motion in the uniform metric, so (4.27) has to be built from scratch. A second subtlety is that (4.25) is given for one $\sigma$ only; the homogeneity (2.3i) is what upgrades it to all scales, and that upgrade is what makes the range of $g$ near $x$ unbounded.

Proposition 4.32 needs, in addition, the passage from weak convergence of $g(X_n)$ to convergence of second moments under uniform integrability, in the space $C[0,1]$.

Formalization scope

• $C[0,1]$ is C(unitInterval, ℝ) with its sup norm; $\rho$ is dist. Mathlib has no measurable structure on it at this commit, so the Borel $\sigma$-algebra is declared in the mission's definitions file.
• $B$ is a measurable map $\Omega\to C[0,1]$ whose coordinates agree, for every $\omega$, with a process satisfying Mathlib's IsBrownianReal. "Measurable" in $\mathcal M$ means Borel measurable.
• $D(g)$ is the set where $g$ is not continuous; $P\{B\in D(g)\}$ is the outer measure of the preimage, so no measurability of $D(g)$ is assumed.
• Assumption (2.1) is a structure: joint measurability of $Y$, local integrability of its paths (the implicit condition that makes $\bar Y_n$ defined), $\bar Y_n$ pinned pointwise by its integral formula, $\sigma>0$, and convergence in distribution of $X_n$ to $\sigma B$. The index $n$ ranges over $\mathbb N$.
• $P\{\cdot\}=1$ is "almost surely". $0<\delta<1$ is added where the confidence level appears.
• The paper writes "$D(g)=C_0[0,1]$" at the end of the proof of Proposition 4.26; its argument proves only $C_0[0,1]\subseteq D(g)$, which is what milestone 4 states.
• Proposition 4.32 uses Bochner integrals; its uniform-integrability hypothesis makes every integral there finite.

The goal is a negation of an existence statement, so it would be trivially true if $\mathcal M$ were empty or if the Brownian hypothesis were unsatisfiable. Neither holds: $\mathcal M$ contains the batch-means functionals of the paper's Example 3.1 (p. 5), and the goal assumes nothing about small balls, (4.27) or continuity of $g$. Those appear only as milestones.

Contributions welcome: the support theorem for Brownian motion in $C[0,1]$ (milestones 1–2), any of the deterministic steps, and the moment-convergence argument of Proposition 4.32.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. https://doi.org/10.1287/moor.15.1.1
• L. Schruben, Confidence interval estimation using standardized time series, Operations Research 31(6):1090–1108, 1983. https://doi.org/10.1287/opre.31.6.1090
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968. https://doi.org/10.1002/9780470316962