Probability

Motivation

Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.

The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.

Setting

A state is an element $s$ of a nonempty standard Borel space $S$, and an action is an element $a$ of a nonempty standard Borel space $A$. The transition kernel $q(\cdot\mid s,a)$ gives a probability distribution for the next state after action $a$ in state $s$. The reward $r(s,a,s')\in\mathbb R$ may depend on that next state $s'$; it is bounded and Borel measurable. Future rewards are discounted by $\beta$ with $0\le\beta<1$. These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.

A plan $\pi=(\pi_1,\pi_2,\ldots)$ assigns a probability distribution of actions to each possible history before a decision. At stage $n$, that history contains $n-1$ completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function $f_n:S\to A$ at each stage; a stationary plan uses the same function $f$ at every stage and is denoted $f^{(\infty)}$. Starting from state $s$, the plan has discounted expected return

$$I(\pi)(s)=\sum_{n=1}^{\infty}\beta^{n-1}\,\mathbb E_s^\pi\bigl[r(\sigma_n,\alpha_n,\sigma_{n+1})\bigr].$$

Here $\sigma_n$ and $\alpha_n$ are the state and action at stage $n$. The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.

Two actions are equivalent at state $s$ when they have the same reward $r(s,a,s')$ for every next state $s'$ and the same transition measure $q(\cdot\mid s,a)$. An action set is essentially countable by a Markov plan $(f_1,f_2,\ldots)$ if, for every $(s,a)$, one of the actions $f_n(s)$ is equivalent to $a$ at $s$. It is essentially finite by that plan if $S$ has a countable Borel partition $(S_n)$ such that, for $s\in S_n$, one of $f_1(s),\ldots,f_n(s)$ is equivalent to every action $a$ at $s$. A finite action set is a special case. Blackwell 1965, pp. 233–234.

Formalization targets

For a probability distribution $p$ on $S$ and $\varepsilon>0$, $(p,\varepsilon)$-optimality asks for a stationary $f$ with

$$p\{s:I(\pi)(s)>I(f^{(\infty)})(s)+\varepsilon\}=0\qquad\text{for every plan }\pi.$$

Theorem 6(b) asserts that such an $f$ always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform $\varepsilon$-optimality statement: for every $\varepsilon>0$ there is a stationary $f$ with $I(\pi)(s)\le I(f^{(\infty)})(s)+\varepsilon$ for all $\pi,s$. Its other targets identify the optimal return with the fixed point of the operator $U_\pi u=\sup_nT_{f_n}u$ and with the unique bounded solution of the optimality equation $u=\sup_{a\in A}T_au$. Blackwell 1965, pp. 232–234.

The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary $f$ with exact optimality:

$$I(\pi)(s)\le I(f^{(\infty)})(s)\qquad\text{for every plan }\pi\text{ and state }s.$$

The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.

Significance

The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.

Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.

Difficulty

On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an $\varepsilon$-optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.

Formalization scope

The Lean model uses nonempty StandardBorelSpace types for $S$ and $A$. “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on $S\times A\times S$, and $0\le\beta<1$; $\beta=0$ is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by $0$ in Lean, corresponding to the paper’s index $1$. The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.

For the operator results, $M(S)$ means bounded and measurable real functions. The suprema defining $U_\pi$ and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps $M(S)$ into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece $n$ corresponds to the paper’s $S_{n+1}$, with rules $f_1,\ldots,f_{n+1}$.

An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.

Selected references

• David Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1), 226–235, 1965. DOI: 10.1214/aoms/1177700285.

Motivation

How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate $\lambda$, service times are exponential with mean $1/\mu$, and $N$ agents serve in parallel. Practitioners use the square-root safety staffing rule $N \approx \lambda/\mu + y\sqrt{\lambda/\mu}$, which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from $0$ and $1$.

Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.

Setting

Fix a service rate $\mu > 0$. For every arrival rate $\lambda > 0$ a waiting-cost function $D_\lambda$ assigns cost $D_\lambda(t)$ to a wait of $t$ time units; it satisfies $D_\lambda(0) = 0$, is strictly increasing, and $t \mapsto D_\lambda(t)e^{-\theta t}$ is integrable on $(0,\infty)$ for every $\theta > 0$. A staffing cost $F$, defined for real $N > 0$, is convex and strictly increasing.

For an integer $N > \lambda/\mu$ the probability of waiting is the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Bigl\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Bigr\}^{-1},\qquad \nu = \lambda/\mu,$$

the expected waiting cost of a delayed customer is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$, and the total cost per unit time is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$. An optimal staffing level $N^*_\lambda$ minimizes $C(\cdot,\lambda)$ over the integers $N > \lambda/\mu$.

Write $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, and for $x > 0$ put $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, and $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$, where $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$ extends the Erlang-C formula to real $M$. The normalized cost is $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, and a surrogate cost is $C[z;\hat F,\hat\pi,\hat G] = \hat F(z) + \hat\pi(z)\hat G(z)$. Rounding is measured by $S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda), C(\lceil N_\lambda(x)\rceil,\lambda)\}$.

Two special functions appear. The Halfin–Whitt delay function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. The Stirling-type approximation is

$$Q_\lambda(x) = \frac{\exp\{N_\lambda(x)[1 - r_\lambda(x) + \log r_\lambda(x)]\}}{\sqrt{2\pi N_\lambda(x)}\,(1-r_\lambda(x))},\qquad r_\lambda(x) = \frac{\lambda/\mu}{N_\lambda(x)}.$$

Asymptotic relations are limits of ratios as $\lambda\to\infty$: $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$, and $a_\lambda \stackrel{\infty}{\ll} b_\lambda$ means $a_\lambda/b_\lambda \to 0$.

Formalization targets

Goal: Theorem 7.1

Assume the regime is quality-driven, display (27): $F_\lambda(\kappa) \stackrel{\infty}{\ll} G_\lambda(\kappa)$ for every $\kappa > 0$. Let $y^*_\lambda$ minimize $F_\lambda(y) + Q_\lambda(y)G_\lambda(y)$ over $y > 0$. Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.

Milestones

In attack order: Lemma C.1 ($G_\lambda$ strictly convex decreasing); the identity $H(N,\nu) = \pi(N,\nu)$ at integer $N$ (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ($P$ strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, $\pi_\lambda(x_\lambda) \stackrel{\infty}{\approx} Q_\lambda(x_\lambda)$ whenever $x_\lambda\to\infty$.

Significance

Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function $P$ is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows $\sqrt{\lambda/\mu}$ and $P$ must be replaced by the Stirling-type expression $Q_\lambda$. The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over $N$ into a smooth problem, and it marks the boundary of validity of square-root staffing.

The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of $G_\lambda$ and of $P$, the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.

Difficulty

The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of $\pi_\lambda$ at a staffing excess $x_\lambda$ that may grow at any rate, from barely faster than a constant to faster than $\sqrt{\lambda}$, where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension $\pi_\lambda$ at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum $x^*_\lambda$ or the surrogate optimum $y^*_\lambda$ says that they do.

Formalization scope

Lean represents $\lambda$ as a positive real, and $\lambda\to\infty$ is the filter atTop on $\mathbb{R}$ with $\mu$ fixed. The standing assumptions on $\mu$ and $D_\lambda$ are the structure WaitModel; $F$ is a function argument with hypotheses ConvexOn and StrictMonoOn on $(0,\infty)$. Staffing levels $N$ are natural numbers. Minimizers ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are function arguments with minimality hypotheses at every $\lambda > 0$, so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.

The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost $C(N,\lambda)$ with the Erlang-C formula.

Conventions committed to: (i) the goal adds the hypothesis $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$, which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when $D_\lambda$ is unbounded); (ii) in $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, since the cost is undefined at unstable levels; (iii) the integrability of $D_\lambda(t)e^{-\theta t}$ is explicit, because a Lean integral of a non-integrable function is $0$; (iv) $P(0) = 1$, the value of formula (11) at $0$; (v) display (15) is stated for $b > 0$, since the ratio $a_\lambda/b$ is undefined at $b = 0$. The instance $\mu = 1$, $F(N) = cN$, $D_\lambda(t) = a\sqrt{\lambda}\,t$ (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking $\pi_\lambda$ or $G_\lambda$ at Lean default values is ruled out by these explicit domain conditions.

Only the first statement of Lemma 4.2 is a milestone: the second, $\pi_\lambda(x_\lambda)\approx Q(x_\lambda)$ under $x_\lambda \stackrel{\sup}{\le} \lambda^{1/6}$, fails as printed at $x_\lambda = \lambda^{1/6}$. Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000 (the version formalized here; every index and page cited in this mission is the report's).
• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, 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
• N. Gans, G. Koole, A. Mandelbaum, Telephone Call Centers: Tutorial, Review, and Research Prospects, Manufacturing & Service Operations Management 5(2):79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071

Why staffing large call centers is a mathematical question

A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.

The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.

The Erlang-C cost model

Customers arrive at rate $\lambda>0$ and receive exponential service at rate $\mu>0$ per server. The service rate $\mu$ is fixed as $\lambda$ grows. For an integer number of servers $N>\lambda/\mu$, the Erlang-C delay probability $\pi(N,\lambda/\mu)$ is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate $N\mu-\lambda$. Let $D_\lambda(t)$ be the cost of a wait of length $t$. It is strictly increasing on $t\ge0$, satisfies $D_\lambda(0)=0$, and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is

$$G(N,\lambda)=(N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt.$$

The staffing cost $F(N)$ is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real $N>0$. Total cost per unit of time at a stable integer level is

$$C(N,\lambda)=F(N)+\lambda\pi(N,\lambda/\mu)G(N,\lambda).$$

Write $N^*_\lambda$ for any minimizing stable integer level. Ties are permitted. For a positive real offset $x$, define $N_\lambda(x)=\lambda/\mu+x\sqrt{\lambda/\mu}$, $F_\lambda(x)=F(N_\lambda(x))-F(\lambda/\mu)$, and $G_\lambda(x)=\lambda G(N_\lambda(x),\lambda)$. The report extends Erlang-C continuously to $\pi_\lambda(x)$ and writes the incremental continuous objective as $C_\lambda(x)=F_\lambda(x)+\pi_\lambda(x)G_\lambda(x)$. These definitions and the integer-extension identity are from Section 3, printed pages 11–12.

Formalization targets

The report defines the efficiency-driven regime by

$$\text{for every }\kappa>0,\qquad \lim_{\lambda\to\infty}\frac{F_\lambda(\kappa)}{G_\lambda(\kappa)}=+\infty.$$

For each $\lambda>0$, choose $y^*_\lambda>0$ to minimize $F_\lambda(y)+G_\lambda(y)$ over $y>0$. Let $S_\lambda(y)$ be the smaller cost of the stable integer levels immediately below and above $N_\lambda(y)$; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is

$$\lim_{\lambda\to\infty} \frac{S_\lambda(y^*_\lambda)-F(\lambda/\mu)} {C(N^*_\lambda,\lambda)-F(\lambda/\mu)}=1.$$

The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.

What the result gives

The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline $F(\lambda/\mu)$, which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.

The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.

Where the difficulty lies

The simple objective replaces the delay probability $\pi_\lambda(y)$ by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with $\lambda$. Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when $N_\lambda(y)$ is just above $\lambda/\mu$, its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.

Formalization scope and conventions

Lean represents $\lambda$, $\mu$, offsets, and costs as real numbers; arrival-rate limits use the real filter at $+\infty$. Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of $D_\lambda$ on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for $G$ and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on $F$ are convexity and strict increase on positive real staffing levels; $F$ does not depend on $\lambda$.

The report asserts that $G(N,\lambda)$ diverges as $N$ decreases to $\lambda/\mu$, although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.

All formulas are total Lean functions. Their values at $\lambda\le0$, unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of $S_\lambda$ ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.

The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.

Selected references

• Sem Borst, Avi Mandelbaum, and Martin I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000. Report PDF. Theorem 6.1, printed p. 19; Corollary 3.3, printed p. 14; Lemma 4.1, printed p. 15; Lemma C.1, printed p. 40.

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

The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative $i$ with probability proportional to $e^{z_i\theta}$, where $z_i$ is a vector of observed attributes and $\theta$ an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate $\theta$ by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.

Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.

Setting

Observations are indexed serially, $m = 0, 1, 2, \dots$, as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation $m$ offers $J_m \ge 1$ alternatives, and alternative $i$ carries a vector $z_{im} \in \mathbb R^K$ of independent variables. For a parameter $\theta \in \mathbb R^K$ the selection probabilities are

$$P_{im}(\theta) = \frac{e^{z_{im}\theta}}{\sum_{j=1}^{J_m} e^{z_{jm}\theta}}, \qquad \bar z_m(\theta) = \sum_{i} P_{im}(\theta)\, z_{im}.$$

The data are generated at a true parameter $\theta^0$: the chosen alternatives $Y_0, Y_1, \dots$ are independent random variables with $\Pr(Y_m = i) = P_{im}(\theta^0)$. The log-likelihood of the first $q$ observations is $L^q(\theta) = \sum_{m<q}\log P_{Y_m m}(\theta)$. The moment matrix of observation $m$ is

$$\Omega_m = \sum_{i} P_{im}(\theta^0)\,(z_{im}-\bar z_m)(z_{im}-\bar z_m)', \qquad \bar z_m = \bar z_m(\theta^0).$$

Axiom 7 asks that $J_m \le J_*$ and $|z_{im}| \le M$ uniformly, and that $\frac1q\sum_{m<q}\Omega_m$ converge to a positive definite matrix $\Omega$. Axiom 6, for a given sample, asks that no nonzero $\gamma$ satisfy $(z_{jm} - z_{Y_m m})\gamma \le 0$ for all observed $m$ and all $j$. A maximum likelihood estimator $\hat\theta^q$ is a measurable choice of a maximizer of $L^q$, wherever one exists.

Formalization targets

Goal: Lemma 6

$$\hat\theta^q \xrightarrow{\Pr} \theta^0 \quad\text{and}\quad \sqrt q\,\Omega^{1/2}(\hat\theta^q - \theta^0) \xrightarrow{d} N(0, I_K) \qquad (q \to \infty).$$

Milestones

1. Axiom 7 implies Axiom 5 (the full-rank condition) in all sufficiently large samples.
2. Equation (42): $P_{im}(\theta) \ge 1/(J_* e^{2M|\theta|})$.
3. Lemma 5: $\Pr(\text{Axiom 6 holds and } L^q \text{ attains its maximum}) \to 1$.
4. Equation (43): the first three derivatives of $\log P_{im}$ are bounded by $2M$, $4M^2$, $8M^3$.
5. Equation (46): each score $\nabla\log P_{Y_m m}(\theta^0)$ has mean zero.
6. Equation (47): each expected Hessian equals $-\Omega_m$.
7. Consistency of $\hat\theta^q$.
8. Equation (58): $q^{-1/2}\,\Omega^{-1/2}\sum_{m<q}\nabla\log P_{Y_m m}(\theta^0) \xrightarrow{d} N(0, I_K)$.

Significance

The result. Lemma 6 is what licenses reading $\hat\theta^q$ as approximately $N(\theta^0, q^{-1}\Omega^{-1})$, so that the diagonal of the inverse information matrix estimates the sampling variances and $q(\hat\theta^q-\theta^0)'\Omega(\hat\theta^q-\theta^0)$ is asymptotically $\chi^2_K$. Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction $\gamma$ of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.

Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization $1/q$ in (58), which must be $1/\sqrt q$, and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.

Difficulty

The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around $\theta^0$, controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances $\Omega_m$ that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin K); $z\theta$ is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.
• The paper's $N$ trials with $R_n$ repetitions are the special case of the serial indexing in which consecutive observations repeat their data; the sample size $\sum_n R_n$ is $q$.
• Axiom 7's limit (27) is taken in its serial form (48), with $P$ evaluated at $\theta^0$.
• The estimator is any measurable selection that maximizes $L^q$ whenever $L^q$ has a maximum, and is unconstrained otherwise. Requiring a maximizer for every sample would be unsatisfiable, since Axiom 6 fails with positive probability, and would make the goal vacuous; this convention rules that out.
• Consistency is TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. $\Omega^{1/2}$ is the positive semidefinite square root CFC.sqrt.
• Needed infrastructure: derivatives of log-sum-exp, a law of large numbers for bounded independent vectors, and a multivariate Lindeberg–Feller theorem. Mathlib provides the one-dimensional i.i.d. central limit theorem only. Contributions of these general results as separate theorems are welcome.

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, Wiley, 1966 (Lindeberg–Feller theorem, pp. 256–258).
• C. R. Rao, Linear Statistical Inference and Its Applications, Wiley (cited by McFadden as Rao (1968), pp. 347–351, for the asymptotic $\chi^2$ test).

Motivation

Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point $x$ does not change for any perturbation $\delta$ in a stated set, typically an $\ell_2$ ball $\|\delta\|_2<R$. Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$ (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.

Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.

Setting

Inputs live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|_2$; classes form a set $\mathcal Y$. A base classifier is a map $f:\mathbb R^d\to\mathcal Y$ with Borel decision regions. For a noise level $\sigma>0$, write $\mathcal N(x,\sigma^2I)$ for the isotropic Gaussian law of $x+\varepsilon$ with $\varepsilon\sim\mathcal N(0,\sigma^2I)$. The class probability of $c$ at $x$ is $\mathbb P(f(x+\varepsilon)=c)$, and the smoothed classifier is

$$g(x)=\arg\max_{c\in\mathcal Y}\ \mathbb P(f(x+\varepsilon)=c).$$

Let $\Phi$ be the standard Gaussian CDF and $\Phi^{-1}$ its inverse on $(0,1)$. A classifier $f$ is consistent with the observed class probabilities (6) for a top class $c_A$ and numbers $\underline{p_A}\ge\overline{p_B}$ if

$$\mathbb P(f(x+\varepsilon)=c_A)\ \ge\ \underline{p_A}\ \ge\ \overline{p_B}\ \ge\ \max_{c\ne c_A}\mathbb P(f(x+\varepsilon)=c).$$

The certified radius is $R=\frac{\sigma}{2}\big(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B})\big)$. In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces $A=\{z:\delta^T(z-x)\le\sigma\|\delta\|\Phi^{-1}(\underline{p_A})\}$ and $B=\{z:\delta^T(z-x)\ge\sigma\|\delta\|\Phi^{-1}(1-\overline{p_B})\}$ of the paper's Appendix A are setA and setB.

Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.

Formalization targets

Goal: Theorem 2 (corrected)

Assume $0<\overline{p_B}\le\underline{p_A}<1$, $\underline{p_A}+\overline{p_B}\le1$, and that some finite set $s$ of classes other than $c_A$ satisfies $1\le\underline{p_A}+|s|\,\overline{p_B}$. Then for every $\delta$ with $\|\delta\|_2>R$ there is a base classifier $f^*$ consistent with (6) and a class $c\ne c_A$ with

$$\mathbb P(f^*(x+\delta+\varepsilon)=c_A)\ <\ \mathbb P(f^*(x+\delta+\varepsilon)=c),$$

so that $g(x+\delta)\ne c_A$ under any tie-breaking. The classifier may depend on $\delta$.

The class-capacity hypothesis is a correction. As printed, with only $\underline{p_A}+\overline{p_B}\le1$, the theorem fails for two classes: with $\mathcal Y=\{c_A,c_B\}$, $\underline{p_A}=0.6$, $\overline{p_B}=0.1$ and $\sigma=\|\delta\|_2=1$, one has $R\approx0.767<1$, yet every consistent $f$ gives $c_A$ probability at least $0.9$, and Theorem 1 then certifies radius $\Phi^{-1}(0.9)\approx1.28$.

Milestones

The milestones are the steps the paper itself states, in its order: the Claims $\mathbb P(X\in A)=\underline{p_A}$ and $\mathbb P(X\in B)=\overline{p_B}$ for $X\sim\mathcal N(x,\sigma^2I)$; the disjointness of $A$ and $B$ (corrected to "null" when $\underline{p_A}+\overline{p_B}=1$); equations (13) and (14) for $Y\sim\mathcal N(x+\delta,\sigma^2I)$,

$$\mathbb P(Y\in A)=\Phi\Big(\Phi^{-1}(\underline{p_A})-\tfrac{\|\delta\|}{\sigma}\Big),\qquad \mathbb P(Y\in B)=\Phi\Big(\Phi^{-1}(\overline{p_B})+\tfrac{\|\delta\|}{\sigma}\Big);$$

the equivalence $\mathbb P(Y\in A)<\mathbb P(Y\in B)\iff\|\delta\|_2>R$; and the existence of the worst-case classifier $f^*$ satisfying (6) with equalities.

Significance

Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about $f$, the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open $\ell_2$ ball of radius $R$. It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.

The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim $A\cap B=\emptyset$ fails at $\underline{p_A}+\overline{p_B}=1$. To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.

Difficulty

Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on $\mathbb R^d$ under a linear functional $z\mapsto\delta^T z$ is the one-dimensional Gaussian with variance $\|\delta\|^2$, and $\Phi$ is a continuous strictly increasing bijection $\mathbb R\to(0,1)$ with $\Phi^{-1}(1-p)=-\Phi^{-1}(p)$. The construction of $f^*$ has a further step the paper leaves informal: the region between $A$ and $B$, of mass $1-\underline{p_A}-\overline{p_B}$, must be shared among "other classes" with none exceeding $\overline{p_B}$, which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $\mathcal N(x,\sigma^2I)$ is the pushforward of Mathlib's stdGaussian under $z\mapsto x+\sigma z$, with $\sigma>0$ a binder. $\Phi$ is cdf (gaussianReal 0 1); $\Phi^{-1}(p)$ is the generalized inverse $\inf\{t:p\le\Phi(t)\}$, which is the true inverse on $(0,1)$ and the junk value $0$ at the endpoints, so every statement that evaluates it assumes $0<p<1$; at $\overline{p_B}=0$ or $\underline{p_A}=1$ the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of $c_A$ to be a strict unique argmax.

A formalization in which the junk endpoint value of $\Phi^{-1}$ makes $R$ negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.

Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on $(0,1)$. Contributions of general Mathlib-style lemmas (the law of $\delta^T X$ for $X\sim\mathcal N(x,\sigma^2I)$, properties of $\Phi^{-1}$) are welcome.

Selected references

• J. M. Cohen, E. Rosenfeld, J. Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML 2019; arXiv:1902.02918v2. https://arxiv.org/abs/1902.02918v2
• M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, S. Jana, Certified Robustness to Adversarial Examples with Differential Privacy, IEEE S&P 2019. https://arxiv.org/abs/1802.03471
• B. Li, C. Chen, W. Wang, L. Carin, Certified Adversarial Robustness with Additive Noise, NeurIPS 2019. https://arxiv.org/abs/1809.03113
• J. Neyman, E. S. Pearson, On the Problem of the Most Efficient Tests of Statistical Hypotheses, Phil. Trans. R. Soc. A 231, 1933. https://doi.org/10.1098/rsta.1933.0009

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$, each with a nonnegative value $v(e)$, and $K$ goods indexed in decreasing order of nonnegative weight:

$$w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.$$

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$. Its value is $\sum_{k=1}^K v(s(k))w(k)$. Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$, chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$, assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$, the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$, observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$. A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$.

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$, which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$:

$$\mathrm{OPT}\le(8+3e)\,\mathbb E[A].$$

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$. Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class-$i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$, the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$. The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$. It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$. An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$, so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

• Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

Motivation

A martingale difference sequence is the standard model of a "fair" sequence of observations whose terms may depend on the past: each new term has conditional mean zero given everything observed before it. Laws of large numbers for such sequences underlie the analysis of stochastic approximation, sequential estimation and online learning, where the noise terms are dependent but conditionally centred.

Classical strong laws concern averages in which every observation keeps the same weight as the sample grows. Kazuoki Azuma's 1967 paper Weighted sums of certain dependent random variables (Tôhoku Math. J. 19) studies weighted sums of dependent variables, and is best known for the exponential moment bound that is now called the Azuma inequality (its display (2.4) together with Remark 1). Its Theorem 3 uses that bound to prove a strong law for weighted averages in which the weights are applied in reverse order, so that the oldest observation always receives the newest, largest weight.

Timeline:

• 1960s: Y. S. Chow (Ann. Math. Statist. 37, 1966) introduces a conditional exponential-moment condition close to Azuma's property [G] in a convergence theorem for independent variables.
• 1967: Azuma proves the moment bound (2.4) for conditionally sub-Gaussian martingale differences, a law of the iterated logarithm for direct weighted sums (Theorem 2), and the strong law for reversed weighted sums (Theorem 3), the subject of this mission.

Setting

Let $(\Omega,\mathfrak A,P)$ be a probability space and $(\mathfrak A_n)_{n\ge0}$ an increasing family of sub-$\sigma$-fields of $\mathfrak A$. A sequence $(x_n)_{n\ge1}$ of real random variables is a sequence of martingale differences if, for every $n\ge1$, $x_n$ is $\mathfrak A_n$-measurable and integrable and $E\{x_n\mid\mathfrak A_{n-1}\}=0$ almost surely. Theorem 3 assumes moreover $|x_n|\le1$ almost surely for every $n$.

Let $(a_n)_{n\ge1}$ be positive increasing weights: $a_n>0$ and $a_n\le a_{n+1}$. Put

$$A_n = a_1+a_2+\dots+a_n,\qquad \bar S_n = a_nx_1 + a_{n-1}x_2+\dots+a_1x_n=\sum_{j=1}^n a_{n-j+1}x_j .$$

The sums $\bar S_n$ are the reversed weighted sums. In passing from $\bar S_n$ to $\bar S_{n+1}$ every existing term changes its weight, so $(\bar S_n)$ is in general not a martingale. In the Lean development, $A_n$ is A a n, $\bar S_n(\omega)$ is Sbar a x n ω, and the martingale-difference property is IsMartingaleDiff μ ℱ x.

Formalization targets

Goal: Theorem 3, (4.9)–(4.10)

If $(x_n)$ is a sequence of martingale differences with $|x_n|\le1$ a.s., $(a_n)$ is positive and nondecreasing, and

$$\frac{a_n}{A_n}=o\Big(\frac{1}{\log\log A_n}\Big)\qquad(n\to\infty),\tag{4.9}$$

then

$$\frac{\bar S_n}{A_n}\longrightarrow0\quad\text{almost surely}.\tag{4.10}$$

Milestones

The milestones follow the paper's proof, in attack order.

1. Remark 1 (p. 358): if $|x_n|\le K_n$ a.s., then $E\{\exp(tx_n)\mid\mathfrak A_{n-1}\}\le\cosh(tK_n)\le\exp(t^2K_n^2/2)$ a.s.
2. The tail step of (4.16) (p. 366): for $|x_n|\le1$, real $c_1,\dots,c_N$ with $\sum c_j^2>0$ and $\lambda\ge0$,

$$P\Big\{\sum_{j=1}^Nc_jx_j>\lambda\Big\}\le\exp\Big(-\frac{\lambda^2}{2\sum_{j=1}^Nc_j^2}\Big).$$

3. The blocks (4.11)–(4.14) (pp. 364–365): for every $\varepsilon>0$ there are indices $n_1<n_2<\cdots$ with $A_{n_1}>2(3+\varepsilon)/(6+\varepsilon)$, $a_n/A_n<\varepsilon/(6+\varepsilon)$ and $a_n\log\log A_n/A_n<\varepsilon^2/64$ for $n>n_1$, and $A_{n_{k-1}}<A_{n_k}\le(1+\varepsilon/3)A_{n_{k-1}}<A_{n_k+1}$.
4. The maximal inequality (4.15) (p. 365): if $A_{N_1}\le(1+\varepsilon/3)A_{N_0}$ with $1\le N_0<N_1$, then

$$2P\{\bar S_{N_1}>(\varepsilon/2)A_{N_0}\}\ge P\Big\{\max_{N_0<n\le N_1}\bar S_n>\varepsilon A_{N_0}\Big\}.$$

5. Block growth (p. 366): (4.11), (4.12) and (4.14) give $A_{n_k}>(2(3+\varepsilon)/(6+\varepsilon))^{k-1}$.

Significance

The result. Theorem 3 shows that reversed weighting does not destroy the strong law, under a growth condition on the weights that is strictly weaker than the condition $a_n^2/\sum_{j\le n}a_j^2\to0$ of the paper's Theorem 2: the paper reproduces an example of T. Tsuchikura satisfying (4.9) but not that condition. The condition allows rapidly growing weights, provided no single weight carries more than an $o(1/\log\log A_n)$ share of the total. Milestone 2 is the one-sided Azuma inequality in the paper's conditional-expectation form, a tool used throughout probability, combinatorics and learning theory. Milestone 4 is a maximal inequality for a process that is not a martingale, where Doob's inequality cannot be used.

Formalizing it. The theorem is proved in the paper; this mission produces a machine-checked proof. Mathlib contains sub-Gaussian moment-generating-function bounds for martingale differences in a kernel formulation (HasCondSubgaussianMGF, which assumes a standard Borel space), and the Prove2Me platform has two-sided Azuma–Hoeffding inequalities under the same assumption. Neither states Remark 1 or the one-sided tail bound in the paper's conditional-expectation form on an arbitrary probability space, and no strong law for reversed weighted sums is formalized.

Difficulty

The obvious route to a strong law for a martingale, Doob's maximal inequality applied along a geometric subsequence, fails at the first step: $(\bar S_n)$ is not a martingale, because each new step reweights all earlier terms. The maximum of $\bar S_n$ over a block of indices therefore needs a separate maximal inequality, and it is there that the monotonicity of the weights is indispensable. A second difficulty is quantitative: the exponential tail bound must be summable over blocks whose growth is controlled only through (4.9), which is weaker than the variance-type condition of Theorem 2, so the block sizes and the constants $\varepsilon/(6+\varepsilon)$, $\varepsilon^2/64$ and $1+\varepsilon/3$ have to be chosen to fit together.

Formalization scope

Conventions committed to in Lean:

• Indices start at $1$: sums run over Finset.Icc 1 n, and $a_0$, $x_0$ are never used. Every hypothesis on $a$ and $x$ is quantified over $n\ge1$.
• The filtration is a Mathlib Filtration ℕ. Its first $\sigma$-field plays the role of $\mathfrak A_0$ and is arbitrary rather than trivial; the paper's $\mathfrak A_0=\{\emptyset,\Omega\}$ is a special case, so the formal statements are at least as general.
• "Positive increasing" is read as $a_n>0$ and $a_n\le a_{n+1}$ (nondecreasing), the weaker hypothesis.
• (4.9) is stated literally as a little-$o$ relation (IsLittleO along atTop). $A_n\to\infty$ is not a hypothesis, since it follows from positivity and monotonicity.
• The conclusion is convergence of the real sequence $\bar S_n(\omega)/A_n$ to $0$ for almost every $\omega$, which contains both the upper and the lower tail; a statement giving only $\limsup\le0$ is not the goal. No real-valued limsup is used anywhere.
• Probabilities are real-valued (μ.real); conditional expectations are Mathlib's μ[f | ℱ n].

A formalization of the goal that replaces $\bar S_n$ by the direct sums $a_1x_1+\dots+a_nx_n$, drops the monotonicity of the weights, or strengthens (4.9) to $a_n/A_n=o(1/\log A_n)$ or to $a_n^2/\sum_{j\le n}a_j^2\to0$ states a different theorem and does not count.

A complete development needs the Azuma moment bound in conditional-expectation form, conditional Chebyshev arguments on events, the Borel–Cantelli lemma (in Mathlib) and elementary real analysis of the blocks. The one-sided Azuma inequality and the maximal inequality (4.15) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. https://doi.org/10.2748/tmj/1178243286
• Y. S. Chow, Some convergence theorems for independent random variables, Annals of Mathematical Statistics 37 (1966), 1482–1493.
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.