Machine Learning

Completed

Algorithmic Game Theory Bandit Algorithms Operations Research·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 3: Even with Full Information and v_t ≡ 1, Every Bidding Policy Has Worst-Case Expected Regret at Least c√TResearch Paper

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)

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$ .
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$ .
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)$ .
Lemma 12: $1-\|P-Q\|_{\mathrm{TV}}\ge\tfrac12\exp\bigl(-(D_{\mathrm{KL}}(P\|Q)+D_{\mathrm{KL}}(Q\|P))/2\bigr)$ .
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$ .
(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

12 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 5: With Adversarial Contexts and K = (α+1)M ≤ T^(1/3), Every Policy for Partially Ordered Contextual Bandits Has Regret ≥ √(KT)/(32e³)Research Paper

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

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Bandit Algorithms Operations Research·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 6: If the HOB Law Switches at an Unknown Value Threshold, Every Bidding Policy Has Regret Ω(T)Research Paper

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:

the lexicographic order $f(\dots,u_{t-1},1,\dots)>f(\dots,u_{t-1},-1,\dots)$ ;
the sign identity $\operatorname{sign}(v_t-v^\star)=-\operatorname{sign}(u_t)$ for $v^\star=f(u)$ ;
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]$ ;
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

9 thms2 active usersReviewed

Bandit Algorithms Operations Research·Captain: mikedeng1

Optimal No-regret Learning in Repeated First-price Auctions 4: Arm Elimination with Graph Feedback and Cross Learning Has Regret Õ(T ∧ √(αMT) ∧ √(KT)) with High ProbabilityResearch Paper

Motivation

In many sequential decision problems, playing one action reveals the outcome of other actions too. A bidder in a first-price auction who bids $b$ and sees the winning price learns whether every bid at or above that price would have won. A recommender that shows one item learns something about related items. Two kinds of side information recur. Graph feedback across actions: playing action $a$ also reveals the rewards of the out-neighbours of $a$ in a directed graph $G$ (Mannor and Shamir 2011; Alon, Cesa-Bianchi, Dekel and Koren 2015). Cross learning across contexts: the reward of the chosen action is revealed under every context, not only the current one (Balseiro, Golrezaei, Mahdian, Mirrokni and Schneider 2019).

Han, Zhou and Weissman (arXiv:2003.09795v7) reduce learning to bid in repeated first-price auctions to a contextual bandit with both structures. Their §3 starts from a simple arm-elimination algorithm that exploits graph feedback (Algorithm 1) and extends it to contexts with cross learning (Algorithm 2). This mission formalizes that layer: the algorithms, their concentration lemma, and their high-probability regret bounds (Theorems 3 and 4).

Timeline:

2011: Mannor and Shamir introduce bandits with side observations given by a graph.
2015: Alon, Cesa-Bianchi, Dekel and Koren show that for adversarial bandits with a directed feedback graph the minimax regret is $\tilde\Theta(\sqrt{\alpha T})$ , with $\alpha$ the independence number; their Lemma 8 bounds the weak domination number by $50\alpha\log n$ .
2016–2020: Cohen, Hazan and Koren, and Lykouris, Tardos and Wali, give elimination-type algorithms for stochastic bandits with graph feedback.
2019: Balseiro et al. introduce cross learning and obtain $\tilde O(\sqrt{KT})$ regret.
2020–2024: Han, Zhou and Weissman obtain $\tilde O(\sqrt{\min\{\alpha M, K\}T})$ for both structures together (this mission) and use it for first-price auctions.

Setting

A stochastic contextual bandit with graph feedback and cross learning (Definition 2) has a horizon $T$ , contexts $\mathcal C = [M]$ , actions $\mathcal A = [K]$ , a joint reward law $P$ supported on $[0,1]^{M\times K}$ with mean rewards $R_{c,a}$ , and a directed graph $G = (\mathcal A, E)$ without self-loops. In round $t$ a context $c_t$ is revealed, the learner picks $a_t$ , nature draws $r_t = (r_{t,c,a})_{c,a}$ iid from $P$ , and the learner observes $r_{t,c,a}$ for every $c \in \mathcal 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).

Definition 1 is the case $M = 1$ , with regret (4). The independence number $\alpha$ of $G$ is the largest size of a set of actions with no edge between any two of them.

Algorithm 2 keeps for each context $c$ an active set $\mathcal A_{\mathrm{act},c}$ and a minimum count $N_c$ , and for each action $a$ a count $n_a$ shared by all contexts. In each round it plays an action of $\mathcal A_{0,c_t} = \{a\in\mathcal A_{\mathrm{act},c_t} : n_a = N_{c_t}\}$ , either of largest out-degree in the graph restricted to $\mathcal A_{0,c_t}$ (Option I) or of in-degree zero there (Option II, for DAGs). When every active action of context $c$ has been observed more than $N_c$ times, the active set drops the actions whose empirical reward falls below the best by more than $6\sqrt{\log(2T)\log(MKT/\delta)/N_c}$ . Algorithm 1 is the case $M = 1$ .

Formalization targets

Goal: Theorem 4

With probability at least $1-\delta$ , writing $L = \log(2T)\log(MKT/\delta)$ ,

R_T(\pi)\le T\wedge\big(K+24\sqrt{KTL}\big)\wedge\begin{cases}50\alpha M(\log K)^2+24\log K\sqrt{50\alpha MTL} & \text{Option I},\\ \alpha M+24\sqrt{\alpha MTL} & \text{Option II, }G\text{ a DAG,}\end{cases}

for every context sequence and every tie-breaking rule.

Milestones

Lemma 1 (p. 13): with probability $1-\delta$ , $|\bar r^t_a - R_a|\le 3\sqrt{\log(2T)\log(KT/\delta)/n^t_a}$ for all rounds and all observed actions of Algorithm 1.
Lemma 10 (p. 35): a directed graph on $n\ge2$ vertices with independence number $\alpha$ has a weakly dominating set of size at most $50\alpha\log n$ .
Theorem 3 (p. 13): the one-context bound $T\wedge(50\alpha(\log K)^2+24\log K\sqrt{50\alpha T\log(2T)\log(KT/\delta)})$ (Option I), resp. $T\wedge(\alpha+24\sqrt{\alpha T\log(2T)\log(KT/\delta)})$ (Option II).
Lemma 1, contextual form (p. 16): the same concentration for Algorithm 2, uniformly over contexts, with $\log(MKT/\delta)$ .

Significance

Theorem 4 shows that one algorithm attains, up to logarithmic factors, the better of two regret rates: $\sqrt{KT}$ , available from cross learning alone, and $\sqrt{\alpha MT}$ , available from graph feedback alone. The paper then shows (Theorem 6) that with adversarial contexts nothing better than $\min\{\sqrt{\alpha MT},\sqrt{KT},T^{2/3}\}$ is possible, while with stochastic contexts and a partial order a variant reaches $\tilde O(\sqrt T)$ for first-price auctions. Algorithm 2 is the building block of that variant.

The results are proved in the paper; none is formalized. A formal development produces machine-checked versions of a concentration inequality with a random number of observations, of a domination bound for directed graphs, and of an elimination analysis with shared counts across contexts. Four printed statements need correction, and the formal statements record the corrected forms: the constant $3$ in Theorem 4's second bound (the printed proof gives $24$ ); Lemma 10, which is false for $n = 1$ and for edgeless graphs as worded; Lemma 1, which fails for $K = T = 1$ and $\delta$ close to $1$ (excluded by $KT \ge 2$ ); and the pseudocode of Algorithms 1–2, whose update $N_c \leftarrow N_c + 1$ can leave $\mathcal A_{0,c}$ empty after an elimination (the formalization keeps the text's invariant $N_c = \min_{a \in \mathcal A_{\mathrm{act},c}} n_a$ , and coincides with the printed algorithm wherever the latter is defined).

Difficulty

The observations of an action are not a fixed sample: how often and when action $a$ is revealed depends on earlier rewards through the algorithm's choices. A union bound with Hoeffding's inequality at a fixed sample size does not apply directly, and Lemma 1 needs a self-normalized martingale inequality.

For Option I, the obvious bound on how long it takes to observe every least-pulled action once more is $|\mathcal A_0|$ rounds, which gives only $\sqrt{KT}$ . Getting $\alpha$ instead of $K$ requires that a vertex of largest out-degree covers a $1/(50\alpha\log K)$ fraction of the remaining vertices; this is the content of Lemma 10, a probabilistic-method bound that is not in Mathlib. For contexts, the per-context analyses must be combined while counts are shared, and the bound in $K$ needs a per-action rather than a per-context accounting.

Formalization scope

Actions Fin K, contexts Fin M, rounds Fin T; paper round $t$ is Lean index $t-1$ . The feedback graph is a relation E with no self-loops; "independence number $\alpha$ " is the hypothesis that every independent set has at most $\alpha$ elements (all bounds increase in $\alpha$ ).
The reward law is a probability measure on Fin M → Fin K → ℝ carried by $[0,1]^{M\times K}$ ; rewards are iid across rounds (Measure.pi). The regret is the pseudo-regret with means $R_{c,a}=\int r_{c,a}\,dP$ .
"With probability at least $1-\delta$ " is: the outer measure of the bad event under $P^{\otimes T}$ is at most $\delta$ . The context sequence is fixed in advance (oblivious adversary); stochastic contexts independent of the rewards follow by conditioning.
"Break ties arbitrarily" is a tie-breaking rule that sees the round, the algorithm's state (including the learner's whole observation history) and the context; the theorems hold for every rule that picks a member of every nonempty set.
The minimum count $N_c$ follows the text's definition $N_c = \min_{a\in\mathcal A_{\mathrm{act},c}}n_a$ . The printed update $N_c\leftarrow N_c+1$ can leave $\mathcal A_{0,c}$ empty after an elimination (for example with edges $a\to b$ and $c\to b$ , when $a$ and $c$ are eliminated), where the printed algorithm is undefined. The formal algorithm agrees with the printed one wherever the latter is defined.
Lemma 1 quantifies over $n^t_a\ge1$ and excludes $K = T = 1$ , where it is false for $\delta$ close to $1$ .
Ruled out: replacing the three-way minimum by a single bound, restricting to a fixed tie-breaking rule, or to stochastic contexts.

Welcome contributions: the self-normalized inequality of de la Peña, Klass and Lai (Lemma 11), Lemma 10, invariants of Algorithm 2 (the active sets stay nonempty and contain an optimal action on the good event), and the deterministic regret accounting given the concentration event.

Selected references

Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, arXiv:2003.09795v7, 2024; Operations Research, 2025. 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. Mannor, O. Shamir, From Bandits to Experts: On the Value of Side-Observations, NeurIPS 2011. https://arxiv.org/abs/1106.2436
S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
V. H. de la Peña, M. J. Klass, T. L. Lai, Self-normalized processes: exponential inequalities, moment bounds and iterated logarithm laws, Annals of Probability 32(3A), 2004. https://doi.org/10.1214/009117904000000397

8 thms2 active usersReviewed

Optimization Reinforcement Learning·Captain: mikedeng1

Structural Estimation of Markov Decision Processes in High-Dimensional State Space with Finite-Time Guarantees: Single-Loop ML-IRL Policy and Reward Iterates Converge at Explicit Finite-Time RatesResearch Paper

Motivation

Structural estimation of Markov decision processes recovers the parameters of an agent's reward from observed behavior, under the hypothesis that the agent acts optimally in a known dynamic environment. In econometrics this is the dynamic discrete choice model of Rust (Rust 1987); in artificial intelligence it is maximum-likelihood inverse reinforcement learning (ML-IRL). With Gumbel-distributed choice shocks the two coincide: the agent behaves like the optimal policy of an entropy-regularized MDP, and the reward parameter is estimated by maximizing the likelihood of the observed trajectories.

The classical estimators are nested: every evaluation of the likelihood solves the inner dynamic program to optimality (Rust's nested fixed-point algorithm), which is expensive when the state space is large. Zeng, Hong and Garcia (arXiv:2210.01282, Operations Research 2025) replace the nested loop by a single loop that alternates one approximate soft policy-iteration step with one stochastic gradient step on the reward parameter, and prove a finite-time guarantee for it. That guarantee, Theorem 1 of the paper, is the subject of this mission.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $P(s'\mid s,a)$ a transition kernel, $\rho$ an initial distribution on $\mathcal S$ and $\gamma\in[0,1)$ a discount factor. The reward $r(s,a;\theta)$ depends on a parameter $\theta\in\mathbb R^p$ . A policy $\pi(a\mid s)$ is a distribution over actions at each state, with entropy $\mathcal H(\pi(\cdot\mid s))=-\sum_a\pi(a\mid s)\log\pi(a\mid s)$ .

The soft Q-function of a pair $(\theta,\pi)$ is $Q(s,a)=r(s,a;\theta)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[V(s')]$ , where $V(s)$ is the expected discounted sum of $r(s_t,a_t;\theta)+\mathcal H(\pi(\cdot\mid s_t))$ along the trajectory of $\pi$ from $s$ . The soft-optimal Q-function $Q_\theta$ is the fixed point of the soft-Bellman operator $\Lambda_\theta Q(s,a)=r(s,a;\theta)+\gamma\sum_{s'}P(s'\mid s,a)\log\sum_b e^{Q(s',b)}$ ; the soft-optimal policy is $\pi_\theta(a\mid s)\propto e^{Q_\theta(s,a)}$ and $V_\theta(s)=\log\sum_a e^{Q_\theta(s,a)}$ .

Given a finite dataset $\mathcal D$ of expert trajectories, the surrogate likelihood is

\widehat L(\theta;\mathcal D)=\mathbb E_{\tau\sim\mathcal D}\Big[\sum_{t\ge0}\gamma^tr(s_t,a_t;\theta)\Big]-\mathbb E_{s_0\sim\rho}[V_\theta(s_0)].

Algorithm 1 (ML-IRL). Starting from $(\theta_0,\pi_0)$ and for $k=0,\dots,K-1$ : estimate the soft Q-function $Q_k$ of $(\theta_k,\pi_k)$ by $\widehat Q_k$ with $\|\widehat Q_k-Q_k\|_\infty\le\varepsilon$ ; set $\pi_{k+1}(a\mid s)\propto e^{\widehat Q_k(s,a)}$ ; sample an expert trajectory $\tau^E_k$ from $\mathcal D$ and an agent trajectory $\tau^A_k$ from $\pi_{k+1}$ ; set $\theta_{k+1}=\theta_k+\alpha\big(h(\theta_k;\tau^E_k)-h(\theta_k;\tau^A_k)\big)$ with $h(\theta;\tau)=\sum_t\gamma^t\nabla_\theta r(s_t,a_t;\theta)$ .

The assumptions are: (1) $0\le r\le C_r$ ; (2) under every policy the state chain mixes geometrically in total variation; (3) $\|\nabla_\theta r\|\le L_r$ and $\nabla_\theta r$ is $L_g$ -Lipschitz in $\theta$ .

Formalization targets

Goal: Theorem 1, explicit form

Write $L_q=L_r/(1-\gamma)$ , $L_c=2L_qL_rC_d\sqrt{|\mathcal S||\mathcal A|}/(1-\gamma)+2L_g/(1-\gamma)$ , $C_1=4C_dL_q^2\sqrt{|\mathcal S||\mathcal A|}$ , $C_0=\|Q_0-Q_{\theta_0}\|_\infty$ and

B=\frac{C_0}{K(1-\gamma)}+\frac{2\gamma\varepsilon}{(1-\gamma)^2}+\frac{4L_q^2}{1-\gamma}\alpha .

There is $C_d>0$ depending only on $(P,\rho,\gamma)$ such that every run with $K\ge1$ and $\alpha=\alpha_0/K^\sigma$ , $\alpha_0>0$ , $\sigma\in(0,1)$ , satisfies, for every realization,

\frac1K\sum_{k=0}^{K-1}\|\log\pi_{k+1}-\log\pi_{\theta_k}\|_\infty\le2\varepsilon+2B,

and in expectation

\frac1K\sum_{k=0}^{K-1}\mathbb E\|\nabla_\theta\widehat L(\theta_k;\mathcal D)\|^2\le2L_cL_q^2\alpha+C_1(B+\varepsilon)+\frac{\mathbb E[\widehat L(\theta_K;\mathcal D)-\widehat L(\theta_0;\mathcal D)]}{K\alpha}.

The printed Theorem 1 states only the rates $O(K^{-1})+O(K^{-\sigma})+O(\varepsilon)$ and $O(K^{-\sigma})+O(K^{-1+\sigma})+O(K^{-1})+O(\varepsilon)$ ; the goal is the explicit pair of inequalities its proof derives, from which those rates follow because $\widehat L$ is bounded.

Milestones

Lemma 2 (the gradient of $\widehat L$ ), Lemma 5 (Lipschitz visitation measures), Lemma 3 (Lipschitz $Q_\theta$ and smooth $\widehat L$ ), Lemma 6 and Lemma 7 (approximate soft policy iteration), and the proof's displays (35), (40), (41), the averaged tracking bound after (44) and the averaged gradient bound on p. 24. The bias bound (48) is a further item of the mission without being a milestone.

Significance

The result. Theorem 1 is a finite-time guarantee for a single-loop structural estimator: with $\sigma=1/2$ both the policy-tracking error and the squared gradient of the surrogate likelihood decay as $O(K^{-1/2})+O(\varepsilon)$ . It shows that the inner dynamic program need not be solved to optimality at each likelihood evaluation, and it quantifies the price of approximate policy evaluation through $\varepsilon$ . The paper reports it as the first finite-time result for an algorithm for either the dynamic discrete choice problem or ML-IRL.

Formalizing it. The result is proved on paper; no part of it is machine-checked. A complete development would put on the platform an entropy-regularized MDP layer (soft values, the soft-Bellman fixed point, the soft-optimal policy), its Lipschitz dependence on a reward parameter, the gradient of a soft-optimal value through its fixed point, and a two-timescale analysis with a biased stochastic gradient. Each of these is reusable by later soft-RL, IRL and structural-estimation formalizations.

Difficulty

Neither iterate converges on its own. The policy $\pi_{k+1}$ chases a target $\pi_{\theta_k}$ that moves whenever $\theta$ moves, so the standard linear convergence of soft policy iteration for a fixed reward does not apply directly. The stochastic gradient $g_k$ samples from $\pi_{k+1}$ rather than from $\pi_{\theta_k}$ , so it is biased, and the standard analysis of unbiased stochastic gradient ascent does not apply either. The analysis must show that the tracking error contracts faster than the reward drifts, and bound the bias by the tracking error through the dependence of the state-action visitation measure on the policy. The gradient formula itself requires differentiating a soft-optimal value through a fixed point.

Formalization scope

The Lean development works with finite $\mathcal S$ and $\mathcal A$ (both nonempty), policies as functions $\mathcal S\to\mathcal A\to\mathbb R$ , $\theta\in$ EuclideanSpace ℝ (Fin p), and discounted expectations as tsums over the occupation distribution of the published FoundationsML.ReinforcementLearning layer. $\|\cdot\|_\infty$ is the maximum over $(s,a)$ ; Lemma 5's $\|w-w'\|$ is the Frobenius norm; total variation is half the $\ell_1$ distance. $Q_\theta$ is chosen by Classical.epsilon among fixed points of $\Lambda_\theta$ , which exist and are unique because $\Lambda_\theta$ is a $\gamma$ -contraction.

Disclosed deviations from the page: Assumption 3 is a hypothesis of the goal (Theorem 1 prints "Assumptions 1 - 2" but its proof uses Assumption 3); $\mathcal S$ is finite, as the proof's $\sqrt{|\mathcal S||\mathcal A|}$ requires, although the title speaks of high-dimensional state spaces; Assumption 3 includes differentiability of $r$ , which the page uses implicitly; $\varepsilon\ge0$ (the page writes $\epsilon_{\rm app}>0$ ); Assumption 2 is stated as the mixing bound the paper derives from irreducibility and aperiodicity; and Algorithm 1's sampling is represented by the conditional means of the sampled gradients given the past, measurable with respect to a filtration, which is the only way the proof uses it.

The statement admits no trivializing reading: the run structure is inhabited (a sorry-free check exhibits a run), $C_d$ is fixed before the reward, the data and the run, every expectation is of a bounded measurable function, the gradient is that of a differentiable function (Lemma 2), and the Frobenius norm is used where the page uses it rather than Lean's sup norm on function types.

Welcome contributions: the existence and uniqueness of the soft-Bellman fixed point, the performance-difference and Gibbs-variational facts behind Lemma 7, the visitation-measure Lipschitz bound of Lemma 5, and the fixed-point differentiation behind Lemma 2.

Selected references

S. Zeng, M. Hong, A. Garcia, Structural Estimation of Markov Decision Processes in High-Dimensional State Space with Finite-Time Guarantees, Operations Research, 2025; arXiv:2210.01282v3, 2024. https://arxiv.org/abs/2210.01282
J. Rust, Optimal Replacement of GMC Bus Engines: An Empirical Model of Harold Zurcher, Econometrica 55(5), 1987. https://doi.org/10.2307/1911259
B. D. Ziebart, A. Maas, J. A. Bagnell, A. K. Dey, Maximum Entropy Inverse Reinforcement Learning, AAAI 2008. https://cdn.aaai.org/AAAI/2008/AAAI08-227.pdf
T. Haarnoja, H. Tang, P. Abbeel, S. Levine, Reinforcement Learning with Deep Energy-Based Policies, ICML 2017. https://arxiv.org/abs/1702.08165

18 thms2 active usersReviewed

Completed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Thompson Sampling with Information Relaxation Penalties III: As T → ∞ the Action Laws of IRS.FH and IRS.V-Zero Converge to That of Thompson SamplingResearch Paper

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:

TS samples $\tilde\theta \sim \mathcal P(y)$ and plays $A^{TS}(y) = \operatorname{argmax}_a \mu_a(\tilde\theta_a)$ .
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.
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

Proposition 4 (p. 53): $\mu_a(\theta_a)$ and $\max_a \mu_a(\theta_a)$ are integrable under the prior.
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)$ .
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.
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.
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

9 thms2 active usersReviewed

Bandit Algorithms Harmonic Analysis Operations Research+1·Captain: mikedeng1

Learning and Optimization with Seasonal Patterns 1: Regret Upper Bound for the Two-Stage Period-Estimation and Confidence-Bound PolicyResearch Paper

Motivation

Many demand, traffic and click-through series are seasonal: their mean repeats after a fixed number of periods (a week of days, a year of months), while the length of that cycle is not known in advance. A retailer choosing among $K$ promotions, or a platform choosing among $K$ recommendations, then faces a multi-armed bandit whose arms have time-varying but periodic mean rewards. Standard stochastic bandit algorithms assume stationary means and fail here, and fully adversarial or arbitrarily drifting models give up the structure that periodicity offers.

N. Chen, C. Wang and L. Wang (arXiv:2005.08088, Operations Research, 2025) propose a two-stage policy for this problem: a spectral first stage that estimates every arm's period from a short exploration phase, and a confidence-bound second stage that learns and exploits the resulting "effective arms". Their main upper bound, Theorem 1, shows that the policy's regret grows like $\sqrt{T\sum_k T_k}$ up to logarithmic factors. This mission formalizes that theorem and the chain of lemmas behind it. The matching lower bound (Theorem 3 of the paper) is the subject of a separate mission of this series.

Setting

At each epoch $t=1,\dots,T$ a decision maker pulls one of $K$ arms. Pulling arm $k$ at epoch $t$ yields the reward $Y_{k,t}=\mu_{k,t}+\epsilon_t$ . The mean $\mu_{k,t}$ has a minimum period $T_k\ge1$ : $\mu_{k,t+T_k}=\mu_{k,t}$ for all $t\ge1$ , and no smaller positive shift has this property. The standing assumptions are:

Assumption 1: $\mu_{k,t}\in[0,1]$ .
Assumption 2: the noises $\epsilon_t$ are independent and sub-Gaussian with parameter $\sigma$ , i.e. $\mathbb E[e^{\lambda\epsilon_t}]\le e^{\sigma^2\lambda^2/2}$ for all real $\lambda$ and $\mathbb P(|\epsilon_t|>x)\le2e^{-x^2/(2\sigma^2)}$ .

The pseudo-regret of an arm sequence $\pi$ is $R^\pi_T=\sum_{t=1}^T(\max_k\mu_{k,t}-\mu_{\pi_t,t})$ , and the number of effective arms is $d=\sum_{k=1}^KT_k$ : arm $k$ at phase $t \bmod T_k$ is one effective arm.

Stage one (Algorithm 1). Each arm is pulled $n$ times in a row. From its $n$ rewards the policy computes the periodogram $|\tilde y_k(v)|$ , the modulus of the discrete Fourier transform $\tilde y_k(v)=\frac1n\sum_sY_{k,s}e^{-2\pi ivs}$ , on $v\in[0,1/2]$ . A data-driven threshold $\tau_k$ is computed from the constants $U_1,U_2$ (sums of sinc-type maxima), $\bar\epsilon_v=\frac{2\sigma H}{1-\pi/24}\sqrt{\log(n)/n}$ and $\sup_v|\tilde y_k(v)|$ . The algorithm repeatedly takes the highest peak above $\tau_k$ in $[g/n,1/2]$ , snaps it to the nearest fraction $j_1/j_2$ with $j_2<n/(2g)$ , and removes a $2g/n$ -neighbourhood. The period estimate $\hat T_k$ is the least common multiple of the selected reciprocals.

Stage two (Algorithm 2). At every later epoch an $S$ -round screening tournament, $S=\lfloor\log_2T\rfloor$ , compares the arms at their current phases modulo $\hat T_k$ . It uses estimated means $m^{(s)}_{k,t}$ and widths $w^{(s)}_{k,t}$ pooled from the stage-one samples and from round-specific index sets $\Psi^{(s)}(t)$ . The weak oracle runs the same policy with the true periods in place of $\hat T_k$ .

The parameters are fixed by (7): $n=\lfloor\sqrt{T/K}\rfloor$ , $g=\lceil\sqrt n\rceil$ , $H=\sqrt{1+\log n}$ . Assumption 3 asks $T>4K$ , $g\ge\max\{2,\sqrt n\}$ and $T_k<n/(2g)$ . Assumption 4 asks the smallest present Fourier coefficient $b_k$ of each arm to dominate a combination of $\bar\epsilon_v$ and the largest coefficient $B_k$ .

Formalization targets

Goal: Theorem 1

Under Assumptions 1–4 and (7), the two-stage policy satisfies

\mathbb E\big[R^\pi_T\big]\le C\sqrt{T\,d\,\log^2(T)\,\log(T/d)} ,

with $C$ depending only on $\sigma$ and $K$ , and with Algorithm 2 run at $\delta=8/T$ .

Stage one: correct period identification

Lemma 1: uniform noise bound for the periodogram, $48n\exp(-(n\delta^2/4\sigma^2)(1-\pi/24)^2)$ .
Lemmas 2–3: leakage bounds $\pi B_kU_1$ , $\pi B_kU_2$ , and $B_k\le(\sup|\tilde\epsilon_k|+\sup|\tilde y_k|)/(1-\pi U_2)$ .
Lemmas 4–5: the threshold separates the neighbourhoods of the present frequencies from the rest, with probability $1-48/n^{H^2-1}$ .
Lemmas 6–7: the sharper noise bound near possible present frequencies, and the location of the peaks within $1/n$ of them.
Theorem 2: $\mathbb P(\Lambda)\ge1-48K/n^{H^2-1}-200K/n^{0.867H^2-1}-200K/n^{0.6934H^2-1}$ .

Stage two: the oracle's regret

Lemma 15: an anytime sub-Gaussian deviation bound.
Lemma 9: the confidence event $\mathcal E$ has probability at least $1-\delta S$ .
Lemma 10: on $\mathcal E$ the optimal arm survives screening, and each epoch's gap is at most $1$ , $8\sigma/2^s$ or $2\sigma/\sqrt T$ .
Lemma 16: the summed widths of a round are at most $4\sigma\sqrt{|\Psi^{(s)}(T)|\,d\log(8T/\delta)\log(T/d)}$ .
Lemma 11: the oracle's expected regret is at most $C\sqrt{Td\log^2(T)\log(T/d)}$ with $C$ depending only on $\sigma$ .

Significance

The theorem shows that unknown seasonality costs only the factor $\sqrt{d}=\sqrt{\sum_kT_k}$ that would be paid if every phase of every arm were a separate stationary arm. Up to logarithmic factors this matches the $\sqrt{TK}$ rate of the classical stationary bandit with $d$ arms in place of $K$ . Together with the paper's lower bound $\Omega(\sqrt{T\max_kT_k})$ it locates the minimax regret of periodic bandits within a factor $\sqrt K$ . Stage one is a non-asymptotic, finite-sample period-identification guarantee for a thresholded periodogram, which is of independent use in spectral estimation.

The paper proves these results; none of them is machine-checked. A complete development yields a verified finite-sample periodogram theory (noise bounds for random trigonometric polynomials, Dirichlet-kernel leakage estimates), a verified anytime sub-Gaussian inequality, and a verified analysis of a nested elimination algorithm with data reuse. The formalization also pins down several points the printed text leaves open: the constant $0.233$ of Lemma 6 and the exponent $0.694$ of Lemma 7 and Theorem 2 are slightly stronger than what the proofs give, and the printed claim that Theorem 1's constant is independent of $K$ is not established by the printed argument.

Difficulty

Two steps resist the obvious approach. In stage one, the periodogram has to be controlled at uncountably many frequencies at once. A union bound over $v$ is unavailable, and the leakage of each present frequency spreads over the whole spectrum, so both the noise and the signal must be bounded uniformly in $v$ with explicit constants. In stage two, the samples used to estimate an effective arm are selected with the estimated periods, which were computed from the same stage-one data, so the usual independence behind confidence bounds fails. Lemmas 9–11 are therefore stated for the weak oracle, whose sample selection does not depend on the data; on the event $\Lambda$ the definitions make the oracle's run and the policy's run the same function of the noise path.

Formalization scope

Epochs are natural numbers $t\ge1$ ; arms are Fin K (the paper's arm $k$ is index $k-1$ ), and $K\ge1$ . The noise is a sequence $\epsilon:\mathbb N\to\Omega\to\mathbb R$ on a probability space, independent, with Mathlib's HasSubgaussianMGF at variance proxy $\sigma^2$ , plus the printed tail clause. Both algorithms are defined in full, as deterministic functions of the noise path, with canonical tie-breaking: smallest maximizer, smallest closest candidate, smallest arm index. Algorithm 1's loop runs at most $n$ passes, and $\mathrm{LCM}(\hat v_i^{-1})$ is the least common multiple of the reduced denominators of the selected frequencies. Algorithm 2 takes its period vector as an argument; the two-stage policy and the oracle are its two instances. Expected regret is an outer expectation: an integrable majorant of the regret whose integral obeys the bound. Probability bounds bound the outer measure of the bad event. Every DFT uses the absolute stage-one epochs, as in Step 8 of Algorithm 1.

Disclosed deviations: Theorem 1's constant depends on $\sigma$ and $K$ (the printed proof does not give uniformity in $K$ ), and $\delta=8/T$ is fixed as in the proof of Lemma 11. Lemma 6 uses $0.2328$ for the printed $0.233$ ; Lemma 7 and Theorem 2 use $0.6934$ for the printed $0.694$ . Lemma 7 covers the nonzero present frequencies. Lemma 11 states the standing Assumption 3 and the parameters (7) as hypotheses, as its proof uses them.

The algorithm is the object of the theorem. Replacing Algorithm 1 by "any estimator that is correct with high probability", or Algorithm 2 by "any policy with the oracle's regret", would make the goal a different and much weaker statement. So would placing the constant after the horizon or the instance, since the regret is at most $T$ , or using a bare Lebesgue integral of a possibly non-measurable regret.

A complete development needs discrete Fourier analysis of finite sequences, Bernstein's inequality for complex polynomials on the unit disc (Lemma 14 of the paper, from Nagy and Totik), sinc-function estimates, anytime concentration for sub-Gaussian sums, and a bookkeeping layer for the nested index sets of Algorithm 2. The concentration and polynomial-inequality parts are reusable beyond this mission. Proofs of individual lemmas, helper lemmas such as the closed form (6) of the frequency components, and alternative arguments are welcome.

Selected references

N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, arXiv:2005.08088v4, 2021; Operations Research, 2025. https://arxiv.org/abs/2005.08088
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
L. Li, Y. Lu, D. Zhou, Provably Optimal Algorithms for Generalized Linear Contextual Bandits, ICML 2017. https://arxiv.org/abs/1703.00048
B. Nagy, V. Totik, Bernstein's Inequality for Algebraic Polynomials on Circular Arcs, Constructive Approximation 37, 223–232, 2013.

17 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Thompson Sampling with Information Relaxation Penalties I: For Natural Exponential Families the Suboptimality Gaps of TS, IRS.FH and IRS.V-Zero Are at Most 2√L[1/√ν + √(2 log T)(K/√ν + 2√(KT))]Research Paper

Motivation

Thompson sampling (TS) is the most widely used heuristic for Bayesian multi-armed bandits: at each step it samples a parameter from the current posterior and plays the arm that is best for the sample. Its Bayesian regret has been analysed extensively (Russo and Van Roy, 2014; Bubeck and Liu, 2013). Min, Maglaras and Moallemi (arXiv:1902.04251) place TS inside a larger family of information relaxation sampling (IRS) policies, obtained from the information-relaxation duality of Brown, Smith and Sun (2010). Each choice of penalty function yields a performance bound $W^z$ and a randomized policy $\pi^z$ ; TS is the member with the trivial penalty. Their Theorem 3 gives explicit, finite- $T$ bounds on the suboptimality gap $W^z(T,y)-V(\pi^z,T,y)$ of three members of the family when the rewards come from a natural exponential family with conjugate priors. This mission formalizes Theorem 3 and the lemmas of its proof (Appendix §D.4).

Setting

There are $K\ge1$ arms $\mathcal A=\{1,\dots,K\}$ and a horizon $T$ . Arm $a$ has an unknown parameter $\theta_a\in\mathbb R$ ; given $\theta_a$ , its rewards $R_{a,1},R_{a,2},\dots$ (indexed by the number of the pull, not by time) are i.i.d. with the natural exponential family law $h_a(dr)\exp(\theta_a r-A_a(\theta_a))$ , where $h_a$ is a reference measure and $A_a$ the log-partition function, $e^{A_a(\theta)}=\int e^{\theta r}h_a(dr)$ . The prior of $\theta_a$ is the conjugate law proportional to $\exp(\xi_a\theta-\nu_a A_a(\theta))\,d\theta$ , indexed by a belief $y_a=(\xi_a,\nu_a)$ ; observing a reward $r$ updates it to $(\xi_a+r,\nu_a+1)$ . Arms are independent.

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

The three performance bounds are

W^{\rm TS}(T,y)=\mathbb E_y\Big[T\max_a\mu_a(\theta_a)\Big],\qquad W^{\rm IRS.FH}(T,y)=\mathbb E_y\Big[T\max_a\hat\mu_{a,T-1}\Big],

W^{\rm IRS.V\text{-}Zero}(T,y)=\mathbb E_y\Big[\max_{n\in\mathcal N_T}\sum_a\sum_{i=0}^{n_a-1}\hat\mu_{a,i}\Big],\qquad\mathcal N_T=\Big\{n\in\mathbb N_0^K:\sum_a n_a=T\Big\}.

With remaining horizon $T$ and current belief $y$ , TS samples $\tilde\theta$ from the prior $\mathcal P(y)$ and plays $\arg\max_a\mu_a(\tilde\theta_a)$ . IRS.FH samples an outcome $\tilde\omega\sim\mathcal I(y)$ and plays $\arg\max_a\hat\mu_{a,T-1}(\tilde\omega)$ . IRS.V-Zero samples $\tilde\omega$ , finds an allocation $\tilde n^*\in\mathcal N_T$ maximizing the bracket above, and plays $\arg\max_a\tilde n^*_a$ . Each policy repeats this at every step with the updated belief. $V(\pi,T,y)$ is the expected total reward of $\pi$ .

Formalization targets

Goal: Theorem 3

If every $A_a$ is $L$ -smooth ( $A_a''\le L$ on $\mathbb R$ ) and $\nu_a=\nu$ for all $a$ , then for every $T\ge2$

W^{\rm TS}-V(\pi^{\rm TS})\le2\sqrt L\Big[\tfrac1{\sqrt\nu}+\sqrt{2\log T}\big(\tfrac K{\sqrt\nu}+2\sqrt{KT}\big)\Big],

W^{\rm IRS.FH}-V(\pi^{\rm IRS.FH})\le2\sqrt L\Big[\tfrac1{\sqrt\nu}+\sqrt{2\log T}\big(\tfrac K{\sqrt\nu}+2\sqrt{KT}-\tfrac13\sqrt{T/K}\big)\Big],

W^{\rm IRS.V\text{-}Zero}-V(\pi^{\rm IRS.V\text{-}Zero})\le\sqrt L\Big[\tfrac1{\sqrt\nu}+\sqrt{2\log T}\big(\tfrac K{\sqrt\nu}+2\sqrt{KT}-\tfrac13\sqrt{T/K}\big)\Big].

The TS bound (60) is also posed alone as a companion statement.

Milestones

Lemma 3: the loss of a first action $a$ in the penalized inner problem is $\mu_{a^*}-\mu_a$ (TS), $\hat\mu_{a^*,T-1}-\hat\mu_{a,T-1}$ (IRS.FH), and at most $\max_{n<T}\hat\mu_{a^*,n}-\hat\mu_{a,0}$ (IRS.V-Zero).
Lemma 4 and Corollary 3: a Gaussian tail, in particular sub-Gaussianity, gives $\mathbb E[(X-\mathbb EX-z\sigma)^+]\le(\sigma/z)e^{-z^2/2}$ .
Lemma 5: $\bar\mu_a=\xi_a/\nu$ , $\mu_a$ is $\sqrt{L/\nu}$ -sub-Gaussian and $\hat\mu_{a,n}$ is $\sqrt{Ln/(\nu(\nu+n))}$ -sub-Gaussian.
Lemma 6: the maximal version of Lemma 4 for $\max_{i\le n}\hat\mu_{a,i}$ .
(259)–(261) and (269)–(275): deterministic summation bounds over the pull counts of an action sequence.

Significance

Theorem 3 shows that the IRS policies, although built from tighter performance bounds than TS, keep the $O(\sqrt{KT\log T})$ behaviour of TS, and that they improve the leading coefficient (IRS.V-Zero) or subtract a $\sqrt{T/K}$ term (IRS.FH, IRS.V-Zero). Because $W^{\rm TS}-V(\pi^{\rm TS})$ is the Bayesian regret of TS, (60) is also an explicit Bayesian regret bound for TS that applies to unbounded rewards such as Gaussian ones. The bounds apply to the Bernoulli family (with $L=1/4$ ) and to Gaussian rewards with known variance.

None of these results has a machine-checked proof. A formal development produces a reusable Lean model of a conjugate-prior Bayesian bandit with natural-exponential-family rewards, the sub-Gaussianity of its posterior mean process, and a Lean account of TS as a belief-Markov randomized policy. The paper's proofs are in its Appendix D.4.

Difficulty

The obvious route to (60) is the standard Bayesian-regret decomposition with upper confidence bounds. For unbounded natural-exponential-family rewards the required concentration does not come from boundedness. It has to come from the conjugate structure: the prior of $\mu_a(\theta_a)=A_a'(\theta_a)$ is sub-Gaussian because $A_a$ is $L$ -smooth, which uses the whole real line as parameter space. For the IRS policies there is a further step: the policy must match nature's randomness in the same way TS does, with the penalized inner problem in place of the true best arm. The printed arguments for (61) and (62) pass through a time- $t$ version of Lemma 3 whose IRS.FH and IRS.V-Zero cases do not hold in full generality as printed, so those two bounds need new or repaired arguments.

Formalization scope

Arms are Fin K and reward indices are 0-based. The parameter space of every arm is $\mathbb R$ , and a belief is a pair $(\xi,\nu)\in\mathbb R^2$ . $\mu_a$ , $\bar\mu_a$ and $\hat\mu_{a,n}$ are defined as integrals, with $\hat\mu_{a,n}$ the predictive mean at the conjugate posterior belief (13), so the closed forms (14) are consequences, not assumptions. Products of probability measures are Measure.infinitePi. $W^{\rm IRS.FH}$ is defined by its closed form (33). $V(\pi,T,y)$ is the recursion of the outer loop: draw the action from the policy's law at the current belief, earn the predictive mean, observe a reward from the predictive law, and update the belief. Every policy is a map from (remaining horizon, current belief) to a law on arms, so no policy can see the true outcome; a formalization in which TS used the true parameter would make (60) trivial and is excluded by construction. Ties are broken by arbitrary measurable selectors, and the goal quantifies over all of them.

Standing hypotheses carried by the goal:

normalization $\int e^{\theta r}h_a(dr)=e^{A_a(\theta)}$ ;
$A_a\in C^2$ with $A_a''\le L$ ;
$\nu>0$ and a proper prior at the initial belief;
integrability (3) of the rewards at the initial belief;
$K\ge1$ .

Properness is not assumed at every belief, since for Bernoulli rewards it fails outside $0<\xi<\nu$ . Lemma 3 (3) carries the added hypothesis that $a$ is strictly suboptimal; without it the printed statement fails at ties. Sub-Gaussianity uses Mathlib's HasSubgaussianMGF with variance proxy $\sigma^2$ .

Useful infrastructure: conjugate updating for exponential families, the moment generating function of a natural exponential family, Doob's maximal inequality for the submartingale $e^{\lambda\hat\mu_{a,n}}$ , and a probability-matching lemma for TS in the belief-recursion model. Contributions are welcome on any milestone, and on a proof that the Beta–Bernoulli instance satisfies the hypotheses.

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
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
S. Bubeck, C.-Y. Liu, Prior-free and prior-dependent regret bounds for Thompson Sampling, NeurIPS 2013. https://arxiv.org/abs/1304.5758

9 thms2 active usersReviewed

Bandit Algorithms Operations Research Probability·Captain: mikedeng1

Thompson Sampling with Information Relaxation Penalties II: The IRS Performance Bounds Are Monotone, W^TS ≥ W^IRS.FH ≥ W^IRS.V-Zero and W^TS ≥ W^IRS.V-EMaxResearch Paper

Motivation

In a Bayesian multi-armed bandit a decision maker pulls one of $K$ arms in each of $T$ periods, observes the reward, and updates a prior belief about each arm's unknown parameter. The best achievable expected total reward, $V^*(T, y)$ , is the value of a dynamic program over beliefs, and for all but the smallest instances it cannot be computed. Upper bounds on $V^*$ are therefore the yardsticks against which heuristics such as Thompson sampling (TS) are measured: the gap between a policy's performance and an upper bound certifies how far the policy can be from optimal.

The conventional benchmark is the expected total reward of a clairvoyant who knows the arms' parameters, $W^{TS}(T, y) = \mathbb E_y[T \max_a \mu_a(\theta_a)]$ , the quantity behind every Bayesian regret bound. Min, Maglaras and Moallemi (arXiv:1902.04251v2, Management Science 2025) apply the information relaxation duality of Brown, Smith and Sun (Operations Research 2010) to the bandit: a clairvoyant who sees the whole future but pays a penalty for using it. Each penalty yields a performance bound $W^z(T,y)$ and a randomized policy (IRS, "information relaxation sampling"); the zero-information penalty recovers TS and $W^{TS}$ , the ideal penalty recovers $V^*$ . The paper's Theorem 2 shows that its intermediate penalties give bounds that are provably tighter than $W^{TS}$ . This mission formalizes that theorem.

Setting

Let $\mathcal A = \{1, \dots, K\}$ , $K \ge 1$ . 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 parameter has a prior $\mathcal P_a(y_a)$ from a conjugate family indexed by a belief $y_a$ , and the Bayesian update $\mathcal U_a(y_a, r)$ is the belief after a reward $r$ : if $\theta_a \sim \mathcal P_a(y_a)$ then $\theta_a \mid R_{a,1} \sim \mathcal P_a(\mathcal U_a(y_a, R_{a,1}))$ . The outcome $\omega = (\theta, (R_{a,n})_{a,n})$ has law $\mathcal I(y)$ , under which arms are independent. Throughout, $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief.

The conditional and predictive mean rewards are $\mu_a(\theta_a) = \mathbb E[R_{a,n} \mid \theta_a]$ and $\bar\mu_a(y_a) = \mathbb E_{y_a}[\mu_a(\theta_a)]$ , and the posterior predictive mean after $n$ rewards of arm $a$ is $\hat\mu_{a,n} = \mathbb E_{y_a}[\mu_a(\theta_a) \mid R_{a,1}, \dots, R_{a,n}]$ . With $\mathcal N_T = \{n \in \mathbb N_0^K : \sum_a n_a = T\}$ and $S_a(n) = \sum_{i=1}^{n} \hat\mu_{a,i-1}$ , the four bounds compared are

W^{TS}(T,y) = \mathbb E_y\Big[T\max_a \mu_a(\theta_a)\Big], \qquad W^{IRS.FH}(T,y) = \mathbb E_y\Big[T\max_a \hat\mu_{a,T-1}\Big],

W^{IRS.V\text{-}Zero}(T,y) = \mathbb E_y\Big[\max_{n\in\mathcal N_T} \sum_a S_a(n_a)\Big], \qquad W^{IRS.V\text{-}EMax}(T,y) = \mathbb E_y\Big[\max_{a_{1:T}} \sum_{t=1}^T \big(r_t - z_t^{IRS.V\text{-}EMax}\big)\Big].

In the last one the clairvoyant chooses a whole action sequence $a_{1:T}$ knowing $\omega$ , and at time $t$ receives the conditional expected reward $\bar\mu_{a_t}$ under the current belief $y_{t-1}$ , minus $W^{TS}(T-t, y_t)$ , plus the expectation of $W^{TS}(T-t, y_t)$ given the history $H_{t-1}$ . A supersolution is a function $\hat V(T, y)$ with $\hat V(0, y) = 0$ and $\hat V(T, y) \ge \mathbb E_{y_a}[R_{a,1} + \hat V(T-1, \mathcal U(y, a, R_{a,1}))]$ for all $T \ge 1$ , $y$ , $a$ (Definition 2).

Formalization targets

Goal: Theorem 2 (p. 25)

W^{TS}(T,y) \ge W^{IRS.FH}(T,y) \ge W^{IRS.V\text{-}Zero}(T,y), \qquad W^{TS}(T,y) \ge W^{IRS.V\text{-}EMax}(T,y),

for every horizon $T$ and every belief vector $y$ of every conjugate model satisfying the standing assumptions.

Milestones (Appendix D.3)

$W^{TS} \ge W^{IRS.FH}$ , (124).
Lemma 1, a variant of Jensen's inequality: for non-decreasing $\varphi$ , $\mathbb E[\max\{X+\varphi(X),0\}] \ge \mathbb E[\max\{\mathbb E X+\varphi(X),0\}]$ .
Corollary 1, its version conditional on a sub- $\sigma$ -field $\mathcal H$ .
Corollary 2, the form for a maximum of affine functions $(i-n)^+X + C_i$ with $\mathcal H$ -measurable $C_i$ .
(155): the interpolating expectations $U_{k,n}$ of (154) decrease in $n$ , with $W^{IRS.FH} = U_{1,0}$ , $W^{IRS.V\text{-}Zero} = U_{K,T}$ and $U_{k+1,0} = U_{k,T}$ .
Lemma 2 (Theorem 4 of Desai, Farias and Moallemi): a supersolution $\hat V$ bounds the inner problem of its own penalty outcome by outcome, hence $W^{\hat z} \le \hat V$ .
(176)–(180): $W^{TS}$ is a supersolution.

Significance

The result. Theorem 2 says that the penalties IRS.FH and IRS.V-Zero, which only require sampling a future and solving a deterministic allocation problem, produce upper bounds on $V^*$ that are never looser than the regret benchmark $W^{TS}$ , and that IRS.V-EMax is too. A bound below $W^{TS}$ gives a sharper certificate of suboptimality for any policy, and the paper's experiments (§5) report these bounds next to the policies' performance. The ordering also organises the paper's family of policies: the bounds move monotonically from the TS benchmark towards the optimal value.

Formalizing it. The theorem is proved in the paper (Appendix D.3); it has no machine-checked proof. A formal development checks three different mechanisms: conditional Jensen for (124); a one-arm-at-a-time interpolation through $U_{k,n}$ , driven by a non-standard Jensen-type inequality (Lemma 1, Corollaries 1–2), for (57); and the supersolution argument of Desai et al. for (58). The paper's own remark (pp. 59–60) shows that the middle inequality does not follow from the general "finer information gives a weaker bound" principle of Brown et al.; formalization fixes exactly which properties of the bandit (conjugacy, independence of arms, the martingale property of $\hat\mu_{a,n}$ ) carry the argument.

Difficulty

The obvious route to $W^{IRS.FH} \ge W^{IRS.V\text{-}Zero}$ is to observe that IRS.FH conditions on more information ( $T-1$ rewards of every arm) than IRS.V-Zero (only the history so far) and invoke monotonicity of dual bounds in the relaxation. That argument fails: the two penalties are not generated by a common function, and the paper exhibits a modified bandit (163)–(165) in which the inequality reverses. The interpolation must instead trade one arm's realized cumulative payoff for a constant per-pull payoff one pull at a time, and each step needs Corollary 2, where conditioning acts inside a maximum of affine functions; ordinary Jensen points the wrong way there.

For (58), the difficulty is that the payoff of the penalised inner problem depends on the whole outcome along an adaptively chosen action sequence; the bound must hold uniformly over all $K^T$ sequences, which is why it is proved pathwise by backward induction rather than in expectation.

Formalization scope

Arms are Fin K (0-based) with [NeZero K]. All arms share one parameter type $\Theta$ (standard Borel, nonempty) and one belief type $Y$ , the disjoint unions of the per-arm ones. Rewards are a Kernel Θ ℝ per arm, priors a Kernel Y Θ per arm, both Markov. The outcome is Fin K → Θ × (ℕ → ℝ) with law the product over arms of $\theta_a \sim \mathcal P_a(y_a)$ followed by an i.i.d. reward sequence. The standing assumptions are one predicate: conjugacy (the update agrees a.e. with Mathlib's posterior of the reward kernel), joint measurability of each $\mathcal U_a$ , and $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief, (3). $\hat\mu_{a,n}$ is the conjugate (pathwise) version $\bar\mu_a(y_{a,n})$ of the conditional expectation (10). $W^{IRS.FH}$ is defined by its closed form (33). In the penalties (26) and (168) the conditional expectations given $H_{t-1}$ are replaced by their conjugate closed forms: $\mathbb E[r_t \mid H_{t-1}] = \hat\mu_{a_t, n_{t-1}(a_t)}$ , and the expectation of $\hat V(T-t, y_t)$ is the integral over the predictive law of the next reward. The supersolution predicate requires the expectation in (166) to exist. Lemma 1 and Corollary 1 compare lower Lebesgue integrals in $[0,\infty]$ ; Corollary 1 adds joint measurability of $\varphi$ ; Corollary 2 assumes the $C_i$ integrable; Lemma 2's integral form assumes the pathwise maximum integrable.

Trivializations ruled out. No expectation in a goal can silently be a junk $0$ : the standing integrability makes every bound an honest integral, and Lemma 1 and Corollary 1 are stated with lower integrals. $W^{IRS.V\text{-}EMax}$ is the penalised clairvoyant value of the penalty generated by $W^{TS}$ , not $W^{TS}$ itself or the closed form (41) substituted into it. The standing assumptions are satisfiable (a sorry-free check with a one-point parameter space is in the development).

A complete development needs: conjugate updating along reward sequences and the martingale property of $\hat\mu_{a,n}$ (Remark 1); measurability of $\theta \mapsto \bigotimes_n \mathcal R_a(\theta)$ ; independence of arms under $\mathcal I(y)$ ; conditional Jensen for finite maxima. Lemma 1, Corollaries 1–2 and Lemma 2 are reusable beyond this mission. Contributions of any milestone, or of the infrastructure lemmas above, are welcome.

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
V. V. Desai, V. F. Farias, C. C. Moallemi, Bounds for Markov Decision Processes, in F. L. Lewis and D. Liu (eds.), Reinforcement Learning and Approximate Dynamic Programming for Feedback Control, Wiley/IEEE Press, pp. 452–473, 2012 (the paper's Desai et al. 2012a; Theorem 4 there is Lemma 2 here).
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

9 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

A Survey of Quantum Learning Theory 5: Atıcı–Servedio: time-efficient quantum learning of k-juntas (corrected)Textbook

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.

5 thms2 active usersReviewed

Quantum Information·Captain: Goku

Quantum Algorithms and Learning Theory — Part II 6: Shadow tomography with poly(log m, log d, 1/ε, log(1/δ)) copiesTextbook

Motivation

This mission develops Chapter 6 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. 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 Aaronson's shadow tomography theorem.

A two-outcome measurement on $\mathbb C^d$ is a POVM $\{E,\mathbb 1-E\}$ with $0\preceq E\preceq\mathbb 1$ . A learner using $k$ copies of an unknown $d$ -dimensional density matrix $\rho$ performs a measurement (a POVM $\{N_o\}_{o\in O}$ with finite outcome set $O$ ) on $\rho^{\otimes k}$ and outputs numbers $b(o)=(b_1(o),\dots,b_m(o))\in[0,1]^m$ .

There is a polynomial $p$ in four variables such that for all $\varepsilon,\delta\in(0,1]$ , all integers $m,d>0$ and all effects $E_1,\dots,E_m$ on $\mathbb C^d$ there exist $k\le p(\log m,\log d,1/\varepsilon,\log(1/\delta))$ and such a learner (depending on $m,d,\varepsilon,\delta$ and $E_1,\dots,E_m$ , but not on $\rho$ ) with

\Pr_{o\sim\{\operatorname{Tr}(N_o\rho^{\otimes k})\}}\Big[\ \forall i\in[m]:\ |\operatorname{Tr}(E_i\rho)-b_i(o)|\le\varepsilon\ \Big]\ \ge\ 1-\delta

for every $d$ -dimensional density matrix $\rho$ .

The number of copies is exponentially smaller in $m$ and $d$ than for full state tomography or for estimating each $\operatorname{Tr}(E_i\rho)$ separately.

Formalization Note The source writes $\varepsilon,\delta\in[0,1]$ ; the endpoints $0$ are excluded because there $1/\varepsilon$ or $\log(1/\delta)$ is undefined. Internal randomness and post-processing of the learner are absorbed into the POVM; $\rho^{\otimes k}$ is the $k$ -fold Kronecker power and logarithms are natural (the base is absorbed by the polynomial).

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

Lemma 6.4.8: A class of size at most M needing Ω(√((N−k+1)k)) quantum membership queries.
Fact 6.4.9: An admissible weight k of order log M/(log(N/log M)+1).
Theorem 6.6.2: Shadow tomography with poly(log m, log d, 1/ε, log(1/δ)) copies.

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, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08. https://ir.cwi.nl/pub/27536/Thesis_S_Arunachalam.

3 thms2 active usersReviewed

Quantum Information·Captain: Goku

A Survey of Quantum Learning Theory 4: Quantum states are PAC-learnable from n·poly(1/ε, 1/γ, log(1/δ)) measurement resultsTextbook

Motivation

This mission develops Chapter 4 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 Aaronson's theorem on "pretty good tomography": an $n$ -qubit state can be PAC-learned from linearly many (in $n$ ) measurement results.

An $n$ -qubit state is a density matrix $\rho\in\mathbb C^{2^n\times 2^n}$ (positive semidefinite, trace $1$ ). A two-outcome measurement is an effect $E$ , i.e. $0\preceq E\preceq \mathrm{Id}$ ; its first outcome has probability $\mathrm{Tr}(E\rho)$ . Let $D$ be a probability distribution (Borel) on the set of effects.

There is a polynomial $p$ in three variables with nonnegative coefficients such that for every $n$ and all $\varepsilon,\gamma>0$ , $\delta\in(0,1)$ there are a number

T\ \le\ n\cdot p\big(1/\varepsilon,\ 1/\gamma,\ \log(1/\delta)\big)

and a (measurable) learner $L$ , mapping $T$ measurement results to an $n$ -qubit density matrix, with the following property: for every $n$ -qubit state $\rho$ and every distribution $D$ , if $E_1,\dots,E_T$ are drawn i.i.d. from $D$ and, independently given the $E_i$ , each $b_i$ is a bit with $\Pr[b_i=1]=\mathrm{Tr}(E_i\rho)$ , then with probability at least $1-\delta$ the output $\sigma=L((E_1,b_1),\dots,(E_T,b_T))$ satisfies

\Pr_{E\sim D}\big[\,|\mathrm{Tr}(E\sigma)-\mathrm{Tr}(E\rho)|>\gamma\,\big]\ \le\ \varepsilon .

The learner knows neither $\rho$ nor $D$ . Only the number of measurement results is bounded, not the running time.

Formalization Note " $T=n\cdot\mathrm{poly}$ " is read as an upper bound on $T$ (a learner may ignore extra results). The condition $\delta<1$ is added: for $\delta\ge 1$ the claim is empty and $\log(1/\delta)\le 0$ . The learner is deterministic and measurable; the probability of success is written out as an integral over $D^{T}$ of the probabilities of the bit strings.

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

§4.1.1, Theorem 4.3: Servedio–Gortler: quantum exact learning needs Ω(max{1/√γ(C), log|C|/n}) queries.
§4.1.1, Corollary 4.4: Servedio–Gortler: D(C) = O(n·Q(C)^3).
§4.1.2, Theorem 4.5: Classical (N,M)-query complexity of exact learning is Θ(min{M,N}).
§4.1.2, Theorem 4.6: Kothari: optimal quantum (N,M)-query complexity of exact learning.
§4.1.2, Theorem 4.8: Kothari: quantum exact learning with O(√((1/γ)/log(1/γ))·log|C|) queries.
Theorem 4.12: Quantum PAC learning needs Ω(d/ε + log(1/δ)/ε) quantum examples.
Theorem 4.13: Diagonal of the square root of an XOR-invariant Gram matrix (corrected: with the factor 2^{-k/2}).
Theorem 4.15: Quantum agnostic learning needs Ω(d/ε² + log(1/δ)/ε²) quantum examples.
Theorem 4.16: Quantum states are PAC-learnable from n·poly(1/ε, 1/γ, log(1/δ)) measurement results.

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.

11 thms2 active usersReviewed

Bandit Algorithms Probability Reinforcement Learning·Captain: mikedeng1

(More) Efficient Reinforcement Learning via Posterior Sampling: PSRL Has Bayesian Regret O(τS√(AT log(SAT))) in Episodic Finite MDPsResearch Paper

Motivation

An agent that interacts repeatedly with an unknown Markov decision process must trade exploration against exploitation. The dominant design principle for provably efficient reinforcement learning has been optimism in the face of uncertainty: UCRL2 (Jaksch, Ortner & Auer, 2010) and REGAL (Bartlett & Tewari, 2009) build confidence sets around the unknown model and act according to the most favourable model in them. Computing that optimistic policy can be expensive, and confidence sets built separately for every state–action pair can be loose.

Posterior sampling for reinforcement learning (PSRL), proposed by Strens (2000), replaces optimism by randomization: at the start of each episode it samples one MDP from the posterior distribution and follows the optimal policy of that sample. It is the reinforcement-learning analogue of Thompson sampling for bandits. Osband, Russo & Van Roy (2013) gave the first regret guarantee for PSRL, and with it the first regret guarantee for an RL algorithm not based on optimism. Their argument transfers the Bayesian-regret analysis of Thompson sampling by Russo & Van Roy (2014) from bandits to MDPs.

Timeline:

2000: Strens proposes PSRL as a heuristic.
2010: Jaksch, Ortner and Auer prove $\tilde O(DS\sqrt{AT})$ regret for UCRL2 in non-episodic MDPs with diameter $D$ .
2013: Osband, Russo and Van Roy prove the $O(\tau S\sqrt{AT\log(SAT)})$ Bayesian regret bound for PSRL in episodic MDPs, the result of this mission.

Setting

A finite-horizon MDP $M=(\mathcal S,\mathcal A,R^M,P^M,\tau,\rho)$ has $S$ states, $A$ actions and horizon $\tau$ . Choosing action $a$ in state $s$ yields a reward drawn from a distribution $R^M_a(s)$ on $[0,1]$ , with mean $\overline R^M_a(s)$ , and moves the state to $s'$ with probability $P^M_a(s'\mid s)$ . Every episode starts from a state drawn from the initial distribution $\rho$ . A policy $\mu$ maps a state and a step $i\in\{1,\dots,\tau\}$ to an action, and its value is the expected total mean reward from step $i$ on,

V^M_{\mu,i}(s)=\mathbb E_{M,\mu}\Big[\sum_{j=i}^{\tau}\overline R^M_{a_j}(s_j)\,\Big|\,s_i=s\Big].

A policy is optimal for $M$ if it maximizes $V^M_{\mu,i}(s)$ for every $s$ and $i$ ; $\mu^M$ denotes a fixed choice of optimal policy for each $M$ .

The true MDP $M^*$ is random with prior $f$ . In episode $k$ , PSRL samples $M_k$ from the posterior $f(\cdot\mid H_{t_k})$ given the history $H_{t_k}$ of all earlier states, actions and rewards, and follows $\mu_k=\mu^{M_k}$ for $\tau$ steps. With $\mu^*=\mu^{M^*}$ , the regret of episode $k$ and the cumulative regret are

\Delta_k=\sum_{s}\rho(s)\big(V^{M^*}_{\mu^*,1}(s)-V^{M^*}_{\mu_k,1}(s)\big),\qquad \mathrm{Regret}(T,\pi^{\mathrm{PS}}_\tau)=\sum_{k=1}^{\lceil T/\tau\rceil}\Delta_k .

In Lean, MDPs are indexed by a parameter $\theta$ in a measurable space $\Theta$ (MDPFamily), the value is value F θ π j with 0-based steps, and the run is the structure PSRLRun.

Formalization targets

Goal: Theorem 1

There is an absolute constant $C>0$ such that, for all $S,A,\tau\ge1$ , every prior $f$ , every measurable optimal-policy selector, every PSRL run with $M^*\sim f$ and every $T$ ,

\mathbb E\big[\mathrm{Regret}(T,\pi^{\mathrm{PS}}_\tau)\big]\le C\,\tau S\sqrt{AT\log(SAT)} .

This is the paper's $O(\cdot)$ statement. It does not fix the constant, which the paper's appendix computes with errors.

Milestones, in the order of the proof

Lemma 1: given $H_{t_k}$ , $M^*$ and $M_k$ have the same conditional law.
Theorem 2, (4): $\mathbb E[\sum_{k\le m}\Delta_k]=\mathbb E[\sum_{k\le m}\tilde\Delta_k]$ , where $\tilde\Delta_k=\sum_s\rho(s)(V^{M_k}_{\mu_k,1}(s)-V^{M^*}_{\mu_k,1}(s))$ .
Lemma 2, (5): the dynamic programming equation $V^M_{\mu,i}=\mathcal T^M_{\mu(\cdot,i)}V^M_{\mu,i+1}$ .
(6): $\mathbb E[\tilde\Delta_k\mid M^*,M_k]$ equals the expected sum of one-step Bellman errors along the visited states.
(7): the pathwise split of $\sum_k\tilde\Delta_k$ on the event $\{M_k,M^*\in\mathcal M_k\}$ .
$\mathbb P(M^*\notin\mathcal M_k)\le1/m$ for the paper's confidence sets (Lemma 17 of Jaksch et al.).
(8): $\mathbb E[\sum_k\tilde\Delta_k]\le(\tau+1)\,\mathbb E[\sum_k\sum_i\min\{\beta_k(s_{k,i},a_{k,i}),1\}]+2\tau$ .
Appendix B: $\sum_k\sum_i\mathbf 1(N_{t_k}(s_{k,i},a_{k,i})\le\tau)\le2\tau SA$ .
Appendix B: $\sum_k\sum_i\sqrt{\mathbf 1(N_{k,i}>\tau)/N_{k,i}}\le\sqrt{8SAm\tau}$ .

Significance

Theorem 1 holds for every prior, with no assumption on the MDP class beyond finiteness and bounded rewards. It shows that a single posterior sample per episode, rather than an optimistic search over a confidence set, already achieves the $\sqrt T$ rate of the optimistic algorithms. The reduction it rests on (Lemma 1 and Theorem 2) applies to any problem in which the agent can sample from the posterior.

The theorem has a paper proof but, as far as is known, no machine-checked proof. A formalization adds three things. First, an exact model of the episodic Bayesian setting, with posterior sampling stated as a conditional law. Second, corrected versions of two steps: the factor in (8), which the page's argument does not justify as printed, and the square-root sum of Appendix B, which is false as printed. Third, reusable pieces: a path-defined finite-horizon value with its dynamic programming equation, a conditional-expectation form of the posterior-sampling identity, and deterministic counting lemmas for visit counts.

Difficulty

The proof combines three kinds of argument, each with its own obstacle in Lean.

Conditioning. Lemma 1 and Theorem 2 identify conditional laws given the history. The history is a random element whose length grows with $k$ , and the posterior-sampling assumption only speaks about indicators of $M_k$ . Extending it to functions of $(M,H_{t_k})$ and applying the tower property needs care with sub- $\sigma$ -algebras. The same issue appears in (8): the confidence event depends on $H_{t_k}$ , so it is not measurable with respect to $\sigma(M^*,M_k)$ , the $\sigma$ -algebra on which (6) conditions. The working argument conditions on $(M^*,M_k,H_{t_k})$ instead.
Concentration over adaptive counts. The bound $\mathbb P(M^*\notin\mathcal M_k)\le1/m$ needs an $L^1$ deviation inequality for empirical transition distributions (Weissman et al.) and Hoeffding's inequality for rewards. Both must hold uniformly over the random number of visits, which the agent's own behaviour determines. Applying the inequalities at a fixed number of samples is not valid, because the sample size is random.
Counting. The appendix sums $N^{-1/2}$ along the visited pairs; the paper's chain loses a factor of $2$ at its integral comparison.

Formalization scope

Model. States and actions are Fin S and Fin A. Steps and episodes are 0-based: Lean step j is the paper's step $j+1$ , and Lean episode k is the paper's episode $k+1$ , with $t_k=k\tau+1$ . MDPs are a measurable family over a parameter space Θ: transition rows satisfy the published IsTransitionKernel, and reward laws are Markov kernels supported on $[0,1]$ . The initial distribution $\rho$ is fixed. The value is defined from the state laws along the trajectory, not by the Bellman recursion.
The run. PSRLRun consists of measurable random elements on a probability space. Posterior sampling, the reset from $\rho$ , rewards and transitions are stated as conditional expectations of indicators. Three assumptions the paper leaves implicit are made explicit:
- the state is reset from $\rho$ at every episode start;
- the state reached after the last action of an episode is observed;
- the sampling step uses fresh randomness.
The optimal-policy selector is any measurable map that is optimal at every step.
Constants and corrections. $O(\cdot)$ is one absolute constant, quantified before every other object; a constant that depends on $S$ , $A$ , $\tau$ , the prior or $T$ would make the goal trivial, because the regret is at most $\lceil T/\tau\rceil\tau$ . Milestone 7 uses the factor $\tau+1$ , which the page's chain proves, where the page prints $\tau$ , and milestone 9 uses $\sqrt{8SAm\tau}$ where the page prints the false bound $\sqrt{2SAT}$ ; both corrections are disclosed in the statements.
Ruled out. The value is not defined by the recursion, which would make Lemma 2 definitional. Measurability is required, so the expectations are not junk zeros. The posterior-sampling clause concerns indicators of $M_k$ only, so it does not already contain Lemma 1.
Needed infrastructure. Conditional expectations with respect to $\sigma$ -algebras generated by random elements; finite-horizon Markov chain laws; Weissman's $L^1$ inequality and Hoeffding's inequality at random sample sizes; elementary bounds on $\sum_j j^{-1/2}$ . The counting milestones (8, 9) and Lemma 2 are self-contained and a good place to start. Proofs of the conditioning steps (milestones 1, 2, 4) are reusable for any posterior-sampling analysis.

Selected references

I. Osband, D. Russo, B. Van Roy, (More) Efficient Reinforcement Learning via Posterior Sampling, NIPS 2013; arXiv:1306.0940v5. https://arxiv.org/abs/1306.0940
T. Jaksch, R. Ortner, P. Auer, Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11, 2010. https://jmlr.org/papers/v11/jaksch10a.html
D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014; arXiv:1301.2609. https://arxiv.org/abs/1301.2609
M. Strens, A Bayesian Framework for Reinforcement Learning, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000 (reference [16] of the paper).
P. L. Bartlett, A. Tewari, REGAL: A Regularization Based Algorithm for Reinforcement Learning in Weakly Communicating MDPs, UAI 2009; arXiv:1205.2661. https://arxiv.org/abs/1205.2661
T. Weissman, E. Ordentlich, G. Seroussi, S. Verdú, M. J. Weinberger, Inequalities for the L1 Deviation of the Empirical Distribution, HP Labs Technical Report HPL-2003-97, 2003.

14 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Distributed Stochastic Gradient Tracking Methods II: With Stepsizes θ/(m+k), DSGT's Mean-Square Error Is at Most 2θ²σ²/(n(θμ−1)(m+k)) Plus Higher-Order TermsResearch Paper

Motivation

Many learning and estimation problems are solved by a group of computing agents that each hold part of the data and can talk only to their neighbours in a communication network. Each agent $i$ has a private cost $f_i$ , and the group wants a minimizer of the average $f=\frac1n\sum_i f_i$ without a central coordinator. In machine learning the agents usually cannot evaluate exact gradients either; they draw noisy stochastic gradients from samples, as in stochastic gradient descent (SGD).

Pu and Nedić (Math. Program. 187 (2021) 409–457) study distributed stochastic gradient tracking (DSGT), where each agent keeps an auxiliary variable that tracks the network-average gradient. With deterministic gradients, gradient tracking achieves linear convergence under a constant stepsize (Nedić, Olshevsky and Shi 2017; Qu and Li 2018). The question for the stochastic setting is whether a network of $n$ agents, each with noisy gradients, matches centralized SGD that averages $n$ samples per step. This mission is the second of two on the paper: it covers the diminishing stepsize $\alpha_k=\theta/(m+k)$ and Theorem 2, which gives an $O(1/k)$ rate whose leading constant does not depend on the network.

Setting

There are $n$ agents and a decision space $\mathbb R^p$ with $p\ge1$ . Agent $i$ has a differentiable cost $f_i:\mathbb R^p\to\mathbb R$ that is $\mu$ -strongly convex with $L$ -Lipschitz gradient (Assumption 2); $x^*$ denotes the minimizer of $f=\frac1n\sum_if_i$ . A query of agent $i$ at a point $x$ returns $g_i(x,\xi_i)$ , where $\xi_i\in\mathbb R^d$ is a random sample. The samples $\xi_{i,k}$ (agent $i$ , iteration $k$ ) are mutually independent, and for every fixed $x$

\mathbb E[g_i(x,\xi_{i,k})]=\nabla f_i(x),\qquad \mathbb E\|g_i(x,\xi_{i,k})-\nabla f_i(x)\|^2\le\sigma^2

(Assumption 1). Agents communicate through a nonnegative coupling matrix $\mathbf W=[w_{ij}]$ that is doubly stochastic, has some positive diagonal entry, and whose positive off-diagonal entries form a connected undirected graph (Assumptions 3–4). Write $\rho_w$ for the spectral norm of $\mathbf W-\frac1n\mathbf 1\mathbf 1^\top$ ; it is below $1$ (Lemma 1).

Stack the local variables as $\mathbf x=[x_1,\dots,x_n]^\top\in\mathbb R^{n\times p}$ , let $\bar x=\frac1n\sum_ix_i$ , and use the Frobenius norm, so that $\|\mathbf x-\mathbf 1\bar x\|^2=\sum_i\|x_i-\bar x\|^2$ is the consensus error. DSGT (4) starts from an arbitrary deterministic $\mathbf x_0$ and $y_{i,0}=g_i(x_{i,0},\xi_{i,0})$ , and iterates

x_{i,k+1}=\sum_j w_{ij}\,(x_{j,k}-\alpha_k y_{j,k}),\qquad y_{i,k+1}=\sum_jw_{ij}\,y_{j,k}+g_i(x_{i,k+1},\xi_{i,k+1})-g_i(x_{i,k},\xi_{i,k}),

with stepsize $\alpha_k=\theta/(m+k)$ .

Formalization targets

Goal: Theorem 2 (p. 418)

Let $\theta>1/\mu$ and let $m$ satisfy condition (14) of the paper: $m$ exceeds $\frac\theta2(\mu+L)$ and $\frac{4\theta L\rho_w^2+2\theta L\rho_w\sqrt{1+3\rho_w^2}}{1-\rho_w^2}$ , and a second explicit inequality in $\theta,m,\mu,L,\rho_w$ and $\|\mathbf W-\mathbf I\|$ holds. Then there are constants $C_1,C_2,C_3$ , independent of $k$ , such that for all $k\ge0$

\mathbb E\|\bar x_k-x^*\|^2\le\frac{2\theta^2\sigma^2}{n(\theta\mu-1)(m+k)}+\frac{C_1}{(m+k)^{\theta\mu}}+\frac{C_2}{(m+k)^2},\qquad \mathbb E\|\mathbf x_k-\mathbf 1\bar x_k\|^2\le\frac{C_3}{(m+k)^2}.

The constants may depend on every datum of the run (network, costs, noise law, starting point, $\theta$ , $m$ ), but not on $k$ .

Milestones

(29)–(30), p. 425. The mean-square errors $U_k=\mathbb E\|\bar x_k-x^*\|^2$ , $X_k=\mathbb E\|\mathbf x_k-\mathbf 1\bar x_k\|^2$ , $Y_k=\mathbb E\|\mathbf y_k-\mathbf 1\bar y_k\|^2$ satisfy a componentwise linear system $V_{k+1}\le\mathbf A_kV_k+b_k$ with an explicit $3\times3$ matrix $\mathbf A_k$ .
(31), p. 425. The positivity of $\beta_k$ , used in $\mathbf A_k$ , reduces to an explicit lower bound on $m$ .
(32)–(36), pp. 425–427. By induction, $U_k\le\hat U/(m+k)$ , $X_k\le\hat X/(m+k)^2$ and $Y_k$ is bounded, with explicit $\hat U$ and $\hat X$ .
p. 427. The refined recursion $U_{k+1}\le(1-\alpha_k\mu)U_k+\frac{2\alpha_kL^2}{\mu n}X_k+\frac{\alpha_k^2\sigma^2}n$ .
p. 427. Product bounds $\prod_{t=0}^{k-1}(1-\frac{\theta\mu}{m+t})\le m^{\theta\mu}/(m+k)^{\theta\mu}$ and their tail versions.
p. 427. Sum–integral bounds for $\sum_{t<k}(m+t)^{\theta\mu-3}$ and $\sum_{t<k}(m+t)^{\theta\mu-2}$ .

Significance

The leading term $2\theta^2\sigma^2/(n(\theta\mu-1)(m+k))$ involves neither $\rho_w$ nor the graph: after a transient, the network-average iterate behaves like centralized SGD run on $n$ samples per step, and the error decreases as $1/n$ with the number of agents (Remark 3 of the paper). The consensus error decays one order faster, as $1/k^2$ . The result is a reference point for later analyses of stochastic gradient tracking, which refine the transient time and the dependence on the network.

The theorem is proved in the paper; to the best of current knowledge no part of it is machine-checked. A complete development formalizes the stacked stochastic model, the conditional-expectation estimates behind the linear system, the induction with tuned constants, and the elementary analytic bounds. Two steps of the printed proof need extra care (see Formalization scope), and repairing them is part of the work.

Difficulty

The estimate for the tracker error $Y_k$ couples all three quantities: bounding $Y_{k+1}$ requires $U_k$ and $X_k$ , and $X_{k+1}$ requires $Y_k$ . A direct estimate of any single error therefore does not close, and the rate for $U_k$ cannot be read off from a scalar recursion until $X_k=O(1/k^2)$ is known. The induction closes only for the constants of the paper and under condition (14), which must be checked to hold for all $k$ at once. The probabilistic estimates need independence of the samples across agents and times, since the variance bound $\sigma^2/n$ for the averaged noise uses that the agents' noises are uncorrelated. Finally, the products and sums of real powers $(m+t)^{\theta\mu-2}$ must be bounded uniformly in $k$ , including the regimes $\theta\mu<2$ and $\theta\mu>2$ .

Formalization scope

Points of $\mathbb R^p$ are EuclideanSpace ℝ (Fin p); stacked variables are functions Fin n → E p, and every matrix norm $\|\mathbf x\|$ is the Frobenius sum $\sum_i\|x_i\|^2$ , never the sup norm of the product type. $\|\mathbf W-\mathbf I\|$ is the Frobenius norm and $\rho_w$ the operator norm of Matrix.toEuclideanCLM applied to $\mathbf W-\frac1n\mathbf 1\mathbf 1^\top$ . The noise space is $\mathbb R^d$ (the paper's $\mathbb R^m$ ; $m$ is the stepsize offset). Expectations are Bochner integrals, and every bounded expectation comes with an integrability conjunct, so a non-integrable error cannot satisfy a bound by having integral $0$ . Powers with real exponents are Real.rpow.

Standing assumptions and additions, all stated in the items:

Assumptions 1–4 hold in every run statement; the paper's Theorem 2 cites only Assumptions 1 and 2, but $\rho_w<1$ rests on Assumptions 3–4.
Assumption 1's "each random vector is independent" is read as mutual independence of all $\xi_{i,k}$ ; its conditional moments given a deterministic $x$ become unconditional moments for each fixed $x$ . The oracle $g_i$ is jointly measurable.
$p\ge1$ , and $\rho_w>0$ (condition (14) and $C$ divide by $\rho_w^2$ ).
The linear system (29) and the induction carry $3\alpha_kL\le1$ (respectively $3\theta L\le m$ ), which the derivation of Lemma 4 (20) uses on p. 445 without stating it. The sum bound for $\sum(m+t)^{\theta\mu-3}$ carries $\theta\mu\ne2$ . The goal carries neither: its constants absorb a finite transient.

The constants $C_1,C_2,C_3$ of the goal are quantified after all data and before $k$ ; a statement with the constants chosen after $k$ would be trivially true and is not this theorem. The goal mentions only the iterates, $x^*$ , $\theta$ , $m$ and the constants of the page, not the auxiliary quantities of the proof.

Contributions welcome: proofs of the analytic milestones (products, sums), the conditional-expectation estimates behind (29), and the repair of the two gaps of the printed proof. The model definitions are shared with the companion mission on constant stepsizes.

Selected references

S. Pu and A. Nedić, Distributed stochastic gradient tracking methods, Mathematical Programming 187 (2021) 409–457. https://doi.org/10.1007/s10107-020-01487-0
A. Nedić, A. Olshevsky and W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM Journal on Optimization 27 (2017) 2597–2633. https://doi.org/10.1137/16M1084316
G. Qu and N. Li, Harnessing smoothness to accelerate distributed optimization, IEEE Transactions on Control of Network Systems 5 (2018) 1245–1260. https://doi.org/10.1109/TCNS.2017.2698261
A. Nemirovski, A. Juditsky, G. Lan and A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19 (2009) 1574–1609. https://doi.org/10.1137/070704277

9 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Distributed Stochastic Gradient Tracking Methods I: With a Constant Stepsize, DSGT's Limiting Mean-Square Error Is at Most (Γ+1)ασ²/(Γμn) Plus a Network TermResearch Paper

Distributed learning with noisy gradients

Many learning and estimation problems are solved by a network of agents: each agent holds part of the data, can talk only to its neighbours, and wants to compute the minimizer of the average of all agents' objectives. Examples are sensor networks, multi-robot systems, and data-parallel training without a central server (Nedić and Ozdaglar 2009; Lian et al. 2017). In these settings the agents rarely know their exact gradients; they sample them, one data point or one mini-batch at a time.

Gradient tracking methods let each agent keep, next to its estimate of the minimizer, a running estimate of the network-average gradient. With exact gradients they converge linearly with a constant stepsize (Qu and Li 2018; Nedić, Olshevsky and Shi 2017), which plain distributed gradient descent does not. S. Pu and A. Nedić (Math. Program. 187 (2021) 409–457) analysed the same scheme when every gradient is replaced by an unbiased noisy sample, and called it DSGT (distributed stochastic gradient tracking). This mission formalizes their constant-stepsize result, Theorem 1.

Setting

There are $n$ agents. Agent $i$ holds a cost $f_i:\mathbb R^p\to\mathbb R$ , and the agents seek

x^*\in\arg\min_{x\in\mathbb R^p} f(x),\qquad f(x)=\frac1n\sum_{i=1}^n f_i(x).

Each $f_i$ is $\mu$ -strongly convex with $L$ -Lipschitz gradient: $\langle\nabla f_i(x)-\nabla f_i(x'),x-x'\rangle\ge\mu\|x-x'\|^2$ and $\|\nabla f_i(x)-\nabla f_i(x')\|\le L\|x-x'\|$ .

Noisy gradients. At time $k$ agent $i$ draws a random sample $\xi_{i,k}$ and observes $g_i(x,\xi_{i,k})$ , with $\mathbb E[g_i(x,\xi_{i,k})]=\nabla f_i(x)$ and $\mathbb E\|g_i(x,\xi_{i,k})-\nabla f_i(x)\|^2\le\sigma^2$ ; the samples are independent.

The network. Agents are coupled by a nonnegative doubly stochastic matrix $\mathbf W=[w_{ij}]$ (rows and columns sum to $1$ ), with $w_{ij}>0$ exactly when $i$ and $j$ communicate, some $w_{ii}>0$ , and a connected undirected communication graph. The number

\rho_w=\Big\|\mathbf W-\tfrac1n\mathbf 1\mathbf 1^\top\Big\|_2<1,

the spectral norm, measures how fast one round of averaging brings the agents together.

DSGT. Each agent keeps $x_{i,k}$ and a tracker $y_{i,k}$ . Stacking them as rows of $\mathbf x_k,\mathbf y_k\in\mathbb R^{n\times p}$ and writing $G(\mathbf x,\boldsymbol\xi)$ for the matrix with rows $g_i(x_i,\xi_i)$ , the method with constant stepsize $\alpha>0$ is

\mathbf x_{k+1}=\mathbf W(\mathbf x_k-\alpha\mathbf y_k),\qquad \mathbf y_{k+1}=\mathbf W\mathbf y_k+G(\mathbf x_{k+1},\boldsymbol\xi_{k+1})-G(\mathbf x_k,\boldsymbol\xi_k),

started from a deterministic $\mathbf x_0$ and $\mathbf y_0=G(\mathbf x_0,\boldsymbol\xi_0)$ . The two error measures are the distance of the average $\bar x_k=\frac1n\sum_ix_{i,k}$ to $x^*$ and the consensus error $\|\mathbf x_k-\mathbf 1\bar x_k\|^2=\sum_i\|x_{i,k}-\bar x_k\|^2$ .

Formalization targets

Goal: Theorem 1

Fix $\Gamma>1$ and a stepsize $\alpha$ below the explicit threshold (7) of the paper (a minimum of three expressions in $\rho_w$ , $\|\mathbf W-\mathbf I\|$ , $\mu$ , $L$ , $\Gamma$ ). Then a certain explicit $3\times3$ matrix $\mathbf A$ has spectral radius $\rho(\mathbf A)<1$ , and with $M_\sigma=[3\alpha^2L^2+2(\alpha L+1)(n+1)]\sigma^2$ ,

\limsup_{k\to\infty}\mathbb E\|\bar x_k-x^*\|^2\le\frac{\Gamma+1}{\Gamma}\frac{\alpha\sigma^2}{\mu n}+\frac{\Gamma+1}{\Gamma-1}\,\frac{4\alpha^2L^2(1+\alpha\mu)(1+\rho_w^2)\rho_w^2}{\mu^2n(1-\rho_w^2)^3}\,M_\sigma,

\limsup_{k\to\infty}\mathbb E\|\mathbf x_k-\mathbf 1\bar x_k\|^2\le\frac{\Gamma+1}{\Gamma-1}\,\frac{4\alpha^2(1+\rho_w^2)\rho_w^2(2\alpha^2L^3\sigma^2+\mu M_\sigma)}{\mu(1-\rho_w^2)^3}.

The constants are the paper's, so the goal is stated with them.

Companion: Corollary 1

Under a further stepsize condition (13), $\rho(\mathbf A)\le1-\frac{\Gamma-1}{\Gamma+1}\alpha\mu$ .

Milestones

The milestones follow the paper's proof: the tracking identity (6); Lemma 1 on $\rho_w$ ; the one-step conditional estimates of Lemmas 2–4 and the auxiliary Lemmas 8–9; the linear system of inequalities (21) and its iterate (22); the determinant criterion Lemma 5; the bound $\det(\mathbf I-\mathbf A)>0$ under the relations (23)–(25); and the lower bound (27) on the auxiliary parameter $\beta$ .

Significance

The first term of the bound on $\mathbb E\|\bar x_k-x^*\|^2$ , $\alpha\sigma^2/(\mu n)$ up to the factor $(\Gamma+1)/\Gamma$ , is the error of centralized stochastic gradient descent that averages $n$ samples per step; it does not depend on the network. The network enters only through terms of order $\alpha^2$ . So for small stepsizes a decentralized method with gradient tracking pays nothing in the limiting error for having no central server. Theorem 1 is one of the standard references for this statement in decentralized stochastic optimization.

The result is proved in the paper, with constants. It has no machine-checked proof that we know of. Formalizing it produces a checked development of the linear-system method for distributed algorithms: conditional moment bounds for coupled stochastic recursions, a $3\times3$ linear system of inequalities between expectations, and a Perron–Frobenius criterion for its stability. The same pattern recurs in the analysis of many gradient-tracking and variance-reduced decentralized methods.

Difficulty

The obvious argument would bound each error by itself, but the three quantities $\mathbb E\|\bar x_k-x^*\|^2$ , $\mathbb E\|\mathbf x_k-\mathbf 1\bar x_k\|^2$ and $\mathbb E\|\mathbf y_k-\mathbf 1\bar y_k\|^2$ feed into one another, and none of them contracts on its own. The tracker error in particular depends on the next iterate, which itself depends on the current noise, so the cross terms do not vanish in conditional expectation and must be estimated separately (Lemmas 8 and 9).

Once the coupled system is set up, its stability needs the spectral radius of a nonnegative $3\times3$ matrix whose entries depend on all constants at once, and the explicit limiting bounds need its inverse. The determinant criterion of Lemma 5 rests on Perron–Frobenius theory, which Mathlib provides only in part.

Formalization scope

Stacked variables are Fin n → EuclideanSpace ℝ (Fin p). Every matrix norm is written out: $\|\mathbf x-\mathbf 1\bar x\|^2=\sum_i\|x_i-\bar x\|^2$ (Frobenius), $\|\mathbf W-\mathbf I\|$ is the Frobenius norm of the $n\times n$ matrix, and $\rho_w$ is the operator norm of $\mathbf W-\frac1n\mathbf 1\mathbf 1^\top$ on Euclidean $\mathbb R^n$ . Spectral radii are taken over $\mathbb C$ , so complex eigenvalues count. Expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion. " $\limsup_k a_k\le B$ " is stated as "for every $\varepsilon>0$ , eventually $a_k\le B+\varepsilon$ ". $\mathcal F_k$ is the σ-algebra generated by $\boldsymbol\xi_0,\dots,\boldsymbol\xi_{k-1}$ , and conditional statements hold almost surely.

Standing assumptions and additions, all stated in the items:

Assumptions 3–4 on $\mathbf W$ are hypotheses of every statement about the iterates, although Theorem 1 cites only Assumptions 1–2.
Independence of the noise is mutual independence of all $\xi_{i,k}$ ; $g_i$ is jointly measurable; $p\ge1$ .
$\rho_w>0$ , because $\beta$ , $\mathbf A$ and (7) divide by $\rho_w$ .
$3\alpha L\le1$ in (20), (21), (22) and Theorem 1: the last step of the paper's proof of (20) needs it, and (7) does not imply it in general (for $\rho_w=0.01$ , $\Gamma=1.1$ , $\mu=L$ it allows $\alpha\approx0.48/L$ ).

The goal speaks only about the DSGT iterates, $x^*$ and the matrix $\mathbf A$ ; it does not assume the linear system (21), $\rho(\mathbf A)<1$ or any estimate of the proof. The clause of Theorem 1 that $\sup_{l\ge k}\mathbb E[\cdot]$ approaches the limsup at the rate $\mathcal O(\rho(\mathbf A)^k)$ carries an unquantified constant and is not formalized: the paper's proof yields only the envelope (22) and the limit of its right-hand side, not a rate at which $\sup_{l\ge k}\mathbb E[\cdot]$ reaches the limsup; the envelope (22) is a milestone. Theorem 2 (diminishing stepsizes) is the subject of the second mission of the series.

A complete development needs conditional expectations of functions of independent samples, a Frobenius-norm calculus for stacked vectors, the consensus contraction of Lemma 1, and the Perron–Frobenius facts behind Lemma 5. The last two are reusable beyond this mission. Proofs of any milestone, and of the deterministic matrix lemmas in particular, are welcome independently.

Selected references

S. Pu, A. Nedić, Distributed stochastic gradient tracking methods, Mathematical Programming 187 (2021) 409–457. https://doi.org/10.1007/s10107-020-01487-0
A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27 (2017) 2597–2633. https://arxiv.org/abs/1607.03218
G. Qu, N. Li, Harnessing smoothness to accelerate distributed optimization, IEEE Trans. Control Netw. Syst. 5 (2018) 1245–1260. https://arxiv.org/abs/1605.07112
A. Nedić, A. Ozdaglar, Distributed subgradient methods for multi-agent optimization, IEEE Trans. Automat. Control 54 (2009) 48–61. https://doi.org/10.1109/TAC.2008.2009515
X. Lian, C. Zhang, H. Zhang, C.-J. Hsieh, W. Zhang, J. Liu, Can decentralized algorithms outperform centralized algorithms? A case study for decentralized parallel stochastic gradient descent, NeurIPS 2017. https://arxiv.org/abs/1705.09056

18 thms2 active usersReviewed

Operations Research Optimal Transport Statistics·Captain: mikedeng1

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 3: Under T₂(τ), W₂-Robust Loss at Radius ρ̃ₙ Bounds True Loss up to 4r⋆+2εₙ+ħρ̃ₙ²Research Paper

Motivation

Wasserstein distributionally robust optimization (Wasserstein DRO) replaces the empirical loss $\mathbb E_{\mathbb P_n}[f]$ of a decision by its worst case over all distributions within Wasserstein distance $\rho$ of the empirical distribution $\mathbb P_n$ . It is used in operations research (newsvendor, portfolio selection) and machine learning (adversarially robust training, regularized regression) because the robust loss is a computable upper estimate of the unknown true loss. The question every user faces is how large $\rho$ must be. Measure-concentration results for the empirical measure in Wasserstein distance (Fournier and Guillin, 2015) require $\rho\sim n^{-1/d}$ on a $d$ -dimensional space, which is useless in high dimension.

Gao (arXiv:2009.04382, Operations Research 2023) shows that a radius of order $1/\sqrt n$ suffices, with no dependence on dimension, as long as the true distribution satisfies a transportation-information inequality and the loss class has controlled complexity. This mission covers the paper's result for the 2-Wasserstein distance, where the robust loss is linked to gradient regularization. Two sibling missions cover the variation-concentration inequality (Theorem 1) and the 1-Wasserstein / Lipschitz case (Corollary 4).

Setting

$\mathcal Z$ is a separable real Banach space with norm $\|\cdot\|$ and dual norm $\|\cdot\|_*$ . $\mathcal P_2(\mathcal Z)$ is the set of Borel probability measures with finite second moment, and $\mathcal W_2$ is the 2-Wasserstein distance: $\mathcal W_2(\mathbb P,\mathbb Q)^2$ is the infimum of $\mathbb E_\pi\|\tilde z-z\|^2$ over couplings $\pi$ of $\mathbb P$ and $\mathbb Q$ .

The Wasserstein regularizer of a loss $f$ at a nominal distribution $\mathbb Q$ and radius $\rho\ge0$ is

\mathcal R_{\mathbb Q,2}(\rho;f)=\sup\{\mathbb E_{\mathbb P}[f]:\mathbb P\in\mathcal P_2(\mathcal Z),\ \mathcal W_2(\mathbb P,\mathbb Q)\le\rho\}-\mathbb E_{\mathbb Q}[f].

A distribution $\mathbb P$ satisfies the transportation-information inequality $T_2(\tau)$ if $\mathcal W_2(\mathbb Q,\mathbb P)\le\sqrt{\tau H(\mathbb Q\|\mathbb P)}$ for every $\mathbb Q\in\mathcal P_2(\mathcal Z)$ , with $H$ the relative entropy. Gaussian measures are the standard example.
A class $\mathcal F$ of losses satisfies Assumption 2 with constant $\hbar>0$ if each $f\in\mathcal F$ is differentiable and $\|\nabla f(\tilde z)-\nabla f(z)\|_*\le\hbar\|\tilde z-z\|$ .
The gradient norm of $f$ under $\mathbb Q$ is $\|\|\nabla f\|_*\|_{\mathbb Q,2}=(\mathbb E_{\mathbb Q}\|\nabla f\|_*^2)^{1/2}$ .
A sample $z_1,\dots,z_n$ is i.i.d. from $\mathbb P_{\mathrm{true}}$ , and $\mathbb E_\otimes$ is expectation over it. The Rademacher complexity of a class $\mathcal H$ is $\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$ , with $\mathfrak R_n(\mathcal H)=\mathbb E_\sigma\sup_{h\in\mathcal H}\frac1n\sum_i\sigma_ih(z_i)$ and $\sigma_i$ independent uniform signs.
The normalized gradient class is $\mathcal G=\{\|\nabla f\|_*^2/\|\|\nabla f\|_*\|^2_{\mathbb P_{\mathrm{true}},2}:f\in\mathcal F\}$ .
Assumption 5 asks for a sub-root function $\psi_n$ (non-negative, non-decreasing, non-constant, with $\psi_n(r)/\sqrt r$ non-increasing) that dominates the localized complexities $\mathbb E_\otimes[\mathfrak R_n(\{cf:f\in\mathcal F,0\le c\le1,c^2\|\|\nabla f\|_*\|^2_{\mathbb P_{\mathrm{true}},2}\le r\})]$ . Its positive fixed point is $r_{n\star}$ .

In Lean the mission's own objects live in the namespace WassFSG.Grad: W2sq, IsP2, regularizer, IsT2, GradLipBound, gradNorm, empGradNorm, gradClass, localized, SubRootLocalComplexity, productRegularizer, epsN, rhoN and rhoTilde. The empirical mean and measure (empMean, empMeasure), the Rademacher complexity (radComp, expectedRad), sub-root functions (IsSubRoot), the class −F (negClass) and the probability count (peelCount) are the shared definitions of the series in WassFSG.Lip.

Formalization targets

Goal: Corollary 6 (2-Wasserstein DRO), pp. 11–12

Write $\epsilon_n=(\hbar\tau t+1+\mathbb E_\otimes[\mathfrak R_n(\mathcal G)])/n$ and $\rho_n=2\sqrt{\tau t/n}\,(1+\mathbb E_\otimes[\mathfrak R_n(\mathcal G)])+\sqrt{4r_{n\star}+2\epsilon_n}$ . Assume in addition that $\|\nabla f(z)\|_*/\|\|\nabla f\|_*\|_{\mathbb P_{\mathrm{true}},2}\le\kappa_g$ , and set $\tilde\rho_n=\rho_n(1+2\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]+\kappa_g^2\sqrt{t/(2n)})$ . If $2\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]+\kappa_g^2\sqrt{t/(2n)}<1/2$ , then with probability at least $1-(N_2+1)e^{-t}$ , every $f\in\mathcal F$ satisfies

\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\tilde\rho_n\|\|\nabla f\|_*\|_{\mathbb P_n,2}+4r_{n\star}+2\epsilon_n

and

\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\mathcal R_{\mathbb P_n,2}(\tilde\rho_n;f)+4r_{n\star}+2\epsilon_n+\hbar\tilde\rho_n^2,

where $N_2=\max(0,\lceil\log_2(\gamma_2\sqrt{\tau tn})\rceil)+1$ .

Milestones, in proof order

Lemma 7 (symmetrization).
Lemma 9 for $p=2$ : a uniform deviation bound with the transport term $\mathcal R_{\otimes,2}(\sqrt{\tau t/n};-\mathcal F)$ .
Lemma 13: the transport term is bounded by gradient norms plus $\hbar\tau t/n$ .
Lemma 14: peeling, which turns the class supremum into each $f$ 's own gradient norm.
Lemma 10: the fixed-point bound $B^2\le r_0\le2A+B^2$ .
Theorem 3: distribution-dependent gradient regularization, $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\rho_n\|\|\nabla f\|_*\|_{\mathbb P_{\mathrm{true}},2}+4r_{n\star}+2\epsilon_n$ .
Lemma 2: $|\mathcal R_{\mathbb Q,2}(\rho;f)-\rho\|\|\nabla f\|_*\|_{\mathbb Q,2}|\le\hbar\rho^2$ .

Significance

Corollary 6 says that solving 2-Wasserstein DRO at a radius $\tilde\rho_n=O(1/\sqrt n)$ gives, with high probability, an upper bound on the true loss of every decision, up to an $O(1/n)$ gap. This holds whenever $\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]=O(1)$ and $r_{n\star}=O(1/n)$ , for example for finite-VC gradient classes, smooth neural networks and Markowitz portfolios (Section 5 of the paper). Combined with the robust-solution argument of Remark 1, this gives $\tilde O(1/\sqrt n)$ excess-risk bounds for the robust solution. Theorem 3 alone is a generalization bound for gradient-norm regularization, an estimator used in its own right.

None of these results is known to be machine-checked. The mission produces a Lean statement of the full chain from a transportation inequality to the DRO guarantee. It also produces reusable infrastructure: the 2-Wasserstein regularizer on a Banach space, transportation-information inequalities, local Rademacher complexities with sub-root bounds, and a peeling argument. The printed failure probability needs a correction (see below), so the formal statement is itself a contribution.

Difficulty

The obvious route is to bound $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]-\mathbb E_{\mathbb P_n}[f]$ by $\mathcal W_2(\mathbb P_n,\mathbb P_{\mathrm{true}})$ times a gradient bound. It fails because $\mathcal W_2(\mathbb P_n,\mathbb P_{\mathrm{true}})$ decays like $n^{-1/d}$ . The radius must instead come from concentration of the loss, and the result has to hold uniformly over $\mathcal F$ , which requires symmetrization and a localization in the gradient norm.

Three points carry the weight:

The transport term of Lemma 9 has to be converted into a gradient norm with a quadratic remainder. This is the step that uses smoothness.
The population gradient norm, which is unknown, has to be replaced by its empirical counterpart in Corollary 6. This needs a separate concentration step for the class $\mathcal G$ .
Every constant (the $(1+\mathbb E_\otimes[\mathfrak R_n(\mathcal G)])$ factors, $\epsilon_n$ , $\tilde\rho_n$ ) appears in the statement and must come out exactly.

Formalization scope

The source is arXiv:2009.04382 (preprint basis); its printed page numbers equal the PDF's.

Standing conventions:

$\mathcal Z$ is a complete, second-countable real normed space with its Borel $\sigma$ -algebra. The paper says "Banach space"; separability and Borel are the setting of the transport results it cites.
$n\ge1$ .
$\nabla f$ is the Fréchet derivative, and its norm is the operator (dual) norm.
$\mathcal W_2$ is used through its square, via the published optimal-transport cost.
Expectations inside the regularizer and Rademacher complexities are extended integrals in $\overline{\mathbb R}$ . $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]$ is the Bochner integral, which is integrable because Assumption 2 gives quadratic growth and $T_2(\tau)$ a finite second moment.
"With probability at least $1-\delta$ , for every $f$ " is the outer measure of the set of samples where some $f$ fails, bounded by $\delta$ .
The page's $\min_{\lambda\ge0}$ in $\mathcal R_{\otimes,2}$ is read as an infimum.

Added hypotheses, all implicit on the page:

$\|\|\nabla f\|_*\|_{\mathbb P_{\mathrm{true}},2}>0$ for $f\in\mathcal F$ , so that $\mathcal G$ and $\kappa_g$ are defined.
$\mathbb E_\otimes[\mathfrak R_n(\mathcal G)]$ is finite. It is passed as a real number; if it is infinite, the bounds are vacuous.
The class bound $\gamma_2$ in Lemma 14, which its proof uses.
$r_{n\star}>0$ .
Continuity and integrability of the family in Lemma 7.

Corrected slip. The printed failure probability $\lceil\log_2(\sqrt{\gamma_2\tau tn})\rceil e^{-t}$ (Theorem 3, Corollary 6) is negative for small $\gamma_2\sqrt{\tau tn}$ and disagrees with Lemma 14, and the peeling in Lemma 14's proof misses one band. The Lean uses $N_2=\max(0,\lceil\log_2(\gamma_2\sqrt{\tau tn})\rceil)+1$ events (and $N_2+1$ in Corollary 6). Milestone texts keep the printed count. Lemma 13's printed proof contains a step that is false in general for signed Rademacher sums. The statement is posed as printed; a correct argument uses the non-negativity of $\mathcal G$ .

Ruled out. A trivializing encoding would take $r_{n\star}=0$ , let the radii be free existentials, use a real supremum (which is $0$ on unbounded sets), or rely on Lean's $x/0=0$ for $\mathcal G$ . None of these is used: every radius is the printed formula, and each degenerate case is excluded by a hypothesis.

Welcome contributions include proofs of the milestones and general lemmas on the Wasserstein regularizer (Lemma 2 is a first-order expansion). McDiarmid's inequality, which Corollary 6's proof uses, is not a milestone and is a welcome general-purpose result.

Selected references

R. Gao, Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality, Operations Research, 2023. arXiv:2009.04382
P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. doi:10.1214/009053605000000282
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162, 2015. doi:10.1007/s00440-014-0583-7
R. Gao, X. Chen, A. J. Kleywegt, Wasserstein distributionally robust optimization and variation regularization, Operations Research, 2024. arXiv:1712.06050
N. Gozlan, C. Léonard, Transport inequalities. A survey, Markov Processes and Related Fields 16, 2010. arXiv:1003.3852

14 thms2 active usersReviewed

Operations Research Optimal Transport Statistics·Captain: mikedeng1

Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality 2: Under T₁(τ), W₁-Robust Loss at Radius 2√(τt/n)+√(4r⋆+2/n) Bounds the True LossResearch Paper

Why the radius of a Wasserstein ball matters

Wasserstein distributionally robust optimization (DRO) replaces the empirical loss $\mathbb E_{\mathbb P_n}[f]$ of a decision or model $f$ by its worst case over all distributions within a Wasserstein distance $\rho$ of the empirical distribution $\mathbb P_n$ . It is used in operations research (newsvendor, portfolio and inventory problems) and in machine learning (robust classification and regression), and it is attractive because the worst-case loss is often a computable convex program (Mohajerin Esfahani and Kuhn 2018; Gao and Kleywegt 2023).

The practical question is how large $\rho$ must be for the robust loss to upper-bound the true, unknown loss $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]$ with high probability. The classical answer goes through measure concentration of $\mathbb P_n$ around $\mathbb P_{\mathrm{true}}$ in Wasserstein distance (Fournier and Guillin 2015), which forces $\rho_n \asymp n^{-1/d}$ in dimension $d$ : the curse of dimensionality. Rui Gao's paper (arXiv:2009.04382; Operations Research, 2023) shows that a radius of order $n^{-1/2}$ suffices, independently of $d$ , under a transportation-information inequality and a complexity assumption on the loss class. This mission formalizes the paper's result for the 1-Wasserstein distance (Sec. 4.2, Theorem 2 and Corollary 4).

Setting

Let $\mathcal Z$ be a separable real Banach space with norm $\|\cdot\|$ . $\mathcal P_1(\mathcal Z)$ is the set of Borel probability measures $\mathbb Q$ with $\mathbb E_{\mathbb Q}\|z\|<\infty$ . The 1-Wasserstein distance is

\mathcal W_1(\mathbb P,\mathbb Q)=\inf\{\mathbb E_\pi\|\tilde z-z\| : \pi \text{ has marginals }\mathbb P,\mathbb Q\}.

For a loss $f:\mathcal Z\to\mathbb R$ the Wasserstein regularizer is the gap between robust and nominal loss,

\mathcal R_{\mathbb Q,1}(\rho;f)=\sup\{\mathbb E_{\mathbb P}[f]:\mathbb P\in\mathcal P_1(\mathcal Z),\ \mathcal W_1(\mathbb P,\mathbb Q)\le\rho\}-\mathbb E_{\mathbb Q}[f].

The Lipschitz norm $\|f\|_{\mathrm{Lip}}$ is the best Lipschitz constant of $f$ .

The data are $n$ i.i.d. samples $z_1,\dots,z_n$ from $\mathbb P_{\mathrm{true}}$ , with empirical distribution $\mathbb P_n=\frac1n\sum_i\delta_{z_i}$ . $\mathbb P_\otimes$ and $\mathbb E_\otimes$ refer to the product law. The distribution $\mathbb P_{\mathrm{true}}$ satisfies the transportation-information inequality $T_1(\tau)$ if $\mathcal W_1(\mathbb Q,\mathbb P_{\mathrm{true}})\le\sqrt{\tau H(\mathbb Q\|\mathbb P_{\mathrm{true}})}$ for every $\mathbb Q\in\mathcal P_1(\mathcal Z)$ , where $H$ is relative entropy. It holds, for example, for every distribution with a sub-Gaussian norm.

The loss class $\mathcal F$ satisfies Assumption 1(I) if $f(\tilde z)-f(z)\le\gamma_1\|\tilde z-z\|$ for all $f\in\mathcal F$ , with $\gamma_1>0$ . It satisfies Assumption 1(II) if $\mathcal Z$ is unbounded and each $f$ attains its Lipschitz norm at infinity, i.e. $\limsup_{\|z-z_0\|\to\infty}(f(z)-f(z_0))/\|z-z_0\|=\|f\|_{\mathrm{Lip}}$ for some $z_0$ .

The Rademacher complexity of a class $\mathcal G$ on the sample is $\mathfrak R_n(\mathcal G)=\mathbb E_\sigma[\sup_{g\in\mathcal G}\frac1n\sum_i\sigma_i g(z_i)]$ , with i.i.d. uniform signs $\sigma_i$ . Assumption 5 asks for a sub-root function $\psi_n$ that dominates the localized complexities:

\psi_n(r)\ge\mathbb E_\otimes\big[\mathfrak R_n(\{cf:f\in\mathcal F,\ 0\le c\le1,\ \|cf\|^2_{\mathrm{Lip}}\le r\})\big].

Sub-root means non-negative, non-decreasing, non-constant, with $\psi_n(r)/\sqrt r$ non-increasing. Its positive fixed point is $r_{n\star}=\psi_n(r_{n\star})$ .

Formalization targets

Goal: Corollary 4 (1-Wasserstein DRO)

Set $\rho_n=2\sqrt{\tau t/n}+\sqrt{4r_{n\star}+2/n}$ and $N_1(t,n)=\max(0,\lceil\log_2(\gamma_1\sqrt{\tau tn})\rceil)+1$ . Under $T_1(\tau)$ , Assumption 1 and Assumption 5, for $t>0$ , with probability at least $1-N_1(t,n)e^{-t}$ ,

\mathbb E_{\mathbb P_{\mathrm{true}}}[f]\le\mathbb E_{\mathbb P_n}[f]+\mathcal R_{\mathbb P_n,1}(\rho_n;f)+4r_{n\star}+\frac2n\qquad\forall f\in\mathcal F.

Milestones

Lemma 7 (symmetrization): $\mathbb E_\otimes\sup_h\{\mathbb E_{\mathbb P_{\mathrm{true}}}h-\mathbb E_{\mathbb P_n}h\}\le2\mathbb E_\otimes[\mathfrak R_n(\mathcal H)]$ .
Lemma 9 ( $p=1$ ): uniform concentration with the product regularizer $\mathcal R_{\otimes,1}(\sqrt{\tau t/n};-\mathcal F)$ .
Lemma 11: the same with $\sqrt{\tau t/n}\sup_{f\in\mathcal F}\|f\|_{\mathrm{Lip}}$ .
Lemma 12 (peeling): each $f$ 's own $2\sqrt{\tau t/n}\|f\|_{\mathrm{Lip}}$ , at cost $1/n$ and $N_1$ events.
Lemma 10: the largest root $r_0$ of $B\sqrt r+A=r$ lies in $[B^2,2A+B^2]$ .
Theorem 2 (Lipschitz regularization): the goal with $\mathcal R_{\mathbb P_n,1}(\rho_n;f)$ replaced by $\rho_n\|f\|_{\mathrm{Lip}}$ ; needs Assumption 1(I) only.
Lemma 1: $\mathcal R_{\mathbb Q,1}(\rho;f)\le\rho\|f\|_{\mathrm{Lip}}$ , with equality under Assumption 1(II).

Significance

Corollary 4 justifies a radius of order $1/\sqrt n$ whenever $r_{n\star}=\tilde O(1/n)$ , which the paper verifies for kernel classes and other examples (Sec. 5). That rate is the one used in practice, and it was not covered by the concentration-based theory. Theorem 2 is a dimension-free generalization bound for Lipschitz-regularized learning in its own right. Lemma 1 links the two by identifying the 1-Wasserstein regularizer with Lipschitz regularization.

The results are proved in the paper. As far as known, none of them is machine-checked. A formalization would check the paper's peeling and fixed-point arguments, which turn out to need a corrected failure-probability count (see Formalization scope). It would also produce reusable Lean infrastructure: Rademacher complexity in the $\frac1n$ , no-absolute-value normalization, localized classes, sub-root functions, $T_1(\tau)$ , and the Wasserstein regularizer on a Banach space.

Difficulty

The obvious route bounds $\mathcal W_1(\mathbb P_n,\mathbb P_{\mathrm{true}})$ and uses Kantorovich–Rubinstein duality. It fails because $\mathcal W_1(\mathbb P_n,\mathbb P_{\mathrm{true}})$ is of order $n^{-1/d}$ , so no dimension-free radius comes out. A dimension-free bound must therefore hold uniformly over an infinite loss class without passing through the distance between $\mathbb P_n$ and $\mathbb P_{\mathrm{true}}$ , and the bound must scale with each function's own Lipschitz norm rather than the class-wide constant $\gamma_1$ . The statements also need measure-theoretic infrastructure that Mathlib lacks or has only partly: transport inequalities, Rademacher averages over classes, and suprema of uncountable families inside expectations.

Formalization scope

Space. $\mathcal Z$ is a real Banach space with its Borel $\sigma$ -algebra, and second countable (separable). The paper says "Banach space"; Borel and separability are implicit in the transport and duality results it cites. The Borel structure is load-bearing for transport costs.
Distances and expectations. $\mathcal W_1$ is the published RWPI.SqrtLasso.transportCost with cost $\|u-w\|$ . Expectations inside regularizers and complexities are extended integrals $\int\varphi^+-\int\varphi^-$ in $[-\infty,\infty]$ (published ModelRiskOT.Duality.extIntegral). $\mathbb E_{\mathbb P_{\mathrm{true}}}[f]$ is the Bochner integral; it is the true expectation because a Lipschitz $f$ is integrable under $\mathbb P_{\mathrm{true}}\in\mathcal P_1$ . Relative entropy is Mathlib's klDiv.
High-probability statements. "With probability at least $1-\delta$ , for every $f\in\mathcal F$ " is the bound $\mathbb P_\otimes\{z:\exists f\in\mathcal F\text{ violating the bound}\}\le\delta$ in outer measure, so the quantifier over $f$ sits inside the event. $\mathcal R_{\mathbb P_n,1}$ uses the empirical distribution of the same sample.
Samples and constants. $n\ge1$ . $r_{n\star}>0$ is a positive fixed point of $\psi_n$ ; taking $r_{n\star}=0$ when $\psi_n(0)=0$ would trivialize the goal and is excluded. $\rho_n$ is the printed formula, not a free radius. Assumption 1(II)'s $\operatorname{diam}(\mathcal Z)=\infty$ is stated as " $\mathcal Z$ is unbounded".
Corrected probability count. The paper prints the failure probability of Lemma 12, Theorem 2 and Corollary 4 as $\lceil\log_2(\sqrt{\gamma_1\tau tn})\rceil e^{-t}$ . That count is negative when $\gamma_1\sqrt{\tau tn}\le1/2$ , which makes the printed claim false. It also puts $\gamma_1$ inside the root, against the proof's own choice of $K$ , and the proof's peeling shells leave a band of Lipschitz norms uncovered. All three statements use the corrected count $N_1(t,n)$ .
Other readings. $\mathcal R_{\otimes,1}$ uses an infimum where the page writes $\min$ . Lemma 9 is stated for $p=1$ only. In Lemma 7 the family consists of continuous, $\mathbb P_{\mathrm{true}}$ -integrable functions. Continuity makes every supremum inside an expectation lower semicontinuous, hence measurable, and the same holds automatically for the Lipschitz classes of the other statements.

Lemma 5 (concentration on the product space under $T_p(\tau)$ , used in Lemma 9's proof) belongs to the companion mission on variation-based concentration and is not restated here. Contributions are welcome at every level: sub-root fixed-point facts, symmetrization, the peeling lemma, and Lemma 1's two directions are independent entry points.

The source is arXiv:2009.04382; its printed page numbers equal the PDF's page numbers.

Selected references

R. Gao, Finite-Sample Guarantees for Wasserstein Distributionally Robust Optimization: Breaking the Curse of Dimensionality, Operations Research, 2023. https://arxiv.org/abs/2009.04382
P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
R. Gao, X. Chen, A. J. Kleywegt, Wasserstein distributionally robust optimization and variation regularization, Operations Research, 2024. https://arxiv.org/abs/1712.06050
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162, 2015. https://doi.org/10.1007/s00440-014-0583-7
N. Gozlan, C. Léonard, Transport inequalities. A survey, Markov Processes and Related Fields 16, 2010. https://arxiv.org/abs/1003.3852

12 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Minimizing Finite Sums with the Stochastic Average Gradient: SAG with Step 1/(16L) Has E[g(x̄ᵏ)] − g(x*) ≤ (32n/k)C₀, and Rate (1 − min{μ/(16L), 1/(8n)})ᵏC₀ if g Is μ-Strongly ConvexResearch Paper

Motivation

Many problems in statistics and machine learning minimize a finite sum: an average of $n$ smooth convex losses, one per data point, often plus a strongly convex regularizer. The full gradient method costs $n$ component gradients per iteration and converges at rate $O(1/k)$ , or linearly when the objective is strongly convex (Nesterov, 2004). The stochastic gradient method costs one component gradient per iteration, but its rates are sublinear, $O(1/\sqrt k)$ and $O(1/k)$ , and these are optimal for algorithms that only see unbiased gradient estimates (Nemirovski et al., 2009).

The stochastic average gradient (SAG) method of Le Roux, Schmidt and Bach exploits the finiteness of the sum: it keeps the last gradient computed for every component and steps along their average. It was the first method with the iteration cost of the stochastic gradient method and the rates of the full gradient method.

Timeline.

2007: Blatt, Hero and Gauchman prove convergence of the incremental aggregated gradient (IAG) method, the deterministic-order ancestor of SAG (SIAM J. Optim. 18(1)).
2012: Le Roux, Schmidt and Bach introduce SAG and prove linear convergence of $\mathbb E\|x^k-x^*\|^2$ for strongly convex sums, with step $1/(2nL)$ , and a faster rate with step $1/(2n\mu)$ when $n\ge 8L/\mu$ (arXiv:1202.6258).
2013–2017: Schmidt, Le Roux and Bach give the analysis formalized here: one step size $1/(16L)$ , an $O(n/k)$ rate for convex sums and a linear rate $(1-\min\{\mu/16L,1/8n\})^k$ for strongly convex sums, both in function values (arXiv:1309.2388; Math. Program. 162, 2017).
2013–2014: SVRG (Johnson and Zhang, 2013) and SAGA (Defazio, Bach and Lacoste-Julien, 2014) give variance-reduced methods with simpler, unbiased updates.

Setting

Let $f_1,\dots,f_n:\mathbb R^p\to\mathbb R$ , $n\ge1$ , and

g(x)=\frac1n\sum_{i=1}^n f_i(x).

Write $f'_i$ for the gradient of $f_i$ and $g'=\frac1n\sum_i f'_i$ . The standing assumptions are: each $f_i$ is convex and differentiable; each gradient is Lipschitz with constant $L>0$ , $\|f'_i(x)-f'_i(y)\|\le L\|x-y\|$ ; and some $x^*$ minimizes $g$ . Put $\sigma^2=\frac1n\sum_i\|f'_i(x^*)\|^2$ . The function $g$ is $\mu$ -strongly convex if $x\mapsto g(x)-\frac\mu2\|x\|^2$ is convex.

A state is $\theta=(y,x)$ : a table $y=(y_1,\dots,y_n)$ of vectors in $\mathbb R^p$ and an iterate $x\in\mathbb R^p$ . One SAG step with index $i$ and step size $\alpha$ replaces $y_i$ by $f'_i(x)$ and then sets

x\leftarrow x-\frac{\alpha}{n}\sum_{j=1}^n y_j

with the refreshed table. The indices $i_1,i_2,\dots$ are independent and uniform on $\{1,\dots,n\}$ ; $\theta^k=(y^k,x^k)$ is the state after $k$ steps, and $\bar x^k=\frac1k\sum_{i=0}^{k-1}x^i$ is the average iterate. Expectations are over the indices only; the data are fixed. The table starts either at $y^0_i=0$ or at the centered gradients $y^0_i=f'_i(x^0)-g'(x^0)$ .

Formalization targets

Goal: Theorem 1 (p. 7)

With $\alpha=\frac1{16L}$ and every $k\ge1$ ,

\mathbb E[g(\bar x^k)]-g(x^*)\le\frac{32n}{k}C_0,

and, if $g$ is $\mu$ -strongly convex with $\mu>0$ ,

\mathbb E[g(x^k)]-g(x^*)\le\Big(1-\min\Big\{\frac{\mu}{16L},\frac1{8n}\Big\}\Big)^kC_0,

where $C_0=g(x^0)-g(x^*)+\frac{4L}n\|x^0-x^*\|^2+\frac{\sigma^2}{16L}$ for $y^0=0$ and $C_0=\frac32[g(x^0)-g(x^*)]+\frac{4L}n\|x^0-x^*\|^2$ for the centered table. All four combinations are stated, with the paper's constants.

Milestones (Appendix B)

The proof of Appendix B builds a Lyapunov function

\mathcal L(\theta)=2h\,g(x+de^\top y)-2h\,g(x^*)+(\theta-\theta^*)^\top\begin{pmatrix}a_1ee^\top+a_2I&be\\ b e^\top&cI\end{pmatrix}(\theta-\theta^*),

with $e^\top y=\sum_iy_i$ and $\theta^*=(f'(x^*),x^*)$ , and fixes constants $a_1,a_2,b,c,d,h$ (App. B.5). The milestones follow it: the expectation identity of Lemma 1 and the inverse of Lemma 2; inequalities (12) and (13); the B.3 bound of $\mathbb E[\mathcal L(\theta^k)\mid\mathcal F_{k-1}]-(1-\delta)\mathcal L(\theta^{k-1})$ by a quadratic in $x^{k-1}-x^*$ and $g'(x^{k-1})$ ; the verification of Constraints 1–9 for the B.5 constants; the one-step decrease and the domination $g(x)-g(x^*)\le\mathcal L(\theta)$ (B.7); the linear, summed and averaged rates in terms of $\mathcal L(\theta^0)$ ; and the initial values of $\mathcal L$ for the two tables (B.8).

Significance

The result. Theorem 1 shows that one component gradient per iteration suffices for the convergence rates of the full gradient method on finite sums. In the strongly convex case the rate $(1-\min\{\mu/16L,1/8n\})^k$ is, for $n$ large relative to $L/\mu$ , better per pass through the data than the full gradient method's. The result started the line of variance-reduced methods (SVRG, SAGA, and their accelerated and proximal variants), which are now standard for empirical risk minimization. The convex-case rate holds without strong convexity and from either initialization.

Formalizing it. The rates are proved on paper, but the proof leans on a large symbolic computation: Table B.3 has dozens of terms, and the verification that the chosen constants satisfy the constraints (B.6) was done with computer algebra and an off-paper script for $n\in\{2,3,4\}$ . A machine-checked proof removes that dependency. The appendix also contains slips: a parametric step of B.4 that fails for $b<0$ , a wrong coefficient in B.8.2's intermediate identity, and a missing argument for $n=1$ . A formal proof settles which claims are right as stated. No formal proof of Theorem 1 is known to be recorded in a proof assistant library.

Difficulty

The method is not a stochastic gradient method in disguise: the step $\frac\alpha n\sum_jy_j$ is a biased estimate of $g'(x)$ , because the table holds stale gradients. The standard argument, a one-step contraction of $\|x^k-x^*\|^2$ in expectation, fails, since the bias depends on the whole table. The analysis must track the joint state $(y,x)\in\mathbb R^{np}\times\mathbb R^p$ through a Lyapunov function with several free parameters, find constants for which its expected decrease is negative uniformly in $n$ and $\mu/L$ , and show that it dominates $g(x)-g(x^*)$ . Each of these steps reduces to sign conditions on rational functions of $n$ and $\mu/L$ that hold for all $n\ge2$ , not just for a few values.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p), and the components are indexed by Fin n. The gradients are an explicit map f', tied to f by HasGradientAt at every point. $g$ and $g'$ are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The expectation over $k$ i.i.d. uniform indices is the uniform average over all $n^k$ index sequences (SAGA.Convex.expectIdx). A conditional expectation given $\mathcal F_{k-1}$ is the average over the next index from an arbitrary current state. The SAG step refreshes the table at the current iterate before the iterate moves. The average iterate includes $x^0$ and excludes $x^k$ .

The standing assumptions are exactly those of §3: $n\ge1$ , $L>0$ , each $f_i$ convex and differentiable with $L$ -Lipschitz gradient, and $x^*$ a minimizer of $g$ . Strong convexity is assumed only where the paper assumes it, in the shifted-convexity form of §3, with $\mu>0$ in Theorem 1 and $\mu\ge0$ in Appendix B. Hypotheses added to milestones, each one used by the paper without stating it, are $n\ge2$ wherever the B.5 constants appear (p. 43: "We will assume $n>1$ "), $\mu\le L$ in the constraint verification (B.6), and the sign conditions $h\ge0$ , $0\le\delta\le1$ , $B_3,B_4>0$ , $B_6^2/(4B_3)+B_8\ge0$ in the B.3 bound. The goal covers $n=1$ .

The goal is stated directly about expectIdx of $g$ along the SAG iterates from the two initial tables. It does not mention the Lyapunov function, its constants, or one-step averages, so it cannot be discharged by unfolding a definition. Junk values of Lean division are excluded by $n\ge1$ , $L>0$ and $k\ge1$ .

A complete development needs the expectation identity of Lemma 1 for block quadratic forms, smoothness and co-coercivity inequalities for convex functions with Lipschitz gradients, Jensen's inequality for finite uniform averages, and exact rational inequalities in $n$ and $\mu/L$ . The first two are reusable for other variance-reduced methods (SAGA, SVRG, IAG). Proofs of any milestone, of the $n=1$ case, and alternative proofs of the constraint verification are all welcome.

Selected references

M. Schmidt, N. Le Roux, F. Bach, Minimizing finite sums with the stochastic average gradient, Mathematical Programming 162 (2017), 83–112. arXiv:1309.2388v2. https://arxiv.org/abs/1309.2388
N. Le Roux, M. Schmidt, F. Bach, A stochastic gradient method with an exponential convergence rate for finite training sets, NeurIPS 2012. https://arxiv.org/abs/1202.6258
D. Blatt, A. O. Hero, H. Gauchman, A convergent incremental gradient method with a constant step size, SIAM Journal on Optimization 18(1) (2007), 29–51. https://doi.org/10.1137/040615961
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4) (2009), 1574–1609. https://doi.org/10.1137/070704277
R. Johnson, T. Zhang, Accelerating stochastic gradient descent using predictive variance reduction, NeurIPS 2013. https://papers.nips.cc/paper/4937-accelerating-stochastic-gradient-descent-using-predictive-variance-reduction
A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A fast incremental gradient method with support for non-strongly convex composite objectives, NeurIPS 2014. https://arxiv.org/abs/1407.0202

19 thms2 active usersReviewed

Complexity Theory Convex Optimization Optimization·Captain: mikedeng1

Tight Complexity Bounds for Optimizing Composite Objectives III: Any Deterministic Algorithm with Gradient and Prox Oracles Needs Ω(m√(γ/λ)·log(λε₀/(γε))) Queries on Smooth Strongly Convex SumsResearch Paper

Motivation

Many problems in machine learning and statistics minimize an average of component losses, $F(x)=\frac1m\sum_{i=1}^m f_i(x)$ : one term per training example, per data shard, or per block of a decomposed objective. Incremental methods such as SAG, SVRG, SAGA, SDCA and their accelerated variants touch one component at a time, so the natural measure of their work is the number of component queries. When every component is $\gamma$ -smooth and $\lambda$ -strongly convex, accelerated incremental methods reach accuracy $\epsilon$ after on the order of $(m+\sqrt{m\gamma/\lambda})\log(\epsilon_0/\epsilon)$ queries, while treating $F$ as one function and running accelerated gradient descent costs $m\sqrt{\gamma/\lambda}\log(\epsilon_0/\epsilon)$ component queries.

Woodworth and Srebro ask how far this can go when the oracle is as strong as possible: for a requested component it returns the value, the gradient, and an exact proximal point, the minimizer of $f_i(u)+\frac\beta2\|x-u\|^2$ . A proximal step solves a whole optimization problem for that component, so it is not obvious that oracle-complexity lower bounds for gradient methods survive. Their Theorem 4 shows that for deterministic algorithms they do: the full $m\sqrt{\gamma/\lambda}$ factor is unavoidable (Woodworth and Srebro, 2016, Theorem 4, p. 6). Randomization is what separates this from the upper bounds of accelerated incremental methods, which the paper treats separately.

Timeline. Nemirovski and Yudin (1983) and Nesterov (2004) gave the $\sqrt{\gamma/\lambda}\log(1/\epsilon)$ lower bound for one smooth strongly convex function under span-restricted methods. Agarwal and Bottou (2015) gave finite-sum lower bounds for deterministic methods with gradient access. Lan and Zhou (2018) proved bounds for randomized incremental gradient methods. Woodworth and Srebro (NeurIPS 2016; revised arXiv v3, 2019) handled arbitrary deterministic and randomized algorithms with a gradient-and-prox oracle and no span assumption.

Setting

Write $E_d=\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . A finite-sum objective is $F(x)=\frac1m\sum_{i=1}^m f_i(x)$ with $m\ge2$ components $f_i:E_d\to\mathbb R$ . A component is $\gamma$ -smooth if it is differentiable and its gradient is $\gamma$ -Lipschitz, and $\lambda$ -strongly convex if $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\lambda2\|x-y\|^2$ for all $x,y$ .

A query names a component $i$ , a point $x$ , and a parameter $\beta>0$ . The oracle $h_F$ answers with $f_i(x)$ , $\nabla f_i(x)$ , and $\mathrm{prox}_{f_i}(x,\beta)=\arg\min_u\{f_i(u)+\frac\beta2\|x-u\|^2\}$ . A deterministic algorithm chooses each query as a function of the answers it has received so far. The quantity bounded from below is the number of queries before some query point $\hat x$ satisfies $F(\hat x)-F(x^*)<\epsilon$ , where $x^*$ minimizes $F$ .

The proof works with directions $v_0,\dots,v_k$ , chosen orthonormal, and indicators $\delta_{i,r}\in\{0,1\}$ with $\sum_i\delta_{i,r}=\lfloor m/2\rfloor$ , and the components (at $\gamma=1$ )

f_i(x)=\frac{1-\lambda}{8}\Big(\delta_{i,1}(\langle x,v_0\rangle^2-2C\langle x,v_0\rangle)+\delta_{i,k}\zeta\langle x,v_k\rangle^2+\sum_{r=1}^k\delta_{i,r}\langle x,v_{r-1}-v_r\rangle^2\Big)+\frac\lambda2\|x\|^2 .

With $Q=\frac{\lfloor m/2\rfloor}{m}(\frac1\lambda-1)+1$ and $q=\frac{\sqrt Q-1}{\sqrt Q+1}$ these define the quantities in the milestones (App. B.4, pp. 16–17).

Formalization targets

Goal: Theorem 4 in $\Omega$ form

Let $R=m\sqrt{\gamma/\lambda}\,\log\frac{\lambda\epsilon_0}{\gamma\epsilon}$ . There are absolute constants $c,C>0$ such that for every $m\ge2$ , $\gamma,\lambda>0$ with $\gamma/\lambda>73$ , $\epsilon>0$ and $\epsilon_0>3\gamma\epsilon/\lambda$ there is a dimension $d\le CR$ with the following property. For every deterministic algorithm $A$ there are $\gamma$ -smooth, $\lambda$ -strongly convex $f_1,\dots,f_m$ on $\mathbb R^d$ and an exact oracle for them, with a minimizer $x^*$ of $F$ and $F(0)-F(x^*)=\epsilon_0$ , such that every query point $x_n$ with $n+1\le cR$ satisfies

F(x_n)-F(x^*)\ge\epsilon .

The constants are left unspecified, as in the paper's $O$ and $\Omega$ .

Milestones

At $\gamma=1$ , $\lambda<1/73$ , the proof establishes, in order: the closed form of $F$ with the factor $\lambda(Q-1)/8$ ; the minimizer $x^*=C\sum_{r=0}^kq^{r+1}v_r$ with $F(x^*)=-\frac{\lambda C^2}{8}(\sqrt Q-1)^2$ ; the ratio bound $\frac{F(x_t)-F(x^*)}{F(0)-F(x^*)}\ge\frac{q^{2t}-q^{2k+2}}{\sqrt Q}$ for points orthogonal to $v_t,\dots,v_k$ ; the exponential bound $\ge\frac1{2\sqrt Q}e^{-4t/(\sqrt Q-1)}$ once $k+1=\lceil t-\frac1{2\log q}\rceil$ ; the choice of $t$ that makes the ratio at least $\epsilon/\epsilon_0$ ; and the final count $\frac m2\lfloor\cdot\rfloor\ge\frac m{40\sqrt\lambda}\log\frac{\sqrt\lambda\epsilon_0}{2\epsilon}$ (pp. 17–18).

Significance

The theorem shows that an exact component prox does not buy a better dependence on the condition number $\gamma/\lambda$ for deterministic methods: the best deterministic method is, up to constants, accelerated gradient descent on $F$ itself. Combined with the paper's randomized lower bounds and known upper bounds, it pins down the gap between deterministic and randomized incremental methods at a factor of about $\sqrt m$ . It also tells designers of distributed and incremental solvers that a prox subroutine per component cannot replace randomization.

The result is proved on paper. To our knowledge it has no machine-checked proof. This mission formalizes the complete deterministic argument: the closed-form algebra of the quadratic construction, the geometric decay of its error along the chain, the counting of rounds, and, as the main work, the adversary that keeps the oracle's answers consistent with an algorithm that has not yet found the later directions. Each algebraic step is checked separately, so its constants are verified individually.

Difficulty

The argument from function values and gradients is standard for span-restricted methods. It does not cover this setting, for two reasons. First, the algorithm is arbitrary and deterministic: its query points need not lie in the span of earlier gradients, so the directions $v_r$ must be chosen adaptively, orthogonal to every query made so far. The hard instance therefore depends on the algorithm, and the oracle must be shown to answer every query consistently with one fixed set of components, chosen at the end. Second, the prox answer is the minimizer of a global problem. The proof must show that, while a component has not been queried in round $t$ , the prox of the truncated component coincides with the prox of the final one. The paper asserts this step for the strongly convex construction ("a fact which follows directly from the previous proof"). A solver has to carry it out for the extra $\frac\lambda2\|x\|^2$ term.

The algebraic steps are also delicate in their constants: the boundary equation at $v_k$ holds only with $\zeta=1-q$ , and the final count uses $\lambda<1/73$ and $\epsilon_0>3\epsilon/\lambda$ to keep the logarithm and the floor away from their degenerate values.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). Components are indexed by Fin m (from 0); $\lambda$ is written lam. A deterministic algorithm is a function from the list of previous responses to the next query, and an oracle is a fixed function from queries to responses (value, gradient, prox). Query n is the paper's $(n+1)$ -st. Prox points are a predicate (IsProx), not a choice function, and queries carry $\beta>0$ . Smoothness is a global gradient that is $\gamma$ -Lipschitz, and strong convexity is Mathlib's StrongConvexOn, which for differentiable functions is equivalent to the gradient inequality above. The minimum is an explicit minimizer, never a real infimum. $\lfloor m/2\rfloor$ is natural-number division.

Choices that strengthen or pin the page's statement, each disclosed in the items:

the domain is all of $\mathbb R^d$ , which is what the proof uses;
the dimension is chosen before the algorithm, which the proof supports;
the point $\hat x$ ranges over query points;
the oracle is exact and memoryless.

The goal mentions none of the proof's objects ( $v_r$ , $\delta$ , rounds, $Q$ , $q$ , $\zeta$ , $C$ , $k$ ), so it cannot be made trivial by fixing the construction. Its conclusion requires a genuine minimizer with $F(0)-F(x^*)=\epsilon_0$ , so the claim cannot hold for degenerate components.

Needed infrastructure: quadratic forms over orthonormal families, gradients and prox points of quadratics plus $\frac\lambda2\|x\|^2$ , and an adaptive Gram–Schmidt adversary. The model of algorithms and oracles is shared with the companion missions on Theorems 1 and 3 and can be reused for other oracle-complexity lower bounds. Proofs of individual milestones, of the consistency step, and of the scaling from $\gamma=1$ to general $\gamma$ are all welcome.

Selected references

B. Woodworth and N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives, NeurIPS 2016; arXiv:1605.08003v3, 2019. https://arxiv.org/abs/1605.08003
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
A. Agarwal and L. Bottou, A Lower Bound for the Optimization of Finite Sums, ICML 2015. https://arxiv.org/abs/1410.0723
G. Lan and Y. Zhou, An Optimal Randomized Incremental Gradient Method, Mathematical Programming, 2018. https://arxiv.org/abs/1507.02000

10 thms2 active usersReviewed

Complexity Theory Convex Optimization Optimization·Captain: mikedeng1

Tight Complexity Bounds for Optimizing Composite Objectives II: Any Deterministic Algorithm with Gradient and Prox Oracle Access Needs Ω(m√(γB²/ε)) Queries on Sums of m Convex γ-Smooth FunctionsResearch Paper

Motivation

Many problems in machine learning and statistics minimize an average of $m$ convex losses, one per data point or per block of data. Incremental methods such as SAG, SVRG, SAGA, SDCA, Finito and Katyusha exploit this finite-sum structure: each step touches one component $f_i$ instead of the whole average, and for smooth components the best of them reach accuracy $\epsilon$ with far fewer component evaluations than full-gradient methods. A natural question is how much of this improvement is possible at all, and whether access to stronger per-component information, such as a proximal step, could do better still.

B. Woodworth and N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives (NeurIPS 2016, arXiv:1605.08003), answer this with lower bounds on the number of component-oracle calls. Their oracle returns, for a requested component, its value, its gradient, and its exact proximal point. Earlier lower bounds covered only gradient access to smooth, strongly convex sums: Agarwal and Bottou (arXiv:1410.0723) for deterministic algorithms, and Lan (arXiv:1507.02000) for randomized algorithms that sample components from a fixed distribution and keep their iterates in the span of the gradients received (p. 2–3 of the paper). Woodworth and Srebro allow any algorithm, any sequence of gradient and prox queries, and iterates anywhere in $\mathbb R^d$ , in all four combinations of Lipschitz or smooth components and bounded or strongly convex objectives. This mission formalizes the deterministic bound for smooth, not strongly convex components on a bounded domain (Theorem 3 of the paper).

Setting

Fix integers $m\ge2$ and $d\ge0$ , and write $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . The domain is the ball $\mathcal X=\{x\in\mathbb R^d:\|x\|\le B\}$ . Given functions $f_1,\dots,f_m:\mathbb R^d\to\mathbb R$ , the objective is

F(x)=\frac1m\sum_{i=1}^m f_i(x).

A component $f_i$ is $\gamma$ -smooth on $\mathcal X$ if it is differentiable and its gradient is $\gamma$ -Lipschitz on $\mathcal X$ : $\|\nabla f_i(x)-\nabla f_i(y)\|\le\gamma\|x-y\|$ for $x,y\in\mathcal X$ . Each $f_i$ is also required to be convex on $\mathcal X$ .

A query is a triple $(i,x,\beta)$ of a component index, a point $x\in\mathbb R^d$ and a parameter $\beta>0$ . The oracle $h_F$ answers it exactly with

h_F(x,i,\beta)=\bigl[f_i(x),\ \nabla f_i(x),\ \operatorname{prox}_{f_i}(x,\beta)\bigr],\qquad \operatorname{prox}_{f_i}(x,\beta)\in\operatorname*{arg\,min}_{u\in\mathcal X}\Bigl\{f_i(u)+\frac\beta2\|x-u\|^2\Bigr\}.

A deterministic algorithm $A$ chooses its first query, and then each next query as a function of the ordered list of answers received so far. Running $A$ against an oracle produces a sequence of query points $x^{(0)},x^{(1)},\dots$ .

Formalization targets

Goal: Theorem 3

There are absolute constants $c,C>0$ such that for every $m\ge2$ and $\gamma,B,\epsilon>0$ there is a dimension $d\le C\,m\sqrt{\gamma B^2/\epsilon}$ with the following property. For every deterministic algorithm $A$ there are convex, $\gamma$ -smooth components $f_1,\dots,f_m$ on the $B$ -ball, an exact oracle for them, and a minimizer $x^*$ of $F$ over the ball, such that

F\bigl(x^{(n)}\bigr)-F(x^*)\ \ge\ \epsilon\qquad\text{for every } n \text{ with } n+1\le c\,m\sqrt{\gamma B^2/\epsilon}.

In words: $\Omega\bigl(m\sqrt{\gamma B^2/\epsilon}\bigr)$ oracle calls are needed before any queried point is strictly $\epsilon$ -suboptimal. The constants are left unspecified, as in the paper's $\Omega$ and $O$ .

Milestones

The proof (Appendix B.3) builds the components adaptively from orthonormal directions $v_0,\dots,v_k$ and indicators $\delta_{i,r}\in\{0,1\}$ . The milestones are the claims it states on the way:

the average of the hard components equals the truncated quadratic $F^{k+1}$ , and agrees with $F^q$ at points orthogonal to $v_q,\dots,v_k$ ;
the explicit minimizer $x_t^*=a\sum_{r=0}^{t-1}\bigl(1-\frac{r+1}{t+1}\bigr)v_r$ of $F^t$ and its value $-\frac{a^2\lfloor m/2\rfloor}{8m}\bigl(1-\frac1{t+1}\bigr)$ ;
$\|x_t^*\|^2\le a^2t/3$ ;
the gap $F(x)-F(x^*)\ge 1/(32k^2)$ for points not yet aware of the later half of the directions;
Lemma 4: the gradient of the partial function $f_i^t$ agrees with that of $f_i$ when $i$ is queried during round $t$ ;
Lemma 5: the same for the constrained prox;
the linear construction that forces $m$ queries when $\epsilon$ is large.

Significance

The result. Running accelerated gradient descent on $F$ , with all $m$ component gradients computed at each step, finds an $\epsilon$ -suboptimal point with $O\bigl(m\sqrt{\gamma B^2/\epsilon}\bigr)$ oracle calls (§2 and Table 1 of the paper). Theorem 3 shows that this is optimal among deterministic algorithms, up to a constant factor: neither incremental access to single components nor an exact prox oracle improves the order of the deterministic complexity. Randomized algorithms need only between $m+\sqrt{m\gamma B^2/\epsilon}$ and $m\log(\epsilon_0/\epsilon)+\sqrt{m\gamma B^2/\epsilon}$ calls (Table 1, with $\epsilon_0$ the suboptimality of the point $0$ ), so Theorem 3 also measures the benefit of randomization in incremental methods such as accelerated SVRG: a factor of order $\sqrt m$ in the dominant term.

Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formal proof needs the adaptive adversary argument in full: the construction of directions orthogonal to all earlier queries, the consistency of answers given by partial functions, and the explicit linear-algebra of the tridiagonal quadratic. The paper's final count $m/(16\sqrt{6\epsilon})$ is false for some parameters (for even $m$ and $\epsilon=1/500$ ), and the large- $\epsilon$ construction needs a dimension of order $m$ that the stated bound $d=O(m\sqrt{\gamma B^2/\epsilon})$ does not allow when $\epsilon\gg\gamma B^2$ ; a complete formal proof settles both points.

Difficulty

The algorithm is arbitrary and adaptive, and it sees exact prox points, which in principle reveal far more about a component than a gradient. The construction must therefore be chosen after the algorithm, round by round, so that every answer the algorithm has received is consistent with the final functions, yet reveals at most one new direction per round. The naive argument, "the algorithm only explores the span of previous gradients", is not available: the algorithm is not restricted to linear spans, and its queries can lie anywhere. Instead, each new direction must be made orthogonal to every point queried so far, and one must show that the partial function used to answer a query has the same gradient and the same constrained prox as the final function at that point (Lemmas 4–5). The constrained prox over the ball is not covered by the paper's unconstrained computation and needs its own argument.

Formalization scope

The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin m (0-based). A query is a structure carrying a component, a point and a parameter $\beta$ with a proof of $\beta>0$ ; the prox answer is described by the published minimizer predicate BoydADMM.Prox.IsProx, not by a choice function. A deterministic algorithm is a function from the list of earlier answers to the next query, and the oracle is a fixed function of the query, required to be exact on every query. The minimum $F(x^*)$ is an explicit attained minimizer over the ball, never a real infimum.

Committed conventions, each disclosed in the item statements:

the dimension $d$ is chosen before the algorithm (stronger than the page's order, and what the proof gives);
the point $\hat x$ ranges over query points, indexed from zero; an algorithm can query any point it wishes to output;
query points range over all of $\mathbb R^d$ , while convexity and smoothness are required on the ball;
$\beta>0$ in every prox query;
the milestones work at the proof's normalization $\gamma=B=1$ , use $\lfloor m/2\rfloor$ as natural-number division, and express " $x^v\in\operatorname{span}\{v_0,\dots,v_{t-1}\}$ " as $\langle x,v_r\rangle=0$ for $t\le r\le k$ .

A trivializing formalization is ruled out: the goal mentions none of $v_r$ , $\delta_{i,r}$ , rounds, $a$ , $k$ or $x_t^*$ , so it cannot be discharged by assumptions about the construction, and the oracle must answer every query exactly.

A full development needs: the adversary construction (orthonormal vectors orthogonal to a finite set of earlier queries), smoothness of the quadratic hard functions (a Hessian bound $\preceq I$ ), existence of constrained prox points, and the arithmetic of the counts. The tridiagonal linear algebra of milestones 2–3 is reusable for other lower-bound constructions in the style of Nesterov's. Proofs of individual milestones, alternative constructions and a corrected explicit constant are all welcome.

Selected references

B. Woodworth, N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives, NeurIPS 2016; arXiv:1605.08003v3, 2019. https://arxiv.org/abs/1605.08003
A. Agarwal, L. Bottou, A Lower Bound for the Optimization of Finite Sums, ICML 2015. https://arxiv.org/abs/1410.0723
G. Lan, Y. Zhou, An Optimal Randomized Incremental Gradient Method, Mathematical Programming 171, 2018. https://arxiv.org/abs/1507.02000
Z. Allen-Zhu, Katyusha: The First Direct Acceleration of Stochastic Gradient Methods, STOC 2017; JMLR 2018. https://arxiv.org/abs/1603.05953
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

12 thms2 active usersReviewed

Complexity Theory Convex Optimization Optimization·Captain: mikedeng1

Tight Complexity Bounds for Optimizing Composite Objectives I: Any Deterministic Algorithm with Gradient and Prox Oracle Access Needs Ω(mLB/ε) Queries on Sums of m Convex L-Lipschitz FunctionsResearch Paper

Motivation

Many optimization problems minimize the average of component losses: one loss per observation, machine, or term in an objective. When an algorithm can inspect one component at a time, the number of component queries is a useful measure of work. A component oracle can provide more than a value or subgradient: a proximal point summarizes a global minimization involving that component. Woodworth and Srebro ask whether this stronger access reduces the worst-case number of queries for nonsmooth finite sums. Their deterministic lower bound answers the question in the regime of convex Lipschitz components on a bounded Euclidean ball (Woodworth and Srebro, 2016, Theorem 1).

The paper studies deterministic and randomized algorithms separately. This mission concerns the deterministic claim in Section 4.1 and its Appendix B.1 proof. The result is relevant to algorithms that alternate among components and use both local subgradient information and component prox computations. The exact oracle matters: a lower bound for an approximate or restricted oracle would not settle the claim made for the stronger one in this paper (Woodworth and Srebro, 2016, pp. 1, 4–5).

Setting

Let $m\ge2$ and let $f_1,\ldots,f_m:\mathbb R^d\to\mathbb R$ be convex functions. Their finite-sum objective is $F(x)=m^{-1}\sum_{i=1}^m f_i(x)$ , minimized over the closed Euclidean ball $\mathcal X=\{x:\|x\|\le B\}$ for $B>0$ . Each component is $L$ -Lipschitz on $\mathcal X$ when $|f_i(x)-f_i(y)|\le L\|x-y\|$ for points $x,y$ in that ball. The paper's notation paragraph prints $f(x)-f(x)$ in this definition; the two-point condition is the intended reading (p. 3).

A query chooses a component index $i$ , a point $x\in\mathbb R^d$ , and $\beta>0$ . The component oracle returns the value $f_i(x)$ , a subgradient of $f_i$ at $x$ , and a point minimizing $f_i(u)+(\beta/2)\|x-u\|^2$ over $u\in\mathcal X$ . The subgradient is global: its defining inequality holds against every point in $\mathbb R^d$ . A deterministic algorithm chooses its next query from the ordered responses to its previous queries. The oracle is exact and makes a fixed response choice for each query. The paper allows algorithms without a span restriction and defines a round by how many distinct components have been queried, not by how many total queries have occurred (pp. 1, 4–5).

For the appendix milestones, $v_0,\ldots,v_k$ are orthonormal directions and $\delta_{i,r}\in\{0,1\}$ records whether component $i$ was missed in round $r$ . The hard components $f_i$ and their truncations $f_i^t$ are the explicit absolute-value sums in equations (6) and (7). These objects support the lower-bound analysis; they do not restrict the theorem's quantified algorithm or hard instance (pp. 5, 11–12).

Formalization targets

Deterministic oracle lower bound

There are absolute constants $c,C>0$ such that, for every $m\ge2$ , $L,B>0$ , and $0<\varepsilon<LB/12$ , some dimension $d\le C mLB/\varepsilon$ defeats every deterministic algorithm: for that algorithm there are convex $L$ -Lipschitz components and a valid oracle whose first $c mLB/\varepsilon$ query points all obey

F(x_n)-F(x^*)\ge\varepsilon,

where $x^*$ minimizes $F$ on $\mathcal X$ . This is the paper's $\Omega(mLB/\varepsilon)$ conclusion. The constants are absolute, and the dimension bound expresses its $O(mLB/\varepsilon)$ clause (Theorem 1, p. 5).

Supporting targets

Appendix B.1 supplies five milestones: the formula and attained minimum of the average hard function, its error gap for a point orthogonal to an unrevealed direction, the query-count inequality, and Lemmas 2 and 3 on subgradient and proximal-response consistency. The first three are quantitative claims for the normalized $L=B=1$ construction; the last two say that answers derived from a truncated component can remain valid for the final component (pp. 11–13).

Significance

The theorem puts a worst-case limit on deterministic methods that can ask for a component prox point as well as a subgradient. Its factor of $m$ says that access to individual components does not remove the cost of discovering information spread across the finite sum. The paper compares this lower bound with its deterministic upper bounds, making the query rate tight up to constants in this regime (Woodworth and Srebro, 2016, Table 1 and Theorem 1).

The mathematical result is proved in the paper; this mission asks for a machine-checked proof of its faithful formal statement. The model of exact component queries, deterministic response histories, and constrained proximal minimizers can also support related oracle-complexity developments. None of the new theorem items in this proposal has a machine-checked proof yet. The already published global subgradient definition is reused as a reference.

Difficulty

The theorem concerns every deterministic algorithm, including one whose future queries depend on all responses so far. A single hard function fixed without regard to that interaction does not capture the adversarial information limit established by the paper. The proof must also show that each answer exposed during the interaction is genuinely a value, subgradient, and constrained prox point for one completed family of component functions. Lemma 2 handles the subgradient requirement, while Lemma 3 handles the more global proximal requirement. The latter is delicate because equation (3) minimizes over the ball, whereas the appendix displays an unconstrained calculation (pp. 11–13).

The printed formula in equation (6) can have Lipschitz constant greater than one, contrary to a sentence on page 11. This affects an explicit constant in the proof, though the theorem's $\Omega$ rate survives rescaling. A verified development must establish a valid uniform Lipschitz bound and carry its normalization into the final constants (Appendix B.1, p. 11).

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d) with its Euclidean inner product and norm. Components use Fin m, a zero-based encoding of the paper's $1,\ldots,m$ . Query number zero is the first query; a bound on $(n+1)$ represents the number of queries made through query $n$ . The proximal operation is a predicate describing all minimizers over $\mathcal X$ ; each legal query has $\beta>0$ . The oracle is memoryless and exact for every query, even when its point lies outside $\mathcal X$ . Candidate points in the goal are the algorithm's query points. The dimension is chosen before the algorithm, as the appendix construction permits. The finite average is an explicit sum and $x^*$ is an explicit feasible minimizer, avoiding a default-valued real infimum.

The milestones use $k\ge1$ , orthonormal directions, binary indicators, and $\sum_i\delta_{i,r}=\lfloor m/2\rfloor$ where the average is involved. Their normalization is $L=B=1$ . Natural-number division represents $\lfloor m/2\rfloor$ , and a finite interval starting at one prevents the term $v_{r-1}$ from underflowing. The goal quantifies over every deterministic algorithm and demands a valid oracle and an attained minimum; the hard directions, indicators, rounds, and truncations occur only in supporting statements. This rules out a fixed easy instance or an oracle allowed to return arbitrary answers.

The development needs Mathlib's Euclidean-space, convexity, finite-sum, and orthonormal-family libraries and the published global-subgradient definition. Contributions that establish the five milestones, a uniform Lipschitz bound for the hard functions, or the algorithm-dependent construction are within scope. The other deterministic smooth regimes and the randomized results have separate problems and are outside this mission.

Selected references

B. Woodworth and N. Srebro, Tight Complexity Bounds for Optimizing Composite Objectives, NeurIPS, 2016; arXiv:1605.08003v3, 2019 revision. arXiv

8 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

On Nonconvex Optimization for Machine Learning: Gradients, Stochasticity, and Saddle Points 1: Perturbed SGD Makes Half Its Iterates ε-Second-Order Stationary within Õ(ℓΔ_f·𝔑/ε²) IterationsResearch Paper

Why saddle points matter for stochastic gradient methods

Most training objectives in machine learning are smooth and nonconvex, and they are minimized by stochastic gradient descent (SGD) and its variants. For nonconvex $f$ the classical guarantee is convergence to an $\epsilon$ -first-order stationary point, $\|\nabla f(x)\|\le\epsilon$ : Ghadimi and Lan (arXiv:1309.5549) showed that SGD reaches one in $\tilde O(\epsilon^{-4})$ stochastic gradient queries, independently of the dimension. A first-order stationary point may be a saddle point, however, and for many problems (matrix sensing and completion, phase retrieval, tensor decomposition, dictionary learning) every second-order stationary point is a global minimum. For these problems, a guarantee for second-order stationary points is a guarantee of global optimality.

Timeline:

2015. Ge, Huang, Jin and Yuan (arXiv:1503.02101) proved that noisy SGD escapes strict saddle points in polynomial time, with a large polynomial dependence on $d$ and $1/\epsilon$ .
2017. Jin, Ge, Netrapalli, Kakade and Jordan (arXiv:1703.00887) showed that gradient descent with occasional perturbations finds an $\epsilon$ -second-order stationary point in $\tilde O(\ell\Delta_f/\epsilon^2)$ iterations, only polylogarithmically worse than plain gradient descent for first-order points.
2019. The paper of this mission, Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811; J. ACM 68(2), 2021), extends this to the stochastic setting with norm-subGaussian gradient noise: perturbed SGD needs $\tilde O(\epsilon^{-4})$ queries when the stochastic gradients are Lipschitz and $\tilde O(d\epsilon^{-4})$ in general.

Setting

Let $f:\mathbb R^d\to\mathbb R$ be bounded below with $f^\star=\inf f$ , and write $\Delta_f=f(x_0)-f^\star$ . Assumption A: $f$ is $\ell$ -gradient Lipschitz, $\|\nabla f(x_1)-\nabla f(x_2)\|\le\ell\|x_1-x_2\|$ , and $\rho$ -Hessian Lipschitz, $\|\nabla^2 f(x_1)-\nabla^2 f(x_2)\|\le\rho\|x_1-x_2\|$ in operator norm. A point $x$ is an $\epsilon$ -second-order stationary point if

\|\nabla f(x)\|\le\epsilon\qquad\text{and}\qquad\lambda_{\min}(\nabla^2 f(x))\ge-\sqrt{\rho\epsilon}.

The algorithm sees only a stochastic gradient $g(x;\theta)$ with $\theta\sim\mathcal D$ . Assumption B asks that $\mathbb E\,g(x;\theta)=\nabla f(x)$ and that the error is norm-subGaussian: $\mathbb P(\|g(x;\theta)-\nabla f(x)\|\ge t)\le2e^{-t^2/(2\sigma^2)}$ for $t\ge0$ . The optional Assumption C asks that each $g(\cdot;\theta)$ is $\tilde\ell$ -Lipschitz. The two cases combine into

\mathfrak N=1+\min\Big\{\frac{\sigma^2}{\epsilon^2}+\frac{\tilde\ell^2}{\ell\sqrt{\rho\epsilon}},\ \frac{\sigma^2d}{\epsilon^2}\Big\},

with $\tilde\ell=+\infty$ when Assumption C is not used.

Perturbed SGD (PSGD, Algorithm 2) draws $\theta_t\sim\mathcal D$ and an independent Gaussian $\xi_t\sim\mathcal N(0,(r^2/d)I)$ at every step and updates

x_{t+1}=x_t-\eta\big(g(x_t;\theta_t)+\xi_t\big).

Formalization targets

Goal: Theorem 16

For a log factor $\iota$ , the proof uses the parameters of Eq. (8): $\eta=1/(\iota^9\ell\mathfrak N)$ , $r=\iota\epsilon\sqrt{\mathfrak N}$ , $\mathscr T=\lceil\iota/(\eta\sqrt{\rho\epsilon})\rceil$ , $\mathscr F=\iota^{-5}\sqrt{\epsilon^3/\rho}$ , and runs for $T=\lceil100\max\{\Delta_f\mathscr T/\mathscr F,\Delta_f/(\eta\epsilon^2)\}\rceil=\tilde O(\ell\Delta_f\mathfrak N/\epsilon^2)$ iterations. The goal states that there is an absolute constant $\mu_0$ such that, for $\iota\ge\mu_0(1+\log Q)$ with $Q=d\,\mathfrak N\max\{1,\ell\Delta_f/\epsilon^2\}(\ell/\sqrt{\rho\epsilon})/\delta$ ,

\mathbb P\Big(\#\{t<T:\ x_t\ \text{is an }\epsilon\text{-second-order stationary point}\}\ge T/2\Big)\ge1-\delta.

Milestones

The proof's two engines, in the paper's order: the concentration inequalities for norm-subGaussian martingale differences (Lemmas 36–39), the descent lemma (Lemma 23), improve-or-localize (Lemma 24), the coupling analysis around a saddle point (Lemmas 27–31), escape from a saddle point (Lemma 25), and the two claims that bound the number of iterates with large gradient and the number near saddle points.

Significance

The theorem shows that adding isotropic Gaussian noise to SGD suffices to find second-order stationary points at essentially the cost SGD pays for first-order points: $\tilde O(\epsilon^{-4})$ queries when Assumption C holds (matching Ghadimi–Lan up to logarithms) and $\tilde O(d\epsilon^{-4})$ in general. Combined with landscape results such as "every second-order stationary point is a global minimum", it yields global convergence of a simple first-order stochastic method from arbitrary initialization for the problems listed above.

The result is proved on paper. As far as is known, none of it is machine-checked: neither the escape-from-saddle-point argument by coupling sequences nor the vector-valued concentration inequalities of Appendix C, whose proofs the paper defers to a separate technical note (arXiv:1902.03736). Formalizing them yields reusable norm-subGaussian martingale bounds in $\mathbb R^d$ , a checked version of the coupling technique that later saddle-escape analyses reuse, and a check of every constant hidden in the paper's $\tilde O(\cdot)$ .

Difficulty

The descent lemma alone cannot rule out that the iterates stall near a strict saddle point, where the gradient is small and the negative curvature is invisible to first-order information. The obvious argument, which says that the perturbation has a component along the negative eigendirection and that component grows, fails as stated: the stochastic gradient noise, the Hessian's variation along the trajectory, and the perturbation all interact over $\mathscr T$ steps. Controlling these interactions needs concentration bounds for vector-valued martingales whose scale is itself random (Lemma 37), which have no counterpart in Mathlib. Bounding how often the iterates can return to saddle regions over the whole run is a separate difficulty, since the times at which the iterates are near a saddle point are random.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$ ; the Hessian is the derivative of the gradient map, and $\lambda_{\min}$ is the Rayleigh-quotient infimum over the unit sphere. The randomness is the infinite product measure of the pairs $(\theta_t,\xi_t)$ , and the PSGD run is a deterministic function of it. Conventions committed to:

Explicit constants in place of $\tilde O(\cdot)$ . The paper writes $\eta=\tilde\Theta(1/(\ell\mathfrak N))$ , $r=\tilde\Theta(\epsilon\sqrt{\mathfrak N})$ (Eq. (4)) and $\tilde O(\ell\Delta_f\mathfrak N/\epsilon^2)$ ; the statements use the proof's Eq. (8) and its $T$ , with $\mathscr T$ and $T$ rounded up to integers. Every "absolute constant $c$ " of a lemma is an existential quantified before the dimension, the oracle, the function and all parameters, so it cannot depend on them.
Calibration of $\iota$ . The printed $\iota=\mu\log(d\ell\Delta_f\mathfrak N/(\rho\epsilon\delta))$ is not invariant under rescaling $x\mapsto\lambda x$ and can be non-positive. The goal and the two claims assume $\iota\ge\mu_0(1+\log Q)$ with the scale-invariant $Q$ above.
Hypotheses made explicit. $\rho>0$ , $\epsilon>0$ , $0<\delta<1$ , $\sqrt{\rho\epsilon}\le\ell$ (the paper's footnote 1, p. 14), $\sigma>0$ , joint measurability of $g$ , and integrability of the stochastic gradients. Assumption B and Condition 35 hold for $t\ge0$ , since the printed " $\forall t\in\mathbb R$ " cannot be satisfied.
Corrections. Lemma 29 requires $\eta\gamma>0$ , Lemma 37 has failure probability $2d(\log(B/b)+1)e^{-\iota}$ , and Lemma 25 is stated at $t_0=0$ from a deterministic saddle point, the case the paper proves.

A formalization that keeps the printed " $\forall t\in\mathbb R$ " in Assumption B, or allows $\sigma=0$ in the tail bound, makes every statement vacuous or trivial; both are excluded. Infrastructure needed: norm-subGaussian vectors and their martingale concentration (reusable well beyond this mission), Gaussian anti-concentration in one direction, and stopping-time arguments for the Markov chain of PSGD. Contributions to any milestone, and to the concentration layer in particular, are welcome.

Selected references

C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, On Nonconvex Optimization for Machine Learning: Gradients, Stochasticity, and Saddle Points, arXiv:1902.04811v2, 2019; J. ACM 68(2), 2021. https://arxiv.org/abs/1902.04811
C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, A Short Note on Concentration Inequalities for Random Vectors with SubGaussian Norm, arXiv:1902.03736, 2019. https://arxiv.org/abs/1902.03736
C. Jin, R. Ge, P. Netrapalli, S. M. Kakade, M. I. Jordan, How to Escape Saddle Points Efficiently, ICML 2017. https://arxiv.org/abs/1703.00887
R. Ge, F. Huang, C. Jin, Y. Yuan, Escaping From Saddle Points — Online Stochastic Gradient for Tensor Decomposition, COLT 2015. https://arxiv.org/abs/1503.02101
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://arxiv.org/abs/1309.5549

17 thms2 active usersReviewed

Optimization Probability Statistics·Captain: mikedeng1

Robustness May Be at Odds with Accuracy 2: The Unit-Norm Soft-Margin SVM Is >99% Accurate but <1% Robust at ε ≥ 2η, While Adversarial Training Gives Accuracy pResearch Paper

Motivation

Adversarial training asks a classifier to work even after an input has been changed within a prescribed perturbation budget. Tsipras, Santurkar, Engstrom, Turner, and Mądry studied why the classifier that performs best on ordinary inputs can behave very differently under these changes. Their explicit model separates one reliably predictive feature from many individually weak features. It lets the same distribution support a highly accurate ordinary classifier and a less accurate but robust classifier Tsipras et al., §2.1–2.2. This mission formalizes the paper's comparison for soft-margin support vector machines at the population level.

The model is relevant to anyone using a training objective as a proxy for performance under perturbations. Its conclusion concerns the optimizer of an expected loss, not the effect of a particular finite sample or optimization algorithm. That distinction makes the example a direct statement about the objectives being optimized.

Setting

A label $y$ is drawn uniformly from $\{-1,+1\}$ . An input $x$ has $d+1$ real coordinates. Its first coordinate, $x_1$ , equals $y$ with probability $p$ and $-y$ with probability $1-p$ , where $p\ge1/2$ . Conditional on $y$ , each of the remaining coordinates is an independent Gaussian variable with mean $\eta y$ and variance one, independently of $x_1$ . Thus $x_1$ is a moderately reliable feature while the other coordinates can be weak predictors individually. These are exactly the ingredients of distribution $D$ in equation (3) Tsipras et al., p. 4.

For a weight vector $w$ , the linear classifier $f_w$ assigns the sign of $w^\top x$ . Its standard accuracy is the probability that $f_w(x)=y$ for a fresh pair $(x,y)$ from $D$ . Its robust accuracy at radius $\varepsilon$ is the probability that this equality holds for every perturbation $\delta$ with $\|\delta\|_\infty\le\varepsilon$ . Both accuracies average the two labels with probability $1/2$ each.

The soft-margin SVM objective combines expected hinge loss and quadratic regularization:

J_\lambda(w)=\mathbb E_D\!\left[\max\{0,1-yw^\top x\}\right] +\frac{\lambda}{2}\|w\|_2^2.

The distributional adversarial objective replaces the hinge loss for each observed pair by its maximum over the $\ell_\infty$ ball before taking the expectation:

J^{\mathrm{adv}}_{\varepsilon,\lambda}(w)= \mathbb E_D\!\left[ \max_{\|\delta\|_\infty\le\varepsilon} \max\{0,1-yw^\top(x+\delta)\}\right] +\frac{\lambda}{2}\|w\|_2^2.

This order follows equation (2), the distributional adversarial loss Tsipras et al., pp. 2, 16–18.

Formalization targets

The goal is Theorem 2.2 Tsipras et al., p. 6. Under $d\ge1$ , $1/2\le p\le0.975$ , and $\eta\ge4/\sqrt d$ , a global minimizer $w^*$ of $J_\lambda$ whose squared Euclidean norm is one satisfies

\operatorname{StdAcc}(f_{w^*})>0.99, \qquad \operatorname{RobAcc}_{\varepsilon}(f_{w^*})<0.01 \quad\text{for every }\varepsilon\ge2\eta.

For a global minimizer of $J^{\mathrm{adv}}_{\varepsilon_{\mathrm{tr}},\lambda}$ with $\varepsilon_{\mathrm{tr}}\ge2\eta$ and either $\varepsilon_{\mathrm{tr}}<2p-1$ or $p=1/2$ , the target is

\operatorname{StdAcc}(f_{w^*}) =\operatorname{RobAcc}_{\varepsilon}(f_{w^*})=p \quad\text{for every }0\le\varepsilon<1.

The milestone list follows Appendix D's stated claims: the Gaussian law of the pooled weak feature, Lemmas D.1–D.5, and the displayed adversarial objective identity. The lemmas give nonstrict $99\%$ and $1\%$ bounds where the theorem states strict inequalities Tsipras et al., pp. 16–18.

Significance

The result gives a concrete distribution on which the ordinary population hinge objective favors weak features enough to achieve near-perfect standard accuracy while remaining vulnerable to a small coordinatewise perturbation. The adversarial objective instead selects a classifier using the first feature, whose standard and robust accuracies are both $p$ . It therefore distinguishes the behavior of the two objectives even without sampling error or a particular training algorithm.

The paper proves these claims informally. The Lean items here compile as definitions and theorem statements with open proofs; they are not yet machine-checked proofs. A completed development would supply the Gaussian probability estimates, optimizer properties, and accuracy calculations needed to close the statements. The law of a pooled Gaussian vector and the relation between $\ell_\infty$ perturbations and the $\ell_1$ weight norm are reusable beyond this example.

Difficulty

The first weak feature alone carries little information, but their normalized sum has a strong Gaussian signal. Consequently, reasoning about one coordinate at a time does not determine what the ordinary SVM minimizer predicts. The theorem also concerns every global minimizer with the stipulated norm, so testing a convenient weight vector does not settle it. The stated strict accuracy constants require quantitative Gaussian tails and an optimizer comparison at the specified $p$ and $\eta$ thresholds. In the adversarial part, the conclusion about accuracy $p$ requires more than proving that weak-feature weights vanish: the remaining first-feature coefficient must have the correct sign and be nonzero.

Formalization scope

Lean represents an input as a function on Fin (d+1); index zero is the paper's $x_1$ , and index i.succ is $x_{i+2}$ . The function norm is the sup norm, so $\|\delta\|\le\varepsilon$ is exactly the $\ell_\infty$ ball. Squared $\ell_2$ norm and $\ell_1$ norm of a weight vector are written as $\sum_iw_i^2$ and $\sum_i|w_i|$ . The conditional law is a product of the two-point first-feature law and the independent Gaussian weak-feature law, assembled into one input vector. GaussianReal's variance argument is one. Labels and predictions are real $\pm1$ , and a zero score is assigned $-1$ . The tie has probability zero for the nondegenerate classifiers in the theorem.

The robust event can be outside the Borel sigma algebra. Its measure in Lean is an outer measure, agreeing with probability under completion. Gaussian affine hinge functions are integrable; the adversarial hinge has the explicit finite closed form supplied by a milestone when the radius is nonnegative. The supremum is over exactly the admissible perturbations. The mission does not reduce the target to a chosen classifier or assume any of the milestone conclusions as goal hypotheses.

Several hypotheses make implicit conditions or a necessary correction explicit. The condition $d\ge1$ prevents $4/\sqrt d$ from becoming Lean's default value at zero. Appendix D assumes that $\lambda>0$ has been tuned so an ordinary global minimizer has $\|w^*\|_2=1$ ; that is represented directly. Evaluation radii are nonnegative, so their balls are not empty. The upper bound $\varepsilon_{\mathrm{tr}}<2p-1$ is needed for the second claim: for larger training radii the zero vector may minimize the adversarial objective and its constant classifier has accuracy $1/2$ , contrary to the printed sentence when $p>1/2$ . At $p=1/2$ that constant classifier has accuracy $1/2=p$ , so the case $p=1/2$ is kept for every training radius. This correction is disclosed rather than silently attributing it to the paper. Appendix D's displayed maximum outside expectation also differs from equation (2); the formalization follows (2), whose per-sample maximum has the displayed closed form. The paper's proof specializes to $\eta=4/\sqrt d$ although Theorem 2.2 states $\eta\ge4/\sqrt d$ ; the target retains the printed theorem's range.

Selected references

Dimitris Tsipras, Shibani Santurkar, Logan Engstrom, Alexander Turner, and Aleksander Mądry, Robustness May Be at Odds with Accuracy, International Conference on Learning Representations, 2019. arXiv:1805.12152v5.

10 thms2 active usersReviewed

Linear Optimization Statistics·Captain: mikedeng1

Fast Rates for Contextual Linear Optimization 2: Any Algorithm Choosing from a Policy Class of Natarajan Dimension η Has Regret ≥ (ρ(Z)/2e⁴)((η−1)/n)^((1+α)/(2+α)) on Some Margin-α InstanceResearch Paper

Motivation

In contextual linear optimization (CLO) a decision maker observes a covariate $X$ (features of a day, a customer, a network state) and then chooses a decision $z$ from a polytope $\mathcal Z$ to minimise an uncertain linear cost $Y^\top z$ . Shortest-path routing with predicted travel times and inventory or portfolio decisions driven by forecasts are standard instances. Since $Y$ is unknown at decision time, the relevant cost is $f^*(X)^\top z$ with $f^*(x) = \mathbb E[Y \mid X = x]$ , and a policy is learned from $n$ past observations $(X_i, Y_i)$ .

Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare two families of methods: estimate-then-optimize (fit $f^*$ , then optimise) and induced empirical risk minimisation (search a policy class directly for low empirical cost). Their main finding is that under a noise condition that controls how often two vertices of $\mathcal Z$ are nearly tied, the regret decays faster than the usual $n^{-1/2}$ . For ERM over a policy class of Natarajan dimension $\eta$ they prove the rate $(\eta/n)^{(1+\alpha)/(2+\alpha)}$ up to logarithms (their Theorem 6). This mission formalizes the matching lower bound, their Theorem 7: no algorithm that only knows the true optimal policy lies in the class can do better.

Setting

A polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$ is nonempty with $\sup_{z \in \mathcal Z}\|z\| \le B$ , $B > 0$ . Its set of extreme points is $\mathcal Z^\angle$ . An instance is a law $\mathbb P_X$ of $X \in \mathbb R^p$ together with a conditional law of $Y \in \mathbb R^d$ given $X = x$ , with $\|Y\| \le 1$ ; $f^*(x)$ is the conditional mean. The optimal set is $\mathcal Z^*(x) = \arg\min_{z\in\mathcal Z} f^*(x)^\top z$ and the gap is

\Delta(x) = \inf_{z \in \mathcal Z^\angle \setminus \mathcal Z^*(x)} f^*(x)^\top z - \min_{z \in \mathcal Z} f^*(x)^\top z

when $\mathcal Z^*(x) \ne \mathcal Z$ , and $\Delta(x) = 0$ otherwise. The noise condition (Assumption 2) with parameters $\alpha, \gamma \ge 0$ is

\mathbb P_X\big(0 < \Delta(X) \le \delta\big) \le (\gamma\delta/B)^\alpha \qquad \forall \delta > 0.

A policy is a map $\pi : \mathbb R^p \to \mathcal Z^\angle$ . A class $\Pi$ of policies Natarajan-shatters $\eta$ points if there are $x_1, \dots, x_\eta$ and values $s_i \ne s_i'$ such that every pattern in $\{0,1\}^\eta$ is realised by some $\pi \in \Pi$ choosing $s_i$ or $s_i'$ at $x_i$ ; the Natarajan dimension is the largest such $\eta$ . An algorithm maps a sample $\mathcal D$ of $n$ i.i.d. draws of $(X, Y)$ to a policy $\hat\pi_{\mathcal D} \in \Pi$ , and its regret is

\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\,\mathbb E_X\Big[f^*(X)^\top \hat\pi_{\mathcal D}(X) - \min_{z\in\mathcal Z} f^*(X)^\top z\Big].

The scale of the bound is the vertex separation

\rho(\mathcal Z) = \inf_{z \in \mathcal Z^\angle,\ z' \in \mathrm{conv}(\mathcal Z^\angle \setminus \{z\})} \|z - z'\|.

Formalization targets

Goal: Theorem 7

Fix $\alpha \ge 0$ , a polytope $\mathcal Z$ , a class $\Pi$ of Natarajan dimension at least $\eta \ge 1$ , and $n \ge 2^{2+\alpha}(\eta - 1)$ . For every algorithm $\mathcal D \mapsto \hat\pi_{\mathcal D} \in \Pi$ there is an instance with $\|Y\| \le 1$ on which some $\pi^* \in \Pi$ is optimal at every $x$ , the noise condition holds with the given $\alpha$ and $\gamma = B/\rho(\mathcal Z)$ , and

\mathrm{Regret}(\hat\pi) \;\ge\; \frac{\rho(\mathcal Z)}{2e^4}\Big(\frac{\eta - 1}{n}\Big)^{\frac{1+\alpha}{2+\alpha}}.

Milestones

$\rho(\mathcal Z) > 0$ when $\mathcal Z$ has two extreme points (Theorem 3, p. 7).
Eq. (25): the vertex-separating directions $w(z)$ have norm at most one and separate $z$ from the other vertices by exactly $\rho(\mathcal Z)$ .
Eq. (14): the error of any estimate of a hidden bit is at least the minimum Bayes risk.
The posterior identity of p. 21.
The Jensen step of p. 21.
The binomial bound $\mathbb E|N^1 - N^0| \le \sqrt{nq}$ of pp. 21–22.
The exponential bound in Eq. (15).
The closing calculation of the proof of Theorem 7 (p. 30).

Significance

Theorem 7 shows that the fast rate of Theorem 6 is optimal in both $n$ and $\eta$ , up to logarithmic factors, among methods that exploit only the well-specification of the policy class. The paper uses this to explain why estimate-then-optimize, which also exploits the structure of the regression class, can beat ERM: it is not subject to this lower bound. At $\alpha = 0$ the bound recovers the order of the paper's slow-rate lower bound (Theorem 3), and as $\alpha \to \infty$ it approaches $\eta/n$ .

The result is proved in the paper; no machine-checked proof of it or of its milestones is known. Formalizing it produces a checked minimax lower bound for a decision problem over an arbitrary polytope, together with a reusable toolkit for Assouad-type arguments over hypercubes of hard instances: the binary Bayes-risk bound, the closed-form posterior for a biased coin, the Jensen step, and the binomial mean absolute deviation bound.

Difficulty

The statement quantifies over every algorithm, including non-measurable and randomisation-free ones, so the argument cannot analyse a specific estimator. The standard route averages the regret over a family of $2^{\eta-1}$ instances and reduces it to hidden-bit estimation, but two features of CLO make the construction delicate. First, the instances must keep $\|Y\| \le 1$ while giving each shattered point a prescribed gap between its optimal vertex and every other vertex of an arbitrary polytope; this is where $\rho(\mathcal Z)$ and the directions of Eq. (25) enter. Second, each instance must satisfy the noise condition with the given $\alpha$ and $\gamma = B/\rho(\mathcal Z)$ , which fixes how much probability mass the near-tied points may carry; the mass cannot simply be spread uniformly as in the slow-rate argument. The constants have to be tracked exactly, since the goal states the explicit constant $1/(2e^4)$ .

Formalization scope

Everything lives in the namespace FastCLO.LowerBound. Vectors are EuclideanSpace ℝ (Fin k). A polytope bundles its constraint rows, right-hand sides, a radius $B > 0$ , nonemptiness and boundedness. An instance is a probability measure $\mu$ on $\mathbb R^p$ and a Markov kernel $\kappa$ with $\kappa(x)(\{\|y\| > 1\}) = 0$ ; $f^*$ is the kernel mean, and the sample law is the $n$ -fold product of $\mu \otimes \kappa$ . Every joint law disintegrates this way. The regret is measured against the optimal value $\min_{z\in\mathcal Z} f^*(x)^\top z$ , which equals the paper's comparison with $\pi^*$ . Natarajan dimension "at least $\eta$ " is the existence of a shattered $\eta$ -tuple. Infima are real infima over sets that are nonempty and bounded under the hypotheses. Probabilities in the noise condition are in $[0,\infty]$ , and $(\gamma\delta/B)^\alpha$ is a real power.

The paper prints Theorem 7 with the distribution chosen before $n$ ; its proof builds the distribution from $n$ , and the formal goal is stated in the proved order: for every $n$ and every algorithm there is an instance. The hypothesis $\eta \ge 1$ excludes the empty case. No measurability is assumed of the algorithm. The algorithm must return a member of $\Pi$ for every sample, and the instance must satisfy $\|Y\| \le 1$ , the optimality of some member of $\Pi$ everywhere, and the noise condition. Dropping any of these would make the bound trivial or false, and none of them is relaxed.

A complete development needs finiteness of the extreme points of a polytope, projections onto convex hulls, products of finitely supported measures, and elementary binomial identities. The generic milestones (3–7) are reusable for other hypercube lower bounds. Proofs of individual milestones are welcome independently of the goal.

The companion missions Fast Rates for Contextual Linear Optimization 1 (the ERM upper bound, Theorem 6) and 3 (the estimate-then-optimize bound, Theorem 8) use the same model.

Selected references

Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, arXiv:2011.03030v3, 2021; Management Science 68(6), 2022. https://arxiv.org/abs/2011.03030
L. Devroye, G. Lugosi, Lower bounds in pattern recognition and learning, Pattern Recognition 28(7), 1995. https://doi.org/10.1016/0031-3203(95)00002-Z
A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804
O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization bounds in the predict-then-optimize framework, NeurIPS 2019. https://arxiv.org/abs/1905.11488

12 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Modern Introduction to Online Learning XII: Coordinate-Wise Krichevsky–Trofimov Betting Has Parameter-Free Regret ‖u‖₁L∞√(2T ln(1 + e‖u‖∞T/ε)) + dεL∞Textbook

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.

7 thms2 active usersReviewed

Missions

Optimal No-regret Learning in Repeated First-price Auctions 3: Even with Full Information and v_t ≡ 1, Every Bidding Policy Has Worst-Case Expected Regret at Least c√TResearch Paper

Learning to bid in first-price auctions

Setting

Formalization targets

Goal: Theorem 9 (p. 36)

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

Significance

Difficulty

Formalization scope

Selected references

Optimal No-regret Learning in Repeated First-price Auctions 5: With Adversarial Contexts and K = (α+1)M ≤ T^(1/3), Every Policy for Partially Ordered Contextual Bandits Has Regret ≥ √(KT)/(32e³)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 in the regime of its proof

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal No-regret Learning in Repeated First-price Auctions 6: If the HOB Law Switches at an Unknown Value Threshold, Every Bidding Policy Has Regret Ω(T)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 34)

Milestones (p. 34)

Significance

Difficulty

Formalization scope

Selected references

Optimal No-regret Learning in Repeated First-price Auctions 4: Arm Elimination with Graph Feedback and Cross Learning Has Regret Õ(T ∧ √(αMT) ∧ √(KT)) with High ProbabilityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Structural Estimation of Markov Decision Processes in High-Dimensional State Space with Finite-Time Guarantees: Single-Loop ML-IRL Policy and Reward Iterates Converge at Explicit Finite-Time RatesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1, explicit form

Milestones

Significance

Difficulty

Formalization scope

Selected references

Thompson Sampling with Information Relaxation Penalties III: As T → ∞ the Action Laws of IRS.FH and IRS.V-Zero Converge to That of Thompson SamplingResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1 (p. 25)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Learning and Optimization with Seasonal Patterns 1: Regret Upper Bound for the Two-Stage Period-Estimation and Confidence-Bound PolicyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Stage one: correct period identification

Stage two: the oracle's regret

Significance

Difficulty

Formalization scope

Selected references

Thompson Sampling with Information Relaxation Penalties I: For Natural Exponential Families the Suboptimality Gaps of TS, IRS.FH and IRS.V-Zero Are at Most 2√L[1/√ν + √(2 log T)(K/√ν + 2√(KT))]Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance