Statistics

Motivation

Ranking and selection (R&S) is the problem of identifying, by simulation, the alternative with the largest mean performance among $k$ candidates, when each alternative can only be observed with noise. It is a basic tool of simulation optimization, with roots in Bechhofer's indifference-zone formulation (Bechhofer 1954). Cloud and parallel computing have made problems with thousands to millions of alternatives routine, and for such large-scale problems the relevant question is how the total sampling budget must grow with $k$ to keep the probability of correct selection (PCS) from collapsing.

Li, Fan and Hong (arXiv:2303.02951, Management Science 2025) call a procedure sample optimal if a budget linear in $k$, $B=ck$, keeps $\liminf_{k\to\infty}\mathrm{PCS}>0$. Order $k$ is the least any procedure can use, since every alternative needs at least one observation. As the paper recalls, Zhong & Hong (2022) and Hong et al. (2022) show that well-known procedures such as KN (Kim & Nelson 2001) and OCBA (Chen et al. 2000) need a budget of order $k\log k$; the procedures previously proved sample optimal, median elimination (Even-Dar et al. 2006) and the knockout-tournament procedures, rely on a rigid halving structure with carefully planned allocations in each round. The paper's surprising observation is that the simplest procedure of all, the greedy procedure, which always samples the alternative that currently looks best, is already sample optimal.

Setting

There are $k$ alternatives. Alternative $i$ yields independent observations $X_{i1},X_{i2},\dots\sim N(\mu_i,\sigma_i^2)$, independent across alternatives, and alternative $1$ is the unique best: $\mu_1>\mu_i$ for $i\ge2$. Write $\bar X_i(n)=\frac1n\sum_{j=1}^nX_{ij}$ for the running average of alternative $i$.

The greedy procedure (Procedure 1) with total budget $B$:

1. takes one observation from each alternative;
2. while the total number of observations is below $B$, takes one more observation from the alternative with the largest current running average $\bar X_i(n_i)$;
3. selects the alternative with the largest final running average.

The PCS is the probability that alternative $1$ is selected. The asymptotic regime is fixed by Assumption 1: there are constants $\gamma>0$ and $\bar\sigma^2>0$ with $\mu_1-\max_{i\ge2}\mu_i\ge\gamma$ and $\max_i\sigma_i^2\le\bar\sigma^2$, however large $k$ is.

For an i.i.d. $N(0,1)$ sequence with running average $\bar Z(n)$, the crossing time of a level $x$ is $\tilde N(x)=\inf\{n\ge1:\bar Z(n)<x\}$. With $\Phi$ the standard normal distribution function, the paper's key function is

$$C(x)=\exp\Bigl(\sum_{n=1}^\infty\frac1n\,\Phi(-\sqrt n\,x)\Bigr),\qquad x>0,$$

which equals $\mathrm E[\tilde N(x)]$ (Lemma 2). Finally, $\bar X_1^*=\min_{n\ge1}\bar X_1(n)$ is the boundary, $N_1^*$ the first time it is attained, and $N_i(b)=\inf\{n\ge1:\bar X_i(n)<b\}$ the boundary-crossing time of alternative $i$.

Formalization targets

Goal: Theorem 1 (p. 15)

Under Assumption 1, if $B=ck$ with $c>C(\gamma/\bar\sigma)$, then there is $\gamma_0\in(0,\gamma)$ with $C\bigl((\gamma-\gamma_0)/\bar\sigma\bigr)=c$, and

$$\liminf_{k\to\infty}\mathrm{PCS}\ \ge\ \Pr\Bigl\{\min_{n\ge1}\bar X_1(n)>\mu_1-\gamma_0\Bigr\}=\Bigl[C\Bigl(\frac{\gamma_0}{\sigma_1}\Bigr)\Bigr]^{-1}>0.$$

The constant $c$ and the gap $\gamma$ are free; the bound depends only on the shape of $C$.

Milestones

1. Lemma 1 (p. 13): $\Pr\{\arg\min_{n\ge1}\bar Z(n)<\infty\}=1$.
2. Lemma 2 (pp. 13–14): for $x>0$, $\Pr\{\tilde N(x)<\infty\}=1$ and $\mathrm E[\tilde N(x)]=C(x)$, continuous and strictly decreasing; for $x<0$, $\mathrm E[\tilde N(x)]=\infty$ and $\Pr\{\tilde N(x)<\infty\}=1-\exp(-\sum_n\frac1n\Phi(\sqrt n\,x))$; for $x=0$, probability $1$ and infinite mean.
3. (4.3) (p. 14): for $x<0$, $\Pr\{\min_{n\ge1}\bar Z(n)>x\}=[C(-x)]^{-1}$.
4. (3.2) (p. 12): $\mathrm{PCS}\ge\Pr\{\sum_{i=2}^kN_i(\bar X_1^*)+N_1^*\le B\}$.
5. (4.4) (p. 15): on $\{\bar X_1^*>\mu_1-\gamma_0\}$, $N_i(\bar X_1^*)\le\tilde N_i((\gamma-\gamma_0)/\bar\sigma)$, pathwise.
6. (EC.1.5) (p. ec3): $\liminf_k\mathrm{PCS}\ge\Pr\{\min_n\bar X_1(n)>\mu_1-\gamma_\epsilon^-\}-\Pr\{\arg\min_n\bar X_1(n)=\infty\}$, where $C((\gamma-\gamma_\epsilon^-)/\bar\sigma)=c-2\epsilon$.

Significance

The result. Theorem 1 shows that a procedure with no tuning parameters, no elimination and no knowledge of $\gamma$ or $\bar\sigma$ achieves the optimal order of budget growth for large-scale R&S. It gives an explicit, computable lower bound on the limiting PCS. The companion Theorem 2 of the paper shows that this bound is the exact limit under the slippage configuration with a common variance, so the constant cannot be improved in general. The same boundary-crossing analysis underlies the paper's explore-first variant, which turns the positive limit into an arbitrarily high one.

Formalizing it. The result is proved in the paper; nothing here is claimed open. As far as is known, no part of it has a machine-checked proof. A formalization adds:

• a precise, total specification of the greedy procedure as a function of an observation array, including tie-breaking and budget rounding;
• the pathwise inclusion behind (3.2), which the paper argues in prose, and whose naive reading is false before $N_1^*$;
• Spitzer-type identities for the Gaussian random walk (Lemma 2), which Mathlib does not have and which are reusable well beyond this paper.

Difficulty

The obvious argument fails at its first step. The greedy procedure's sample sizes depend on all past observations of all alternatives, so the PCS has no tractable expression, and the classical route through pairwise comparisons at fixed sample sizes does not apply. The boundary-crossing perspective sidesteps this, at three costs. First, (3.2) requires a careful pathwise argument: before the best alternative's running average reaches its minimum, it can lead, be sampled, and lose the lead, so "once best, always best" is false until $N_1^*$. Second, Lemma 2 is a fluctuation-theory identity (Spitzer's formula for the mean ladder epoch of a Gaussian walk), not an elementary computation. Third, the limit $k\to\infty$ combines a strong law over i.i.d. crossing times with a continuity argument in $\gamma_0$, which needs the continuity and strict monotonicity of $C$.

Formalization scope

• Model. One observation array $X_{ij}$ indexed by $i,j\in\mathbb N$, measurable, with $X_{ij}\sim N(\mu_i,v_i)$, and mutually independent as a whole family. Problem $k$ uses alternatives $0,\dots,k-1$; Lean's alternative $0$ is the paper's alternative $1$. One sequence $(\mu_i,v_i)$ serves every $k$, not a triangular array. Variances are positive ($v_i>0$), as the paper's normalizations by $\sigma_i$ require.
• Procedure. A deterministic map from the array to the selected index. Ties in every arg max go to the smallest index (a null event under normality). The budget $B=ck$ is $\lfloor ck\rfloor$; the number of greedy steps uses truncated subtraction, so the procedure is total.
• Quantities. Crossing times and argmins take values in $\mathbb N\cup\{\infty\}$; $\mathrm E[\tilde N(x)]$ is a lower Lebesgue integral in $[0,\infty]$; probabilities and the liminf are in $[0,\infty]$. "$\min_n y(n)>a$" means bounded below with infimum $>a$. $C$ is applied only at positive arguments.
• Ruled out. Crossing times typed in $\mathbb N$ (where an empty infimum is $0$), the junk value of a divergent tsum ($C(x)=1$ for $x\le0$), an unbounded infimum read as $0$, and a "for every $\gamma_0$ with $C(\cdot)=c$" statement that holds vacuously: the goal asserts the existence of $\gamma_0$.
• Infrastructure. Running averages and crossing times of random walks, the Gaussian Spitzer identity, the strong law for i.i.d. $\mathbb N\cup\{\infty\}$-valued variables, and a pathwise analysis of the greedy procedure. The random-walk results are reusable for any boundary-crossing or sequential-testing development. Contributions on any milestone are welcome, and proofs of Lemma 2 by a route other than Siegmund's are equally useful.
• Source. The PDF is the arXiv v3 preprint (11 Dec 2023); every page and equation number refers to it.

Selected references

• Z. Li, W. Fan, L. J. Hong, The (Surprising) Sample Optimality of Greedy Procedures for Large-Scale Ranking and Selection, arXiv:2303.02951v3, 2023; Management Science, 2025. https://arxiv.org/abs/2303.02951
• R. E. Bechhofer, A Single-Sample Multiple Decision Procedure for Ranking Means of Normal Populations with known Variances, Annals of Mathematical Statistics 25(1), 1954. https://doi.org/10.1214/aoms/1177728845
• D. Siegmund, Sequential Analysis: Tests and Confidence Intervals, Springer, 1985. https://doi.org/10.1007/978-1-4757-1862-1
• Y. Zhong, L. J. Hong, Knockout-Tournament Procedures for Large-Scale Ranking and Selection in Parallel Computing Environments, Operations Research 70(1), 2022. https://doi.org/10.1287/opre.2020.2065

Motivation

Online platforms run controlled experiments in which subjects (users, sessions, sellers) arrive one at a time and must be assigned to control or treatment on arrival, before later subjects are seen. A good design makes the two groups look alike in their observed covariates, because covariate imbalance inflates the variance of treatment-effect estimates. Classical offline remedies such as matched-pair designs need all covariates in advance, and the simplest online design, complete randomization, ignores covariates altogether.

Zhao and Zhou (arXiv:2201.12936, Management Science 2025) measure imbalance by the cost of the best one-to-one matching between the treated and the control subjects, which links sequential experimental design to online matching. They propose the pigeonhole design: partition the covariate space into cells and, inside each cell, assign each arrival to the group that is currently short there. This mission formalizes their main upper bound for one continuous covariate.

Setting

A horizon $T$, assumed even, of subjects arrives sequentially. Subject $t$ carries a covariate $x_t\in[0,1]$, and the whole sequence $x=(x_1,\dots,x_T)$ is fixed in advance by an adversary who does not see the randomization (an oblivious adversary). Each subject is assigned, at arrival and irrevocably, to the control group $A$ or the treated group $B$, and in the end $|A|=|B|=T/2$.

The discrepancy of a split is the cost of a minimum-weight perfect matching between the two groups (display (1) of the paper):

$$d_{A,B}=\min_{e:A\to B\ \text{bijective}}\ \sum_{a\in A}|x_a-x_{e(a)}| .$$

The completely randomized design chooses $A$ uniformly among the $\binom{T}{T/2}$ subsets of size $T/2$; its expected discrepancy is written $\mathrm{ALG}^{\mathsf C}(x)$.

A pigeonhole design takes a partition of $[0,1]$ into cells. When subject $t$ arrives: (1) if one group already holds $T/2$ subjects, $t$ joins the other; (2) otherwise, if the cell of $x_t$ currently holds fewer control than treated subjects, $t$ joins control, if fewer treated, $t$ joins treatment, and on a tie a fair coin decides. Its expected discrepancy is the average of $d_{A,B}$ over the coins.

The uniform pigeonholes with parameter $\eta\in(0,1)$ are the $T^{\eta}$ cells $[0,T^{-\eta}),[T^{-\eta},2T^{-\eta}),\dots,[1-T^{-\eta},1]$.

Formalization targets

Goal: Lemma 3

For every fixed $\eta\in(0,1)$ there are $C>0$ and $T_0$ such that, for every even $T\ge T_0$ and every $x\in[0,1]^T$, the pigeonhole design with uniform pigeonholes satisfies

$$\mathbb E\bigl[d_{A,B}\bigr]\ \le\ C\Bigl(T^{\frac12-\frac\eta2}+T^{\frac\eta2}(\log T)^{\frac12}\Bigr).$$

The constant may depend on $\eta$ but on nothing else. Corollary 1, the case $\eta=1/2$ giving $O(T^{1/4}(\log T)^{1/2})$, is included as a separate statement.

Milestones

In attack order:

1. Hoeffding's inequality for a binomial with deviation $\sqrt{n\log n}$ (Lemma EC.1).
2. The value of $\mathrm{ALG}^{\mathsf C}$ on the two-point instance $(0,\dots,0,1,\dots,1)$ (Lemma EC.4, with corrected constant).
3. Permutation invariance of the completely randomized design (Lemma EC.5).
4. $\mathrm{ALG}^{\mathsf C}$ is $\Theta(T^{1/2})$ in the worst case (Lemma 2).
5. Every run of a pigeonhole design is balanced (remark after Definition 3).
6. A median-crossing swap does not decrease the single-cell design's expected discrepancy (Lemma EC.7, corrected).
7. The single-cell design has expected discrepancy $O(T^{1/2})$ (Proposition EC.1).
8. At the stopping time $\tau$, each cell has at most one unmatched subject and $|H^0_\tau-H^1_\tau|=T-\tau$.
9. The subjects matched inside cells contribute $O(T^{1/2-\eta/2})$ (Component 1).
10. The unmatched subjects and the last $T-\tau$ subjects contribute $O(T^{\eta/2}(\log T)^{1/2})$ (Component 2).

Significance

Lemma 3 shows that a simple, time-invariant, covariate-aware online rule beats complete randomization by a polynomial factor: with $\eta=1/2$ the expected discrepancy is $O(T^{1/4}(\log T)^{1/2})$, against $\Theta(T^{1/2})$ for complete randomization (Lemma 2). A companion result of the paper (Lemma 4) shows that no pigeonhole design does better than $\Omega(T^{1/4})$, so the bound is tight up to the logarithm. The same two-component argument underlies the paper's multi-dimensional result.

The paper proves these statements in an e-companion; none is machine-checked. A formalization adds the following. It fixes the exact model behind each expectation, namely an average over coin vectors with the balancing rule included. It repairs the places where the printed argument does not close as written. The printed constant of Lemma EC.4 is wrong, and the stated value here is the corrected one. Lemma EC.7 is false as printed in its strict form and trivial in its weak form, and the stated version is the one the proof actually establishes. The printed proof of Lemma 2 passes through a lemma (EC.6) that is false. Component 2 relies on a conditional binomial law that does not hold literally. A complete development would certify Lemma 3 independently of these slips.

Difficulty

The natural first idea is to bound each cell separately and add the results. This handles subjects that are paired inside their own cell, but it leaves out the balancing rule. Once one group is full, every later subject is forced into the other group regardless of its covariate. These forced subjects can be far from everything they are matched to. The number of forced subjects, $T-\tau$, equals the imbalance among the cells' leftover subjects, which is random and read at a random time. Bounding its expectation requires a concentration argument that is uniform over time.

A second difficulty is the per-cell bound itself. Inside one cell the design pairs consecutive arrivals with random orientation, but the number of pairs in a cell is random and depends on the stopping time. A bound of the form $c\,\ell\sqrt n$ for a cell of length $\ell$ holding $n$ subjects must therefore survive a coin-dependent truncation. Finally, the discrepancy is a minimum over matchings, so every upper bound must exhibit a matching, and every comparison between instances (Lemma EC.7) is an exchange argument over all coin outcomes.

Formalization scope

All statements live in the namespace PigeonholeDesign.Upper, and the conventions are fixed as follows:

• Time and assignments. Subjects are indexed by Fin T, from $0$, so the paper's subject $t$ is index $t-1$, and its odd index $i$ is an even 0-based position. An assignment is Fin T → Bool, with true meaning treated.
• Discrepancy. The minimum over bijections between the two groups of the summed distances, which equals the assignment problem (1). When the groups differ in size this infimum is Lean's junk value $0$. The balance milestone shows that the designs never produce such a split.
• Randomness. The pigeonhole design is run on a coin vector in $\{0,1\}^T$, and coin $t$ is read only when subject $t$ meets a tie. Every expectation is the average over all $2^T$ coin vectors (respectively over all $\binom{T}{T/2}$ control sets), never one run or the best run.
• Partition. The printed partition has $T^{\eta}$ cells, which is not an integer in general. It is pinned as $K=\lceil T^{\eta}\rceil$ equal cells of length $1/K\le T^{-\eta}$, with the last cell closed. This coincides with the printed one when $T^\eta$ is an integer.
• Asymptotics. "$O(f(T))$" means that there exist $C>0$ and $T_0$, chosen before $T$ and $x$, depending only on $\eta$ (an absolute $C$ where the page says "absolute constant"). "$\Theta$" means both bounds. The logarithm is natural.
• Corrected statements. Lemma EC.4 uses $1/\sqrt{2\pi}$ in place of the printed $1/\sqrt\pi$. Lemma EC.7 is the non-strict inequality for the specific swap of positions $i+1$ and $j+1$. Component 2 states only its conclusion. Lemma EC.6 is not posed.

Several formalizations would make the statements easy for the wrong reason, and the statements rule them out. The junk value $0$ of an unbalanced split never applies, because the designs are balanced. A bound on a single run, or on the best run, in place of the average over all coin vectors is not the claim. Constants may not depend on $T$ or $x$. The partition is fixed, and the statements do not range over arbitrary partitions.

A complete development needs:

• finite combinatorics of the design run;
• one-dimensional matching (on the line the sorted matching is optimal);
• binomial and hypergeometric tail and mean-absolute-deviation estimates;
• a central-binomial asymptotic for Lemma EC.4.

The design definitions and the balance lemma are reusable by the paper's lower-bound and multi-dimensional missions. Contributions of any milestone, of alternative proofs that bypass the faulty printed steps, and of sharper constants are welcome.

Selected references

• J. Zhao and Z. Zhou, Pigeonhole Design: Balancing Sequential Experiments from an Online Matching Perspective, arXiv:2201.12936v6 (2024); Management Science (2025). https://arxiv.org/abs/2201.12936
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830
• C. R. Blyth, Expected absolute error of the usual estimator of the binomial parameter, The American Statistician 34 (1980) 155–157. https://doi.org/10.1080/00031305.1980.10483022
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific (1997), Chapter 7.8 (assignment problem).

Motivation

Online marketplaces (ride hailing, delivery, freelancing, retail supply chains) test changes to their product with randomized controlled trials: a fraction $\rho$ of the arriving customers is treated, the rest is kept as control, and the difference in outcomes is scaled up to estimate what would happen if everybody were treated. In a market with limited supply this estimate is biased. Treated and control customers compete for the same drivers or the same inventory, so the outcome of one group depends on the size of the other. This effect is called marketplace interference, and it makes the standard estimator overstate the effect of a treatment.

Bright, Delarue and Lobel (arXiv:2205.02274v4) model the platform's matching decision as a linear program and propose to estimate the treatment effect from the shadow prices of that program, which measure the marginal value of one more unit of demand of each type. This mission formalizes their fluid-limit comparison between the standard RCT estimator and the shadow-price estimator: in a symmetric experiment, the shadow-price estimator is never more biased.

Setting

A matching network is a finite directed graph with one demand node $u^d_i$ for each demand type $i\in[n_d]$ (only incoming arcs), one supply node $u^s_j$ for each supply type $j\in[n_s]$ (only outgoing arcs), and intermediate nodes. Each arc $(u,w)$ has a value $v_{u,w}\in\mathbb R$ per unit of flow and a capacity $k_{u,w}\ge0$. Given a demand vector $d$ and a supply vector $s$, the platform solves the LP (2)

$$\Phi(d,s)=\max\sum_{(u,w)}v_{u,w}x_{u,w}$$

over arc flows $x$ with $0\le x\le k$, flow into each $u^d_i$ at most $d_i$, flow out of each $u^s_j$ at most $s_j$, and flow balance at each intermediate node. Its dual (5) has a nonnegative price $a_i$ for each demand constraint, a price $b_j$ for each supply constraint, a price $\xi_{u,w}$ for each capacity and a free potential at each intermediate node. The price $a_i$ is the shadow price of demand type $i$.

Demand arrives at rate $\lambda\ge0$ under global control and at rate $\lambda+\beta\ge0$ under global treatment; supply arrives at rate $\pi\ge0$. An experiment treats a fraction $\rho\in(0,1)$ of demand, so the platform observes the market at the intermediate rate $\lambda+\rho\beta$. The partial-treatment value function is $\Psi(\eta)=\Phi(\lambda+\eta\beta,\pi)$ for $\eta\in[0,1]$, and the global treatment effect in the fluid limit is

$$\Delta=\Psi(1)-\Psi(0)=\Phi(\lambda+\beta,\pi)-\Phi(\lambda,\pi).$$

Two estimators are computed from the experiment state alone. The RCT estimator is $\hat\Delta_{\mathrm{RCT}}=\bar v^*\cdot\beta$, where $\bar v^*_i$ is the average value per unit of type-$i$ demand in the optimal flow of $\Phi(\lambda+\rho\beta,\pi)$, computed along the supply-to-demand paths that carry it ((9)–(10)). The shadow-price estimator is $\hat\Delta_{\mathrm{SP}}=a^\rho\cdot\beta$, where $a^\rho$ is the demand part of the optimal dual solution of $\Phi(\lambda+\rho\beta,\pi)$ ((11)). Two assumptions stand throughout: the optimal primal and dual solutions of $\Phi(\lambda+\rho\beta,\pi)$ are unique (Assumption 2), and $\beta$ is sign-consistent, $\beta\ge0$ or $\beta\le0$ componentwise (Assumption 3).

Formalization targets

Goal: Theorem 4 (p. 21)

In a symmetric experiment, $\rho=\tfrac12$,

$$\bigl|\hat\Delta_{\mathrm{SP}}-\Delta\bigr|\ \le\ \bigl|\hat\Delta_{\mathrm{RCT}}-\Delta\bigr|.$$

The statement fixes no constant other than the symmetric design. It holds for every network, every admissible rate vector and every path decomposition of the optimal flow.

Milestones

• Proposition 1 (p. 13): $\Psi$ is concave and piecewise linear with finitely many pieces on $[0,1]$.
• Theorem 2 (p. 14): if $\beta\ge0$, then $\bar v^*\cdot(\lambda+\beta)\ge\Psi(1)$ and $\bar v^*\cdot\lambda\le\Psi(0)$, with the reverse inequalities if $\beta\le0$. Consequently $|\hat\Delta_{\mathrm{RCT}}|\ge|\Delta|$.
• Proposition 6 (p. 21): $\Psi'(\eta)=a^\eta\cdot\beta$ off finitely many points, and $\Delta=\int_0^1a^\eta\cdot\beta\,d\eta$.

Companion results

• Theorem 9 (p. 27): for $\rho<\tfrac12$ and $\beta\le0$, the estimator $\hat\Delta_{\mathrm{SP+}}=(1-2\rho)\hat\Delta_{\mathrm{RCT}}+2\rho\hat\Delta_{\mathrm{SP}}$ is no more biased than $\hat\Delta_{\mathrm{RCT}}$.
• Theorem 10 (p. 27): for any $\rho$, if $(\bar v^*-a^0)\cdot\beta\ge(a^0-a^1)\cdot\beta$, then $\mathrm{Bias}_{\mathrm{SP}}\le\mathrm{Bias}_{\mathrm{RCT}}$; if $(a^0-a^1)\cdot\beta=0$, then $\mathrm{Bias}_{\mathrm{SP}}=0$.

Significance

Theorem 4 says that a platform running a 50/50 experiment never does worse by replacing the average value $\bar v^*$ with the marginal value $a^\rho$. The comparison does not depend on the network, on the capacities, or on how strongly treatment and control interfere. Theorem 2 shows that the standard estimator is biased in a known direction, and Theorem 4 shows that a different use of the same experiment data reduces that bias. The SP estimator needs only the dual solution of an LP the platform already solves.

All results of this mission are proved in the paper (Appendix C), and none has a machine-checked proof. The milestones are statements about parametric linear programs: concavity and piecewise linearity of the optimal value in the right-hand side, and the identification of its derivative with the optimal dual. These hold well beyond this paper and are absent from the platform.

Difficulty

Two steps resist the naive argument. The bound $\bar v^*\cdot\lambda\le\Psi(0)$ needs a feasible flow for the control market built from the experiment's optimal flow. Scaling the arc flow does not give one, because types share arcs. The flow has to be scaled path by path and type by type, which is why $\bar v^*$ is defined through paths. The identification $\Psi'(\eta)=a^\eta\cdot\beta$ needs LP sensitivity analysis in a parametric right-hand side: strong duality at every $\eta$, and the fact that dual optima are supergradients of $\Psi$. Because $\Psi$ has kinks, the identification holds only off finitely many points. Finally, a pointwise comparison of $a^\rho$ with $\bar v^*$ does not give Theorem 4. The proof compares integrals of $a^\eta\cdot\beta$ over $[0,\rho]$ and $[\rho,1]$, and the symmetric design is what balances the two sides.

Formalization scope

Everything is defined in MarketInterference.FluidBias. The network is a structure with arcs E and intermediate nodes I, both finite. An arc's tail is a supply node or an intermediate node, and its head is a demand node or an intermediate node, so the sink and source convention holds by construction. Demand types are Fin nd, and Lean index $i$ is the paper's type $i+1$. $\Phi$ is the supremum of the objective over the feasible set. For $d,s\ge0$ that set contains $0$ and lies in the box $[0,k]$, so the supremum is a maximum. The dual (5) is encoded arc by arc, and the four printed constraint families (5b)–(5e) are its four tail/head cases. Optimality of a primal or dual solution is stated explicitly. Strong duality is not assumed.

The estimators are the right-hand sides of (9)–(11). They are computed from an optimal primal flow, one of its path decompositions, and an optimal dual solution of the experiment LP. Neither is defined from $\Psi$ or from its derivative. A formalization that defined $\hat\Delta_{\mathrm{SP}}$ as $\Psi'(\rho)$, or $\hat\Delta_{\mathrm{RCT}}$ through $\Psi$, would trivialize the goal and is ruled out. With intermediate nodes, the decomposition of the optimal flow into paths, which (10) treats as given, is not unique. The theorems therefore hold for every decomposition. Paths are lists of distinct arcs. In (10), a type with $\lambda_i+\rho\beta_i=0$ has $\beta_i=0$, and Lean's $x/0=0$ makes its term vanish. Assumption 2 is stated as uniqueness of the whole optimal primal flow and of the whole dual solution $(a,b,m,\xi)$, as printed. Assumption 3 is a disjunction of the two sign conditions. Assumption 1 (random tie-breaking) concerns only the finite random market and is not added. The limits in Corollary 1 and Propositions 2 and 5 are not needed here: $\Delta$, $\hat\Delta_{\mathrm{RCT}}$ and $\hat\Delta_{\mathrm{SP}}$ are defined directly in the fluid model. Proposition 6's derivative is stated with HasDerivAt off a finite set, and its dual selection $\eta\mapsto a^\eta$ is arbitrary. The statements follow arXiv:2205.02274v4. Its printed slips are corrected as disclosed: the ill-defined $y^*$ of (10) is read as any path decomposition, and "$u^s_i$" on p. 9 is read as $u^d_i$.

A complete development needs LP strong duality and complementary slackness for this network LP, parametric-LP results (concavity and piecewise linearity of the optimal value along a ray, and dual optima as supergradients), path decompositions of flows, and the fundamental theorem of calculus for piecewise linear functions. The parametric-LP layer can be reused for any LP-based value function. Proofs of any milestone are welcome, as are general lemmas on network LPs.

Selected references

• I. Bright, A. Delarue, I. Lobel, Reducing Marketplace Interference Bias Via Shadow Prices, arXiv:2205.02274v4, 2024; Management Science, 2025. https://arxiv.org/abs/2205.02274
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 5 (sensitivity analysis; Theorem 5.1).
• R. Johari, H. Li, I. Liskovich, G. Y. Weintraub, Experimental Design in Two-Sided Platforms: An Analysis of Bias, Management Science, 2022 (cited by the paper as [Johari et al. 2022]). https://arxiv.org/abs/2002.11142

Learning many related regressions at once

Service providers such as hospitals or retail stores each fit a predictive model on their own data, and many of them have few observations. The models of different providers are usually similar but not identical: most coefficients agree, while each provider deviates from the common model in a few features of its own. Multitask learning asks how data from all providers can be pooled to estimate every provider's model better than it could estimate alone, without being misled by the providers that differ.

Xu and Bastani (arXiv:2112.14233v5) model this with sparse heterogeneity: every task parameter is a shared vector plus a sparse deviation. They propose the robust multitask estimator (RMEstimator), which combines per-task least-squares estimates by a coordinatewise trimmed mean and then corrects each task by a LASSO regression centred at that shared estimate. Their main fixed-design guarantee, Proposition 5, is a high-probability bound on the $\ell_1$ estimation error of each task. The same estimator drives the paper's multitask contextual bandit algorithm (§5), whose regret analysis rests on this bound. The approach builds on transfer learning with a single proxy model (Bastani 2021) and on the robustness of the trimmed mean to corrupted samples (Lugosi and Mendelson 2021).

The model and the estimator

There are $N$ tasks. Task $j\in[N]$ has $n_j\ge1$ observations, a fixed design matrix $X^j\in\mathbb R^{n_j\times d}$ whose columns satisfy the normalization $\frac1{n_j}\|X^j_{(\cdot,i)}\|_2^2=1$ (equation (1)), and responses

$$Y^j=X^j\beta^j+\epsilon^j,\qquad \beta^j=\beta^\dagger+\delta^j,\qquad \|\delta^j\|_0\le s .$$

The noise terms $\epsilon^j_k$ are mutually independent across all tasks and observations, and each is $\sigma_j$-subgaussian with mean zero: $\mathbb E[e^{\lambda\epsilon^j_k}]\le e^{\sigma_j^2\lambda^2/2}$ for all $\lambda\in\mathbb R$. Assumption 1 asks that the sample covariance matrices $\widehat\Sigma^j=X^{j\top}X^j/n_j$ satisfy $\lambda_{\min}(\widehat\Sigma^j)\ge\psi>0$.

Given a trimming level $\omega$ and regularization levels $\lambda_j$, Algorithm 1 computes:

1. the OLS estimates $\widehat\beta^j_{\mathrm{ind}}=(X^{j\top}X^j)^{-1}X^{j\top}Y^j$;
2. the shared estimate $\widehat\beta^\dagger_{\mathrm{RM},(i)}=\mathrm{TrimmedMean}(\{\widehat\beta^j_{\mathrm{ind},(i)}\}_{j\in[N]},\omega)$ for each coordinate $i$, where the trimmed mean sorts the $N$ values, discards the $N\omega$ smallest and the $N\omega$ largest, and averages the rest;
3. for each task, $\widehat\beta^j_{\mathrm{RM}}\in\arg\min_\beta\big\{\frac1{n_j}\|X^j\beta-Y^j\|_2^2+\lambda_j\|\beta-\widehat\beta^\dagger_{\mathrm{RM}}\|_1\big\}$.

A coordinate $i$ is $\zeta$-poorly-aligned, $i\in\mathcal I^\zeta_{\mathrm{poor}}$, if fewer than a fraction $\zeta$ of the tasks satisfy $\beta^j_{(i)}\neq\beta^\dagger_{(i)}$; otherwise it is $\zeta$-well-aligned (Definition 2).

Formalization targets

Goal: Proposition 5

For every constant $C_0>2$, every $0<\zeta<1/2$, every $0<\eta\le 1/2-1/C_0-\zeta$, every task $j$ and every $\lambda_j>0$, every output of Algorithm 1 with $\omega=\zeta+\eta$ satisfies

$$\|\widehat\beta^j_{\mathrm{RM}}-\beta^j\|_1\le\frac{6\lambda_js}{\zeta\psi}+4C_0\,d\,(3\zeta+4\eta)\max_{i\in[N]}\sqrt{\frac{\sigma_i^2}{n_i\psi}\log\frac3\eta}$$

with probability at least $1-\big(3d\,e^{-N\eta^2/9}+2d\,e^{-\lambda_j^2n_j/(32\sigma_j^2)}\big)$.

The printed Proposition 5 (p. 17) has $C_0$ where this statement has $4C_0$. The proof on pp. 41–43 ends with $\|\widehat\beta^j_{\mathrm{RM}}-\beta^j\|_1\le 6s\lambda_j/(\zeta\psi)+4\|(\widehat\beta^\dagger_{\mathrm{RM}}-\beta^\dagger)_{\mathcal I_{\mathrm{poor}}}\|_1$ and combines it with (16), whose coefficient is $C_0$, so it establishes the bound with $4C_0$. The goal is the bound the proof supports.

Milestones, in proof order

1. (6): $|\mathcal I^\zeta_{\mathrm{well}}|\le s/\zeta$.
2. Proposition 4: the trimmed mean of $N$ samples, fewer than $\zeta N$ of them arbitrarily corrupted and the rest independent and subgaussian, has $\mathbb P[|\widehat\mu-\mu|\ge C_0\max_{j\in\mathcal J^c}\sigma_j(3\zeta+4\eta)\sqrt{\log(3/\eta)}]\le 3e^{-N\eta^2/9}$.
3. Lemma 1: $\mathbb P[\tfrac2{n_j}\|X^{j\top}\epsilon^j\|_\infty\le\lambda_j/2]\ge1-2d\,e^{-\lambda_j^2n_j/(32\sigma_j^2)}$.
4. OLS subgaussianity (p. 41): each $\widehat\beta^j_{\mathrm{ind},(i)}$ is $\sqrt{\sigma_j^2/(n_j\psi)}$-subgaussian with mean $\beta^j_{(i)}$.
5. (16): the shared estimate is accurate on $\mathcal I_{\mathrm{poor}}$ with probability $1-3d\,e^{-N\eta^2/9}$.
6. (19): the LASSO cone inequality on the event of Lemma 1.
7. Final display of p. 43: $\|\widehat\beta^j_{\mathrm{RM}}-\beta^j\|_1\le 6s\lambda_j/(\zeta\psi)+4\|(\widehat\beta^\dagger_{\mathrm{RM}}-\beta^\dagger)_{\mathcal I_{\mathrm{poor}}}\|_1$ on that event.

Significance

Proposition 5 separates two error sources: a LASSO term of order $s\lambda_j$, which depends only on the task's own sample size, and a trimmed-mean term that shrinks with the number of tasks through $\max_i\sqrt{\sigma_i^2/n_i}$. With the hyperparameters of Appendix A.2 it yields Theorem 1, an error of order $\sqrt{sd/n_j}+d/\sqrt{Nn_j}$ up to logarithmic factors, against $d/\sqrt{n_j}$ for a single task alone. The same decomposition underlies the paper's data-poor guarantee (Proposition 8) and the regret bounds of its multitask bandit algorithm.

The result is proved on paper; none of it has been machine-checked. A formal development checks the constant bookkeeping, including the factor 4 that the printed statement omits, and the use of the trimmed mean for samples that are independent but not identically distributed, which is where this paper departs from the classical i.i.d. robust-statistics results. Proposition 4 and Lemma 1 are reusable on their own: a corruption-robust concentration bound for the trimmed mean and a noise bound for fixed-design LASSO.

Difficulty

The obvious estimator of the shared parameter, the average of the per-task estimates, converges to the average of the $\beta^j$, which differs from $\beta^\dagger$ in up to $\min\{Ns,d\}$ coordinates, so the LASSO correction would have to undo a dense bias. The trimmed mean avoids this only on poorly-aligned coordinates, and only with high probability. The proof of Proposition 4 must control the samples that survive trimming even though they are not identically distributed and trimming biases the conditional means; that step needs a moment bound for subgaussian variables and a Hoeffding argument on a random index set. The LASSO step needs the cone inequality with a support $\bar{\mathcal I}_j=\mathcal I_{\mathrm{well}}\cup\mathcal I_j$ that is not the support of $\beta^j-\beta^\dagger$, and the counting bound (6) to control its size.

Formalization scope

• Tasks, coordinates and observations are Fin N, Fin d, Fin (n j); paper index $i$ is Lean i − 1. Designs are deterministic matrices; only the noise is random.
• Definition 1 with mean zero is Mathlib's HasSubgaussianMGF with variance proxy $\sigma_j^2$, $\sigma_j>0$. Independence of all noise terms is iIndepFun over the pairs $(j,k)$.
• Sparsity is $\|\beta^j-\beta^\dagger\|_0\le s$ with $\delta^j=\beta^j-\beta^\dagger$. The model requires $n_j\ge1$.
• $\lambda_{\min}(\widehat\Sigma^j)\ge\psi$ is written $v^\top\widehat\Sigma^jv\ge\psi\|v\|_2^2$ for all $v$.
• $\|\cdot\|_1$, $\|\cdot\|_\infty$, $\|\cdot\|_0$ and $\beta_I$ are explicit finite sums, suprema, counts and restrictions. $\log$ is the natural logarithm.
• The trimmed mean removes $\lfloor N\omega\rfloor$ values from each end and divides by the number kept; this is the paper's formula whenever $N\omega\in\mathbb N$.
• The LASSO step is the predicate "is a global minimizer", never a choice function, and $\lambda_j$ is the parameter (the initialization $\lambda_j=\lambda/\sqrt{n_j}$ is not imposed). The OLS inverse is Lean's matrix inverse, which Assumption 1 makes a genuine inverse.
• "With probability at least $1-p$" is: the outer probability of the failure event is at most $p$. The constant $C_0>2$ is universally quantified, and the trimming level is $\omega=\zeta+\eta$ wherever the paper fixes it.
• The deterministic milestones (19) and the final display of p. 43 are stated for an arbitrary centre $b$ in place of $\widehat\beta^\dagger_{\mathrm{RM}}$; their proofs use no property of it.

A formalization that drops Assumption 1 (making the OLS inverse a junk zero), lets the corrupted samples of Proposition 4 be independent or well-behaved, fixes a single $C_0$ existentially, or reads a junk minimizer from Classical.choose, does not state the paper's result.

The development needs least-squares algebra for fixed designs, a Hoeffding bound for independent bounded variables, moment bounds for subgaussian variables, and the LASSO basic inequality. Proofs of any milestone are welcome, and so are alternative arguments for Proposition 4 with better constants.

Selected references

• K. Xu and H. Bastani, Multitask Learning and Bandits via Robust Statistics, arXiv preprint, v5, 2024. https://arxiv.org/abs/2112.14233
• G. Lugosi and S. Mendelson, Robust multivariate mean estimation: the optimality of trimmed mean, Annals of Statistics, 2021. https://arxiv.org/abs/1907.11391
• H. Bastani, Predicting with Proxies: Transfer Learning in High Dimension, Management Science, 2021. https://arxiv.org/abs/1812.11097
• P. Bühlmann and S. van de Geer, Statistics for High-Dimensional Data, Springer, 2011. https://doi.org/10.1007/978-3-642-20192-9
• R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society B, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x

Motivation

Personalized decisions — which drug to prescribe, which product to recommend, which price to quote — are made one user at a time, from user features observed on arrival, and the effect of each decision is learned only from the users it was applied to. This is the contextual (covariate) bandit. In electronic records and online platforms the feature vector is high-dimensional, often with more coordinates than there will ever be users, while the outcome is binary or count-valued, so a linear reward model is a poor fit. Wang, Wei and Yao (arXiv:1812.02962, published in Management Science, 2025) combine three ingredients: a generalized linear model (GLM) for rewards, sparsity of the parameter vectors, and the minimax concave penalty (MCP) of Zhang (2010) for estimation.

Timeline. Goldenshluger and Zeevi (2013) obtained $O(\log T)$ regret for a two-armed linear bandit with low-dimensional covariates, under a margin condition, and showed it is the right order. Bastani and Bayati (2020) extended the setting to high-dimensional sparse linear rewards with the LASSO, obtaining $O(s_0^2\log^2 T)$ regret. Wang, Wei and Yao (2018 preprint) treat GLM rewards with the MCP and claim $O(|\mathcal K|s^2(s+\log d)\log T)$, recovering the $\log T$ order in the high-dimensional setting.

Setting

At each time $t=1,2,\dots$ a user with covariate vector $x_t\in\mathcal X\subseteq\mathbb R^d$ arrives; the $x_t$ are i.i.d. with an unknown law $\mathcal P_x$. The decision-maker chooses a decision $\pi_t\in\mathcal K=\{1,\dots,K\}$, $K\ge2$, and observes only the reward of that decision.

The reward of decision $k$ at covariate $x$ has law $g(r\mid x^\top\beta_k)\,\nu(dr)$, where $\nu$ is a known base measure on $[-R_{\max},R_{\max}]$, $g(\cdot\mid\eta)$ a known density, and $\beta_k\in\mathbb R^d$ an unknown sparse parameter: its support $\mathcal S_k$ has at most $s$ elements. Write $f(r\mid\eta)=-\log g(r\mid\eta)$ and $\mu(\eta)=\int r\,g(r\mid\eta)\,d\nu(r)$, so the expected reward is $\mu(x^\top\beta_k)$. The Bernoulli–logistic model is $\nu=\delta_0+\delta_1$, $\mu(\eta)=1/(1+e^{-\eta})$.

The cumulative regret compares the decisions with the oracle that knows every $\beta_k$:

$$R^C(T)=\sum_{t=1}^T\mathbb E\Big[\max_k\mu(x_t^\top\beta_k)-\mu(x_t^\top\beta_{\pi_t})\Big].$$

The G-MCP-Bandit algorithm has inputs $t_0,h,\lambda_{1,0},\lambda_{2,0},a$. At time $t$, with probability $\min\{1,t_0/t\}$ it explores: it plays a uniformly random decision (ε-decay random sampling). Otherwise it forms a shortlist $\Pi_t$ of the decisions whose estimated mean reward, under the random-sample estimates $\beta^{random}_k$ (trained on exploration data only), is within $h/2$ of the best; it then plays the decision of $\Pi_t$ with the largest estimated mean under the whole-sample estimates $\beta^{whole}_k$ (trained on all data of $k$). Both estimates are computed by the 2-step weighted Lasso (2sWL): an $\ell_1$-penalized maximum likelihood fit with weights $\lambda$, then a refit whose weights $w_j=\max(0,\lambda-|\beta_{1,j}|/a)$ are the MCP derivatives at the first fit, both over the ball $\|\beta\|_1\le b$, with the anytime schedules $\lambda_1(t)=\lambda_{1,0}\sqrt{1+\log d/\log(t+1)}$ and $\lambda_2(t)=\lambda_{2,0}\sqrt{(\log(t+1)+\log d)/(t+1)}$.

The paper assumes A.1 (bounded covariates, rewards and parameters; $\beta_{\min}$ lower-bounds the nonzero coefficients), A.2 (margin: $\mathbb P(0<|\mu(x^\top\beta_i)-\mu(x^\top\beta_j)|\le\gamma)\le CR_{\max}\gamma$), A.3 (every decision is either $h$-suboptimal everywhere or $h$-optimal on a region $U_k$ of probability at least $p^*$), A.4 (a restricted eigenvalue condition with constant $\kappa$ for samples in $U_k$) and A.5 (smoothness and convexity of $f$ with derivative bounds $\sigma,\sigma_2,\sigma_3$).

Formalization targets

Goal: Theorem 1 (p. 15)

For every $a\ge2304s/(\kappa p^*)$ there are constants $C_0\ge10$ and $C_4,C_5,T_0,C_\beta>0$, independent of $T$, such that with $t_0=2C_0|\mathcal K|$, $\lambda_{1,0}=C_5$, $\lambda_{2,0}=C_4$, for every $T\ge T_0$,

$$R^C(T)\le R_{\max}(T_0+|\mathcal K|)+\Big(6R_{\max}|\mathcal K|C_0+41R_{\max}|\mathcal K|+2e^{4\sigma_2x_{\max}b}CR_{\max}^3|\mathcal K|x_{\max}^2C_\beta s^3\Big)\log(T+1).$$

The goal keeps every explicit coefficient of the page and leaves the constants the paper calls "independent of $T$" existential.

Milestones

In the order the proof of Theorem 1 (pp. ec5–ec8) uses them:

1. Proposition 2 (p. 13): the exploration count $n_k$ is between $C_0(1+\log(T+1)-\log(t_0+1))$ and $3C_0(1+\log T-\log t_0)$ with probability $\ge1-2/(T+1)$.
2. Lemma EC.8, statements 2 and 3 (p. ec16): enough exploration samples of an optimal decision fall in its region $U_k$.
3. Proposition 4 (p. 18): $\|\beta^{random}_k(T)-\beta_k\|_1\le\min\{1/(\sigma_2x_{\max}),h/(4e\sigma_2R_{\max}x_{\max})\}$ with probability $\ge1-15/(T+1)$.
4. Lemma EC.10 (p. ec20): a Lipschitz bound for $\mu$, and the $h/2$ separation it implies on $U_i$.
5. Proposition 6 (p. 19): $\|\beta^{whole}_k(T)-\beta_k\|_2\le\sqrt{C_\beta s^2/(T+1)}$ with probability $\ge1-13/(T+1)$.

Significance

Theorem 1 says that, under the stated assumptions, learning with high-dimensional GLM rewards costs regret logarithmic in the horizon, the order known to be unavoidable already for low-dimensional linear bandits. It improves the $\log^2T$ of the LASSO bandit and shows how a non-convex penalty, computed by two convex weighted-Lasso solves, can be analysed under the non-i.i.d. sampling that a bandit induces. Propositions 4 and 6 are estimation results of independent interest: tail bounds for an MCP estimator trained on random and on adaptively collected samples.

The result is proved on paper; it is not formalized anywhere. The mission produces a machine-checked statement of the full algorithm and its regret, and the milestones isolate reusable facts: an exploration-count bound for ε-decay sampling, a Lipschitz bound for GLM means, and the estimator tail bounds. Alternative arguments and sharper constants are welcome as separate theorems.

Difficulty

The whole-sample data are not i.i.d.: which samples decision $k$ receives depends on the past estimates. Standard high-dimensional estimation results (restricted eigenvalue arguments for the Lasso or MCP) assume i.i.d. designs, and so does the analysis of the oracle estimator. The obvious argument — apply the i.i.d. result to $\beta^{whole}$ — fails at this step. The paper instead extracts an i.i.d. subsample, the exploration samples in $U_k$, and controls the rest through a martingale count. A second difficulty is that the MCP objective is non-convex; the 2sWL estimate must be shown to coincide with the oracle estimator, which requires a minimum signal strength $\beta_{\min}$ and a sufficiently large $a$.

Formalization scope

Covariates are Fin d → ℝ with $d\ge1$, decisions are Fin K with $K\ge2$ (the paper's decision $k$ is k.val + 1), times are $t\ge1$. Norms are explicit sums. Pinned readings, all disclosed in the items:

• The reward family is a base measure $\nu$ concentrated on $[-R_{\max},R_{\max}]$ with a jointly measurable, positive, normalized density $g$; $\mathbb E[R_k\mid x,\beta]=\mu(x^\top\beta)$.
• A.5's derivatives are in the linear predictor $\eta$, bounded for $|\eta|\le bx_{\max}$; smoothness is ContDiff ℝ ∞.
• Both weighted-Lasso steps minimize over $B_b=\{\|\beta\|_1\le b\}$ (A.1's "all feasible β").
• A.3's "every $x$" means every $x\in\mathcal X$; A.4 is required for $k\in\mathcal K_o$ only.
• Exploration is driven by exogenous coins $V_t\sim\mathrm{Unif}[0,1]$ and uniform draws $A_t$, independent of the covariates and rewards. The rewards of different decisions at the same time may be dependent.
• The algorithm uses the box's anytime $\lambda_1(t),\lambda_2(t)$, with $\lambda_{1,0}=C_5$, $\lambda_{2,0}=C_4$.
• Propositions 4 and 6 are stated for $k\in\mathcal K_o$, with the algorithm parameters and the threshold on $T$ that Lemma EC.9 supplies. Lemma EC.10 adds the bound $|f'|\le\sigma_2$ its proof uses.

Trivializing formalizations are ruled out: the estimates are minimizers of the stated objective over $B_b$ (not arbitrary functions), the selection and tie-breaking rules are measurable (otherwise every expectation would be the junk value $0$), and every existential constant comes before the probability space, the rules and $T$, so that $C_\beta$ and $T_0$ cannot depend on the horizon. The trailing $O(|\mathcal K|s^2(s+\log d)\log T)$ and the explicit lower bound on $T_0$ are not formalized.

A complete development needs a measurable argmin selection over a compact ball, Chernoff bounds for sums of independent non-identical Bernoulli variables, differentiation under the integral for GLM means, a restricted-eigenvalue oracle inequality for the weighted Lasso with GLM loss, and a martingale concentration bound. The first three are reusable beyond this mission. Contributions on any milestone are welcome.

Selected references

• X. Wang, M. M. Wei and T. Yao, Online Learning and Decision-Making under Generalized Linear Model with High-Dimensional Data, arXiv preprint, 2018 (Management Science, 2025). https://arxiv.org/abs/1812.02962
• H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1), 2020. https://doi.org/10.1287/opre.2019.1902
• A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1), 2013. https://doi.org/10.1287/11-SSY032
• C.-H. Zhang, Nearly Unbiased Variable Selection under Minimax Concave Penalty, Annals of Statistics 38(2), 2010. https://doi.org/10.1214/09-AOS729

Motivation

Many operational risk questions ask for a small probability $p_u=P(L(X)\ge u)$: the chance that the cost $L$ of a decision, evaluated at a random scenario $X\in\mathbb R^d$, exceeds a large threshold $u$. Examples are large delays in project networks or vehicle routing, large portfolio credit losses, and failures in engineered systems. Plain Monte Carlo needs on the order of $p_u^{-1}$ samples to estimate $p_u$ to fixed relative accuracy, which is prohibitive when $p_u$ is $10^{-6}$ or smaller. Importance sampling (IS) draws samples from a different distribution and reweights them by a likelihood ratio, but classical efficient IS schemes are built for one model at a time: they need the distribution of $X$ and the structure of $L$ (e.g. linearity or convexity) to solve for a good sampling distribution.

Deo and Murthy (arXiv:2102.07060v3, published in Operations Research, 2025) propose a self-structuring sampler that needs neither: it applies a fixed multiplicative stretching to ordinary samples of $X$ and uses only black-box evaluations of $L$. Their main result is that this sampler is asymptotically optimal in the standard sense of logarithmic efficiency (Asmussen and Glynn 2007, Ch. 6) over a nonparametric class of light- and Weibull-type-tailed distributions and nonconvex losses.

Setting

Write $\mathbb R^d_+=\{x:x\ge0\}$ and $\mathbb R^d_{++}=\{x:x>0\}$ (componentwise), and $\|x\|=\max_i|x_i|$. The random vector $X=(X_1,\dots,X_d)$ has density $f_X$. Its marginal cumulative hazards are $\Lambda_i(x)=-\log P(X_i>x)$, $\Lambda(x)=(\Lambda_1(x_1),\dots,\Lambda_d(x_d))$, and $Y=\Lambda(X)$ is the standardized vector. Let $q_i=\Lambda_i^{\leftarrow}$ be the left-continuous inverse, $q(y)=(q_1(y_1),\dots,q_d(y_d))$, $\hat q(t)=q(t\mathbf 1)/\|q(t\mathbf 1)\|$ and $\Lambda_{\min}(u)=\min_i\Lambda_i(u)$.

The standing assumptions are:

• Assumption 2.1 on the loss: risk sets $\{x\in\operatorname{supp}X: L(x)\ge u\}$ lie in $\mathbb R^d_+$ for large $u$, and $L(nx_n)/n^\rho\to L^*(x)$ for every $x_n\to x$ in $\mathbb R^d_+$, with $\rho>0$ and $L^*>0$ somewhere on $\mathbb R^d_+$.
• Assumption 3.1 on the marginals: each $\Lambda_i$ is continuous, eventually strictly increasing, and regularly varying with index $\alpha_i>0$ ($\Lambda_i(sx)/\Lambda_i(s)\to x^{\alpha_i}$).
• Assumption 3.2 on the dependence: $Y$ has density $p(y)e^{-\varphi(y)}$ with $n^{-1}\varphi(ny_n)\to I(y)$ and $n^{-\varepsilon}\log p(ny_n)\to0$ along every $y_n\to y\ne0$ in $\mathbb R^d_+$.
• Assumption 5.1: each $\Lambda_i$ is eventually convex or concave.
• The limit $q^*=\lim_{t\to\infty}\hat q(t)$ exists.

The sampler (Algorithm 1) fixes a hyper-parameter $l=l(u)$ and maps a sample $x$ to $T(x)=x\,(u/l)^{\kappa(x)}$, with either exponent

$$\kappa^{(1)}(x)=\frac1\rho\frac{\log(1+|x|)}{\|\log(1+|x|)\|_\infty}\qquad\text{or}\qquad \kappa^{(2)}(x)=\frac{\log(1+|x|)}{\log l}.$$

With $J$ the closed-form Jacobian of Table 1 and $Z=T(X)$, the single-sample estimator is

$$\zeta(u)=\frac{J(X)f_X(Z)}{f_X(X)}\,\mathbb I\big(L(Z)\ge u\big),\qquad M_{2,u}=E[\zeta(u)^2].$$

Formalization targets

Goal: Theorem 5.1 (logarithmic efficiency)

Under Assumptions 2.1, 3.1, 3.2, 5.1, existence of $q^*$, $L^*(q^*x)>0$ for some $x\in\mathbb R^d_+$, and any slowly varying $l(u)\to\infty$, for either exponent,

$$M_{2,u}<\infty\ \text{for large }u,\qquad \lim_{u\to\infty}\frac{\log M_{2,u}}{\log p_u^2}=1.$$

The goal fixes neither the exponent, nor the hyper-parameter $l$, nor the loss or the distribution beyond the stated assumptions.

Milestones

The milestones follow the paper's proof chain (Appendix A.3 for $\kappa^{(1)}$, Appendix E for $\kappa^{(2)}$):

1. Proposition 2.1: $\zeta(u)$ is unbiased and $T$ is invertible.
2. Lemma 3.1: the coordinates of $Y$ are standard exponential.
3. Theorem 3.1: $\{Y/t\}$ satisfies a large deviations principle with rate $I$.
4. Lemma 3.2: $I$ is continuous and homogeneous, and $\inf_{y_i>c}I=c$.
5. Lemma A.1: the rare event in standardized coordinates.
6. Theorem 4.1: the tail asymptotic

$$\log p_u=-\Lambda_{\min}(u^{1/\rho})\big[I^*+o(1)\big],\qquad I^*=\inf\{I(y):L^*(q^*y^{1/\alpha})\ge1,\ y\ge0\}.$$

7. Lemmas A.4 and A.5: bounds on $T^{-1}$, and $\psi_u=\Lambda\circ T^{-1}\circ q$ is $o(t(u))$ on compacts.
8. Lemma A.6: $M_{2,u}$ as a Laplace-type functional of $Y_u=Y/t(u)$.
9. Lemma A.7: the density exponent $a_u\ge I+o(1)$.
10. Lemma A.9: the rare set stays a fixed distance from the origin.
11. Display (85): the $\kappa^{(2)}$ bound on $T^{-1}$.

Significance

Theorem 4.1 gives the exponential decay rate of $p_u$ for a broad class of nonconvex losses (piecewise affine and quadratic functions, values of mixed integer programs, neural-network feature maps) under nonparametric, copula-style dependence. Previously such asymptotics were known only for specific losses and distribution families. Theorem 5.1 shows that one simple, model-oblivious transformation attains the best possible exponential rate for the second moment, so the relative error grows more slowly than any power $p_u^{-\varepsilon}$. This supports using the sampler for value-at-risk, conditional value-at-risk and chance-constrained optimization.

The results are proved in the paper's appendices (Appendices A, D.1 and E). None of them has a machine-checked proof. Formalizing them would require regular variation and Potter bounds, a tail large deviations principle in $\mathbb R^d$, and a Varadhan-type integral lemma along a real speed. These are general tools that are missing from Mathlib and are reusable well beyond this paper.

Difficulty

The obvious argument is to bound $M_{2,u}$ by computing the likelihood ratio on the rare set. This fails because the rare set, after standardization, is described only asymptotically: $L_u(x)=u^{-1}L(q(t(u)x))$ converges to $f_{LD}(x)=L^*(q^*x^{1/\alpha})$ only continuously on $\mathbb R^d_{++}$, not uniformly. The exponent of the likelihood ratio involves the density of $Y$ at two different scales ($t(u)p$ and $\psi_u(t(u)p)$) and the hazard rates at points pulled back by $T^{-1}$. A lower bound on it must hold uniformly enough to apply a Varadhan-type lemma with a varying family of functions, while the transformed sample stays inside a region where the asymptotic density assumptions apply. The upper and lower large-deviations bounds also rely on homogeneity of $I$ and $f_{LD}$, which hold only for the heaviest-tailed coordinates of $q^*$.

Formalization scope

Points of $\mathbb R^d$ are Fin d → ℝ with the sup norm, and components are 0-based. $X$ is modelled by its law $\mu$ together with a density $f_X$. $M_{2,u}$ is a lower Lebesgue integral and $p_u=\mu\{L\ge u\}$; both are extended nonnegative reals, so neither $+\infty$ nor $0$ is collapsed to a junk value. Logarithms of probabilities in large-deviations statements are taken in EReal, where $\log0=-\infty$. $I^*$ is an EReal infimum, equal to $+\infty$ over an empty set. Regular variation is the real-variable limit with an eventually positive denominator, and reuses the published definition HeavyTailNV.Tail.IsRegularlyVarying. The Jacobian is Table 1's closed form. Statements that evaluate $q$ at $t(u)p$ take $p\in\mathbb R^d_{++}$.

The following hypotheses are added relative to the printed statements, each disclosed on its item:

• $l(u)\to\infty$ in Theorem 5.1 and Lemma A.7 (the paper states it in §2.2 and uses it in Lemma A.5 and Appendix D.1).
• "$L^*(q^*x)$ not identically zero" is read as positivity somewhere.
• Measurability of $L$.
• $0<l\le u$, and $l>1$ for $\kappa^{(2)}$, together with an IS support condition in Proposition 2.1 and Lemma A.6. Proposition 2.1 is false as printed without them.
• $p(ny_n)>0$ eventually inside (13).
• $d\ge1$ where junk values at $d=0$ would otherwise matter.
• In Theorem 4.1, continuity of the rate $I$ on $\mathbb R^d_+\setminus\{0\}$, which the theorem's hypothesis "the tail LDP in Theorem 3.1" carries through Lemma 3.2(a) and which the proof uses.

The following printed statements are corrected:

• Lemma A.6 is stated without its spurious factor $t(u)^{2d}$.
• Lemma A.9 is restricted to points with $q(t(u)p)\in\operatorname{supp}X$. As printed it fails when $L$ is large off the support.
• Lemma 3.2's "$I(0)=0$" becomes a limit at $0$, since (13) does not determine $I(0)$.
• Theorem 3.1 is stated with real speed $t$, which implies the printed sequence form.

Lemmas A.8 and A.10 and Corollary A.1 are not posed. Their uniform claims over all of $\mathbb R^d_+$ depend on pointwise versions of the hazard rates and on the values of $L$ off the support and off $\mathbb R^d_+$, which the hypotheses do not control; Corollary A.1 fails as printed when $X$ has negative components.

A trivializing formalization is ruled out explicitly. The goal is the limit (23) for the estimator $\zeta(u)$ of §5.2 with Table 1's Jacobian, for every admissible $l$ and both exponents. It is not the bound $M_{2,u}\ge p_u^2$, not a statement about an unspecified IS density, and not a statement for one fixed $l$. The finiteness conjunct prevents Lean's $\log 0=0$ convention from satisfying it.

Contributions are welcome at every level. The general tools (Potter bounds, the tail LDP, a Varadhan lemma for continuously converging functions) are useful as separate developments.

Selected references

• A. Deo, K. Murthy, Achieving Efficiency in Black-Box Simulation of Distribution Tails with Self-Structuring Importance Samplers, Operations Research, 2025; preprint arXiv:2102.07060v3, 2023. https://arxiv.org/abs/2102.07060
• S. Asmussen, P. W. Glynn, Stochastic Simulation: Algorithms and Analysis, Springer, 2007. https://doi.org/10.1007/978-0-387-69033-9
• L. de Haan, A. Ferreira, Extreme Value Theory: An Introduction, Springer, 2006. https://doi.org/10.1007/0-387-34471-3
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4