Operations Research

Why reentrant lines, and why this one

A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.

Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.

Timeline:

• 1993: Kumar conjectured that the three-buffer line $1 \to 2 \to 1$ is stable under the first-in-first-out (FIFO) discipline whenever the load condition holds, for exponential distributions.
• 1993: Wang proved that the FIFO fluid model of this line is stable, which with Dai's theorem confirms the conjecture.
• 1996: Dai and Weiss (Theorem 3.1) proved stability of the fluid model for every work-conserving discipline, with an explicit emptying time.

Setting

A reentrant line has $I$ stations and $K$ classes. Fluid enters as class $1$ at rate one; class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and service rate $\mu_k = 1/m_k$, and on completion becomes class $k+1$ (class $K$ leaves). The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$, and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$.

A fluid model solution is a pair of paths $Q(t) \in \mathbb R^K$ (fluid levels) and $T(t) \in \mathbb R^K$ (cumulative time spent serving each class) such that, for $t \ge 0$:

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t)\quad(\mu_0T_0(t) = t),\qquad Q_k(t) \ge 0,$$

each $T_k$ starts at $0$ and is nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, with busy time $B_i(t) = \sum_{k \in C_i} T_k(t)$, is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

A set of fluid model solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution with $|Q(0)| = \sum_k Q_k(0) = 1$ has $Q(t) = 0$ for all $t \ge \delta$.

The three-buffer line of Figure 1 has $I = 2$, $K = 3$ and route $1 \to 2 \to 1$: classes $1$ and $3$ at station $1$, class $2$ at station $2$. The load condition (3.1) is

$$\rho_1 = m_1 + m_3 < 1, \qquad \rho_2 = m_2 < 1 .$$

Formalization targets

Goal: Theorem 3.1

$$m_1, m_2, m_3 > 0,\ \ m_1 + m_3 < 1,\ \ m_2 < 1 \ \Longrightarrow\ \text{the work-conserving fluid model (1.8)–(1.13) of } 1 \to 2 \to 1 \text{ is stable.}$$

The goal fixes no emptying time: it asserts only that some $\delta > 0$ works, which is Definition 1.3.

Milestones, in attack order

1. Lemma 2.2 (ii): a nonnegative absolutely continuous $g$ with $\dot g(t) \le -\varepsilon$ almost everywhere where $g(t) > 0$ vanishes from $g(0)/\varepsilon$ on, and is nonincreasing.
2. Display (3.2) (already proved on the platform): at a regular point, the maximum of finitely many functions has the derivative of every component that attains it.
3. Lemma 3.2: for nonnegative linear functions $G_i$ of $Q$ with (a) $\dot G_i \le -\varepsilon_i$ while $W_i > 0$ and (b) $G_i \le \min_{j \ne i} G_j$ while $W_i = 0$, the maximum $G$ is absolutely continuous and nonnegative, and $\dot G(t) \le -\min_i \varepsilon_i$ at regular points with $G(t) > 0$.
4. Drift identity (proof of Theorem 3.1): with $\theta = m_1/(m_1+m_3)$, $G_1 = \theta Q_1^+ + (1-\theta)Q_3^+$ and $G_2 = Q_2^+$, where $Q_k^+ = \sum_{l \le k} Q_l$, one has $G_i(t) = G_i(0) + t - B_i(t)/\rho_i$.
5. Drift rate: $\dot G_i(t) = -(1/\rho_i - 1) < 0$ whenever $W_i(t) > 0$.
6. Condition (b): $W_1(t) = 0 \Rightarrow G_1(t) \le G_2(t)$ and $W_2(t) = 0 \Rightarrow G_2(t) \le G_1(t)$.
7. Emptying time: every work-conserving solution with $|Q(0)| = 1$ is empty from $\max\{\rho_1/(1-\rho_1), \rho_2/(1-\rho_2)\}$ on.

Significance

Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.

The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.

Difficulty

The obvious approach is to split cases on the relative loads, as the paper notes ($m_1 + m_3/m_2 < 1$ or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.

Formalization scope

All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:

• Classes and stations are 0-based (Fin 3, Fin 2). The paper's class $k$ is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.
• Paths are total functions ℝ → Fin K → ℝ; every equation is imposed only for $t \ge 0$, and derivatives are taken at $t > 0$ (HasDerivAt).
• Work conservation (1.13) is in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. This is equivalent to the paper's integral condition for continuous paths.
• No Lipschitz continuity is assumed; it follows from (1.10)–(1.12).
• $m_k > 0$ is an explicit hypothesis (the paper takes it for granted). $|Q(0)| = \sum_k Q_k(0)$.
• Lemma 2.2 (ii) is stated with $\dot g(t) \le -\varepsilon$; the paper prints $<$, but every application uses $\le$, and the stated version is the stronger lemma.
• Lemma 3.2 is stated for any reentrant line with $I \ge 1$ stations, assuming only (1.8)–(1.12), as in the paper.

A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every $m$ satisfying (3.1), with $|Q(0)| = 1$ (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.

Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• P. R. Kumar, Re-entrant lines, Queueing Systems 13, 87–110, 1993. https://doi.org/10.1007/BF01158927
• A. N. Rybko and A. L. Stolyar, Ergodicity of stochastic processes describing the operation of open queueing networks, Problems of Information Transmission 28, 199–220, 1992.
• D. D. Botvich and A. A. Zamyatin, Ergodicity of conservative communication networks, Rapport de recherche 1772, INRIA, 1992.

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$-concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$. At the start of period $t$, the firm has inventory $x$, which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$. If $y>x$, it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$. After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$. The corresponding price is $P_t(d)$, the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$.

Actual demand is $\alpha_t d+\beta_t$. The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$, with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$. No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$, incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$. For a post-order inventory $y$ and expected demand $d$, write

$$g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].$$

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$. This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$-convex real function $f$ satisfies

$$f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k$$

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$. A function is symmetrically $k$-concave when its negative is symmetrically $k$-convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$, then for every period

$$G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.$$

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$. An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$, and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$.

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$-convexity to symmetric $k$-convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$-convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$, that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$-concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$. The statement must assert Bellman optimality at every $x$, including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$, matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$, with $T>0$ and terminal value $v_{T+1}=0$. Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$. The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$.

The formal assumptions include $k\ge0$ and $c_t\ge0$, and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$.

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

• Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

Why the simplex method needs smoothed analysis

The simplex method solves linear programs quickly in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972). Smoothed analysis, introduced by Spielman and Teng (JACM 2004), explains the gap: it measures the expected running time when every constraint row of a worst-case input is perturbed by a small random amount of size $\sigma$. For the shadow vertex pivot rule, the running time is controlled by a purely geometric quantity, the number of edges of a random polygon, and the smoothed complexity of the method is essentially an upper bound on that number.

Timeline (bounds on the expected shadow size of smoothed unit LPs, as surveyed in §1.1 of the paper). Borgwardt (1987) proved $\Theta(d^{1.5}\sqrt{\log n})$ for rows drawn from a centered Gaussian, asymptotically as $n\to\infty$; this is the case $\bar a_i=0$ of the model below. Spielman and Teng (2004) gave the first smoothed bound, $O(d^3n\sigma^{-6}+d^6n\log^3 n)$. Deshpande and Spielman (FOCS 2005) improved the dependence on $\sigma$ to $O(dn^2\log n\,\sigma^{-2}+d^2n^2\log^2 n)$. Vershynin (SIAM J. Comput. 2009) reduced the dependence on $n$ to polylogarithmic, $O(d^3\sigma^{-4}+d^5\log^2 n)$. Dadush and Huiberts (arXiv:1711.05667, STOC 2018, SIAM J. Comput. 2020) proved $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^{2.5}\log n\,\sigma^{-1}+d^{2.5}\log^{1.5}n)$ for Gaussian perturbations by a simpler argument, which also gives bounds for Laplace perturbations.

Setting

Fix dimensions $n\ge d\ge3$ and a shadow plane, a two-dimensional linear subspace $W\subseteq\mathbb R^d$, chosen independently of the randomness. The constraint vectors $a_1,\dots,a_n\in\mathbb R^d$ are independent, and $a_i\sim N_d(\bar a_i,\sigma)$ is Gaussian with center $\bar a_i$, $\|\bar a_i\|\le1$, and standard deviation $\sigma>0$ in every coordinate, i.e. with density $(2\pi\sigma^2)^{-d/2}e^{-\|x-\bar a_i\|^2/(2\sigma^2)}$.

Let $Q=\operatorname{conv}(a_1,\dots,a_n)$. The shadow polygon is $Q\cap W$. An edge of a convex set $K$ is a segment $[u,v]$, $u\ne v$, which is an extreme subset of $K$; $|\operatorname{edges}(K)|$ is the number of edges. The number of pivots of the shadow vertex method on the unit LP $\{x:Ax\le\mathbf1\}$ between two objectives spanning $W$ is at most $|\operatorname{edges}(Q\cap W)|$ (the paper's Lemma 11 and Theorem 12).

The proof passes through general row distributions with density $\mu$ and mean $y$, described by four parameters: the log-Lipschitz constant $L$ ($\mu(x)\le e^{L\|x-x'\|}\mu(x')$); the line variance $\tau^2$ (the least variance of $\mu$ restricted to a line); the $n$-th deviation $r_n$ (the least $r$ with $\int_r^\infty\Pr[|(X-y)^\mathsf T\theta|\ge t]\,dt\le r/n$ for all unit $\theta$); and the cutoff radius $R_{n,d}$ (the least $R$ with $\Pr[\|X-y\|\ge R]\le 1/(d\binom nd)$). The Gaussian is not log-Lipschitz; the Laplace–Gaussian distribution $LG_d(\bar a,\sigma,r)$, whose density equals the Gaussian one inside the ball of radius $r\sigma$ around $\bar a$ and decays like $e^{-\|x-\bar a\|r/\sigma}$ outside, replaces it.

Formalization targets

Goal: Theorem 13 with explicit constants

$$\mathbb E\big[|\operatorname{edges}(\operatorname{conv}(a_1,\dots,a_n)\cap W)|\big]\le 3+\frac{128\pi e^2 d^2\sqrt{\log n}}{\sigma^2}\big(1+4\sigma\sqrt{d\log n}\big)\big(1+16\sigma\sqrt{\log n}\big).$$

The paper states $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^{2.5}\log n\,\sigma^{-1}+d^{2.5}\log^{1.5}n)$; the constant above is the one its proof produces (Theorem 22's proof, Lemma 45, Lemma 46).

Intermediate targets (milestones)

• the parametrized shadow bound (Theorem 22), $\mathbb E|\operatorname{edges}|\le 2+8\pi e^2d^{1.5}(L/\tau)(1+R_{n,d})(1+4r_n)$;
• its ingredients: the edge-counting reduction (Lemma 25), the perimeter bound $2\pi(1+4r_n)$ (Lemmas 19, 26), the conditioning on bounded diameter (Lemma 29), the chord combination calculus (Lemmas 35, 36), and the two expected-length bounds (Lemmas 39, 40, 41), together with the trade-off $LR(1/2)\ge d/3$ (Lemma 21);
• the Gaussian specialisation: Laplace–Gaussian tails (Lemma 44), its parameters (Lemma 45), and the comparison with the Gaussian (Lemma 46).

Significance

The bound gives the best known smoothed complexity of a simplex method, with only $\sqrt{\log n}$ dependence on the number of constraints. Section 4 of the paper turns it into a complete two-phase shadow vertex algorithm with $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^3\log^{1.5}n)$ expected pivots. The parametrized Theorem 22 applies to any perturbation family with bounded parameters, so it also yields shadow bounds for Laplace and other noise models.

The result is proved; it has not been machine-checked. A formalization adds a verified chain from four distributional parameters to a polygon edge count. The intermediate statements have independent value: an expected-perimeter bound for random polygons, the deterministic chord-length identity for simplices, and tail estimates for the Laplace–Gaussian distribution.

Difficulty

The expected number of edges is a sum, over all $\binom nd$ index sets, of the probability that their simplex meets $W$ in an edge; there are far too many terms for per-set estimates to give a bound polylogarithmic in $n$. The paper's route (inspired by Kelner and Spielman) instead compares the expected perimeter with the expected length of an edge, and the hard part is a lower bound on the expected length of an edge conditioned on it appearing. That conditioning is on a probability-zero configuration (the simplex lying in a fixed hyperplane), and its analysis needs Blaschke's change of variables, the shape decomposition of the simplex, and log-Lipschitz shifts of densities. On the Gaussian side, the density is not log-Lipschitz, which forces the Laplace–Gaussian detour and a comparison of edge counts under two different laws.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d), $[n]$ is Fin n, $\log$ is the natural logarithm. The Gaussian is the published SmoothedSimplex.Shadow.gaussian, the edge relation is the published Hirsch.Adj, and the rows' joint law is Measure.pi. Edges are segments counted once; the perimeter is the sum of edge lengths. Expectations are lower Lebesgue integrals in $[0,\infty]$, and every edge-count bound also asserts almost-everywhere measurability of the count, so the integral is a genuine expectation. Conditional expectations are stated multiplied out (no division by a probability), and the parameters of Definitions 15–18 are upper-bound predicates (lower bound for the line variance), which is how every statement of the paper uses them.

Hypotheses added relative to the page, each implicit there: $\sigma>0$; $L,\tau>0$ and $R,r\ge0$ in Theorem 22; positivity of log-Lipschitz densities; the standing $n\ge d\ge3$ of §3 in Lemma 44. Lemmas 39 and 41 are stated on the explicit conditional densities that the paper derives in Lemma 37, instead of through regular conditional distributions; Lemma 39 takes the conclusion $d/3\le LR$ of Lemma 21 as a hypothesis, as its proof uses it. Two printed slips are corrected: Lemma 46's formula is stated for $\operatorname{conv}(a_1,\dots,a_n)\cap W$, as its sentence and proof have it, and Lemma 35 refers to Definition 33 (not 34).

The goal mentions only Gaussian rows, $W$, and the edge count of $\operatorname{conv}(a)\cap W$. It cannot be trivialized by an unsatisfiable parameter hypothesis or a bound on edge lengths, since it has neither; and it counts edges of the polygon, not of the polytope $\operatorname{conv}(a)$.

A complete development needs: Gaussian and Laplace–Gaussian tail bounds; measurability of the edge count of a random polygon; the perimeter monotonicity of convex sets; Blaschke's change of variables (Theorem 7 of the paper, quoted from Blaschke 1935), which Mathlib does not have; and the regular conditioning of Lemmas 32, 37 and 38. The Blaschke formula, the perimeter facts for convex polygons, and the tail bounds are reusable well beyond this mission. Contributions to any milestone, or to these supporting results as separate theorems, are welcome.

Selected references

• D. Dadush, S. Huiberts, A Friendly Smoothed Analysis of the Simplex Method, SIAM J. Comput. 49(5), 2020 (STOC 2018); preprint arXiv:1711.05667v4, 2019. https://arxiv.org/abs/1711.05667
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3), 2004. https://doi.org/10.1145/990308.990310
• R. Vershynin, Beyond Hirsch Conjecture: Walks on Random Polytopes and Smoothed Complexity of the Simplex Method, SIAM J. Comput. 39(2), 2009. https://doi.org/10.1137/070683386
• A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005 (cited as [DS05] in the paper).
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972 (cited as [KM70] in the paper).

Motivation

Airlines sell the seats of one flight leg at several prices. Cheaper fare classes tend to book earlier, so the seller must decide, as low-fare requests arrive, how many seats to hold back for later and more valuable passengers. The standard control is nested protection levels: a number $p_k$ of seats is reserved for the $k$ most expensive classes together, and a request of class $k+1$ is accepted only while more than $p_k$ seats remain. Littlewood (1972) gave the optimal rule for two classes; Belobaba's EMSR heuristic (1987, 1989) extended it to many classes without an optimality guarantee.

S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes (Operations Research 41(1), 1993) treat any number of classes with independent random demands and characterize optimal protection levels by first-order conditions on the expected revenue: Theorem 1 states that a policy with $f_{k+1}$ in the subdifferential of the expected revenue of the $k$ highest classes at $p_k$, for every $k$, is optimal. Their Theorem 2 addresses the question practitioners face first: seats and bookings are whole numbers. If demand is integer valued, is an optimal policy available among integer protection levels? The theorem answers yes. This mission formalizes that theorem and the chain of results in its proof.

Timeline.

• Littlewood (1972): two fare classes, rule $f_2 = f_1 \Pr[X_1 > p_1]$.
• Belobaba (1987, 1989): EMSR heuristic for many classes.
• Curry (1990) and Wollmer (1992): multiple nested classes, continuous and discrete demand respectively.
• Brumelle and McGill (1993): subdifferential optimality conditions for any number of classes (Theorem 1), existence of an optimal integer policy for integer demand (Theorem 2), and the probability conditions (31) (Theorem 3).

Setting

Classes are numbered $k = 1, 2, \dots$, class $1$ paying the highest fare. Class $k$ has a random demand $X_k \ge 0$ and fare $f_k$, with $f_1 > f_2 > \cdots$. The demands are mutually independent on a probability space $(\Omega, \mathcal F, P)$. A protection-level policy is a sequence $p = (p_1, p_2, \dots)$ with $p_k \ge 0$; the dummy level $p_0 = 0$ is never used.

For a demand vector $x$ and $s$ available seats, the revenue of the $k$ highest classes is defined recursively (Eqs. (8)–(9), p. 130):

$$R_1[s; p; x] = \begin{cases} f_1 s & 0 \le s < x_1,\\ f_1 x_1 & x_1 \le s,\end{cases}$$ $$R_{k+1}[s; p; x] = \begin{cases} R_k[s; p; x] & 0 \le s < p_k,\\ (s - p_k) f_{k+1} + R_k[p_k; p; x] & p_k \le s < p_k + x_{k+1},\\ x_{k+1} f_{k+1} + R_k[s - x_{k+1}; p; x] & p_k + x_{k+1} \le s.\end{cases}$$

The expected revenue is $ER_k[s; p; X] = E\,R_k[s; p; X]$. A policy is optimal if it maximizes $ER_k[s; \cdot\,; X]$ for every $k$ and every $s \ge 0$ (p. 130).

For a function $g$ and $t \ge 0$, $\delta_+ g(t)$ and $\delta_- g(t)$ are the right and left derivatives, with $\delta_- g(0) = +\infty$, and the subdifferential is $\delta g(t) = [\delta_+ g(t), \delta_- g(t)]$ (p. 131). Condition (20) is

$$f_{k+1} \in \delta ER_k[p_k; (p_0, \dots, p_{k-1}); X], \qquad k = 1, 2, \dots$$

A function is CLBI (Concave and Linear Between Integers, p. 132) if it is concave on $s \ge 0$ and linear on each interval $[m, m+1]$, $m = 0, 1, 2, \dots$

Formalization targets

Goal: Theorem 2 (p. 132)

If every $X_k$ is integer valued and the fares are positive, there is a policy $p^*$ with $p^*_k \in \{0, 1, 2, \dots\}$ such that

$$ER_k[s; q; X] \le ER_k[s; p^*; X] \qquad \text{for every policy } q,\ k \ge 1,\ s \ge 0,$$

and $p^*$ satisfies (20). The competitor $q$ ranges over all real protection levels.

Milestones (in proof order)

1. (27): $\delta ER_1[s; p; X] = [f_1 \Pr[X_1 > s], f_1 \Pr[X_1 \ge s]]$, and $ER_1$ is CLBI.
2. Covering property (p. 132): if $g$ is CLBI and $\delta_+ g(s_2) < c < \delta_- g(s_1)$ with $s_1 < s_2$, then $c \in \delta g(n)$ for an integer $n \in [s_1, s_2]$.
3. (28)–(29): for $s \ge p_k$,

$$\delta_+ ER_{k+1}[s] = f_{k+1}\Pr[X_{k+1} > s - p_k] + \sum_{i=0}^{\lfloor s - p_k\rfloor} \delta_+ ER_k[s - i]\Pr[X_{k+1} = i],$$

and the analogous formula for $\delta_-$ at $s > p_k$. 4. Corollary 1 (p. 131): concavity of $ER_k$ and $f_{k+1} \in \delta ER_k[p_k]$ give concavity of $ER_{k+1}$. 5. CLBI propagation (p. 133): if $ER_k[\cdot; p^*; X]$ is CLBI and integer $p^*_1, \dots, p^*_k$ satisfy (20), then $ER_{k+1}[\cdot; p^*; X]$ is CLBI. 6. (30): for $s$ large enough, $\delta_+ ER_{k+1}[s; p; X] < f_{k+2}$. 7. Theorem 1 (p. 131): a policy satisfying (20) is optimal.

Significance

The result. Theorem 2 justifies computing protection levels in whole seats: with integer demand, restricting to integer policies loses nothing against arbitrary real protection levels. The construction also shows that (20) is solvable at every level, so the sufficient condition of Theorem 1 is never empty for integer demand. Many later revenue-management models assume an optimal nested policy exists and rely on this result or its dynamic-programming analogues.

Formalizing it. The theorem is proved on the page by an induction on the class index, but several steps are compressed: (28)–(29) are printed without the range of $s$ on which they hold, and (30) is asserted "by recursive application". To our knowledge none of these statements has a machine-checked proof. A formal development gives a verified account of one-sided derivatives of expectations of piecewise-linear random functions and of the integer covering property. These pieces are reusable for other newsvendor-type and nested-inventory models. The probability-condition characterization (Theorem 3) is the subject of a companion mission in the same series.

Difficulty

Concavity of the expected revenue does not hold for arbitrary policies. It is only guaranteed level by level, when the protection level already chosen at level $k$ satisfies (20). Existence of an integer optimum therefore cannot be obtained by rounding a real optimum: the integer levels must be chosen one at a time, and each choice must preserve both concavity and the CLBI shape needed for the next. A second obstacle is analytic. The one-sided derivatives of $ER_{k+1}$ are expectations of derivatives of a random piecewise-linear function. Exchanging differentiation and expectation, and computing the sums in (28)–(29) exactly at integer and non-integer $s$, is where informal arguments and formal ones diverge. Finally there are infinitely many classes, so the policy $p^*$ is an infinite sequence built by recursion.

Formalization scope

• Model. Classes are indexed by $\mathbb N$ from $1$; fares, demands and protection levels are sequences $\mathbb N \to \mathbb R$. Seats, demands and protection levels are real; an integer policy is a sequence of natural numbers read as reals. Integer-valued demand means each $X_k(\omega)$ is a natural number. Expectations are Bochner integrals.
• Standing assumptions (§1). $P$ is a probability measure. The demands are measurable, nonnegative and mutually independent, and the fares are strictly decreasing.
• Added hypotheses. The goal assumes positive fares, $f_k > 0$ for $k \ge 1$. The page leaves this implicit (fares are average revenues), and without it the theorem is false. The same assumption appears in (30), and (27) assumes $f_1 \ge 0$, without which $ER_1$ is convex rather than concave.
• Derivatives. One-sided derivatives are required to exist, with their value asserted; no default value of an undefined derivative is used. The convention $\delta_- g(0) = +\infty$ is built into the subdifferential.
• Optimality. Optimality is global: against every real protection-level policy, at every level $k \ge 1$ and every $s \ge 0$.
• Paper's slips corrected. (28)–(29) are stated on their range $s \ge p_k$ (resp. $s > p_k$). (30) is stated for every $k \ge 1$, as the induction uses it, rather than the printed $k = 2, 3, \dots$
• Not a trivialization. The goal assumes only the model, integer demand and positive fares. It does not assume concavity, CLBI, (20) or any derivative formula, and optimality is not restricted to integer competitors or to one $k$.
• Duplication. Corollary 1 and Theorem 1 are restated from the companion mission in this series.
• Contributions. Proofs of the measure-theoretic derivative lemmas, of the covering property (a statement about real functions), and of the induction are all welcome.

Selected references

• S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes, Operations Research 41(1):127–137, 1993. https://doi.org/10.1287/opre.41.1.127
• K. Littlewood, Forecasting and Control of Passenger Bookings, AGIFORS Symposium Proceedings 12:95–117, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, 1987. http://hdl.handle.net/1721.1/68077
• P. P. Belobaba, Application of a Probabilistic Decision Model to Airline Seat Inventory Control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• R. E. Curry, Optimal Airline Seat Allocation with Fare Classes Nested by Origins and Destinations, Transportation Science 24(3):193–203, 1990. https://doi.org/10.1287/trsc.24.3.193
• R. D. Wollmer, An Airline Seat Management Model for a Single Leg Route When Lower Fare Classes Book First, Operations Research 40(1):26–37, 1992. https://doi.org/10.1287/opre.40.1.26

Related work on the platform. The two-class, integer-capacity EMSR rule of Belobaba (1987) is formalized as SeatInventory.Nested.emsr_protection_level_optimal. It is a relative of the $k = 1$ case of Theorem 2, but it lives in a different model: two classes, a fixed integer capacity, and only integer competitors.

Motivation

Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy $\varepsilon$. In fixed dimension $n$ the answer is of order $n\log(1/\varepsilon)$, and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.

Timeline:

• 1960: B. Grünbaum proves that every half-space whose boundary passes through the centroid of a convex body in $\mathbb R^n$ contains at least a fraction $(n/(n+1))^n \ge 1/e$ of its volume.
• 1965: A. Levin and D. J. Newman independently introduce the center of gravity method and prove its linear rate.
• 1983: A. Nemirovski and D. Yudin show that $\Omega(n\log(1/\varepsilon))$ oracle calls are necessary for small $\varepsilon$, so the method's oracle complexity is optimal.

Setting

Let $\mathcal X\subset\mathbb R^n$ be a convex body: a compact convex set with non-empty interior. Let $f:\mathcal X\to[-B,B]$ be continuous and convex, and let $x^*\in\mathcal X$ be a minimizer of $f$ on $\mathcal X$. A vector $w$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le w^\top(x-y)$ for every $y\in\mathcal X$. The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of $f$.

For a set $\mathcal S$ of finite positive volume, its center of gravity is

$$c(\mathcal S)=\frac{1}{\mathrm{vol}(\mathcal S)}\int_{x\in\mathcal S}x\,dx .$$

The center of gravity method sets $\mathcal S_1=\mathcal X$ and, for $t\ge1$, computes $c_t=c(\mathcal S_t)$, queries the first order oracle at $c_t$ to obtain a subgradient $w_t$, and sets

$$\mathcal S_{t+1}=\mathcal S_t\cap\{x\in\mathbb R^n:(x-c_t)^\top w_t\le0\}.$$

After $t$ steps it outputs $x_t\in\operatorname{argmin}_{1\le r\le t}f(c_r)$, found with $t$ calls to the zeroth order oracle.

The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.

Formalization targets

Goal: Theorem 2.1 (p. 245)

For every run of the method and every $t\ge1$,

$$f(x_t)-\min_{x\in\mathcal X}f(x)\le 2B\Big(1-\frac1e\Big)^{t/n}.$$

Milestones (proof of Theorem 2.1, pp. 246–247)

1. Lemma 2.2 (Grünbaum). If $\mathcal K$ is centered, $\int_{\mathcal K}x\,dx=0$, then for every $w\ne0$,

$$\mathrm{Vol}\big(\mathcal K\cap\{x:x^\top w\ge0\}\big)\ge\tfrac1e\,\mathrm{Vol}(\mathcal K).$$

2. (2.2). $\mathcal S_t\setminus\mathcal S_{t+1}\subset\{x\in\mathcal X:(x-c_t)^\top w_t>0\}\subset\{x\in\mathcal X:f(x)>f(c_t)\}$, hence $x^*\in\mathcal S_t$ for every $t$.
3. Volume decay. If $w_s\ne0$ for $s\le t$, then $\mathrm{vol}(\mathcal S_{t+1})\le(1-1/e)^t\,\mathrm{vol}(\mathcal X)$.
4. Shrunk copies. For $\varepsilon\in[0,1]$ and $\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x: x\in\mathcal X\}$, $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X)$.
5. Values on shrunk copies. Every $x_\varepsilon\in\mathcal X_\varepsilon$ satisfies $f(x_\varepsilon)\le f(x^*)+2\varepsilon B$.

Significance

Theorem 2.1 is a linear rate whose number of queries to reach accuracy $\varepsilon$, $O(n\log(2B/\varepsilon))$, depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ($O(n^2\log(1/\varepsilon))$ queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.

On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.

Difficulty

The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to $1/e$ of the volume as $n\to\infty$, so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in $[0,\infty]$ in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with $|f|\le B$, continuity and convexity required on $\mathcal X$ only; its values off $\mathcal X$ are irrelevant. Subgradients are relative to $\mathcal X$ (Definition 1.2). A run is a predicate on sequences indexed from $1$; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer $x^*$ is a hypothesis, as in the book's standing notation; it exists here by compactness. The output $x_t$ is any argmin, so the goal bounds the minimum $\min_{1\le r\le t}f(c_r)$.

Added hypotheses, all disclosed in the statements: $n\ge1$ in the goal, because the exponent $t/n$ is undefined for $n=0$; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is $0$, which would make every unbounded convex set "centered". The milestone on volume decay assumes $w_s\ne0$, which is the book's own reduction.

The center of gravity is defined with the real volume $\mathrm{vol}(\mathcal S)$ and is meaningless when that volume is $0$ or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.

Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §2.1. https://arxiv.org/abs/1405.4980
• B. Grünbaum, Partitions of mass-distributions and of convex bodies by hyperplanes, Pacific Journal of Mathematics 10(4):1257–1261, 1960. https://doi.org/10.2140/pjm.1960.10.1257
• A. Yu. Levin, On an algorithm for the minimization of convex functions, Soviet Mathematics Doklady 6:286–290, 1965.
• D. J. Newman, Location of the maximum on unimodal surfaces, Journal of the ACM 12(3):395–398, 1965. https://doi.org/10.1145/321281.321291
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

Motivation

Many controlled queueing, inventory and maintenance systems are modelled as controlled Markov processes (CMPs) on a countable state space whose one-stage cost grows without bound: the holding cost of a queue grows with its length. For such systems the natural performance measure is the long-run average cost, and the basic question is whether some simple policy, one that looks only at the current state and never randomizes, is optimal among all policies, including those that use the whole history.

When the cost is bounded, the classical answer goes through a bounded solution of the average cost optimality equation (ACOE). For unbounded costs, bounded solutions are rare: in many queueing models the relative value function grows with the state, and growth conditions such as (5.2) of the survey may fail (Arapostathis et al. 1993, p. 307). Sennott (1986; 1989) replaced boundedness by one-sided conditions on the discounted value functions, which are often easy to verify for queueing models because the relative values are bounded below. This mission formalizes Sennott's existence theorem in the form given in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus, Theorem 5.9.

Timeline. For bounded costs, Ross (1983, the survey's Theorem 5.2) obtained a bounded ACOE solution, and with it an optimal stationary policy, when the differential discounted values are uniformly bounded. Federgruen, Hordijk and Tijms (1979) treated unbounded costs under Lyapunov-type recurrence conditions, which restrict how fast the cost may grow (survey, Remark 5.7). Sennott (1986, 1989) replaced these by a uniform lower bound and a pointwise, one-step integrable upper bound on the differential discounted values. The survey (1993, Theorem 5.9) states the result with compact action sets and continuous data, and Sennott's 1999 book (§7.2) gives the finite-action version in textbook form.

Setting

The state space is $S=\{0,1,2,\dots\}$. For each state $i$ the set $U(i)$ of admissible actions is a nonempty compact subset of a metric space $A$. Choosing $a\in U(i)$ in state $i$ costs $c(i,a)\ge0$, and the next state is $j$ with probability $P(j\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$.

An admissible policy $\pi\in\Pi$ chooses the action at time $t$ according to a probability distribution $\pi_t(\cdot\mid h_t)$ concentrated on $U(x_t)$, where $h_t=(x_0,a_0,\dots,x_t)$ is the history; it may use the whole history and may randomize. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$, applied at every step. Given an initial state $i$ and a policy $\pi$, the states and actions $(X_t,A_t)$ form a stochastic process with law $P^\pi_i$ and expectation $E^\pi_i$.

For $\beta\in(0,1)$, the discounted cost and the average cost of $\pi$ from $i$ are

$$J_\beta(i,\pi)=E^\pi_i\sum_{t=0}^\infty\beta^tc(X_t,A_t),\qquad J(i,\pi)=\limsup_{N\to\infty}\frac1N\,E^\pi_i\sum_{t=0}^{N-1}c(X_t,A_t),$$

both in $[0,\infty]$. The optimal values are $J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi)$ and $J^*(i)=\inf_{\pi\in\Pi}J(i,\pi)$, and the differential discounted value is $h_\beta(i)=J^*_\beta(i)-J^*_\beta(0)$. A policy $f\in\Pi_{SD}$ is AC-optimal if $J(i,f)=J^*(i)$ for every $i$.

Sennott's conditions (Assumptions 5.14–5.16) are:

1. $J^*_\beta(i)<\infty$ for all $i\in S$ and $\beta\in(0,1)$;
2. there is a nonnegative integer $L$ with $h_\beta(i)\ge-L$ for all $i$ and $\beta$;
3. there is $M:S\to\mathbb R_+$ with $h_\beta(i)\le M(i)$ for all $i$ and $\beta$, and for each $i$ some $a(i)\in U(i)$ with $\sum_jP(j\mid i,a(i))M(j)<\infty$.

Formalization targets

Goal: Theorem 5.9

$$\text{Under Assumptions 5.14–5.16, there is } f\in\Pi_{SD}\text{ with } J(i,f)=\inf_{\pi\in\Pi}J(i,\pi)\ \text{ for every } i\in S.$$

The goal asserts only existence. It does not fix the optimal cost, and it does not claim that the optimal cost is constant or that an optimality equation holds.

Milestones

1. Theorem 2.1 (i), (iii), countable form: the discounted cost optimality equation $J^*_\beta(i)=\inf_{a\in U(i)}\{c(i,a)+\beta\sum_jP(j\mid i,a)J^*_\beta(j)\}$ and a $\beta$-discount optimal $f_\beta\in\Pi_{SD}$.
2. Display (5.15): $(1-\beta)J^*_\beta(0)+h_\beta(i)=c(i,f_\beta(i))+\beta\sum_jP(j\mid i,f_\beta(i))h_\beta(j)$.
3. The limit objects: along a subsequence $\beta_n\to1$, $f_{\beta_n}\to f$, $h_{\beta_n}\to h\ge-L$ pointwise, and $(1-\beta_n)J^*_{\beta_n}(i)\to\rho^*$, a constant.
4. The average cost optimality inequality (ACOI) $\rho^*+h(i)\ge c(i,f(i))+\sum_jP(j\mid i,f(i))h(j)$.
5. An ACOI along $f$ with $h$ bounded below gives $J(i,f)\le\rho$.
6. Theorem A.2: the Abelian inequalities between Cesàro and Abel means (already on the platform).
7. $J(i,\pi)\ge\rho^*$ for every $\pi\in\Pi$.

Significance

The result. Theorem 5.9 is the standard existence theorem for average-optimal stationary policies with unbounded costs on countable state spaces. Its conditions are verified routinely for controlled queues, where relative values are monotone in the queue length and hence bounded below. It shows that randomization and memory do not reduce the long-run average cost, and the ACOI it produces is the starting point for value and policy iteration and for structural results such as threshold policies.

Formalizing it. The theorem is proved in the literature (Sennott 1989; Sennott 1999, Theorem 7.2.3; survey, p. 308). It has no machine-checked proof. The finite-action version, SennottDP.SEN.thm_7_2_3_sen_acoi, is posed on Prove2Me and still open; this mission poses the compact-action version, which needs continuity and compactness arguments that the finite case avoids. A formal proof also requires a general theory of history-dependent policies on path space (Ionescu-Tulcea), the discounted optimality equation with unbounded costs, and the passage from Abel to Cesàro means. All three are reusable well beyond this paper.

Difficulty

The obvious argument lets $\beta\to1$ in the discounted optimality equation (5.6). Two steps fail without more structure. First, $h_\beta$ need not converge, and with unbounded costs it is not uniformly bounded, so the limit has to be taken pointwise along a subsequence, with only a lower bound uniform in the state. Second, the limit cannot be passed through the infinite sum $\sum_jP(j\mid i,a)h_\beta(j)$ by dominated convergence, because no integrable dominating function exists for every action. Only an inequality survives (Fatou), so the limit is an ACOI, not an equation. The inequality then has to be turned into optimality against all of $\Pi$, which includes history-dependent randomized policies whose costs are not described by any optimality equation. The lower bound for these comes from comparing Cesàro and Abel means, not from dynamic programming.

Formalization scope

The Lean development uses the following representation and conventions.

• States, actions, model. The state space is ℕ. The action space is a metric space with its Borel σ-algebra. U i is nonempty and compact, c is measurable and nonnegative on admissible pairs, P is a Markov kernel, and $c(i,\cdot)$, $P(j\mid i,\cdot)$ are continuous on $U(i)$.
• Policies. $\Pi$ consists of all history-dependent randomized policies, with admissibility required almost surely. $J^*$ and $J^*_\beta$ are infima over all of $\Pi$, never over stationary policies only. Restricting the infimum to $\Pi_{SD}$ would drop the Tauberian half of the theorem and is not the paper's statement.
• Costs. Costs are lower Lebesgue integrals in $[0,\infty]$ against the Ionescu-Tulcea path measure, and the average cost is a limsup in $[0,\infty]$.
• Explicit hypotheses. $h_\beta$ is a difference of real parts and is used only under Assumption 5.14, so it is never read off an infinite $J^*_\beta$. The quantifiers over $i$ and $\beta$ in Assumption 5.15, implicit on the page, are universal, and $L$ is a natural number as printed. Every series $\sum_jP(j\mid i,a)h(j)$ carries a summability hypothesis or conclusion.
• Corrected claim. Remark 5.8(a) as printed claims that any scalar $\rho$ satisfying the ACOI with $h$ bounded below is the optimal average cost. That is false ($h\equiv0$, $\rho=\sup c$), so only the inequality $J(i,f)\le\rho$, which the proof uses, is stated.
• Sequences. The milestones about limits are stated for any sequence $\beta_n\in(0,1)$ with $\beta_n\to1$, not only increasing ones.

A trivializing formalization is excluded. Sennott's conditions are satisfiable (a one-action, zero-cost model satisfies all three), and AC-optimality is measured against all admissible policies, so the goal cannot hold vacuously or by a junk value.

Welcome contributions: the Markov property of the path measure for history-dependent policies; the discounted optimality equation for nonnegative unbounded costs; a measurable-selection or compactness argument for minimizing actions on compact $U(i)$; Fatou's lemma for series with converging weights; and the Abelian inequalities in a form applied to expected costs.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM J. Control Optim. 31(2) (1993) 282–344. https://doi.org/10.1137/0331018
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Oper. Res. 37(4) (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
• L. I. Sennott, A new condition for the existence of optimal stationary policies in average cost Markov decision processes, Oper. Res. Lett. 5 (1986) 17–23 (reference [155] of the survey; no stable link checked).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, New York, 1983 (reference [150] of the survey).
• A. Federgruen, A. Hordijk, H. C. Tijms, Denumerable state semi-Markov decision processes with unbounded costs, average cost criterion, Stochastic Process. Appl. 9 (1979) 223–235 (reference [53] of the survey).
• R. Sznajder, J. A. Filar, Some comments on a theorem of Hardy and Littlewood, J. Optim. Theory Appl. 75 (1992) (reference [176] of the survey, cited for Theorem A.2).