Machine Learning

Motivation

Spectral clustering recovers group labels from a similarity matrix: compute its leading eigenvectors, embed each point as a row of the eigenvector matrix, and cluster the rows with k-means. It is a standard last step of convex-relaxation methods for clustering, which first estimate a clustering matrix $X$ (with $X_{ij} = 1$ when $i$ and $j$ belong to the same cluster) and then have to turn the estimate back into labels.

Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) estimate $X$ by a linear program on a thresholded Gaussian kernel and then round it this way (Algorithm 1, steps 3–4). Their Theorem 2 controls the error of the rounding step in terms of the $\ell_1$ error of the estimate. The argument follows Lei and Rinaldo (Ann. Statist. 43(1), 2015), who analysed spectral clustering for stochastic block models with a polynomial-time $(1+\epsilon)$-approximate k-means step, combined with the Davis–Kahan theorem in the form of Yu, Wang and Samworth (Biometrika 102(2), 2015). The same pattern, "matrix estimation error ⇒ eigenvector error ⇒ misclassification count", recurs throughout the analysis of SDP and spectral methods for community detection and mixture models.

Setting

There are $n$ points and $r$ clusters. A fixed labelling $\varphi : [n] \to [r]$ gives clusters $C_k = \{i : \varphi(i) = k\}$ of sizes $n_k \ge 1$, and $n_{\min} = \min_k n_k$. The true clustering matrix is $X^0_{ij} = 1$ if $\varphi(i) = \varphi(j)$ and $0$ otherwise. Its scaled membership matrix is

$$U^0 = Z^0\,\mathrm{Diag}(1/\sqrt{n_1},\dots,1/\sqrt{n_r}),\qquad U^0_{ik} = \begin{cases} 1/\sqrt{n_k} & \varphi(i) = k,\\ 0 & \text{otherwise.}\end{cases}$$

The estimate $\hat X \in \mathbb R^{n\times n}$ is any symmetric matrix with entries in $[0,1]$. Spectral rounding takes a matrix $\hat U \in \mathbb R^{n\times r}$ of orthonormal eigenvectors of $\hat X$ for its $r$ largest eigenvalues (ties broken arbitrarily), and runs k-means on the rows of $\hat U$. A membership matrix $\Theta \in \mathbb M_{n,r}$ is a $\{0,1\}$-matrix with exactly one $1$ per row; a pair $(\hat\Theta, \hat B)$ with $\hat B \in \mathbb R^{r\times r}$ is a $(1+\epsilon)$-approximate k-means solution on the rows of $\hat U$ if

$$\|\hat U - \hat\Theta\hat B\|_F^2 \le (1+\epsilon)\min_{\Theta\in\mathbb M_{n,r},\, B\in\mathbb R^{r\times r}}\|\hat U - \Theta B\|_F^2 .$$

Let $O$ be an optimal rotation, an orthogonal $r\times r$ matrix minimising $\|\hat U - U^0O\|_F$. With $v_i$ and $\bar v_i$ the rows of $U^0O$ and $\hat\Theta\hat B$, the misclassified set of cluster $k$ is

$$\mathcal S_k = \Big\{ i \in C_k : \|\bar v_i - v_i\| \ge \tfrac{1}{2\sqrt{n_k}} \Big\}.$$

Norms: $\|A\|_1 = \sum_{i,j}|A_{ij}|$ (entrywise), $\|A\|_F^2 = \sum_{i,j}A_{ij}^2$.

Formalization targets

Goal: Theorem 2, (15), without outliers

For every $\hat X$, $\hat U$, $(\hat\Theta,\hat B)$ and optimal $O$ as above and every $\epsilon > 0$,

$$\sum_{k\in[r]}\frac{|\mathcal S_k|}{n_k} \;\le\; 64(2+\epsilon)\,\frac{\|X^0 - \hat X\|_1}{n_{\min}^2}.$$

Milestones

1. Davis–Kahan (Theorem 3, case $s=1$): an eigengap $g$ of a symmetric $\Sigma$ below its top $r$ eigenvalues gives an orthogonal $\hat O$ with $\|U - \hat U\hat O\|_F \le 2^{3/2}\|\hat\Sigma - \Sigma\|_F/g$.
2. Eigenstructure of $X^0$: $U^0$ consists of top-$r$ eigenvectors of $X^0$ with eigenvalues $n_1,\dots,n_r$, and $X^0$ vanishes on the orthogonal complement, so the eigengap is $n_{\min}$.
3. (G.6)(iii): $\|A - B\|_F^2 \le \|A - B\|_1$ for matrices with entries in $[0,1]$.
4. (G.6): $\|\hat U - U^0 O\|_F^2 \le 8\|\hat X - X^0\|_1/n_{\min}^2$.
5. Lemma 5, (G.4) (Lei–Rinaldo): for $V = \Theta^*B^*$ and a $(1+\epsilon)$-approximate k-means solution on any $\hat V$, $\sum_k |\mathcal S_k|\delta_k^2 \le 4(4+2\epsilon)\|V - \hat V\|_F^2$.
6. Centre separation: the rows of $B^* = \mathrm{Diag}(1/\sqrt{n_k})O$ satisfy $\|b^*_l - b^*_k\| = \sqrt{1/n_k + 1/n_l}$.

Companion: permutation recovery

If $64(2+\epsilon)\|X^0 - \hat X\|_1/n_{\min}^2 \le 1$, the k-means labels agree with $\varphi$ up to one permutation of $[r]$ on every point outside $\bigcup_k\mathcal S_k$.

Significance

Inequality (15) separates the analysis of the algorithm into an estimation part (how close $\hat X$ is to $X^0$ in $\ell_1$, Theorem 1 of the paper) and a purely deterministic rounding part. Any estimator of the clustering matrix with entries in $[0,1]$ — the Robust-LP, the SDP relaxations of Peng–Wei or Amini–Levina, a thresholded kernel — inherits a misclassification bound from its $\ell_1$ error through this one statement, with an explicit constant. The companion statement shows that the sets $\mathcal S_k$ really are the misclassified points.

The result is proved on paper; none of it is formalized. Mathlib has the spectral theorem for Hermitian matrices but no eigenspace perturbation bound of Davis–Kahan type, and the platform has no k-means approximation lemma for membership matrices. A machine-checked Davis–Kahan theorem in Frobenius norm and a machine-checked Lei–Rinaldo lemma are reusable well beyond this paper: they are the two standard ingredients of every spectral clustering guarantee for block models and mixtures.

Difficulty

The k-means part is elementary but bookkeeping-heavy: the comparison point in the $(1+\epsilon)$ bound must be a feasible k-means solution, which is why the true embedding $U^0O$ has to factor as a membership matrix times a centre matrix. The main obstacle is the Davis–Kahan step. The naive route through individual eigenvectors fails when eigenvalues of $\hat X$ or of $X^0$ are repeated (here $X^0$ has eigenvalue $n_k$ with multiplicity whenever cluster sizes coincide), and only the subspace is stable; the bound must be stated up to an orthogonal matrix and proved for the whole eigenspace, with no ordering or separation assumption on the eigenvalues of $\hat X$.

Formalization scope

Points are Fin n, clusters Fin r, matrices Matrix ι κ ℝ; the norms are explicit sums, not Mathlib's matrix norm instances. The labelling $\varphi$ is fixed; membership matrices are encoded by assignments $a : [n]\to[r]$, and "$\le (1+\epsilon)\min$" by "$\le (1+\epsilon)\cdot$ the cost of every assignment and every centre matrix". "Top-$r$ eigenvectors" is variational: orthonormal columns, eigenvector equations, and every Rayleigh quotient on the orthogonal complement at most each selected eigenvalue. $n_{\min}$ is a finite minimum and requires $r \ge 1$.

Departures from the printed text, each disclosed in the item concerned:

• No outliers ($m = 0$). The printed Theorem 2 allows outliers; it is false for $m \ge 1$, because the outlier rows of $U^0$ are zero, so the true embedding is not k-means feasible and Lemma 5 does not apply. A counterexample with two clusters of size $M > 256$, one isolated outlier and $\epsilon = 2$ violates (15).
• No probability, no $\bar\epsilon$, no separation condition. (15) is deterministic in $\|X^0 - \hat X\|_1$; the printed probabilistic hypotheses only feed Theorem 1 into the permutation claim.
• The printed $n_{\min} > r$ is replaced by the weaker $n_k \ge 1$.
• Davis–Kahan is stated for the leading eigenspace ($s = 1$), the only case used.
• In Lemma 5 the thresholds are required to satisfy $\delta_k \ge 0$, which the page leaves implicit; for a negative $\delta_k$ the bound (G.4) fails at $\hat V = V$.

The goal quantifies over every optimal rotation $O$, not over some orthogonal matrix chosen afterwards (which could make $\mathcal S_k$ empty), and over every top-eigenvector matrix and every approximate k-means solution; a formalization that fixes $\hat U$ to good eigenvectors, compares only against the true labels, or drops the eigenvalue-dominance clause (allowing bottom eigenvectors) proves a different and partly false statement.

Contributions welcome: Davis–Kahan in Frobenius norm for symmetric real matrices (general $s$ included), the Lei–Rinaldo lemma in full, and the eigenstructure of block-constant matrices.

Selected references

• P. R. Srivastava, P. Sarkar, G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, arXiv:1912.07546v3, 2021; Operations Research 71(1), 2023. https://arxiv.org/abs/1912.07546
• J. Lei, A. Rinaldo, Consistency of spectral clustering in stochastic block models, Annals of Statistics 43(1), 215–237, 2015. https://doi.org/10.1214/14-AOS1274
• Y. Yu, T. Wang, R. J. Samworth, A useful variant of the Davis–Kahan theorem for statisticians, Biometrika 102(2), 315–323, 2015. https://doi.org/10.1093/biomet/asv008
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM Journal on Numerical Analysis 7(1), 1–46, 1970. https://doi.org/10.1137/0707001

Learning to bid in first-price auctions

Most online advertising inventory is sold one impression at a time in automated auctions, and since about 2019 the major ad exchanges have moved from second-price to first-price rules: the highest bidder wins and pays its own bid. A bidder in a first-price auction must trade off winning probability against the price paid, and that trade-off depends on the unknown distribution of competing bids. A bidder who takes part in many such auctions can learn that distribution as it goes. The natural yardstick is regret: the expected shortfall of the bidder's cumulative reward relative to an oracle that knows the distribution of competing bids from the start.

Han, Zhou and Weissman (arXiv:2003.09795, Operations Research, 2025) give bidding policies whose expected regret is $\widetilde O(\sqrt T)$ over $T$ auctions, both for iid and for adversarial private values, under the censored feedback that real exchanges provide (only the winning bid is announced). Their Theorem 9 shows that the $\sqrt T$ rate cannot be improved, even in a much easier setting. This mission is that lower bound.

Related results put it in context. With binary feedback (only "won" or "lost"), regret of order $T^{2/3}$ is unavoidable (Kleinberg and Leighton, 2003). With a fixed value, repeated first-price bidding is a pricing problem on a one-dimensional action set whose reward $(1-b)G(b)$ need not be continuous in $b$. Theorem 9 shows that the extra information of the full competing bid buys $\sqrt T$ and nothing better.

Setting

In each round $t=1,\dots,T$ a bidder has a private value $v_t\in[0,1]$, submits a bid $b_t\in[0,1]$, and faces the highest other bid (HOB) $m_t\in[0,1]$, the largest bid of all competitors. The bidder wins when $b_t\ge m_t$, and its payoff is

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

The HOBs $m_1,\dots,m_T$ are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$. No smoothness is assumed: $G$ may have atoms. The expected reward of bid $b$ at value $v$ is $R(v,b)=(v-b)G(b)$, and the regret of the bids $b_1,\dots,b_T$ is

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

A policy $\pi$ chooses $b_t$ from what it has observed before round $t$, and it may use internal randomness. Theorem 9 makes the problem as easy as possible: the value is $v_t=1$ in every round, and the HOB $m_t$ is revealed at the end of every round (full information), rather than only when the bidder loses. A policy is then a rule $b_t=\beta_t(u,m_1,\dots,m_{t-1})$, where $u$ is the policy's internal randomness.

The lower bound uses two HOB laws on $\{1/3,2/3\}$. For $\Delta\in(0,1/4)$, $G_1$ puts mass $\tfrac12+\Delta$ on $1/3$ and $\tfrac12-\Delta$ on $2/3$, and $G_2$ the reverse. $P_i^{\otimes T}$ is the law of $T$ iid HOBs from $G_i$. The total variation distance is $\|P-Q\|_{\mathrm{TV}}=\tfrac12\int|dP-dQ|$, and $D_{\mathrm{KL}}(P\|Q)=\int dP\log\frac{dP}{dQ}$ is the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 9 (p. 36)

There is an absolute constant $c>0$ such that, for every horizon $T\ge1$,

$$\inf_\pi\sup_G\ \mathbb E_G\bigl[R_T(\pi;v)\bigr]\ \ge\ c\sqrt T,\qquad v_t\equiv 1,$$

where the supremum is over all HOB distributions on $[0,1]$ and the infimum is over all full-information policies, randomized ones included. The constant is left unspecified, as in the paper; the paper's proof gives $c=1/(24e^2)$.

Milestones (App. A–B, pp. 36–38)

1. Oracle rewards (p. 37): with $v_t=1$, $\max_b(1-b)G_1(b)=(1+2\Delta)/3$, $\max_b(1-b)G_2(b)=1/3$ and $\max_b(1-b)(G_1+G_2)(b)=2/3$.
2. Separation (20): for every bid $b_t\in[0,1]$, the instantaneous regrets under $G_1$ and $G_2$ sum to at least $2\Delta/3$.
3. Two-point reduction (21): for every policy, $\tfrac12\mathbb E_{G_1}[R_T]+\tfrac12\mathbb E_{G_2}[R_T]\ge\frac{\Delta T}{3}\bigl(1-\|P_1^{\otimes T}-P_2^{\otimes T}\|_{\mathrm{TV}}\bigr)$.
4. Lemma 12: $1-\|P-Q\|_{\mathrm{TV}}\ge\tfrac12\exp\bigl(-(D_{\mathrm{KL}}(P\|Q)+D_{\mathrm{KL}}(Q\|P))/2\bigr)$.
5. KL computation (p. 37): $D_{\mathrm{KL}}(P_1^{\otimes T}\|P_2^{\otimes T})=T\,D_{\mathrm{KL}}(G_1\|G_2)\le32T\Delta^2$.
6. (22): $1-\|P_1^{\otimes T}-P_2^{\otimes T}\|_{\mathrm{TV}}\ge\tfrac12\exp(-32T\Delta^2)$.

Significance

The theorem shows that the upper bounds of the paper, $C\sqrt T\log^{2.5}T$ for iid values and $C\sqrt T\log^3T$ for adversarial values, are optimal up to logarithmic factors. Because the lower bound holds with a constant value and with every HOB revealed, it is not caused by censoring or by the value process. The $\sqrt T$ comes from the statistical difficulty of locating the maximizer of $(1-b)G(b)$ when $G$ is learned from samples. The same lower bound therefore applies to every richer feedback model and every value model that contains the constant sequence.

The milestones are general tools. Lemma 12 (a symmetrised Bretagnolle–Huber inequality), the product rule for KL divergences of iid laws, and the reduction (21) are the standard steps of Le Cam's two-point method. They recur in essentially every minimax lower bound for bandits and online learning.

The theorem has a complete proof in the paper (App. B). As far as is known it has not been machine-checked, and the needed pieces are only partly in Mathlib: there is a Kullback–Leibler divergence with a chain rule, but at the pinned revision there is no total variation distance and no Bretagnolle–Huber or Le Cam inequality. The work is to formalize the known proof.

Difficulty

The arithmetic is elementary, and the difficulty lies in the probabilistic reduction. The first idea, bounding the regret round by round under a single law, fails: for any fixed $G$ a policy that happens to bid the right point has zero regret, so the lower bound must come from a policy's inability to know which of two laws it faces. Making that precise requires the law of the observed history $(m_1,\dots,m_{t-1})$ under each hypothesis, the identity $\int\min\{dP,dQ\}=1-\|P-Q\|_{\mathrm{TV}}$, and monotonicity of total variation under marginalization from $T$ to $t-1$ coordinates. A randomized policy adds one more integration, over its internal randomness, before the per-round bound applies. The KL step needs the tensorization of KL over product measures and an elementary but explicit logarithmic inequality.

Formalization scope

All declarations live in the namespace FirstPriceLearning.LowerBound.

• Time. Rounds are Fin T; Lean round t is paper time $t+1$.
• HOB law. A measure μG on ℝ. The goal asks for a probability measure giving no mass outside $[0,1]$. The CDF is (μG (Set.Iic x)).toReal, with atoms allowed.
• Reward and regret. $R(v,b)=(v-b)G(b)$, and the oracle term is the supremum over $b\in[0,1]$ (a bounded nonempty family, attained). The regret is the pseudo-regret (3), a sum of expected-reward gaps.
• Policies. A policy carries a probability space $(U,\mu_U)$, with U : Type, for its internal randomness and bid maps bid t : U → (Fin t → ℝ) → ℝ that are jointly measurable with values in $[0,1]$. The history type Fin t → ℝ makes the policy non-anticipating by construction: it cannot read $m_t$ or later HOBs, and it never sees $G$.
• Expectation. An integral over $u\sim\mu_U$ independent of $m\sim G^{\otimes T}$ (Measure.prod with Measure.pi).
• Quantifiers. The goal is stated as $\exists c>0\ \forall T\ge1\ \forall\pi\ \exists G$, which implies the inf–sup form. The constant precedes $T$ and the policy, and the law is chosen after the policy.
• Divergences. KL is Mathlib's InformationTheory.klDiv, valued in $[0,\infty]$. Total variation is defined locally as $\tfrac12\int|p-q|\,d(P+Q)$ with Radon–Nikodym densities. In Lemma 12 the right-hand side is $0$ when a divergence is infinite ($\exp(-\infty)=0$).
• Hard laws. $G_1,G_2$ are explicit two-point measures; the milestones (20)–(22) are stated for $\Delta\in(0,1/4)$ as printed.

Two trivializing formalizations are excluded. A policy that observes $m_t$ (or $G$) before bidding would make the bound false rather than trivial, and the types forbid it. A non-measurable bid map would make the expectation the junk value $0$, and measurability is required. Restricting the policy class to deterministic policies, or reading $(\infty).\mathrm{toReal}=0$ in Lemma 12, would change the theorem and is not done.

Reusable beyond this mission: the total variation distance, Lemma 12, and the tensorization bound for KL. Contributions are welcome at every milestone, especially Lemma 12 and the data-processing step behind (21).

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
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009 (Lemma 2.6). https://doi.org/10.1007/b13794
• J. Bretagnolle, C. Huber, Estimation des densités: risque minimax, Z. Wahrscheinlichkeitstheorie verw. Gebiete 47, 1979. https://doi.org/10.1007/BF00535278
• R. Kleinberg, T. Leighton, The Value of Knowing a Demand Curve: Bounds on Regret for Online Posted-Price Auctions, FOCS, 2003. https://doi.org/10.1109/SFCS.2003.1238232

Motivation

A bidder in repeated first-price auctions faces a learning problem with two kinds of side information. Their private value is a context that changes every round, and the outcome of one bid reveals something about other bids (graph feedback across actions) and about other values (cross learning across contexts). Han, Zhou and Weissman (arXiv:2003.09795v7) abstract this structure into partially ordered contextual bandits and show that, when contexts are iid, an arm-elimination policy has regret $\widetilde O(\sqrt{\alpha\beta T})$ (Theorem 5), with no polynomial dependence on the number of contexts or actions.

Theorem 6 of the same paper asks whether this survives when contexts are chosen by an adversary. It does not: with adversarial contexts every policy suffers regret polynomial in $\min\{\alpha M, K\}$. This separation is what forces the paper to look beyond the partially ordered structure for its $\widetilde O(\sqrt T)$ adversarial-value result (Theorem 2). The lower bound is also of independent interest for contextual bandits with cross learning (Balseiro et al., NeurIPS 2019) and with feedback graphs (Alon et al., COLT 2015).

Setting

A stochastic contextual bandit with graph feedback and cross learning (Definition 2, p. 14) has a horizon $T$, $M$ contexts $\mathcal C$, $K$ actions $\mathcal A$, a joint reward law $P$ on $[0,1]^{\mathcal C\times\mathcal A}$ with means $R_{c,a}$, and a directed graph $G=(\mathcal A,E)$ without self-loops. In round $t$ the learner sees a context $c_t$, picks $a_t$, nature draws a fresh reward vector $r_t\sim P$, and the learner observes $r_{t,c,a}$ for every context $c$ and every $a\in I_t=\{a_t\}\cup\{a:(a_t,a)\in E\}$. The regret (5) is

$$R_T(\pi)=\sum_{t=1}^T\Big(\max_{a\in\mathcal A}R_{c_t,a}-R_{c_t,a_t}\Big).$$

The independence number $\alpha$ of $G$ is the size of a largest set of actions with no edge between any two of them; for a partial order, $\beta$ is the size of a largest set of pairwise incomparable elements.

The instance is a partially ordered contextual bandit (Definition 3, pp. 16–17) if $G$ is a DAG equal to its own transitive closure, so that $a_1\preceq_G a_2$ iff $a_1=a_2$ or $(a_1,a_2)\in E$ is a partial order, and there is a partial order $\preceq_{\mathcal C}$ on contexts with $c_1\preceq_{\mathcal C}c_2\Rightarrow a^\star(c_1)\preceq_G a^\star(c_2)$ for optimal actions $a^\star(c)\in\arg\max_a R_{c,a}$.

A policy $\pi$ chooses $a_t$ from its internal randomness, the contexts $c_1,\dots,c_t$ and the earlier observations. The context sequence is oblivious: fixed in advance, possibly depending on $\pi$ but not on its random draws.

Formalization targets

Goal: Theorem 6 in the regime of its proof

For integers $\alpha\ge1$, $M\ge1$, with $K=(\alpha+1)M$, $K^3\le T$ and $M\mid T$: there is a feedback graph $G$ on $K$ actions with independence number $\alpha$ such that for every policy $\pi$ there are a reward law $P$ (making $(G,P)$ partially ordered with the total order on contexts, $\beta=1$) and contexts $(c_t)$ with

$$\mathbb E[R_T(\pi)]\ \ge\ \frac{\sqrt{KT}}{32e^3}.$$

Because $\alpha M\le K$, this is at least $\frac1{32e^3}\min\{\sqrt{\alpha MT},\sqrt{KT},T^{2/3}\}$, the printed form of Theorem 6, in this regime.

Milestones

Along the proof (pp. 22–24): the construction is a partially ordered contextual bandit with $\beta=1$ and independence number $\alpha$; properties 1–4 of the mean rewards; property 5, the KL divergence of the observed rewards; the regret decomposition (7); the testing lemma (Lemma 13, p. 36)

$$\frac1n\sum_{i=1}^nQ_i(\Psi\ne i)\ \ge\ \frac1{2n}\sum_{i=2}^n e^{-D_{\mathrm{KL}}(Q_1\|Q_i)};$$

the self-referential inequality (8)

$$R_T\ \ge\ \frac{\sqrt{KT}}{16e^3}\exp\Big(-\frac{16KR_T}{3T}\Big),\qquad R_T=\max_u\mathbb E_u[R_T(\pi)];$$

and the final step $R_T\ge\sqrt{KT}/(32e^3)$.

Significance

The theorem separates stochastic from adversarial contexts. Under iid contexts, Theorem 5 gives $\widetilde O(\sqrt{\alpha\beta T})$; with adversarial contexts, even when $\beta=1$, regret must grow like $\sqrt{\alpha MT}$, matching the upper bound of Theorem 4 up to logarithms. For first-price auctions with adversarial values (Remark 2), the bound shows that the partially ordered structure alone cannot give $\widetilde O(\sqrt T)$; the paper's $\widetilde O(\sqrt T)$ algorithm must use the extra correlation of auction rewards.

The paper proves the theorem in full. As far as we know, none of it has been formalized; in particular, no machine-checked version of a Bayesian multi-hypothesis lower bound for bandits with graph feedback and cross learning exists. A formal proof will produce reusable pieces: Lemma 13 is a general testing inequality; the KL chain rule for adaptively collected bandit observations, with feedback revealed on a graph, is needed for any information-theoretic bandit lower bound; and the interaction model is shared with the paper's upper bounds.

Difficulty

The standard minimax argument for $K$-armed bandits compares two instances that differ in one arm, and the regret follows directly from a testing error. Here that argument fails: feedback graphs and cross learning mean that pulling one arm can reveal everything, and a policy may pay to explore. The proof instead plays a uniform prior over $(\alpha+1)^M$ instances and obtains an inequality in which the maximal regret $R_T$ appears on both sides, (8). If the regret is small, the policy has not explored enough to tell the instances apart, which in turn forces large regret. Making this rigorous requires the chain rule of KL divergence over the adaptively chosen observations, the specific ordering of contexts (decreasing over blocks, so early observations say nothing about late optimal actions), and the regime $K^3\le T$ to close the self-referential bound.

Formalization scope

• Contexts are Fin M, rounds Fin T (paper index = Lean index + 1). The goal uses actions Fin K; the construction uses Fin M × Fin (α + 1), with $j=0$ the action $(i,0)$.
• A reward law is a measure on Fin M → A → ℝ. Definition 2 requires a probability measure carried by $[0,1]^{M\times K}$ and a graph without self-loops. Means are integrals, and $\max_a$ is a supremum over the finite action set.
• Definition 3's "DAG equal to its transitive closure" is encoded as "no self-loops and transitive". The printed $\arg\max$ is read as a selection of maximisers.
• Independence numbers are exact: a set of the given size exists, and none is larger.
• Policies are randomized and non-anticipating. The action is a measurable function of the internal randomness (an arbitrary probability space), the contexts so far and the past observations, and the argument types enforce non-anticipation. An observation is the reward vector with unrevealed coordinates set to $0$; the learner knows its own action, so this carries exactly the revealed rewards. Deterministic-only policies would give a weaker theorem, and they are not the class used.
• Expected regret integrates over the internal randomness and iid reward vectors, with the context sequence fixed.
• KL divergence is Mathlib's $[0,\infty]$-valued klDiv. In Lemma 13, $e^{-\infty}$ is read as $0$, so an infinite divergence cannot be truncated to $0$ and inflate the right side.
• The reduction from general $(M,K,T)$ by "dummy contexts and actions" (p. 21) is not formalized. It needs $\min\{K,(\alpha+1)M,T^{1/3}\}\ge\alpha+1$, and the printed theorem is false at $K=1$. The hypotheses $M\mid T$ and $\alpha\ge1$ replace the paper's "without loss of generality".
• Property 5 assumes $u_c\neq0$, because for $u_c=0$ the two laws coincide. (7) is stated for each $u$, which implies the printed form for the maximum.

Needed infrastructure: Bernoulli product measures and their KL divergence, the KL chain rule for the law of an adaptive interaction, and a Bretagnolle–Huber-type inequality. Contributions of these general lemmas, and of the measurability facts for the interaction, 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. https://arxiv.org/abs/2003.09795
• Z. Gao, Y. Han, Z. Ren, Z. Zhou, Batched Multi-armed Bandits Problem, NeurIPS 2019 (source of Lemma 13). https://arxiv.org/abs/1904.01763
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• N. Alon, N. Cesa-Bianchi, O. Dekel, T. Koren, Online Learning with Feedback Graphs: Beyond Bandits, COLT 2015. https://arxiv.org/abs/1502.07617
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794

Motivation

In a first-price auction the highest bidder wins and pays her own bid. Display advertising moved to first-price auctions around 2019, and a bidder who participates in millions of them faces a learning problem: at each round $t$ she sees a private value $v_t\in[0,1]$ for the item, bids $b_t\in[0,1]$, and wins when $b_t$ is at least the highest other bid (HOB) $m_t$, earning $(v_t-b_t)\mathbb 1(b_t\ge m_t)$. Since the HOB is unknown, she must learn how much to shade her bid.

Han, Zhou and Weissman (arXiv:2003.09795v7, Operations Research, 2025) show that when the HOBs are iid draws from an unknown distribution, a bidder can achieve regret $\widetilde O(\sqrt T)$ against the oracle that knows the distribution, whether the values are iid or chosen by an oblivious adversary, and with only censored feedback. Their §2.2 justifies the iid assumption by the size of the bidder population, and notes that learning "could become impossible even when the iid assumption is only slightly violated". Section 5.2 makes this precise. This mission formalizes that impossibility result, Theorem 8.

Setting

Fix a horizon $T$. Values $v=(v_1,\dots,v_T)\in[0,1]^T$ form an oblivious sequence, fixed in advance. Fix two probability laws $P,Q$ on $[0,1]$ and a threshold $v^\star$. The HOBs are independent across rounds with

$$m_t\sim P\ \text{ if } v_t<v^\star,\qquad m_t\sim Q\ \text{ if } v_t\ge v^\star .$$

Feedback is full information: $m_t$ is revealed at the end of round $t$. The laws $P,Q$ are known to the bidder; only $v^\star$ is not.

The payoff of bid $b$ against HOB $m$ at value $v$ is $r(v,b;m)=(v-b)\mathbb 1(b\ge m)$ (ties are won). For a law $\mu$ of the HOB with CDF $G$, the expected reward is $R(v,b)=(v-b)G(b)$, and the oracle reward is $\max_{b\in[0,1]}R(v,b)$.

A policy $\pi$ draws internal randomness $u$ once and bids $b_t=\pi_t(u;v_1,\dots,v_t;m_1,\dots,m_{t-1})\in[0,1]$. Its expected regret is

$$\mathbb E[R_T(\pi;v^\star,v)]=\sum_{t=1}^T\Big(\max_{b\in[0,1]}\mathbb E_{m\sim L_t}\big[(v_t-b)\mathbb 1(b\ge m)\big]-\mathbb E\big[(v_t-b_t)\mathbb 1(b_t\ge m_t)\big]\Big),$$

with $L_t=P$ if $v_t<v^\star$ and $L_t=Q$ otherwise: the oracle knows $v^\star$ and bids optimally at every round.

Formalization targets

Goal: Theorem 8 (p. 34)

There are an absolute constant $c>0$ and laws $P,Q$ on $[0,1]$ such that for every $T$ and every policy $\pi$ there are a threshold $v^\star\in[0,1]$ and values $v\in[0,1]^T$ with

$$\mathbb E[R_T(\pi;v^\star,v)]\ \ge\ c\,T .$$

The constant is existential, which is the paper's $\Omega(T)$; the value $1/16$ obtained in the paper's argument is not hard-coded.

Milestones (p. 34)

The paper's argument consists of a hard family indexed by signs $u\in\{\pm1\}^T$, with thresholds $f(u)=\frac12+\frac14\sum_t u_t/2^t$ and values $v_1=\frac12$, $v_{t+1}=v_t+u_t/2^{t+2}$, and four displayed claims:

1. the lexicographic order $f(\dots,u_{t-1},1,\dots)>f(\dots,u_{t-1},-1,\dots)$;
2. the sign identity $\operatorname{sign}(v_t-v^\star)=-\operatorname{sign}(u_t)$ for $v^\star=f(u)$;
3. the oracle reward $v_t-m_t$ with $m_t=\frac18\mathbb 1(v_t\ge v^\star)$ under $P=\delta_0$, $Q=\delta_{1/8}$, and $v_t\in[\frac14,\frac34]$;
4. the posterior-reward bound $\mathbb E_{m\sim\mathrm{Unif}\{0,1/8\}}[(v-b)\mathbb 1(b\ge m)]\le v-\frac18$ for $v\ge\frac14$;

and the Bayesian bound: averaged over uniform $u$, every policy has expected regret at least $T/16$.

Significance

The result. The upper bounds of the paper rely on the HOBs being iid and independent of the bidder's value. Theorem 8 shows that this cannot be relaxed to a mild form of dependence: one threshold, two known laws and full-information feedback already force linear regret against the per-round oracle. The paper concludes that a weaker benchmark is needed once HOBs may depend on values, and leaves that benchmark open.

Formalizing it. The theorem is proved in the paper, on one page; it is not known to be machine-checked. A formal proof pins down the quantifier order (the constant and the laws chosen before the policy, the threshold and values after it), the policy class (randomized, full information) and the treatment of ties, and it provides a reusable model of non-anticipating randomized bidding policies with full-information feedback.

Difficulty

The obvious attempt is to fix a threshold and values and argue that the bidder cannot know on which side of $v^\star$ each $v_t$ falls. For any fixed instance this fails: a policy can be tuned to that instance and bid optimally, with zero regret. The lower bound must therefore pass through an average over a family of instances. The family has to make the side of the threshold at round $t$ independent of everything the bidder has seen up to round $t$, including the past HOBs, which in full information reveal the past sides exactly. The dyadic construction does this. The formal difficulty is the bookkeeping: expressing the expected regret of an arbitrary randomized policy as an integral over its internal randomness and the HOBs, and exchanging the average over $u$ with that integral so that the conditional uniformity of $m_t$ can be used.

Formalization scope

• Time. Rounds are Fin T; Lean round $t$ is the paper's round $t+1$.
• Laws and CDF. HOB laws are Measure ℝ, with probability and support in $[0,1]$ required of the existential witnesses $P,Q$. The CDF is $G(x)=\mu((-\infty,x])$. Atoms are allowed, as in the paper; the construction uses point masses.
• Oracle. $\max_{b\in[0,1]}R(v,b)$ is the supremum over the subtype $[0,1]$; no arg max $b^\star_P(v)$ is chosen. The paper's two-term regret $\mathbb 1(v_t<v^\star)\mathbb E_P[\cdot]+\mathbb 1(v_t\ge v^\star)\mathbb E_Q[\cdot]$ is written with the law $L_t$.
• Policies. A structure with a probability space of internal randomness and, for each round, a jointly measurable bid map of the randomness, $v_1,\dots,v_t$ and $m_1,\dots,m_{t-1}$, with values in $[0,1]$. The types prevent reading $m_t$ or $v^\star$. Deterministic policies are the case of a one-point randomness space.
• Expectation. The bidder's expected payoff at round $t$ is a Bochner integral over the product of the policy's randomness law and the product law of $(m_1,\dots,m_T)$. A local check confirms that this integrand is measurable and bounded, so the integral is never Lean's junk value $0$, which would trivialize the lower bound.
• Knowledge of $(P,Q)$. The laws are fixed before $T$ and $\pi$; a policy chosen afterwards may depend on them. This encodes "revealed to the bidder" and is stronger than choosing $(P,Q)$ after $\pi$.
• Ties. $\mathbb 1(b\ge m)$ throughout; the oracle bids $b=m_t=1/8$ and wins.

A formalization in which the threshold or the values are chosen before the policy, the bid reads $m_t$, the expected payoff is not integrable, or the oracle bids a fixed price, is a different and easier statement; all four are excluded by the definitions above.

Contributions welcome: proofs of the four displayed claims (elementary real analysis on dyadic sums and on point masses), the Bayesian bound (the measure-theoretic core), and the step from the Bayesian bound to the goal. The policy and regret definitions are reusable for other full-information lower bounds in this series.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; read as arXiv:2003.09795v7, §5.2, pp. 33–34. https://arxiv.org/abs/2003.09795

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 1 (p. 25)

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

This mission develops Chapter 5 of A Survey of Quantum Learning Theory by Srinivasan Arunachalam and Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

This is a corrected form of the Atıcı–Servedio theorem on learning juntas from uniform quantum examples.

A function $f:\{0,1\}^n\to\{0,1\}$ is a $k$-junta if it depends on at most $k$ of its $n$ input bits. A uniform quantum example of $f$ is the $(n+1)$-qubit state $\sum_{x\in\{0,1\}^n}2^{-n/2}|x,f(x)\rangle$; a uniform classical example is a pair $(x,f(x))$ with $x$ uniform on $\{0,1\}^n$. The error of a hypothesis $h$ is $\Pr_{x}[h(x)\neq f(x)]$ for uniform $x$.

Time is measured in the following hybrid cost model, which is the one the source's proof sketch counts in. A learner (1) applies a circuit over the gate set $\{H,T,\mathrm{CNOT}\}$ to $T_Q$ uniform quantum examples and some ancillas in $|0\rangle$ and measures every qubit in the computational basis; (2) maps the outcome by a Boolean circuit of AND/OR/NOT gates to a set $V\subseteq[n]$ of variables; (3) reads $T_C$ uniform classical examples and outputs the truth-table hypothesis $h(x)=f(x_j)$ for the first example $x_j$ that agrees with $x$ on $V$ ($h(x)=0$ if there is none). Its time is the number of quantum gates, plus the number of measured qubits, plus the number of Boolean gates, plus $T_C$ (one unit per classical example, which is read and written into the table cell indexed by its $V$-bits), plus $2^{|V|}$ table cells (worst case over the outcomes).

For every $\delta\in(0,1)$ there is a constant $C>0$ such that for all $n,k$ with $2\le k\le n$ and all $\varepsilon\in(0,1/2]$ there is such a learner with

$$T_Q\le C\,\frac{k\log k}{\varepsilon},\qquad T_C\le C\,2^k\log\frac1\varepsilon,\qquad \mathrm{time}\le C\Big(\frac{nk\log k}{\varepsilon}+2^k\log\frac1\varepsilon\Big),$$

which, for every $k$-junta $f$, outputs with probability at least $1-\delta$ (over the measurement outcomes and the classical examples) a hypothesis of error at most $\varepsilon$.

The theorem shows that quantum examples remove the $n^{\Theta(k)}$ search over candidate variable sets that the best known classical learners need, which is why juntas are a notorious bottleneck classically.

Formalization Note The source states no cost model, no confidence parameter, and $O(2^k)$ classical examples. The cost model above, the fixed-confidence reading (constants depend on $\delta$ only), and the $O(2^k\log(1/\varepsilon))$ classical examples of the source's own proof sketch are the corrections. The thresholds $k\ge2$ and $\varepsilon\le1/2$ make $\log k$ and $\log(1/\varepsilon)$ positive.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 5.4: Atıcı–Servedio: time-efficient quantum learning of k-juntas (corrected).

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Srinivasan Arunachalam and Ronald de Wolf, A Survey of Quantum Learning Theory, 2017, v3. https://arxiv.org/pdf/1701.06806v3.

Why parameter-free regret matters

In online convex optimization, a learner makes a prediction before seeing the next loss. A standard regret guarantee often depends on a learning rate chosen using the size of the comparator that will be assessed later. That comparator is unknown during play. Chapter 13 of Orabona's textbook uses coin betting to obtain a bound that adapts to every comparator while the algorithm uses only its initial wealth and a bound on the observed subgradients. The coordinate-wise form allows the guarantee to reflect a comparator whose important coordinates differ greatly in size.

The motivating task is deterministic. An adversary may choose convex losses over successive rounds, and the performance measure compares the learner's cumulative loss with the loss of a single fixed vector. The algorithm is allowed to know the coordinate bound $L_\infty$ and its initial wealth parameter $\varepsilon$; it does not know the final comparator $u$ or a suitable learning rate for it. The capstone is Theorem 13.9, p. 215, the chapter's coordinate-wise Krichevsky–Trofimov result.

The learner and the betting rule

There are $T$ rounds, numbered $1,\ldots,T$, in a space $\mathbb R^d$. In round $t$ the learner outputs $x_t$, pays $\ell_t(x_t)$, and then receives a subgradient $g_t$ of the loss at $x_t$. A subgradient supports the loss everywhere: $\ell_t(y)\ge\ell_t(x_t)+\langle g_t,y-x_t\rangle$ for every $y\in\mathbb R^d$. Each coordinate obeys $|g_{t,i}|\le L_\infty$. For a fixed comparator $u$, regret is

$$\operatorname{Regret}_T(u)=\sum_{t=1}^T\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

The underlying KT bettor begins with wealth $\varepsilon>0$. Given coin outcomes $c_t\in[-1,1]$, it wagers a fraction $\beta_t=(\sum_{j=1}^{t-1}c_j)/t$ of its wealth before outcome $c_t$ arrives. Its signed wager is $b_t=\beta_t\operatorname{Wealth}_{t-1}$, and $\operatorname{Wealth}_t=\operatorname{Wealth}_{t-1}+c_tb_t$. The denominator is $t$, including the first round, when the past sum and the wager are zero. Algorithm 13.1, p. 208 defines this update.

For optimization, Algorithm 13.3, p. 215 applies a separate KT update to every coordinate. With $L_\infty>0$, the prediction is fixed by past gradients and past predictions:

$$x_{t,i}=-\frac{\sum_{j=1}^{t-1}g_{j,i}}{L_\infty t} \left(\varepsilon-\sum_{j=1}^{t-1}\frac{g_{j,i}}{L_\infty}x_{j,i}\right).$$

This is the algorithm studied in the target theorem. A run includes the update and an admissible subgradient at each round; it is not an arbitrary sequence of predictions satisfying a bound after the fact.

Formalization targets

The main target records both inequalities in Theorem 13.9. For every comparator $u\in\mathbb R^d$,

$$\operatorname{Regret}_T(u) \le L_\infty\sum_{i=1}^d |u_i|\sqrt{2T\ln\left(1+\frac{e|u_i|T}{\varepsilon}\right)}+d\varepsilon L_\infty \le \|u\|_1L_\infty\sqrt{2T\ln\left(1+\frac{e\|u\|_\infty T}{\varepsilon}\right)}+d\varepsilon L_\infty.$$

The milestone path consists of three statements drawn directly from the chapter: the gamma-potential one-step inequality (13.1), the continuous-coin wealth guarantee of Theorem 13.4, and the one-dimensional KT regret display in §13.2.1. The first controls the change in the betting potential, the second relates that potential to final wealth, and the third is the scalar guarantee used by the coordinate-wise theorem. All three retain the printed constants and the source's one-based indexing.

What the theorem gives

The first inequality charges each comparator coordinate according to its own magnitude. The second expresses the result using familiar $\ell_1$ and $\ell_\infty$ norms. Both apply to the same run without choosing a new algorithm for a new $u$. At $u=0$, the bound is $d\varepsilon L_\infty$, showing directly the cost of the initial-wealth choice. For a sparse or uneven comparator, the coordinate sum can be more informative than a bound that uses only the largest coordinate.

The mathematical results are proved in the cited textbook. This mission supplies Lean statements for those results; the theorem files are proof targets and do not yet contain machine-checked proofs. A completed development would connect the betting potential, the one-dimensional optimization reduction, and the coordinate aggregation through reusable lemmas. Its definition layer can also serve later formalizations of coin-betting algorithms with other wealth potentials.

Where the difficulty lies

The prediction uses a changing wager fraction determined by the previous outcomes. A direct fixed-fraction calculation does not describe that sequence of wagers. The chapter instead identifies a gamma-function potential that can be compared with the changing wealth at every round. For continuous coin outcomes, the potential must satisfy an inequality for every real $c\in[-1,1]$, including interior values rather than only the binary endpoints.

The optimization guarantee adds another boundary: a lower bound on betting wealth must become an upper bound on regret for every real comparator. The desired expression has a logarithm, a square root, and the exact factor $e$ inside it. The coordinate-wise result must preserve the scalar constant in every coordinate and then justify the second inequality involving $\|u\|_\infty$. These are the places where a weaker or altered constant would change the target.

Formalization scope

Lean represents $\mathbb R^d$ as functions Fin d → ℝ; its function norm is the sup norm, while the $\ell_1$ quantity is the explicit sum $\sum_i|u_i|$. The theorem assumes $d\ge1$, $T\ge1$, $\varepsilon>0$, and $L_\infty>0$. These make the finite-dimensional setting nonempty and the printed quotients and logarithms operate on their intended domains. Time index zero is unused. All sums over rounds use $1,\ldots,T$.

Losses are real-valued and subdifferentiable on the whole space, as in Algorithm 13.3. The run records full-space subgradients selected at the learner's predictions and their coordinate bounds. This selected-gradient condition is sufficient for the printed regret inequalities; global boundedness of every possible subgradient is a stronger convention used in the one-dimensional prose. The gamma potential is a separate definition with Real.Gamma; its arguments are positive on the domains used by the wealth theorem. The bettor's wealth is a finite product of its exact per-round returns.

The formalization must keep the explicit update in the run predicate. Allowing $x_t$ to depend on the current $g_t$, or replacing the update by a generic betting rule, would no longer state Algorithm 13.3's guarantee. Contributions are welcome on the gamma-potential inequality, the wealth bound, the one-dimensional regret bound, and the final coordinate aggregation. The supporting results should retain the chapter's constants and handle the first round and zero-valued coin outcomes.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv.