The OR Formalization Drive

Motivation

Dynamic pricing under limited inventory is a core problem of revenue management: a seller holds $C_0$ units of a perishable product (airline seats, hotel rooms, seasonal goods) and must choose prices over a finite selling horizon while demand is random and responds to price. The exactly optimal policy solves a stochastic dynamic program whose state is the remaining inventory, and it changes the price after every sale. In practice sellers often prefer a simpler rule, fixed in advance: solve the deterministic version of the problem, in which random demand is replaced by its mean, and charge the resulting prices whatever happens.

Gallego and van Ryzin (Management Science 1994) showed that in continuous time with Poisson demand this fixed-price heuristic is asymptotically optimal, and bounded its relative loss by the coefficient of variation of demand. Bitran and Caldentey's survey (MSOM 2003, §3.2.1) extends this bound to a discrete-time, periodic-review model with general demand distributions, as Proposition 8, proved in the paper's Appendix. The proof combines three ingredients: a Lagrangian duality argument showing that the deterministic problem is an upper bound on the optimal expected revenue, a sample-path comparison of lost sales, and a distribution-free moment bound of Gallego (1992) on $E[(X-C)^+]$.

Setting

A single product is sold over $N \ge 1$ periods $n = 1, \dots, N$ starting from inventory $C_0$. In period $n$ the seller charges a price $p \ge 0$, and the demand $D_n(p)$ is a nonnegative random variable with finite mean $E[D_n(p)]$, whose law may depend on $n$ and $p$ arbitrarily. With inventory $C$ the seller sells $\min\{D, C\}$ units; unmet demand is lost.

The optimal expected revenue $V_1(C_0)$ is defined by the Bellman recursion $V_{N+1} \equiv 0$,

$$V_n(C) = \sup_{p \ge 0} E\big[p\min\{D_n(p), C\} + V_{n+1}\big(C - \min\{D_n(p), C\}\big)\big].$$

The deterministic problem (32)–(33) is

$$V_1^{\det}(C_0) = \sup_{p \in [0,\infty)^N} \sum_{n=1}^N p_n E[D_n(p_n)] \quad \text{subject to} \quad \sum_{n=1}^N E[D_n(p_n)] \le C_0,$$

and $p^{\det}$ denotes an optimal solution. The deterministic-price heuristic charges $p^{\det}_n$ in period $n$ regardless of sales. Its period demands $D_n(p_n^{\det})$ are independent, $\mathscr{D}_n^{\det} = \sum_{i=1}^n D_i(p_i^{\det})$ is the cumulative demand, and its expected revenue is

$$V_1(p^{\det}, C_0) = \sum_{n=1}^N p_n^{\det} E\Big[D_n(p_n^{\det}) - \big(D_n(p_n^{\det}) - (C_0 - \mathscr{D}_{n-1}^{\det})^+\big)^+\Big].$$

With $\sigma_n^2 = \operatorname{Var}(\mathscr{D}_n^{\det})$, eq. (34) defines

$$\eta_n^{\det}(C_0) = \frac{\sqrt{\sigma_n^2 + (C_0 - E[\mathscr{D}_n^{\det}])^2} - (C_0 - E[\mathscr{D}_n^{\det}])}{2},$$

and $\nu(C_0) = \sigma_N / E[\mathscr{D}_N^{\det}]$ is the coefficient of variation of the total demand.

Formalization targets

Goal: Proposition 8, eq. (35)

Assume that $p \mapsto p\,E[D_n(p)]$ is concave and $p \mapsto E[D_n(p)]$ is convex on $[0,\infty)$ for each $n$, that some price $p^\infty \ge 0$ has $\sum_n E[D_n(p^\infty)] < C_0$, and that $p^{\det}$ is optimal for (32)–(33). Then

$$1 \ge \frac{V_1(p^{\det}, C_0)}{V_1(C_0)} \ge \frac{1}{V_1^{\det}(C_0)} \sum_{n=1}^N p_n^{\det} E[D_n(p_n^{\det})]\left(1 - \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}\right) \ge 1 - \max_n \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}.$$

The constants are the paper's, and the goal is the full chain.

Milestones

1. Gallego's bound (Appendix, (*)): for square-integrable $X$, $E[(X - C)^+] \le \frac12\big(\sqrt{\operatorname{Var}X + (C - EX)^2} - (C - EX)\big)$, which is at most $\frac12\sqrt{\operatorname{Var} X}$ when $EX \le C$.
2. Eq. (24): in one period, $E[p\min\{D(p), C\}] \le p\min\{E[D(p)], C\}$, so $V(C) \le V^{\det}(C)$.
3. Proposition 6, eq. (26): in one period, $V(C, p^{\det})/V(C) \ge 1 - \nu^{\det}/2$.
4. $V_1^{\det}$ is concave in the capacity (first sentence of the Appendix proof).
5. Proposition 8, first assertion: $V_1(C_0) \le V_1^{\det}(C_0)$.
6. The Appendix display bounding $V_1(p^{\det}, C_0)$ below by $\sum_n p_n^{\det}E[D_n](1 - E[(\mathscr{D}_n^{\det} - C_0)^+]/E[D_n])$.
7. Eq. (36), after the goal: if $E[D_n(p)] = T_n\lambda(p)$, one constant price solves (32)–(33) and $1 \ge V_1(p^{\det},C_0)/V_1(C_0) \ge 1 - \nu(C_0)/2$.

Significance

The result gives a guarantee for a pricing policy that needs no inventory tracking: its relative loss is controlled by the first two moments of cumulative demand, with no distributional assumption beyond finite variance. When demand grows while its coefficient of variation shrinks, as for sums of independent period demands, the guarantee tends to one, which is the discrete-time form of asymptotic optimality of fixed prices. The upper bound $V_1 \le V_1^{\det}$ is used throughout revenue management as the benchmark for heuristics (fluid or deterministic LP bounds).

The paper's proof is complete in the Appendix, and the mathematics is not in question beyond minor typos. None of it is machine-checked. A formal development adds a checked Bellman model of periodic-review pricing with general demand laws, a checked fluid upper bound for it, and a checked form of Gallego's moment bound, all reusable for other revenue-management statements. A related platform theorem, RevenueManagement.deterministic_upper_bound (mission The Theory and Practice of Revenue Management III), states the deterministic bound for a Bernoulli-arrival model with at most one sale per period; the model here is different (arbitrary demand laws, continuous inventory), and neither statement implies the other.

Difficulty

The upper bound $V_1(C_0) \le V_1^{\det}(C_0)$ is the hard part. The natural induction replaces $V_2$ by $V_2^{\det}$ and applies Jensen's inequality, but $V_2^{\det}(C)$ is $-\infty$ at capacities where the remaining deterministic problem is infeasible, while $V_2(C)$ stays nonnegative. The induction therefore fails as stated when mean demand never vanishes. The paper's argument also passes through the Lagrangian dual of (32)–(33), and strong duality for that program on $[0,\infty)^N$ under the Slater point $p^\infty$ is not available in Mathlib in this form.

The lower bound is less deep but technical: it needs the product law of the period demands, linearity of expectation for truncated sums, and variances of partial sums. Gallego's inequality is elementary once the right quadratic bound on $(x - C)^+$ is found, but it is not in Mathlib.

Formalization scope

• Periods are Fin N, 0-based. Demand laws are μ n p : Measure ℝ, probability measures carried by $[0,\infty)$ with finite mean, required at every price (laws at negative prices never enter a statement).
• The Bellman value is computed in $[0,\infty]$ with the lower Lebesgue integral and ⨆ over $p \ge 0$, so no supremum takes a junk value; the paper's $V_n$ is valueToGo M (N - n + 1). Ratios use its real value.
• $V_1^{\det}$ is an EReal supremum over the feasible set ($-\infty$ if infeasible). In the goal $p^{\det}$ is an optimal solution, so $V_1^{\det}(C_0)$ is its objective value.
• The heuristic's demands are independent: the joint law is the product measure.
• Implicit hypotheses made explicit: "concave objective and convex feasible region" is read as concavity of $p\,E[D_n(p)]$ and convexity of $E[D_n(p)]$ on $[0,\infty)$, the latter making (33) convex for every capacity; existence of the optimal deterministic solution; finite variance and positive mean of each $D_n(p_n^{\det})$; and $V_1^{\det}(C_0) > 0$, without which the ratios are $0/0$.
• The typo $\mathscr{D}_n^{\det} := \sum_{i=1}^n D_n(p^{\det})$ on p. 221 is read as $\sum_{i=1}^n D_i(p_i^{\det})$.

Trivializing formalizations ruled out: $V_1$ is defined by the Bellman recursion, not as a supremum over an unspecified policy class or as a variable constrained by hypotheses; $\eta_n^{\det}$ is the expression (34), not a hypothesis-supplied bound on expected overflow; the goal does not assume strong duality or a Lagrange multiplier, since that is the proof's key step; independence is built into the joint law, not assumed as an inequality; variances are taken only under square integrability, since Mathlib's variance is $0$ for infinite variance.

Needed infrastructure: measurability of the Bellman integrand (monotonicity of $V_n$ in inventory), Jensen's inequality for $\min\{\cdot, C\}$ (ConcaveOn.le_map_integral), Lagrangian strong duality for a separable concave program with one convex constraint, marginals and variances of sums under Measure.pi, and Gallego's bound. The duality and moment results are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the upper bound, are welcome.

Selected references

• G. R. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–230, 2003. https://doi.org/10.1287/msom.5.3.203.16061
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11(1):55–60, 1992 (as cited in Bitran and Caldentey 2003).
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993.

Motivation

Mission IX (09-proportional-fairness-core) formalized proportional fairness (PF) as a control policy and proved the technical core of its stability theory: under a load condition, the PF fluid model is stable (Theorem 10.5), via an entropy Lyapunov function that is genuinely not Lipschitz continuous — a departure from every other stability argument in J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org). A stability theorem for one fixed arrival-rate vector is, on its own, a narrower claim than practitioners actually want: real systems see load that changes over time, and a control policy worth adopting should not need re-tuning every time the mix of traffic shifts. This mission completes Theorem 10.5's proof and turns it into exactly that stronger guarantee — proportional fairness is maximally stable: stable throughout the entire region where any policy could be stable, without knowing the arrival rates in advance — and specializes the result to two concrete network families, bandwidth-sharing networks and queueing networks under head-of-line proportional processor sharing (HLPPS), that were already familiar from earlier in the book under different control policies.

Setting

Fix a unitary network operating under PF control with mean service times $m > 0$, routing matrix $P$, a partition of job classes into demand groups $\{\mathcal I(\ell), \ell \in \mathcal L\}$, and a reduced allocation set $\tilde{\mathcal A} \subset \mathbb R^{\mathcal L}_+$ (all restated from mission IX, Definition 10.3). The entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38, mission IX) admits an alternative decomposition $\varphi = \sum_\ell \varphi_\ell$ in terms of the within-group entropy term

$$f(t) := \sum_{\ell\in\mathcal L}\sum_{i\in\mathcal I(\ell)} Z_i(t)\log\!\left(\frac{Z_i(t)}{Y_\ell(t)}\right), \qquad Y(t) := GZ(t) \quad \text{(Eq. 10.50)},$$

with the convention that the term for class $i$ is $0$ when $Z_i(t)=0$. Here $D^+$/$D^-$ denote the upper-right/upper-left Dini derivatives (Appendix A.4, Eqs. A.9-A.10): at a point where the ordinary derivative may not exist, these one-sided $\limsup$s still let a Lyapunov-drift argument go through. A control policy is maximally stable (Section 5.7) for a network if its implementation does not depend on the arrival-rate vector $\lambda$ and it is stable for every $\lambda$ in the network's stability region $\Lambda^*$ — the largest region any policy could possibly stabilize.

Formalization targets

Goal: Corollary 10.16 — maximal stability of PF control for a unitary network

$$\text{IsMaximallyStable}\Big(\lambda \mapsto \text{PFFluidStable}(\lambda, m, P, \mathrm{grp}, \tilde{\mathcal A})\Big)$$

for the single PF policy value (its implementation never depends on $\lambda$). This is the applied payoff of Theorem 10.5 (mission IX): combined with Theorem 6.2 (mission III, fluid stability implies SPN stability) and Corollary 5.6 (mission II, a $\lambda$-independent policy stable throughout the subcritical region is automatically maximally stable), it upgrades a single-$\lambda$ stability statement to the strongest form the book's own framework can express.

Supporting milestones

Lemmas 10.11-10.15 supply the remaining technical content of Theorem 10.5's proof that mission IX's own milestones left open: Lemma 10.11 is the uniform negative-drift bound $\sum_i \dot Z_i(t)\log(\dot D_i(t)/\alpha_i) \le -\varepsilon$ at every regular point with $Z(t) \ne 0$; Lemmas 10.12-10.14 establish continuity and two successively sharper Dini-derivative bounds on the within-group entropy term $f$; Lemma 10.15 shows that positivity of the departure rate $\dot D_i(t)$ propagates from occupied classes to every class. Corollaries 10.17 and 10.18 specialize the goal to bandwidth-sharing networks and to HLPPS-controlled queueing networks, respectively.

Significance

The result itself. A stability theorem tied to one fixed $\lambda$ is of limited practical use: it would need to be re-verified every time the arrival-rate vector changes, which real traffic does constantly. Maximal stability removes that dependency entirely — a single policy, implemented without any knowledge of $\lambda$, is guaranteed stable throughout the full region any control could stabilize. Corollaries 10.17 and 10.18 make this concrete for two network families with independent histories in the literature: bandwidth-sharing networks (the original motivation for proportional fairness, Kelly 1997) and queueing networks under HLPPS, connecting PF's static, utility-theoretic motivation to a scheduling rule that predates it.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=maximal%20stability, q=bandwidth%20sharing) finds no relevant hits on the platform. This mission formalizes the remaining entropy-Lyapunov lemmas, the within-group entropy term, the BWS and HLPPS network models (restated locally, since no other drafted chunk covers Sections 4.5-4.6), and the maximal-stability predicate, reusing only Mathlib's general real-analysis substrate (Dini derivatives via Filter.limsup) and definitions restated from missions II, III, V, and IX under this series' restate-not-import convention for concurrently-drafted chunks.

Difficulty

The obvious approach to Corollary 10.16 — restate "maximally stable" with an explicit $\lambda$-dependent policy family and add "the policy doesn't actually depend on $\lambda$" as a side hypothesis — obscures the point: a policy that is definitionally independent of $\lambda$ is a stronger and cleaner claim than one that happens to satisfy an extra equation. This formalization instead instantiates the abstract policy type at Unit, so $\lambda$-independence holds by construction rather than as a hypothesis to verify, matching the book's own reading of Section 5.7's definition. A second difficulty is Lemma 10.13's Dini-derivative inequality (Eq. 10.56): the plain-text extraction of this display equation loses bracket and subscript structure that changes its meaning, so the exact grouping was confirmed against the PDF page directly and cross-checked against the book's own re-derivation of the same bracketed expression inside Lemma 10.14's proof. A third is Corollary 10.17's proof, which genuinely depends on three facts outside this chunk's own chapter portion (Proposition 4.4 and the Section 4.4 model translation, Proposition 5.1, Theorem 5.2); rather than silently assuming them or re-deriving their proofs from scratch, they are stated as explicit hypotheses of the milestone itself, so the item's actual content — deriving the two-sided conclusion — is exactly what remains to be proved.

Formalization scope

RestatedCore, RestatedFluidModel, and the maximal-stability predicate MaximalStability are restated verbatim (or, for MaximalStability, in shape) from missions IX, III/V, and II respectively, since concurrently-drafted chunks in this series do not import one another's Lean files even when they share a sub-namespace. New to this chunk: diniUpperLeft (Eq. A.10, needed alongside mission IX's diniUpperRight for Lemma 10.13's two-sided bound), the within-group entropy term withinGroupEntropy (Eq. 10.50, deliberately not named f, since the book's own f already denotes the unrelated PF optimization objective of Eq. 10.2 within the same chapter), and BWSNetworkData/QueueingNetworkDataHL/HLPPSFluidStable (Sections 4.5-4.6, restated locally since no drafted chunk's BRIEF.md covers them). The formalization does not admit a trivializing reading: IsMaximallyStable is instantiated with the genuine, non-vacuous predicate PFFluidStable/HLPPSFluidStable — the same predicate whose stability Theorem 10.5 (mission IX) already establishes on the load-condition region — never with a policy type or stability predicate engineered to make the maximal-stability claim vacuous. Contributions completing the eight by sorry proofs are welcome, particularly Lemma 10.13's Dini-derivative estimate (Section B.4's preliminary results) and Lemma 10.15's connectivity argument (Appendix B.9/B.17).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33–37.
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.

Motivation

An inventory manager who stocks many products, faces random demand and pays ordering, holding and shortage costs must decide each period how much of each product to order. In general the optimal decision depends on the whole state and is found by solving a dynamic programme, which becomes impractical as the number of products grows. Myopic (or base stock) policies avoid this: in each period they aim at a target level computed from that period's data alone. Knowing when such a policy is optimal over an infinite horizon tells a practitioner when the multi-period problem decouples into a sequence of one-period problems.

Arthur F. Veinott, Jr. gave such conditions in Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem (Management Science 12(3):206–222, 1965). Earlier results of this type were for a single product (the paper cites Karlin, Management Science 6(3), 1960, Bellman–Glicksberg–Gross, Management Science 2(1), 1955, Iglehart–Karlin 1962, and the Arrow–Karlin–Scarf volume of 1958); Veinott's model allows several products, several demand classes, costs and demand distributions that change over time, general ordering constraints and general stock dynamics (backlogging, lost sales, and mixtures), and it does not use the functional equation of dynamic programming. Instead, the proofs analyse the inventory process directly.

Setting

There are $n$ products and $m$ demand classes. Vectors are compared componentwise: $u \le v$ means $u_j \le v_j$ for all $j$. In period $i = 1, 2, \dots$ the manager observes the inventory vector $x_i \in X_i \subseteq \mathbb{R}^n$ (negative coordinates are backlogs) and orders up to a vector $y_i \in Y_i \subseteq \mathbb{R}^n$, subject to $y_i \ge q_i(x_i)$, where $q_i$ is a vector of extended-real functions (for instance $q_i(x) = x$ forbids disposal). A random demand vector $D_i$ with law $\Phi_i$ and values in a Borel set $\mathfrak{D}_i \subseteq \mathbb{R}^m$ then occurs, and the next inventory vector is $x_{i+1} = s_i(y_i, D_i) \in X_{i+1}$. The demands $D_1, D_2, \dots$ are independent. Ordering $y_i - x_i$ costs $c_i \cdot (y_i - x_i)$, the holding and shortage cost is $g_i(y_i, D_i)$, and $\alpha_i \ge 0$ is the discount factor of period $i$.

Regrouping the ordering costs gives the one-period cost

$$W_i(y,t) = c_i\, y + g_i(y,t) - \alpha_i\, c_{i+1}\, s_i(y,t), \qquad G_i(y) = \int_{\mathfrak{D}_i} W_i(y,t)\, d\Phi_i(t),$$

with discount weights $\beta_1 = 1$ and $\beta_i = \alpha_1 \cdots \alpha_{i-1}$. The integrals are assumed finite, and $G_i \ge \gamma_i$ with $\sum_i |\beta_i \gamma_i| < \infty$. An ordering policy $\bar Y$ chooses $y_i$ as a Borel function of the past; it is feasible if $y_i \in Y_i$ and $y_i \ge q_i(x_i)$ for every possible history. Its cost is

$$f(x_1 \mid \bar Y) = \sum_{i=1}^\infty \beta_i\, E\, G_i(y_i) \in (-\infty, +\infty],$$

and a feasible policy of least cost is optimal.

Let $\bar y_i$ minimize $G_i$ over $Y_i$. When $\bar y_i$ is not attainable from $x$, the minimal feasible level $w_i(x)$ is the least element of $Y_i \cap \{y : y \ge q_i(x),\ y \ge \bar y_i\}$. The base stock ordering policy orders up to $\bar y_i$ if $q_i(x_i) \le \bar y_i$ and up to $w_i(x_i)$ otherwise.

Formalization targets

The hypotheses are: (3a) $\bar y_i \in Y_i$ minimizes $G_i$ over $Y_i$; (3b) $q_{i+1}(s_i(\bar y_i, t)) \le \bar y_{i+1}$ for $t \in \mathfrak{D}_i$; (3c) $Y_i$ is closed and linearly ordered by $\le$; (3d) $G_i$ and $s_i(\cdot, t)$ are nondecreasing on $\{y \in Y_i : y \ge \bar y_i\}$, and $q_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$.

Goal: Theorem 3.2

Under (3a)–(3d), the base stock ordering policy

$$\bar Y_i^*(H_i^*) = \begin{cases} \bar y_i, & q_i(x_i^*) \le \bar y_i, \\ w_i(x_i^*), & q_i(x_i^*) \not\le \bar y_i \end{cases}$$

is feasible and optimal: $f(x_1 \mid \bar Y^*) \le f(x_1 \mid \bar Y)$ for every feasible $\bar Y$.

Milestones

1. A nonempty, closed, linearly ordered, bounded-below subset of $\mathbb{R}^n$ has a least element (p. 212); hence $w_i(x)$ exists and equals $\bar y_i$ when $q_i(x) \le \bar y_i$.
2. $w_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$ (p. 214).
3. Once $q_k(x_k^*) \le \bar y_k$, the base stock policy orders up to $\bar y_i$ for all $i \ge k$.
4. Theorem 3.1: under (3a) and (3b), if $q_1(x_1) \le \bar y_1$, ordering up to $\bar y_i$ in every period is optimal, with cost $\sum_i \beta_i G_i(\bar y_i)$.
5. The coupling (3.1): before the first period $T$ with $q_T(x_T^*) \le \bar y_T$,

$$\bar y_i < y_i^* = w_i(x_i^*) \le w_i(x_i) \le y_i.$$

6. Pathwise dominance: $G_i(y_i^*) \le G_i(y_i)$ for every $i$ and every possible demand path.
7. The reduction behind (2.3): $E\, W_i(y_i, D_i) = E\, G_i(y_i)$, by independence of $y_i$ and $D_i$.

Significance

The theorem shows that under (3a)–(3d) the infinite-horizon, nonstationary, multi-product problem is solved by one-period optimization: compute $\bar y_i$ from $G_i$ alone, and when it is unreachable order the least feasible amount. No value function is computed. It covers backlogging and lost sales, products stocked in fixed proportions, and time-varying cost and demand data, and Theorem 3.1 alone settles the frequent case in which the initial stock is small.

The result is proved in the paper. To our knowledge it has not been machine-checked: this mission produces a Lean model of a general stochastic, infinite-horizon, multi-product inventory problem (feasible policies, the expected discounted cost with $+\infty$ allowed), and a checked proof that a myopic policy is optimal in it. The model and its cost are reusable for other base stock and myopic optimality results.

Difficulty

The obvious argument would compare the base stock policy with an arbitrary policy period by period using (3a) alone. That fails once $\bar y_i$ is unreachable. The base stock policy then holds less stock than $\bar y_i$ would require, and it has to be shown that no other policy can reach a lower-cost level later. The proof couples the two trajectories along every demand path, using the monotonicity in (3d) and the linear order of $Y_i$ from (3c), until the base stock level becomes attainable, after which (3b) keeps it attainable. The formal difficulties are:

• the existence and monotonicity of the least element $w_i(x)$ in a closed chain of $\mathbb{R}^n$;
• the measurability of the base stock policy, which is part of its feasibility;
• the passage from pathwise dominance to the expected discounted cost when the cost may be $+\infty$.

Formalization scope

Periods are 0-based in Lean (Lean period $k$ is the paper's period $k+1$). Vectors are Fin n → ℝ with the product order; $q_i$ takes values in Fin n → EReal. Policies are functions of the past demands. The paper shows on p. 219 that this loses no generality once $x_1$ is fixed. The cost is excess, a $[0,\infty]$-valued series of lower Lebesgue integrals of $\beta_i(G_i(y_i) - \gamma_i)$, plus the finite real $\sum_i \beta_i\gamma_i$, taken in EReal. A divergent series therefore gives $+\infty$ and never the junk value $0$. "Minimal element" is IsLeast. The $G_i$ in the statements is the integral of $W_i$ built from the data, and the policy in the goal is constructed from $\bar y$, $q$, $w$ and $s$. Neither is an arbitrary object satisfying the conclusion. The goal concludes optimality, which includes feasibility: a pathwise or conditional statement would not be the theorem.

Hypotheses added relative to the page, each used by the paper without being stated:

• Order feasibility: from every $x \in X_i$ some $y \in Y_i$ with $y \ge q_i(x)$ exists (p. 212 asserts the set defining $w_i(x)$ has a minimal element, which needs it nonempty). The least-element lemma likewise assumes $A$ nonempty.
• (3d)'s $q$-clause in one-sided form: if $x \le x'$ in $X_i$ and $q_i(x) \not\le \bar y_i$, then $q_i(x) \le q_i(x')$. This is the form the proof on p. 214 uses; monotonicity on the region $\{q_i(x) \not\le \bar y_i\}$ alone admits a counterexample to Theorem 3.2.
• Integrability of $W_i(y_i, D_i)$ in the milestone $E W_i = E G_i$.
• Borel measurability of $q_i$ on all of $\mathbb{R}^n$ rather than on $X_i$ (a harmless strengthening).

A complete development needs: least elements of closed chains in $\mathbb{R}^n$; measurability of the least-element selection $x \mapsto w_i(x)$; a Fubini/independence argument for $E\,W_i(y_i,D_i)=E\,G_i(y_i)$; and monotone summation of lower integrals. The least-element lemma and the cost encoding are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments.

Selected references

• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• R. Bellman, I. Glicksberg, O. Gross, On the Optimal Inventory Equation, Management Science 2(1):83–104, 1955. https://doi.org/10.1287/mnsc.2.1.83
• S. Karlin, Dynamic Inventory Policy with Varying Stochastic Demands, Management Science 6(3):231–258, 1960. https://doi.org/10.1287/mnsc.6.3.231

Motivation

Large-scale data-intensive computing splits a job into many small "map tasks," each of which must be assigned to one of thousands of general-purpose servers in a data center — the MapReduce paradigm introduced by Dean and Ghemawat (2008). Because a task's input data is stored on only a few of those servers, routing it to a server that already holds its data ("data locality") avoids costly network transfer, so a task-allocation policy that ignores locality can leave a server farm badly underutilized even when raw compute capacity is ample. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 11 to a rigorous stability analysis of Xie, Yekkehkhany, and Lu's (2016) workload-weighted task allocation (WWTA) policy, which routes each arriving task to whichever eligible server currently carries the least (locality-weighted) backlog. This mission formalizes the chapter's central result: WWTA is not merely a reasonable heuristic but is maximally stable — it keeps the system stable whenever any routing policy could.

Setting

A task allocation model (Sections 11.2-11.3) has L task categories and K servers; a class is a pair $(\ell,k)$, a category routed to a specific server, with mean service time $m_{\ell k} > 0$ (Eq. 11.3) reflecting both data locality (local, rack-local, or remote access) and the server's relative processing speed. Tasks in category $\ell$ arrive according to a Markovian arrival process (MArP) with long-run average rate $\nu_\ell$ — a substantially more general model than the independent Poisson streams used elsewhere in the book, needed to capture batches of map tasks generated from a single job. Routing is by immediate commitment: each task is assigned to a server the instant it arrives, based only on its category and the current backlog, with no possibility of later reassignment. The workload of server $k$ at time $t$ (Eq. 11.7) is $W_k(t) := \sum_\ell m_{\ell k} Z_{\ell k}(t)$, the locality-weighted total backlog assigned to it. Workload-weighted task allocation (WWTA), Definition 11.3, routes an arriving category-$\ell$ task to any server achieving $\operatorname{argmin}_{k} m_{\ell k} W_k(t-)$ (Eq. 11.8, ties broken arbitrarily), where $W(t-)$ is the workload vector's left limit at the arrival instant.

Formalization targets

Goal: Theorem 11.6 — WWTA fluid model stability under the load condition

If there exists $\lambda = (\lambda_{\ell k}) \ge 0$ with $\sum_k \lambda_{\ell k} = \nu_\ell$ for each category (Eq. 11.4) and $\sum_\ell m_{\ell k}\lambda_{\ell k} < 1$ for each server (Eq. 11.5), then the WWTA fluid model — the deterministic fluid equations (11.11)-(11.16) that arise as scaling limits of the stochastic model under WWTA control — is stable: every solution reaches the zero state in finite time proportional to its initial size.

Supporting milestones

Lemma 11.2 shows this load condition is equivalent to subcriticality of the task allocation model, in the sense of Section 5.2's general definition, reducing an existence statement over the model's full $G,R,A,b$ apparatus to a simple linear-feasibility check. Theorem 11.4 establishes that fluid limits of the stochastic model exist and satisfy the general fluid equations (11.11)-(11.15) under any immediate-commitment routing policy, and the WWTA-specific equation (11.16) under WWTA — the chapter's version of the fluid-limit machinery Chapter 6 builds for the book's standard model, adapted to Markovian (not Poisson) arrivals and immediate-commitment routing. Theorem 11.5 is the corresponding replacement for Theorem 6.2 (mission III): fluid limit stability implies stability of the original stochastic model. Corollary 11.7 is the mission's other headline consequence: WWTA is maximally stable, stabilizing the model whenever any simply structured routing policy could.

Significance

The result itself. A task-allocation heuristic motivated purely by an intuitive "balance-the-weighted-backlog" idea turns out to have the strongest stability guarantee a policy can have: it never needs re-tuning as arrival rates change, and no alternative policy can stabilize a regime WWTA cannot. Xie, Yekkehkhany, and Lu (2016) proved this fact (calling it "throughput optimality") by direct analysis of the discrete stochastic model using a quadratic Lyapunov function; Dai and Harrison's contribution is to prove the same conclusion via the fluid-model route, and — because the task allocation model violates two of the standing assumptions under which Chapter 6's general theory was built (MArP rather than Poisson arrivals, immediate-commitment routing rather than the book's default relaxed control) — to show that the general fluid-stability machinery survives those changes with only minor modification.

Formalizing it. A live prior-art check (GET /theorems?q=task+allocation, q=server%20farm, q=data%20locality) finds no relevant hits on the platform (workload returns one unrelated text-corpus-statistics result). This mission formalizes the task allocation model, WWTA, the fluid equations, and the stochastic-to-fluid bridge from scratch, reusing Mathlib's general real-analysis, measure-theory, and PMF-based Markov-chain substrate, and restating (per this series' convention for concurrently-drafted chunks) the minimal apparatus needed from missions I and III.

Difficulty

The obvious approach to Definition 11.3 — pick a canonical minimizer of $m_{\ell\cdot}W_\cdot(t-)$, e.g. via Finset.min' — silently narrows WWTA to a single tie-breaking rule, when (11.8) explicitly allows any minimizer; this mission instead states WWTA as domination over every server, accepting every admissible tie-break. A second difficulty is genuinely structural: Theorem 11.4's "for almost all $\omega$" existence claim is a measure-theoretic statement about a probability space that mission III's own analogous Theorem 6.5 sidesteps by fixing a sample point $\omega$ together with the specific SLLN limit that argument needs — this mission follows the same precedent rather than introducing a bare "almost everywhere" quantifier, which does not by itself supply the type information Lean's typeclass resolution needs to identify an ambient measure. A third is connecting Definition 11.3's discrete, arrival-indexed routing rule to the raw (pre-limit) process family that Theorem 11.4's existence argument operates on: the book's own proof derives the needed consequence (Eq. 11.22, "server $k$ receives no more category-$\ell$ tasks in a neighbourhood of $t$") via an explicit $\varepsilon$-$\delta$ argument from the discrete policy, which this mission takes as a documented hypothesis rather than re-deriving, since building the arrival-sequence-to-counting-process reconstruction is genuinely Chapter 2/4 machinery outside this chapter's own numbered results.

Formalization scope

Classes are represented as pairs (ℓ,k) : Fin L × Fin K rather than flattened to a single index, avoiding an arbitrary choice of encoding. TaskAllocationProcessFamily, FluidLimitPath, and TaskAllocationFluidLimitStable restate mission III's SPNProcessFamily/FluidLimitPath/ FluidLimitStable apparatus, adapted to this model's (E,D,Z) triple and doubly-indexed classes; PositiveRecurrent restates mission I's renewal-theoretic positive-recurrence notion. The formalization does not admit a trivializing reading: IsWWTA accepts every admissible tie-break rather than a single canonical one, SatisfiesWWTAFluidEquation requires Nonempty (Fin K) so its min_{k} is a genuine minimum rather than a junk value at zero servers, and the goal's conclusion WWTAFluidStable is the same non-vacuous fluid-model-stability predicate (Definition 6.3, specialized) used throughout this series. Contributions completing the five by sorry proofs are welcome, particularly Theorem 11.4's fluid-limit compactness argument (mirroring mission III's own Theorem 6.5 proof) and Theorem 11.6's explicit quadratic-Lyapunov-function argument.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. Dean and S. Ghemawat, "MapReduce: simplified data processing on large clusters," Communications of the ACM 51 (2008), 107–113.
• Q. Xie, A. Yekkehkhany, and Y. Lu, "Scheduling with multi-level data locality: throughput and heavy-traffic optimality," IEEE INFOCOM 2016.

Motivation

Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).

In data-driven problems the situation is different: the parameters $x_1,\dots,x_n$ are samples, and all of them lie in the same space $\mathbb R^m$. Robustifying each sample by its own uncertainty set $\mathcal Z_i$ gives the objective $\sum_i c_i\inf_{x_i\in\mathcal Z_i}f(x_i)$, and the sets $\mathcal Z_i$ typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on $\mathbb R^m$ itself rather than on $\mathbb R^{m\times n}$. This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.

Setting

Let $m,n\ge1$ and write $[1:n]=\{1,\dots,n\}$. Let $\mathcal P$ be the set of Borel probability measures on $\mathbb R^m$. The data are:

• a measurable utility $f:\mathbb R^m\to\mathbb R$ (the decision variable is suppressed);
• weights $c_1,\dots,c_n>0$ with $\sum_{i=1}^n c_i=1$;
• nonempty Borel uncertainty sets $\mathcal Z_1,\dots,\mathcal Z_n\subseteq\mathbb R^m$, which may intersect or coincide.

For $S\subseteq[1:n]$ write $\mathcal Z_S=\bigcup_{i\in S}\mathcal Z_i$ and $N=[1:n]$. The distribution set is

$$\mathcal P_n=\Big\{\mu\in\mathcal P\ \Big|\ \forall S\subseteq[1:n]:\ \mu(\mathcal Z_S)\ge\sum_{i\in S}c_i\Big\}.$$

Each $\mu\in\mathcal P_n$ must give every union of uncertainty sets at least the total weight of its indices. For $\mu\in\mathcal P$ the expectation $\int f\,d\mu$ is the extended integral $\int f^+d\mu-\int f^-d\mu\in[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 2.1 (Eq. (4), pp. 96–97)

$$\sum_{i=1}^n\Big[c_i\inf_{x_i\in\mathcal Z_i}f(x_i)\Big]=\inf_{\mu\in\mathcal P_n}\int_{\mathbb R^m}f(x)\,d\mu(x),$$

as an identity in $[-\infty,+\infty]$, with no boundedness assumption on $f$ and no disjointness assumption on the $\mathcal Z_i$.

Milestones (proof of Theorem 2.1, p. 97)

1. Every $\mu\in\mathcal P_n$ satisfies $\mu(\mathbb R^m\setminus\mathcal Z_N)=0$, hence $\int_{\mathbb R^m}f\,d\mu=\int_{\mathcal Z_N}f\,d\mu$.
2. Weak duality. With $f_i=\inf_{\mathcal Z_i}f$ finite, every $\alpha\in\mathbb R^{2^n}$ satisfying $\sum_S\alpha_S\mathbf 1(x\in\mathcal Z_S)\le f(x)$ on $\mathcal Z_N$ and $\alpha_S\ge0$ for $S\ne N$ obeys $\sum_i c_i\sum_S\alpha_S\mathbf 1(i\in S)\le\sum_i c_if_i$.
3. The nested dual solution. If $f_1\ge\dots\ge f_n$, the vector with $\alpha_{\{1,\dots,i\}}=f_i-f_{i+1}$, $\alpha_N=f_n$ and all other coordinates $0$ is feasible and has objective $\sum_i c_if_i$.

Further statements

• For pairwise disjoint $\mathcal Z_i$: $\mathcal P_n=\{\mu\in\mathcal P\mid\mu(\mathcal Z_i)=c_i,\ i=1,\dots,n\}$ (p. 97).
• Corollary 2.1 (Eq. (5)): $\inf_{x'\in\mathcal Z}f(x')=\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z)=1}\int f\,d\mu$.
• Corollary 5.2 (nested distributions, p. 107): for $\mathcal Z_1\subseteq\dots\subseteq\mathcal Z_n$ and $0=p_0<p_1<\dots<p_n=1$,

$$\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z_i)\ge p_i\ \forall i}\int f\,d\mu=\sum_{i=1}^n(p_i-p_{i-1})\inf_{x_i\in\mathcal Z_i}f(x_i).$$

Significance

The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space $\mathbb R^m$. This is what allows distributions in $\mathcal P_n$ to be compared with the true data-generating distribution as $n$ grows: in §3 of the paper a kernel density estimator is shown to lie in $\mathcal P_n$ for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.

Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.

Difficulty

The inequality $\ge$ from the left side is the easy half: point masses $\sum_ic_i\delta_{x_i}$ with $x_i\in\mathcal Z_i$ belong to $\mathcal P_n$. The substance is the reverse bound, that no $\mu\in\mathcal P_n$ can do better than $\sum_ic_if_i$. For disjoint sets this is immediate, since $\mu(\mathcal Z_i)=c_i$. For overlapping sets a measure may place mass in intersections, and a single point of $\mathcal Z_i\cap\mathcal Z_j$ can serve several indices at once; the constraint family over all $2^n$ subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded $\mathcal Z_i$, infinite integrals, infima equal to $-\infty$) must also be handled rather than assumed away.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ with its Borel $\sigma$-algebra; no norm is used. Indices $1,\dots,n$ are Fin n, subsets are Finset (Fin n), and $\{1,\dots,i\}$ is Finset.Iic i.
• $\mathcal P_n$ is a Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, $\emptyset$ and $[1:n]$ included.
• $\int f\,d\mu$ is expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, $\int f^+-\int f^-$. The Bochner integral is not used, because its value $0$ on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set $\mathcal Z_i$.
• Readings of the printed statements. (i) The paper allows $f$ to take the value $-\infty$; here $f$ is real-valued. The excluded case is the one the proof disposes of in its first sentence, where both sides are $-\infty$. (ii) No boundedness hypothesis is added: when some $\inf_{\mathcal Z_i}f=-\infty$ both sides are $-\infty$, and otherwise every $\mu\in\mathcal P_n$ has a finite negative part. (iii) Corollary 2.1 prints "$f:\mathbb R\cup\{-\infty\}$" without a domain; it is read as $f:\mathbb R^m\to\mathbb R$. (iv) Corollary 5.2 is corrected: the paper prints the coefficient $(p_n-p_{n-1})$, while its proof sets $c_i=p_i-p_{i-1}$; the printed version is false (for $\mathcal Z_1=\{a\}\subseteq\mathcal Z_2=\{a,b\}$, $f(a)=1$, $f(b)=0$, $p_1=1/4$, the left side is $1/4$ and the printed right side $3/4$). The mission states $(p_i-p_{i-1})$. (v) The standing hypotheses of Theorem 2.1 ($f$ measurable, $\mathcal Z_i$ nonempty Borel) are made explicit in Corollary 5.2.
• The ordering $f_1\ge\dots\ge f_n$ is a hypothesis of the nested-dual milestone only, as the proof's "without loss of generality"; the goal does not assume it. Milestones 2 and 3 assume $f$ bounded below on each $\mathcal Z_i$ (the proof's first reduction), so that $f_i$ is a real number.
• Ruled out. A Bochner-integral formulation, a restriction to disjoint sets, a distribution set containing non-probability measures, or a set $\mathcal P_n$ defined by the singleton constraints $\mu(\mathcal Z_i)\ge c_i$ alone would each change or trivialise the theorem; none is used.
• Definitions (file Model): the set $\mathcal P_n$, the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$, where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$. The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$. This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$, its Borel $\sigma$-algebra and Lebesgue measure $dx$. The data are:

• a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$;
• a utility $f:V\times\mathbb R^m\to\mathbb R$, Borel measurable in $x$ for each $v$;
• a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$;
• radii $\epsilon(n)>0$.

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$, and the box-robust sample objective is

$$J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').$$

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$. The equicontinuity modulus of $f$ is

$$d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.$$

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$, and with the uniform box kernel density estimator

$$h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.$$

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$; $d(\epsilon)\to0$ as $\epsilon\downarrow0$; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$. Then for every choice of maximisers $v(n)$, with probability one,

$$\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .$$

Milestones (proof of Theorem 3.1, p. 99)

1. $h_n$ is the density of a probability measure in $\mathcal P_n$.
2. $J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$.
3. Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$.
4. Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$, for every $v$,

$$J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).$$

5. Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$, then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$, uniformly in $v$, and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$, the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$, and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$, with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$, and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
• The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$-th problem uses the first $n$. "With probability one" is ∀ᵐ ω ∂P.
• The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
• Readings and corrections of the printed text:
  • the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$, as the proof on p. 99 writes it;
  • "$\max_{v,x}|f(v,x)|\le C$" is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
  • "$d(\epsilon)\downarrow0$" is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$;
  • implicit hypotheses made explicit: $\mathcal F\ne\emptyset$, $\epsilon(n)>0$, measurability of $f(v,\cdot)$, $h^*$ a Lebesgue density;
  • the monotonicity in "$\epsilon(n)\downarrow0$, $n\epsilon(n)^m\uparrow\infty$" is kept in the goal; milestone 5 uses the limits only, as the paper states it;
  • the paper's $M_n$ ("there exists $\{M_n\}\to0$") is made explicit as $M_n=C\int|h_n-h^*|$, so Eq. (7) is stated for every sample.
• Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
• Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
• The definitions (boxes, $\mathcal P_n$, the kernel, the estimator, $J_n$, $d$) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$, the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
• Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
• L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
• A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).

Motivation

Internet routers, wireless base stations, and data-switch fabrics all face the same recurring decision: in each discrete time slot, which of many possible transfer operations should be executed, given the packets currently queued and the physical constraints (link capacities, interference between simultaneous transmissions) on what can be done at once? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 12 to exactly this question, under the name packet networks. Unlike every prior chapter of the book, which works in continuous time with Poisson-driven Markov chains, this chapter builds its stability theory from scratch for a discrete-time, slotted model — the natural setting for a system that makes one scheduling decision per clock tick. This mission formalizes the chapter's foundational layer: the model itself, its notion of a feasible schedule and control policy, subcriticality, and the discrete-time fluid-limit machinery that Chapters 13 and 14 (back-pressure control and random proportional scheduling, respectively) build their own stability proofs on top of.

Setting

A packet network (Section 12.1) has I packet classes and J activities (service types); activity $j$ transfers a packet from its input class $u(j)$ to its output class $d(j)$ (or removes it from the network if $d(j)=0$), giving an $I\times J$ input-output matrix $R$. A processing plan for class $i$ (Definition 12.2) is a chain of activities from $i$ to exit; Assumption 12.1 requires every class to have one and forbids cycles. In each timeslot the system manager chooses a schedule $s\in\mathbb Z^J_+$ from a feasible set $S$ satisfying the packet-availability constraint $Bs\le z$ (the current buffer contents); $S$ is typically built (Section 12.2) from a link usage matrix $A$ and a set $C$ of feasible link configurations via $S_c := \{s : As\le c\}$, $S := \bigcup_{c\in C} S_c$. A Markovian control policy (Definition 12.3, Eq. 12.8) chooses $s(\tau) = f(Z(\tau-1), U(\tau))$ from the current buffer contents and an independent randomization variable; it is admissible if it never overdraws a buffer, and stable if the resulting discrete-time Markov chain $Z$ is irreducible and positive recurrent.

Formalization targets

Goal: Theorem 12.10 — fluid limit stability implies positive recurrence

If the DTMC $Z$ under a Markovian policy $f$ is irreducible and its fluid limit is stable (Definitions 12.14-12.15), then $Z$ is positive recurrent. This is the chapter's own version of Theorem 6.2 (mission III) — the technical fulcrum that lets a deterministic fluid-model stability argument certify the stability of the original discrete, stochastic system — restated for a genuinely different probabilistic model, since Theorem 6.2 was built under continuous-time, Poisson-arrival hypotheses this chapter does not share.

Supporting milestones

Propositions 12.6-12.7 characterize the convex hulls $\langle S_c\rangle$ and $\langle S\rangle$ as explicit polytopes cut out by the link usage matrix — the combinatorial core that Theorem 12.8 (stability implies subcriticality, this chapter's analog of Theorem 5.2) and Proposition 12.9 (a necessary condition for subcriticality) both build on. Lemma 12.11 records that the schedule-usage counting process is Lipschitz; Lemma 12.12 is the functional strong law of large numbers the external arrival process satisfies; and Theorem 12.13 combines them to establish existence of discrete-time fluid limits satisfying the chapter's own fluid equations (12.31)-(12.36) — the chapter's analog of Theorem 6.5.

Significance

The result itself. Theorem 12.10 is what makes the rest of Chapter 12 (and Chapters 13-14) tractable: rather than analyzing an infinite-state discrete-time Markov chain's positive recurrence directly — a notoriously hard problem in general — it suffices to exhibit a deterministic fluid model and show every solution of that fluid model empties in finite time. This is the same strategy Chapter 6 established for the book's continuous-time model, but Chapter 12 cannot simply invoke that earlier theorem: the packet network model uses discrete time slots rather than a continuous clock, and its probabilistic structure (arbitrary i.i.d. arrival increments rather than Poisson arrivals) is different enough that the fluid-limit compactness argument has to be redone, even though — as the book's own text notes — "the proof mimics that of Theorem 6.2."

Formalizing it. A live prior-art check (GET /theorems?q=packet+network, q=discrete-time+Markov+chain, q=slotted+time) finds no relevant hits. A dedicated further check for MarkovMixing, a different mission's own corpus offering a PositiveRecurrent predicate for Markov chains, found a representationally distinct formalization (a row-function transition kernel rather than this series' own PMF-based jump-chain convention); this mission restates positive recurrence and irreducibility locally instead, consistent with every mission in this series since mission I. Everything else — the packet network model, schedules and configurations, the subcritical region, Markovian policies, and the discrete-time fluid-limit apparatus — is formalized from scratch.

Difficulty

The most consequential decision in this mission is representational, not mathematical: Theorem 12.10's fluid-limit-stability hypothesis quantifies over all fluid limit paths, which are themselves scaling limits of a genuinely stochastic discrete-time process — reconstructing that process from Chapter 2/4's own primitive stochastic elements (arrival processes, phase-type service mechanics) would require rebuilding infrastructure this chapter's own numbered results do not supply. Following mission III's own precedent for its structurally identical Theorem 6.5, this mission instead takes the raw, per-initial-state schedule-usage and arrival processes as given data satisfying only the recap properties the chapter's own proofs actually cite (Eq. 12.9-12.10's system equation, monotonicity), and fixes a single sample point together with an explicit SLLN hypothesis rather than a bare "for almost all $\omega$" quantifier — matching the book's own statement of Theorem 12.13, which itself begins "Fix an $\omega\in\Omega_1$" rather than quantifying almost everywhere within the theorem itself. A second difficulty is genuinely combinatorial: Proposition 12.6's proof constructs an explicit product-form probability distribution over schedules (one independent randomization per link) whose mean recovers an arbitrary point of the polytope $\{Ax\le c\}$ — a real combinatorial argument, not a formal consequence of the convex-hull operator's definition.

Formalization scope

Classes, activities, links, schedules and configurations are represented via Fin-indexed types throughout; S and C are taken as Finsets (every worked example in the book has finitely many configurations, and the link usage matrix's single-1-per-column structure bounds each schedule component, so this is a genuine, if implicit, standing feature of the model rather than an added restriction). IsScheduleSetAt/IsScheduleSet characterize $S_c$/$S$ via an ↔ against the underlying capacity constraint, rather than constructing them, matching how set-valued model data is handled elsewhere in this series. The formalization does not admit a trivializing reading: the ambient chain's positive recurrence (PositiveRecurrent) is the same non-vacuous renewal-theoretic notion used throughout this series, PacketFluidLimitStable quantifies over every genuine fluid limit path (not a hand-picked one), and subcriticalRegion is stated with a strict inequality ($A\hat s < \hat c$) exactly as Eq. 12.24 requires, not weakened to $\le$. Contributions completing the eight by sorry proofs are welcome, particularly Proposition 12.6's explicit randomized- schedule construction and Theorem 12.13's compactness argument (mirroring mission III's own Theorem 6.5 proof, adapted to discrete time).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

Why shrink an uncertainty set

Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision $v$ and a parameter $x \in \mathbb{R}^m$ with objective $f(v, x)$ to be maximized, the robust problem around a nominal parameter $x_0$ with a deviation set $\Delta$ is

$$\max_{v} \min_{x_\delta \in \Delta} f(v, x_0 + x_\delta).$$

When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix $\alpha \in (0,1)$ and solve the same problem over the shrunken set $\alpha\Delta = \{\alpha x : x \in \Delta\}$. The heuristic is easy to implement, but the meaning of the set $\alpha\Delta$ is unclear, and it has lacked a justification.

Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.

Setting

Let $\mathbb{R}^m$ carry the Euclidean norm $\|\cdot\|_2$ and its Borel $\sigma$-algebra, and let $\mathcal P$ be the set of Borel probability measures on $\mathbb{R}^m$. Let $V$ be any set of decisions and $f : V \times \mathbb{R}^m \to \mathbb{R}$. Fix $x_0 \in \mathbb{R}^m$, a deviation set $\Delta \subseteq \mathbb{R}^m$, and $\alpha \in (0,1)$. Write $x_0 + \Delta = \{x_0 + x : x \in \Delta\}$.

The two-scenario set is

$$\hat{\mathcal P}' = \{\mu \in \mathcal P \mid \mu(\{x_0\}) \ge 1-\alpha,\ \mu(x_0 + \Delta) = 1\}.$$

A distribution in $\hat{\mathcal P}'$ describes a system that is, with probability at least $1-\alpha$, in a normal state where the parameter equals $x_0$, and otherwise in an abnormal state where the parameter deviates by an element of $\Delta$. The DRSP value of a decision $v$ is $\inf_{\mu \in \hat{\mathcal P}'} \int f(v, x)\, d\mu(x)$.

Two further quantities enter. The radius of the deviation set is $D = \max_{x \in \Delta} \|x\|_2$. The curvature bound is a constant $h \ge 0$ with

$$-hI \preceq H_v(x) \preceq hI \quad \text{for all } v, x,$$

where $H_v(x)$ is the Hessian of $f(v, \cdot)$ at $x$ and $\preceq$ is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.

Formalization targets

Goal: Theorem 4.1 (p. 104)

If $f(v,\cdot)$ is twice differentiable with $-hI \preceq H_v(x) \preceq hI$ for all $v, x$, then for all $v$

$$\inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) - \alpha D^2 h \;\le\; \min_{x_\delta \in \alpha\Delta} f(v, x_0 + x_\delta) \;\le\; \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) + \alpha D^2 h.$$

Milestones (the displays of the proof on p. 105)

1. The mean-value step $f(v, x_0 + x_1) = f(v, x_0) + g_v(x_0 + \beta x_1)x_1$ for some $\beta \in [0,1]$, where $g_v$ is the gradient of $f(v,\cdot)$.
2. The gradient bound $\|g_v(x_0 + \beta x_1) - g_v(x_0 + \alpha\beta' x_1)\| \le h\|\beta x_1 - \alpha\beta' x_1\| \le h\|x_1\| \le hD$, stated together with the general fact that the Hessian bound makes $g_v$ $h$-Lipschitz.
3. The pointwise sandwich: for $x_1 \in \Delta$, $f(v, x_0 + \alpha x_1)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha f(v, x_0 + x_1)$.
4. The min sandwich: $\min_{\alpha\Delta} f(v, x_0 + \cdot)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha \min_{\Delta} f(v, x_0 + \cdot)$.
5. The two-scenario value: $(1-\alpha) f(v, x_0) + \alpha \min_{x_\delta\in\Delta} f(v, x_0 + x_\delta) = \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x)$, which the paper derives from its Corollary 5.2 (p. 107).

Further results

Corollary 4.2 (p. 104): if every $f(v,\cdot)$ is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if $\Delta$ is star shaped, every $f(v,\cdot)$ is convex with $f(v, x_0) - \min_{\Delta} f(v, x_0 + \cdot) \ge 1$ and has Hessian bounded by $h$, then the shrunken value lies between the DRSP values over $\hat{\mathcal P}''$ and $\hat{\mathcal P}'$, where $\hat{\mathcal P}''$ requires only $\mu(\{x_0\}) \ge \max(0, 1-\alpha-\alpha D^2 h)$.

Significance

The result gives a physical meaning to the parameter $\alpha$ of the shrinkage heuristic: $1-\alpha$ is a lower bound on the probability that the system is in its nominal state. The error $\alpha D^2 h$ vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.

Difficulty

Two points need care. First, the step from the Hessian bound $-hI \preceq H_v \preceq hI$, a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of $x_0 + \Delta$.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m) with its Borel $\sigma$-algebra. Measures are Measures, and membership in $\hat{\mathcal P}'$ includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.

The formalization makes the following readings explicit:

1. $\Delta$ is compact. The page writes min over $\alpha\Delta$ and max over $\Delta$, which presuppose attainment. Compactness together with continuity of $f(v,\cdot)$ gives attainment, a finite $D$, finite integrals and measurability of $x_0 + \Delta$. The goal additionally states that the minimum over $\alpha\Delta$ is attained.
2. $0 \in \Delta$. Without it $\hat{\mathcal P}'$ is empty, since $\mu(\{x_0\}) \ge 1-\alpha > 0$ and $\mu(x_0+\Delta)=1$ force $x_0 \in x_0 + \Delta$. The page's two-scenario reading presupposes it. In Corollary 4.3 it follows from star-shapedness once $\Delta$ is nonempty, and nonemptiness is added there.
3. Twice differentiable with bounded Hessian means that $f(v,\cdot)$ and its derivative are differentiable everywhere and $|D^2 f(v,\cdot)(x)[y,y]| \le h\|y\|_2^2$ for all $x, y$. The constant $h$ is one constant for all $v$.
4. The minima over $\Delta$ and $\alpha\Delta$ are written as infima, which equal the minima under the hypotheses above.

The Lean functions drspValue and devRadius return $0$ on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped $0 \in \Delta$ would make the inequalities hold or fail for the wrong reason and is ruled out.

Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, S. Mannor, Percentile Optimization for Markov Decision Processes with Parameter Uncertainty, Operations Research 58(1):203–213, 2010. https://doi.org/10.1287/opre.1080.0685
• E. Delage, Y. Ye, Distributionally Robust Optimization under Moment Uncertainty with Applications to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• D. Bertsimas, D. B. Brown, C. Caramanis, Theory and Applications of Robust Optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510