Operations Research

Why expected interval length matters

A simulation run often estimates a steady-state mean without producing independent observations. A confidence interval must account for dependence in the output, and the relevant variance constant may be unknown. Standardized time series (STS) methods use the shape of an integrated output path to cancel that constant rather than estimating it separately. The resulting interval can be computed from one run, but its length can vary substantially with the chosen standardizing functional. Glynn and Iglehart introduced a common functional framework for these methods and asked how short their expected intervals can be as the run grows. Their 1990 paper identifies a universal lower bound.

The comparison is operational. A shorter confidence interval conveys a more precise estimate at the same nominal coverage. The authors also compare STS with procedures that consistently estimate the variance constant. They state that the lower bound is attained by the latter procedures and approached, but not attained, by STS intervals. The present mission isolates the bound for STS itself, Corollary 4.16. It does not make the claim that a particular STS rule attains it. This distinction follows the paper's introduction and §4.

The stochastic setting

Let $Y(t)$ be a real simulation output process for $t\ge0$. Its integrated average path at run length $n$ is $\overline Y_n(t)=n^{-1}\int_0^{nt}Y(s)\,ds$ for $0\le t\le1$. The unknown steady-state mean is $\mu$. The paper assumes a functional central limit theorem in the space $C[0,1]$ of continuous real paths:

$$X_n(t):=\sqrt n\bigl(\overline Y_n(t)-\mu t\bigr) \ \Rightarrow\ \sigma B(t),\qquad \sigma>0,$$

where $B$ is standard Brownian motion. Convergence is weak convergence of random continuous paths in the uniform topology. This is Assumption (2.1), rather than a claim that every output process satisfies it. The paper lists several classes of processes for which such a theorem is available under further conditions (§2, pp. 2–3).

An STS scale functional $g:C[0,1]\to\mathbb R$ belongs to $\mathcal M$ when it is measurable, positively homogeneous, unchanged by subtracting any multiple of the identity path $k(t)=t$, positive at $B$ almost surely, and continuous at $B$ almost surely. The last two conditions ensure that the Brownian ratio is a meaningful distributional limit. The paper also describes these functionals through the bridge map $(\Gamma x)(t)=x(t)-t x(1)$: a member of $\mathcal M$ can be written as $b\circ\Gamma$ for a suitable $b$. Thus the scale is determined by a Brownian bridge while the endpoint $B(1)$ is independent of it (Propositions 2.7–2.8).

Define $H(x)=P\{B(1)/g(B)\le x\}$. For a confidence level $1-\delta$, choose endpoints $\alpha,\beta$ with $H(\beta)-H(\alpha)=1-\delta$. The STS confidence interval from equation (2.10) has endpoints $\overline Y_n(1)-g(\overline Y_n)\beta$ and $\overline Y_n(1)-g(\overline Y_n)\alpha$. Its length is $L_n=g(\overline Y_n)(\beta-\alpha)$. Here $\delta$ lies strictly between zero and one; the endpoint equation is part of the construction, not an arbitrary choice.

Formalization target

The goal is Corollary 4.16 for every nonnegative $g\in\mathcal M$ under Assumption (2.1). Write $\Phi$ for the standard normal distribution function and $p=\Phi^{-1}(1-\delta/2)$. Then

$$\liminf_{n\to\infty}\sqrt n\,E[L_n] \ \ge\ 2\sigma p =2\sigma\Phi^{-1}(1-\delta/2).$$

The expectation and liminf admit $+\infty$. The statement does not impose an integrability assumption that would remove that case. It quantifies over every admissible STS functional and every interval whose endpoints have the specified Brownian confidence mass (Corollary 4.16, p. 12).

Three substantial targets precede the corollary. Proposition 4.1(a) relates scaled expected length to $\sigma E[g(B)](\beta-\alpha)$. Proposition 4.3 says a symmetric choice of $\alpha,\beta$ minimizes $\beta-\alpha$. Theorem 4.8 gives $E[g(B)]\Phi^{-1}_g(1-\delta/2)\ge\Phi^{-1}(1-\delta/2)$, where $\Phi^{-1}_g$ denotes the quantile of $H$. The milestone list also includes the cited Brownian independence, mixture distribution, scale invariance, and continuous mapping statements that put these targets in context.

What the bound establishes

The corollary supplies a benchmark for the asymptotic expected length of any interval in this STS class. A proposed standardizing functional cannot beat the normal-quantile constant while retaining the stated functional limit and confidence construction. It also identifies the quantity against which the paper's other interval procedures can be compared. The bound applies uniformly to the class $\mathcal M$, not to a chosen batch size or a particular form of $g$ (Glynn–Iglehart 1990, §4).

The mathematical result has been proved in the source paper. This mission supplies formal statements and their shared definitions as proof targets; it does not claim that their Lean proofs already exist. A complete development would formalize the known arguments for the milestones and corollary, including the Brownian path representation, weak convergence, quantile properties, and expectation inequalities. Those components could be reused in other work on simulation output analysis and ratios of weakly convergent processes.

Where the formal proof is demanding

Weak convergence alone does not imply convergence of expectations. In particular, a continuous mapping limit for $g(X_n)$ cannot simply be integrated as an ordinary finite real expectation when the family is not uniformly integrable. Proposition 4.1(a) asks only for a lower bound, and its statement must still account for $E[g(B)]=+\infty$. This is why the goal is expressed with a liminf and extended nonnegative expectations rather than a real-valued limit. A separate difficulty is that the interval width depends jointly on a distributional scale and a choice of two quantiles. Bounding either one in isolation does not state the corollary.

Formalization scope and conventions

Paths are Mathlib's $C([0,1],\mathbb R)$ with its uniform metric and Borel sigma algebra. A standard Brownian motion is a measurable random continuous path agreeing with an $\mathbb R_{\ge0}$-indexed real Brownian motion on $[0,1]$. The paper's discontinuity set $D(g)$ is the set where $g$ is not continuous. Assumption (2.1) includes joint measurability of $Y$ and finite-interval pathwise integrability so that each integrated average is defined. The path $\overline Y_n$ is supplied together with its defining integral equation, which determines it pointwise. Its values are not free parameters.

Indices $n$ are natural numbers. At $n=0$, the average uses Lean's total division and is zero; this initial value does not affect an asymptotic statement. The positive Brownian scale $\sigma$ is finite. The parameters satisfy $0<\delta<1$, and $H(\beta)-H(\alpha)=1-\delta$. The normal and STS quantiles appear as real parameters pinned by their distribution-function equations, avoiding an unbounded or empty real infimum. Expected nonnegative lengths and scales are integrals valued in $\mathbb R_{\ge0}\cup\{+\infty\}$. The class $\mathcal N$ explicitly requires measurability of $b$, the standing convention needed for its equality with $\mathcal M$.

The corollary retains the entire class $\mathcal M$ and Assumption (2.1), with $g\ge0$ on all continuous paths. It cannot be replaced by a statement about a single easy functional or by assuming the bound on an auxiliary criterion. Useful contributions include the Brownian bridge independence theorem, the normal scale-mixture identity, distribution-function regularity, and the asymptotic expectation result.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. DOI: 10.1287/moor.15.1.1.

Why cores of games with side payments

A cooperative game with side payments assigns to each coalition of players the total payoff it can secure on its own and share freely among its members. The core is the set of ways of dividing the payoff of the grand coalition that no coalition can improve upon. It is the basic stability notion of cooperative game theory and of its applications in operations research: cost allocation for shared facilities, network design, inventory pooling and linear production games all ask whether a core allocation exists and what it looks like.

The core can be empty, and the question of when it is not was answered independently by Bondareva (1963) and Shapley (1967): the core is nonempty exactly when the game is balanced, a linear-programming condition on weighted families of coalitions. Scarf (1967) extended the existence half to games without side payments, and Billera (1970) recast balancedness for those games.

Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981) reads these results through fuzzy coalitions, in which each player participates at a rate between 0 and 1. In §6 every game on a family of coalitions is extended to a concave positively homogeneous function of fuzzy coalitions, and the Bondareva–Shapley theorem becomes a statement about that extension. This mission formalizes §2 and §6 of the paper: the core of a fuzzy game with side payments, its superdifferential description, and Proposition 6.1.

Setting

Let $N=\{1,\dots,n\}$ be the set of players. A coalition $A\subseteq N$ is identified with its characteristic vector $\tau^A\in\{0,1\}^n$, and $\tau^N=(1,\dots,1)$. A fuzzy coalition is a vector $\tau\in[0,1]^n$, where $\tau_i$ is the rate at which player $i$ participates.

A fuzzy game with side payments is a worth function $v$ with $v(0)=0$ that is positively homogeneous, $v(t\tau)=t\,v(\tau)$ for $t>0$. Homogeneity extends $v$ from $[0,1]^n$ to the orthant $\mathbb R^n_+$. Its core is

$$\operatorname{core}(v)=\Big\{c\in\mathbb R^n:\ \sum_{i\in N}c_i=v(\tau^N),\ \ \sum_{i\in N}\tau_ic_i\ge v(\tau)\ \text{for all }\tau\in[0,1]^n\Big\},$$

the allocations that no fuzzy coalition blocks. The superdifferential of $v$ at $\tau$ is $\partial v(\tau)=\{c:\ v(\tau)-v(\sigma)\ge\sum_i c_i(\tau_i-\sigma_i)\ \text{for all }\sigma\in\mathbb R^n_+\}$.

A usual game with side payments is given by a family $\mathscr C$ of nonempty coalitions that contains $N$ and every singleton $\{i\}$, and by a worth $v(A)\in\mathbb R$ for each $A\in\mathscr C$. Its core is the set of $c\in\mathbb R^n$ with $\sum_{i\in N}c_i=v(N)$ and $\sum_{i\in A}c_i\ge v(A)$ for every $A\in\mathscr C$. For $\tau\in\mathbb R^n_+$, $\mathscr C(\tau)$ is the set of nonnegative weights $m(A)$, $A\in\mathscr C$, with $\sum_{A\ni i}m(A)=\tau_i$ for each player $i$, and

$$\pi v(\tau)=\sup_{m\in\mathscr C(\tau)}\ \sum_{A\in\mathscr C}m(A)\,v(A).$$

The game is balanced if $\pi v(\tau^N)=v(N)$.

Formalization targets

Goal: Proposition 6.1

$$\operatorname{core}(v)\neq\emptyset\iff \pi v(\tau^N)=v(N),\qquad\text{and then}\qquad \operatorname{core}(v)=\operatorname{core}(\pi v).$$

The first half is the Bondareva–Shapley theorem for an arbitrary family $\mathscr C$. The second identifies the core of the discrete game with the core of the fuzzy game $\pi v$.

Milestones

1. §2 (4)–(5). For a positively homogeneous $v$ with $v(0)=0$, $\operatorname{core}(v)=\partial v(\tau^N)$.
2. Remark 2.1. Such a $v$ is concave on $\mathbb R^n_+$ if and only if it is superadditive, $v(\tau+\sigma)\ge v(\tau)+v(\sigma)$.
3. Proposition 2.1. If $v$ is moreover concave, its core is convex, compact and nonempty; if $v$ is differentiable at $\tau^N$, the core is $\{Dv(\tau^N)\}$.
4. §6 (5). If $m\in\mathscr C(\tau)$ and $m(A)>0$, then $A\subseteq A_\tau=\{i:\tau_i>0\}$.
5. §6 (2). $\pi v$ is the smallest concave positively homogeneous function on $\mathbb R^n_+$ with $\pi v(\tau^A)\ge v(A)$ for every $A\in\mathscr C$.
6. §6, after (6). The core of the fuzzy game $\pi v$ is nonempty, convex and compact, whether or not $v$ is balanced.

Significance

Proposition 6.1 is the standard criterion for the existence of core allocations in transferable-utility games. In operations research it is the tool behind core results for linear production games, flow games, facility location and inventory games: one exhibits a family of balancing weights, or the absence of one, and reads off whether a stable cost or profit allocation exists. Aubin's version adds that a balanced game's core is the superdifferential of a concave function, so it is described by convex analysis and, when $\pi v$ is smooth at $\tau^N$, reduces to a single point given by the gradient.

The result is classical and proved in the literature. To our knowledge, no machine-checked proof of the Bondareva–Shapley theorem exists in Mathlib or on this platform: the platform has results on cores of convex (supermodular) games, which are a different hypothesis. The mission therefore produces a first formal proof of the theorem for a general family $\mathscr C$ of coalitions, the superdifferential description of the fuzzy core, and the minimality of the concave extension $\pi v$. The definitions (fuzzy coalitions, balances, $\pi v$) are reusable by later missions on games without side payments and on values of fuzzy games.

Difficulty

The inclusion $\operatorname{core}(v)\subseteq\operatorname{core}(\pi v)$ and the necessity of balancedness are short computations with the balancing weights. The difficulty is sufficiency: from $\pi v(\tau^N)=v(N)$, a core allocation has to be produced. This is an existence statement for a system of linear inequalities, and it needs a duality or separation argument. Mathlib's finite-dimensional linear programming duality and separation theorems do not apply off the shelf, because $\pi v$ is a supremum over a polytope of weights indexed by coalitions, and its attainment and finiteness must be established first. Proposition 2.1 similarly needs the existence of supergradients of a concave function at an interior point and their compactness, which are not packaged for functions defined only on an orthant.

Formalization scope

Players are Fin n; multiutilities and fuzzy coalitions are Fin n → ℝ with the coordinatewise order, and the cube is Set.Icc 0 1. The commitments are:

• A fuzzy game is a function on $\mathbb R^n$ whose values off the orthant are never used; $v(0)=0$ and homogeneity for every $t>0$ and $\tau\ge0$ are hypotheses of every §2 statement, because §2 states them once for the whole section. Concavity is concavity on $\mathbb R^n_+$.
• In the superdifferential (5), $\sigma$ ranges over $\mathbb R^n_+$, the domain of the extended $v$; the paper leaves this implicit.
• "Differentiable at $\tau^N$" is DifferentiableAt at the interior point $(1,\dots,1)$, and $Dv(\tau^N)$ is the vector of partial derivatives.
• The family $\mathscr C$ contains $N$ and all singletons and excludes $\emptyset$; the core and $\pi v$ use only coalitions in $\mathscr C$, so $v(\emptyset)=0$ plays no role. Because $N\in\mathscr C$ and $\emptyset\notin\mathscr C$, the family exists only for $n\ge1$.
• $\pi v$ is a real supremum. For $\tau\ge0$ the set of values is nonempty and bounded above, so the value is the paper's; off the orthant the set is empty and the value is never used.
• The printed $v(\mathscr C)$ and $\tau^{\mathscr C}$ in §6 (2)–(3) are read as $v(A)$ and $\tau^A$, as §6 (4) settles.

Balancedness is the equation $\pi v(\tau^N)=v(N)$ with $\pi v$ built from the balances of §6 (3)–(4); a formalization that defines "balanced" through the core, or takes $\pi v$ to be an envelope already known to agree with the core, makes the goal empty and is ruled out. Contributions welcome: proofs of the milestones, a general Bondareva–Shapley lemma for finite families of coalitions, and supergradient existence for concave functions on convex sets with nonempty interior.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1), 1981, 1–13. https://doi.org/10.1287/moor.6.1.1
• O. N. Bondareva, Some applications of linear programming methods to the theory of cooperative games, Problemy Kibernetiki 10, 1963, 119–139 (in Russian; no stable online copy).
• L. S. Shapley, On balanced sets and cores, Naval Research Logistics Quarterly 14(4), 1967, 453–460. https://doi.org/10.1002/nav.3800140404
• H. E. Scarf, The core of an N person game, Econometrica 35(1), 1967, 50–69. https://doi.org/10.2307/1909703
• L. J. Billera, Some theorems on the core of an n-person game without side-payments, SIAM Journal on Applied Mathematics 18(3), 1970, 567–579. https://doi.org/10.1137/0118007
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Many decisions are made before their objective coefficients are known. A planner may know the feasible decisions and the form of a linear optimization problem, but must predict its cost vector from available features. Squared prediction error measures how close a forecast is to the eventual coefficients; it need not measure the quality of the decision chosen with that forecast. Elmachtoub and Grigas define a loss based on the excess realized cost of the resulting decision, then introduce a convex surrogate, SPO+, for training prediction rules Elmachtoub and Grigas, 2020, §§2–3.

The central population question is whether minimizing the surrogate still selects predictions that minimize the decision loss when the full data distribution is available. Their Theorem 1 answers this under conditions on the feasible region and the conditional distribution of costs Elmachtoub and Grigas, 2020, p. 21. The result concerns the loss itself, before sample size, model capacity, or an algorithm for fitting a predictor enter the picture.

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact, and convex. Given a cost vector $c\in\mathbb R^d$, a decision $w\in S$ incurs cost $c^\top w$. The nominal value, optimal-decision set, and support function are

$$z^*(c)=\min_{w\in S}c^\top w,\qquad W^*(c)=\arg\min_{w\in S}c^\top w,\qquad \xi_S(c)=\max_{w\in S}c^\top w.$$

An optimization oracle $w^*$ returns one element of $W^*(c)$ for each $c$, without a tie-breaking rule. For a predicted cost $\hat c$ and realized cost $c$, the unambiguous SPO loss uses the worst realized decision among all decisions optimal for the prediction:

$$\ell_{\mathrm{SPO}}(\hat c,c) =\max_{w\in W^*(\hat c)}c^\top w-z^*(c).$$

This is Definition 2 of the paper. Its SPO+ loss, Definition 3, is

$$\ell_{\mathrm{SPO+}}(\hat c,c) =\xi_S(c-2\hat c)+2\hat c^\top w^*(c)-z^*(c).$$

The factor $2$ is fixed by the paper's surrogate. Proposition 3 states that SPO+ upper-bounds SPO, is convex in $\hat c$, and has the explicit subgradient $2(w^*(c)-w^*(2\hat c-c))$ Elmachtoub and Grigas, 2020, pp. 17–18.

Let $x$ denote an observed feature, $\nu$ its probability law, and $\kappa_x$ the conditional law of $c$ given $x$. Their joint law is $D=\nu\otimes\kappa$. A measurable predictor $f$ maps each $x$ to a cost prediction $f(x)$. The population risks $R_{\mathrm{SPO}}(f)$ and $R_{\mathrm{SPO+}}(f)$ are expectations over $(x,c)\sim D$ of the corresponding losses at $(f(x),c)$, as in displays (11) and (12) Elmachtoub and Grigas, 2020, p. 20. There is no prescribed parametric predictor class.

Formalization targets

Theorem 1: Fisher consistency of SPO+

Write $m(x)=\mathbb E[c\mid x]$. Under Assumption 1, the optimal-decision set $W^*(m(x))$ is a singleton for almost every $x$; each conditional law is centrally symmetric about $m(x)$ and continuous on all of $\mathbb R^d$; and $S$ has nonempty interior. The goal says that every measurable minimizer $f$ of SPO+ population risk satisfies

$$f(x)=m(x)\quad\text{for }\nu\text{-almost every }x, \qquad R_{\mathrm{SPO}}(f)\le R_{\mathrm{SPO}}(g) \quad\text{for every measurable }g.$$

This is the paper's Fisher-consistency statement, including its stronger identification of every SPO+ minimizer with the conditional mean Elmachtoub and Grigas, 2020, Theorem 1. The goal does not assert that a minimizer exists.

Supporting propositions

The milestone list follows the paper's numbered results: Proposition 3's pointwise upper bound, convexity, and subgradient; Proposition 6's mean minimizer and uniqueness claims for a single cost law; and both directions of Proposition 5, which relate SPO risk minimizers to decisions optimal at the mean Elmachtoub and Grigas, 2020, pp. 18, 22–23. The single-law propositions have no feature variable.

Significance

Theorem 1 identifies a condition under which a convex training objective preserves the population target of the decision loss. Its identification statement is stronger than merely saying that one selected SPO+ minimizer is SPO-optimal: all SPO+ minimizers agree almost surely with conditional mean cost. The propositions isolate what this depends on. Proposition 6 concerns the surrogate risk, while Proposition 5 connects a prediction's optimal-decision set to the true risk.

The result was proved in the cited preprint and published in Management Science in 2022; this mission asks for a Lean proof of that known result, not a new consistency theorem. A completed development would provide reusable definitions for cost-based decision losses and a checked account of the distributional assumptions needed for uniqueness. The published oracle predicate is already available on the platform; the two losses, risks, and distributional predicates are introduced here.

Difficulty

The SPO loss may jump when a predicted cost admits more than one optimal decision. Its definition takes the maximum realized cost over that whole decision set. Consequently, showing that a prediction selects one mean-optimal decision does not by itself control the SPO loss; Proposition 5's converse requires a singleton set. The surrogate is convex but generally not differentiable, because the support function of $S$ need not be differentiable. Establishing the unique population minimizer also depends on how the cost law covers the space: absolute continuity by itself permits a bounded-support law for which nearby predictions tie. These are substantive issues in moving from the single-cost-law statements to an almost-sure claim about measurable predictors Elmachtoub and Grigas, 2020, §4 and Appendix B.

Formalization scope

The code represents $\mathbb R^d$ by EuclideanSpace ℝ (Fin d) and $c^\top w$ by its standard inner product. Every theorem assumes the paper's nonempty compact convex $S$. Real infima and suprema encode the attained minima and maxima on $S$. An oracle is an explicit parameter satisfying the published SPOBounds.Natarajan.IsOracle predicate; it is not given an extra measurability or tie-breaking assumption. The SPO loss is the paper's unambiguous Definition 2, which differs from the oracle-dependent loss in the published module.

Expected losses are extended nonnegative integrals, so an infinite risk remains infinite. Conditional costs are represented by a Markov kernel $\kappa$, and the joint law by $\nu\otimes\kappa$. Integrability of costs makes the conditional and joint means finite. Central symmetry means equality of the conditional law with its reflection $c\mapsto 2m(x)-c$. Assumption 1.3, “continuous on all of $\mathbb R^d$,” is pinned to absolute continuity with respect to Lebesgue measure and full support, meaning every nonempty open set has positive probability. This full-support condition is needed for Proposition 6(b)'s uniqueness claim: a continuous law confined to a small ball supplies a counterexample to the weaker reading.

The risks range over all measurable predictors, as display (12) requires. A Bochner integral for an arbitrary nonintegrable loss, a restricted hypothesis class, the oracle-dependent SPO loss of Definition 1, or absolute continuity without full support would change or trivialize the target. Contributions to the support-function, measurable-risk, and conditional-law infrastructure are useful beyond this mission; the seven numbered proposition parts provide its immediate formalization targets.

Selected references

• A. N. Elmachtoub and P. Grigas, Smart “Predict, then Optimize”, arXiv:1710.08005v5, 2020; published in Management Science 68(1), 2022. Preprint

Motivation

A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.

The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order $\sqrt{NT\log NT}$ (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most $K$ products be displayed, no policy can have regret smaller than order $\sqrt{NT/K}$ on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.

Timeline. The square-root lower bound for $N$-armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining $O(N^2\log^2T)$ and $O(N\log T)$ bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent $\Omega(\sqrt{NT/K})$ lower bound formalized here; Chen and Wang (2017) later obtained $\Omega(\sqrt{NT})$ when $K<N/4$.

Setting

There are $n$ products. An instance consists of a no-purchase weight $v_0>0$, attraction parameters $v_1,\dots,v_n$ with $0\le v_i\le v_0$, and revenues $r_i\in[0,1]$. At each period $t=1,\dots,T$ the seller offers an assortment $S_t\subseteq\{1,\dots,n\}$ and observes a choice $c_t\in S_t\cup\{0\}$, where $0$ means no purchase. Under the multinomial logit (MNL) model,

$$p_i(S)=\frac{v_i}{v_0+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

and choices are independent across periods given the offered sets. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i/(v_0+\sum_{j\in S}v_j)$.

A policy chooses $S_t$ from the past assortments and choices, possibly at random. It satisfies the $K$-cardinality constraint if $|S_t|\le K$ always. Its regret over $T$ periods is

$$\mathrm{Reg}_\pi(T,v)=\mathbb E_\pi\Big(\sum_{t=1}^{T}R(S^*,v)-R(S_t,v)\Big),$$

where $S^*$ maximizes $R(\cdot,v)$ over assortments of at most $K$ products.

A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.

Formalization targets

Goal: Theorem 2 (p. 14)

There is an absolute constant $C>0$ such that for all $n\ge2$, $1\le K\le n$ and $T\ge n$ there is a finitely supported randomized instance, chosen before the policy, such that every policy $\pi$ respecting the $K$-cardinality constraint satisfies

$$\mathbb E_{v}\big[\mathrm{Reg}_\pi(T,v)\big]\ge C\sqrt{\frac{nT}{K}} .$$

The constant is not fixed; any positive value suffices.

Milestones

The paper proves Theorem 2 in two cases.

1. Lemma E.1 (p. 57): the Bernoulli divergence bound $\mathrm{kl}(\alpha,\alpha+\epsilon)\le 4\epsilon^2/\alpha$ in the direction used by Lemma E.2.
2. Lemma E.2 (p. 57): for a guessing algorithm on $N\ge12$ coins and $t\le N\alpha/(60\epsilon^2)$, at least $N/3$ hiding places $j$ of the biased coin have $\mathcal P_j(a_t=j)\le 1/2$.
3. Lemma 5.1 (p. 15): on the Bernoulli instance $I_{\mathrm{MAB}}$ with $\epsilon=\frac1{100}\sqrt{N\alpha/T}$, every online algorithm has expected regret at least $\epsilon T/6$.
4. Lemma E.4 (p. 60): one period of MNL feedback on the instance $\hat I_{\mathrm{MNL}}$, where $\epsilon=\sqrt{1/(32T)}$, has divergence at most $4\epsilon^2$.
5. Lemma E.5 (p. 61): over $T$ periods the two choice laws of that instance have divergence at most $4T\epsilon^2$.

Items 1–3 serve the case $K<n$, which the paper reduces to a multi-armed bandit through the instance $I_{\mathrm{MNL}}$ of Definition 5.2 ($NK$ products in $N$ groups of $K$, one hidden group with larger attraction). Items 4–5 serve the case $K=n$ through the two-point instance $\hat I_{\mathrm{MNL}}$ of Definition E.1.

Significance

The theorem shows that the $\sqrt{T}$ growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size $K$ is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.

The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude $\alpha$ close to $1$, where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the $K=N$ case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.

Difficulty

The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers $K$ products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over $T$ pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.

A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.

Formalization scope

Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length $T$, laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight $v_0$ is explicit (Definition 5.2 has $v_0=K$). $R(S^*,v)$ is a maximum over the finite, nonempty family $\{S:|S|\le K\}$.

Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then $n,K,T$, then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with $C=0$ allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.

Hypotheses added to the printed statements: $n\ge2$ and $K\ge1$ in Theorem 2 (the claim fails for $n=1$ and $K=0$); $0<\alpha$, $0<\epsilon$, $\alpha+\epsilon\le3/4$ in Lemma E.1; $0<\alpha$, $0<\epsilon$, $2\alpha+\epsilon\le1$ in Lemma E.2; $0<\alpha$, $2\alpha+\epsilon\le1$, $T\ge1$ in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's $\epsilon=\sqrt{1/(32T)}$, with $T\ge1$ and $n\ge2$ so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.

The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in $[0,\infty]$). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound $d(p,q)\le(q-p)^2/(p(2-p-q))$ (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019; preprint arXiv:1706.03880v2. https://arxiv.org/abs/1706.03880 — DOI https://doi.org/10.1287/opre.2018.1832
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
• X. Chen, Y. Wang, A Note on a Tight Lower Bound for MNL-Bandit Assortment Selection Models, arXiv:1709.06109, 2017. https://arxiv.org/abs/1709.06109

Motivation

The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level $s$, order enough to bring it up to the order-up-to level $S$. Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.

Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal $s$ and $S$ and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the $(s,S)$ grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).

Setting

One-period demands $D$ are i.i.d. and integer valued, with $p_j=\Pr\{D=j\}$, $j\ge0$, and $p_0<1$. An order costs $K>0$. $G(y)$ is the one-period expected cost when a period starts at inventory position $y\in\mathbb Z$. The paper assumes only:

• $-G$ is unimodal: for some integer $m$, $G$ is nonincreasing on $y\le m$ and nondecreasing on $y\ge m$;
• $\lim_{|y|\to\infty}G(y)>\min_yG(y)+K$.

Write $y_1^*$ and $y_2^*$ for the smallest and largest minimizers of $G$. The renewal density $m$ and renewal function $M$ are

$$m(0)=(1-p_0)^{-1},\quad m(j)=\sum_{l=0}^{j}p_l\,m(j-l)\ (j\ge1),\qquad M(0)=0,\quad M(j)=M(j-1)+m(j-1).$$

For integers $s<S$, the long-run average cost of the (s, S) policy is

$$c(s,S)=\frac{K+\sum_{j=0}^{S-s-1}m(j)\,G(S-j)}{M(S-s)}.$$

A pair $(s,S)$ is an optimal policy if $c(s,S)\le c(s',S')$ for all integers $s'<S'$. The optimal cost $c^*$ is the value of any optimal policy. For fixed $S$, $s$ is an optimal reorder level if $c(s,S)\le c(s',S)$ for all $s'<S$.

The algorithm (§3, p. 659) starts at any minimizer $y^*$ of $G$.

• Step 0. Decrease $s$ from $y^*$ until $c(s,y^*)\le G(s)$. Set $S^0:=y^*$, $c^0:=c(s,S^0)$ and $S:=y^*+1$.
• Step 1. While $G(S)\le c^0$: if $c(s,S)<c^0$, set $S^0:=S$, increase $s$ while $c(s,S^0)\le G(s+1)$, and set $c^0:=c(s,S^0)$. In either case, $S:=S+1$.

Formalization targets

Goal: Theorem 1(a)

For every demand law with $p_0<1$, every $K>0$, every $G$ satisfying the two assumptions, and every minimizer $y^*$ of $G$, the algorithm terminates. On termination, with final values $s,S^0,c^0$,

$$c(s,S^0)\le c(s',S')\ \text{ for all integers } s'<S',\qquad c^0=c(s,S^0)=c^*.$$

Milestones

The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:

1. the weighted-average identity (6), $c(s-1,S)=\alpha_nc(s,S)+(1-\alpha_n)G(s)$ with $\alpha_n=M(n)/M(n+1)$ and $n=S-s$, and Lemma 0 on the comparisons it implies;
2. Lemma 1(a): a reorder level $s^0<y_1^*$ with $G(s^0)\ge c(s^0,S)\ge G(s^0+1)$ (condition (7)) is optimal for $S$;
3. Corollary 1, the stopping rule of Step 0;
4. Lemma 2(a)–(c), the bounds $y_2^*\le S^*$ and $S^*\le\bar S^*=\max\{y\ge y_2^*:G(y)\le c^*\}$, which give the stopping rule of Step 1;
5. Lemma 3(a), the single-comparison test for improvement, and Corollary 2(b) with Lemma 3(b), which justify the inner loop.

Significance

The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any $G$ with $-G$ unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.

Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).

Difficulty

Optimality is claimed over all pairs $s'<S'$, an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed $S$, the skipped reorder levels are handled by the unimodality of $c(\cdot,S)$ (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of $c$ in $(s,S)$ is not available. The paper uses no structure of $c$ beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.

Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at $-\infty$ may be finite, so $\min_{s<S}c(s,S)$ need not be attained for every $S$. Lattice demands, for which $m$ vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.

Formalization scope

• Levels $s,S,y$ are integers. Demand values are natural numbers, and the demand law is the published VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis $p_0<1$. All costs are real.
• The cost is the ratio above. Equation (1) on p. 655 is misprinted as $M(S-s)K+\sum\cdots$, and the ratio is the form fixed by (3) and (5). The Lean value $c(s,S)$ for $s\ge S$ is a junk $0$, so every quantifier over reorder levels carries $s<S$.
• $m$ is defined by the solved recursion $m(j)=(1-p_0)^{-1}\sum_{l=1}^{j}p_l\,m(j-l)$ (p. 660), and $M(j)=\sum_{i<j}m(i)$.
• The growth assumption is encoded as: $G$ has a minimizer $y_0$ and $G(y)>G(y_0)+K$ for all but finitely many $y$. Under unimodality this is equivalent to the page's limit condition. It is not strengthened to $G\to+\infty$.
• Optimality is among (s, S) policies. That an (s, S) policy is optimal among all policies is Veinott (1966) and is neither stated nor used. $c^*$, $c^*(S)$, $y_i^*$, $\bar S^*$, $\bar S_c$ and $s'$ are never real infima: they are the cost of a given optimal pair, $\exists$-statements, or binders characterised as least or greatest elements.
• The algorithm is a step function on the state $(s,S,S^0,c^0,\text{phase})$ that keeps the paper's order of tests and its weak and strict inequalities. The run with $n$ steps returns an output only if the algorithm has terminated.
• Ruled out as trivializing: comparing only with the pairs the algorithm visits or with a bounded box; assuming termination, or a budget that returns the current state; assuming $G\to+\infty$; leaving $c(s,S)$ unguarded for $s\ge S$.
• Repaired statements. Lemma 3(a) is stated with condition (7) at $S^0$ as an extra hypothesis. With $s^0$ merely optimal it fails when $m$ has a zero: for $p=(1/5,0,1/5,3/5)$, $m(1)=0$ and adjacent reorder levels tie. The algorithm always has (7). Lemma 1(b), "an optimal reorder level satisfying (7) exists for every $S$", is false when $\lim_{y\to-\infty}G(y)$ is finite. An example is $D\equiv2$, $K=1$, $G(0)=5$, $G(y)=10-0.1\cdot2^{-|y|}$ ($y\neq0$), $S=1$, where no optimal reorder level exists. It is not posed here, and the goal does not depend on it.
• Not formalized: Theorem 1(b)–(c), the operation counts, which depend on a bookkeeping model described in words; Corollary 3, which the paper notes is not needed for the algorithm; and the variant for a general starting level $S_0$.
• Welcome contributions: general facts about the discrete renewal density ($m\ge0$, $M>0$), the identity (6), and lemmas on $c(\cdot,S)$ that are reusable for related (s, S) and (r, Q) work.

Selected references

• Y.-S. Zheng and A. Federgruen, Finding Optimal (s, S) Policies Is About As Simple As Evaluating a Single Policy, Operations Research 39(4):654–665, 1991. https://doi.org/10.1287/opre.39.4.654
• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5):525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM J. Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• A. Federgruen and P. Zipkin, An Efficient Algorithm for Computing Optimal (s, S) Policies, Operations Research 32(6):1268–1285, 1984. https://doi.org/10.1287/opre.32.6.1268
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Why arrival averages and time averages agree

Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.

Before 1982 the property had been proved under strong extra structure:

• Strauch (1970) proved an instantaneous version, at a fixed time point, which does not by itself give limit theorems.
• Wolff (1970) proved a limit theorem for a stationary observed process, using particular properties of its interaction with the Poisson stream.
• Stidham (1972) proved a limit theorem for regenerative processes, under restrictions on how regeneration points relate to the arrivals.
• Wolff (1982), the source of this mission, proved the limit theorem with no stationarity, regeneration or ergodicity at all. The only link assumed between system and arrivals is that the system does not anticipate future arrivals. The proof uses Watanabe's (1964) martingale characterization of the Poisson process.
• Melamed and Whitt (1990) recast the result as one instance of a general "arrivals see time averages" (ASTA) principle for arbitrary point processes.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. On it live a process $N=\{N(t),t\ge0\}$, the state of a system, with values in an arbitrary measurable space, and a Poisson process $A=\{A(t),t\ge0\}$ at rate $\lambda>0$, counting customer arrivals in $(0,t]$. The interaction between $A$ and $N$ is unspecified: arrivals may change the state.

Fix a set $B$ of states with $\{N(t)\in B\}\in\mathcal F$ for every $t\ge0$, and define

$$U(t)=\mathbf 1\{N(t)\in B\},\qquad V(t)=t^{-1}\int_0^tU(s)\,ds,\qquad Y(t)=\int_0^tU(s)\,dA(s),\qquad Z(t)=\frac{Y(t)}{A(t)}.$$

$V(t)$ is the fraction of time in $[0,t]$ that $N$ is in $B$. $Y(t)$ is the number of arrivals up to $t$ who find $N$ in $B$, and $Z(t)$ is the fraction of arrivals who do.

The paths of $U$ are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. $U$ is assumed jointly measurable in $(\omega,t)\in\Omega\times[0,\infty)$. The single structural assumption is the Lack of Anticipation Assumption (LAA):

for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ and $\{U(s),0\le s\le t\}$ are independent.

The paper's proof of (6) uses this independence for every event of $\mathcal F_t$, the σ-field generated by $\{A(s),U(s);0\le s\le t\}$. The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to $\mathcal F_t$: for each $t\ge0$, $\{A(t+u)-A(t),u\ge0\}$ is independent of $\mathcal F_t$. This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of $A$ and from the past of $U$ is not independence from their joint past.

Formalization targets

Goal: Theorem 1 (p. 225)

Under lack of anticipation (with respect to $\mathcal F_t$, see above), for every random variable $V(\infty)$,

$$V(t)\to V(\infty)\ \text{w.p. 1}\quad\Longleftrightarrow\quad Z(t)\to V(\infty)\ \text{w.p. 1},\qquad t\to\infty.$$

The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.

Milestones

The proof in §2 passes through the following statements, which form the milestone list:

1. (2), (3): $E\{Y(t)\}=\lambda tE\{V(t)\}=\lambda E\{\int_0^tU(s)\,ds\}$.
2. (6): $E\{Y(t+h)-Y(t)\mid\mathcal F_t\}=\lambda E\{\int_t^{t+h}U(s)\,ds\mid\mathcal F_t\}$.
3. Lemma 1: $R(t)=Y(t)-\lambda tV(t)$ is a martingale.
4. (7): the second-moment bound $E\{R^2(t)\}\le\lambda t+2\lambda^2t^2$.
5. (10): the grid strong law $R(nh)/n\to0$ w.p. 1.
6. (11): the pathwise interpolation bound between grid points.
7. Lemma 2: $R(t)/t\to0$ w.p. 1.
8. The strong law $A(t)/t\to\lambda$ for the Poisson process.

Companion: Theorem 2 (p. 228)

For a Poisson process with bounded, integrable rate $\lambda(t)$ and $\Lambda(t)/t\to\bar\lambda\in(0,\infty)$, where $\Lambda(t)=\int_0^t\lambda(s)\,ds$, the same equivalence holds with $V(t)$ replaced by the rate-weighted average $\bar V(t)=\Lambda(t)^{-1}\int_0^tU(s)\lambda(s)\,ds$. Display (12), $E\{Y(t)\}=\int_0^tE\{U(s)\}\lambda(s)\,ds$, is its analogue of (3).

Significance

Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).

The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:

• the strong law for the Poisson process;
• a strong law for square-integrable martingale differences;
• Stieltjes integration against a counting path.

Difficulty

The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of $A$ are independent of the past of $U$. The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.

On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, $U(t)=\mathbf 1\{A \text{ jumps at } t\}$ satisfies LAA with $V\equiv0$ but $Z\equiv1$. The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.

Formalization scope

• Time and paths. Time is $\mathbb R$, and every hypothesis concerns $t\ge0$ only. Processes are maps $\mathbb R\to\Omega\to(\cdot)$. A Poisson process with intensity function $\lambda(\cdot)$ is a counting process $A:\mathbb R\to\Omega\to\mathbb N$ with $A(0)=0$, every path non-decreasing and right-continuous, Poisson-distributed increments with mean $\int_s^t\lambda$, and independent increments over any finite increasing sequence of times. The constant-rate case is Theorem 1's setting.
• The averages. $Y(t)$ is encoded as $\sum_{k=1}^{A(t)}U(T_k)$ over the arrival epochs $T_k=\inf\{s\ge0:A(s)\ge k\}$, which is the Lebesgue–Stieltjes integral $\int_{(0,t]}U\,dA$ with multiplicities. $Z(t)=0$ when $A(t)=0$, and $V(0)=0$; limits do not see these values.
• The standing hypotheses. These are carried as binders of the goal: measurability of $\{N(t)\in B\}$ for $t\ge0$, path regularity w.p. 1 (left continuity at $t>0$, right limits at $t\ge0$), joint measurability on $\Omega\times[0,\infty)$, and lack of anticipation as independence of the σ-field of future increments of $A$ from $\mathcal F_t$. The milestones (2), (3), (7) and (11) need less: (2) and (3) are stated under the printed LAA, and (7) and (11) under no independence assumption at all.
• The limit and the expectations. $V(\infty)$ is an arbitrary function $\Omega\to\mathbb R$, shared by both sides of the equivalence. Expectations in the milestones come with integrability conclusions, or are lower integrals in $[0,\infty]$, so that no identity holds through Lean's junk value $0$ for non-integrable functions.
• Ruled out. A formalization in which $V(\infty)$ is quantified separately on each side, which loses "to the same limit". A goal that assumes Lemma 2, (3) or the strong law $A(t)/t\to\lambda$ as a hypothesis. A definition of $Y$ that counts distinct jump times and not arrivals.

Welcome contributions:

• a reusable Poisson-process library: the strong law, square moments, independence of increments from a past σ-field;
• a martingale strong law of Feller's type;
• Stieltjes sums against counting paths.

All of these are useful well beyond this mission.

Selected references

• R. W. Wolff, Poisson Arrivals See Time Averages, Operations Research 30(2):223–231, 1982. https://doi.org/10.1287/opre.30.2.223
• S. Watanabe, On discontinuous additive functionals and Lévy measures of a Markov process, Japanese Journal of Mathematics 34:53–70, 1964. https://doi.org/10.4099/jjm1924.34.0_53
• B. Melamed and W. Whitt, On arrivals that see time averages, Operations Research 38(1):156–172, 1990. https://doi.org/10.1287/opre.38.1.156
• P. Brémaud and J. Jacod, Processus ponctuels et martingales: résultats récents sur la modélisation et le filtrage, Advances in Applied Probability 9(2):362–416, 1977. https://doi.org/10.2307/1426091
• S. Stidham, Regenerative processes in the theory of queues, with applications to the alternating-priority queue, Advances in Applied Probability 4(3):542–577, 1972.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.

Motivation

Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.

The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.

Setting

Fix a positive integer $n$ and write $x(t)\in\mathbb R^n$ for the vector after round $t\ge0$. Let $F:\mathbb R^n\to\mathbb R^n$ be the map whose fixed point the iteration seeks. For component $i$, the step size $\alpha_i(t)$ lies in $[0,1]$, the noise is $w_i(t)$, and $\tau^i_j(t)\le t$ is the time from which component $j$ was read. Thus $x^i(t)$ has coordinates $x_j(\tau^i_j(t))$. With $\alpha_i(t)=0$ when component $i$ is idle, all rounds obey the single update equation

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr).$$

All quantities live on a probability space with law $\mathsf P$. The increasing filtration $\mathcal F(t)$ represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp $\tau^i_j(t)$ tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.

For a vector $v$ with strictly positive coordinates, the weighted maximum norm is $\|z\|_v=\max_i |z_i|/v_i$. Assumption 5 provides $x^*\in\mathbb R^n$ and $\beta\in[0,1)$ such that $\|F(x)-x^*\|_v\le\beta\|x-x^*\|_v$ for every $x$. Assumption 6, used in the boundedness milestone, requires the related growth bound $\|F(x)\|_v\le\beta\|x\|_v+D$ for some real $D$. The weighted norm permits different component scales.

Formalization targets

Boundedness under a weighted growth bound

Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts

$$\mathsf P\!\left(\exists M\in\mathbb R\;\forall t,i,\ |x_i(t)|\le M\right)=1.$$

The bound $M$ may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.

Almost-sure convergence under a weighted contraction

The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:

$$\mathsf P\!\left(\lim_{t\to\infty}x(t)=x^*\right)=1.$$

This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.

Significance

The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).

The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.

Difficulty

A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.

Formalization scope

Vectors are functions Fin n → ℝ, with $n>0$; the source labels coordinates $1,\ldots,n$, while Fin n starts at zero. Function order is componentwise. The model sets $\alpha_i(t)=0$ on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in $[0,1]$, and all delays are at most the current time, on every sample path.

The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of $x(t)$ and its running maximum as $\mathcal F(t)$-measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.

The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of $v$. Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.

Selected references

• John N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. DOI: 10.1023/A:1022689125041.

Motivation

Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating $x \leftarrow x + \alpha\,(F(x) - x + w)$ with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).

Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping $F$: a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.

Setting

A mapping $F:\mathbb R^n\to\mathbb R^n$ with components $F_1,\dots,F_n$ is given, and the goal is to solve $F(x)=x$. Time is discrete, $t=0,1,2,\dots$. The iterate $x(t)\in\mathbb R^n$ evolves by

$$x_i(t+1)=x_i(t)+\alpha_i(t)\bigl(F_i(x^i(t))-x_i(t)+w_i(t)\bigr),\qquad x^i(t)=\bigl(x_1(\tau^i_1(t)),\dots,x_n(\tau^i_n(t))\bigr),$$

where $\alpha_i(t)\in[0,1]$ is a stepsize ($\alpha_i(t)=0$ when component $i$ is not updated), $w_i(t)$ is noise, and $0\le\tau^i_j(t)\le t$ are delays: the update of component $i$ may read component $j$ as it was at an earlier time. All quantities are random variables on a probability space $(\Omega,\mathcal F,P)$ with an increasing sequence of σ-fields $\{\mathcal F(t)\}$, the history up to the choice of the stepsizes at time $t$.

Vector inequalities are componentwise and $e$ is the vector of ones. The paper's assumptions are:

• Assumption 1: every delay index $\tau^i_j(t)$ tends to infinity, with probability 1.
• Assumption 2: $x(0)$, $\alpha_i(t)$, $\tau^i_j(t)$ are $\mathcal F(t)$-measurable and $w_i(t)$ is $\mathcal F(t+1)$-measurable; $E[w_i(t)\mid\mathcal F(t)]=0$; and $E[w_i^2(t)\mid\mathcal F(t)]\le A+B\max_j\max_{\tau\le t}|x_j(\tau)|^2$ for deterministic constants $A,B$.
• Assumption 3: $\sum_t\alpha_i(t)=\infty$ and $\sum_t\alpha_i^2(t)\le C$ with probability 1, for a deterministic $C$.
• Assumption 4: $F$ is monotone ($x\le y\Rightarrow F(x)\le F(y)$), continuous, has a unique fixed point $x^*$, and $F(x)-re\le F(x-re)\le F(x+re)\le F(x)+re$ for all $x$ and all $r>0$.

In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.

Formalization targets

Goal: Theorem 2 (p. 189)

Under Assumptions 1–4, if $x(t)$ is bounded with probability 1, then

$$\lim_{t\to\infty}x(t)=x^*\qquad\text{with probability 1.}$$

Boundedness is a hypothesis, not a conclusion: for monotone $F$ it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.

Milestones

1. Lemma 1 (p. 190): for a scalar recursion $W(t+1)=(1-\alpha(t))W(t)+\alpha(t)w(t)$ with martingale-difference noise whose conditional variance is bounded by an a.s. bounded $B(t)$, and stepsizes with $\sum\alpha=\infty$, $\sum\alpha^2\le C$, $W(t)\to0$ with probability 1.
2. Lemma 4 (p. 193): the sequences $U^{k+1}=(U^k+F(U^k))/2$, $U^0=x^*+re$, and $L^{k+1}=(L^k+F(L^k))/2$, $L^0=x^*-re$, satisfy $F(U^k)\le U^{k+1}\le U^k$ and $F(L^k)\ge L^{k+1}\ge L^k$.
3. Lemma 5 (p. 193): $U^k\to x^*$ and $L^k\to x^*$.
4. Lemma 6 (p. 194): on a sample path where $L^k\le x(t)\le U^k$ from time $t_k$ on and all delays exceed $t_k$ from time $t'_k$ on, $x_i(t)\le X_i(t)+W_i(t;t'_k)$, where $X_i$ relaxes from $U^k_i$ towards $F_i(U^k)$ and $W_i(t;t'_k)$ accumulates the noise from $t'_k$.
5. Lemma 7 (p. 195): under the choices of $\delta_k$ and $t''_k$ made on pp. 194–195, $x_i(t)\le U^{k+1}_i$ for all $t\ge t''_k$.

Significance

Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.

The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.

Difficulty

The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes $U^k,L^k$ to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.

Formalization scope

• Components are Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. $re$ is r • 1.
• The update is stated in the paper's unified form for every $t$, with $\alpha_i(t)=0$ off the update times; the update sets $T^i$ are not represented. The paper sets $\tau^i_j(t)=t$ off $T^i$; the formalization leaves $\tau^i_j(t)$ free there, which is more general. $\alpha_i(t)\in[0,1]$ and $\tau^i_j(t)\le t$ hold on every sample path.
• Conditional expectations are generalized, written with set integrals (CondMeanZero, CondSqLe): $\int_S w\,dP=0$ for every $\mathcal F(t)$-set $S$ on which $w$ is integrable, and $\int_S w^2\,dP\le\int_S g^+\,dP$ in $[0,\infty]$. Mathlib's condExp is not used: it is $0$ for non-integrable functions and would make the noise assumptions vacuous.
• Series conditions use partial sums (divergence to $+\infty$; every partial sum at most $C$), never tsum, which is $0$ for non-summable sequences. The constants $A,B,C$ are chosen before the almost-sure quantifier; the bound on $x(t)$ is chosen after it.
• The paper treats $x(t)$ as determined by $\mathcal F(t)$ and uses this implicitly; Theorem 2 assumes it explicitly (Adapted).
• Lemma 1 leaves $W(0)$ unconstrained, as on the page. Lemmas 4 and 5 hold for every $r>0$. Lemmas 6 and 7 are pathwise: they fix one sample path and take the induction's objects ($k$, $t_k$, $t'_k$, $t''_k$, $X$, $\delta_k$) as given with exactly the properties the paper has established for them; they are not existential statements about these times.
• A trivializing formalization (junk conditional expectations, tsum for the series, a deterministic bound on $x(t)$, or a second unrelated $x^*$) is ruled out by the choices above.

Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version $W(t;t_0)$), and lemmas on monotone maps satisfying (7).

Selected references

• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994) 185–202. https://doi.org/10.1023/A:1022689125041
• C. J. C. H. Watkins and P. Dayan, Q-learning, Machine Learning 8 (1992) 279–292. https://doi.org/10.1007/BF00992698
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994) 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://hdl.handle.net/1721.1/3719
• B. T. Poljak and Ya. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automation and Remote Control 34 (1973) 377–397.
• H. Robbins and S. Monro, A Stochastic Approximation Method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586