Machine Learning

Why shrink a best subset?

Best subset selection fits a linear predictor using at most $k$ of $p$ available columns. Its explicit limit on the number of selected variables makes the model easy to interpret, but the search can still fit noise: among many subsets of the same size, one can align unusually well with a noisy response. Mazumder, Radchenko and Dedieu study this effect in Subset Selection with Shrinkage. They add a penalty on the size of the selected coefficients and show how this changes prediction error when the signal-to-noise ratio is low.

An $\ell_1$ penalty is familiar from the Lasso. The estimator here also keeps the subset-size constraint, so its comparison class and its tuning parameter have a different role from those in an unconstrained Lasso. The paper's Theorem 3 gives three deterministic error bounds for this estimator, each valid on a specified event of the Gaussian noise. These bounds are the target of this mission. The separate probability estimates for the events are Theorem 1 of the paper and belong to another mission in this series.

Setting

Let $X\in\mathbb R^{n\times p}$ be a fixed design matrix whose columns have Euclidean norm one. The observation is $y=f^*+\epsilon$, where $f^*\in\mathbb R^n$ is a fixed mean and the coordinates of $\epsilon$ are independent $N(0,\sigma^2)$ random variables, with $\sigma>0$. The result below fixes one realized noise vector $\epsilon$ and assumes it lies in an event stated below. No assumption that $f^*$ is itself a linear combination of columns of $X$ is required.

For $1\le k\le p$, write $B_0(k)=\{\beta\in\mathbb R^p:\|\beta\|_0\le k\}$, where $\|\beta\|_0$ counts nonzero coordinates. An $\ell_1$-regularized best subset estimator is any minimizer

$$\hat\beta_1\in\operatorname*{argmin}_{\beta\in B_0(k)}\bigl\{\|y-X\beta\|_2^2+\lambda\|\beta\|_1\bigr\}.\tag{16}$$

The objective has no factor $1/2$. The assertion applies to every minimizer, so tied solutions are covered. The sparse minimum singular value is $\gamma_s=\inf\{\|Xu\|_2/\|u\|_2:u\ne0,\ \|u\|_0\le s\}$. When $p\ge1$ and $s\ge1$ its domain is nonempty. Write $u_1^\sharp,\ldots,u_p^\sharp$ for the decreasing rearrangement of $|u_1|,\ldots,|u_p|$.

The paper defines three noise events used here. $\mathcal H$ bounds the largest coordinate of $X^\top\epsilon$ by $\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}$. On $\mathcal F$, every $u\in\mathbb R^p$ satisfies

$$\epsilon^\top Xu\le(4+\sqrt2)\sigma\max\left\{\sum_{j=1}^{p}u_j^\sharp\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|_2\right\}.$$

On $\mathcal G_s$, every $u\in B_0(s)$ satisfies $\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|_2$. Here $\delta_0\in(0,1]$ and all logarithms are natural. These definitions, including the constant in $\mathcal G_s$, are the printed deterministic events of p. 13.

Formalization targets

Exact slow rate on $\mathcal H$

At $\lambda=2\sigma\sqrt{2\log(2p)}+2\sigma\sqrt{2\log(1/\delta_0)}$, Theorem 3(A) states

$$\|f^*-X\hat\beta_1\|_2^2\le\inf_{\beta\in B_0(k)}\bigl[\|f^*-X\beta\|_2^2+2\lambda\|\beta\|_1\bigr]\qquad(\epsilon\in\mathcal H).$$

Slow rate on $\mathcal F$

For $\lambda\ge(8+2\sqrt2)\sigma\sqrt{\log(2p)}$, a positive universal constant $C_A$ gives

$$\|f^*-X\hat\beta_1\|_2^2\le C_A\left[\inf_{\beta\in B_0(k)}\bigl(\|f^*-X\beta\|_2^2+\lambda\|\beta\|_1\bigr)+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal F).$$

Fast rate on $\mathcal G_{2k}$

For every $\lambda\ge0$, a positive universal constant $C_B$ gives

$$\|f^*-X\hat\beta_1\|_2^2\le C_B\left[\inf_{\beta\in B_0(k)}\|f^*-X\beta\|_2^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2 k+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal G_{2k}).$$

The $k$ multiplying $\gamma_{2k}^{-2}\lambda^2$ distinguishes this rate from the $\ell_2$-penalized estimator's bound. The three claims together, with their separate tuning conditions, are Theorem 3 on p. 16. The milestones follow the displays of its proof in Supplement B.6, pp. 42–43.

What the result provides

Each inequality compares the prediction of any selected minimizer with that of every sparse competitor. The first bound has an exact leading constant and no additive noise term on $\mathcal H$. The second keeps a linear penalty term when $\lambda$ meets a fixed noise-dependent threshold. The third replaces the linear term with a quadratic $\lambda$ term controlled by the sparse minimum singular value. This distinguishes regimes in which coefficient shrinkage changes the error rate. The paper also combines deterministic bounds with event probabilities in subsequent corollaries; those probability statements are separate from this goal.

The paper proves Theorem 3. The formalization task is to verify its model definitions, event interpretation and all three inequalities in Lean, with the same constants and quantifiers. The milestone statements isolate the basic inequality, the $\mathcal H$ bound, the rearranged-coordinate bound, the $\mathcal F$ case split and the sparse $\ell_1$ step. A complete proof would also provide reusable finite-dimensional norm and matrix estimates. This mission does not include the paper's numerical experiments, data-driven model-size selection, the $\ell_2$-penalized estimator, or the event-probability theorem.

Difficulty

The constraint $\|\beta\|_0\le k$ makes the estimator a minimizer over a nonconvex set. A standard unconstrained Lasso argument does not directly supply the paper's bound for every feasible sparse comparator. The slow rates rely on two different noise controls: a coordinatewise bound on $\mathcal H$ and a maximum of a sorted-coordinate term and a prediction-norm term on $\mathcal F$. The fast rate also needs the sparse minimum singular value to relate coefficient error to prediction error. The constants in these steps matter: replacing the exact first tuning equality or dropping the factor $k$ in the fast rate would state a different theorem.

Formalization scope

Lean uses Fin n → ℝ and Fin p → ℝ for vectors and Matrix (Fin n) (Fin p) ℝ for $X$. Norms are explicit finite sums, rather than the function type's default supremum norm. The paper's one-based sorted index $j$ is j.val + 1; the sum using $u^\sharp$ is encoded as a maximum over coordinate permutations, which agrees with the decreasing rearrangement. The events are predicates on realized noise vectors. The Gaussian law explains the model but is not needed in these deterministic statements. The estimator is an argmin predicate, never a chosen minimizer.

The universal constants precede all dimensions and data in the Lean goal. The infima in the three displayed bounds are expressed as inequalities for every $\beta\in B_0(k)$, avoiding the default value of an empty or unbounded real infimum. The standing conditions are $1\le k\le p$, unit-norm columns, $\sigma>0$ and $0<\delta_0\le1$. The first slow-rate branch retains the paper's equality for $\lambda$. The fast branch additionally requires $\gamma_{2k}>0$ or $\lambda=0$: this makes the $\lambda^2/\gamma_{2k}^2$ term meaningful under Lean's total division, which returns zero at a zero denominator. The displayed events use the paper's original $\mathcal G_s$ constant; this mission makes only a deterministic claim on that event.

The sparse domain for $\gamma_{2k}$ is nonempty under these conditions. All square-root radicands and logarithm arguments in the target are in their intended ranges. The formalization must rule out a universal constant that depends on $n$, $p$, $k$, $X$ or $\lambda$, and must apply to every minimizer. Contributions to the shared norm inequalities, rearrangement identity and matrix calculations are useful beyond this theorem.

Selected references

• Rahul Mazumder, Peter Radchenko and Antoine Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research 71 (2023), arXiv preprint version 4 (2022), arXiv:1708.03288v4. This mission cites the preprint's page and theorem numbering.

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors, choosing the $k$ that minimize the residual sum of squares. Mixed-integer optimization made it computable at moderate scale (Bertsimas, King & Mazumder, 2016), which reopened the statistical question of when it should be used. Empirical comparisons (Hastie, Tibshirani & Tibshirani, 2020) found that best subsets predicts poorly when the signal-to-noise ratio (SNR) is low: by fitting the noise exactly within its chosen support it overfits, and shrinkage methods such as the Lasso do better there.

Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty to the cardinality-constrained problem. Their Theorem 2 quantifies the effect of an $\ell_2$ (Euclidean-norm) penalty: it proves prediction-error bounds that are linear in the penalty level and therefore remain small in the low-SNR regime where best subsets fails. This mission formalizes that theorem.

Setting

The data follow the model

$$y=f^*+\epsilon,$$

where $y,f^*,\epsilon\in\mathbb R^n$, $f^*$ is an unknown deterministic mean and $\epsilon$ is a noise vector (in the paper, with independent $N(0,\sigma^2)$ entries, $\sigma>0$). The design $X\in\mathbb R^{n\times p}$ is deterministic and its columns have unit Euclidean norm. Write $\|\cdot\|$ for the Euclidean norm, $\|\beta\|_0$ for the number of nonzero coordinates of $\beta$, and $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$.

For a model size $k$ and a penalty level $\lambda\ge0$, the $\ell_2$-regularized best-subsets estimator is any solution

$$\hat\beta_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|\quad\text{s.t.}\quad\|\beta\|_0\le k.$$

The penalty is the norm $\|\beta\|$, not its square, and the loss carries no factor $1/2$. The quantity of interest is the prediction error $\|f^*-X\hat\beta_2\|^2$.

The minimal $s$-sparse eigenvalue of $X$ is $\gamma_s=\min_{u\neq0,\,u\in B_0(s)}\|Xu\|/\|u\|$. For $u\in\mathbb R^p$, $u^\sharp_1\ge\dots\ge u^\sharp_p$ is the non-increasing rearrangement of $|u_1|,\dots,|u_p|$. Given $\delta_0\in(0,1]$, three noise events are sets of noise vectors:

$$\mathcal E_s=\big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\big\},$$ $$\mathcal F=\Big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\max\Big(\textstyle\sum_{j=1}^p u^\sharp_j\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|\Big),\ \forall u\in\mathbb R^p\Big\},$$ $$\mathcal G_s=\big\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\big\}.$$

The paper's Theorem 1 shows these events have high probability; Theorem 2 is a deterministic statement on each of them. The symbol $\lesssim$ means "up to a positive universal multiplicative constant", one that does not depend on $n,p,k,X,f^*,\sigma,\lambda$ or $\delta_0$.

Formalization targets

Goal: Theorem 2 (p. 14)

Let $1\le k\le p$.

(A) Slow rate. If $\lambda\ge[8+2\sqrt2]\sigma\sqrt{2k\log(ep/k)}$, then on $\mathcal E_{2k}$

$$\|f^*-X\hat\beta_2\|^2\le\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+2\lambda\|\beta\|\big],$$

and on $\mathcal F$

$$\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+\lambda\|\beta\|\big]+\sigma^2\log(1/\delta_0).$$

(B) Fast rate. For every $\lambda\ge0$, on $\mathcal G_{2k}$

$$\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\|f^*-X\beta\|^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2+\sigma^2\log(1/\delta_0).$$

The bounds hold for every minimizer $\hat\beta_2$ and for misspecified models: $f^*$ need not lie in the column span of $X$.

Milestones

The steps of the printed proof (Supplement B.2, pp. 39–40), in the order the proof uses them: the basic inequality (29); the bound (30) on $\mathcal E_{2k}$ and its consequence (31); the dichotomy on $\mathcal F$, where (30) implies (31) and (32) implies (33); the elementary inequality (34); the basic inequality on $\mathcal G_{2k}$ (p. 40); and the bound of $\lambda\|\beta-\hat\beta_2\|$ through $\gamma_{2k}$ (p. 40).

Significance

The result. The slow-rate bound of part (A) is linear in $\lambda$. When the signal $\|\beta^*\|$ is small compared with $\sigma$, the term $\lambda\|\beta^*\|$ is smaller than the rate $\sigma^2 k\log(ep/k)$ that best subsets attains, and the paper's Theorem 4 shows that in this regime the prediction error of best subsets is at least of order $\sigma^2\gamma_k^2k\log(ep/k)$. Together the two results explain the empirical finding that shrinkage helps best subsets at low SNR. Part (B) shows nothing is lost at high SNR: the fast rate is the minimax rate $\sigma^2k\log(ep/k)$ over $k$-sparse vectors plus the shrinkage term $\gamma_{2k}^{-2}\lambda^2$. Combined with Theorem 1, the bounds give the high-probability statements of the paper's Corollaries 1 and 3.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist. The mission produces a checked deterministic core: once the events are granted, every constant ($8+2\sqrt2$, the factor $2\lambda$, the threshold $2k\log(ep/k)$) is verified exactly. Together with the companion mission on Theorem 1 it would yield fully checked high-probability oracle inequalities for a cardinality-constrained estimator, which no current formal library contains.

Difficulty

Every step is elementary, but the bookkeeping is exact. The obvious reading "insert the event's inequality into (29)" does not by itself work on $\mathcal F$: the event's right-hand side is a maximum of a sorted weighted sum and a prediction-norm term, and the first branch has to be compared with $\sqrt{2k\log(ep/k)}\,\|u\|$ for the $2k$-sparse difference $u=\hat\beta_2-\beta$, including when $2k$ exceeds $p$. That comparison is a combinatorial estimate on sorted sums, not a substitution. On $\mathcal G_{2k}$, the penalty difference $\lambda(\|\beta\|-\|\hat\beta_2\|)$ is not controlled by the event at all and has to be converted into prediction errors through $\gamma_{2k}$. In both parts the final constant must not depend on $k$, $p$ or $\delta_0$.

Formalization scope

All objects are explicit Lean definitions in the namespace SubsetShrink.L2:

• vectors are functions on Fin n and Fin p with 0-based indices, and $X$ is a real Matrix (Fin n) (Fin p);
• the Euclidean norm, $\|\cdot\|_0$ and the inner product are explicit finite sums, since Mathlib's norm on Fin m → ℝ is the sup norm;
• $\sum_j u^\sharp_j\sqrt{\log(2p/j)}$ is encoded as a maximum over permutations, which equals the sorted sum by the rearrangement inequality;
• $\gamma_s$ is a real infimum over the nonzero vectors of $B_0(s)$, a nonempty set when $p,s\ge1$.

The model consists of $X$ with unit columns, $f^*$, $\epsilon$, $\sigma>0$ and $y=f^*+\epsilon$. The estimator is a predicate that every minimizer satisfies; no minimizer is chosen and existence is not assumed. "On the event" is a hypothesis that the noise vector satisfies the event's printed inequality, so no probability measure appears. $\mathcal G_{2k}$ is the event as printed on p. 13; the correction of its probability bound belongs to the mission on Theorem 1 and does not affect these deterministic statements.

Committed conventions:

• each $\lesssim$ is an existential constant $C>0$ quantified before all other data;
• an infimum over $B_0(k)$ is stated as a bound for every $\beta\in B_0(k)$;
• $\delta_0\in(0,1]$ is universally quantified;
• the model size satisfies $1\le k\le p$.

Part (B) assumes $\gamma_{2k}>0$ or $\lambda=0$. When $\gamma_{2k}=0<\lambda$ the paper's bound is vacuous ($\gamma_{2k}^{-2}\lambda^2=+\infty$), but Lean's $0^{-1}=0$ would turn it into a false claim.

A formalization that lets the constant depend on $k$, $p$ or $\delta_0$, fixes a particular minimizer, weakens an event (for example drops "for all $u\in B_0(s)$"), or computes the infimum as a real ⨅ over an unbounded set would trivialize the theorem and is ruled out.

Not formalized here: the probability bounds of Theorem 1, the $\ell_1$-penalized Theorem 3, the lower bound of Theorem 4, the data-driven choice of $k$ (Theorem 5), and the corollaries and numerical experiments. These are separate missions or follow-ups. Contributions of reusable lemmas (the rearrangement bound for the sorted sum, properties of $\gamma_s$, the elementary absorption inequality (34)) are welcome.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• T. Hastie, R. Tibshirani, R. Tibshirani, Best subset, forward stepwise or Lasso? Analysis and recommendations based on extensive comparisons, Statistical Science 35(4), 2020. https://doi.org/10.1214/19-STS733
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670

Motivation

Offline policy learning chooses a treatment rule from logged data: given $n$ observations of features $X_i$, the action $A_i$ taken and the reward obtained, pick a policy $\pi:\mathcal X\to\{1,\dots,d\}$ from a class $\Pi$ whose expected reward is close to the best in the class. Zhou, Athey and Wager (arXiv:1810.04778v2) bound the regret of their cross-fitted augmented inverse-propensity-weighted learner by a quantity of order $\kappa(\Pi)\sqrt{V_*/n}$, where $\kappa(\Pi)$ is an entropy integral built from Hamming covering numbers of $\Pi$. A bound of this kind is only useful for a concrete policy class if $\kappa(\Pi)$ is finite and explicit.

Decision trees are the class the paper uses in practice: they are interpretable, they are the standard object in personalized-treatment applications, and the paper's computational sections (a mixed-integer program and a tree-search algorithm) optimize over them. Lemma 4 of the paper is the bridge between the general regret theory and trees: it bounds the Hamming covering number of the class $\Pi_L$ of depth-$L$ trees, and hence $\kappa(\Pi_L)$. Covering and complexity bounds for trees in the 0–1 (two-action) setting go back to VC-dimension arguments; the multi-action Hamming-cover version here is the one this paper's regret bound consumes.

Setting

Features are points $x\in\mathbb R^p$ with components $x(1),\dots,x(p)$; there are $d$ actions, written $1,\dots,d$. A deterministic policy is a map $\pi:\mathbb R^p\to\{1,\dots,d\}$.

Hamming distance and covers. Fix points $x_1,\dots,x_n$ (repetitions allowed). For two policies,

$$H(\pi_1,\pi_2)=\frac1n\sum_{j=1}^n\mathbf 1\{\pi_1(x_j)\ne\pi_2(x_j)\}.$$

The $\varepsilon$-Hamming covering number $N_H(\varepsilon,\Pi,\{x_1,\dots,x_n\})$ is the least $K$ such that some $\pi_1,\dots,\pi_K\in\Pi$ have every $\pi\in\Pi$ within Hamming distance $\varepsilon$ of some $\pi_i$. The covering number of the class is the worst case over point sets,

$$N_H(\varepsilon,\Pi)=\sup\{N_H(\varepsilon,\Pi,\{x_1,\dots,x_m\}) : m\ge1\},$$

and the entropy integral is $\kappa(\Pi)=\int_0^1\sqrt{\log N_H(\varepsilon^2,\Pi)}\,d\varepsilon$.

Decision trees. A depth-$L$ tree has $L$ layers: $L-1$ layers of branch nodes and a final layer of leaves, so $2^{L-1}-1$ branch nodes and $2^{L-1}$ leaves; a depth-1 tree is a single leaf. A branch node carries a split variable $i\in\{1,\dots,p\}$ and a threshold $b\in\mathbb R$, and sends $x$ to its left child if $x(i)<b$ and to its right child otherwise. Each leaf carries an action. $\Pi_L$ is the set of policies computed by depth-$L$ trees. In the Lean development these are DTree p d L, DTree.eval and treePolicies p d L; the Hamming layer is hammingDist, hammingCoverNumOn, hammingCoverNum and entropyIntegral.

Formalization targets

Goal: Lemma 4, part 1 (p. 27)

For $p,d,L\ge1$ and $\varepsilon>0$, $N_H(\varepsilon,\Pi_L)$ is finite and

$$\log N_H(\varepsilon,\Pi_L)\le(2^L-1)\log p+2^L\log d+(2^L-1)\log\Big(\frac L\varepsilon+1\Big).$$

Milestones (App. F)

1. Display (66), p. 67: for any reals $r_1,\dots,r_m$ there are $\lceil L/\varepsilon\rceil$ thresholds $b_i$ such that every indicator $\mathbf 1_b(r)=\mathbf 1\{r<b\}$ is within Hamming distance $\varepsilon/L$ of some $\mathbf 1_{b_i}$ with respect to $r_1,\dots,r_m$.
2. App. F, Step 2, p. 69: for any $n\ge1$ points, $p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ depth-$L$ trees $\varepsilon$-cover $\Pi_L$, i.e. $N_H(\varepsilon,\Pi_L,\{x_1,\dots,x_n\})\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$.
3. App. F, Step 2, p. 69: $N_H(\varepsilon,\Pi_L)\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$.

Companion: Lemma 4, part 2 (p. 27)

$$\kappa(\Pi_L)\le\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1}.$$

It is posed as printed, as a second theorem of the mission rather than a milestone of the goal.

Significance

The result. Lemma 4 makes the abstract regret theory of the paper concrete: with part 2 it gives Theorem 4, the regret bound $O_p\big((\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1})\sqrt{V_*/n}\big)$ for learning depth-$L$ trees, which for fixed $L,p,d$ is $O_p(\sqrt{V_*/n})$. The covering bound grows only logarithmically in $1/\varepsilon$, which is the property the paper's Assumption 3 asks of a policy class. The same counting gives covering bounds for any class of piecewise-constant rules on axis-aligned partitions of bounded depth.

Formalizing it. The result is proved in the paper (App. F) but, as far as known, has no machine-checked proof. The paper omits the induction that combines per-node threshold grids into a cover of whole trees ("a straightforward but lengthy induction (omitted)"), and its appendix counts $2^L-1$ branch nodes where §6.1's trees have $2^{L-1}-1$. A formal proof fixes both: it supplies the omitted induction and confirms that the printed bound holds for the class actually defined in §6.1. The milestones are reusable statements about threshold indicators and tree covers. The companion part 2 is posed with the printed constant $4/3$, although the printed derivation evaluates $\int_0^1(L/\varepsilon^2)^{1/4}d\varepsilon$ as $\frac43L^{1/4}$ where the integral equals $2L^{1/4}$; whether the printed bound holds is part of what the mission settles.

Difficulty

The one-dimensional step (66) is elementary once the Hamming distance between two threshold indicators is identified with a count of points between the thresholds. The difficulty is in passing from single thresholds to whole trees. Replacing each branch node's threshold independently by its nearest grid threshold, with grids built on all $n$ points, does not give an $\varepsilon$ cover: the errors at different nodes of the same layer add up, and the naive bound is $(2^{L-1}-1)\varepsilon/L$ rather than $\varepsilon$. The points that reach a node depend on the thresholds above it, so the approximation has to respect the tree structure, while the number of candidate trees must still be counted as a product over nodes. The passage from finite point sets to $N_H(\varepsilon,\Pi_L)$, which is a supremum over all point sets in $\mathbb N\cup\{\infty\}$, and the arithmetic with $\lceil L/\varepsilon\rceil$ and real logarithms are routine but must be done in the stated types.

Formalization scope

• Features range over all of $\mathbb R^p$ (Fin p → ℝ); the paper's $\mathcal X$ is a bounded subset of $\mathbb R^p$, and a bound over $\mathbb R^p$ implies the bound over every $\mathcal X\subseteq\mathbb R^p$. Actions are Fin d, split variables Fin p (0-based); policies are deterministic.
• Point sets are sequences Fin m → (Fin p → ℝ) with repetitions allowed, $m\ge1$; covers are proper (centres in $\Pi_L$). $N_H(\varepsilon,\Pi)$ is in ℕ∞, $\kappa(\Pi)$ a lower Lebesgue integral in ℝ≥0∞ over $(0,1]$.
• Depth follows §6.1: DTree p d 1 are leaves, DTree p d 0 is empty. The bounds are the printed ones, which over-count for this convention; the Lean was not switched to the appendix's convention, which would change $\Pi_L$.
• Standing hypotheses: $p\ge1$, $d\ge1$, $L\ge1$ ("Let $L$ be any fixed positive integer"), $\varepsilon>0$ (needed for $\lceil L/\varepsilon\rceil$).
• The goal asserts finiteness of $N_H(\varepsilon,\Pi_L)$ explicitly. Without it the inequality would be trivially true for an infinite covering number, because Lean's toNat ⊤ = 0 and Real.log 0 = 0. The covering number is an infimum that is $0$ only for an empty class, and $\Pi_L$ is nonempty under the hypotheses, so the cover is not trivialized either.
• Not posed: the $O(\log 1/\varepsilon)$ remark of Lemma 4.1 (a remark on the right-hand side); Theorem 4 (p. 28, the combination with the regret theorem, which belongs to the companion mission on regret); the mixed-integer program and tree search of §6.2–6.3 and App. G (computational).

Contributions welcome: proofs of the milestones, the omitted per-node induction as a stand-alone lemma, and the companion part 2.

Selected references

• Z. Zhou, S. Athey, S. Wager, Offline Multi-Action Policy Learning: Generalization and Optimization, arXiv preprint, 2018 (v2). https://arxiv.org/abs/1810.04778
• L. Breiman, J. Friedman, R. Olshen, C. Stone, Classification and Regression Trees, Wadsworth, 1984. https://doi.org/10.1201/9781315139470
• D. Bertsimas, J. Dunn, Optimal classification trees, Machine Learning 106, 1039–1082, 2017. https://doi.org/10.1007/s10994-017-5633-9
• S. Athey, S. Wager, Policy Learning With Observational Data, Econometrica 89(1), 133–161, 2021. https://doi.org/10.3982/ECTA15732

Learning to bid in first-price auctions

Display advertising has been moving from second-price to first-price auctions: several exchanges began rolling them out in 2017, and Google Ad Manager completed its move at the end of 2019 (Davies 2019). In a second-price auction bidding one's value is a dominant strategy; in a first-price auction the optimal bid depends on the distribution of the competing bids, which a bidder does not know and must learn from repeated play. Most of the learning literature on auctions takes the seller's side of the second-price auction (reserve prices, e.g. Cesa-Bianchi, Gentile, Mansour 2015); on the bidder's side of the first-price auction, the main prior approach is the cross-learning framework of Balseiro et al. 2019.

Han, Zhou and Weissman (arXiv:2003.09795) study the bidder's problem with the feedback that ad exchanges actually provide, where only the winning price is announced, and with no assumption on the distribution of the competing bids. Their two upper bounds are $\widetilde O(\sqrt T)$ regret: Theorem 1 for iid private values and Theorem 2, the subject of this mission, for values chosen by an oblivious adversary. A matching $\Omega(\sqrt T)$ lower bound holds even under full information (Theorem 9).

Setting

A single bidder plays $T$ rounds. In round $t$ she observes a private value $v_t\in[0,1]$, bids $b_t\in[0,1]$, and wins if $b_t\ge m_t$, where $m_t\in[0,1]$ is the highest other bid (HOB). Her payoff is (1)

$$r(v_t,b_t;m_t)=(v_t-b_t)\,\mathbb 1(b_t\ge m_t).$$

The HOBs are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$; $G$ may be discrete, continuous or mixed. Feedback is censored: after round $t$ only $\max\{b_t,m_t\}$ is revealed, so $m_t$ is observed only when the bidder loses. The expected reward is $R(v,b)=(v-b)G(b)$, and the regret of a policy $\pi$ against the value sequence $v=(v_1,\dots,v_T)$ is (3)

$$R_T(\pi;v)=\sum_{t=1}^T\Big(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Big),$$

the shortfall against an oracle that knows $G$. A policy bids in round $t$ as a (possibly randomized) function of $v_1,\dots,v_t$ and of the feedback of rounds $1,\dots,t-1$. An oblivious adversary fixes the whole value sequence in advance, independently of the bids and the HOBs.

The policy analysed is ML-IS-UCB (Algorithm 4). It restricts bids to the grid $b^i=(i-1)/K$, $i\in[K]$, with $K=\lceil\sqrt T\rceil$; it splits time into $L=\lceil\log_2T\rceil$ levels after an initialization phase of $T_0=(L+1)\lceil\sqrt T\rceil$ zero bids; and at each level it computes a width $w^\ell_{i,t}$, an interval-splitting reward estimate $\hat r^\ell_{i,t}$ and a candidate set $\mathcal B^\ell_t$ by the displays (12)–(16).

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $T\ge2$ some policy $\pi$ satisfies, for every value sequence $v\in[0,1]^T$ and every $G$ on $[0,1]$,

$$\mathbb E\big[R_T(\pi;v)\big]\le C\sqrt T\log^3T .$$

The constant is unspecified, so the goal survives any improvement of the constants below.

The explicit bound: Theorem 7

For every $\gamma\ge3$, the ML-IS-UCB policy satisfies

$$\mathbb E\big[R_T(\pi^{\mathrm{ML\text{-}IS\text{-}UCB}};v)\big]\le4+(L+4)\lceil\sqrt T\rceil+80\gamma^{3/2}\log(LKT)(1+\log T)\,L\sqrt T .$$

Milestones

In the order of the proof (Section 4.3 and Appendix C):

1. Lemma 7: with probability at least $1-4T^{-3}$, $|\hat r^\ell_{i,t}-r_{i,t}|\le w^\ell_{i,t}$ for all $i,\ell$ and $T_0<t\le T$, and $w^\ell_{i,t}$ is bounded by (18) in terms of the true interval probabilities $p_j=G(b^{j+1})-G(b^j)$.
2. Lemma 8: on that event the best grid bid is never eliminated, and a round assigned to level $\ell$ has regret at most $8\cdot2^{-\ell}$ against the grid.
3. Display (19): the grid regret is at most $T_0+8\sum_\ell2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|$.
4. Lemma 16: a deterministic counting bound for the sums $\sum_t\sum_{j\ge i(t)}v_j/n^\ell_{j,t}$.
5. Lemma 9: $2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|\le10\gamma^{3/2}\log(LKT)(1+\log T)\sqrt T$.
6. Theorem 7.

A supporting item, not a milestone, states the quantization step $\max_{b\in[0,1]}R(v,b)\le\max_iR(v,b^i)+1/K$ for the grid of Algorithm 4.

Significance

The result shows that adversarial values cost at most a logarithmic factor relative to iid values in repeated first-price auctions with censored feedback, and that no regularity of $G$ is needed. ML-IS-UCB is also an algorithmic template: its widths are computed before the data of the current level is used, which makes the estimates at each level independent of the bids that select them, and its interval-splitting estimator uses the variance of each interval rather than a uniform bound. Remark 3 notes that replacing the interval probabilities by $1$ gives only $\widetilde O(\sqrt{KT})$.

All results of the paper are proved in the preprint; none of them is machine-checked. A complete development formalizes a multi-level elimination algorithm with data-dependent level assignment, a Bernstein-type concentration argument for estimates indexed by random sets, and the counting lemma behind the logarithmic factors. Each of these is reusable for other elimination-based bandit algorithms.

Difficulty

The obvious route is a single UCB index per grid bid, (11) on p. 27, built from all past observations through the estimates $\hat p^t_j=\sum_{s\le t}\mathbb 1(b_s\le b^j)\mathbb 1(m_s\in(b^j,b^{j+1}])/\sum_{s\le t}\mathbb 1(b_s\le b^j)$. It fails because $\hat p^t_j$ is not a normalized binomial variable: each bid depends on the earlier HOBs, so conditioned on the bids the HOBs are no longer independent and $\hat p^t_j$ is not even unbiased. Self-normalized martingale bounds control each $\hat p^t_j$ separately but not the sum $\sum_{j\ge i}\hat p^t_j$ that the reward estimate needs. Algorithm 4 restores conditional independence through its level structure, and Lemma 7 has to make that precise: the sets $\Phi^\ell(t)$ are random, and the bound must hold uniformly over all $(i,\ell,t)$ with a variance term estimated from a held-out sample. Lemma 9 then needs the variance-sensitive width (18); a crude width loses a factor $\sqrt K$ (Remark 3).

Formalization scope

• Model. Rounds are Fin T; Lean round $t$ is paper time $t+1$. The HOB law is a probability measure μG on ℝ with μG [0,1]ᶜ = 0, and $G(x)$ is (μG (Set.Iic x)).toReal; atoms are allowed. The maximum in (3) is a supremum over $[0,1]$.
• Policies. A policy has internal randomness $u\sim\mu_U$ and, for each $u$, a bidding rule whose round-$t$ bid receives only the values of rounds $\le t$ and the feedback $\max\{b_s,m_s\}$ of rounds $<t$, enforced by the argument types; bids lie in $[0,1]$ and are jointly measurable. The expectation is a Bochner integral over $u$ and $m\sim G^{\otimes T}$, and Theorems 2 and 7 also assert integrability, so the integral cannot be a junk value.
• Algorithm 4. Grid indices are 0-based ($b^{i+1}=i/K$, $b^{K+1}=1$); inside the algorithm times are the paper's $1,\dots,T$. Every quantity $n,w,\hat p,\hat r,\mathcal B$ is defined by its formula for every $(i,\ell,t)$. The estimators (14) and $\hat p^0$ are computed from the feedback, not from $m$, and the algorithm recomputes its own past decisions, so it is a censored-feedback rule. "An arbitrary $i$" is a selection rule depending on the time and the level only. If no level breaks (impossible for $\gamma\ge3$, $T\ge2$) the round goes to level $L$ with bid $0$.
• Hypotheses added to the printed statements, each disclosed in its item: $T\ge2$ in Theorem 2 (the printed bound is $0$ at $T=1$); Lemmas 8, 9 and (19) are stated pathwise under the inequalities of Lemma 7 that their proofs use; Lemma 16 assumes that the set contains $\lceil\sqrt T\rceil$ initialization rounds with bid $0$, which its proof uses; the quantization display is adapted from the grid of Lemma 4 to that of Algorithm 4.
• Ruled out. A policy that reads $m_t$, $G$ or future values, a constant $C$ chosen after $T$, $v$ or $G$, a policy chosen after $v$ or $G$, and an expectation of a non-integrable function would each make the goal trivial; the statements exclude all four.
• Needed and welcome. Bernstein and multiplicative Chernoff bounds for binomial variables (Lemmas 14, 15 of the paper are cited from the literature), measurability of the run of the algorithm, and the harmonic-sum bound $\sum_{k=a}^T1/k\le1+\log T$. Contributions toward any milestone, or alternative proofs of the goal, are welcome.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
• N. Cesa-Bianchi, C. Gentile, Y. Mansour, Regret Minimization for Reserve Prices in Second-Price Auctions, IEEE Transactions on Information Theory 61(1), 2015. https://doi.org/10.1109/TIT.2014.2365772
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• J. Davies, What to know about Google's implementation of first-price ad auctions, Digiday, 2019. https://digiday.com/media/buyers-welcome-auction-standardization-as-google-finally-goes-all-in-on-first-price/

Learning a cost vector from optimal decisions

In inverse optimization, an observer sees decisions made by an expert who solves an optimization problem, and wants to recover the expert's unknown objective. Besbes, Fonseca and Lobel study a contextual version: in each period a feasible set and a context function are revealed, a learner must act before seeing the expert's choice, and then observes the expert's optimal action. The learner pays the expert's cost of its own action. This models, for example, a platform imitating a dispatcher's routing decisions or a recommender learning a user's trade-offs, where only optimal choices, not costs, are ever observed (Besbes, Fonseca, Lobel, arXiv:2106.14015).

For the one-period (offline) problem the paper shows that the circumcenter policy, which acts as if the unknown cost were the center of the smallest revolution cone containing the set of costs still consistent with the data, is minimax optimal (Theorem 1). The natural online policy is to apply it greedily in every period. This mission formalizes the paper's Theorem 2, which shows that this greedy policy can fail badly: its worst-case regret can grow linearly in the horizon, even when the initial uncertainty is small in a precise geometric sense.

Setting

Costs live in $\mathbb R^d$ and actions in $\mathbb R^n$. The true cost $c^\star$ lies on the unit sphere $S^d$. An action set $\mathcal X\in\mathfrak B$ is a nonempty compact subset of $\mathbb R^n$ of diameter at most $1$; a context function $f\in\mathfrak F$ is a $1$-Lipschitz map $\mathbb R^n\to\mathbb R^d$. The forward problem with cost $c$ has solution set

$$\psi(c,\mathcal X,f)=\arg\min_{x\in\mathcal X} f(x)'c .$$

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$, set to $0$ if either vector is $0$. The uncertainty angle of a set $C$ is

$$\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\theta(c,\hat c),$$

and a circumcenter $\hat c(C)$ is a unit vector attaining this infimum. A set is pointed when $\alpha(C)<\pi/2$, i.e. it fits inside an open half-space cone.

Online protocol. In periods $t=1,\dots,T$ nature reveals $\mathcal X_t$ and $f_t$, the learner picks $x^\pi_t\in\mathcal X_t$, and then an optimal expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ is revealed. Starting from a closed set $C_0\subseteq S^d$, the knowledge set is

$$C(\mathcal I_t)=\{c\in C_0:\ c'f_s(x^\star_s)\le c'f_s(x)\ \ \forall x\in\mathcal X_s,\ s<t\},$$

the regret is $R^\pi_T=\sum_{t=1}^T\big(f_t(x^\pi_t)-f_t(x^\star_t)\big)'c^\star$, and the worst-case regret $\mathcal{WCR}^\pi_T(C_0)$ is its supremum over $c^\star\in C_0$ and admissible instances. The greedy circumcenter policy chooses $x^\pi_t\in\psi\big(\hat c(C(\mathcal I_t)),\mathcal X_t,f_t\big)$.

Formalization targets

Goal: Theorem 2 (pp. 13–14)

There is a closed, nonempty, pointed $C_0\subseteq S^3$ such that

$$\mathcal{WCR}^{\pi_{greedy}}_T(C_0)=\Omega(T).$$

Concretely: there are $C_0$ and $\kappa>0$ such that for every horizon $T\ge1$ some $c^\star\in C_0$ and admissible $(\mathcal X_t,f_t)$ admit a greedy run, and every greedy run (any circumcenter, any tie-break) has regret at least $\kappa T$. The constant $\kappa$ is left existential, as the page claims only $\Omega(T)$.

Milestones (the proof's displayed steps, App-9–App-11)

1. Lemma 2 (p. 12): a circumcenter exists for every nonempty set, and is unique when the set is pointed and not $\{0\}$.
2. Step 1: for $0<\bar\alpha<\pi/2$ and $0\le\varepsilon\le\tan\bar\alpha/2$, the set $C_{\varepsilon,\bar\alpha}$, a polyhedral cone cut by three half-spaces and intersected with $S^3$, has the unique circumcenter

$$\hat c(C_{\varepsilon,\bar\alpha})=\tfrac{1}{\sqrt{1+\varepsilon^2}}(1,\varepsilon,0).$$

3. Step 2: with $C_0=C_{0,\bar\alpha}$, $f_t=\mathrm{id}$, $\mathcal X_t=\{\bar x_t,0\}$, $\varepsilon_t=t\tan\bar\alpha/(2T)$, the greedy knowledge sets are $C(\mathcal I_t)=C_{\varepsilon_{t-1},\bar\alpha}$.
4. Step 3: in that instance, with $\tan\bar\alpha\le 2$, each period's regret is at least $\sin\bar\alpha/4$.

Significance

The result separates offline from online learning in this model. Theorem 1 makes the circumcenter the best one-shot guess, yet Theorem 2 shows that one-shot optimality says nothing about information collection: a greedy learner can keep choosing actions that are wrong by a fixed margin while the revealed expert actions cut away only slivers of the knowledge set. This is the reason the paper introduces its EllipsoidalCones algorithm, which acts greedily on an enlarged ellipsoidal-cone superset and attains logarithmic regret for pointed initial sets. Theorem 2 is the lower bound that makes that design necessary.

On the formal side, the paper's proof is complete but compressed; it asserts the circumcenter of a three-generator spherical polygon "using Definition 2" and leaves the induction's geometric inclusions to the reader. A machine-checked version fixes the normalization of the circumcenter and the quantitative condition behind "$\varepsilon^2\le1$", and gives a reusable formal treatment of uncertainty angles and circumcenters, which the paper's other results (Theorem 1, Theorem 3, Lemma 10) all use. No result of the paper has a formal statement or proof on Prove2Me yet.

Difficulty

The arithmetic of Step 3 is elementary once the knowledge sets are known. The difficulty is in Steps 1 and 2. Identifying the circumcenter of $C_{\varepsilon,\bar\alpha}$ requires a minimax argument over the whole sphere: one must show that no other unit vector has a smaller maximal angle to the three extreme rays, and that the minimizer is unique, which rests on Lemma 2. The greedy policy is defined through this minimizer, so without uniqueness nothing can be said about its actions. Step 2 then needs an exact description of each knowledge set: showing that the new half-space makes the previous one redundant inside $C_0$ requires the sign information carried by the other constraints. A naive bound on the regret that ignores the knowledge-set dynamics fails, because a priori the policy might learn $c^\star$ after a few periods.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), so norms, diameters and Lipschitz constants are Euclidean. The angle uses the paper's convention $\theta(c,0)=\theta(0,\hat c)=0$; Mathlib's InnerProductGeometry.angle is not used. Action sets are required to be nonempty (otherwise no action exists). Periods are $0$-based in Lean: Lean period $t$ is the paper's period $t+1$, and Lean's knowledge set at $t$ is the paper's $C(\mathcal I_{t+1})$. The construction and the goal are in dimension $d=3$, as in the proof; the goal holds for every action dimension $n\ge1$.

The worst-case regret is never written as a real supremum, whose junk values would decide the statement. The lower bound is stated by exhibiting the instance. A run of the greedy policy is a predicate quantifying over every circumcenter choice and every minimizer, and nature's sequences are arbitrary. Two pins relative to the page: the printed circumcenter $(1,\varepsilon,0)$ is normalized as in Step 3, and Step 3 assumes $\tan\bar\alpha\le2$, which the page's "$\varepsilon^2\le1$" needs (the goal uses $\bar\alpha=\pi/4$).

Two trivializations are ruled out. Without pointedness the claim holds for $C_0=S^3$ with antipodal costs, so $\alpha(C_0)<\pi/2$ is part of the goal. A bound over all runs would hold vacuously if no run existed, so the goal also asserts that a greedy run exists.

A complete development needs spherical geometry of polyhedral cones (extreme rays, angles to a cone), continuity of the uncertainty-angle objective for Lemma 2, and elementary trigonometry. The Geometry and Online definitions are shared with the other missions of this series and are reusable for any work on inverse optimization or learning from revealed preferences. Proofs of any milestone are welcome, as are alternative arguments for Lemma 2.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023 (preprint used here; published in Operations Research, 2025). https://arxiv.org/abs/2106.14015
• M. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
• R. K. Ahuja, J. B. Orlin, Inverse Optimization, Operations Research 49(5), 2001. https://doi.org/10.1287/opre.49.5.771.10607

Motivation

Most display advertising is sold in first-price auctions: the highest bidder wins and pays its own bid. Since the industry's move away from second-price formats around 2019, a bidder can no longer bid its value and must instead learn how much to shade its bid, from data about how the other bidders behave. A demand-side platform faces this problem millions of times a day with very little information. When it wins it pays its bid and learns nothing about the competition beyond the fact that it won; when it loses it sees only the winning price.

Han, Zhou and Weissman (arXiv:2003.09795v7, Operations Research 2025) cast this as an online learning problem and gave the first bidding policies with $\tilde O(\sqrt T)$ regret against an arbitrary unknown distribution of competing bids. This mission is the first of a series of six on that paper. It covers the case of stochastic private values, and the route to it through a general class of contextual bandits.

Setting

A single bidder takes part in $T$ rounds. In round $t$ she observes a private value $v_t\in[0,1]$, bids $b_t\in[0,1]$, and the highest other bid (HOB) is $m_t\in[0,1]$. She wins iff $b_t\ge m_t$, so her payoff is $r(v_t,b_t;m_t)=(v_t-b_t)\mathbb 1(b_t\ge m_t)$. The HOBs are iid with an unknown CDF $G$ on $[0,1]$; no continuity or shape assumption is made, and atoms are allowed. The values $v_1,\dots,v_T$ are iid with an unknown distribution $F$ on $[0,1]$, independent of the HOBs.

Feedback is censored: at the end of round $t$ only the winning bid $y_t=\max\{b_t,m_t\}$ is revealed. A policy $\pi$ chooses $b_t$ from its own internal randomness, $v_1,\dots,v_t$ and $y_1,\dots,y_{t-1}$. With the expected reward $R(v,b)=(v-b)G(b)$, the regret is

$$R_T(\pi;v)=\sum_{t=1}^T\Big(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Big),$$

the gap to an oracle that knows $G$.

The paper reaches its bound through partially ordered contextual bandits. These are contextual bandits with $M$ contexts and $K$ actions, rewards in $[0,1]$, and a feedback graph $G$ on the actions. Playing $a$ reveals the rewards of $a$ and its out-neighbours under every context (cross learning). The graph is a transitively closed DAG, so it induces a partial order $\preceq_G$ on actions. There is also a partial order $\preceq_{\mathcal C}$ on contexts along which some choice of optimal action is monotone (Definitions 2 and 3). Algorithm 3 is an arm-elimination algorithm for this class. The auction becomes such a bandit when values are clipped to the grid $\mathcal C=\{1/M,\dots,1\}$ and bids are restricted to $\mathcal A=\{1/K,\dots,1\}$: a bid $b$ reveals $\mathbb 1(m_t\le b')$ for every $b'\ge b$.

Formalization targets

Goal: Theorem 1

$$\exists\,C>0\ \ \forall\,T\ge2\ \ \exists\,\pi\ \ \forall\,F,G:\qquad \mathbb E\big[R_T(\pi;v)\big]\le C\sqrt T\,\log^{2.5}T .$$

The policy may depend on $T$ but not on $F$ or $G$, and $C$ is absolute. The goal leaves the policy unspecified. That makes it the weakest stable form of the paper's result: any later policy with a better logarithmic factor still proves it.

Milestones, in attack order

1. Lemma 5 (p. 20): the largest maximiser $b^\star(v)$ of $R(v,\cdot)$ over the grid $\mathcal A$ is non-decreasing in $v$.
2. Lemma 4 (p. 20): pathwise, quantization costs at most $(2/M+1/K)T$ regret.
3. Lemma 3.1 (p. 19): for iid $X_1,\dots,X_T$ in a finite poset of width $\beta$, $\mathbb E\sum_t(1+\sum_{s<t}\mathbb 1(X_s\preceq X_t))^{-1}\le\beta(1+\log T)^2$.
4. Lemma 2 (p. 18): with probability $1-\delta$, Algorithm 3's minimum counts satisfy $N^{t-1}_{c_t}\ge\sum_{s<t}\mathbb 1(c_s\preceq_{\mathcal C}c_t)/(\alpha\log(MKT^2/\delta))-1$.
5. Theorem 5, iid contexts (p. 18): $\mathbb E[R_T]\le1+24\sqrt{\alpha\beta T\log(2T)\log(2MKT^2)\log(2MKT^3)}(1+\log T)$.
6. Corollary 1, iid values (p. 20): Algorithm 3 on the quantized auction with $M=K=\lceil\sqrt T\rceil$, $\delta=1/(2T)$ has expected regret $O(\sqrt T\log^{2.5}T)$. This is the explicit policy behind the goal.

Significance

The result. Theorem 1 shows that a bidder facing an arbitrary unknown competition distribution can learn to bid as well as the oracle up to $\tilde O(\sqrt T)$. That rate is optimal up to logarithms: mission 3 of the series formalizes the $\Omega(\sqrt T)$ lower bound. Theorem 5 is of independent interest. For partially ordered contextual bandits with iid contexts, the regret depends on the widths $\alpha,\beta$ of the two orders and not on the numbers $M,K$ of contexts and actions. Mission 5 of the series shows that this fails for adversarial contexts.

Formalizing it. The results are proved in the paper, with full proofs in its Appendix C; none of them has a machine-checked proof. Beyond the theorems, the mission produces a reusable model of repeated auctions with censored feedback, with policies that are non-anticipating by construction. It also produces a definition of contextual bandits with graph feedback and cross learning, and an executable definition of an elimination algorithm with randomized exploration. Lemmas 3, 4 and 5 are self-contained and need no bandit machinery.

Difficulty

The obvious approach discretizes and runs one bandit algorithm per context. That gives regret $\tilde O(\sqrt{MT})$ and, after balancing against the quantization error of Lemma 4, only $\tilde O(T^{2/3})$. Reaching $\sqrt T$ requires information to flow across contexts. Lemma 2 says that a round with a small context feeds the minimum counts of every larger context. Lemma 3 turns this into a bound on the sum of confidence widths that depends on the width $\beta$ of the context order and not on $M$. Lemma 2 is a statement about a randomized algorithm whose active sets depend on the whole past, and its proof uses the uniform choice among the sources of the active set together with the extra elimination rule ($\star\star$). The step from a high-probability bound to an expectation over iid contexts must keep the contexts independent of the rewards and of the algorithm's randomness.

Formalization scope

• Time and grids. Rounds are Fin T: paper round $t$ is index $t-1$. The grids (6) are finite sets of reals. Context $i$ and action $j$ of Fin M, Fin K stand for $(i+1)/M$ and $(j+1)/K$. The paper's $M=K=T^{1/2}$ are $\lceil\sqrt T\rceil$.
• HOB law. $G$ is a probability measure on $\mathbb R$ carried by $[0,1]$, with $G(x)=\mu_G((-\infty,x])$. Atoms are allowed.
• Policies. A policy has an internal probability space. Its round-$t$ bid takes the values as Fin (t+1) → ℝ and the feedback $\max\{b_s,m_s\}$ as Fin t → ℝ. It never sees $m$, $G$ or $F$. The expectation is an integral against $\mu_U\otimes F^{\otimes T}\otimes G^{\otimes T}$.
• Integrability. Every expected-regret bound also asserts that the regret is integrable. This rules out the trivializing reading in which a non-measurable policy has expected regret $0$ (Lean's value of a non-integrable integral).
• Horizon. Theorem 1 and Corollary 1 start at $T\ge2$: at $T=1$ the printed bound is $0$, but an uninformed first bid has positive regret.
• Algorithm 3. The algorithm is a deterministic function of the contexts, the reward vectors and one uniform $u_t\in[0,1]$ per round. The uniform choice in ($\star$) is the $\lfloor u_tn\rfloor$-th of the $n$ candidates. The topological ordering of the contexts is an argument, and every theorem quantifies over all such orderings. An active set emptied off the good event has minimum count $+\infty$, and the algorithm then plays action $0$.
• Definition 3. "$a^\star(c)=\arg\max_aR_{c,a}$" is read as some selection of maximisers that is monotone. The independence numbers enter as upper bounds.
• Probabilities. "With probability at least $1-\delta$" means the failure set has measure at most $\delta$. Lemma 2 is stated for every fixed context sequence.
• Rewards in Corollary 1. The quantized auction rewards lie in $[-1,1]$, and Algorithm 3 runs on them as printed. The formalization does not claim that they are a Definition 2 instance.

Not stated here: the adversarial parts of Theorem 5 and Corollary 1, Lemma 3.2, and the contextual form of Lemma 1. Proof contributions are welcome at every level. Useful infrastructure includes an anytime concentration bound for running means under adaptive sampling (the contextual Lemma 1) and Dilworth's theorem for finite posets (the step from $\beta=1$ to general $\beta$ in Lemma 3). Lemmas 3, 4 and 5 can be attacked first and independently.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
• N. Alon, N. Cesa-Bianchi, O. Dekel, T. Koren, Online Learning with Feedback Graphs: Beyond Bandits, COLT 2015. https://arxiv.org/abs/1502.07617
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• R. P. Dilworth, A Decomposition Theorem for Partially Ordered Sets, Annals of Mathematics 51(1), 1950. https://doi.org/10.2307/1969503