Probability

Motivation

A call center has to decide how many agents to staff. In practice the decision is often posed as a service-level constraint rather than a cost trade-off: use the fewest agents for which the expected waiting cost, or the fraction of customers who wait, stays below a target. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; journal version in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) treat this constraint problem in Section 8 of their paper, alongside the cost-minimization problem of Sections 5–7, and show that a simple square-root staffing rule solves it asymptotically as the arrival rate grows.

The rule matters because it is what practitioners use. Under the classical Erlang-C model, the exact optimum requires evaluating the Erlang-C formula over many staffing levels. The asymptotic rule replaces this with a single equation in the Halfin–Whitt function $P$: when the target is a delay probability $\varepsilon$ (Example 8.5 of the paper), it reduces to staffing $\lambda/\mu + P^{-1}(\varepsilon)\sqrt{\lambda/\mu}$ servers.

Timeline. Erlang's formula for the M/M/N delay probability dates from 1917. Halfin and Whitt (Operations Research 29, 1981) identified the limit $P(x)$ of the delay probability under square-root staffing $N = \lambda/\mu + x\sqrt{\lambda/\mu}$ with integer $N$. Jagers and Van Doorn (Operations Research Letters 5, 1986; SIAM Review 33, 1991) studied the continued Erlang loss and delay functions at non-integer numbers of servers, including their convexity, which is what lets the staffing problem be relaxed to a continuous one. Borst, Mandelbaum and Reiman (2000/2004) used these to prove asymptotic optimality of square-root rules for both the cost and the constraint formulations.

Setting

Customers arrive at rate $\lambda$ to $N$ identical servers, each with service rate $\mu > 0$; $\mu$ is fixed while $\lambda \to \infty$. Stability requires $N > \lambda/\mu$. A customer who waits $t$ time units costs $D_\lambda(t)$, where $D_\lambda(0) = 0$, $D_\lambda$ is strictly increasing on $[0,\infty)$ and $\int_0^\infty D_\lambda(t)e^{-\theta t}\,dt < \infty$ for all $\theta > 0$.

The Erlang-C probability of waiting is

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Big\}^{-1},$$

and the conditional waiting cost is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$. The waiting cost per unit time with $N$ servers is

$$K(N,\lambda) = \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda).$$

Given a target $M_\lambda > 0$, the optimal staffing level is the least integer $N > \lambda/\mu$ with $K(N,\lambda) \le M_\lambda$; call it $N^*_\lambda$.

In the continuous parametrization $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, define $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, the continuous Erlang-C function $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$, and $K_\lambda(x) = \pi_\lambda(x)G_\lambda(x)$. The Halfin–Whitt function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. A staffing function $x_\lambda > 0$ is judged by the rounding gap

$$T_\lambda(x) = \min\big\{|K(\lfloor N_\lambda(x)\rfloor,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - M_\lambda|,\ |K(\lceil N_\lambda(x)\rceil,\lambda) - K(N^*_\lambda,\lambda)|\big\}.$$

It is asymptotically optimal when $T_\lambda(x_\lambda)/M_\lambda \to 0$ as $\lambda\to\infty$.

Formalization targets

Goal: Theorem 8.2 (rationalized regime)

Suppose that for some $\kappa > 0$ and $\gamma \in (0,\infty)$, $G_\lambda(\kappa)/M_\lambda \to \gamma$, i.e. the waiting cost is comparable to the target. Let $y^*_\lambda > 0$ solve $P(y)G_\lambda(y) = M_\lambda$. Then

$$\lim_{\lambda\to\infty}\frac{T_\lambda(y^*_\lambda)}{M_\lambda} = 0.$$

Supporting milestones

• Lemma C.1: $G_\lambda$ is strictly convex and decreasing on $(0,\infty)$.
• Section 3: $\pi_\lambda(x) = \pi(N_\lambda(x),\lambda/\mu)$ when $N_\lambda(x)$ is an integer.
• Lemma 8.1: if $z^*_\lambda > 0$ solves $\hat\pi_\lambda(z)\hat G_\lambda(z) = M_\lambda$ and $K_\lambda(z^*_\lambda)/(\hat\pi_\lambda\hat G_\lambda)(z^*_\lambda) \to 1$, then $T_\lambda(z^*_\lambda)/M_\lambda \to 0$.
• Lemma B.1: $P$ is strictly convex and decreasing on $(0,\infty)$.
• Eq. (17): $\limsup a_\lambda/b = \infty$ implies $\liminf P(a_\lambda)/P(b) = 0$ and $\liminf \pi_\lambda(a_\lambda)/\pi_\lambda(b) = 0$.
• Lemma 4.1 (Halfin–Whitt): for bounded $x_\lambda > 0$, $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$; with $x_\lambda \to x$, $\pi_\lambda(x_\lambda)/P(x)\to 1$.

Further target: Theorem 8.6 (efficiency-driven regime)

If $G_\lambda(\kappa)/M_\lambda \to 0$ for every $\kappa > 0$ and $y^*_\lambda > 0$ solves $G_\lambda(y) = M_\lambda$, then $T_\lambda(y^*_\lambda)/M_\lambda \to 0$.

Significance

The theorem certifies the staffing rule used in workforce-management practice: the excess staffing is determined by one scalar equation involving the Gaussian function $P$ and the scaled waiting cost, and rounding the resulting staffing level misses the constraint by a vanishing fraction of the target. Lemma 8.1 is a reusable framework: any approximation $\hat\pi_\lambda\hat G_\lambda$ that is asymptotically exact at the proposed staffing level yields an asymptotically optimal rule, and the paper instantiates it in three regimes (Theorems 8.2, 8.6, 8.9).

The results are proved on paper. To the best of current knowledge none of them, nor the Halfin–Whitt limit for the continuous Erlang-C extension, has a machine-checked proof. A formalization would produce the first verified heavy-traffic limit of the Erlang-C delay probability, a verified continuous Erlang-C extension with its integer identity, and the convexity facts about $P$ and $G_\lambda$ that many staffing papers cite without proof.

Difficulty

The obvious argument is to quote Halfin and Whitt: the delay probability converges to $P(x)$ under square-root staffing, so $P$ can replace the Erlang-C formula. That limit, as published in 1981, is about integer server counts along sequences with a convergent excess-staffing parameter. The paper needs it for the continuous function $H$ at non-integer server counts and for staffing functions that are merely bounded, and it also needs the identity $H(N,\nu) = \pi(N,\nu)$ at integers and the monotonicity of $\pi_\lambda$ in $x$, both cited from Jagers and Van Doorn rather than proved. None of these is in Mathlib. A second obstacle is that the staffing function $y^*_\lambda$ is defined only implicitly by an equation involving $G_\lambda$, which depends on the arbitrary cost functions $D_\lambda$; nothing a priori prevents it from escaping to infinity, outside the range where the Halfin–Whitt approximation applies. Finally, $T_\lambda$ compares integer-level costs given by the Erlang-C formula with a continuous approximation, so both representations of the delay probability are in play at once.

Formalization scope

The queue itself is not formalized: there is no Markov chain and no waiting-time distribution. Every statement is about the closed-form waiting cost $K(N,\lambda)$ with $\pi$ given by the Erlang-C formula, exactly as the paper's analysis is. Conventions, all in the namespace DimCallCenters.Constraint:

• lam : ℝ is the arrival rate (λ is a Lean keyword); limits are Filter.atTop in lam, with μ fixed. Objects indexed by λ ($M_\lambda$, $N^*_\lambda$, $y^*_\lambda$) are functions of lam constrained only for lam > 0.
• WaitModel packages μ > 0 and $D_\lambda$ with $D_\lambda(0) = 0$, strict monotonicity on $[0,\infty)$, and integrability of $D_\lambda(t)e^{-\theta t}$ on $(0,\infty)$ for θ > 0 (the paper's finiteness of $G$; integrability is required because Lean's integral of a non-integrable function is 0).
• $N^*_\lambda$ is a function Nstar : ℝ → ℕ given with its two defining properties (feasible; below every feasible integer level above λ/μ). $y^*_\lambda$ and $z^*_\lambda$ are any positive solutions of their equations; existence and uniqueness are not hypotheses.
• In $T_\lambda$ the round-down term is dropped when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ (an unstable level where $K$ is undefined). This can only enlarge $T_\lambda$.
• Asymptotic relations are limits of ratios. $\limsup = \infty$ and $\liminf = 0$ are stated with ∃ᶠ ("frequently"), $\limsup < \infty$ as eventual boundedness.
• $P$ is defined through explicit $\phi$, $\Phi$, $h$; the formula also gives $P(0) = 1$, used in Lemma 4.1(2) at $x = 0$.
• No hypothesis $\lim_{N\downarrow\lambda/\mu}G(N,\lambda) = \infty$ is added: it is not needed for the statements here.

A trivializing formalization is ruled out: $T_\lambda$ keeps all of the paper's terms and is never replaced by a smaller quantity, and the hypotheses are jointly satisfiable — $D_\lambda(t) = a\sqrt{\lambda/\mu}\,t$ with $M_\lambda = M\lambda$ satisfies (33) for every $\kappa$ with $\gamma = a/(\mu\kappa M)$.

Infrastructure needed: the continuous Erlang-C function and its integer identity; the Halfin–Whitt limit (a Gaussian approximation of Poisson/gamma tails); calculus facts about the normal hazard rate. These are reusable beyond this mission, notably by the sibling missions on the cost-minimization problem. Example 8.5 (delay-probability target with $D_\lambda = 1_{t>0}$) motivates the rule but violates the strict monotonicity of $D_\lambda$, so it is not an instance of the theorem as stated. Contributions on any milestone, and on Theorem 8.9 (quality-driven regime, which needs Lemma 4.2), are welcome.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• A. A. Jagers, E. A. Van Doorn, On the Continued Erlang Loss Function, Operations Research Letters 5:43–46, 1986.
• A. A. Jagers, E. A. Van Doorn, Convexity of Functions which are Generalizations of the Erlang Loss Function and the Erlang Delay Function, SIAM Review 33:281–282, 1991.

Motivation

A classifier built from a neural network produces a real score and predicts a binary label from its sign. A network can have many hidden units, so a guarantee based only on the number of parameters can be uninformative even when its output weights are small. Bartlett's 1998 paper asks whether a classifier's margin on training examples and the total magnitude of its weights can control its probability of error without fixing the number of units. Its Theorem 28 gives such a statement for two-layer networks whose activation is bounded and nondecreasing. The paper also discusses why this parameter-magnitude view supports weight decay and early stopping as learning heuristics, while leaving their algorithmic behavior outside the theorem's scope (Bartlett 1998, pp. 526, 534–535).

The theorem combines two results in the same paper. Theorem 2 turns the fat-shattering dimension of a real-valued function class into a margin generalization bound. Corollary 24 controls that dimension for finite combinations of affine-input units when the sum of the absolute combination weights is bounded. Lemmas 19, 22, and 23 supply covering estimates along that path. These are the milestones of this mission, with the source statements preserved in the milestone record (Bartlett 1998, pp. 527, 532–534).

Setting

An input is a vector $x\in\mathbb R^n$, represented in Lean as Fin n → ℝ. A label is $y\in\{-1,+1\}$; Lean's Bool is converted by pm, where true means $+1$. A probability distribution $P$ lives on labeled inputs. From an independent sample $z=((x_i,y_i))_{i=1}^m$, the empirical margin error at scale $\gamma>0$ is the fraction of indices with $y_i h(x_i)<\gamma$. The population error is the probability that $\operatorname{sgn}(h(x))\ne y$, where $\operatorname{sgn}(0)=+1$. The inequality in the empirical error is strict, as in the paper's definition (Bartlett 1998, p. 526).

Fix a bounded nondecreasing activation $\sigma:\mathbb R\to[-1,1]$. The first-layer class $F$ contains every $x\mapsto\sigma(w\cdot x+w_0)$, with an arbitrary weight vector and bias. The network class $H$ contains all finite sums $\sum_{i=1}^N\alpha_i f_i$ with $f_i\in F$ and $\sum_i|\alpha_i|\le A$. Thus $A$ bounds the output layer's total weight magnitude, while $N$ can vary without an imposed width limit. The bias $w_0$ is part of every unit. For a class $G$, $\operatorname{fat}_G(\eta)$ records the largest length of an input sequence whose every sign pattern can be realized with separation at least $\eta$ around one vector of thresholds (Bartlett 1998, pp. 526, 533–534).

Formalization targets

Two-layer generalization

For $0<\gamma\le1$, $0<\delta<1/2$, $A\ge1$, and an independent sample of length $m\ge1$, the goal is one universal $c>0$ such that, with probability at least $1-\delta$, every $h\in H$ satisfies

$$\operatorname{er}_P(h)<\widehat{\operatorname{er}}_z^\gamma(h)+ \sqrt{\frac{c}{m}\left( \frac{A^2n}{\gamma^2}\log\!\left(\frac{32A}{\gamma}\right)(\log m)^2+ \log\!\left(\frac1\delta\right)\right)}.$$

The paper prints $\log(A/\gamma)$ in this display. That term vanishes at $A=\gamma=1$, although the class can then contain halfspace classifiers with nonzero sample complexity. The proof obtains a positive factor at that corner through Corollary 24 at scale $\gamma/16$, giving $\log(32A/\gamma)$. The goal states this correction and records the printed statement separately in the moderation notes. The constant precedes all network, distribution, margin, confidence, and sample parameters in Lean; it cannot be selected after observing the instance (Bartlett 1998, pp. 533–534).

Capacity and margin milestones

Corollary 24 bounds $\operatorname{fat}_H(\eta)$ by a constant multiple of $M^2A^2n\eta^{-2}\log(MA/\eta)$ when the activation has range $[-M/2,M/2]$. Theorem 2 then converts a finite fat dimension at scale $\gamma/16$ into a simultaneous bound on population error for all members of $H$. The three covering lemmas track how shattering, pseudodimension, and an $\ell_1$ weight budget affect covers in sample $\ell_1$, $\ell_\infty$, and $\ell_2$ distances. Each bound retains the scale and explicit constants printed by the paper, subject to the stated corrections to undefined or false boundary cases (Bartlett 1998, pp. 527, 532–533).

Significance

The goal gives a width-independent generalization guarantee for a chosen network when its empirical margin error and total output weight are small. It applies to the entire class $H$ at once, so choosing a network after inspecting the sample does not turn the bound into a claim about only one fixed predictor. It does not assert that a learning algorithm finds such a network or that the displayed constants are optimal. Bartlett notes that later work had improved a logarithmic factor, and that empirical agreement with neural-network performance remained an open experimental question at the time (Bartlett 1998, pp. 534–535).

The paper proves the mathematical result. This mission asks for a machine-checked proof of its corrected formal statement and the stated supporting results; the draft theorem files currently contain proof obligations. A completed development would also make the fat dimension and strict external sample-cover definitions available for other margin analyses. Those objects differ from the platform's fixed-architecture neural networks and closed-ball covering numbers, so they are defined here with the conventions of this paper.

Difficulty

Counting hidden units gives no finite width-independent capacity bound, because $H$ permits arbitrarily many terms. Bounding each unit separately also does not control the full combination class: different small contributions can produce distinct values on a sample. The challenging step is relating covers of the base class to covers of all finite combinations under the total absolute-weight constraint, and then relating those covers back to fat-shattering. Even once a finite capacity estimate is available, the probability statement must hold simultaneously for every $h\in H$, including a network selected after sampling (Bartlett 1998, pp. 532–534).

Formalization scope

Lean uses $\mathbb N\cup\{\infty\}$ for fat dimensions and covering numbers, so an unbounded class cannot acquire a spurious dimension zero. Covers are external finite sets of real functions and use the strict distance $<\varepsilon$ of Definition 3. Sample $\ell_1$ and $\ell_2$ distances are normalized by $m$. Pseudodimension is the supremum of positive-scale fat dimensions, matching the paper's right limit. Theorems assume $m\ge1$, and sample indices are zero-based. The network class is generated from its weights rather than supplied as an arbitrary set satisfying the desired bound.

The paper says it ignores measurability issues and assumes all sets considered are measurable (Bartlett 1998, p. 526). The goal makes the event of a violating network measurable. Its individual network functions are measurable from monotonicity of $\sigma$ and finite sums; the restated Theorem 2 has explicit hypotheses for measurable class members, the violating event, and the double-sample event in its proof. Theorem 2 additionally restricts $d=\operatorname{fat}_H(\gamma/16)$ to $d\le34m$, where its printed logarithmic bound remains valid. Corollary 24 uses $n\ge1$ because a zero-dimensional input still permits a biased constant unit. Lemma 23 uses $d\ge1$ and $0<\gamma<emM/d$ in place of the printed $\gamma\ge0$: at $\gamma=0$ or $d=0$, or for $\gamma\ge emM/d$, the printed strict inequality fails, while on the rest of the printed range it is kept. These are recorded as corrections rather than attributed to the printed wording.

The deeper-network part of Theorem 28 is outside this proposal. Its printed chain through Corollary 27 has an unresolved range issue when the input box bound $B$ is smaller than the activation range, and the displayed $\log n$ factor also vanishes at $n=1$. This mission's goal is Part 1 and uses none of those claims. Contributions that establish the corrected covering lemmas, the capacity corollary, or the simultaneous margin bound fit the present proof frontier (Bartlett 1998, pp. 533–534).

Selected references

• P. L. Bartlett, The Sample Complexity of Pattern Classification with Neural Networks: The Size of the Weights is More Important than the Size of the Network, IEEE Transactions on Information Theory 44(2), 525–536, 1998. DOI.

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979) 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

Every step of the dynamic programming algorithm on a general state space does three things: it takes a conditional expectation of the cost-to-go under a transition kernel, it minimizes the resulting function of state and control over the control, and, if a policy is to be produced, it picks a control for each state that attains or nearly attains that minimum. On a finite or countable state space all three are harmless. On an uncountable state space each can destroy the measurability needed to take the next expectation: the infimum over an uncountable family of measurable functions need not be measurable, and a minimizer chosen state by state need not be a measurable function of the state, so it does not define a policy at all.

Section 7.5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), settles the three operations for semicontinuous costs and continuous kernels. The results are the topological half of the book's measurability theory; the descriptive set theory half (lower semianalytic functions and analytically measurable selectors, §7.6–7.7) is a separate mission in this series. The semicontinuous results are what Propositions 8.6–8.7 and Corollaries 9.17.2–9.17.3 of the book use to obtain Borel-measurable optimal policies for finite-horizon and infinite-horizon models with lower semicontinuous costs and compact control sets.

Timeline. The exact selection theorem for lower semicontinuous functions (Proposition 7.33 below) is credited by the book's notes to Dubins and Savage, How to Gamble If You Must (1965). The Hausdorff metric on closed sets goes back to Hausdorff's Set Theory. Measurable selection in the closed-valued setting was later systematized by Kuratowski and Ryll-Nardzewski (1965), whose theorem gives a different route to results of this kind.

Setting

Throughout, $R^*=[-\infty,+\infty]$ is the extended real line. A function $f:X\to R^*$ on a metrizable space $X$ is lower semicontinuous if every sublevel set $\{x\mid f(x)\le c\}$, $c\in\mathbb R$, is closed, and upper semicontinuous if every superlevel set $\{x\mid f(x)\ge c\}$ is closed (Definition 7.13). $C(X)$ is the space of bounded continuous real-valued functions on $X$.

For a separable metrizable space $Y$, $P(Y)$ is the set of Borel probability measures on $Y$ with the weak topology (convergence of integrals of functions in $C(Y)$). A stochastic kernel $q(dy\mid x)$ on $Y$ given $X$ is a map $x\mapsto q(dy\mid x)$ from $X$ to $P(Y)$, and it is continuous if this map is continuous (Definition 7.12). The integral of a Borel-measurable $f:Y\to R^*$ is $\int f\,dp=\int f^+dp-\int f^-dp$ with the convention $-\infty+\infty=+\infty-\infty=+\infty$ (Eq. (43) of Chapter 7).

For a compact metric space $Y$, $2^Y$ is the collection of closed subsets of $Y$ with the topology of the Hausdorff metric (Appendix C). For $D\subseteq X\times Y$, the section at $x$ is $D_x=\{y\mid (x,y)\in D\}$, the projection is $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and a function $\varphi:\mathrm{proj}_X(D)\to Y$ has its graph in $D$ if $(x,\varphi(x))\in D$ for every $x\in\mathrm{proj}_X(D)$. "Borel-measurable" refers to the Borel σ-algebras of the topologies in question; on $\mathrm{proj}_X(D)$ this is the Borel σ-algebra of the subspace topology.

Formalization targets

Goal: Proposition 7.33

Let $X$ be metrizable, $Y$ compact metrizable, $D\subseteq X\times Y$ closed, and $f:D\to R^*$ lower semicontinuous. Put

$$f^*(x)=\min_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

Then $\mathrm{proj}_X(D)$ is closed, $f^*$ is lower semicontinuous, and there is a Borel-measurable $\varphi:\mathrm{proj}_X(D)\to Y$ with graph in $D$ and

$$f\bigl(x,\varphi(x)\bigr)=f^*(x)\qquad\forall x\in\mathrm{proj}_X(D).$$

Milestones

• Proposition 7.32: for $f^*(x)=\inf_{y\in Y}f(x,y)$, lower semicontinuity of $f$ and compactness of $Y$ give lower semicontinuity of $f^*$ and attainment; upper semicontinuity of $f$ gives upper semicontinuity of $f^*$.
• Lemma 7.18: there is a Borel-measurable $\sigma:2^Y-\{\emptyset\}\to Y$ with $\sigma(A)\in A$.
• Lemma 7.20: for lower semicontinuous $f$ on a nonempty compact $Y$, the argmin map $x\mapsto\{y\mid f(x,y)\le f^*(x)\}$ is Borel-measurable into $2^Y$.
• Lemma 7.14: $f$ is lower semicontinuous and bounded below iff $f_n\uparrow f$ for some $f_n\in C(X)$ (and dually).
• Proposition 7.30: $x\mapsto\int f(x,y)\,q(dy\mid x)$ is continuous for $f\in C(X\times Y)$ and continuous $q$.
• Proposition 7.31: the same map is lower (upper) semicontinuous and bounded below (above) when $f$ is.
• Lemma 7.21: an open $G\subseteq X\times Y$, $Y$ separable, has open projection and a Borel-measurable selector with graph in $G$.
• Proposition 7.34: for open $D$ and upper semicontinuous $f$, $\mathrm{proj}_X(D)$ is open, $f^*=\inf_{D_x}f$ is upper semicontinuous, and for each $\varepsilon>0$ there is a Borel-measurable $\varphi_\varepsilon$ with graph in $D$ and

$$f\bigl(x,\varphi_\varepsilon(x)\bigr)\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

Significance

The results. Propositions 7.31–7.33 are the closure properties that make the dynamic programming recursion stay inside the class of lower semicontinuous functions bounded below: the expectation step preserves the class (7.31), the minimization step preserves it (7.32, 7.33), and the minimization admits a Borel-measurable exact minimizer (7.33). This is why, in semicontinuous models, the optimal cost functions are lower semicontinuous and optimal policies can be taken Borel-measurable and nonrandomized. Proposition 7.34 gives the weaker, $\varepsilon$-optimal counterpart for upper semicontinuous costs, where the infimum need not be attained.

Formalizing them. All of these results are proved in the book; none is open. As far as is known, none has a machine-checked proof: Mathlib has semicontinuity, the Hausdorff extended metric on closed and on nonempty compact sets, and the weak topology on probability measures, but no theorem combining them into a measurable selection result of this kind. A formal development would supply measurable selectors for semicontinuous minimization in Lean and the Borel-measurability of set-valued maps into the hyperspace of closed sets, both reusable well beyond dynamic programming.

Difficulty

The obvious attempt at the goal is to pick, for each $x$, some minimizer $y$ of $f(x,\cdot)$ over the compact section $D_x$. The minimizer exists by compactness and lower semicontinuity, but the choice is made pointwise and gives no control on measurability: a minimizer chosen by the axiom of choice need not be Borel-measurable. The argmin sets $F^*(x)$ vary with $x$ only semicontinuously: they can jump from a single point to a large set, so a continuous selection generally does not exist, and continuity arguments cannot replace measurability. Lemma 7.18 isolates the hardest part: a choice of a point of each nonempty closed set that is measurable as a function of the set itself.

A second difficulty is bookkeeping at infinity. Values $\pm\infty$ are allowed throughout, so sublevel sets, minima, integrals and $\varepsilon$-bounds must all be handled in $R^*$; the integral in Proposition 7.31 uses the convention $\infty-\infty=+\infty$, which is not Mathlib's.

Formalization scope

• Extended reals. Values are in EReal. The only place where values of opposite infinite sign are combined is the integral, which is the published definition DupacovaWets.Consistency.expect (reused, not restated): $\int f^+-\int f^-$ with an explicit case returning $+\infty$ when $\int f^+=\infty$, exactly the book's convention (42). The $\varepsilon$-bound of Proposition 7.34 adds a real $\varepsilon$ to a value different from $-\infty$, which is safe in EReal.
• Semicontinuity is Mathlib's LowerSemicontinuous/UpperSemicontinuous, equivalent to Definition 7.13 for EReal-valued functions. Lemma 7.13 of the book (the sequential characterization) is Mathlib's lowerSemicontinuous_iff_le_liminf together with first countability of metrizable spaces, and is not restated here.
• Functions on $D$. Functions "on $D$" are functions on $X\times Y$ with LowerSemicontinuousOn f D (resp. UpperSemicontinuousOn); values off $D$ play no role. $\mathrm{proj}_X(D)$ is Prod.fst '' D, selectors are functions on that subtype, and its σ-algebra is the Borel σ-algebra of the subspace topology.
• Hyperspace. $2^Y$ is Closeds Y, and $2^Y-\{\emptyset\}$ for compact $Y$ is NonemptyCompacts Y, each with the Hausdorff extended metric and the Borel σ-algebra of its topology. This topology agrees with the book's (the exponential topology of Appendix C, independent of the metric).
• Boundedness. "Bounded below/above" is by a real constant. BddBelow in EReal would be vacuous and is not used.
• Edge cases. Proposition 7.32(a)'s attainment clause is stated for nonempty $Y$, since for $Y=\emptyset$ the infimum is $+\infty$ and nothing attains it.
• Argmin minimum. Lemma 7.20 assumes nonempty $Y$ because its defining formula uses a minimum; for empty $Y$ there is no minimizer.
• Ruling out trivial readings. The graph condition $(x,\varphi(x))\in D$ is part of every selection statement; without it the goal would follow from the unconstrained case. The selector must be Borel-measurable on $\mathrm{proj}_X(D)$ and must attain the minimum exactly, not up to $\varepsilon$.

A complete development needs the Borel structure of the hyperspace (measurability of maps into Closeds Y from upper semicontinuity in the sense of Kuratowski, Proposition C.4 of the book), the construction of a measurable choice function on NonemptyCompacts Y, and approximation of semicontinuous functions by monotone sequences in $C(X)$. Each of these is reusable on its own; proofs of individual milestones by any route are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Section 7.5 and Appendix C. https://web.mit.edu/dimitrib/www/soc.html
• L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965.
• K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors," Bull. Acad. Polon. Sci. 13 (1965), 397–403.
• F. Hausdorff, Set Theory, Chelsea, New York, 1957.

Motivation

Empirical risk minimization (ERM) chooses, from a class $\mathcal F$ of loss functions, the one with the smallest average loss on a sample $X_1,\dots,X_n$. Its standard guarantees bound the excess population risk by a term of order $1/\sqrt n$, whatever the variance of the losses. When good functions in $\mathcal F$ have small variance, a better trade-off is available in principle: minimize the empirical risk plus a standard-deviation penalty $\sqrt{2\rho\,\mathrm{Var}_{\widehat P_n}(f)/n}$. Maurer and Pontil (COLT 2009) showed that this sample variance penalization enjoys faster rates, but the penalized objective is non-convex even for convex losses, so it cannot be minimized efficiently in general.

Duchi and Namkoong (arXiv:1610.02581v3, 2017; NIPS 2017) replace the variance penalty by a distributionally robust objective: the worst-case average loss over all reweightings of the sample within a $\chi^2$-divergence ball of radius $\rho/n$. This objective is convex whenever the loss is convex, and it equals the empirical risk plus the standard-deviation penalty up to an error of order $1/n$. Theorem 3 of the paper turns this into a guarantee for the minimizer of the robust objective, using covering numbers of the class. This mission formalizes Theorem 3 and the lemmas its proof rests on.

Setting

Let $\mathcal X$ be a measurable space, $P$ a probability measure on it, and $X_1,\dots,X_n$ ($n\ge1$) an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $\mathcal F$ be a nonempty class of measurable functions $f:\mathcal X\to[M_0,M_1]$, and set $M = M_1-M_0$. Write $\mathbb E[f]=\int f\,dP$, $\mathrm{Var}(f)$ for the variance of $f(X)$, and

$$\mathbb E_{\widehat P_n}[f] = \frac1n\sum_{i=1}^n f(X_i),\qquad \mathrm{Var}_{\widehat P_n}(f) = \frac1n\sum_{i=1}^n f(X_i)^2 - \big(\mathbb E_{\widehat P_n}[f]\big)^2 .$$

For $\rho\ge0$, the $\chi^2$ ball $\mathcal P_n$ is the set of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_i p_i = 1$ and $\frac12\sum_i (np_i-1)^2\le\rho$: the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$. The robust risk of $f$ is

$$R_n(f) = \sup_{P:\,D_\phi(P\|\widehat P_n)\le \rho/n}\mathbb E_P[f(X)] = \max_{p\in\mathcal P_n}\sum_{i=1}^n p_i f(X_i),$$

and a robust minimizer is any $\widehat f\in\operatorname{argmin}_{f\in\mathcal F} R_n(f)$.

Complexity is measured by empirical $\ell_\infty$ covering numbers. For $V\subset\mathbb R^m$, $N(V,\epsilon,\|\cdot\|_\infty)$ is the least number of points $v_1,\dots,v_N\in V$ such that every $v\in V$ lies within sup-distance $\epsilon$ of some $v_i$. For $x\in\mathcal X^m$ let $\mathcal F(x)=\{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}$, and

$$N_\infty(\mathcal F,\epsilon,m) = \sup_{x\in\mathcal X^m} N\big(\mathcal F(x),\epsilon,\|\cdot\|_\infty\big)\in\mathbb N\cup\{\infty\}.$$

Formalization targets

Goal: the oracle inequality (16)

Let $n\ge 8M^2/t$, $t\ge\log 12$, $\epsilon>0$ and $\rho\ge 9t$. With probability at least $1-2(3N_\infty(\mathcal F,\epsilon,2n)+1)e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f(X)] \le \inf_{f\in\mathcal F}\left\{\mathbb E[f] + 2\sqrt{\frac{2\rho}{n}\mathrm{Var}(f)}\right\} + \frac{19M\rho}{3n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .$$

The certificate (15)

Under the same hypotheses and with the same probability, simultaneously for all $f\in\mathcal F$,

$$\mathbb E[f(X)] \le R_n(f) + \frac{11}{3}\frac{M\rho}{n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .$$

Supporting results (milestones)

1. Theorem 1, inequality (10): for every vector $z\in[M_0,M_1]^n$, the robust mean minus the sample mean lies between $\big(\sqrt{2\rho s_n^2/n}-2M\rho/n\big)_+$ and $\sqrt{2\rho s_n^2/n}$.
2. Lemma C.1: a uniform empirical Bernstein bound over $\mathcal F$ with probability $1-6N_\infty(\mathcal F,\epsilon,2n)e^{-t}$.
3. Lemma A.1, first bound: $\mathbb P(s_n\ge\sqrt{\mathbb E s_n^2}+t)\le\exp(-nt^2/(2M^2))$.
4. Bernstein's inequality for one fixed $f$, as displayed in the proof (p. 38).
5. The certificate (15).

Significance

Inequality (15) says the robust risk is a uniform upper confidence bound on the population risk, with an $O(1/n)$ slack instead of the $O(1/\sqrt n)$ slack of the empirical risk. Inequality (16) says the robust minimizer competes with the best variance-penalized population risk in the class. When some $f\in\mathcal F$ has small risk and small variance, the excess risk of $\widehat f$ is of order $1/n$ up to the covering term, a rate ERM does not achieve in general (§3.3 of the paper gives an example). For a parametric class with $N_\infty(\mathcal F,\epsilon,2n)$ polynomial in $1/\epsilon$, choosing $\epsilon=M/n$ gives Corollaries 3.1 and 3.2 of the paper.

The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission's output is a formal proof of Theorem 3 and its ingredients: a deterministic analysis of the $\chi^2$-constrained linear program (Theorem 1 (10)), a covering-number empirical Bernstein inequality (Lemma C.1, from Maurer and Pontil), concentration of the sample standard deviation (Lemma A.1), and the scalar Bernstein inequality in the form used. Each of these is reusable outside distributionally robust optimization.

Difficulty

The deterministic part, (10), is a short analysis of a quadratically constrained linear program. The main obstacle is Lemma C.1. A union bound over a cover of $\mathcal F$ fails directly: the cover depends on the sample, and a population-level cover of $\mathcal F$ need not be finite. The standard route goes through a ghost sample of size $n$ (hence covering at $2n$ points), a symmetrization that must preserve the sample variance rather than only the mean, and a concentration bound for the sample variance itself. Lemma A.1 needs concentration of $s_n$, a non-linear and non-smooth function of the sample, at the sub-Gaussian rate $M/\sqrt n$. Finally, the oracle inequality (16) holds for an infimum over the whole class, while the concentration step for the comparison function is only proved for one fixed $f$ at a time.

Formalization scope

The sample is the coordinate process of the product measure $P^{\otimes n}$ on $\mathcal X^n$ (Measure.pi). Each probability statement bounds the probability of the bad event, the set of samples where the inequality fails for some $f$ (or some minimizer). This set need not be measurable, and its measure is then the outer measure, as is standard in empirical-process theory. Probability bounds are computed in $[0,\infty]$, and the covering number is valued in $\mathbb N\cup\{\infty\}$, so an infinite covering number makes the bound trivial rather than collapsing to zero. Covering numbers are internal (centres in $\mathcal F(x)$) and use closed sup-norm balls, as on p. 9; this is Mathlib's Metric.coveringNumber. The empirical variance is normalized by $1/n$. The $\chi^2$ ball is encoded as weight vectors on the sample points; with tied sample values this gives the same supremum as the paper's distributions on the sample. Statement (16) is formalized for every minimizer of the robust risk, and the event is empty if no minimizer exists. The infimum ranges over the nonempty class $\mathcal F$, on which every term is at least $M_0$. Population moments are those of bounded measurable functions, hence finite.

Deviations from the printed text:

• Lemma A.1 is stated only for its first (upper-tail) bound. The paper derives the second bound from Lemma A.4, which is false as printed; the second bound is not stated. $M>0$ is assumed because $M^2$ is a denominator.
• Lemma C.1 is the paper's restatement of Maurer and Pontil's Theorem 6, with a general radius $\epsilon$. It is formalized as printed, with the implicit assumption $\epsilon>0$ made explicit.
• $n\ge1$ is assumed throughout. The hypothesis $n\ge 8M^2/t$ is kept as printed.

A trivializing formalization is ruled out: the bound is not taken over all functions, a probability bound is not formed from the real part of an infinite covering number, and the minimizer is not a hypothesis that can fail to exist for the given sample.

Needed infrastructure: product-measure concentration (Bernstein, and a bounded-difference or convex-Lipschitz inequality for $s_n$), symmetrization with a ghost sample, and finite union bounds over a cover. Contributions are welcome on any milestone, in particular a general covering-number empirical Bernstein inequality, which is reusable on its own.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017 (NIPS 2017; JMLR 20, 2019). https://arxiv.org/abs/1610.02581
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2

Motivation

Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.

Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).

Timeline:

• 1980–1988: Coffman and Mitrani, then Federgruen and Groenevelt — the achievable performance vectors of a single-station multiclass queue form a polytope described by conservation laws.
• Early 1990s: Kumar (reference [Kuma] of the paper), using a potential-function argument he attributes to Meyn, derives a single lower bound on the mean number in system for re-entrant lines with deterministic routing (described on p. 16 of the paper).
• 1992–1994: Bertsimas, Paschalidis and Tsitsiklis — parametric families of linear bounds for general open networks with Markovian routing (Theorem 4.1), and the nonparametric polyhedron (Theorems 4.2–4.4), shown to be at least as tight.

Setting

A network has $N$ single-server stations and $R$ job classes. Class $r$ is served at station $\sigma(r)$, and $C_i$ is the set of classes served at station $i$. Class-$r$ jobs arrive from outside as a Poisson stream of rate $\lambda_{0r}$, service times are exponential with rate $\mu_r$, and after service a class-$r$ job becomes a class-$s$ job with probability $p_{rs}$ or leaves with probability $p_{r0}=1-\sum_s p_{rs}$. The traffic equations

$$\lambda_r=\lambda_{0r}+\sum_{r'}\lambda_{r'}p_{r'r}\qquad(15)$$

have a unique solution $\lambda$ (the network is open), and $\sum_{r\in C_i}\lambda_r/\mu_r<1$ at every station.

The state $\vec n=(n_1,\dots,n_R)$ counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write $B_r$ for the event that station $\sigma(r)$ serves class $r$, and $B_{0i}$ for the event that station $i$ is idle. Under such a policy $\vec n(t)$ is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution $\pi$ and that $E_\pi[n_r^2]<\infty$ for all $r$. Let $\bar n_r=E_\pi[n_r]$, which equals $\lambda_rx_r$ with $x_r$ the mean response time of class $r$ (Little's law), and define

$$I_{rr'}=E_\pi[1\{B_r\}n_{r'}],\qquad N_{ir'}=E_\pi[1\{B_{0i}\}n_{r'}].$$

For a set $S$ of classes, f-parameters are reals $f(r)\ge 0$ for $r\in S$ such that $\mu_r\big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))+\sum_{r'\notin S}p_{rr'}f(r)\big]$ is nonnegative and the same for all $r\in C_i\cap S$; that common value is $f_i$, and $f_i=0$ when $C_i\cap S=\emptyset$ (restriction (17)). The sums over $r'\notin S$ include the exit $r'=0$.

Formalization targets

Goal: Theorem 4.1

For every policy satisfying Assumption A, every $S$ and every f-parameters satisfying (17),

$$\sum_{r\in S}\lambda_rf(r)x_r\ \ge\ \frac{N'(S)}{D'(S)},$$

where

$$N'(S)=\sum_{r\in S}\lambda_{0r}f^2(r)+\sum_{r\notin S}\lambda_r\sum_{r'\in S}p_{rr'}f^2(r')+\sum_{r\in S}\lambda_r\Big[\sum_{r'\in S}p_{rr'}(f(r)-f(r'))^2+\sum_{r'\notin S}p_{rr'}f^2(r)\Big],$$ $$D'(S)=2\Big[\sum_{i=1}^Nf_i-\sum_{r\in S}\lambda_{0r}f(r)\Big].$$

The formal goal is the product form $N'(S)\le D'(S)\sum_{r\in S}f(r)\bar n_r$.

Milestones

1. The utilization identity $E_\pi[1\{B_r\}]=\lambda_r/\mu_r$ (pp. 16 and 19).
2. Theorem 4.2: the linear equalities (24), (25) between $\bar n_r$ and $I_{rr'}$.
3. Theorem 4.3: $\sum_{r\in C_i}I_{rr'}+N_{ir'}=\bar n_{r'}$ (28).
4. Theorem 4.4: any nonnegative $(x,I,N)$ satisfying (24), (25), (28), with $\bar n_r=\lambda_rx_r$ in those equalities, satisfies every inequality of Theorem 4.1. This statement is deterministic.

Significance

Theorem 4.1 gives, for each choice of $S$ and $f$, a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost $\sum_r c_rx_r$ subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables $(\bar n,I,N)$ implies all of these inequalities at once, so the parametric search over $f$ is unnecessary.

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.

Difficulty

Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions ($n_r$, $n_rn_{r'}$) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending $\sum_n\pi(n)(\mathcal Gg)(n)=0$ to quadratic $g$ needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify $\mu_rE_\pi[1\{B_r\}]$ with $\lambda_r$. Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because $f\ge0$ on $S$, $f_i\ge0$ and at most one class per station is in service.

Formalization scope

Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs $\tau_k$ of the paper are not built: the paper notes that its expectations at $\tau_k$ are expectations under the invariant distribution of $\vec n(t)$.

Conventions fixed in Lean:

• $\lambda_rx_r$ appears only as the mean number in system $\bar n_r$ (Little's law, used by the paper on pp. 11 and 20); response times are not formalized.
• Sums over $r'\notin S$ include the exit $r'=0$ (p. 15).
• f-parameters are nonnegative on $S$ (p. 9).
• The network is open: (15) has a unique solution, and $\lambda$ is an input constrained by (15), never defined from the policy.
• (18) is stated multiplied by $D'(S)$, which avoids Lean's $x/0=0$ and is (18) whenever $D'(S)>0$.

A quotient-form statement of (18) would be trivially true when $D'(S)=0$, and defining $\lambda_r$ as $\mu_rE_\pi[1\{B_r\}]$ would make the utilization identity hold by definition; both are excluded.

Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.

Selected references

• D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan WP #3509-92-MSA, 1992; Ann. Appl. Probab. 4(1), 1994. https://doi.org/10.1214/aoap/1177005200
• C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queuing network control, Math. Oper. Res. 24(2), 1999. https://doi.org/10.1287/moor.24.2.293

Motivation

In the secretary problem, $n$ items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a $1/e$ fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least $1/e$ (Ferguson 1989).

Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a $16$-competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.

Timeline for graphic matroids:

• 2007, Babaioff–Immorlica–Kleinberg: $16$-competitive.
• 2009, Babaioff–Dinitz–Gupta–Immorlica–Talwar (SODA 2009, Theorem 1.5): $3e\approx 8.15$-competitive, through a random reduction to partition matroids. This mission formalizes that result.
• 2009, Korula–Pál (ICALP 2009): $2e$-competitive, by a different reduction.

Setting

Let $G=(V,E)$ be a finite simple graph. Each edge $e$ has a value $v(e)\ge 0$. A set $S\subseteq E$ is independent in the graphic matroid of $G$ if the graph $(V,S)$ has no cycle. The offline optimum is

$$\mathrm{OPT}(G,v)=\max\Big\{\sum_{e\in S}v(e): S\subseteq E\ \text{acyclic}\Big\}.$$

The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is $\alpha$-competitive if $\mathrm{OPT}(G,v)\le\alpha\cdot\mathbb E[\text{value of the selected set}]$ for every $G$ and every $v\ge 0$.

A partition matroid on a subset $U'\subseteq E$ is given by a family $P$ of nonempty, pairwise disjoint parts with union $U'$: a set is independent when it lies in $U'$ and meets each part at most once. Its max-weight base has value $\mathrm{val}(P,v)=\sum_{p\in P}\max_{e\in p}v(e)$.

Definition 5.1. A random partition $\mu$ (a probability distribution on such families, chosen from $G$ alone) is an $\alpha$-partition scheme if every partition in its support has only acyclic independent sets, and for every $v\ge 0$,

$$\mathrm{OPT}(G,v)\le \alpha\cdot\mathbb E_{P\sim\mu}[\mathrm{val}(P,v)].$$

The random partition of Lemma 5.3. Pick an edge $\{u,w\}$ uniformly at random. With probability $\tfrac12$ colour $u$ red and $w$ blue, otherwise the reverse. Colour every other vertex red or blue independently with probability $\tfrac12$. Each red vertex $x$ gets a part: the red-blue edges at $x$. Then repeat on the edges with both endpoints blue, with fresh randomness.

The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.

Formalization targets

Goal: Theorem 1.5

For every finite simple graph $G$ and every $v\ge 0$:

1. every possible output of the algorithm is an acyclic set of edges of $G$;

$$\mathrm{OPT}(G,v)\le 3e\cdot\mathbb E[\mathrm{ALG}].$$

Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.

Milestones

• Section 2, p. 4. On $m\ge1$ arrivals, the classical rule selects the maximum with probability at least $1/e$.
• Theorem 5.4, first clause. For a fixed partition $P$, the per-part rule outputs a set independent in the partition matroid, and $\mathrm{val}(P,v)\le e\cdot\mathbb E_\pi[\mathrm{ALG}]$.
• Lemma 5.3, independence. Every partition the random construction can produce is a partition matroid on a subset of $E$, and each of its independent sets is a forest.
• Lemma 5.3. The construction is a $3$-partition scheme.
• Section 5, p. 10. Any $\alpha$-partition scheme for a graphic matroid, combined with the per-part rule, gives a feasible, $e\alpha$-competitive algorithm.

Significance

The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an $\alpha$-partition property.

The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant $3e$ is not the best known for graphic matroids (Korula–Pál improve it to $2e$), so the formal goal is this algorithm's guarantee, not the best possible ratio.

Difficulty

The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.

Formalization scope

• Graph. A SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of $S$ is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.
• Values. Values are a real function v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.
• OPT is a Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.
• Random partition. A PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.
• Random order. The edges are numbered by a fixed enumeration. An arrival order is a permutation of the numbers, and expectation over the order is the average over all $|E|!$ permutations.
• Classical rule. It samples $\lfloor m/e\rfloor$ arrivals of a part with $m$ edges. Ties are broken by preferring the smaller edge number among equal values.
• Constants. Competitiveness is multiplicative ($\mathrm{OPT}\le 3e\cdot\mathbb E[\mathrm{ALG}]$), so a zero expectation is not a loophole.
• Ruling out trivial formalizations. In Definition 5.1 the random partition is fixed before the valuation, and the independence requirement holds for every partition in its support. A partition allowed to depend on $v$ would make every matroid $1$-partitionable.

A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443. https://dl.acm.org/doi/10.5555/1283383.1283429
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Matroid Secretary Problems, Journal of the ACM 65(6), 2018. https://doi.org/10.1145/3212512
• N. Korula, M. Pál, Algorithms for Secretary Problems on Graphs and Hypergraphs, ICALP 2009, LNCS 5556. https://doi.org/10.1007/978-3-642-02930-1_42
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493