Operations Research

Motivation

Random equations of the form $R \overset{\mathcal L}{=} \Psi(R)$, with $\Psi$ a random function independent of $R$, describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations $R = Q + MR$, and the stationary workload of certain queueing and storage models. When $\Psi(t)$ acts like multiplication by a random variable $M$ for large $|t|$, and $\mathbf E|M|^\kappa = 1$ for some $\kappa > 0$, the solution has power-law tails: $P(R > t) \sim C_+ t^{-\kappa}$. This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.

A tail asymptotic alone says nothing about how fast $t^\kappa P(R > t)$ approaches $C_+$. For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of $1 - \hat\eta$, where $\eta$ is a tilted law of $\log M$, plus a remainder $O(t^{-\beta/2})$.

Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space carrying independent real random variables $M \ge 0$ and $R$. Fix $\kappa > 0$ with $\mathbf E M^\kappa = 1$ (the Cramér condition, (2.3)) and $\beta > 0$ with $\mathbf E M^{\kappa+\beta} < \infty$ (3.3).

The tilted law of $M$ is the probability measure $\eta(dx) = e^{\kappa x} P(\log M \in dx)$ on $\mathbb R$, computed on $\{M > 0\}$. Its transforms are $\tilde\eta(\beta) = \int e^{\beta t}\eta(dt)$ for real $\beta$ and $\hat\eta(\theta) = \int e^{i\theta t}\eta(dt)$ for complex $\theta$; for a function $f$, $\hat f(\theta) = \int e^{i\theta t} f(t)\,dt$. Convolution powers are $\eta^{(0)} = \delta_0$, $\eta^{(n+1)} = \eta^{(n)} * \eta$, and the renewal measure is $\nu = \sum_{n \ge 0}\eta^{(n)}$. A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of $\log M$ given $M \ne 0$.

Set $m = \mathbf E M^\kappa \log M$ and

$$g_1(t) = e^{\kappa t}\big(P(R > e^t) - P(MR > e^t)\big), \qquad C_+ = \frac1m\int_0^\infty \big(P(R > t) - P(MR > t)\big) t^{\kappa - 1}\,dt,$$

with $g_{-1}$ and $C_-$ defined the same way for the lower tail. The strip is $D = \{\theta : -\beta < \Im\theta < 0\}$, and $\mathscr C$ denotes a positively oriented closed contour in $D$ enclosing every zero of $1 - \hat\eta$ in $D$.

Formalization targets

Goal: Theorem 3.2

If, in addition, $\eta^{(n_0)} = (1 - \delta)\varphi_0 + \delta\varphi_1$ for some $n_0$, with $\delta \in [0, 1)$, $\varphi_0$ absolutely continuous and $\delta\tilde\varphi_1(\beta) < 1$, and $\hat\eta \ne 1$ on $\Im\theta = -\beta$, then $\int_0^\infty |P(R > t) - P(MR > t)|\,t^{\kappa+\beta-1}dt < \infty$ implies

$$t^\kappa P(R > t) = C_+ - \frac1{2\pi}\,\Re\oint_{\mathscr C} e^{-i\theta\log t}\,\frac{\hat g_1(\theta)}{1 - \hat\eta(\theta)}\,d\theta + O(t^{-\beta/2}), \qquad t \to \infty,$$

with the analogous statement for $P(R < -t)$; and if $R \overset{\mathcal L}{=} \Psi(R)$ with $R$ independent of $(M, \Psi)$, the integrability hypotheses may be replaced by $\mathbf E|(\Psi(R)^\pm)^{\kappa+\beta} - ((MR)^\pm)^{\kappa+\beta}| < \infty$. The theorem also asserts that $\eta$ is a spread-out probability measure.

Milestones

1. Lemma 9.5: Stone's inversion formula for the density of $\sum_n \chi * \mu^{(n)}$.
2. Theorem 3.1: the renewal measure splits as $\nu = \nu_0 + \nu_1$, $\nu_1$ finite with $\tilde\nu_1(\beta) < \infty$, $\nu_0$ with continuous bounded density

$$p(t) = \frac1m - \frac1{2\pi}\oint_{\mathscr C} e^{-i\theta t}\frac{d\theta}{1 - \hat\eta(\theta)} + o(e^{-\beta t}).$$

3. (9.23) and (9.24): the smoothed identity and the smoothed rate $K * \Re r_1(t) = o(e^{-\beta t})$ for the kernel $K(t) = be^{-bt}\mathbf 1_{t>0}$.
4. Theorem 9.6: the Beurling–Ganelius Tauberian remainder theorem.

Significance

Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form $(\log t)^{j-1}t^{\Im\theta_l}$ times oscillating factors, one family for each zero $\theta_l$ of $1 - \hat\eta$ with $0 < -\Im\theta_l \le \beta/2$, and their form does not depend on the unknown law of $R$. It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.

The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.

Difficulty

The first-order theorem follows from the key renewal theorem applied to $r(t) = e^{\kappa t}P(R > e^t)$. That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields $e^{\beta t}g_1 \in L^1$ but not $e^{\beta t}g_1(t) = o(1)$, so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of $r$, where Stone's decomposition with the contour expansion of the renewal density gives an $o(e^{-\beta t})$ remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for $r$ and for the contour term, and costs half the exponent. The contour expansion itself requires showing that $1 - \hat\eta$ has finitely many zeros in the strip and handling their orders through residues.

Formalization scope

All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps $\Omega \to \mathbb R$ on a probability space; $M \ge 0$ almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as $\mathbf E M^{\kappa+\beta}$ and $\tilde\mu(\beta)$ are lower Lebesgue integrals in $[0, \infty]$. The transforms $\hat\mu$ and $\hat f$ are Bochner integrals at complex arguments with the $+i$ sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.

The contour. A contour $\mathscr C$ is the positively oriented boundary of an axis-parallel rectangle whose closure lies in $D$ and whose interior contains every zero of $1 - \hat\eta$ in $D$; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.

The variable in (3.8) and (3.10). The paper prints $e^{-i\theta t}$ in the contour term, but its proof establishes the expansion in the logarithmic variable $s = \log t$. The targets are stated with $e^{-i\theta\log t}$, which is what the proof gives. With the printed $e^{-i\theta t}$ the contour term would decay exponentially and the statement would claim $t^\kappa P(R > t) = C_+ + O(t^{-\beta/2})$, which is not what is proved. Hypothesis (3.7) is printed with $P(R > -t)$ and is read with $P(R > t)$.

Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of $1 - \hat\eta$ in $D$; and the contour must enclose all zeros in the strip, not a chosen subset.

Theorem 9.6 is stated for a complex-valued kernel and a finite strip width $a$; the application with $a = \infty$ follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of $\chi$ has compact support, which the proof uses and the application provides.

Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.

Selected references

• C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Ann. Appl. Probab. 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
• H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Math. 131:207–248, 1973. https://doi.org/10.1007/BF02392040
• C. Stone, On absolutely continuous components and renewal theory, Ann. Math. Statist. 37(1):271–275, 1966. https://doi.org/10.1214/aoms/1177699617
• T. H. Ganelius, The remainder in Wiener's Tauberian theorem, Acta Univ. Gothoburgensis, Mathematica Gothoburgensia 1, 1962 (cited in Goldie 1991).
• A. K. Grincevičius, One limit distribution for a random walk on the line, Lithuanian Math. J. 15:580–589, 1975 (cited in Goldie 1991).

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

Interior-point methods solve linear programs in polynomially many iterations, but the classical analyses assume something about the instance before the algorithm starts: a known strictly feasible primal–dual pair, a nonempty interior, or a big-$M$ bound on the feasible region of order $2^L$, where $L$ is the bit length of the data. In practice none of this is known in advance, and an infeasible or unbounded instance should be reported rather than assumed away.

Ye, Todd and Mizuno (1994) removed these assumptions. They embed a standard-form linear program and its dual into a single homogeneous and self-dual artificial program (HLP), which always has a known interior starting point, and apply the Mizuno–Todd–Ye predictor–corrector method to it. The resulting algorithm needs no regularity assumption, no big-$M$ parameter, and an $O(\sqrt n L)$ iteration bound, the best known for interior-point methods. Self-dual embeddings of this kind are now the standard initialization in interior-point solvers for linear and conic programs.

Timeline. Karmarkar (1984) gave the first polynomial interior-point method on a homogeneous canonical form. Mizuno, Todd and Ye (1990) introduced the predictor–corrector method with $O(\sqrt nL)$ iterations under a known interior start. Kojima, Mizuno and Yoshise (1993) built a self-dual big-$M$ artificial problem. Ye, Todd and Mizuno (1994) combined homogeneity and self-duality without big $M$, obtaining the result formalized here.

Setting

Given $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, the primal problem is (LP) $\min\{c^Tx : Ax=b,\ x\ge0\}$ and its dual is (LD) $\max\{b^Ty : A^Ty\le c\}$, with dual slacks $s=c-A^Ty$.

Fix $x^0>0$, $s^0>0$, $y^0$ and put $\bar b=b-Ax^0$, $\bar c=c-A^Ty^0-s^0$, $\bar z=c^Tx^0+1-b^Ty^0$. The homogeneous self-dual program (HLP) in the variables $(y,x,\tau,\theta,s,\kappa)$ is

$$\begin{aligned} \min\ & ((x^0)^Ts^0+1)\,\theta\\ \text{s.t. } & Ax-b\tau+\bar b\theta=0,\qquad s=-A^Ty+c\tau-\bar c\theta\ge0,\qquad \kappa=b^Ty-c^Tx+\bar z\theta\ge0,\\ & -\bar b^Ty+\bar c^Tx-\bar z\tau=-(x^0)^Ts^0-1,\qquad x\ge0,\ \tau\ge0 . \end{aligned}$$

Its feasible set is $\mathcal F_h$, and $\mathcal F_h^0$ is the subset with $(x,\tau,s,\kappa)>0$. A strictly self-complementary solution is an optimal solution with $\theta=0$ and $(x+s;\tau+\kappa)>0$. The paper then fixes $y^0=0$, $x^0=s^0=e$, so the objective is $(n+1)\theta$ and $(0,e,1,1,e,1)\in\mathcal F_h^0$.

With $\mu=(x^Ts+\tau\kappa)/(n+1)$, the neighborhood of the central path is $\mathcal N(\beta)=\{z\in\mathcal F_h^0 : \|(Xs;\tau\kappa)-\mu e\|\le\beta\mu\}$ (Euclidean norm). The predictor–corrector algorithm starts at $(0,e,1,1,e,1)$. At even steps it solves a Newton system with centering parameter $\gamma=0$ and moves by the largest step keeping the iterate in $\mathcal N(1/2)$. At odd steps it takes a full Newton step with $\gamma=1$. A termination projection then solves a least-squares problem on the columns where $x_j^k\ge s_j^k$ and produces a candidate exact solution.

Formalization targets

Goal: Corollary 7

For integer data with bit length $L$ and $n\ge1$, there is an absolute constant $C$ and a finite predictor–corrector run that reaches, within

$$k\le C\sqrt n\,L$$

iterations, an iterate whose termination output $u=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ either has $\tau^*>0$ with $x^*/\tau^*$ optimal for (LP) and $(y^*/\tau^*,s^*/\tau^*)$ optimal for (LD), or has $\tau^*=0$ with $c^Tx^*<0$ and (LD) infeasible, or $-b^Ty^*<0$ and (LP) infeasible.

Theorem 6

The same bound, with the conclusion that the termination output, rescaled to the normalization $e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1$, is a strictly self-complementary solution of (HLP).

Milestones

Proposition 1 (self-duality of skew-symmetric programs), Theorem 2 (ii), (iv), (v), Theorem 5 (ii), the two Mizuno–Todd–Ye estimates in the proof of Theorem 6, the predictor-step and corrector-step claims, the termination claim, the integrality and $O(L)$ size of the (HLP) data, and Theorem 3 (i), (ii).

Significance

The result. Corollary 7 gives a single polynomial algorithm that decides the status of an arbitrary linear program. It returns optimal primal and dual solutions when they exist and an infeasibility certificate otherwise. It needs no Phase I, no big-$M$ constant and no interior assumption, and its $O(\sqrt nL)$ iteration count matches the best bound known under those assumptions. Theorem 3 is the bridge: an exact strictly self-complementary solution of (HLP) determines the status of (LP) and (LD).

Formalizing it. The paper's result is proved; no machine-checked proof of it is known. The mission produces a formal account of the self-dual embedding, the central-path neighborhood analysis for (HLP), an exact finite-termination step from an approximate iterate, and the reading of a bit-length complexity bound with explicit quantifier order. The neighborhood estimates and the bit-length machinery are reusable for other interior-point and complexity results.

Difficulty

The per-step estimates are short calculations once the orthogonality $d_x^Td_s+d_\tau d_\kappa=0$ is available. The step that resists is termination. Geometric decrease of the gap reaches $2^{-O(L)}$ in $O(\sqrt nL)$ iterations, but turning such an iterate into an exact strictly self-complementary solution requires a quantitative separation: on $\mathcal N(1/2)$, once the gap is below $2^{-O(L)}$, the comparison $x_j\ge s_j$ must identify the optimal partition and the least-squares projection must land in the positive orthant. That separation bound rests on determinant estimates for integer matrices (Hadamard-type bounds in terms of $L$) and on the strict complementarity of (HLP), neither of which comes from the iteration analysis itself. A second subtlety is that the algorithm is not a function: without a rank assumption the Newton system leaves $d_y$ undetermined.

Formalization scope

• Data for the complexity statements are integer matrices and vectors, cast to $\mathbb R$; all optimization objects are real. $L$ is Schrijver's encoding size, $\sum(1+\lceil\log_2(|v|+1)\rceil)$ over the entries plus the dimensions, so $L\ge1$ whenever $n\ge1$.
• Every $O(\cdot)$ is pinned with an absolute constant chosen before $m$, $n$ and the data: $O(\sqrt nL)$ as $C\sqrt n\,L$, $2^{-O(L)}$ as $2^{-C'L}$, and $O(L)$ as $C\cdot L$. The hypothesis $n\ge1$, implicit in the paper, is explicit.
• The algorithm is a relation on finite runs: any solution of the Newton system may be used, and each predictor step taken before termination must attain the maximum in (13). The conclusion asserts a successful run and its output. Stopping at the successful iterate avoids requiring a later step whose maximum may not exist.
• The termination projection is defined relationally (an output is built from a minimizer) and its existence is part of the conclusion. Theorem 6 is stated for the output rescaled to the normalization (9): the projection imposes only homogeneous constraints, so the unscaled output need not be feasible for (HLP).
• "(LP) has a solution (feasible and bounded)" is read as "(LP) has an optimal solution". "An indication that (LP) or (LD) is infeasible" is the negative sign of $c^Tx^*$ or $-b^Ty^*$ together with the infeasibility it certifies, not the bare disjunction "one of them is infeasible".
• "Optimal for (HLP)" means minimizing the objective over $\mathcal F_h$. It is not defined as $\theta=0$, which would make Theorem 2 (iv) definitional.
• Norms are Euclidean and written out explicitly, since Lean's default norm on $\mathbb R^n$ is the sup norm.
• (LP) and (LD) are built on the published general-form LP definitions (LinearOptimization_DualLP). The self-dual objects of the Vanderbei and Matoušek series are different embeddings and are not reused.

A complete development needs: skew-symmetric LP duality and strict complementarity (Goldman–Tucker) for (HLP), the Mizuno–Todd–Ye neighborhood calculus, and Hadamard-type bounds on integer determinants. Contributions to any milestone, or to these supporting libraries, are welcome.

Selected references

• Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt nL)$-iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• S. Mehrotra, Y. Ye, Finding an interior point in the optimal face of linear programs, Mathematical Programming 62, 497–515, 1993. https://doi.org/10.1007/BF01585180
• M. Kojima, S. Mizuno, A. Yoshise, A little theorem of the big M in interior point algorithms, Mathematical Programming 59, 361–375, 1993. https://doi.org/10.1007/BF01581253
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 373–395, 1984. https://doi.org/10.1007/BF02579150
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

Motivation

Linear programming algorithms often compute a solution to an auxiliary problem before extracting a solution to the original primal and dual pair. For a homogeneous self-dual formulation, the extraction requires a positive scaling coordinate. If that coordinate vanishes, the same auxiliary solution may instead describe infeasibility or unboundedness. Ye, Todd, and Mizuno introduced a homogeneous self-dual linear program that can start from arbitrary positive primal and dual slack vectors, even when the original programs have no known feasible point (Ye–Todd–Mizuno 1994).

Their Theorem 3 concerns strictly self-complementary optimal solutions of the auxiliary program. Theorem 9 addresses a different question: under a regularity assumption on the original programs, does a general optimal solution of the auxiliary program still have a positive scaling coordinate? The distinction matters because optimality alone does not require every complementary pair to have a positive member. This mission formalizes the statement of Theorem 9 and the numbered identities that frame it.

Setting

Fix a real matrix $A\in\mathbb R^{m\times n}$, a right-hand side $b\in\mathbb R^m$, and a cost vector $c\in\mathbb R^n$. The primal linear program (LP) minimizes $c^Tx$ subject to $Ax=b$ and $x\ge0$. Its dual (LD) maximizes $b^Ty$ subject to $A^Ty\le c$; $y\in\mathbb R^m$ is unrestricted. The dual slack is $s=c-A^Ty$.

An interior feasible point of (LP) is an $x$ with $Ax=b$ and every $x_j>0$. An interior feasible point of (LD) is a $y$ with every component of $c-A^Ty$ positive. “Interior” here is the paper's strict coordinatewise feasibility condition, not the topological interior of an equality-constrained set in ambient space. The existence of such a point implies ordinary feasibility for the corresponding program.

The paper builds an auxiliary program (HLP) from initial vectors $x^0>0$, $s^0>0$, and $y^0$. It uses the derived data

$$\bar b=b-Ax^0,\qquad \bar c=c-A^Ty^0-s^0,\qquad \bar z=c^Tx^0+1-b^Ty^0.$$

A point is a tuple $(y,x,\tau,\theta,s,\kappa)$ with $x,s,\tau,\kappa\ge0$ and free $y,\theta$. Its equality constraints are

$$\begin{aligned} Ax-b\tau+\bar b\theta&=0,\\ s&=-A^Ty+c\tau-\bar c\theta,\\ \kappa&=b^Ty-c^Tx+\bar z\theta,\\ -\bar b^Ty+\bar c^Tx-\bar z\tau&=-(x^0)^Ts^0-1. \end{aligned}$$

The objective is to minimize $((x^0)^Ts^0+1)\theta$. A feasible point is optimal when no feasible point has a smaller objective. The paper calls an optimal point self-complementary, whether or not its complementary pairs satisfy strict inequalities (p. 57, after Theorem 2(v)). After introducing the general construction, the paper fixes $y^0=0$ and $x^0=s^0=e$, the all-ones vector. That is the instance used in Theorem 9.

Formalization targets

Goal: Theorem 9

If both (LP) and (LD) have interior feasible points, then every self-complementary solution $w^*=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ of this fixed (HLP) satisfies

$$\tau^*>0.$$

The theorem quantifies over every optimal point, including those that are not strictly self-complementary. The printed tuple writes $\theta^*=0$; Theorem 2(iv) entails that fact from optimality, so it is not an extra hypothesis in the goal (Theorem 9, p. 64).

Supporting targets

Theorem 2(iv) states that (HLP) has zero optimal value and, for every feasible point under arbitrary positive initial $x^0,s^0$, satisfies

$$((x^0)^Ts^0+1)\theta=x^Ts+\tau\kappa.$$

Corollary 4 states that a positive $\kappa$ at an optimum under the fixed initialization entails infeasibility of (LP) or (LD). Equation (9) states the corresponding normalization identity

$$e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1.$$

These are separate milestone statements, each tied to its index and page in the paper (Theorem 2(iv), p. 57; equation (9), p. 58; Corollary 4, p. 59).

Significance

Theorem 9 says that the auxiliary model does not lose its positive scale at any optimum when the primal and dual programs are both strictly feasible. With $\tau^*>0$, the homogeneous primal and dual variables can be divided by $\tau^*$ to recover solutions in the original scale. The result applies even when the auxiliary optimum lacks strict complementarity; that is the additional coverage beyond the strictly self-complementary case of Theorem 3 (Ye–Todd–Mizuno 1994, pp. 58 and 64).

The mathematical result was proved in 1994. This mission's remaining work is a machine-checked proof of the stated regularity result and its supporting claims in the paper's specific (HLP) model. The definitions of the homogeneous feasible set, its slacks, and its optimality relation are reusable for the other results in the same paper. The full algorithm and complexity estimate belong to the other missions in this series.

Difficulty

The optimality condition controls the objective, and Theorem 2(iv) identifies that objective with a sum of complementarity terms. Those facts alone permit $\tau^*=0$; they do not force the scaling coordinate to be positive. Theorem 3's assertion for a strictly self-complementary point cannot be applied to an arbitrary optimal point, because its strict support condition may fail. The challenge is to use interior feasibility of both original programs to exclude all zero-scale optima while retaining the full set of HLP optima in the quantifier.

Formalization scope

The Lean model uses finite-dimensional real vectors indexed by Fin m and Fin n, a real matrix $A$, and a six-field HLP point in the paper's order $(y,x,\tau,\theta,s,\kappa)$. The standard-form primal and dual feasible sets are reused from a published LP definition with the same minimization and maximization orientation. Paper-specific interior predicates and the homogeneous program are defined locally. Slack fields in an HLP point are constrained to equal their formulas, so they cannot be chosen independently to make a statement true.

The model first defines (HLP) for general $x^0,y^0,s^0$ and then substitutes the paper's choice (7). It treats self-complementarity as objective minimization over the whole feasible set. Defining it by $\theta=0$ or by a complementarity equation would erase the content of Theorem 2(iv). The objective and normalization constants are exact, including the $n+1$ in the fixed instance. No real supremum or infimum is used to define optimality; it is a direct comparison against every feasible point.

The dimensions $m,n$ may be zero. Empty coordinatewise inequalities then have their usual vacuous meaning, but the equations remain in force. In particular the prescribed point $(0,e,1,1,e,1)$ is strictly feasible for every $A,b,c$, as a separate sorry-free local verification checks. This excludes an empty-feasible-set reading of the HLP definitions. Contributions proving the three numbered milestones, the goal, or reusable finite-dimensional LP lemmas are within scope.

Selected references

• Yinyu Ye, Michael J. Todd, and Shinji Mizuno, An $O(\sqrt nL)$-Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. DOI 10.1287/moor.19.1.53.

Motivation

Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.

Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.

Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, $(p,\varepsilon)$-optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation $J^* = T(J^*)$ under (P), (N) and (D).

Setting

The states $S$ and actions $A$ are non-empty Borel sets. A law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$. The return $r(s,a,t)$ is a Borel function with $-\infty < r \le 0$ whose expectation $\int r(s,a,t)\,dq(t\mid s,a)$ is finite for every $(s,a)$. A policy $\pi = (\pi_1,\pi_2,\dots)$ draws the $n$th action from a kernel $\pi_n(\cdot\mid s_1,a_1,\dots,s_n)$ that may depend on the whole history. A Markov policy $(f_1,f_2,\dots)$ uses measurable maps $f_n:S\to A$, and a stationary policy $f^{(\infty)}$ uses one map at every stage. The expected return from the initial state $s$ is

$$I(\pi)(s) = \sum_{n\ge1} E^\pi_s\, r(s_n,a_n,s_{n+1}) \in [-\infty,0],$$

and the optimal return is

$$v^*(s) = \sup_\pi I(\pi)(s),$$

the supremum over all policies. Write $M(S)$ for the non-positive, extended real-valued Borel functions on $S$. For $u\in M(S)$ and an action $a$,

$$T_a u(s) = \int \big[r(s,a,t) + u(t)\big]\,dq(t\mid s,a).$$

$T$ denotes the same operator for a measurable rule $f$ in place of $a$, and $U = \sup_n T_n$ for a Markov policy $(f_1,f_2,\dots)$. A policy $\pi^*$ is $(p,\varepsilon)$-optimal, for a probability $p$ on $S$, if $p\{I(\pi^*) \ge v^* - \varepsilon\} = 1$. The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.

Formalization targets

Goal: the optimality equation (Theorem 8.2, negative case)

$$v^*(s) = \sup_{a\in A} T_a v^*(s) \qquad\text{for all } s\in S.$$

The equation involves no constants and no regularity hypotheses on $v^*$.

Milestones

1. Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$.
2. Theorem 6.1: if $Uv\ge v$ for $v\in M(S)$, some Markov policy generated from $\hat\pi$ has $I(\pi)\ge v-\varepsilon$.
3. Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$.
4. Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
5. Lemma 7.1, Lemma 7.2: measurability of $(s,\nu)\mapsto\int u(s,x)\,d\nu(x)$, and Borel measurability of the set of pairs $(s, e_\pi(s))$, where $e_\pi(s)$ is the law of the future under $\pi$.
6. Theorem 7.1: $v^*$ is absolutely measurable.
7. Theorem 8.1: for every $p$ and $\varepsilon>0$ a $(p,\varepsilon)$-optimal Markov policy exists.

Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).

Significance

The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in $\sup_a T_a v^*$ can be tested for optimality. Value iteration and policy improvement can be compared with $v^*$. The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case $v^*$ satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that $v^*$ is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.

Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.

Difficulty

Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state $t$, a policy that is $\varepsilon$-optimal from $t$ and concatenates. Without measurable selection this concatenation is not a policy. The set of $t$ where a given policy is $\varepsilon$-optimal need not be Borel, and $v^*$ itself need not be Borel measurable, so even $\int v^*\,dq$ needs justification. Second, the contraction argument of the discounted case is unavailable. $U$ does not contract, it conserves $v+c$ along with $v$, and value iteration from $0$ can converge to a function strictly above $v^*$. The paper's Example 6.1 shows that the limit of $U^n0$, the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.

Formalization scope

• States and actions are non-empty standard Borel types. Policies are the published Blackwell plans (DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from $0$ (Lean's π.κ n is the paper's $\pi_{n+1}$). Markov policies are MarkovPlan; "$\pi$-generated" and $G(\hat\pi)$ are the published IsGenerated and IsGeneratedPlan.
• Only the negative case is formalized: $r\le0$ real-valued, $qr$ integrable, $\beta=1$. The discounted and positive parts of Theorems 5.2, 7.1, 8.1 and 8.2, including the uniqueness and minimality clauses of Theorem 8.2, are not stated.
• Returns take values in EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map $-\infty$ to $0$ and make the goal false or vacuous.
• $v^*$ is the supremum over all plans. It is not assumed measurable and is never replaced by a measurable modification. $T_a v^*$ is a lintegral of a possibly non-measurable function, which equals the completion integral because $v^*$ is absolutely measurable (Theorem 7.1).
• Explicit readings of the page: the hypothesis $u\in M(S)$ of each operator statement is IsNegM u. Theorem 5.2(b) assumes $u+c\in M(S)$. "$U$ conserves $v$" includes $v\in M(S)$. Lemma 6.2 asserts that the limit defining $v_\pi$ exists. Theorem 6.2 states $\ge$ everywhere and $>$ where $\sup_j I(\pi^j) > -\infty$ (the printed $>$ fails where the supremum is $-\infty$). $(p,\varepsilon)$-optimality is "$p$-almost everywhere". Absolute measurability is NullMeasurable for every probability measure. $P(X)$ carries the Giry σ-field. The extra Theorem 8.4 reads the printed "$I(\pi) < u$" as "$\le$" (the strict reading is false).
• Reusable infrastructure: the negative model, the Ionescu-Tulcea law of the future (futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.

Selected references

• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• D. Blackwell, Positive Dynamic Programming, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
• L. E. Dubins and L. J. Savage, How to Gamble If You Must, McGraw-Hill, 1965.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$, how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

$$s = \lambda + \gamma\sqrt{\lambda},$$

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$, its mean and variance are both $\lambda$, so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$. The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

• The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
• Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
• Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$, the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$-th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$, the number of arrivals in $(0, t]$. This is a Poisson process of rate $\lambda$.

Customers are numbered $k = 0, 1, 2, \dots$; customer $k$ arrives at $\tau_{k+1}$, is served at once, and has service time $D_k$. Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$. The number of busy servers is

$$N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.$$

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$. Each customer carries a class label $J_k$, the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$. The class-$i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$.

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$, then

$$P\big(N(t) = k\big) = e^{-\lambda}\frac{\lambda^k}{k!}, \qquad k = 0, 1, 2, \dots$$

The law depends on the service-time distribution only through its mean.

Milestones

1. Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$, pathwise.
2. Proof of Proposition 2.4 (p. 712): for $t \ge 1$, $A(t) - A(t-1)$ has the same law as $A(1)$.
3. Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$.
4. §2.5, splitting (p. 713): the class-$i$ arrivals form independent Poisson streams of rates $\lambda p_i$; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
5. §2.5, "Hence" (p. 713): for $t > \max_i d_i$, the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$, and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$, connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$.

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$, the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$-server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

• a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
• Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
• the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$.

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$: the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

• The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
• The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
• Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$, and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$, avoiding pushforwards of possibly non-measurable maps.
• Standing conventions: service rate $1$; the system starts empty at time $0$; arrival counted at $t$, departure not; "steady state" means the law at each fixed $t > \max_i d_i$, with no limit $t \to \infty$; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$, and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$. Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
• Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

• W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
• D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651