Operations Research

Motivation

Financial firms owe each other money. When some firms cannot meet their obligations, the payments that actually clear in the network are a fixed point: what a firm can pay depends on what it receives, which depends on what others can pay. Eisenberg and Noe (Management Science, 2001) introduced this clearing model under a fixed pro-rata payment rule. Later work asked what happens when firms choose how to pay their creditors, which turns the clearing problem into a game.

Bertschinger, Hoefer and Schmand (arXiv:1908.01714v3; Mathematics of Operations Research, 2025) study this game in an abstract form, the flow allocation game. Each node of a directed network receives a fixed external supply plus whatever flows in, and decides how to split its total supply among its outgoing edges, subject to edge capacities. Each node wants to maximize its own total outflow (its payments, which in the financial reading is what keeps it solvent). The paper's first main result is that, when strategies rank single units of flow, there is always a strong equilibrium, stable against every coalition, which is at the same time socially optimal for the total flow.

Timeline:

• 2001: Eisenberg and Noe, clearing payments under pro-rata rules, existence of a greatest clearing vector.
• 2018: Csóka and Herings (Management Science): decentralized clearing with integral monotone allocation rules; the feasible flows form a complete lattice (restated for all monotone profiles as Theorem 2 of the present paper).
• 2019–2025: Bertschinger, Hoefer and Schmand, strategic allocation; existence of optimal strong equilibria for unit-ranking strategies (Theorem 9), strong price of anarchy bounded by the min-max cycle length (Theorem 16), hardness results for other welfare functions and for edge-ranking strategies.

Setting

A flow allocation game $\Gamma = (G, (b_v)_{v\in V}, (c_e)_{e\in E})$ consists of a finite directed multigraph $G = (V, E)$, a fixed supply $b_v \in \mathbb N_0$ at each node and a capacity $c_e \in \mathbb N_0$ on each edge. $E^+(v)$ and $E^-(v)$ are the outgoing and incoming edges of $v$, and $c^+_v = \sum_{e\in E^+(v)} c_e$.

Every node is a player. A strategy profile $\mathbf a = (a_e)_{e\in E}$ assigns to each edge an allocation function $a_e : \mathbb N_0 \to \mathbb N_0$: when the tail of $e$ has total supply $y$, it forwards $a_e(y)$ units on $e$. The profile is unit-ranking if for all $y$, $e$, $v$: $a_e(y) \le c_e$ (1); $\sum_{e\in E^+(v)} a_e(y) \le y$ (2); $\sum_{e\in E^+(v)} a_e(y) = \min\{c^+_v, y\}$ (no fraud, (3)); and each $a_e$ is non-decreasing (5). Equivalently, every node ranks the single units of its outgoing capacity.

A flow $\mathbf f \in \mathbb N_0^E$ gives node $v$ the total supply $f_v = b_v + \sum_{e\in E^-(v)} f_e$, and is feasible for $\mathbf a$ if $f_{(v,w)} = a_{(v,w)}(f_v)$ on every edge (4). The clearing state $\hat{\mathbf f}$ of $\mathbf a$ is the coordinatewise supremum of the feasible flows. Player $v$'s utility is $u_v(\mathbf a) = \sum_{e\in E^+(v)} \hat f_e$, and the total flow is $\mathrm{Flow}(\mathbf a) = \sum_{e\in E} \hat f_e$.

A unit-ranking profile $\mathbf a$ is a strong equilibrium if no non-empty coalition $C \subseteq V$ has a joint deviation $\mathbf a'_C$ such that $(\mathbf a'_C, \mathbf a_{-C})$ is unit-ranking and $u_v(\mathbf a'_C, \mathbf a_{-C}) > u_v(\mathbf a)$ for all $v \in C$.

The circulation network $G'$ adds a node $s$, an uncapacitated edge $(v, s)$ and an edge $(s, v)$ of capacity $b_v$ for every $v$. An optimal circulation $f^*$ maximizes the total flow over all edges of $G'$.

Formalization targets

Goal: Theorem 9 (first sentence)

$$\exists\, \mathbf a:\quad \mathbf a \text{ is a strong equilibrium} \ \text{ and } \ \mathrm{Flow}(\mathbf a') \le \mathrm{Flow}(\mathbf a) \text{ for every unit-ranking } \mathbf a'.$$

Milestones (in the order of the proof)

1. Theorem 2 (p. 12, integral version p. 13): for a monotone profile the feasible flows form a non-empty complete lattice; the clearing state is its greatest element.
2. Proposition 5 (p. 17): a feasible flow, with the non-forwarded flow $\max\{0, f_v - c^+_v\}$ sent to $s$, is a circulation of $G'$, and $\sum_v \max\{0, f_v - c^+_v\} = \sum_v b_v$.
3. Proof of Theorem 9, p. 23, first display: an optimal circulation saturates every $(s, v)$ and

$$\sum_{e\in E'} f^*_e = 2\sum_v b_v + \mathrm{Flow}(f^*) \ge 2\sum_v b_v + \mathrm{Flow}(\mathbf a).$$

4. Proof of Theorem 9, p. 23: with thresholds $\tau_e = f^*_e$ and arbitrary rankings, the threshold-ranking profile $\mathbf a^*$ is unit-ranking and its clearing state is $f^*$.
5. Proof of Theorem 9, pp. 23–24: a profitable coalitional deviation from a unit-ranking profile produces a cycle of $G$ on which the new clearing state carries strictly more flow.

Companion: Corollary 12

For every flow-monotone $Q$ (if $\hat{\mathbf f} > \hat{\mathbf f}'$ then $Q(\mathbf a) \ge Q(\mathbf a')$) there is a strong equilibrium maximizing $Q$ over all unit-ranking profiles.

Significance

Strong equilibria rarely exist in network games, and when they do they are usually not efficient. Theorem 9 gives both at once: every unit-ranking game has a strong equilibrium, and one of them maximizes the total flow, so the price of stability for $\mathrm{Flow}$ is $1$. Corollary 12 extends this to every flow-monotone welfare function, including egalitarian welfare, Nash social welfare and the number of solvent firms. In the financial reading, a coalition of firms cannot jointly reorder its payments to make every member better off, and the stable payment pattern can be chosen to clear the largest possible volume of debt.

The results are proved in the paper and, to our knowledge, have no machine-checked proof. Formalizing them yields a reusable Lean development of clearing states (the Knaster–Tarski structure of feasible flows), the circulation representation of feasible flows, and integral maximum circulations with a cycle-augmentation argument. The second mission of this series (strong price of anarchy, Theorem 16) builds on the same model.

Difficulty

The obvious argument fails at the deviation step. After a coalition deviates, the clearing state of the new profile is an implicit object: the greatest fixed point of a map that mixes the deviators' new strategies with everyone else's old ones. Nothing ties it pointwise to the optimal circulation, and comparing utilities alone gives no contradiction, because a deviator's gain can be paid for by flow that appears elsewhere in the network. The increase of flow has to be traced through deviators and non-deviators alike, and the two kinds of node obey different constraints.

A second difficulty is that the threshold profile built from an optimal circulation $f^*$ has clearing state exactly $f^*$. The clearing state is a supremum over all feasible flows, so it is not enough that $f^*$ is feasible. The claim depends on optimality: for a circulation that is not optimal it is false, as a two-node cycle carrying one unit on edges of capacity two already shows.

Formalization scope

All data are natural numbers: supplies, capacities, strategies $a_e : \mathbb N \to \mathbb N$ and flows, as the paper prescribes for unit-ranking games (p. 13). The graph is a finite type of edges with tail and head maps, so multi-edges and self-loops are allowed. A profile is one function on edges. The clearing state is the coordinatewise sSup in $\mathbb N$; the definition does not assume that the supremum is a feasible flow, which is milestone 1. Optimal circulations are optimal among integral circulations, which the paper justifies by integrality of capacities (p. 23). Natural-number subtraction is used only where it is the page's $\max\{0,\cdot\}$.

Coalitions are non-empty. With $C = \emptyset$ the condition "every member strictly gains" holds vacuously and no profile would be a strong equilibrium; the paper reads it the same way (Proposition 4, Proposition 17). Deviations must again be unit-ranking profiles; the broader deviations of Remark 10 are not formalized. The maximization in the goal ranges over all unit-ranking profiles, not over threshold-ranking ones. A goal maximizing only over threshold profiles, or one that drops the optimality conjunct, is a strictly weaker theorem and is ruled out.

Out of scope: the second sentence of Theorem 9 (polynomial-time computation and polynomial-space representation) and the polynomial-space sentence of Corollary 12. Both need a model of computation. The threshold representation behind them is milestone 4.

A complete development needs: Knaster–Tarski on a finite product of intervals (Mathlib's OrderHom fixed-point lattice), flow conservation bookkeeping on finite multigraphs, existence of integral optimal circulations, and extraction of a cycle from an infinite backward walk in a finite graph. The last two are reusable beyond this mission. Proofs of any milestone, and sorry-free lemmas about clearing states, are welcome.

Selected references

• N. Bertschinger, M. Hoefer, D. Schmand, Flow Allocation Games, Mathematics of Operations Research, 2025. Preprint arXiv:1908.01714v3, 2023. https://arxiv.org/abs/1908.01714v3
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• P. Csóka, P. J.-J. Herings, Decentralized Clearing in Financial Networks, Management Science 64(10), 4681–4699, 2018. https://doi.org/10.1287/mnsc.2017.2847
• A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2), 285–309, 1955. https://doi.org/10.2140/pjm.1955.5.285

Why a fluid limit for matching markets

Two-sided platforms (ride hailing, delivery, freelancing, logistics) collect demand and supply requests over a matching cycle and then clear them with an optimization problem. When such a platform runs an experiment, treated and control units compete for the same supply, so the outcome of one unit depends on the treatment of others. Interference bias of this kind is the subject of Bright, Delarue and Lobel, Reducing Marketplace Interference Bias Via Shadow Prices (arXiv:2205.02274v4; Management Science, 2025). Their analysis of estimators, including the shadow-price estimator built from linear-programming duals, is carried out in a deterministic fluid limit. Theorem 1 of the paper justifies that step: as the market becomes dense, the expected matching value per unit of density converges to the optimal value of a deterministic linear program with the arrival rates as inputs.

The same kind of statement, the expected value of a random linear program converging to the value of the program at the mean data, is also used in network revenue management and in stochastic matching, where fluid linear programs serve as benchmarks.

Setting

Network. There are $n_d$ demand types and $n_s$ supply types. A directed network has one demand node $u^d_i$ per demand type (a sink), one supply node $u^s_j$ per supply type (a source) and a finite set $\mathcal U_*$ of intermediate nodes. Every arc $(u,w)$ carries a value $v_{u,w}\in\mathbb R$ and a capacity $k_{u,w}\ge 0$.

Matching program. For a density $\tau$, demand vector $d$ and supply vector $s$, $\Phi_\tau(d,s)$ is the maximum of $\sum_{(u,w)} v_{u,w}x_{u,w}$ over flows $x$ with inflow at most $d_i$ at $u^d_i$, outflow at most $s_j$ at $u^s_j$, flow balance at every intermediate node and $0\le x_{u,w}\le\tau k_{u,w}$ (display (2), p. 7). Write $\Phi:=\Phi_1$. Without intermediate nodes this is a capacitated bipartite transportation problem.

Random counts. Demand units of type $i$ arrive at rate $\lambda_i\ge 0$ and supply units of type $j$ at rate $\pi_j\ge 0$. At density $\tau$ the numbers of units collected in one cycle are independent Poisson counts

$$D^{\tau,\lambda}_i\sim\mathrm{Poisson}(\lambda_i\tau),\qquad S^\tau_j\sim\mathrm{Poisson}(\pi_j\tau).$$

Treatment effect. If a treatment changes the demand rates from $\lambda$ to $\lambda+\beta$ (with $\lambda+\beta\ge 0$), the global treatment effect at density $\tau$ is $\Delta^\tau=\frac1\tau\mathbb E[\Phi_\tau(D^{\tau,\lambda+\beta},S^\tau)-\Phi_\tau(D^{\tau,\lambda},S^\tau)]$ (Definition 1, p. 8).

Formalization targets

Goal: Theorem 1, display (7), p. 12

$$\lim_{\tau\to\infty}\mathbb E\Big[\frac1\tau\,\Phi_\tau\big(D^{\tau,\lambda},S^\tau\big)\Big]=\Phi(\lambda,\pi),$$

for every network, every $\lambda\ge 0$ and every $\pi\ge 0$, along integer densities $\tau$. No rate of convergence and no constant is fixed.

Milestones

1. Lemma 1 (p. 37), scaling. For integer $d,s\ge 0$ and $\tau>0$, $\frac1\tau\Phi_\tau(d,s)=\Phi(\frac1\tau d,\frac1\tau s)$, and $x$ is optimal on the right if and only if $\tau x$ is optimal on the left.
2. Poisson tail bound (proof of Lemma 2, p. 38). For $V\sim\mathrm{Poisson}(\lambda_0)$, $\mathbb P(V\ge t)\le e^{-t}$ for every $t\ge 7\lambda_0$ (Janson, Łuczak and Ruciński 2000, Corollary 2.4).
3. Lemma 2 (p. 38). If $X_n\sim\mathrm{Poisson}(\lambda n)$ for $n\ge 1$, then $Z=\sup_{n\ge1}X_n/n$ has finite mean, whatever the joint law of the $X_n$.

Companion: Corollary 1, display (8), p. 13

$$\lim_{\tau\to\infty}\Delta^\tau=\Phi(\lambda+\beta,\pi)-\Phi(\lambda,\pi).$$

Significance

Theorem 1 is the bridge between the paper's stochastic model and its deterministic analysis. Corollary 1 follows from it and identifies the estimand $\Delta=\Phi(\lambda+\beta,\pi)-\Phi(\lambda,\pi)$. Every fluid-limit result of the paper is stated about this deterministic quantity: that the RCT estimator overestimates the treatment effect (Theorem 2), and that in a symmetric experiment the shadow-price estimator is no more biased than the RCT estimator (Theorem 4). Without Theorem 1 those results describe a linear program, not the experiment.

The result is proved in the paper (Appendix C.1, pp. 37–39). As far as a search of the Prove2Me catalogue shows, it has not been formalized: the catalogue has fluid limits of queueing networks and several Poisson concentration bounds, but no law of large numbers for the value of a random network-flow program. A formal development would provide a reusable definition of the capacitated network-flow program with supply and demand bounds, its scaling identity, and an integrability tool for suprema of scaled Poisson counts. The two other missions of this series, on the shadow-price estimator in the fluid limit and in finite samples, use the same network program.

Difficulty

The obvious argument is: $\frac1\tau D^\tau\to\lambda$ and $\frac1\tau S^\tau\to\pi$, $\Phi$ is continuous, so the expectations converge. Each step needs care.

• The counts at different densities are defined only through their laws. A pathwise limit needs a coupling of the counts across $\tau$, which is not part of the statement.
• Continuity of $\Phi$ in its right-hand side, including at data where some $\lambda_i$ or $\pi_j$ is zero, is a statement about the value function of a parametric linear program. Mathlib has no theory of LP value functions.
• Passing the limit inside the expectation needs a dominating function. The paper builds one from the supremum of scaled Poisson counts (Lemma 2), whose integrability rests on the Poisson tail bound. That bound is not in Mathlib either.

Formalization scope

Representation.

• Demand types are Fin nd and supply types Fin ns; Lean index $i$ is the paper's type $i+1$.
• A network is a structure with arc type E and intermediate-node type I. Each arc's tail is a supply or intermediate node and its head is a demand or intermediate node, which builds in the source/sink structure. Values are real and capacities nonnegative.
• $\Phi_\tau(d,s)$ is the supremum of the objective over the feasible set of (2). For nonnegative data this set contains $0$ and lies in the box $[0,\tau k]$, so the supremum is a maximum.

Probability.

• The count law at density $\tau$ is the product of independent Poisson laws on $\mathbb N^{n_d}\times\mathbb N^{n_s}$. Independence across types and between demand and supply is the paper's reading of a Poisson process per type; it is used by the proofs but not written out.
• Expectations are Bochner integrals. The integrand of the goal is bounded by $\sum|v_{u,w}|k_{u,w}$, and every function on the countable count space is measurable, so the expectation is genuine and not the junk value $0$.
• The limit is taken along integer $\tau\to\infty$, as on p. 12.
• In Lemma 2, $\max_{n\ge1}$ is read as a supremum in $[0,\infty]$, and "finite mean" as a finite lower Lebesgue integral.

Ruled out. A trivializing formalization is excluded: the expectation is taken against the Poisson laws with means $\lambda_i\tau$ and $\pi_j\tau$, with the factor $1/\tau$ inside the expectation, not against point masses at the rates or in the rescaled form $\mathbb E[\Phi(\frac1\tau D^\tau,\frac1\tau S^\tau)]$. No hypothesis beyond $\lambda,\pi\ge 0$ is imposed.

Not stated.

• The second sentence of Theorem 1, the almost-sure convergence of optimal primal and dual solutions. It assumes unique optima only inside its proof and needs a coupling across $\tau$ that the paper does not construct.
• Lemma 1's "$z^*=\tau x^*$" presupposes unique optima. It is stated as the equivalence "$x$ is optimal for $\Phi(\frac1\tau d,\frac1\tau s)$ if and only if $\tau x$ is optimal for $\Phi_\tau(d,s)$".

The statements follow arXiv:2205.02274v4. Its printed slips are corrected as disclosed in each item's Formalization Note.

Infrastructure needed.

• Monotonicity and continuity of the value of a capacitated linear program in its right-hand side.
• The Poisson Chernoff bound.
• Convergence in probability of scaled Poisson counts.

The network-program definition and the Poisson tail bound are reusable beyond this mission. Contributions toward any of these are welcome.

Selected references

• I. Bright, A. Delarue, I. Lobel, Reducing Marketplace Interference Bias Via Shadow Prices, arXiv preprint, v4, 2024; Management Science, 2025. https://arxiv.org/abs/2205.02274v4
• S. Janson, T. Łuczak, A. Ruciński, Random Graphs, Wiley, 2000, Corollary 2.4. https://doi.org/10.1002/9781118032718

Motivation

Global sensitivity analysis asks how much of the uncertainty in the output $Y$ of a model, a simulator or a learned predictor is attributable to an input $X$. A standard way to answer is to compare the law of $Y$ with its law after $X$ is revealed, and to average that discrepancy over $X$. Variance-based indices (Sobol' 1993; Wagner 1995) compare conditional and unconditional means. Density-based and distribution-based indices compare whole distributions. Rényi's postulates for measures of dependence ask, among other things, that such an index vanish exactly under independence (zero-independence) and reach its maximum exactly when $Y$ is a function of $X$ (max-functionality, Postulate E). Variance-based indices fail the first postulate, because the conditional mean can be constant while the conditional law moves.

Borgonovo, Figalli, Plischke and Savaré (Management Science, 2025) propose indices in which the discrepancy is an optimal transport cost. The squared 2-Wasserstein case is the numerator of the Wasserstein correlation coefficient of Wiesel (2022), whose Theorem 2.2 gives max-functionality for that coefficient. The paper extends max-functionality to general continuous costs, through a strict-convexity property of the transport cost on Dirac masses (Lemma 4). This mission formalizes that result, Theorem 5, together with the zero-independence property, Proposition 3.

Setting

Let $(\Omega,\mathcal B,P)$ be a probability space and $\mathsf X$, $\mathsf Y$ Polish spaces with their Borel $\sigma$-algebras. The input $X:\Omega\to\mathsf X$ and the output $Y:\Omega\to\mathsf Y$ are measurable, with laws $\mu$ and $\nu$.

A cost is a continuous function $k:\mathsf Y\times\mathsf Y\to[0,+\infty]$ with $k(y,y')=0$ if and only if $y=y'$. It need not be symmetric, a metric, or finite. For probability measures $\nu,\nu'$ on $\mathsf Y$, a coupling is a probability measure $\pi$ on $\mathsf Y\times\mathsf Y$ with marginals $\nu$ and $\nu'$, and the optimal transport cost is

$$K(\nu,\nu')=\inf_{\pi\in\Pi(\nu,\nu')}\iint k(y,y')\,d\pi(y,y').$$

For a sub-$\sigma$-algebra $\mathcal F$ of the Borel sets of $\mathsf X$, a version of the conditional distribution of $Y$ given $(X,\mathcal F)$ is a Markov kernel $x\mapsto\nu^{\mathcal F}_x$ that is $\mathcal F$-measurable in $x$ and satisfies $P(X\in A,\,Y\in B)=\int_A\nu^{\mathcal F}_x(B)\,d\mu(x)$ for $A\in\mathcal F$ and Borel $B$. The OT-based sensitivity measure of Definition 1 is

$$\xi^K(Y,X\mid\mathcal F)=\int_{\mathsf X}K(\nu,\nu^{\mathcal F}_x)\,d\mu(x),$$

written $\xi^K(Y,X)$ when $\mathcal F$ is the full Borel $\sigma$-algebra. The candidate maximum is

$$\mathbb M^K[Y]=\mathbb E[k(Y,Y')]=\iint k(y,y')\,d\nu(y)\,d\nu(y'),$$

with $Y'$ an independent copy of $Y$; for $k(y,y')=\|y-y'\|_2^2$ it equals twice the total variance of $Y$.

Formalization targets

Goal: Theorem 5 (max-functionality)

If $\mathbb M^K[Y]<+\infty$, then for every sub-$\sigma$-algebra $\mathcal F$ and every version of the conditional distribution,

$$\xi^K(Y,X\mid\mathcal F)\le\mathbb M^K[Y],$$

and

$$\xi^K(Y,X\mid\mathcal F)=\mathbb M^K[Y]\iff Y=f(X)\ P\text{-a.s. for some }\mathcal F\text{-measurable }f:\mathsf X\to\mathsf Y.$$

Milestones

The steps of the paper's proof, in order:

1. (57): $K(\nu,\nu')\le\iint k\,d\nu\,d\nu'$.
2. $K(\nu,\delta_{y'})=\int k(y,y')\,d\nu(y)$.
3. Lemma 4: for $y_1\ne y_2$ in $\operatorname{supp}\nu$ and $t\in(0,1)$,

$$K\big(\nu,(1-t)\delta_{y_1}+t\delta_{y_2}\big)<(1-t)K(\nu,\delta_{y_1})+tK(\nu,\delta_{y_2}).$$

4. (62): the disintegration $\int K(\nu,\delta_y)\,d\nu(y)=\int_{\mathsf X}\int K(\nu,\delta_y)\,d\nu^{\mathcal F}_x(y)\,d\mu(x)$.
5. The bound $K(\nu,\nu')\le\int K(\nu,\delta_y)\,d\nu'(y)$.
6. (63): at the maximum, that bound is an equality for $\mu$-a.e. $x$.
7. (65): Jensen's inequality for $K(\nu,\cdot)$ over the representation (64) of a mixture.

Companion: Proposition 3 (zero-independence)

$$\xi^K(Y,X)=0\iff X\text{ and }Y\text{ are independent}.$$

Significance

The result. Together, Proposition 3 and Theorem 5 place $\xi^K$ on a scale from $0$ (no information about $Y$ in $X$) to $\mathbb M^K[Y]$ (complete information), so the ratio $\xi^K(Y,X\mid\mathcal F)/\mathbb M^K[Y]$ is a normalized measure of association. This normalization is what lets practitioners rank inputs of a simulator or features of a model on a common scale. The result covers all continuous costs vanishing exactly on the diagonal, including the powers of a metric that give the Wasserstein indices, and arbitrary sub-$\sigma$-algebras $\mathcal F$, which model partial information about $X$ (for example the information carried by a function $g(X)$).

Formalizing it. The theorem is proved in the paper; the work here is to formalize the known proof. As far as is known, no machine-checked version of this result or of Wiesel's Wasserstein-correlation theorem exists. Along the way the development needs facts about optimal transport with extended-real costs that are not in Mathlib: the product-coupling bound, the transport cost to a Dirac mass, convexity and lower semicontinuity of $K(\nu,\cdot)$, and cyclical monotonicity of optimal plans.

Difficulty

The inequality and the "functional dependence ⇒ equality" direction are direct computations with the product coupling and with Dirac conditional laws. The converse is the hard direction. Equality of the integrals gives only the pointwise equality (63) almost everywhere, and the step from there to "$\nu^{\mathcal F}_x$ is a Dirac mass" needs strict convexity of $K(\nu,\cdot)$. Strict convexity fails for general measures: $K(\nu,\cdot)$ is affine along many segments. It holds only between Dirac masses at distinct points of $\operatorname{supp}\nu$ (Lemma 4), and even there it fails when the costs involved are infinite. A non-Dirac conditional law is not a two-point mixture, so the strict inequality must be carried over to general measures with an integrand that takes values in $[0,+\infty]$. The last step, building an $\mathcal F$-measurable $f$ from the conditional laws, is measure-theoretic bookkeeping that is easy to get wrong.

Formalization scope

• Spaces and values. $\mathsf X$ and $\mathsf Y$ are Polish with their Borel $\sigma$-algebras; the paper's supports in $\mathbb R^{n_X}$, $\mathbb R^{n_Y}$ are such spaces. All of $k$, $K$, $\mathbb M^K$ and $\xi^K$ take values in $[0,+\infty]$ (ℝ≥0∞), so $+\infty$ is allowed as on the page, and integrals are lower Lebesgue integrals.
• Transport cost. $K$ is the published definition RWPI.SqrtLasso.transportCost. Its first argument is the marginal $\nu$, and the cost is evaluated as $k(y,y')$ with $y\sim\nu$.
• Conditional laws. The conditional distribution is not a chosen object. Any Markov kernel satisfying the defining property IsCondDistrib is admissible, and every theorem quantifies over all versions and over all sub-$\sigma$-algebras $\mathcal F$.
• Ruled-out encodings. The goal must not fix $\mathcal F$ to the Borel $\sigma$-algebra or fix a version of the kernel. Its conclusion must not be replaced by "$\nu^{\mathcal F}_x$ is a Dirac mass for $\mu$-a.e. $x$", which is an intermediate step of the proof, not the theorem.
• Disclosed correction. Lemma 4 carries the extra hypotheses $K(\nu,\delta_{y_1}),K(\nu,\delta_{y_2})<+\infty$. As printed, both sides of (19) can be $+\infty$ under the lemma's assumptions. Theorem 5 is stated as printed.
• Not posed. The cyclical monotonicity of optimal plans, cited from Villani (2008, Ch. 5), and the existence of optimal plans used in Proposition 3 are standard optimal-transport facts. They are not milestones but are welcome as supporting lemmas.

Selected references

• E. Borgonovo, A. Figalli, E. Plischke, G. Savaré, Global Sensitivity Analysis via Optimal Transport, Management Science, 2025 (authors' manuscript of 7 March 2024 used here). https://doi.org/10.1287/mnsc.2023.01796
• J. Wiesel, Measuring Association with Wasserstein Distances, Bernoulli 28(4):2816–2832, 2022. https://doi.org/10.3150/21-BEJ1438
• C. Villani, Optimal Transport: Old and New, Springer, 2008. https://doi.org/10.1007/978-3-540-71050-9
• A. Rényi, On Measures of Dependence, Acta Mathematica Academiae Scientiarum Hungaricae 10:441–451, 1959. https://doi.org/10.1007/BF02024507
• I. M. Sobol', Sensitivity Estimates for Nonlinear Mathematical Models, Mathematical Modelling and Computational Experiments 1:407–414, 1993.
• H. M. Wagner, Global Sensitivity Analysis, Operations Research 43(6):948–969, 1995. https://doi.org/10.1287/opre.43.6.948

Motivation

Firms that sell to the same customers over time learn who bought from whom. Behavior-based pricing (BBP) — charging a firm's own past customers one price and the rival's past customers another — has been studied since Fudenberg and Tirole (2000) and Villas-Boas (1999). A second instrument is the disclosure of product quality: free samples, demonstrations and trial versions reveal the quality of a new product, at a cost per customer reached. With purchase histories, a firm can disclose differently to its own customers and to the rival's: behavior-based disclosure (BBD). The classical disclosure model is Jovanovic (1982), in which costly disclosure leads a firm to reveal quality only above a threshold.

Zhang and Li (2025) combine the two instruments in a two-period Hotelling duopoly and compare BBD with uniform disclosure. Their Proposition 1 shows that BBD always raises second-period profits; this mission is about the whole game, where the answer depends on the disclosure cost.

Setting

A unit mass of customers is uniformly distributed on $[0,1]$; firm A is at $0$, firm B at $1$, the transportation cost is $1$, marginal costs are $0$ and the market is fully covered.

Period 1. The firms charge prices $p_{a1},p_{b1}\ge 0$. The first-period purchase splits the line at $x_1$: A's old customers are $[0,x_1]$ (A's turf), B's are $[x_1,1]$ (B's turf).

Period 2. Each firm $i$ launches a new product of quality $q_i$, with $q_a,q_b$ independent and uniform on $[0,1]$. A firm discloses its quality to a segment iff it exceeds a disclosure threshold $\hat q$; disclosing costs $c$ per customer reached. A segment that sees no disclosure believes the quality is $\hat q/2$. Under uniform disclosure each firm has one threshold $\hat q_i$ for the whole line; under BBD it has $\hat q_{io}$ for its own customers and $\hat q_{in}$ for the rival's. On each turf the two firms then play a price game (A charges $p_{ao}$ and B charges $p_{bn}$ on A's turf; $p_{an}$ and $p_{bo}$ on B's turf), and customers stay or switch according to their beliefs and prices.

Forward-looking customers. The share $x_1$ is the location of the marginal consumer, who compares the two first-period options including the expected second-period surplus of staying or switching ((6) for uniform disclosure, (15) for BBD):

$$-x_1-p_{a1}+\max\{-(1-x_1)+E(\tilde q_{bn}-p^*_{bn}),\,-x_1+E(\tilde q_{ao}-p^*_{ao})\}=-(1-x_1)-p_{b1}+\max\{-x_1+E(\tilde q_{an}-p^*_{an}),\,-(1-x_1)+E(\tilde q_{bo}-p^*_{bo})\}.$$

Two-period profits (8) are $\Pi_a=p_{a1}x_1+E(\pi_{a2})$ and $\Pi_b=p_{b1}(1-x_1)+E(\pi_{b2})$, with $E(\pi_{i2})$ the ex ante second-period profit at share $x_1$. A symmetric subgame-perfect equilibrium is a common first-period price $p^*$ together with a second-period equilibrium at every share and a consistent share at every price pair, such that neither firm gains from any other nonnegative first-period price. Its total profits are $\Pi^*_a,\Pi^*_b$.

The standing assumption is $0<c<5/36$ (p. 8515).

Formalization targets

Goal: Proposition 3(a)

There is a cutoff $c_l\in(0,5/36)$ such that for every $c\in(0,5/36)$, symmetric subgame-perfect equilibria exist under both regimes and, for any two of them,

$$c>c_l\;\Rightarrow\;\Pi^{*,U}_i<\Pi^{*,BBD}_i,\qquad c<c_l\;\Rightarrow\;\Pi^{*,BBD}_i<\Pi^{*,U}_i\qquad (i=a,b).$$

The value of $c_l$ is left unfixed, as in the paper.

Milestones

1. (5) and (14): the ex ante second-period profit as a function of $x_1$ and the equilibrium thresholds, in region 1, e.g. under BBD

$$E(\pi_{a2})=\tfrac{(1+2x_1)^2+(3-4x_1)^2}{18}+\tfrac{4-\hat q_{ao}^3-\hat q_{an}^3-\hat q_{bo}^3-\hat q_{bn}^3}{216}-c\,[1-x_1\hat q_{ao}-(1-x_1)\hat q_{an}].$$

2. (7) and (16): in region 1 the first-period share is $x_1=\tfrac12+\tfrac38(p_{b1}-p_{a1})$ under both regimes.
3. (9) and (17): existence of symmetric equilibria, and their prices

$$p^{*,U}=\tfrac23\big(2-c+\tfrac{c}{\sqrt{1+27c}}\big),\qquad p^{*,BBD}=\tfrac43-\tfrac{c(5+54c)}{3\sqrt{1+12c}}+\tfrac{c(5+162c)}{3\sqrt{1+108c}},$$

with share $x_1^*=\tfrac12$. 4. Table 1, total profits, both regimes, in closed form. 5. Proposition 2: a cutoff $c_h\in(0,5/36)$ across which the comparison of first-period prices and profits reverses.

Significance

Proposition 3(a) is the paper's answer to the managerial question in its title. BBD lets a firm disclose to its own customers more often than to the rival's (retention-focused disclosure), which improves the efficiency of disclosure and raises second-period profits. In the first period, however, BBD changes how hard firms compete for customers, and when disclosure is cheap the first-period loss dominates. The result locates the sign change of the total effect at a single cutoff, and together with Proposition 2 ($c_l<c_h$) it separates three regimes of $c$: total profits fall, total profits rise despite lower first-period profits, and both rise.

None of these results is formalized anywhere. The paper's proofs are in an Online Appendix and its displayed formulas are the end points of long computations. A complete development would produce:

• a machine-checked solution of a two-period Hotelling model with behavior-based pricing, including corner regions of the second-period price game;
• a costly-disclosure equilibrium in the Jovanovic style;
• a verified single-crossing analysis of algebraic functions of $c$.

Difficulty

The model nests three equilibrium notions: a clamped price game on each turf, threshold disclosure as a best response to the rival and to the induced beliefs, and first-period pricing with forward-looking customers. The first-order condition behind (9) and (17) involves the derivative of $E(\pi_{a2})$ in $x_1$, and every threshold, including the rival's, moves with $x_1$; treating the rival's thresholds as fixed gives a wrong price.

The symmetric first-order condition alone does not settle the equilibrium. A deviation in first-period price can push the share outside the region where all second-period prices are interior, into the corner regions 2 and 3 of Lemma 1/2, where the second-period profit has a different form. The paper checks these deviations only in its Online Appendix.

The final comparison is a sign analysis of an expression with three different square roots on $(0,5/36)$. The difference of total profits is small throughout: for example, about $-5\cdot10^{-4}$ at $c=0.01$ and $3.5\cdot10^{-3}$ at $c=0.1$.

Formalization scope

• Representation. Qualities are integrated by iterated interval integrals over $[0,1]$. The base value $v$ cancels and is omitted; full coverage is built in. Prices are nonnegative, turf shares are clamped to the turf, and the nondisclosure belief stays $\hat q/2$ when a firm considers a deviation.
• Equilibria, not formulas. Second-period prices are Nash equilibria of the clamped turf games for every belief pair in $[0,1]^2$. Thresholds are best responses ("disclose iff $q>\hat q$" is optimal), never roots of the indifference equation. The share satisfies (6)/(15) as printed, a maximum of two expectations, with corner shares $x_1\in\{0,1\}$ read through nearby interior shares (at an endpoint one turf is empty and its second-period prices are not pinned down, so (6)/(15) is not evaluated there). First-period deviations range over all nonnegative prices, and the second-period profile is an equilibrium at every share, including shares reached only after a deviation.
• Readings. "In region 1" for (5), (7), (14), (16) means that every belief pair on the support is in region 1: $\tfrac12-\hat q_{bn}/8<x_1<\tfrac12+\hat q_{an}/8$ (BBD), $\tfrac12-\hat q_b/8<x_1<\tfrac12+\hat q_a/8$ (uniform). Table 1's uniform total profit is used; the sentence on p. 8517 prints $\sqrt{1+72c}$ for $\sqrt{1+27c}$.
• Ruled out. Hard-wiring $x_1=\tfrac12$, defining thresholds or prices by their closed forms, or stating the goal on the Table 1 formulas alone would each trivialize the mission; the cutoff is quantified before $c$ and lies strictly inside $(0,5/36)$, and existence of equilibria is part of the goal.
• Not posed. Proposition 3(b), (c) (consumer surplus and welfare are defined in the paper only by their Table 1 values) and Proposition 4.
• Needed. Piecewise-quadratic integrals over the belief support; Nash equilibria of clamped linear-demand games; existence of a consistent first-period share (an intermediate-value argument on a suitable equilibrium selection); and sign analysis with square roots. The second-period model is the same as in the companion mission on Proposition 1, and lemmas about it are reusable there. Contributions of any of the milestones, of Lemma 1/2 in all regions, or of the corner-region versions of (4), (5), (13), (14) are welcome.

Selected references

• J. Zhang and K. J. Li, Retention or Acquisition? Behavior-Based Quality Disclosure, Management Science 71(10), 8510–8525, 2025. https://doi.org/10.1287/mnsc.2022.01081
• D. Fudenberg and J. Tirole, Customer Poaching and Brand Switching (cited in Zhang and Li as "Customer poaching and firm switching"), RAND Journal of Economics 31(4), 634–657, 2000.
• J. M. Villas-Boas, Dynamic Competition with Customer Recognition, RAND Journal of Economics 30(4), 604–631, 1999.
• B. Jovanovic, Truthful Disclosure of Information, Bell Journal of Economics 13(1), 36–44, 1982.

Motivation

A multiclass queueing network routes jobs of several classes through shared stations. Whether such a network is stable depends on the scheduling policy and not only on the load: the Lu–Kumar and Rybko–Stolyar examples are unstable under a static-priority policy with every station loaded below capacity (Bramson, Stability of Queueing Networks, 2008). A network operator who does not control, or does not know, the policy in use therefore wants robust stability: stability under every policy of a given family.

Zhao, Gurvich and Hasenbein (arXiv:2303.17746v3) study robust stability over the family of queue-ratio policies, which steer each station's workload towards fixed proportions across its classes and contain the static-priority and quadratic max-weight policies as special cases. Their analysis is hierarchical. Under a queue-ratio policy the fluid model first reaches state-space collapse and then follows a linear Skorohod problem. This mission formalizes the second layer: a purely algebraic sufficient condition for stability of that Skorohod problem holds for every queue-ratio policy as soon as it holds at the finitely many static-priority "corners".

Timeline. Dai (1995) reduced stability of the queueing network to stability of its fluid model. Delgado (2010) related fluid stability under state-space collapse to stability of a Skorohod problem. Chen (1996) gave the Chen-$\mathcal S$ sufficient condition for stability of a linear Skorohod problem. Zhao, Gurvich and Hasenbein (preprint 2023, Operations Research 2025) proved that Chen-$\mathcal S$ is inherited from the static-priority corners (their Theorem 4).

Setting

Fix an open network with $J$ stations and $K$ classes. Class $k$ is served at station $s(k)$, and the $J\times K$ constituency matrix $C$ has $C_{jk}=1$ if $s(k)=j$ and $0$ otherwise. $M=\operatorname{diag}(m_1,\dots,m_K)$ holds the mean service times $m_k>0$. $P$ is the substochastic routing matrix, and $\alpha\ge 0$ the vector of exogenous arrival rates. The network is open: $I+P+P^2+\cdots$ converges and $I-P^\top$ is invertible. Then $Q=(I-P^\top)^{-1}$, $\lambda=Q\alpha$ and the traffic intensities are $\rho=CM\lambda$.

A ratio matrix is a $K\times J$ matrix $\Delta$ with $\Delta_{kj}=\delta_k\ge 0$ if $s(k)=j$ and $\Delta_{kj}=0$ otherwise, normalized by

$$CM\Delta=I.$$

It is static-priority if at each station $j$ exactly one class $k$ with $s(k)=j$ has $\Delta_{kj}=1/m_k$ and all others have $\Delta_{lj}=0$. For a ratio matrix with $CMQ\Delta$ invertible, the reflection matrix and drift are

$$R_\Delta=(CMQ\Delta)^{-1},\qquad \theta_\Delta=R_\Delta(\rho-e).$$

A square matrix $R$ is an S-matrix if $Ru>0$ for some $u>0$, and completely-$\mathcal S$ if every principal sub-matrix is an S-matrix. The pair $(R,\theta)$ is Chen-$\mathcal S$ if $R$ is completely-$\mathcal S$ and some $h>0$ satisfies $h_a^\top[\theta_a+R_{ab}u]<0$ for every partition $(a,b)$ of the stations with $a\neq\emptyset$ and every $u\ge 0$ with $\theta_b+R_bu=0$. Ratio matrices are neighbors if they differ in at most one column.

Formalization targets

Goal: Theorem 4

If for every static-priority $\Delta$ the matrix $CMQ\Delta$ is invertible and $(R_\Delta,\theta_\Delta)$ is Chen-$\mathcal S$, and all $\det(CMQ\Delta)$ over static-priority $\Delta$ have one sign, then

$$\forall\,\Delta\ \text{ratio matrix}:\quad CMQ\Delta\ \text{invertible and}\ (R_\Delta,\theta_\Delta)\ \text{Chen-}\mathcal S.$$

The network is arbitrary: any $J$, $K$, routing and service times.

Milestones

For neighbors $\Delta_1,\Delta_2$ and $\Delta_3=\lambda\Delta_1+(1-\lambda)\Delta_2$ with $\lambda\in(0,1)$:

• Lemma 4. The $k$th rows of $R_{\Delta_1}$ and $R_{\Delta_2}$ are proportional with ratio $\det(CMQ\Delta_2)/\det(CMQ\Delta_1)$, and $R_{\Delta_3}$ is a rank-one update of either.
• Theorem 6. $R_{\Delta_3}=\beta R_{\Delta_1}+(1-\beta)R_{\Delta_2}$, with $\beta=\lambda\det R_{\Delta_2}/(\lambda\det R_{\Delta_2}+(1-\lambda)\det R_{\Delta_1})$.
• Lemma 3. Invertibility of $CMQ\Delta_3$ when the determinants of $CMQ\Delta_1$ and $CMQ\Delta_2$ share a sign.
• Theorem 5(i), (ii). Completely-$\mathcal S$, and Chen-$\mathcal S$ of $(R_\Delta,\theta_\Delta)$, pass from $\Delta_1,\Delta_2$ to $\Delta_3$.
• Theorem 3. The completely-$\mathcal S$ analogue of the goal.

Significance

By Chen's theorem, Chen-$\mathcal S$ of $(R_\Delta,\theta_\Delta)$ makes the Skorohod problem of the policy $\Delta$ stable. Theorem 4 reduces this requirement over a continuum of policies to a finite check, one per static-priority policy, and the paper combines it with a state-space-collapse result to certify robust queue-ratio stability of the DHV, push-started Lu–Kumar and Lu–Kumar networks. The orthogonal convexity of Theorem 5 is of independent interest: the Chen-$\mathcal S$ region of ratio matrices is in general not convex, yet it is convex along every axis-parallel segment.

The results are proved on paper and nothing in this mission has been machine-checked. A formal development checks the matrix algebra (adjugate and Sherman–Morrison identities, determinant-sign arguments) and settles the details the paper leaves out. The proof of Theorem 5(ii) is given there only as "an identical argument" to that of part (i). Theorem 6's claim $\beta\in(0,1)$ needs a same-sign hypothesis that the page omits (see below).

Difficulty

The obvious argument fails because the convexity is only orthogonal. The set of ratio matrices is a product of simplices. A convex combination of two arbitrary Chen-$\mathcal S$ ratio matrices need not be Chen-$\mathcal S$, and the inverse $R_\Delta=(CMQ\Delta)^{-1}$ is not affine in $\Delta$. Two pieces of structure must be found and exploited instead. Moving one column of $\Delta$ changes $CMQ\Delta$ in one column, which makes $R_\Delta$ move along a line in a reparametrized coordinate $\beta$. Then completely-$\mathcal S$ and Chen-$\mathcal S$, whose definitions quantify over all partitions and over the solution sets $\{u\ge 0:\theta_b+R_bu=0\}$, must be shown to survive that line. The latter sets move with $\beta$ in a way that does not follow from convexity of either endpoint's set. Passing from neighbors to all ratio matrices needs a column-by-column descent through faces of the product of simplices. Invertibility must be maintained along the way, which is where the common determinant sign at the corners enters.

Formalization scope

• Stations are Fin J, classes Fin K; the paper's index $i$ is Lean's $i-1$. The network is a structure Network J K with fields $s$, $m$, $P$, $\alpha$ and the hypotheses $m>0$, $P\ge 0$, row sums of $P$ at most one, $\alpha\ge 0$, summability of $P^n$, and invertibility of $I-P^\top$. The remark $K>J$ and the renewal arrivals are not used.
• $C$, $M=\operatorname{diag}(m)$, $Q=(I-P^\top)^{-1}$, $\lambda=Q\alpha$, $\rho=CM\lambda$ are definitions computed from the network. $R_\Delta$ and $\theta_\Delta$ are definitions computed from $\Delta$; $\theta_\Delta$ is never a free vector.
• Ratio matrices include $\delta\ge 0$. Without it the goal would assert extrapolation outside the polytope of ratio matrices.
• Lean's matrix inverse is $0$ on singular matrices. Every hypothesis on a corner and the goal's conclusion state invertibility of $CMQ\Delta$ explicitly.
• Partitions are a : Finset (Fin J) with $b=a^{\mathrm c}$; sub-matrices are indexed by the subtypes. Chen-$\mathcal S$ quantifies over $a\neq\emptyset$ (for $a=\emptyset$ the condition reads $0<0$ and would make Chen-$\mathcal S$ unsatisfiable and the goal vacuous); $b=\emptyset$ is allowed. Principal sub-matrices in completely-$\mathcal S$ are those of nonempty index sets.
• "All determinants have the same sign" is a single sign for all corners: either all are positive or all are negative.
• The "Then, $\Delta_1,\Delta_2,\Delta_3$ are ratio-matrix neighbors" sentence of Lemmas 3, 4 and Theorems 5, 6 is kept as a first conjunct.
• Deviation. Theorem 6 asserts $\beta\in(0,1)$ under invertibility alone, which fails when $\det R_{\Delta_1}$ and $\det R_{\Delta_2}$ have opposite signs. That clause is stated under $\det R_{\Delta_1}\det R_{\Delta_2}>0$; the two identities are stated unconditionally.

A complete development needs the adjugate and determinant identities for matrices differing in one column, a Sherman–Morrison formula for rank-one updates, and a decomposition of ratio matrices along faces of a product of simplices. The definitions of S-matrices, completely-$\mathcal S$ and Chen-$\mathcal S$ are reusable for other work on reflected processes. Proofs of the milestones, alternative proofs of Theorem 5 that avoid linear-programming duality, and counterexamples showing a hypothesis cannot be dropped are all welcome.

Selected references

• Y. Zhao, I. Gurvich, J. Hasenbein, A Hierarchical Approach to Robust Stability of Multiclass Queueing Networks, arXiv:2303.17746v3, 2024. https://arxiv.org/abs/2303.17746
• H. Chen, A sufficient condition for the positive recurrence of a semimartingale reflecting Brownian motion in an orthant, Annals of Applied Probability 6(3):758–765, 1996 (reference [5] of the source).
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1):49–77, 1995 (reference [10] of the source).
• R. Delgado, State space collapse and stability of queueing networks, Mathematical Methods of Operations Research 72(3):477–499, 2010 (reference [16] of the source).
• M. Bramson, Stability of Queueing Networks, Lecture Notes in Mathematics 1950, Springer, 2008. https://doi.org/10.1007/978-3-540-68896-9

Motivation

Thompson sampling (TS) is the standard randomized heuristic for the Bayesian multi-armed bandit: at each decision it samples a parameter vector from the current posterior and pulls the arm that would be best if the sample were true. It ignores the remaining horizon. Min, Maglaras and Moallemi (arXiv:1902.04251, Management Science, 2025) obtain horizon-aware generalizations of TS from the information relaxation duality of Brown, Smith and Sun (Oper. Res. 2010). Each penalty function yields an upper bound on the Bayes-optimal value and an IRS policy. Such a policy samples a whole future outcome and plays the first action of the penalized clairvoyant optimum. With the zero-information penalty it is exactly TS.

Two of these policies, IRS.FH and IRS.V-Zero, are designed to interpolate between TS and the myopic rule. When one period remains they pull the arm with the highest predictive mean (Remark 5 of the paper). This mission formalizes the other end, Proposition 1: when many periods remain, they randomize exactly as Thompson sampling does. The paper presents this as the sense in which IRS policies "behave like TS during the initial decision epochs" and shift smoothly from exploration to exploitation without a tuning parameter.

Setting

There are $K \ge 1$ arms $\mathcal A = \{1,\dots,K\}$. Arm $a$ has an unknown parameter $\theta_a$. Given $\theta_a$, its rewards $R_{a,1}, R_{a,2}, \dots$ are i.i.d. with law $\mathcal R_a(\theta_a)$. The prior of $\theta_a$ is $\mathcal P_a(y_a)$, a member of a conjugate family indexed by a belief $y_a$. A Bayesian update $\mathcal U_a$ maps $(y_a, r)$ to the posterior belief after a reward $r$. The arms are independent. Throughout, rewards are integrable: $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief (display (3)).

• The conditional mean reward is $\mu_a(\theta_a) = \mathbb E[R_{a,n} \mid \theta_a]$, and the predictive mean is $\bar\mu_a(y_a) = \mathbb E_{y_a}[\mu_a(\theta_a)]$.
• The outcome $\omega = (\theta, (R_{a,n})_{a,n})$ has law $\mathcal I(y)$.
• The posterior predictive mean after the first $n$ rewards of arm $a$ is $\hat\mu_{a,n}(\omega; y_a) = \mathbb E_{y_a}[\mu_a(\theta_a) \mid R_{a,1},\dots,R_{a,n}]$.

At remaining horizon $T$ and belief $y$, the three policies act as follows:

1. TS samples $\tilde\theta \sim \mathcal P(y)$ and plays $A^{TS}(y) = \operatorname{argmax}_a \mu_a(\tilde\theta_a)$.
2. IRS.FH samples $\tilde\omega \sim \mathcal I(y)$ and plays $A^{IRS.FH}(T,y) = \operatorname{argmax}_a \hat\mu_{a,T-1}(\tilde\omega)$, the arm with the best posterior mean after $T-1$ sampled rewards of every arm.
3. IRS.V-Zero samples $\tilde\omega \sim \mathcal I(y)$ and solves the allocation problem

$$\max_{n \in \mathcal N_T} \sum_{a=1}^K \sum_{i=1}^{n_a} \hat\mu_{a,i-1}(\tilde\omega), \qquad \mathcal N_T = \Big\{n \in \mathbb N_0^K : \sum_a n_a = T\Big\}.$$

It then plays the arm $A^{IRS.V\text{-}Zero}(T,y) = \operatorname{argmax}_a \tilde n^*_a$ to which the optimal allocation $\tilde n^*$ assigns the most pulls.

Each action is a random variable driven by the policy's own sample.

Formalization targets

Goal: Proposition 1 (p. 25)

Assume $\mu_i(\theta_i) \ne \mu_j(\theta_j)$ almost surely under $\mathcal P(y)$, for all $i \ne j$. Then for every arm $a$,

$$\lim_{T\to\infty} \mathbb P[A^{IRS.FH}(T,y) = a] = \mathbb P[A^{TS}(y) = a], \qquad \lim_{T\to\infty} \mathbb P[A^{IRS.V\text{-}Zero}(T,y) = a] = \mathbb P[A^{TS}(y) = a].$$

This holds for every choice of the tie-breaking rules in the argmaxes and in the allocation problem.

Milestones

1. Proposition 4 (p. 53): $\mu_a(\theta_a)$ and $\max_a \mu_a(\theta_a)$ are integrable under the prior.
2. Proposition 5 (p. 54): $\hat\mu_{a,n}$ and the sample mean $\frac1n\sum_{i\le n} R_{a,i}$ converge almost surely to $\mu_a(\theta_a)$.
3. Display (109) (p. 54): if a sequence of vectors converges to a vector with distinct entries, every argmax rule eventually selects the argmax of the limit.
4. The allocation argument (113)–(123) (pp. 54–56): if the payoff rows converge to distinct limits, then for large $T$ every optimal allocation gives its largest share only to the arm with the largest limit.
5. Display (55) alone: the IRS.FH half of the goal.

Significance

Proposition 1 identifies the long-horizon behaviour of the two IRS policies with that of Thompson sampling. Together with Remark 5 it pins down both ends of the horizon. It explains why their simulated regret curves track TS early and the myopic policy late (§5 of the paper). It also shows that the design choice "play the arm with the largest allocation" in IRS.V-Zero is the one that recovers TS. Other selection rules, such as any arm with a positive allocation, need not.

The paper gives a complete proof in Appendix D.1–D.2. A machine-checked version adds three things. It fixes the probabilistic model of a conjugate Bayesian bandit with infinite reward sequences in Lean, which the companion missions on the same paper also need. It makes the role of tie-breaking explicit. And it repairs a step of the printed proof: the bound $n^\circ(A^\circ_T) \ge \lfloor T/2 \rfloor$ in §D.2 holds only for two arms, and the general case needs $\lceil T/K \rceil$ and a threshold growing with $K$. No formalization of this result is known on Prove2Me or in Mathlib.

Difficulty

The IRS.FH half reduces to almost-sure convergence of posterior means, which is a martingale argument (Lévy's upward theorem). That argument needs $\mu_a(\theta_a)$ to be measurable with respect to the limit $\sigma$-algebra of the reward sequence, a fact supplied by the strong law of large numbers. Building the outcome law, a mixture over $\theta$ of infinite product measures, and identifying the conjugate update with conditional expectation are where the measure theory lies.

The IRS.V-Zero half does not follow from convergence of the posterior means alone. The selected arm is a function of an optimal allocation of a combinatorial problem whose size grows with $T$. The naive expectation that the arm with the best limit receives "most" pulls has to be proved by an exchange argument that handles the finitely many early terms, where the posterior means can still be badly ordered. The printed version of this argument is correct only for $K = 2$.

Formalization scope

• Arms are Fin K with NeZero K; the reward sequence of an arm is ℕ → ℝ, 0-based.
• One parameter type and one belief type serve all arms; reward laws and priors are Markov kernels.
• Conjugacy is stated as Bayes' rule on rectangles for every belief. The update is assumed jointly measurable, and the standing integrability (3) is assumed for every belief.
• The outcome law $\mathcal I(y)$ is a product over arms of mixtures $\int \delta_\theta \otimes \mathcal R_a(\theta)^{\otimes \mathbb N}\, \mathcal P_a(y_a)(d\theta)$.
• $\hat\mu_{a,n}$ is the pathwise conjugate version $\bar\mu_a(y_{a,n})$ of the conditional expectation (10), defined at every outcome so that it can sit inside an argmax.
• $\mathbb P[A = a]$ is the mass of $\{a\}$ under the pushforward of the policy's sampling law. All tie-breaking rules are required to be measurable; otherwise the pushforward would be the zero measure.
• The assumption of the proposition is required almost surely under the prior, not as injectivity of $\mu$.
• A formalization in which the selectors were non-measurable, the outcome law degenerate, or the distinctness hypothesis unsatisfiable would make the goal vacuous. The definitions rule out the first two, and a deterministic two-arm instance shows the hypotheses are satisfiable.

The development needs Lévy's upward theorem (MeasureTheory.tendsto_ae_condExp in Mathlib) and the strong law of large numbers (ProbabilityTheory.strong_law_ae). It also needs a lemma identifying iterated conjugate updates with the posterior given finitely many rewards, and the measurability of $\theta \mapsto \mathcal R_a(\theta)^{\otimes\mathbb N}$. These last two are reusable for any Bayesian bandit or sequential-estimation development. Contributions of the two deterministic milestones are self-contained and welcome first.

Selected references

• S. Min, C. Maglaras, C. C. Moallemi, Thompson Sampling with Information Relaxation Penalties, Management Science, 2025; preprint arXiv:1902.04251v2, 2021. https://arxiv.org/abs/1902.04251
• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research 58(4), 2010. https://doi.org/10.1287/opre.1090.0796
• W. R. Thompson, On the Likelihood that One Unknown Probability Exceeds Another in View of the Evidence of Two Samples, Biometrika 25(3/4), 1933. https://doi.org/10.2307/2332286
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014. https://doi.org/10.1287/moor.2014.0650

Motivation

Multi-server queues model call centres, hospital wards, cloud server pools and any system in which $n$ identical servers work through one first-come-first-served (FCFS) line. Capacity planning for such systems needs bounds on the steady-state queue length and on the probability of delay (the chance that an arriving job finds every server busy) that are explicit, hold for every $n$, and stay informative as the load approaches capacity.

For a single server, Kingman's bound (Kingman 1962, ref. [89] of the paper) gives exactly this: the mean wait is at most a multiple of $1/(1-\rho)$ that depends only on the first two moments of the inter-arrival and service times. For $n$ servers with general distributions (the GI/GI/n queue), no comparable explicit bound was known.

Timeline.

• 1962: Kingman's single-server bound.
• 1981: Halfin and Whitt identify the heavy-traffic regime $\sqrt n(1-\rho)\to\beta$ in which the probability of delay is nondegenerate (Halfin and Whitt 1981).
• 2013: Gamarnik and Goldberg prove (for the GI/G/n queue) that the steady-state number waiting is stochastically dominated by the supremum of a process built from independent renewal processes (Gamarnik and Goldberg 2013). Their bound is not explicit and needs more than two service moments.
• 2017–2025: Li and Goldberg derive explicit bounds with $1/(1-\rho)$ scaling under $\mathbb E[A^2]<\infty$ and $\mathbb E[S^{2+\epsilon}]<\infty$ (arXiv:1706.04628, Mathematics of Operations Research 2025).

Setting

A GI/GI/n queue has $n\ge1$ identical servers and one FCFS line. Jobs arrive with i.i.d. inter-arrival times distributed as a nonnegative random variable $A$. Each job needs an i.i.d. service time distributed as a nonnegative random variable $S$, independent of the arrivals. An arriving job starts service at the first server to become free, in order of arrival.

Write $\mu_A=1/\mathbb E[A]$ and $\mu_S=1/\mathbb E[S]$ for the arrival and service rates, and $\rho=\mu_A/(n\mu_S)$ for the traffic intensity. The moment index is

$$r^*=\sup\{r:\mathbb E[S^r]<\infty\},$$

which may be $+\infty$. Normalised moments are $\mathbb E[(A\mu_A)^2]$ and $\mathbb E[(S\mu_S)^r]$.

$Q(t)$ is the number of jobs in the system (in service and waiting) at time $t$. "$Q(\infty)$ exists" means that, whatever the initial condition, $Q(t)$ converges in distribution as $t\to\infty$ to a random variable $Q(\infty)$. The steady-state number waiting is $L(\infty)=\max(0,Q(\infty)-n)$, and the steady-state probability of delay is $\mathbb P(Q(\infty)\ge n)$.

The milestones also use equilibrium renewal processes. For a nonnegative $X$ with finite mean, its equilibrium law $R(X)$ satisfies $\mathbb P(R>y)=\frac1{\mathbb E[X]}\int_y^\infty\mathbb P(X>z)\,dz$. An equilibrium renewal process with renewals distributed as $X$ has its first renewal interval distributed as $R(X)$ and the later ones distributed as $X$.

$A_e(t)$ counts the renewals in $[0,t]$ of such a process for $A$. $N_{e,1}(t),\dots,N_{e,n}(t)$ count those of $n$ independent such processes for $S$, also independent of $A_e$.

Formalization targets

Goal: Theorem 2 (pp. 9–10)

Assume

• $\mathbb E[A^2]<\infty$;
• $r^*>2.5$;
• $\mu_A<n\mu_S$;
• $Q(\infty)$ exists.

Then for all $x>0$ and all $r\in[2.5,r^*)$,

$$\mathbb P\Big(L(\infty)\ge\frac x{1-\rho}\Big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^6)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)x^{-\frac r2}+1.1\,e^{-.0225\,\mathbb E[(A\mu_A)^2]^{-1}x},$$ $$\mathbb P\big(Q(\infty)\ge n\big)\le 2\cdot10^4\,\mathbb E[(S\mu_S)^2]\,(10^7)^r\Big(\mathbb E[(S\mu_S)^2]^{r-1}r^{2.5r}+r^{1.5r}\mathbb E[(S\mu_S)^r]\Big)\big(n(1-\rho)^2\big)^{-\frac r2}+1.1\,e^{-.0028\,\mathbb E[(A\mu_A)^2]^{-1}n(1-\rho)^2}.$$

The paper states the infimum over $r$. With $r$ universally quantified the statement is equivalent, because the exponential term does not depend on $r$.

Milestones

They follow the paper's proof, in attack order:

• Lemma 1, the Gamarnik–Goldberg comparison $\mathbb P(L(\infty)\ge x)\le\mathbb P(\sup_{t\ge0}(A_e(t)-\sum_{i=1}^nN_{e,i}(t))\ge x)$;
• Lemma 2, which splits that supremum into an arrival part and a service part;
• Lemmas 8, 9 and 10, which reduce the arrival part to Kingman's bound with an explicit exponent;
• Lemma 3, the exponential bound for the arrival part;
• Lemma 4 and Theorem 10, conditional bounds from central moments of the pooled process $\sum_iN_{e,i}(t)$;
• Lemmas 5 and 6, those central-moment bounds;
• the explicit bound for $r\in(2.5,r^*)$ displayed on p. 28;
• Lemma 14, a transient comparison for a queue started with all servers busy;
• Lemma 7 and Corollary 5, comparisons with fewer servers that make the bound informative at the level $Q(\infty)\ge n$.

Significance

The result. The bounds hold for every $n$ and every load with $\rho<1$, and they depend on the distributions only through a few normalised moments. In the Halfin–Whitt regime, $n(1-\rho)^2$ stays bounded away from zero, so the delay bound stays informative. As $\rho\to1$ with $n$ fixed, the queue tail decays at the Kingman scale $1/(1-\rho)$. These are the first such bounds for general GI/GI/n queues; earlier explicit results needed Poisson arrivals or exponential service. The paper derives from Theorem 2 bounds at a fixed $r$ (Corollaries 1–2), a refinement beyond $1/(1-\rho)$ scaling when $n(1-\rho)^2$ is large (Corollary 3), and optimised bounds under growth conditions on $\mathbb E[(S\mu_S)^r]$ (Theorem 3).

Formalization. The theorem is proved in the paper, partly in a supplemental appendix, and none of it is formalized; there are no machine-checked results for multi-server queues with general distributions anywhere. A complete development would add to the platform the first FCFS multi-server queue with general distributions, its steady state, equilibrium renewal processes, and the Gamarnik–Goldberg comparison chain. Each is reusable for later work on many-server queues.

Difficulty

The obvious route is to compare the $n$-server queue with a single-server one, or to apply a heavy-traffic limit. The first loses a factor of $n$; the second gives limits but no bounds at a fixed $n$.

The paper's route needs two hard ingredients:

• Comparison with renewal processes. The stochastic comparison of Lemmas 1 and 14 is a theorem about the sample-path dynamics of FCFS service, not a calculation.
• Uniform moment bounds. Explicit control of $\mathbb E|\sum_{i=1}^nN_{e,i}(t)-nt|^r$ at the scale $(nt)^{r/2}$, uniformly in $n$ and $t$, is required. Classical renewal moment bounds are either asymptotic in $t$ or lose the dependence on $n$.

For the probability of delay, Lemma 1 at level $0$ gives only the trivial bound $1$. A second comparison across server counts (Lemma 7) is needed.

Formalization scope

Laws. $A$ and $S$ are represented by their laws $\mu_A,\mu_S$: probability measures on $\mathbb R$ carried by $[0,\infty)$, integrable, with positive mean. Positivity of the means is implicit in the paper, which needs $\mu_X=1/\mathbb E[X]$ finite; it is stated explicitly. $\mathbb E[(X\mu_X)^r]$ is a real integral and is used only where it is finite: $r<r^*$ for $S$, and $r=2$ with $\mathbb E[A^2]<\infty$ for $A$. $r^*$ is an extended real.

The queue.

• The queue is the Kiefer–Wolfowitz workload recursion, driven by an initial condition and i.i.d. pairs of inter-arrival and service times.
• An initial condition gives the first-arrival time and the residual service time at each server. No job waits at time $0$.
• "$Q(\infty)$ exists with law $\pi$" quantifies over every initial law of that kind, independent of the inputs. This class is narrower than the paper's, so the hypothesis is weaker and the stated theorem is stronger. The paper's proof uses only such initial conditions (Lemma 7 through Lemma 14).
• $L(\infty)$ is the truncated difference $\max(0,Q(\infty)-n)$.

Renewal processes.

• Counts are natural numbers, computed pathwise from the renewal intervals.
• Bounding families are arbitrary probability spaces carrying mutually independent intervals with the prescribed laws.
• Suprema of processes are taken in the extended reals.

Ruled out. None of the following trivializing formalizations is used:

• a steady-state hypothesis that no queue satisfies, or one restricted to an initial-condition class that drops what Lemma 7 needs;
• a real-valued supremum or infimum, which collapses to $0$ on unbounded families;
• a Bochner moment of a non-integrable function, which is $0$ in Lean.

The infimum over $r$ is stated as a universal quantifier.

Needed infrastructure. Equilibrium distributions and renewal counting processes, moment and maximal inequalities for sums of independent renewal processes, Kingman's exponential martingale bound, and the sample-path comparison of FCFS multi-server queues. Contributions on any of these are welcome: the renewal and random-walk results (Lemmas 5, 6, 8–10) are independent of queueing.

Selected references

• Y. Li and D. A. Goldberg, Simple and explicit bounds for multi-server queues with 1/(1−ρ) scaling, Mathematics of Operations Research, 2025; arXiv:1706.04628v3. https://arxiv.org/abs/1706.04628
• D. Gamarnik and D. A. Goldberg, Steady-state GI/G/n queue in the Halfin–Whitt regime, Annals of Applied Probability 23(6), 2382–2419, 2013. https://doi.org/10.1214/12-AAP905
• S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3), 1981. https://doi.org/10.1287/opre.29.3.567
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24, 383–392, 1962 (ref. [89] of Li–Goldberg).
• J. F. C. Kingman, A martingale inequality in the theory of queues, Mathematical Proceedings of the Cambridge Philosophical Society 60(2), 359–361, 1964 (ref. [90] of Li–Goldberg; the source of Lemma 9).