Machine Learning

Bandit Algorithms Information Theory Operations Research·Captain: mikedeng1

Phase Transitions in Bandits with Switching Constraints: every policy with at most S switches has regret at least the phase-dependent rate up to a logarithmic factorResearch Paper

Motivation

In many sequential decision problems, changing the action is costly or administratively limited: a retailer can revise a posted price only a few times per season, a clinical trial can change its treatment allocation only a few times, and a firm can reconfigure its production line only so often. The multi-armed bandit with switching constraints (BwSC) captures this tension between learning and limited adaptivity: the learner must explore to find a good action, but every change of action consumes a hard budget. Simchi-Levi and Xu (arXiv:1905.10825, Management Science 2023) determine the optimal regret of this problem up to logarithmic factors.

Timeline. Classical bandit theory gives the minimax regret $\Theta(\sqrt{KT})$ for $K$ arms and horizon $T$ with unlimited switching (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020). Cesa-Bianchi, Dekel and Shamir (2013) showed that in adversarial bandits with switching costs the regret is $\widetilde\Theta(T^{2/3})$ . For stochastic bandits processed in a fixed number of batches, Perchet, Rigollet, Chassang and Snowberg (2016) and Gao, Han, Ren and Zhou (2019) obtained regret rates of the form $T^{1/(2-2^{1-M})}$ for $M$ batches. Simchi-Levi and Xu (2019, revised 2021) treat a hard budget $S$ on the number of switches and prove matching upper and lower bounds; the lower bound, Theorem 2, is the subject of this mission.

Setting

There are $K>1$ arms and $T$ rounds. In round $t$ the learner picks $a_t\in[K]$ and observes a reward $X_t\sim\mathcal N(\mu_{a_t},1)$ from the unit-variance Gaussian environment with mean vector $\mu\in\mathbb R^K$ ; admissible environments have mean spread $|\mu_i-\mu_j|\le1$ . A policy $\pi$ chooses $a_{t+1}$ by a Markov kernel from the past actions and rewards; $\mathbb P^\pi_\mu$ is the law of the history. The regret is

R^\pi_\mu(T)=T\max_i\mu_i-\mathbb E^\pi_\mu\Big[\sum_{t=1}^T X_t\Big].

With unit switching costs, the number of switches is $\sum_{t=1}^{T-1}\mathbb 1\{a_t\neq a_{t+1}\}$ . For a budget $S\in\mathbb N$ , the class $\Pi_S$ of $S$ -switch policies consists of the policies whose number of switches is at most $S$ almost surely under every environment.

The budget enters through the phase index $q(S,K)=\lfloor (S-1)/(K-1)\rfloor$ (with $q(0,K)=0$ ) and the remainder $r(S,K)=S-1-q(S,K)(K-1)$ (so $r(0,K)=-1$ ). Two rates appear, with $a(q)=1/(2-2^{-q})$ :

A=\frac{(K-r(S,K))^{2-a(q(S,K))}}{K}\,T^{a(q(S,K))},\qquad B=K^{1-a(q(S,K)+1)}\,T^{a(q(S,K)+1)}.

In Lean these are IsSwitchPolicy S T π, qIdx S K, rIdx S K, rateA K S T, rateB K S T, on top of the published BanditPolicy, banditMeasure, banditRegret and gaussianBandit.

Formalization targets

Goal: Theorem 2 (p. 21)

There is an absolute constant $C>0$ such that for all $K>1$ , $S\in\mathbb N$ , $T\ge2K$ and every $\pi\in\Pi_S$ , some admissible Gaussian environment $\mu$ satisfies

R^\pi_\mu(T)\ \ge\ \frac{C}{\log T}\max\{A,\ B\}.

The constant is not fixed: the goal asserts the shape of the bound, which survives any improvement of constants.

Milestones

The proof in Appendix J (pp. 59–75) reduces to the regime $q(S,K)+2\le\log_2\log_2(T/K)$ (p. 59, two bounds by $O(\sqrt{KT})$ outside it) and then runs a five-step program on two families of environments:

the localized Pinsker inequality (Lemma 5) and the generalized reverse Fano inequality (Proposition 5, (35));
counting bounds on risky events under a single environment (Lemmas 6–7, Corollary 4);
bad-event regret bounds under alternative environments and the reduction to bad-event probabilities (Lemmas 8–11);
divergence bounds for restricted measures (property 1 of p. 72, Lemmas 12–13);
the final probability bounds (46)–(47).

Significance

The result. Theorem 2, together with the AdaLS upper bound (Theorem 1), shows that the optimal regret is $\widetilde\Theta(\max\{A,B\})$ for every $K$ , $S$ and $T$ . In particular, for fixed $K$ the regret as a function of $T$ is $\widetilde\Theta(T^{1/(2-2^{-q(S,K)})})$ : it changes only when $S$ crosses a multiple of $K-1$ , a phase transition in the switching budget, and $\Theta(\log\log T)$ switches suffice for the classical $\sqrt T$ rate. The lower bound holds for all randomized adaptive policies, not only batched ones.

Formalizing it. The result is proved on paper but has no machine-checked proof. Formalizing the lower bound adds a reusable change-of-measure toolkit for adaptively collected data: a reverse Fano-type inequality over families of measure spaces, stopping-time-based counting arguments on switching patterns, and divergence bounds for censored histories. Three printed steps needed repair (see Formalization scope), so the formal development also certifies a corrected version of the argument.

Difficulty

The obvious argument fails at the counting step. A naive choice of risky events (arms unobserved in fixed time windows) only gives a sum of probabilities of at least $K-1-\lfloor S/(q+1)\rfloor$ , which vanishes when $S$ is at the end of a phase; this loses the floor $\lfloor (S-1)/(K-1)\rfloor$ in the exponent. The paper's events in the last window are defined through the stopping time at which the switching budget is exhausted, and they interact with the measure-change step: the restricted measures must hide enough information about the tested arm to make divergences small, while still deciding the stopping-time event. A second difficulty is that the policy is adaptive and randomized, so all events and measures are path-dependent.

Formalization scope

Model. Histories are the published canonical bandit histories Fin T → Fin K × ℝ; rounds are 1-based in every statement (entry $s$ is round $s+1$ ). Environments are unit-variance Gaussian (gaussianBandit), which is all the proof uses (p. 59).
Admissible policies. IsSwitchPolicy S T π asks the budget to hold almost surely under every unit-variance Gaussian environment, a weaker requirement than the paper's "for all sub-Gaussian $\mathcal D$ ", so the goal covers at least the paper's policy class. The regret lower bound is witnessed by one Gaussian instance with mean spread at most $1$ , which implies the paper's bound on the supremum.
Conventions. $S\in\mathbb N$ and unit costs (§3, p. 14); $q(0,K)=0$ and $r(0,K)=-1$ by the paper's convention $\lfloor x\rfloor=0$ for $x<0$ ; $\tau=\infty$ is encoded as $T+1$ ; divergences are Mathlib's klDiv in $[0,\infty]$ , and the reverse KL is $D_{\rm re}(\mathbb P\|\mathbb Q)=\mathrm{KL}(\mathbb Q\|\mathbb P)$ ; conditional expectations in Lemmas 8 and 10 are stated in product form.
Repairs. (i) Lemma 8's integrand is the regret $T\mu^*-\sum_t\mu_{a_t}$ ; the printed integrand is non-positive for $j=q+2$ . (ii) The artificial measures (45) are replaced by records stopped at the first pull of the tested arm in the window; the printed measures do not have the claimed divergence. (iii) The p. 59 bound $\sqrt{2KT}$ is corrected to $2\sqrt{KT}$ , and the companion bound for the first term, which the page omits, is a separate milestone. The first-class lemmas assume $q(S,K)\ge1$ , where the page's construction is defined; the goal does not.
Ruled out. A constant $C$ depending on $K$ , $S$ or $T$ ; dropping the mean-spread condition; restricting to deterministic or batched policies; a switching constraint only in expectation; or stating the theorem for one fixed $(K,S)$ — each makes the statement trivial or different, and none is used.
Infrastructure. Reused: the published canonical bandit model, the Bernoulli divergence ExploreFirst.FundIneq.klBer, the first half of Lemma 5 (ExploreFirst.Collective.lemma_6) and the classical bound BanditAlgorithm.bandit_minimax_lower_bound. Needed and reusable beyond this mission: the divergence decomposition for stopped histories, joint convexity and data processing for KL across different spaces, and the KL divergence of unit-variance Gaussians. Proofs of any milestone, and of the Gaussian-instance reduction, are welcome.

Selected references

D. Simchi-Levi and Y. Xu, Phase Transitions in Bandits with Switching Constraints, Management Science, 2023; arXiv:1905.10825v4. https://arxiv.org/abs/1905.10825
T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
N. Cesa-Bianchi, O. Dekel and O. Shamir, Online Learning with Switching Costs and Other Adaptive Adversaries, NeurIPS 2013. https://arxiv.org/abs/1302.4387
V. Perchet, P. Rigollet, S. Chassang and E. Snowberg, Batched Bandit Problems, Annals of Statistics, 2016. https://arxiv.org/abs/1505.00369
Z. Gao, Y. Han, Z. Ren and Z. Zhou, Batched Multi-armed Bandits Problem, NeurIPS 2019. https://arxiv.org/abs/1904.01763
S. Gerchinovitz, P. Ménard and G. Stoltz, Fano's Inequality for Random Variables, Statistical Science, 2020. https://arxiv.org/abs/1702.05985

26 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Efficient Online Linear Optimization with Approximation Algorithms: Online Gradient Descent with Infeasible Projections onto CH(αK) Has Expected α-Regret at Most α²R²/(Tη) + ηF²/2 + 3FεResearch Paper

Online learning with an approximation algorithm

Many sequential decision problems have a combinatorial action set: each round a decision maker picks a route, a schedule or a cut, and only afterwards learns its cost. When the offline problem — minimize a known linear cost over the action set — is NP-hard, the best available tool is an approximation algorithm, which returns a feasible action whose cost is within a factor $\alpha$ of optimal. The natural benchmark online is then the $\alpha$ -regret: the learner's average cost minus $\alpha$ times the average cost of the best fixed action in hindsight.

Kakade, Kalai and Ligett (SIAM J. Comput. 2009) showed that any $\alpha$ -approximation oracle can be converted into an online algorithm with vanishing $\alpha$ -regret, but their conversion may call the oracle $O(T)$ times per round. Garber (arXiv:1709.03093, Mathematics of Operations Research 2021) gave the first conversion whose expected $\alpha$ -regret is $O(T^{-1/3})$ while the number of oracle calls per round is polylogarithmic in $T$ , in both the full-information and the bandit settings. This mission formalizes the full-information regret bound, Theorem 1 of that paper.

Setting

Vectors live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|$ and dot product $x\cdot f$ ; $\mathbb R^d_+$ is the non-negative orthant. An instance consists of compact sets $\mathcal K,\mathcal F\subset\mathbb R^d_+$ , with $\mathcal K$ nonempty, and constants $R,F,C>0$ such that $\|x\|\le R$ on $\mathcal K$ , $\|f\|\le F$ on $\mathcal F$ , and $0\le x\cdot f\le C$ for $x\in\mathcal K$ , $f\in\mathcal F$ . Here $\mathcal K$ is the set of actions and $\mathcal F$ the set of loss (or payoff) vectors.

An $\alpha$ -approximation oracle ( $\alpha>0$ ) is a map $\mathcal O_{\mathcal K}$ that, for every $c\in\mathbb R^d_+$ , returns $\mathcal O_{\mathcal K}(c)\in\mathcal K$ with $\mathcal O_{\mathcal K}(c)\cdot c\le\alpha\min_{x\in\mathcal K}x\cdot c$ when $\alpha\ge1$ (loss minimization), or $\mathcal O_{\mathcal K}(c)\cdot c\ge\alpha\max_{x\in\mathcal K}x\cdot c$ when $\alpha<1$ (payoff maximization).

Over $T$ rounds an oblivious adversary fixes $f_1,\dots,f_T\in\mathcal F$ in advance, and the learner plays $x_1,\dots,x_T\in\mathcal K$ . The $\alpha$ -regret is

\frac1T\sum_{t=1}^Tx_t\cdot f_t-\alpha\min_{x\in\mathcal K}\frac1T\sum_{t=1}^Tx\cdot f_t\quad(\alpha\ge1),\qquad \alpha\max_{x\in\mathcal K}\frac1T\sum_{t=1}^Tx\cdot f_t-\frac1T\sum_{t=1}^Tx_t\cdot f_t\quad(\alpha<1).

The algorithm (Algorithm 3) is online gradient descent over $\mathrm{CH}(\alpha\mathcal K)$ , the convex hull of $\alpha\mathcal K=\{\alpha x:x\in\mathcal K\}$ , with exact projections replaced by infeasible projections: a point $\tilde y$ with $\|\tilde y-z\|^2\le\|y-z\|^2$ for all $z\in\mathrm{CH}(\alpha\mathcal K)$ . They are computed by Algorithm 2, which repeatedly runs an Ellipsoid-method separation-or-decomposition procedure (Lemma 5) driven by an extended oracle $\hat{\mathcal O}_{\mathcal K}$ (Lemma 1) that accepts every direction in $\mathbb R^d$ . When no separating direction is found, the procedure returns a probability vector $(a_1,\dots,a_N)$ over feasible points $s_1,\dots,s_N\in\mathcal K$ , and the learner samples its next action from it.

Formalization targets

Goal: Theorem 1 (regret bound)

For $\eta>0$ , $\varepsilon\in(0,(\alpha+2)R]$ and $T\ge1$ , the points $s_1,\dots,s_T$ played by Algorithm 3 satisfy

\mathbb E\big[\alpha\text{-regret}(\{(s_t,f_t)\}_{t\in[T]})\big]\le\frac{\alpha^2R^2}{T\eta}+\frac{\eta F^2}{2}+3F\varepsilon .

The statement covers both $\alpha\ge1$ and $\alpha<1$ and every dimension $d\ge2$ .

Milestones

Lemma 1 (p. 6): the extended oracle $\hat{\mathcal O}_{\mathcal K}(c)=(v,s)$ satisfies $v\cdot c\le\min_{x\in\alpha\mathcal K}x\cdot c$ , $s$ dominates $v$ on $\mathcal F$ , and $\|v\|\le(\alpha+2)R$ .
Lemma 2 (p. 7): online gradient descent with infeasible projections keeps the regret bound $\frac1{2T\eta}\|x_1-x\|^2+\frac\eta{2T}\sum_t\|f_t\|^2$ against every $x$ in the feasible set.
Lemma 6 (p. 11): if $\min_i(x-v_i)\cdot w\le\varepsilon$ for every unit vector $w$ , the minimum-norm convex combination $p$ of the $v_i$ satisfies $\|p-x\|\le\varepsilon$ .
Lemma 5 (pp. 9–10): with $N\ge c\,d^2\ln\frac{(\alpha+1)R+\|x\|}{\varepsilon}$ Ellipsoid iterations, the procedure either finds $w$ with $(x-z)\cdot w\ge\varepsilon$ on $\alpha\mathcal K$ and $\|w\|\le1$ , or a convex combination $p$ of oracle outputs with $\|x-p\|\le3\varepsilon$ .
Lemma 7 (p. 12): Algorithm 2 terminates and returns an infeasible projection $\tilde y$ of its input onto $\mathrm{CH}(\alpha\mathcal K)$ with $\|p-\tilde y\|\le3\varepsilon$ .

Significance

Theorem 1 shows that low $\alpha$ -regret needs nothing beyond black-box access to an offline approximation algorithm, with an oracle cost per round that grows only logarithmically in the accuracy. It applies to any combinatorial problem with a linear objective and a known approximation algorithm, and it is the base of the paper's bandit result (Theorem 2), whose analysis reuses the same infeasible-projection argument.

The result is proved in the paper; none of it has been machine-checked. The mission adds a formal account of the model and the algorithms, including the conventions the paper leaves implicit (which Ellipsoid method, what the expectation ranges over). It also records two printed claims that are not stated here because they are incorrect as written: Lemma 7's iteration count $\lceil\alpha^2R^2/\varepsilon^2\rceil$ , replaced by termination, and the bound $2\alpha^2R^2$ in Lemma 7's "Moreover" clause. A formal proof would confirm the regret bound independently of these slips.

Difficulty

The obvious approach, online gradient descent over $\mathrm{CH}(\alpha\mathcal K)$ , needs Euclidean projections onto a set that can only be accessed by approximate linear optimization over $\mathcal K$ , and only for directions in $\mathbb R^d_+$ . Such an oracle cannot certify membership in $\mathrm{CH}(\alpha\mathcal K)$ and cannot optimize over it exactly, so exact projection is out of reach. Simulating the projection by an Ellipsoid run on $\mathrm{CH}(\alpha\mathcal K)$ itself also fails: the oracle answers only non-negative directions, and its answers are off by the factor $\alpha$ . The regret analysis must therefore survive projections that are infeasible, decompositions that are only approximately correct, and points that are not even in $\mathcal K$ .

For a formal proof the hardest part is Lemma 5. It is an Ellipsoid-method volume argument whose cut rule queries the oracle at every iterate, whose iteration constant is universal, and whose logarithm can be negative.

Formalization scope

All work is in the namespace ApproxOLO.FullInfo, in one definitions module. Vectors are Fin d → ℝ, and every norm is the Euclidean euclNorm x = √(x·x); Mathlib's ‖·‖ on this type (the sup norm) is not used anywhere. The two regimes $\alpha\ge1$ and $\alpha<1$ are kept everywhere, in the oracle, the regret, the extended oracle and the update $y_{t+1}=\tilde y_t\mp\eta f_t$ . The oracle guarantee is stated for every $x\in\mathcal K$ , which is equivalent to the min/max form. In the regret, the min and max are sInf/sSup of the image of the compact nonempty $\mathcal K$ .

The Ellipsoid method, which the paper does not specify, is fixed as follows: it starts at the unit ball, and its update is the standard central cut from the published LinearOptimization_EllipsoidMethod module, with cut vectors $x-v$ and $-w$ in that module's sign convention. That update has the factor $d^2/(d^2-1)$ , so Lemma 5, Lemma 7 and Theorem 1 assume $d\ge2$ . $T\ge1$ is assumed wherever the factor $1/T$ appears. The universal constant $c$ of Lemma 5 is quantified once, before the dimension and the instance. Each call of the procedure uses a positive integer number of iterations $N$ satisfying that lower bound, and the number may differ from call to call.

Algorithms 2 and 3 are run predicates. The choices the paper leaves open ( $s_1$ , the iteration budgets, the optimal solution of Problem (5)) are quantified universally. The expected $\alpha$ -regret is Eq. (1) evaluated at the per-round expected losses $\sum_ia_i\,s_i\cdot f_t$ . This equals the expectation by linearity, because the iterates never depend on the samples and the adversary is oblivious.

A statement with $N=0$ allowed, an infeasible oracle hypothesis, a fixed $\alpha\ge1$ , or a sup-norm in place of the Euclidean norm would be a different and partly trivial theorem; the statements exclude each of these. The sanity file exhibits an instance, an oracle and a one-round run satisfying all hypotheses.

Not formalized: the oracle-complexity bound $K(\eta,\varepsilon)$ and the "In particular" rates of Theorem 1 (big- $O$ statements with hidden constants), Lemma 7's iteration count and "Moreover" clause, the bandit setting (Definition 1, Algorithm 4, Theorem 2), and the comparison scheme of Lemmas 3–4. Reusable beyond this mission: the extended oracle, infeasible projections and Lemma 2, Lemma 6 on minimum-norm points of convex hulls, and the separation-or-decomposition procedure. Proofs of any milestone are welcome, as is a formal version of the oracle-complexity bound with explicit constants.

Selected references

D. Garber, Efficient Online Linear Optimization with Approximation Algorithms, Mathematics of Operations Research 46(1), 2021; preprint arXiv:1709.03093v1, 2017. https://arxiv.org/abs/1709.03093
S. M. Kakade, A. T. Kalai, K. Ligett, Playing Games with Approximation Algorithms, SIAM Journal on Computing 39(3), 2009. https://doi.org/10.1137/070701704
M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, Proceedings of ICML, 2003 (the origin of online gradient descent, reference [17] of the paper).
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 8 (the Ellipsoid method).
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

9 thms4 active usersReviewed

Probability Statistics·Captain: Shuze Chen

The Nature of Statistical Learning Theory I: The Key Theorem of Learning TheoryTextbook

Motivation

Empirical risk minimization (ERM) is the inductive principle behind most of statistical learning: a learning machine picks, from a set of functions, the one with the smallest average loss on the training data, in place of the one with the smallest expected loss under the unknown distribution. Whether this substitution is justified is the first question of learning theory, and Chapter 2 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) answers it.

The history is short. Vapnik and Chervonenkis gave the entropy criterion for uniform convergence of frequencies to probabilities in 1968 and published the proof in 1971 (Theory Probab. Appl. 16, 264–280); in 1981 they extended it to uniformly bounded real functions (Theory Probab. Appl. 26, 532–553); in 1989 they proved the key theorem, which reduces consistency of ERM to uniform one-sided convergence. The book states all of these results without proofs (Preface, p. xi); the proofs are in Vapnik, Statistical Learning Theory (Wiley 1998) and the cited papers.

Setting

Let $F$ be a probability measure on a measurable space $Z$ , and let $Q(z,\alpha)$ , $\alpha\in\Lambda$ , be a set of real functions on $Z$ indexed by an arbitrary parameter set $\Lambda$ . The risk of $\alpha$ is $R(\alpha)=\int Q(z,\alpha)\,dF(z)$ . For an i.i.d. sample $z_1,\dots,z_\ell$ drawn from $F$ , the empirical risk is $R_{\mathrm{emp}}(\alpha)=\frac1\ell\sum_{i=1}^\ell Q(z_i,\alpha)$ . Probabilities $P$ are taken under the product measure $F^\ell$ .

For $c\in\mathbb R$ let $\Lambda(c)=\{\alpha\in\Lambda : R(\alpha)>c\}$ . The ERM method is nontrivially consistent (from p. 38 on simply "consistent") if for every $c$ with $\Lambda(c)$ nonempty,

\inf_{\alpha\in\Lambda(c)}R_{\mathrm{emp}}(\alpha)\xrightarrow[\ell\to\infty]{P}\inf_{\alpha\in\Lambda(c)}R(\alpha). \tag{2.3}

Removing the functions of smallest risk rules out consistency that is caused only by a single function lying below all the others. Uniform one-sided convergence means $\lim_{\ell\to\infty}P\{\sup_{\alpha}(R(\alpha)-R_{\mathrm{emp}}(\alpha))>\varepsilon\}=0$ for all $\varepsilon>0$ (2.4). Uniform two-sided convergence is the same with $|R(\alpha)-R_{\mathrm{emp}}(\alpha)|$ (2.6).

For a set of bounded functions $A\le Q(z,\alpha)\le B$ , the random VC entropy $H^\Lambda(\varepsilon;z_1,\dots,z_\ell)=\ln N^\Lambda(\varepsilon;z_1,\dots,z_\ell)$ is the logarithm of the size of a minimal $\varepsilon$ -net, in the metric $C$ (maximum over the sample points), of the vectors $(Q(z_1,\alpha),\dots,Q(z_\ell,\alpha))$ . The net is internal: its points are themselves vectors of the set. The VC entropy is $H^\Lambda(\varepsilon,\ell)=E\,H^\Lambda(\varepsilon;z_1,\dots,z_\ell)$ . For indicator functions, $N^\Lambda(z_1,\dots,z_\ell)$ is the number of distinct binary vectors on the sample. From it the book defines the entropy $H^\Lambda(\ell)=E\ln N^\Lambda$ , the annealed VC entropy $H^\Lambda_{\mathrm{ann}}(\ell)=\ln E N^\Lambda$ , and the growth function $G^\Lambda(\ell)=\ln\sup_{z_1,\dots,z_\ell}N^\Lambda$ .

Formalization targets

Goal: Theorem 2.1, the key theorem (p. 38)

If $A\le R(\alpha)\le B$ for all $\alpha\in\Lambda$ , then

\text{ERM is consistent}\iff\lim_{\ell\to\infty}P\Bigl\{\sup_{\alpha\in\Lambda}\bigl(R(\alpha)-R_{\mathrm{emp}}(\alpha)\bigr)>\varepsilon\Bigr\}=0\quad\forall\varepsilon>0.

Only the risks are bounded, not the functions. The constants $A$ and $B$ are arbitrary, and they appear only in the hypothesis.

Milestones

Section 2.3.1, p. 41. For a finite set of integrable functions, $\xi^\ell=\sup_\alpha|R(\alpha)-R_{\mathrm{emp}}(\alpha)|\to0$ in probability.
Section 2.7, pp. 55–56. For indicator functions, $H^\Lambda(\ell)\le H^\Lambda_{\mathrm{ann}}(\ell)\le G^\Lambda(\ell)$ for every $\ell$ .
Section 2.6.1, p. 50. For indicator functions, $H^\Lambda(\ell)/\ell$ is non-increasing for $\ell\ge1$ .
Theorem 2.3, p. 45. For bounded real functions, uniform two-sided convergence holds iff $\lim_{\ell\to\infty}H^\Lambda(\varepsilon,\ell)/\ell=0$ for all $\varepsilon>0$ (2.10).
Corollary of Theorem 2.3, p. 45. The indicator case, $\lim H^\Lambda(\ell)/\ell=0$ . It is already proved on the platform as VapnikChervonenkis.Entropy.theorem4_entropy_criterion and is referenced here.

Significance

The key theorem says that consistency of ERM is decided by the worst function of the set, in the one-sided sense of (2.4). Every analysis of ERM must therefore control a supremum over the whole set, a worst-case analysis (p. 39). This turns the question of consistency into the question of uniform laws of large numbers. Theorem 2.3 and its corollary answer that question through the VC entropy. The three capacity concepts $H^\Lambda\le H^\Lambda_{\mathrm{ann}}\le G^\Lambda$ underlie the "three milestones" of §2.7: consistency, a fast rate of convergence, and distribution-free guarantees. These are also the objects of the later missions of this series.

The platform already has the 1971 indicator-class criterion (Proved) and the related entropy-rate lemmas for event classes. It has no real-valued loss class with a parameter set, no notion of nontrivial consistency, no key theorem, and no VC entropy built from $\varepsilon$ -nets of real functions. This mission supplies those definitions with the book's conventions, and states the key theorem and its neighbours as open targets.

Difficulty

The theorem is an equivalence between a statement about infima over the shrinking families $\Lambda(c)$ and a statement about one supremum over all of $\Lambda$ . Neither the functions nor the empirical risks are bounded; only the risks are. The empirical infimum over $\Lambda(c)$ may therefore be $-\infty$ , and no compactness of $\Lambda$ is available. Single-function laws of large numbers control each $\alpha$ separately, but they do not control the supremum: for an infinite $\Lambda$ they are not enough, and that is the content of the chapter. For Theorem 2.3, the necessity direction is a genuine probabilistic argument about the growth of covering numbers, and the measurability of suprema over an uncountable $\Lambda$ must be handled explicitly.

Formalization scope

All declarations are in the namespace NatureSLT.Consistency. The parameter set $\Lambda$ is an arbitrary Lean type and $Q:\Lambda\to Z\to\mathbb R$ . A sample of size $\ell$ is Fin ℓ → Z under Measure.pi (fun _ => F), and a probability is a value of that measure in $[0,\infty]$ . The risk is a Bochner integral, and every theorem that uses it assumes each $Q(\cdot,\alpha)$ integrable. Logarithms are natural. The minimal $\varepsilon$ -net is internal and uses the metric $C$ , as in the book's footnote 3; it is not Mathlib's external covering number. "Monotonically decreases" (p. 50) is read as non-increasing.

Suprema of deviations and the infimum of empirical risks over $\Lambda(c)$ are taken in the extended reals, so they are genuine values and never a junk default. The infimum of the risks is a real infimum over a nonempty $\Lambda(c)$ , which is bounded below by $c$ . No extended-real subtraction occurs: the event $|X-a|>\varepsilon$ is written as $X<a-\varepsilon$ or $a+\varepsilon<X$ .

The book's "some (technical) conditions of measurability" are explicit hypotheses. In Theorem 2.1, $\sup_\alpha(R-R_{\mathrm{emp}})$ and $\inf_{\Lambda(c)}R_{\mathrm{emp}}$ are measurable functions of the sample. In Theorem 2.3, $Q(\cdot,\alpha)$ , $\xi^\ell$ , the half-sample deviation and the random VC entropy are measurable. For indicator classes, $N^\Lambda$ is measurable.

A trivializing formalization is ruled out. Consistency is the nontrivial notion (2.3), quantified over every nonempty $\Lambda(c)$ , not the classical one that a minorizing function satisfies trivially. The probability of a non-measurable event is never read as $0$ : Lean evaluates it as an outer measure.

Beyond the paper. One strengthened variant is posed, key_theorem_strong (finding F1). It is Theorem 2.1 with the two measurability hypotheses removed and probabilities read as outer probabilities. The known argument needs only monotonicity and finite subadditivity of the probability of events, together with the weak law of large numbers for a single integrable function, so measurability is never used.

Contributions are welcome on any item. Reusable beyond this mission are the risk and empirical-risk definitions, uniform one- and two-sided convergence, and the VC entropy of a real class. Theorems 2.2 (maximum likelihood), 2.4 (one-sided convergence through minorant classes), 2.5 and 2.6 (nonfalsifiability) are not part of this mission.

Selected references

V. N. Vapnik, The Nature of Statistical Learning Theory, 2nd ed., Springer, 2000. doi:10.1007/978-1-4757-3264-1
V. N. Vapnik, Statistical Learning Theory, Wiley, 1998. ISBN 978-0-471-03003-4.
V. N. Vapnik and A. Ya. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities", Theory Probab. Appl. 16 (1971), 264–280. doi:10.1137/1116025
V. N. Vapnik and A. Ya. Chervonenkis, "Necessary and sufficient conditions for the uniform convergence of means to their expectations", Theory Probab. Appl. 26 (1981), 532–553. doi:10.1137/1126059
V. N. Vapnik and A. Ya. Chervonenkis, "The necessary and sufficient conditions for consistency of the method of empirical risk minimization", Yearbook of the Academy of Sciences of the USSR on Recognition, Classification, and Forecasting 2 (1989), 217–249; English translation in Pattern Recognition and Image Analysis 1(3) (1991), 284–305.

11 thms4 active usersReviewed

Completed

Operations Research Statistics·Captain: mikedeng1

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low VI: A BIC-Type Choice of the Model Size Yields Oracle Inequalities for the Expected Prediction ErrorResearch Paper

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors: it minimizes the residual sum of squares $\|y-X\beta\|^2$ over all $\beta$ with at most $k$ nonzero coordinates. It is the classical benchmark for sparse regression, and mixed-integer optimization has made it computable at scales that used to be out of reach (Bertsimas, King & Mazumder, 2016). When the signal-to-noise ratio is low, however, best subsets overfits, and Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty $\lambda\|\beta\|_q$ ( $q\in\{1,2\}$ ) to it. Their oracle inequalities for the penalized estimators hold for a fixed model size $k$ , and the practitioner still has to choose $k$ .

§3.5 of the paper removes that choice. It replaces the cardinality constraint with BIC-type penalties that depend on the candidate model size, and Theorem 5 shows that the resulting estimators satisfy oracle inequalities for the expected prediction error over all of $\mathbb R^p$ , with no condition on the design beyond the normalization of its columns. This mission formalizes Theorem 5 and the steps of its printed proof.

Setting

We observe $y=f^*+\epsilon\in\mathbb R^n$ . The mean $f^*\in\mathbb R^n$ is deterministic and unknown, and $\epsilon$ has independent $N(0,\sigma^2)$ entries with $\sigma>0$ . The design $X\in\mathbb R^{n\times p}$ is deterministic, with $p\ge1$ and columns of unit Euclidean norm. The prediction error of an estimate $\hat\beta$ is $\|f^*-X\hat\beta\|^2$ . For $\beta\in\mathbb R^p$ , $\|\beta\|$ is the Euclidean norm, $\|\beta\|_1=\sum_j|\beta_j|$ , and $\|\beta\|_0$ is the number of nonzero coordinates.

For nonnegative tuning parameters $a$ and $b$ , the data-dependent penalties are

\lambda_\beta=a\sqrt{\|\beta\|_0\log(ep/\|\beta\|_0)},\qquad \mu_\beta=b\log(ep/\|\beta\|_0),

with the convention $0\cdot\infty=0$ , so the empty model is not penalized. The BIC-type estimators are

\hat\beta^B_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0,\qquad \hat\beta^B_1\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0,

where $\lambda\ge0$ is a fixed number. Both are unconstrained problems. Solving them is equivalent to solving the constrained problems with $\|\beta\|_0\le k$ for each $k$ and then choosing $k$ by the penalty. A minimizer exists but need not be unique.

The proof works on events of the noise vector. For an integer $s$ and $\delta_0\in(0,1]$ the event $G'_s$ requires

\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+3\log(1/\delta_0)}\,\|Xu\|\qquad\text{for every }u\text{ with }\|u\|_0\le s .

Formalization targets

Goal: Theorem 5 (p. 21)

There exist universal constants $a_0,b_0,c_0$ such that, if $a\ge a_0\sigma$ or $b\ge b_0\sigma^2$ ,

\mathbb E\|f^*-X\hat\beta^B_2\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0\Big]+\sigma^2,

and, if $\lambda\ge c_0\sigma\sqrt{\log(ep)}$ or $b\ge b_0\sigma^2$ ,

\mathbb E\|f^*-X\hat\beta^B_1\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0\Big]+\sigma^2 .

Here $\lesssim$ hides one universal multiplicative constant. The constants are not specified, so the goal records the shape of the bound and is not invalidated by later improvements of the constants.

Milestones (proof of Theorem 5, B.13, and B.5)

(51): the deterministic basic inequality for $\hat\beta^B_2$ .
(54): for $a\gtrsim\sigma$ , with probability at least $1-\delta_0/2$ , $\|f^*-X\hat\beta\|^2+\mu_{\hat\beta}\|\hat\beta\|_0\lesssim\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\sigma^2\log(1/\delta_0)+\mu_\beta\|\beta\|_0$ .
The union bound over model sizes: with $G=\bigcap_{s=1}^pG'_s$ , where $G'_s$ is taken at $\delta_0=(s/[ep])^s\epsilon_0$ , we have $P(G^c)\le\epsilon_0$ .
(55): for $b\gtrsim\sigma^2$ , the analogue of (54) with probability at least $1-\epsilon_0$ .
(56): under either condition, the high-probability oracle inequality with $\inf_\beta$ and $\sigma^2\log(1/\delta_0)$ .
The tail-to-expectation step of B.5: if $W\le\kappa\log(1/\delta_0)$ with probability at least $1-\delta_0/2$ , then $\mathbb EW^+\le\kappa/2$ .
(58): the high-probability counterpart of (56) for $\hat\beta^B_1$ .

Significance

The result. Theorems 2 and 3 of the paper give oracle inequalities only over the sparsity class $\{\|\beta\|_0\le k\}$ for a $k$ fixed in advance. Theorem 5 makes the model size data-driven. Its bounds hold over all of $\mathbb R^p$ and need no restricted-eigenvalue or sparse-eigenvalue condition on $X$ . Corollary 6 of the paper deduces from it that the estimators attain the error rates of Corollaries 3 and 4 while selecting models of the same order as the true model size. The paper also notes that the slow-rate bound for $\hat\beta^B_1$ with $b=0$ is a bound for the Lasso.

Formalizing it. Theorem 5 is a published result with a printed proof (Supplement B.13). The proof is written up to unspecified universal constants, and it defers two steps to other parts of the paper ("repeating the argument after inequality (32)" and "repeating the argument in the proof of Corollary 3"). A formal proof makes every constant and every deferred step explicit. No part of the paper has been machine-checked, to the best of our search.

Difficulty

The argument is long rather than deep. The obvious first attempt fixes the selected model size $\hat k=\|\hat\beta\|_0$ and applies a high-probability bound for that size. This fails because $\hat k$ is random and depends on $\epsilon$ , so a bound for each fixed $s$ says nothing about the random $\hat k$ . The noise term must be controlled simultaneously over all model sizes, at a total failure probability that does not grow with $p$ . The second obstacle is the passage from high-probability bounds, which hold for every $\delta_0$ and grow like $\log(1/\delta_0)$ , to a bound in expectation. That passage needs the high-probability statement with a constant that is uniform in $\delta_0$ .

Formalization scope

Representation. Vectors are Fin n → ℝ and Fin p → ℝ, and the design is a Matrix (Fin n) (Fin p) ℝ.
- The norms $\|\cdot\|$ , $\|\cdot\|_1$ and $\|\cdot\|_0$ are explicit definitions (l2, l1, l0), because Mathlib's norm on Fin m → ℝ is the sup norm.
- The noise law is the product of $n$ centred Gaussians with variance $\sigma^2$ (noiseLaw).
- Logarithms are natural, and $e=\exp(1)$ .
Model. The standing hypotheses are:
- unit-norm columns of $X$ ;
- $\sigma>0$ and $p\ge1$ ;
- $a,b\ge0$ , and $\lambda\ge0$ for $\hat\beta^B_1$ .
The quantities $X$ , $f^*$ , $\sigma$ , $a$ , $b$ , $\lambda$ and the penalties are inputs. The randomness is the law of $\epsilon$ alone, and $y=f^*+\epsilon$ .
Estimators are argmin predicates IsBIC2, IsBIC1: " $\hat\beta$ minimizes the objective over all of $\mathbb R^p$ ". Every statement holds for every minimizer.
- In Theorem 5 an estimator is a measurable map $y\mapsto\hat\beta(y)$ that is a minimizer for every $y$ , and the bound is claimed for every such selection.
- The expectation is a lower Lebesgue integral in $[0,\infty]$ , so a non-integrable error cannot make the bound vacuous.
Constants.
- " $\lesssim$ " is one universal constant $C>0$ , quantified before every other parameter.
- " $\inf_\beta[\dots]$ " is written as "for every $\beta$ ".
- "With probability at least $1-\delta$ " is the existence of a measurable event of probability at least $1-\delta$ on which the inequality holds.
- The constants $a_0$ , $b_0$ and $c_0$ carry no sign, as on the page.
Correction. Theorem 1 of the paper states $P(G_s)\ge1-\delta_0$ for an event with coefficient $1$ on $\log(1/\delta_0)$ . That bound is false for small $\delta_0$ (already for $n=p=s=1$ ). The union bound here uses the corrected event $G'_s$ with coefficient $3$ , which inside $\lesssim$ changes nothing downstream.
Ruled out. None of the following counts as a formalization of the goal:
- an arbitrary or non-measurable selection of the minimizer;
- a Bochner integral, which is $0$ for a non-integrable error;
- a constant that depends on $n$ , $p$ , $\delta_0$ or the design;
- a fixed $\delta_0$ or $\epsilon_0$ .
Not formalized here. The fixed- $k$ oracle inequalities (Theorems 2 and 3), the noise events of Theorem 1, the lower bound (Theorem 4), Corollaries 1–6 and the numerical study are not part of this mission. Some of them are the subjects of the other missions of this series. The proof of Theorem 5 needs the probability bounds for the events $F$ and $G'_s$ of Theorem 1 and the deterministic arguments of Theorems 2 and 3. A solver may prove them here or import them once they are published.
Contributions welcome.
- Gaussian chi-square tail bounds (Laurent–Massart);
- the bound for the sorted- $\ell_1$ event $F$ (Bellec, Lecué & Tsybakov);
- the existence of measurable selections of the argmin;
- the layer-cake step.
These are reusable well beyond this paper.

Selected references

R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
B. Laurent, P. Massart, Adaptive estimation of a quadratic functional by model selection, Annals of Statistics 28(5), 2000. https://doi.org/10.1214/aos/1015957395
L. Birgé, P. Massart, Gaussian model selection, Journal of the European Mathematical Society 3, 2001. https://doi.org/10.1007/s100970100031

15 thms4 active usersReviewed

Reinforcement Learning Statistics·Captain: mikedeng1

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 2: The Conservative Model-Based Policy Is ε-Optimal w.p. 1−δ at the Sample Size of Theorem 1Research Paper

Motivation

Reinforcement learning with a generative model (a simulator that returns an independent next state for any queried state–action pair) is the standard setting for measuring how many samples are needed to plan in an unknown Markov decision process. The simplest algorithm is model-based planning: query each pair $N$ times, build the empirical transition kernel, and plan in the resulting empirical MDP. Azar, Munos and Kappen (2013) showed that $\widetilde O\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^3\varepsilon^2}\big)$ total samples suffice and are necessary, but only for $\varepsilon \le 1/\sqrt{(1-\gamma)|\mathcal S|}$ . Agarwal, Kakade and Yang (2020) extended the range to $\varepsilon \le 1/\sqrt{1-\gamma}$ . A sample size barrier remained: for larger $\varepsilon$ , no algorithm was known to be minimax optimal with fewer than $\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^2}$ samples.

Li, Wei, Chi and Chen (arXiv:2005.12900v8, Operations Research, 2024) remove the barrier: the sample size is minimax optimal over the full range $0 < \varepsilon \le 1/(1-\gamma)$ . They give two planners. The first (Theorem 1) perturbs the rewards slightly at random. The second, the subject of this mission, leaves the rewards unchanged and instead chooses among near-optimal actions by a randomized but structured rule.

Timeline:

2013: Azar–Munos–Kappen, minimax sample complexity of model-based planning for $\varepsilon \le 1/\sqrt{(1-\gamma)|\mathcal S|}$ .
2018: Sidford, Wang, Wu, Yang and Ye, a model-free variance-reduced method, minimax for $\varepsilon \le 1$ .
2020: Agarwal–Kakade–Yang, model-based planning minimax for $\varepsilon \le 1/\sqrt{1-\gamma}$ , via absorbing MDPs.
2020 (v1) – 2024: Li–Wei–Chi–Chen, the full range $\varepsilon \le 1/(1-\gamma)$ (this paper).

Setting

A finite discounted MDP $\mathcal M = (\mathcal S,\mathcal A,P,r,\gamma)$ has states $\mathcal S$ , actions $\mathcal A = \{1,\dots,|\mathcal A|\}$ , a transition kernel $P(\cdot\mid s,a)$ , rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in(0,1)$ . A deterministic policy $\pi:\mathcal S\to\mathcal A$ has value $V^\pi(s)$ , the expected discounted sum of rewards from $s$ , and Q-function $Q^\pi(s,a) = r(s,a) + \gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ . The optimal value is $V^\star(s) = \max_\pi V^\pi(s)$ and $Q^\star = r + \gamma P V^\star$ .

The data are $N$ independent next states $s^i_{s,a}\sim P(\cdot\mid s,a)$ for every pair, and the empirical kernel is $\widehat P(s'\mid s,a) = \frac1N\sum_i \mathbb 1\{s^i_{s,a} = s'\}$ . The empirical MDP $\widehat{\mathcal M} = (\mathcal S,\mathcal A,\widehat P,r,\gamma)$ has optimal functions $\widehat Q^\star$ and $\widehat V^\star$ .

The conservative planner (Algorithm 2) draws a threshold $\varsigma\sim\mathrm{Unif}(0,\xi)$ independently of the data and plays

\widehat\pi_{\mathrm c}(s) := \min\{a\in\mathcal A : \widehat Q^\star(s,a) > \widehat V^\star(s) - \varsigma\},

the smallest-indexed action whose empirical Q-value is within $\varsigma$ of optimal.

Formalization targets

Goal: Theorem 2

There are universal constants $c_0, c_1 > 0$ such that, for every MDP as above, every $\delta > 0$ and $0 < \varepsilon \le \frac1{1-\gamma}$ , with $\xi = \frac{c_1(1-\gamma)\varepsilon}{|\mathcal S|^5|\mathcal A|^5}$ and

N \ge \frac{c_0\log\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)\varepsilon\delta}\big)}{(1-\gamma)^3\varepsilon^2},

with probability at least $1-\delta$ over the data and $\varsigma$ ,

\forall (s,a):\qquad V^{\widehat\pi_{\mathrm c}}(s)\ge V^\star(s)-\varepsilon \quad\text{and}\quad Q^{\widehat\pi_{\mathrm c}}(s,a)\ge Q^\star(s,a)-\gamma\varepsilon.

The constants are left unspecified, as in the paper.

Milestones

The paper's own steps, in the order of §6.4:

Lemma 7: $\widehat V^{\pi^\star} - \widehat V^{\widehat\pi_{\mathrm c}} \le \frac{\xi}{1-\gamma}\mathbf 1$ .
Lemma 3 and (88): the $(s,a)$ -absorbing MDPs reproduce $Q^\star$ at the right reward and depend Lipschitz-continuously on it.
(56): a point of a finite net gives an absorbing MDP within $\omega$ of $\widehat Q^\star$ .
Lemma 8: with probability $1-\delta$ over $\varsigma$ , the near-optimal action sets are unchanged by any perturbation of size $\frac{\xi\delta}{8|\mathcal S||\mathcal A|}$ .
(57): consequently $\widehat\pi_{\mathrm c}$ coincides with the conservative policy of every nearby absorbing MDP.
Lemmas 2 and 1: the policy-evaluation bounds used for the remaining terms of (53).

Significance

Theorem 2 shows that the minimax sample size $\widetilde O\big(\frac{|\mathcal S||\mathcal A|}{(1-\gamma)^3\varepsilon^2}\big)$ is reachable over the whole range of $\varepsilon$ without altering the reward function: a planner can keep the model it estimated and only change how it breaks near-ties. The guarantee covers both value and Q-function suboptimality, and with a sample size proportional to $1/(1-\gamma)$ rather than $1/(1-\gamma)^2$ in the large- $\varepsilon$ regime it allows a coarse but correct policy to be computed from very few samples.

None of these results is formalized. The mission produces a machine-checked account of the decoupling argument for data-dependent policies (absorbing MDPs, nets, stability of the tie-breaking rule), which the companion missions on Theorems 1 and 3 share. The paper omits the last step of the proof of Theorem 2 ("follows from an identical argument as in the proof of Theorem 1"); a formal proof has to supply it, including the analogue of Lemma 5 for $\widehat\pi_{\mathrm c}$ , which the paper does not state.

Difficulty

The policy $\widehat\pi_{\mathrm c}$ depends on all the data, so the standard concentration argument for a fixed policy (Lemma 1) does not apply to $\widehat V^{\widehat\pi_{\mathrm c}} - V^{\widehat\pi_{\mathrm c}}$ . A union bound over all $|\mathcal A|^{|\mathcal S|}$ deterministic policies costs a factor $|\mathcal S|$ in the sample size, which is exactly the barrier. The leave-one-out construction removes the samples of one pair $(s,a)$ from the policy; it works only if the policy is stable under the small change of $\widehat Q^\star$ that this causes. The greedy policy is not stable when two actions nearly tie. The conservative rule is stable with high probability over $\varsigma$ (Lemma 8), but only because it takes the smallest near-optimal action: the set $\{a : \widehat Q^\star(s,a) > \widehat V^\star(s)-\varsigma\}$ is stable, and a rule that picked an arbitrary member of it would not be.

Formalization scope

All declarations live in the namespace BreakingSample.Conservative. The MDP layer reuses the platform's FoundationsML.ReinforcementLearning definitions (IsTransitionKernel, PolicyValue, QFunction); deterministic policies enter as point-mass stochastic policies, and $V^\star$ is the maximum over the finite set of maps $\mathcal S\to\mathcal A$ . Norms are sup norms on finite function types. The order on $\mathcal A$ is an arbitrary linear order on a finite type.

Probability: a data set is a map $\mathcal S\times\mathcal A\times\mathrm{Fin}\,N\to\mathcal S$ with the product law, so probabilities of data events are finite sums. The threshold $\varsigma$ has the uniform law on $[0,\xi]$ ; joint probabilities are $\sum_x \mathbb P(x)\,\mathrm{Unif}(0,\xi)\{\varsigma : (x,\varsigma)\in E\}$ , with the outer measure for non-measurable sections. "With probability at least $1-\delta$ " is stated as an upper bound $\delta$ on the probability of the failure event. Because the policy defined by (10) is a predicate on policies, the conclusion is stated for every policy satisfying (10). The universal constants are quantified before all types and parameters. The goal adds $N>0$ , the standing assumption of (3); "the same assumptions of Theorem 1" is formalized with the goal's own constants $c_0, c_1$ .

A trivializing formalization is ruled out: $\widehat\pi_{\mathrm c}$ is the smallest-index rule of (10), not an arbitrary policy within $\varsigma$ of optimal, and $\varsigma$ is random, not fixed.

Infrastructure that a complete development needs and that is reusable: Bellman optimality for finite MDPs with deterministic policies and real rewards, the resolvent identities, Bernstein's inequality for the empirical kernel, the absorbing-MDP construction, and the analogue of Lemma 5 for the conservative policy. Proofs of any milestone, and of the policy-evaluation lemmas, are welcome.

Selected references

G. Li, Y. Wei, Y. Chi, Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8. https://arxiv.org/abs/2005.12900
M. G. Azar, R. Munos, H. J. Kappen, Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model, Machine Learning 91, 2013. https://doi.org/10.1007/s10994-013-5368-1
A. Agarwal, S. Kakade, L. F. Yang, Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal, COLT 2020. https://arxiv.org/abs/1906.03804
A. Sidford, M. Wang, X. Wu, L. F. Yang, Y. Ye, Near-Optimal Time and Sample Complexities for Solving Markov Decision Processes with a Generative Model, NeurIPS 2018. https://arxiv.org/abs/1806.01492

17 thms4 active usersReviewed

Bandit Algorithms Operations Research Statistics·Captain: mikedeng1

Distribution-Free Contextual Dynamic Pricing 1: The DIP Policy Has Expected Regret at Most C T^(2/3) log T Plus 4 p_max L Times the Episode-Weighted ℓ₁ Estimation ErrorsResearch Paper

Motivation

In contextual dynamic pricing a seller posts a price for each arriving customer, observes only whether the customer buys, and must learn the demand from these binary responses while selling. The problem arises in e-commerce, insurance and consumer lending, where every customer comes with features (product attributes, customer characteristics) that shift the willingness to pay. Most regret analyses assume either that the noise distribution of the valuation is known up to a parameter, or that it belongs to a parametric family. Luo, Sun and Liu (arXiv:2109.07340, Mathematics of Operations Research, 2024) drop that assumption: the valuation is linear in the features plus a noise with an unknown distribution, and they give a policy, DIP, whose regret is bounded without parametric knowledge of the noise.

This mission formalizes the paper's main upper bound, Theorem 1, together with the chain of lemmas and propositions of its proof. The source is the arXiv v2 preprint (6 March 2023); all proofs are in its Appendix A.

Setting

At each period $t = 1, 2, \dots$ a customer arrives with a covariate $x_t \in \mathcal X \subseteq \mathbb R^{d_0}$ , where $\|x\|_\infty \le 1$ on $\mathcal X$ . The customer's valuation is $v_t = x_t^\top\theta_0 + z_t$ , with an unknown parameter $\theta_0$ , $\|\theta_0\|_1 \le W$ for a known $W$ , and market noises $z_t$ drawn i.i.d. from an unknown CDF $F$ . The seller posts a price $p_t \in (0, p_{\max})$ and observes $y_t = \mathbf 1\{v_t \ge p_t\}$ ; the revenue is $p_ty_t$ . The expected revenue of price $p$ at linear value $q = x^\top\theta_0$ is

f_q(p) = p\bigl(1 - F(p - q)\bigr).

The clairvoyant price $p^*(x)$ maximizes $f_{x^\top\theta_0}$ over $p > 0$ and is assumed to lie in $(0, p_{\max})$ . The regret of period $t$ is $r_t = f_{x_t^\top\theta_0}(p^*(x_t)) - f_{x_t^\top\theta_0}(p_t)$ , and $R_T = \sum_{t=1}^T r_t$ .

Two assumptions are made on $F$ . Assumption 1: $F$ is $L$ -Lipschitz. Assumption 2: there is a constant $C_A$ with $f_q(p^*(x)) - f_q(p) \le C_A(p^*(x) - p)^2$ for all $x \in \mathcal X$ , $q = x^\top\theta_0$ and $p \in [0, p_{\max}]$ .

The DIP policy (Algorithm 4) splits time into episodes of lengths $\ell_1 = \alpha_1$ and $\ell_k = 2^{k-2}\ell_2$ , $\ell_2 = \alpha_2$ , for $k \ge 2$ . In episode $k \ge 2$ it takes an estimate $\hat\theta_{k-1}$ computed from episode $k-1$ (Inner Algorithm A), cuts $G(\hat\theta) = [-\|\hat\theta\|_1, p_{\max} + \|\hat\theta\|_1]$ into $d_k = C_d\lceil(2^{k-2}\ell_2)^{1/6}\rceil$ equal pieces with midpoints $m_j$ , and runs a UCB rule (Inner Algorithm B) over the candidate prices $m_j + x_t^\top\hat\theta \in (0, p_{\max})$ . The UCB step is analysed as a perturbed linear bandit (PLB): rewards $Z_t = \langle\xi_t, A_t\rangle + \eta_t$ whose parameters satisfy $\|\xi_s - \xi_t\|_\infty \le C_p$ . The algorithm M-LinUCB (Algorithm 5) is optimistic linear UCB with forced exploration of new coordinates.

Formalization targets

Goal: Theorem 1 with the $\tilde O$ pinned

For every model satisfying the standing assumptions and Assumptions 1–2, every DIP configuration with $p_{\max} + 2W < C_d\,p_{\max}$ and $\lambda > 0$ , there is $C > 0$ such that every run of DIP satisfies, for all $T \ge 2$ ,

\mathbb E(R_T) \le C\,T^{2/3}\log T + 4p_{\max}L\sum_{k=2}^{n}2^{k-2}\ell_2\,\mathbb E\|\hat\theta_{k-1} - \theta_0\|_1,

where $n = n(T, \alpha_1, \alpha_2)$ is the number of episodes. The printed statement reads $\tilde O(T^{2/3})$ ; the single logarithm is what the proof gives.

Milestones

In the order of the proof: Lemma 1 (the pricing problem of one episode is a PLB with perturbation $2L\|\hat\theta - \theta_0\|_1$ ); Lemma 2 (M-LinUCB on that PLB is Inner Algorithm B); Lemmas S1–S5 (weighted averages, the elliptical potential lemma, the shadow parameter, the self-normalized bound, a confidence ellipsoid); Lemma 3 (M-LinUCB on a PLB has regret $\tilde O(d\sqrt{T_0}) + 2a_{\max}C_pT_0$ with high probability); Proposition 4 (the discrete-part regret of one episode); Lemma S6 (the confidence term in $\sqrt d\log T_0$ form); Proposition 3 (the total regret of one episode, $\mathbb E(R_{T_0}) \le C'_3\log(C'_2T_0)T_0^{2/3} + 4p_{\max}L\|\hat\theta - \theta_0\|_1T_0$ ). Lemmas S2 and S4 are already proved on the platform and are referenced.

Significance

The bound separates the cost of learning the unknown noise distribution, $T^{2/3}$ up to a logarithm, from the cost of estimating $\theta_0$ , which enters only through the $\ell_1$ estimation errors. Any estimator with a known error rate therefore gives an explicit regret rate for DIP: if $\mathbb E\|\hat\theta_k - \theta_0\|_1 = O(\ell_k^{-\alpha})$ with $0 < \alpha \le 1/2$ , the regret is $\tilde O(T^{2/3 \vee (1-\alpha)})$ (p. 19). The rate of the paper's logistic-regression estimator on adaptively collected data is not established; the authors study it by simulation. Lemma 3 is a regret bound for linear bandits with bounded parameter drift that is linear in the drift and $\tilde O(d\sqrt{T_0})$ otherwise, which the authors note is of independent interest.

The results are proved in the paper, not formalized. The two textbook lemmas the paper quotes, the elliptical potential lemma (S2) and the self-normalized bound (S4), are already proved on the platform; the paper's own results (Lemma 3, the PLB reduction, the episode analysis and Theorem 1) have no machine-checked proof. Faithfulness checks during drafting found printed slips that the formal statements correct and disclose: the unsquared norm in Lemma S2, the finite UCB of an unpulled arm in display (2), and a missing nonemptiness condition for the candidate price sets.

Difficulty

The obvious argument treats each episode as a linear bandit around the central parameter $\xi^* = (1 - F(m_j))_j$ and invokes the standard optimistic regret bound. That fails because the parameter $\xi_t$ moves with the covariate $x_t$ through the estimation error $x_t^\top(\hat\theta - \theta_0)$ ; the ridge estimate then tracks no fixed vector, and a general misspecified-bandit bound pays an extra factor $\sqrt d$ in the drift term (Remark 5, p. 21), which destroys the $T^{2/3}$ rate once $d$ grows with the horizon. A second difficulty is bookkeeping: the per-episode bound must hold uniformly over the random estimate $\hat\theta_{k-1}$ , over the growing discretization $d_k$ , and over the truncated last episode, before the episodes are summed.

Formalization scope

Periods are 1-based; arm indices are Fin d, 0-based. Norms are written out: $\|v\|_1 = \sum_i|v_i|$ , $\|v\|_\infty$ coordinatewise. The probability space carries a filtration $\mathcal G$ ; covariates and prices are $\mathcal G_{t-1}$ -measurable (adaptive or adversarial covariates and randomized prices are allowed), and $z_t$ has CDF $F$ and is independent of $\mathcal G_{t-1}$ . Conditional sub-Gaussianity is Mathlib's HasCondSubgaussianMGF, which needs a standard Borel sample space. Expectations are lower Lebesgue integrals of nonnegative regrets. "With probability at least $1 - \delta$ " means a measurable event of probability at least $1 - \delta$ on which the bound holds.

The standing assumptions are $\|\theta_0\|_1 \le W$ , $p_{\max} > 0$ , $\|x\|_\infty \le 1$ on $\mathcal X$ , and $p^*(x) \in (0, p_{\max})$ maximizing the revenue over $p > 0$ . Hypotheses added to the printed statements: $p_{\max} + 2\|\hat\theta\|_1 < d\,p_{\max}$ (resp. $p_{\max} + 2W < C_d\,p_{\max}$ ), which makes every candidate price set nonempty; $\|\hat\theta\|_1 \le W$ in Proposition 3; $\delta \in (0,1)$ in Lemma 3; finite action sets; a nonempty index set in Lemma S1. Algorithm 3 is read with forced exploration of unpulled arms, as Lemma 2 fixes. Inner Algorithm A is any measurable estimator of the previous episode's data with values in $\{\|\theta\|_1 \le W\}$ ; the paper's logistic regression with projection is one instance. Algorithms are run predicates that hold for every tie-breaking rule. The constants of Theorem 1, Proposition 3 and Lemma S6 are chosen before the processes, the estimate, $d$ and the horizon.

The formalization cannot be satisfied trivially: expectations are integrals of nonnegative quantities, so no non-integrability default applies; the run predicates are satisfiable (a sorry-free check accompanies the drafts); LinUCB is a closed form whose maximality over the confidence ellipsoid is itself a milestone, not a real supremum; and the noise CDF is pinned by $\mathbb P(z_t \le c) = F(c)$ .

A complete development needs the PLB analysis (Lemmas S3, S5, 3), which is reusable for any linear bandit with one-sparse actions, and the conditional Hoeffding step for Lemma 1, for which a platform theorem exists. Proofs of any milestone, and reusable lemmas on ridge estimates with diagonal designs, are welcome.

Selected references

Y. Luo, W. W. Sun, Y. Liu, Distribution-Free Contextual Dynamic Pricing, Mathematics of Operations Research, 2024; arXiv:2109.07340v2. https://arxiv.org/abs/2109.07340 , https://doi.org/10.1287/moor.2023.1369
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (Lemma 19.4, Theorem 20.4). https://doi.org/10.1017/9781108571401
Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS, 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
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

17 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Modern Introduction to Online Learning VII: The Perceptron's Mistakes Exceed the Competitor's Hinge-Power Loss by at Most q²R²‖u‖²/2 + qR‖u‖√(q²R²‖u‖²/4 + L_q)Textbook

Motivation

An online classifier must predict a label before learning the correct answer. Its errors matter directly: a low numerical loss is useful only if it controls the number of wrong predictions. Chapter 8 of Orabona's textbook examines this connection for linear classification, where a vector of weights produces a score by taking an inner product with the incoming example. The Perceptron is a particularly spare example: it changes its weights only after a mistake, and it needs no learning rate or chosen comparator. This makes its guarantee a useful point of contact between classification mistakes and the convex losses used elsewhere in online optimization.

Theorem 8.2 compares the Perceptron's mistake count with a whole family of comparator losses, indexed by a real exponent $q\ge1$ . The theorem is a known result in the book, not an unsolved conjecture. The mission concerns a faithful Lean statement and, subsequently, its machine-checked proof. The distinction matters because other Perceptron bounds on the platform address batch separability, multiclass prediction, or a hinge loss only on update rounds; those results do not state this theorem with its constants and quantifiers.

Setting

Fix a dimension $d$ and a sequence of feature vectors $z_t\in\mathbb R^d$ with binary labels $y_t\in\{-1,1\}$ , for rounds $t=1,\ldots,T$ . The Perceptron begins at $x_1=0$ . At round $t$ it predicts $\widetilde y_t=\operatorname{sign}(\langle z_t,x_t\rangle)$ , where $\operatorname{sign}(0)=0$ . It records a mistake when $y_t\widetilde y_t\le0$ and, on exactly those rounds, adds $y_tz_t$ to its weights. Write $\tau_t=\mathbf 1\{y_t\widetilde y_t\le0\}$ and $M=\sum_{t=1}^T\tau_t$ . A zero score is a mistake even though it is not a strict sign disagreement.

For a score $m\in\mathbb R$ , a label $y\in\{-1,1\}$ , and a real power $q\ge1$ , the hinge-power loss is $\ell_q(m,y)=\max(1-ym,0)^q$ . A fixed competitor $u\in\mathbb R^d$ has cumulative loss $L_q(u)=\sum_{t=1}^T\ell_q(\langle z_t,u\rangle,y_t)$ . The loss is zero when $u$ gives every example the correct sign with margin at least one. The book assumes the input vectors obey $\|z_t\|_2\le R$ ; $R$ is a nonnegative radius. The sequence is arbitrary, so the result includes examples chosen with knowledge of earlier predictions.

Formalization targets

Perceptron mistake guarantee

The goal is Theorem 8.2, p. 144 of Orabona. For every $u\in\mathbb R^d$ and every real $q\ge1$ ,

M-L_q(u)\le\frac{q^2R^2\|u\|_2^2}{2} +qR\|u\|_2\sqrt{\frac{q^2R^2\|u\|_2^2}{4}+L_q(u)}.

All constants and the full family of powers are part of the target. For a competitor with $L_q(u)=0$ , choosing $q=1$ yields the finite mistake bound $M\le R^2\|u\|_2^2$ , as the book explains on p. 144. For a nonseparable sequence, the same statement measures mistakes relative to the competitor's nonzero loss.

Milestone statements

The milestone list follows the book's named ingredients: Lemma 4.29 converts an implicit square-root inequality into an explicit one; the constant-step clause of Theorem 2.13 gives the linear-loss gradient bound; and displays (8.4) and (8.5) relate the Perceptron updates to the comparator and to the hinge loss. Theorem 2.13 is stated in the linear, whole-space case used on p. 145. The printed (8.4) has an invalid extra term on its left; the milestone retains the printed text for provenance, while the Lean statement gives the valid comparator inequality used by (8.5). The correction is described in the item and moderation notes.

Significance

The guarantee answers a practical question about a simple online rule: how many classification errors can it make when a fixed linear predictor has small convex loss? The answer has explicit dependence on the feature radius, comparator norm, loss exponent, and comparator loss. It contains the separable margin case and also applies when no comparator classifies every example with margin one. The quantifier over all $u$ permits a later analyst to choose a competitor after seeing the sequence without changing the algorithm or the theorem.

A complete formalization would provide a reusable account of a deterministic online classifier, its exact zero-score convention, and the passage from update counts to a family of hinge losses. The local Lean declarations currently compile as statements with proof placeholders; compilation does not establish the mathematical inequalities. A proof of the goal and milestones remains to be supplied and checked. In particular, the correction to (8.4) should be made explicit in any downstream development so that later results never depend on the false printed left side.

Difficulty

The mistake count is discontinuous in the prediction score, while the competitor is measured by a smooth family of convex surrogates. A direct comparison of their per-round losses does not give the theorem's constants. The update rule also depends on its own current score, so its condition must be tied to the weight sequence generated by earlier rounds. Treating the update indicators as free variables, or counting only rounds with a strictly negative score, changes the statement.

The book's proof passes through an implicit inequality involving $\sqrt M$ . That relation alone is weaker than the displayed goal until its constants and nonnegative domains are handled precisely. Real powers require special attention at a zero hinge value. The printed (8.4) introduces an additional difficulty: with $u=0$ and two one-dimensional examples $z_1=1$ , $z_2=-1$ carrying positive labels, its left side is positive while its right side is zero. The valid comparator inequality has to be distinguished from that printed display.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$ , its Euclidean inner product and norm, and sequences indexed by natural numbers with active rounds $1,\ldots,T$ . Index zero carries no data requirement. A total recursive definition fixes $x_1=0$ and every later Perceptron update. Mathlib's Real.sign supplies $\operatorname{sign}(0)=0$ ; an indicator records both a wrong sign and a zero score. The comparator loss uses a maximum with zero before taking a real power. No probability space is needed because Algorithm 8.2 is deterministic.

The Lean theorems explicitly require binary labels on the active rounds, $q\ge1$ for the goal, $R\ge0$ , and $\|z_t\|_2\le R$ . They allow $T=0$ , $d=0$ , and $R=0$ ; the formulas remain meaningful in these cases. The set $X$ in the book's theorem is omitted because the assertion uses only the given feature sequence and its norm bound. The constant-step milestone requires $\eta>0$ because its formula divides by $\eta$ . The definitions include a mistake count, hinge-power loss, cumulative comparator loss, and the fixed algorithm; the theorem layer can reuse Mathlib's inner-product and real-analysis results. Contributions toward these statements, the algebraic milestone, or the full theorem proof are in scope. A run that can skip a zero-score update or whose iterates are chosen independently of the recursion is outside this mission.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 8, pp. 141–146; Lemma 4.29, p. 45; Theorem 2.13, p. 13. arXiv PDF.

8 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Modern Introduction to Online Learning III: Adaptive Online Subgradient Descent on s-Self-Bounded Losses Has Regret 4sD² + 2D√(s Σ_t ℓ_t(u))Textbook

Motivation

In online convex optimization, a learner selects a point before seeing the current loss. A useful guarantee compares the learner's accumulated loss with that of a single fixed point chosen in hindsight. A step size chosen from a preannounced bound on all future gradients can be wasteful when the realized gradients are small. Chapter 4 of Orabona's online learning text studies step sizes determined from the gradients observed so far. Its adaptive online subgradient descent bound uses the actual sum of squared subgradient norms, without requiring that sum in advance (Theorem 4.14, p. 40).

The chapter then asks for a more informative guarantee when the losses have small values at a good competitor. For self-bounded losses, a small loss at a point limits the size of its subgradients. Theorem 4.30 on p. 45 turns that relation into a bound in terms of the competitor's cumulative loss. This is useful for problems such as the squared hinge loss discussed immediately after the theorem: if one feasible comparator has zero loss on every round, the regret bound becomes independent of the number of rounds. These are known textbook results. The goal here is a machine-checked formulation and, eventually, a proof of the stated constants.

Setting

Fix a finite horizon $T\ge1$ and a nonempty, closed, convex decision set $V\subseteq\mathbb R^d$ . Its Euclidean diameter is at most $D$ : every $a,b\in V$ satisfy $\|a-b\|_2\le D$ . In round $t\in\{1,\ldots,T\}$ , the learner plays $x_t\in V$ and receives a convex loss $\ell_t$ . The loss sequence is arbitrary. A subgradient $g_t$ of $\ell_t$ at $x_t$ satisfies $\ell_t(y)\ge\ell_t(x_t)+\langle g_t,y-x_t\rangle$ for every $y\in\mathbb R^d$ . The regret against a fixed competitor $u\in V$ is

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

The learner uses projected online subgradient descent. After observing $g_t$ , it sets

\eta_t=\frac{\sqrt2D}{2\sqrt{\sum_{i=1}^{t}\|g_i\|_2^2}}, \qquad x_{t+1}=\Pi_V(x_t-\eta_tg_t)

when $g_t\ne0$ . If $g_t=0$ , the algorithm leaves $x_{t+1}=x_t$ . Here $\Pi_V$ is a Euclidean nearest point in $V$ . The current gradient appears in the sum defining $\eta_t$ because the update is made after that gradient is observed. The initial point $x_1$ is any member of $V$ , and every admissible choice of subgradient is allowed.

A loss $f$ is $s$ -self-bounded on $V$ when it is bounded below, has a subgradient at each point of $V$ , and every subgradient $g$ at every $x\in V$ satisfies

\|g\|_2^2\le 2s\left(f(x)-\inf_{y\in\mathbb R^d}f(y)\right).

The infimum is over the whole ambient space. The target theorem additionally assumes that each loss is nonnegative everywhere. The $s$ in these formulas is nonnegative. These conventions follow Definition 4.26 and Theorem 4.30 of the pinned preprint.

Formalization targets

Adaptive gradient bound

The first milestone is Theorem 4.14. Under the setting above, for every $u\in V$ ,

\operatorname{Regret}_T(u)\le D\sqrt{2\sum_{t=1}^{T}\|g_t\|_2^2}.

This bound depends on the gradient sequence encountered by the algorithm. The printed theorem also equates this expression with a minimum over constant positive step sizes. At zero accumulated gradient energy that minimum is an unattained infimum, so the formal milestone states the regret inequality in every case and the identity with the minimum only when the accumulated squared gradient norm is positive.

Self-bounded loss bound

The goal is Theorem 4.30. If every loss is nonnegative, convex, and $s$ -self-bounded on $V$ , then for every fixed $u\in V$ ,

\operatorname{Regret}_T(u) \le 4sD^2+2D\sqrt{s\sum_{t=1}^{T}\ell_t(u)}.

The target includes the intermediate displayed bound on p. 45 and Lemma 4.29 as milestones. Their statements capture the passage from a regret bound involving the learner's cumulative loss to one involving the competitor's cumulative loss. The constants $4$ and $2$ are those printed in the theorem; the goal does not replace them with asymptotic notation.

Significance

Theorem 4.14 provides a guarantee without supplying a gradient bound or the horizon-dependent sum of squared gradients to the learner. Theorem 4.30 sharpens the interpretation when the losses are self-bounded: for a comparator with $\sum_t\ell_t(u)=0$ , the regret is at most $4sD^2$ . For larger comparator losses, the bound changes continuously with their accumulated value. The guarantee holds against each competitor, not merely one selected by an infimum over $V$ .

A formal development would make the algorithm's timing, its zero-gradient branch, the ambient-space infimum, and the exact numerical constants explicit. These details are reusable in later analyses of adaptive step sizes and small-loss bounds. The proposal contains open Lean theorem statements and a compiled definitions file; it does not claim that these results already have machine-checked proofs in this mission. The metric projection relation is reused from an existing published definition, and the intended work is proving the open statements and developing their supporting inequalities.

Difficulty

A fixed step size can be selected after looking at all gradients, but that selection does not define an online update. The adaptive step size must use only gradients observed through the current round. The zero-gradient case needs an explicit update rule because its displayed quotient has a zero denominator on an all-zero prefix. These issues already appear in the first milestone.

For the goal, the self-bounded inequality controls subgradient norms using loss at the learner's own points. Substituting that control into the gradient bound yields a right-hand side containing $\sum_t\ell_t(x_t)$ , although the desired statement is expressed using $\sum_t\ell_t(u)$ . The intermediate estimate on p. 45 is therefore implicit. The square-root inequality of Lemma 4.29 supplies the separate arithmetic statement needed to express the final result with the printed constants. A direct substitution that treats the learner's loss as the competitor's loss would not justify the theorem.

Formalization scope

The Lean carrier is EuclideanSpace ℝ (Fin d), including dimension zero; the theorem remains valid there. Rounds are indexed from one, with index zero unused, and sums range over Finset.Icc 1 T. The loss functions are real-valued on the whole Euclidean space. The book permits extended-real losses that take $+\infty$ outside their domain; this formalization addresses the real-valued case. Full-space subgradients retain the source's definition. Convexity and nonnegativity hold on the whole Euclidean space, and self-boundedness holds at every feasible point, for each round through $T$ .

The adaptive run is a relation covering every legal selection of subgradients and projections. It requires the update after every nonzero gradient and the unchanged point after a zero gradient. The closed, convex, nonempty set assumptions ensure that Euclidean projection is meaningful. The diameter condition is written as $\|a-b\|_2\le D$ for all feasible $a,b$ , so it also covers any valid upper bound on the diameter. Self-boundedness uses the real infimum of the full range of each loss, together with boundedness below; global nonnegativity in the goal guarantees that condition. The explicit $T\ge1$ and $s\ge0$ conditions prevent boundary values from silently changing the meaning of a quotient or a square root.

The goal must hold for every comparator $u\in V$ and every admissible run. A definition that checks self-boundedness only at $u$ , or permits arbitrary next decisions, would lose the algorithmic guarantee. The reusable components are the regret and gradient-energy definitions, the adaptive run relation, the self-boundedness predicate, and the scalar inequality in Lemma 4.29. Contributions that establish the projection analysis and the three listed milestones directly support the goal.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 4, pp. 34–49. arXiv

7 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Modern Introduction to Online Learning I: Projected Online Gradient Descent Has Regret D²/(2η_T) + Σ_t η_t‖g_t‖²/2Textbook

Why online gradient descent matters

In online learning, a decision is made before the loss for that round is revealed. The learner cannot optimize a known objective once and use its minimizer forever: the sequence of objectives may be arbitrary. A basic performance measure is regret, the learner's total loss minus the loss of one fixed decision chosen with hindsight. A regret bound that grows more slowly than the number of rounds shows that the learner's average excess loss vanishes. Orabona's introduction develops this measure and derives a bound for projected online gradient descent without requiring advance knowledge of the loss sequence (Orabona, Chapter 1 and Theorem 2.13).

The result is useful because it separates the geometry of the feasible set from the size of the gradients seen during play. It also supports step sizes that change with time, which matters when a learner adjusts its updates as more rounds pass. The exact endpoint term in the theorem records information that would be discarded by a coarser regret estimate (Orabona, Theorem 2.13 and the discussion on p. 14).

Decisions, losses, and projection

Let $V$ be a nonempty closed convex set in a real inner-product space. At round $t=1,\ldots,T$ , the learner chooses $x_t\in V$ , receives a differentiable convex loss function $\ell_t$ , and incurs $\ell_t(x_t)$ . For a fixed competitor $u\in V$ , the book's regret is

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

The competitor stays fixed through all $T$ rounds; it is not the best separate decision for each round. The losses may differ on every round, and their sequence is arbitrary (Orabona, p. 2).

A metric projection $\Pi_V(z)$ is a point of $V$ nearest to $z$ in Euclidean distance. Convexity makes the projection single valued when $V$ is nonempty and closed. Projected online gradient descent, Algorithm 2.1, starts from an arbitrary $x_1\in V$ , chooses positive step sizes $\eta_t$ , forms $g_t=\nabla\ell_t(x_t)$ , and sets

x_{t+1}=\Pi_V(x_t-\eta_t g_t).

The projection keeps the next decision feasible even when the unconstrained gradient step leaves $V$ (Orabona, Algorithm 2.1, p. 12). The first-order optimality condition of Theorem 2.8, the projection inequality of Proposition 2.11, and the one-round inequality of Lemma 2.12 are the numbered milestones leading to the main statement. Lemma 2.31 records the parallel one-round statement for subgradients (Orabona, pp. 11–13, 19).

Formalization targets

For $V$ of finite diameter $D=\sup_{x,y\in V}\|x-y\|_2$ , positive nonincreasing step sizes, and any $u\in V$ , the main target is the complete first inequality of Theorem 2.13:

\operatorname{Regret}_T(u)\le \frac{D^2}{2\eta_T} +\sum_{t=1}^{T}\frac{\eta_t}{2}\|g_t\|_2^2 -\frac{\|x_{T+1}-u\|_2^2}{2\eta_T}.

The negative terminal term is part of the target. The constant-step clause of the same theorem is a separate companion item. If $\eta_t=\eta>0$ on every round, it states

\operatorname{Regret}_T(u)\le \frac{\|u-x_1\|_2^2}{2\eta} +\frac{\eta}{2}\sum_{t=1}^{T}\|g_t\|_2^2 -\frac{\|x_{T+1}-u\|_2^2}{2\eta}.

This clause has no finite-diameter hypothesis, so it applies on unbounded feasible sets as well (Orabona, Theorem 2.13, p. 13).

What the bound supplies

The theorem gives a deterministic guarantee against every fixed feasible competitor, for every loss sequence and every valid run of the algorithm. It exposes the cumulative effect of the gradient magnitudes and the step sizes. Its constant-step form uses the distance from the initial decision to the comparator rather than the diameter of the whole set. The bound is therefore informative on some unbounded sets where the diameter term has no finite value (Orabona, Theorem 2.13 and p. 14).

This is a known textbook theorem, not an open conjecture. The mission asks for machine-checked proofs of the source statements in a reusable Lean interface: a fixed-comparator regret definition, a finite-horizon run predicate, and the projection and one-step results. The published metric-projection predicate is reused, while the one-based regret and run definitions are specific to this book's convention.

Where the argument is delicate

An immediate attempt to sum the one-round estimate leaves squared-distance terms with different coefficients when the step size varies. They do not cancel as they would with a fixed coefficient. The theorem's monotonicity condition on the step sizes and the finite diameter of $V$ are what make a uniform bound possible; omitting either changes the first displayed claim. Keeping the final negative squared-distance term also requires more care than proving only the weaker bound obtained by dropping it. On the nonsmooth side, an arbitrary vector cannot replace a subgradient: its defining inequality supplies the link between a loss difference and the linearized direction (Orabona, Lemmas 2.12 and 2.31, Theorem 2.13).

Formalization scope

Lean uses a complete real inner-product space, covering the book's $\mathbb R^d$ and using only the geometry needed by this chapter. Time remains one based: round zero is unused, sums run from $1$ through $T$ , and the output after the last round is $x_{T+1}$ . The horizon satisfies $T\ge1$ , so the last step size and the terminal iterate are part of an actual run. The run predicate requires a gradient and a metric projection at every round through $T$ ; it does not select a favorable projection after seeing the comparator. The theorem requires each loss to be convex and differentiable on an open neighborhood containing $V$ , as in Algorithm 2.1.

The diameter in the main target is Mathlib's real Metric.diam V, with boundedness imposed so that it is the finite supremum in the book. The constant-step clause has no boundedness requirement. The projection relation is the published OnlineConvexOpt.FirstOrder.IsMetricProjection: it includes membership in $V$ and minimal distance to the point being projected. Thus, the update cannot be satisfied by an arbitrary point of $V$ . Every regret claim quantifies over a comparator $u\in V$ ; extending the quantifier outside $V$ would assert a different result.

For Lemma 2.31, losses are real valued on $V$ , and the stated subgradient inequality is relative to $V$ . The book defines a full-space subgradient for an extended-real-valued function; every such subgradient gives the relative inequality used here. This is the precise convention for that milestone and is disclosed in its item description. Contributions that establish the projection inequality, the single-round inequalities, and either complete form of Theorem 2.13 fit the mission. The regret and run definitions can be reused in later deterministic online optimization results, while the projection predicate is already shared with another textbook development.

Selected references

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

7 thms4 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Operations Research·Captain: mikedeng1

Fast Convergence of Regularized Learning in Games I: If Every Player Runs Optimistic FTRL with Step Size 1/(2(n−1)), the Sum of All Players' Regrets Is at Most 2n(n−1)RResearch Paper

Motivation

When the players of a game repeatedly adjust their strategies with no-regret learning algorithms, the empirical distribution of play converges to a coarse correlated equilibrium, and in smooth games the average social welfare approaches the price-of-anarchy guarantee of the game (Roughgarden 2009). For generic no-regret algorithms such as Hedge the convergence rate is $O(1/\sqrt T)$ , because each player's regret after $T$ rounds is of order $\sqrt T$ in the worst case, against an adversary.

Other players are not adversaries: they are also learning, and their strategies change slowly. Syrgkanis, Agarwal, Luo and Schapire (NIPS 2015, arXiv:1507.00407v5) identify a property of learning algorithms, regret bounded by variation in utilities (RVU), under which this predictability can be exploited in general multi-player games, and show that a natural class of algorithms has it. This mission formalizes their first main consequence: if every player uses optimistic follow the regularized leader (OFTRL), the sum of all players' regrets stays bounded by a constant independent of $T$ , so the average welfare converges at rate $O(1/T)$ .

Timeline. Rakhlin and Sridharan (COLT 2013; NIPS 2013) introduced optimistic mirror descent and showed $O(\log T / T)$ convergence to the minimax value in two-player zero-sum games when both players use it. Syrgkanis et al. (2015) extend the fast-rate phenomenon to general $n$ -player games and arbitrary no-regret algorithms with the RVU property (Theorem 4), and establish RVU for OFTRL (Proposition 7), giving Corollary 8.

Setting

A game has $n$ players. Each player $i$ has a finite strategy set $S_i$ with $|S_i| = d$ , and a utility $u_i(s) \in [0,1]$ for each pure profile $s = (s_1, \dots, s_n)$ . A mixed strategy is a point $w_i$ of the probability simplex $\Delta = \Delta(S_i) \subset \mathbb R^d$ , and a mixed profile $w = (w_1, \dots, w_n)$ induces the product distribution on pure profiles.

The game is played for $T$ rounds. At round $t$ each player picks $w_i^t \in \Delta$ and then observes the utility vector $u_i^t \in \mathbb R^d$ with entries

u^t_{i,x} = \mathbb E_{s_{-i}\sim w^t_{-i}}\big[u_i(x, s_{-i})\big], \qquad x \in S_i ,

so that $\langle w_i^t, u_i^t\rangle$ is the expected utility of player $i$ at round $t$ . The regret of player $i$ is

r_i(T) = \sup_{w^* \in \Delta} \sum_{t=1}^T \langle w^* - w_i^t, u_i^t\rangle .

The primal norm is $\|v\| = \|v\|_1$ and its dual is $\|v\|_* = \|v\|_\infty$ . A regularizer $\mathcal R : \Delta \to \mathbb R$ is 1-strongly convex if $\mathcal R(\tfrac{a+b}{2}) \le \tfrac{\mathcal R(a) + \mathcal R(b)}{2} - \tfrac{\|a-b\|_1^2}{8}$ for all $a, b \in \Delta$ , and $R$ denotes a bound on its range, $\mathcal R(f) - \mathcal R(g) \le R$ on $\Delta$ . Optimistic FTRL with step size $\eta > 0$ and predictors $M^t_i$ plays $w_i^0 = \operatorname{argmin}_\Delta \mathcal R$ and, for $T \ge 1$ ,

w_i^T \in \operatorname*{argmax}_{w \in \Delta}\ \Big\langle w, \sum_{t=1}^{T-1} u_i^t + M_i^T\Big\rangle - \frac{\mathcal R(w)}{\eta}.

With one-step recency bias, $M_i^T = u_i^{T-1}$ : the algorithm bets that the next utility vector equals the last one.

An algorithm has the RVU property with constants $\alpha > 0$ , $0 < \beta \le \gamma$ if for every utility sequence

\sum_{t=1}^T\langle w^* - w^t, u^t\rangle \le \alpha + \beta\sum_{t=1}^T \|u^t - u^{t-1}\|_*^2 - \gamma \sum_{t=1}^T \|w^t - w^{t-1}\|^2 .

Formalization targets

Goal: Corollary 8

If every player runs OFTRL with $M_i^t = u_i^{t-1}$ and $\eta = 1/(2(n-1))$ , $n \ge 2$ , then for every $T$

\sum_{i} r_i(T) \le \frac{nR}{\eta} = 2n(n-1)R .

Milestones

Theorem 19 (supp. p. 3): the regret of OFTRL with any predictor sequence is at most $R/\eta + \sum_t \|u^t - M^t\|_*\|w^t - g^t\| - \frac{1}{2\eta}\sum_t(\|w^t - g^t\|^2 + \|w^t - g^{t-1}\|^2)$ , where $g^t$ is the leader sequence.
Lemma 20 (supp. p. 4): $\|w^t - g^t\| \le \eta\|M^t - u^t\|_*$ and $\|g^t - w^{t+1}\| \le \eta\|M^{t+1}\|_*$ .
Proposition 7 (p. 5): OFTRL with $M^t = u^{t-1}$ has RVU with $\alpha = R/\eta$ , $\beta = \eta$ , $\gamma = 1/(4\eta)$ .
Display (2) (p. 4): $\|u_i^t - u_i^{t-1}\|_*$ is at most the total variation between the opponents' product distributions, which is at most $\sum_{j \ne i}\|w_j^t - w_j^{t-1}\|_1$ .
The variation bound (p. 4): $\sum_i \|u^t_i - u^{t-1}_i\|_*^2 \le (n-1)^2 \sum_i \|w_i^t - w_i^{t-1}\|_1^2$ .
Theorem 4 (p. 4): if every player satisfies RVU with $\beta \le \gamma/(n-1)^2$ and $\|\cdot\| = \|\cdot\|_1$ , then $\sum_i r_i(T) \le \alpha n$ .

A companion statement, Proposition 2 (p. 3), turns a regret bound into a welfare bound in a $(\lambda,\mu)$ -smooth game: $\frac1T\sum_t W(w^t) \ge \frac{\lambda}{1+\mu}\mathrm{OPT} - \frac{1}{1+\mu}\frac1T\sum_i r_i(T)$ .

Significance

Corollary 8 says that uncoupled learning dynamics, in which each player sees only its own utility vectors, can keep the total regret of all players bounded by a constant in an arbitrary finite game. By Proposition 2 this gives $O(1/T)$ convergence of the average welfare to the price-of-anarchy bound in smooth games, against $O(1/\sqrt T)$ for generic no-regret algorithms. The RVU framework has since become a standard tool in the analysis of optimistic learning in games, and Theorem 4 decouples the game-level argument from the choice of algorithm.

The paper's proofs are in its supplementary material (App. A and C). None of the results here has a machine-checked proof to our knowledge. A complete formalization produces a reusable layer: utility vectors of mixed profiles, total-variation subadditivity for finite product distributions, and the regret analysis of optimistic FTRL under an $\ell_1$ -strongly convex regularizer.

Difficulty

The game-level step (Theorem 4) is short once display (2) is available, but (2) itself, subadditivity of total variation over products of $n-1$ finite distributions, is not available in Mathlib in this form.

The core is the single-player analysis. Theorem 19 and Lemma 20 compare the iterates with the leader sequence, an object the algorithm never computes, and both rest on the quadratic-growth fact that a maximizer $w$ of a $1/\eta$ -strongly concave function $F$ satisfies $F(w) \ge F(g) + \frac{1}{2\eta}\|w - g\|^2$ . Footnote 3's midpoint inequality does not give the constant $\frac{1}{2\eta}$ in a single application; it has to be upgraded to the standard form of strong convexity first.

Formalization scope

Players are Fin n, strategies Fin d; time keeps the paper's indices $t = 1, \dots, T$ with $w^0$ and $u^0$ . $u_i^0$ is the utility vector against $w^0_{-i}$ , the formula of p. 2 at $t = 0$ , which the paper uses but never writes. Mixed profiles and expectations come from the published definition agt_games. $\|\cdot\|_1$ is defined explicitly and $\|\cdot\|_*$ is Mathlib's sup norm. Regret and $R$ are never written as suprema: a bound on $\sum_i r_i(T)$ is stated for every profile of comparators in $\Delta$ , and $R$ is any upper bound on the range of every regularizer.

Added hypotheses, each disclosed in its statement:

each regularizer is continuous on $\Delta$ , which makes footnote 3 equivalent to standard strong convexity;
$n \ge 2$ in the goal;
Theorem 4's condition is written as $\beta(n-1)^2 \le \gamma$ , so $n = 1$ involves no division by zero;
RVU is assumed in Theorem 4 only on the realized play, a weaker hypothesis than the paper's;
$T \ge 1$ and $1 + \mu > 0$ in Proposition 2;
per-player regularizers $\mathcal R_i$ (footnote 2).

Theorem 19, Lemma 20 and Proposition 7 are stated for $\ell_1$ ; the paper allows any norm.

OFTRL is an argmax predicate, so the goal holds for every trajectory the dynamics can produce, not for a chosen one. It is not the entropic closed form (Optimistic Hedge). The utility bound $u_i \in [0,1]$ is kept, since the game-level statements are false without it. A sanity file shows that $\mathcal R(w) = \frac d2\sum_x w_x^2$ satisfies the strong-convexity hypothesis and that OFTRL runs exist, so the hypotheses are satisfiable.

Contributions are welcome for each milestone. The quadratic-growth lemma for midpoint strongly convex continuous functions on the simplex and the total-variation bound for products are reusable beyond this mission.

Selected references

V. Syrgkanis, A. Agarwal, H. Luo, R. E. Schapire, Fast Convergence of Regularized Learning in Games, NIPS 2015. arXiv:1507.00407v5. https://arxiv.org/abs/1507.00407
A. Rakhlin, K. Sridharan, Online Learning with Predictable Sequences, COLT 2013. https://arxiv.org/abs/1208.3728
A. Rakhlin, K. Sridharan, Optimization, Learning, and Games with Predictable Sequences, NIPS 2013. https://arxiv.org/abs/1311.1869
T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, STOC 2009. https://doi.org/10.1145/1536414.1536485

9 thms4 active usersReviewed

Bandit Algorithms Probability Reinforcement Learning·Captain: mikedeng1

Provably Efficient Reinforcement Learning with Linear Function Approximation 2: LSVI-UCB Has Regret O(√(d³H³Tι²) + ζdHT√ι) on ζ-Approximately Linear MDPsResearch Paper

Motivation

Reinforcement learning with large or continuous state spaces relies on function approximation: value functions are represented as functions of a $d$ -dimensional feature map instead of tables indexed by states. Before 2019, regret guarantees for exploration with function approximation either needed strong assumptions (deterministic dynamics, a generative model) or applied only to tabular problems. Jin, Yang, Wang and Jordan (arXiv:1907.05388, COLT 2020) showed that in a linear MDP, where transitions and rewards are linear in known features, an optimistic version of least-squares value iteration, LSVI-UCB, has regret $\tilde O(\sqrt{d^3H^3T})$ , with no dependence on the number of states or actions (Theorem 3.1).

Exact linearity is rarely satisfied by features chosen in practice. A guarantee that collapses under a small modelling error would say little about real use, and a naive adaptation of linear-bandit methods can break down entirely when the model is wrong. Theorem 3.2 of the same paper addresses this: if the MDP is only $\zeta$ -approximately linear, LSVI-UCB with an episode-dependent bonus still has sublinear regret plus an additive term linear in $\zeta T$ . This mission formalizes that result. A companion mission formalizes Theorem 3.1.

Setting

An episodic MDP has a measurable state space $\mathcal S$ , a finite action set $\mathcal A$ , a horizon $H$ , and for each step $h\in[H]$ a transition kernel $\mathbb P_h(\cdot\mid x,a)$ and a reward $r_h:\mathcal S\times\mathcal A\to[0,1]$ . A policy $\pi$ chooses an action $\pi(x,h)$ at state $x$ and step $h$ . Its value functions satisfy the Bellman equation

Q^\pi_h(x,a)=r_h(x,a)+\int V^\pi_{h+1}\,\mathrm d\mathbb P_h(\cdot\mid x,a),\qquad V^\pi_h(x)=Q^\pi_h(x,\pi(x,h)),\qquad V^\pi_{H+1}=0,

and $V^\star_h(x)=\max_aQ^\star_h(x,a)$ is the optimal value, with $Q^\star$ defined by the same recursion.

A feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ with $\|\phi\|\le1$ makes the MDP $\zeta$ -approximately linear (Assumption B) if for every step $h$ there are signed measures $\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ on $\mathcal S$ and a vector $\theta_h$ with

\big\|\mathbb P_h(\cdot\mid x,a)-\langle\phi(x,a),\mu_h(\cdot)\rangle\big\|_{\mathrm{TV}}\le\zeta,\qquad|r_h(x,a)-\langle\phi(x,a),\theta_h\rangle|\le\zeta

for all $(x,a)$ , together with the normalization $\|\theta_h\|\le\sqrt d$ and a $\sqrt d$ bound on the masses of $\mu_h$ . At $\zeta=0$ this is a linear MDP.

LSVI-UCB (Algorithm 1) plays $K$ episodes. In episode $k$ , with data $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$ from earlier episodes, it computes backwards from $Q^k_{H+1}\equiv0$

\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I,\qquad w^k_h=(\Lambda^k_h)^{-1}\sum_{\tau<k}\phi^\tau_h\big[r_h(x^\tau_h,a^\tau_h)+\max_aQ^k_{h+1}(x^\tau_{h+1},a)\big],

Q^k_h(x,a)=\min\big\{\langle w^k_h,\phi(x,a)\rangle+\beta_k\|\phi(x,a)\|_{(\Lambda^k_h)^{-1}},\,H\big\},

and then acts greedily, $a^k_h=\arg\max_aQ^k_h(x^k_h,a)$ . An adversary may choose each initial state $x^k_1$ . The regret after $K$ episodes is

\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],

where $\pi_k$ is the greedy policy of episode $k$ . Throughout, $T=KH$ and $\iota=\log(2dT/p)$ .

Formalization targets

Goal: Theorem 3.2

There are absolute constants $c,C>0$ such that for every $\zeta$ -approximately linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta_k=c\,(d\sqrt\iota+\zeta\sqrt{kd})H$ , with probability at least $1-p$ ,

\mathrm{Regret}(K)\le C\Big(\sqrt{d^3H^3T\iota^2}+\zeta dHT\sqrt\iota\Big).

The constants are not fixed numerically, so improvements of the constants in the proof do not invalidate the target.

Milestones

The milestones follow Appendix C: the approximate linearity of $Q^\pi$ (Lemma C.1) and the bound on its weights (Lemma C.2); the trace inequality D.1 and the adversarial-noise bound C.4; the self-normalized concentration bound D.3 (published) and the concentration event of Lemma C.3; the key estimate C.5; approximate optimism C.6; the recursive formula C.7; and the elliptical potential lemma D.2 (published) with the bonus-sum bound (21)–(24).

Significance

Theorem 3.2 shows that the regret of LSVI-UCB degrades gracefully under misspecification: the extra cost is of order $\zeta dHT\sqrt\iota$ , linear in $T$ because of the bias of linear approximation and negligible when $\zeta\lesssim1/\sqrt T$ . The paper also converts it into a PAC guarantee with an additive $\tilde O(\zeta dH^2)$ error. It is a reference point for later work on misspecified linear bandits and RL, which asks how far the linear term can be improved.

The result is proved on paper; no machine-checked proof is known. The formalization supplies an episodic MDP on a general measurable state space, LSVI-UCB as a function of the observed data, and its interaction with an adaptive adversary on a filtered probability space. These are shared with the companion mission on Theorem 3.1 and are reusable for other optimistic algorithms with linear function approximation. At $\zeta=0$ the goal specializes to Theorem 3.1 under the same normalization; this is a consistency check, not a dependency.

Difficulty

The central difficulty is that the regression targets $r_h+V^k_{h+1}(x^\tau_{h+1})$ depend on the data through $V^k_{h+1}$ , which is computed from all earlier episodes. A martingale concentration bound for a fixed function does not apply. Lemma C.3 needs a bound that holds uniformly over the class of functions LSVI-UCB can produce, which requires a covering-number argument whose size depends on $\beta_k$ ; that is why the constant $C$ must be independent of $c_\beta$ and $c_\beta$ is chosen afterwards. Under misspecification a second error appears: the deviations $r_h-\langle\phi,\theta_h\rangle$ and $(\mathbb P_h-\langle\phi,\mu_h\rangle)V$ are not mean-zero and can be adversarial, so they cannot be concentrated away. Lemma C.4 absorbs them into the bonus at the price of the $\zeta\sqrt{kd}$ term in $\beta_k$ . Optimism then holds only up to an error that accumulates over the horizon (Lemma C.6).

Formalization scope

Indices are 1-based, as on the page; values and estimates are $0$ outside $1\le h\le H$ .
Values: $V^\pi$ and $V^\star$ are defined by the Bellman recursions (1) and (2), not by $\sup_\pi$ .
Measurability: the state space is a bare measurable space. Features $\phi(\cdot,a)$ are assumed measurable, and lemmas about a policy $\pi$ assume it measurable, so that every integral is meaningful.
Actions: $\mathcal A$ is finite and nonempty. Argmax ties are broken towards the least action of a fixed linear order on $\mathcal A$ .
Interaction: the run is a process adapted to an arbitrary filtration, with actions given by Algorithm 1 and the next-state law holding conditionally on the past. The initial states are only required to be adapted.
Probability statements: "with probability $1-p$ " is "the bad set has (outer) measure at most $p$ ".
Constants: $c$ and $C$ are quantified before all types, dimensions, horizons, $\zeta$ , $p$ and runs. The hypotheses $d,H,K\ge1$ and $0\le\zeta\le1$ are stated.
Assumption B measures the TV distance by the total variation norm $|\nu|(\mathcal S)$ . The page's normalization $\|\mu_h(\mathcal S)\|\le\sqrt d$ is replaced by the same bound on the vector of total variations $(|\mu_h^{(i)}|(\mathcal S))_i$ , because Lemma C.2 is false under the printed form; the replacement implies the printed condition and holds for tabular MDPs.
Lemma C.7 carries the $+4H\zeta$ term that its own proof derives; the printed statement omits it. Theorem 3.2 is unaffected.

Lemmas C.3 and C.5 are formalized as printed. Their proofs use $\sup_x|V^k_{h+1}(x)|\le H$ , which Algorithm 1 does not enforce from below; a solver may find that one of them needs an additional argument.

A formalization in which the goal assumes the event $\mathfrak E$ , the optimism of Lemma C.6 or the recursion of Lemma C.7, or in which the run does not fix the actions to Algorithm 1's, would be trivial or false; the goal assumes none of these. Contributions are welcome on the linear-algebra lemmas (D.1, C.4, (21)–(24)), on measurability of the LSVI-UCB estimates, and on the covering argument behind Lemma C.3.

Selected references

C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
Y. Abbasi-Yadkori, D. Pál, C. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019; arXiv:1902.04779. https://arxiv.org/abs/1902.04779

16 thms4 active usersReviewed

Completed

Bandit Algorithms Probability Reinforcement Learning·Captain: mikedeng1

Provably Efficient Reinforcement Learning with Linear Function Approximation 1: LSVI-UCB Has Regret O(√(d³H³Tι²)) with Probability 1 − p on Linear MDPsResearch Paper

Motivation

Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order $\sqrt{H^2SAT}$ have been known since the work on UCRL and UCBVI, but they scale with the number of states $S$ and actions $A$ and say nothing when $S$ is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.

Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension $d$ and the horizon $H$ and independent of $S$ and $A$ . The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.

Timeline:

2017–2018: Azar, Osband, Munos (arXiv:1703.05449) and Jin, Allen-Zhu, Bubeck, Jordan (arXiv:1807.03765) give near-optimal $\sqrt T$ regret for tabular episodic MDPs.
2019: Yang and Wang (arXiv:1902.04779) study linear transition models with a simulator; Jin, Yang, Wang, Jordan prove Theorem 3.1 below without a simulator.
2020: Zanette, Lazaric, Kochenderfer, Brunskill (arXiv:2003.00153) improve the dependence on $d$ under a low inherent Bellman error assumption.

Setting

An episodic MDP $\mathrm{MDP}(\mathcal S,\mathcal A,H,\mathbb P,r)$ has a measurable state space $\mathcal S$ , a finite action set $\mathcal A$ , a horizon $H$ , transition kernels $\mathbb P_h(\cdot\mid x,a)$ and deterministic rewards $r_h(x,a)\in[0,1]$ for steps $h=1,\dots,H$ . A policy $\pi(x,h)$ chooses an action at each state and step. Its value functions satisfy the Bellman equation $Q^\pi_h=r_h+\mathbb P_hV^\pi_{h+1}$ , $V^\pi_h(x)=Q^\pi_h(x,\pi(x,h))$ , $V^\pi_{H+1}=0$ , where $\mathbb P_hV(x,a)=\int V\,d\mathbb P_h(\cdot\mid x,a)$ ; the optimal values $V^\star_h$ , $Q^\star_h$ satisfy the same recursion with a maximum over actions.

The MDP is linear (Assumption A) with feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ if $\|\phi\|\le1$ and for each step there are signed measures $\boldsymbol\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ and a vector $\theta_h$ with

\mathbb P_h(\cdot\mid x,a)=\langle\phi(x,a),\boldsymbol\mu_h(\cdot)\rangle,\qquad r_h(x,a)=\langle\phi(x,a),\theta_h\rangle,

and $\|\theta_h\|\le\sqrt d$ , $\|(|\mu_h^{(1)}|(\mathcal S),\dots,|\mu_h^{(d)}|(\mathcal S))\|\le\sqrt d$ .

In each episode $k=1,\dots,K$ an adversary chooses the initial state $x^k_1$ ; the agent then plays $H$ steps, the next state $x^k_{h+1}$ being drawn from $\mathbb P_h(\cdot\mid x^k_h,a^k_h)$ . LSVI-UCB (Algorithm 1) computes, backwards over $h$ , the Gram matrix $\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I$ of the past features $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$ , the ridge-regression weight $w^k_h$ for the targets $r_h+\max_aQ^k_{h+1}$ , and the optimistic estimate

Q^k_h(x,a)=\min\Big\{(w^k_h)^\top\phi(x,a)+\beta\sqrt{\phi(x,a)^\top(\Lambda^k_h)^{-1}\phi(x,a)},\ H\Big\},

and then plays greedily with respect to $Q^k_h$ . Its policy in episode $k$ is $\pi_k$ , and the regret is

\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],\qquad T=KH.

Formalization targets

Goal: Theorem 3.1

There are absolute constants $c,C>0$ such that for every linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta=c\cdot dH\sqrt\iota$ , $\iota=\log(2dT/p)$ ,

\mathbb P\Big(\mathrm{Regret}(K)\le C\sqrt{d^3H^3T\iota^2}\Big)\ge1-p .

Milestones

The milestones follow Appendix B of the paper: linearity of $Q^\pi$ (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.

A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators $\mathbb T^\pi_h$ of (8) map linear action-value functions to linear ones for every policy, then $\mathbb P_h$ is linear in $\phi$ .

Significance

The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension $d$ of the features and polynomially on $H$ , not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.

The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures $\boldsymbol\mu_h$ (see Formalization scope) and the existential reading of the weights in Lemma B.1.

Difficulty

The regression targets $r_h+\max_aQ^k_{h+1}(x^\tau_{h+1},\cdot)$ depend on all past data through $Q^k_{h+1}$ . The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating $V^k_{h+1}$ as fixed, fails because $V^k_{h+1}$ is not measurable with respect to the past at the time $x^\tau_{h+1}$ is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.

A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the $KH$ steps) needs every object to be measurable with respect to the right σ-algebra.

Formalization scope

Model. $\mathcal S$ is any measurable space; $\mathcal A$ is a finite nonempty type with its discrete σ-algebra and a linear order used only to break ties in the argmax. Steps and episodes are 1-based. $V^\pi$ , $Q^\pi$ , $V^\star$ , $Q^\star$ are defined by the Bellman recursions (1) and (2), with value $0$ outside $1\le h\le H$ ; theorems about general policies assume them measurable.
Assumption A is stated with the total-variation normalization $\|(|\mu_h^{(i)}|(\mathcal S))_i\|\le\sqrt d$ instead of the printed $\|\boldsymbol\mu_h(\mathcal S)\|\le\sqrt d$ ; under the printed condition Lemma B.1 is false. The feature map is assumed measurable.
Runs. A run is a process on a probability space with a filtration over the flattened time $(k-1)(H+1)+(h-1)$ : states are adapted, actions are those of Algorithm 1, and the conditional law of $x^k_{h+1}$ given the past is $\mathbb P_h(\cdot\mid x^k_h,a^k_h)$ . The initial states are otherwise unrestricted.
Constants. $c$ and $C$ are quantified before the spaces, $d$ , $H$ , $K$ , $p$ , the MDP and the run; $d,H,K\ge1$ and $p\in(0,1)$ . "With probability $1-p$ " is an upper bound on the outer measure of the failure event.
Ruling out trivializations. The goal does not assume the good event, optimism, or any milestone conclusion; $\beta$ is fixed by the existentially quantified $c$ , not free; the regret uses the model value of the greedy policy, not a realized return. A sorry-free check exhibits a linear MDP and a run satisfying all hypotheses.
Known gap. Algorithm 1 clips $Q^k_h$ only from above, so the bound $|V^k_{h+1}|\le H$ that Lemma B.3's proof needs (and the target bound in Lemma B.2's proof, here an explicit hypothesis) is not automatic off the good event. Lemma B.3 is stated as printed, for every $c_\beta>0$ ; a solver who finds it unprovable should report this in the discussion.
Infrastructure needed: covering numbers of norm balls, the self-normalized martingale bound, Azuma–Hoeffding (in Mathlib), integration against signed measures, and measurability of the algorithm's outputs. The MDP and run definitions are reusable for other episodic RL results; contributions of general lemmas about them are welcome.

Selected references

C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
M. G. Azar, I. Osband, R. Munos, Minimax Regret Bounds for Reinforcement Learning, ICML 2017. https://arxiv.org/abs/1703.05449
C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019. https://arxiv.org/abs/1902.04779
A. Zanette, A. Lazaric, M. Kochenderfer, E. Brunskill, Learning Near Optimal Policies with Low Inherent Bellman Error, ICML 2020. https://arxiv.org/abs/2003.00153

19 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition V: Under the Proximal-PL Inequality, Proximal-Gradient Converges at Rate (1 − μ/L)^kResearch Paper

Motivation

Many problems in machine learning and signal processing minimize a smooth loss plus a simple non-smooth regularizer: $\ell_1$ -regularized least squares, group-sparse regression, and constrained problems written with an indicator function. The standard algorithm for this composite form is the proximal-gradient method, a gradient step on the smooth part followed by a proximal step on the regularizer. Its classical linear convergence guarantee needs the smooth part to be strongly convex, a hypothesis that fails for $\ell_1$ -regularized least squares with fewer observations than variables and for most problems of interest without explicit $\ell_2$ regularization.

For smooth problems the Polyak–Łojasiewicz (PL) inequality $\tfrac12\|\nabla f(x)\|^2 \ge \mu(f(x) - f^*)$ gives a linear rate for gradient descent without convexity (Polyak 1963). Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) propose a generalization to the composite setting, the proximal-PL inequality, under which the proximal-gradient method converges linearly with a one-paragraph proof. They show that it contains the PL case, the strongly convex case, and convex objectives with quadratic growth, and that it is equivalent to the Kurdyka–Łojasiewicz inequality (Bolte, Nguyen, Peypouquet, Suter 2017) and to the proximal error bound used earlier by Luo, Tseng and Drusvyatskiy–Lewis.

Timeline:

1963: Polyak proves linear convergence of gradient descent under the PL inequality.
1993: Luo and Tseng prove linear convergence of feasible descent methods under an error bound.
2015–2016: Bolte et al. and Li–Pong obtain linear rates of proximal gradient under the KL inequality; Drusvyatskiy and Lewis relate error bounds and quadratic growth (arXiv:1602.06661).
2016: Karimi, Nutini and Schmidt introduce the proximal-PL inequality and Theorem 5.

Setting

Let $f, g : \mathbb R^d \to \mathbb R$ and consider problem (11),

\min_{x \in \mathbb R^d} F(x) = f(x) + g(x).

The function $f$ is differentiable with an $L$ -Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L\|x - y\|$ with $L > 0$ . The function $g$ is convex. $F$ has a minimizer $x^*$ , and $F^* = F(x^*)$ .

For a base point $x$ and a parameter $\alpha > 0$ , the proximal model is

m_{x,\alpha}(y) = \langle \nabla f(x), y - x\rangle + \frac{\alpha}{2}\|y - x\|^2 + g(y) - g(x),

and the paper's measure of non-stationarity is

\mathcal D_g(x, \alpha) = -2\alpha \min_{y} m_{x,\alpha}(y). \tag{13}

$F$ satisfies the proximal-PL inequality with modulus $\mu > 0$ if

\tfrac12\,\mathcal D_g(x, L) \ge \mu\bigl(F(x) - F^*\bigr) \quad \text{for all } x. \tag{12}

When $g$ is constant, $\mathcal D_g(x, \alpha) = \|\nabla f(x)\|^2$ and (12) is the PL inequality.

The proximal-gradient method with step size $1/L$ starts at an arbitrary $x_0$ and sets

x_{k+1} \in \operatorname*{argmin}_y m_{x_k, L}(y). \tag{14}

The proximal residual function of Appendix E is $\mathcal R_g(\lambda, x, a) = \min_y [\|\lambda(y - x) + a\|^2 + 2\lambda(g(y) - g(x))]$ .

Formalization targets

Goal: Theorem 5 (p. 8)

Under the hypotheses above,

F(x_k) - F^* \le \Bigl(1 - \frac{\mu}{L}\Bigr)^k \bigl[F(x_0) - F^*\bigr] \qquad \text{for every } k \ge 0.

Milestones (proof of Theorem 5)

The quadratic upper bound (2), p. 2: an $L$ -Lipschitz gradient gives $f(y) \le f(x) + \langle\nabla f(x), y - x\rangle + \frac L2\|y - x\|^2$ .
Descent by $\mathcal D_g$ , p. 9: if $x^+$ minimizes $m_{x,L}$ , then $F(x^+) \le F(x) - \frac{1}{2L}\mathcal D_g(x, L)$ .
The one-step contraction (15), p. 9: $F(x^+) - F^* \le (1 - \mu/L)[F(x) - F^*]$ .

Companion results

Lemma 2 (p. 17): for convex $g$ , $\mathcal R_g(\cdot, x, a)$ is non-increasing on $(0, \infty)$ .
Lemma 1 = Corollary 1 (p. 17): $\mathcal D_g(x, \mu_2) \ge \mathcal D_g(x, \mu_1)$ for $\mu_2 \ge \mu_1 > 0$ .
Appendix F, item 1 (p. 18): for constant $g$ , $\mathcal D_g(x, \alpha) = \|\nabla f(x)\|^2$ , and proximal-PL is PL.
Appendix F, item 2 (p. 18): for $\mu$ -strongly convex $f$ , $F^* \ge F(x) - \frac{1}{2\mu}\mathcal D_g(x, \mu)$ .
Appendix F, item 4 (p. 19): for convex $f$ and $F$ with quadratic growth of modulus $\mu$ , $\mathcal D_g(x, \mu/2) \ge \frac{\mu}{2}(F(x) - F^*)$ .
Two well-definedness statements: for convex $g$ and a positive parameter, the minima in (13) and (27) are attained.

Significance

Theorem 5 gives a global linear rate for the proximal-gradient method under a hypothesis that does not require strong convexity, or convexity of $f$ . Through the classes of Section 4.1 it covers $\ell_1$ -regularized least squares, the composite strongly convex case, and convex composite problems with quadratic growth. The quantity $\mathcal D_g$ also drives the analysis of proximal coordinate descent (Theorem 6, mission VI of this series), and Lemma 1 is what lets the sufficient conditions of Appendix F, which hold with $\mathcal D_g(x, \lambda)$ for $\lambda \le L$ , be used in (12).

The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The work here is to formalize the known proofs, including the properties of $\mathcal D_g$ and $\mathcal R_g$ that the paper uses without stating: the minimum in (13) exists, and the value is finite.

Difficulty

The proof of Theorem 5 is short; the difficulty sits in the objects. $\mathcal D_g$ is defined through a minimum over $\mathbb R^d$ of a function involving a non-smooth convex $g$ , so every step that replaces the minimum by its value at a particular point needs the minimum to be finite and attained. The paper never states these facts, and they fail for an arbitrary $g$ : for $g(y) = -\|y\|^2$ and $\alpha < 2$ the model is unbounded below and the minimum in (13) does not exist. The monotonicity of $\mathcal D_g$ in its second argument (Lemma 1) rests on the convexity inequality of $g$ , and Appendix F item 4 relies on the projection onto the solution set, whose existence depends on that set being closed, convex and non-empty.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d), $\nabla f$ is Mathlib's gradient f, and the Lipschitz hypothesis is written literally, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖, with 0 < L.
The non-empty solution set is a point xstar with F xstar ≤ F y for all y; $F^*$ is f xstar + g xstar, never a free real.
$g$ is real-valued and convex (ConvexOn ℝ Set.univ g). Indicator functions of convex sets, which the paper lists among its examples, take the value $+\infty$ and are outside this formalization; the formulas (13)–(15) subtract values of $g$ , which is undefined at $+\infty$ .
The minimum in (13) and (27) is a real infimum. A real infimum of a set that is unbounded below has the junk value $0$ in Lean, so $\mathcal D_g(x, \alpha)$ is used only with $\alpha > 0$ and convex $g$ , where the infimum is a minimum; this rules out the trivializing reading in which $\mathcal D_g$ vanishes and (12) becomes $F \le F^*$ .
A proximal-gradient run is any sequence whose every step is a minimizer of the model; the minimizer is unique for convex $g$ , but uniqueness is not assumed.
No relation between $\mu$ and $L$ is assumed, as in the paper.
The PL predicate in Appendix F item 1 is the published ShiOptRates.PolyakLojasiewicz (the paper's (3) multiplied by 2), and (2) is the published ShiOptRates.QuadUpper.

Quadratic growth is stated with the distance to the solution set, $\operatorname{dist}(x, \mathcal X^*)$ , which equals $\|x - x_p\|$ for the projection $x_p$ the paper uses. Appendix F item 3 (Hoffman's bound with an unspecified constant $\theta(A, B)$ ) and the equivalences of Appendix G are not included.

Contributions of every kind are welcome: proofs of the milestones, of the companion lemmas, and reusable facts about $\mathcal D_g$ (finiteness, attainment, continuity in $x$ ) that other proximal-method missions can import.

Selected references

H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46, 1993. https://doi.org/10.1007/BF02096261
J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Mathematical Programming 165, 2017. https://doi.org/10.1007/s10107-016-1091-6
D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Mathematics of Operations Research 43(3), 2018. https://arxiv.org/abs/1602.06661
G. Li, T. K. Pong, Calculus of the exponent of Kurdyka–Łojasiewicz inequality and its applications to linear convergence of first-order methods, Foundations of Computational Mathematics 18, 2018. https://arxiv.org/abs/1602.02915

7 thms4 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 3: The Two-Phase RSG Method Finds an (ε, Λ)-Solution within S(Λ)[N(ε) + T(ε, Λ)] Oracle CallsResearch Paper

Motivation

Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.

The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.

Setting

The objective is a differentiable function $f:\mathbb R^n\to\mathbb R$ bounded below, with true optimal value $f^*=\inf_x f(x)$ . Its gradient map $g=\nabla f$ is $L$ -Lipschitz: $\|g(y)-g(x)\|\le L\|y-x\|$ for all $x,y$ . The mission uses $L>0$ . No convexity is assumed.

A stochastic first-order oracle returns a vector $G(x_k,\xi_k)$ when called at the current iterate $x_k$ . Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most $\sigma^2$ . The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes $\sigma>0$ because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.

A randomized stochastic gradient run starts at $x_1$ and uses $x_{k+1}=x_k-\gamma_k G(x_k,\xi_k)$ . It chooses an output index $R\in\{1,\ldots,N\}$ with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs $x_R$ . For a parameter $\widetilde D>0$ , the constant stepsize in equation (2.13) is $\gamma_k=\min\{1/L,\widetilde D/(\sigma\sqrt N)\}$ . The paper writes $D_f=\sqrt{2(f(x_1)-f^*)/L}$ and

\mathcal B_N=\frac{LD_f^2}{N}+\left(\widetilde D+\frac{D_f^2}{\widetilde D}\right)\frac{\sigma}{\sqrt N}.

The two-phase method makes $S$ independent RSG runs, yielding $\bar x_1,\ldots,\bar x_S$ . For each candidate it averages $T$ fresh oracle outputs into an estimated gradient $\widehat g_s$ . It selects a candidate $\bar x^*$ whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.

Formalization targets

The first target is the one-run mean bound of Corollary 2.2, $L^{-1}\mathbb E\|g(x_R)\|^2\le\mathcal B_N$ , followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.

For arbitrary positive $S,N,T$ , Theorem 2.4(a) states the stronger quantitative tail bound

\Pr\left\{\|g(\bar x^*)\|^2\ge2\left(4L\mathcal B_N+\frac{3\lambda\sigma^2}{T}\right)\right\}\le\frac{S+1}{\lambda}+2^{-S}\qquad(\lambda>0).

The goal, Theorem 2.4(b), specializes those parameters to an accuracy $\varepsilon>0$ and failure probability $0<\Lambda<1$ . It sets

S=\left\lceil\log_2\frac2\Lambda\right\rceil,\qquad N=\left\lceil\max\left\{\frac{32L^2D_f^2}{\varepsilon},\left(\frac{32L(\widetilde D+D_f^2/\widetilde D)\sigma}{\varepsilon}\right)^2\right\}\right\rceil,\qquad T=\left\lceil\frac{24(S+1)\sigma^2}{\Lambda\varepsilon}\right\rceil.

An $(\varepsilon,\Lambda)$ -solution is a point satisfying $\Pr\{\|g(\bar x^*)\|^2\le\varepsilon\}\ge1-\Lambda$ . With those parameter values, the method computes such a point using at most $S(N+T)$ stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.

Significance

The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.

The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.

Difficulty

Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's $1,\ldots,S$ . The objective's true infimum is carried by IsGLB (Set.range f) fstar, so $D_f$ cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.

All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final $2^{-S}\le\Lambda/2$ comparison. Positive $\sigma$ and $\widetilde D$ avoid zero steps and an empty post-optimization average.

The formal goal states the probability guarantee. The $S(N+T)$ oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.

Selected references

Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. arXiv:1309.5549v1.

11 thms4 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 2: The Randomized Stochastic Gradient-Free Method with Gaussian Smoothing Bounds (1/L)E‖∇f(x_R)‖² for Nonconvex fResearch Paper

Motivation

Many optimization problems in simulation-based design, reinforcement learning and machine learning can be evaluated but not differentiated. Their objective is an expectation $f(x) = \mathbb E[F(x,\xi)]$ that can only be sampled through noisy function values $F(x,\xi)$ . Gradients may be unavailable because the model is a black box, a simulator, or a legacy code. Methods for this setting are called zeroth-order or derivative-free stochastic methods. The objective $f$ is often nonconvex, so the realistic target is an approximately stationary point, $\|\nabla f(x)\|^2 \le \epsilon$ , not a global minimizer.

Ghadimi and Lan (arXiv:1309.5549; SIAM J. Optim. 23(4), 2013) gave the first complexity bounds for stochastic zeroth-order methods on nonconvex problems. Their randomized stochastic gradient free (RSGF) method combines two ingredients. The first is the Gaussian smoothing and random finite-difference estimator of Nesterov and Spokoiny (Found. Comput. Math. 17, 2017; preprint 2011). The second is a randomized stopping rule that outputs an iterate chosen at random along the trajectory. The resulting bound has become the standard reference point for derivative-free nonconvex stochastic optimization.

Timeline:

1952: Kiefer and Wolfowitz introduce finite-difference stochastic approximation.
2011: Nesterov and Spokoiny analyze Gaussian random gradient-free oracles for convex and deterministic nonconvex problems.
2013: Ghadimi and Lan prove the nonconvex stochastic rate of the RSGF method (Theorem 3.2) and its $O(n/\epsilon^2)$ complexity (Corollary 3.3).

Setting

Let $\mathbb R^n$ be Euclidean space and let $\xi$ be a random vector with distribution $P$ on a measurable space $\Xi$ . The problem is

f^* := \inf_{x\in\mathbb R^n}\Big\{ f(x) := \int_\Xi F(x,\xi)\,dP(\xi) \Big\}. \tag{3.1}

The sample functions $F(\cdot,\xi)$ lie in $\mathcal C^{1,1}_L(\mathbb R^n)$ almost surely: they are differentiable, and their gradients are $L$ -Lipschitz. Two assumptions describe the noise. Assumption A1 concerns the first-order oracle $G(x,\xi) = \nabla_x F(x,\xi)$ : it is unbiased, $\mathbb E[G(x,\xi)] = \nabla f(x)$ , and has variance at most $\sigma^2$ . Assumption A3 says the zeroth-order oracle is unbiased, $\mathbb E[F(x,\xi)] = f(x)$ .

For a smoothing parameter $\mu > 0$ and an $n$ -dimensional standard Gaussian vector $u$ , the Gaussian smoothing of $f$ is $f_\mu(x) = \mathbb E_u[f(x+\mu u)]$ (3.3). The RSGF method starts from $x_1$ and uses stepsizes $\gamma_k$ . At step $k$ it draws a fresh sample $\xi_k$ and a fresh Gaussian direction $u_k$ , forms the zeroth-order estimator

G_\mu(x_k,\xi_k,u_k) = \frac{F(x_k+\mu u_k,\xi_k) - F(x_k,\xi_k)}{\mu}\,u_k, \tag{3.12}

and sets $x_{k+1} = x_k - \gamma_k G_\mu(x_k,\xi_k,u_k)$ (3.13). The output is $x_R$ , where the random iteration count $R \in \{1,\dots,N\}$ has the probability mass function

P_R(k) = \frac{\gamma_k - 2L(n+4)\gamma_k^2}{\sum_{j=1}^N[\gamma_j - 2L(n+4)\gamma_j^2]}. \tag{3.15}

In the Lean development, $f$ is objective P F, $G_\mu$ is szoGrad (the published RandomGradFree.Shared.oracle applied to $F(\cdot,\xi)$ ), and $f_\mu$ is the published RandomGradFree.Shared.smoothing. The smoothing parameter is μs, because μ names the probability measure.

Formalization targets

Goal: Theorem 3.2 a)

Let $0 < \gamma_k < 1/[2(n+4)L]$ for $k = 1,\dots,N$ , with $N \ge 1$ , and let $D_f^2 = 2(f(x_1)-f^*)/L$ . Then

\frac1L\,\mathbb E\|\nabla f(x_R)\|^2 \le \frac{D_f^2 + 2\mu^2(n+4)\big(1 + L(n+4)^2\sum_{k=1}^N(\frac{\gamma_k}{4} + L\gamma_k^2)\big) + 2(n+4)\sigma^2\sum_{k=1}^N\gamma_k^2}{\sum_{k=1}^N[\gamma_k - 2L(n+4)\gamma_k^2]}. \tag{3.16}

The stepsizes are left free, so every stepsize policy specializes the goal.

Companions

Theorem 3.2 b), (3.17): for convex $f$ with a minimizer $x^*$ , the bound on $\mathbb E[f(x_R) - f^*]$ .
Corollary 3.3, (3.26): for the constant stepsizes (3.24) and $\mu \le D_f/((n+4)\sqrt{2N})$ ,

\frac1L\,\mathbb E\|\nabla f(x_R)\|^2 \le \frac{12(n+4)LD_f^2}{N} + \frac{4\sigma\sqrt{n+4}}{\sqrt N}\Big(\tilde D + \frac{D_f^2}{\tilde D}\Big).

Milestones

The milestones follow the paper's proof.

Properties of the smoothing. These are Theorem 3.1 a)–c): $f_\mu$ has an $L$ -Lipschitz gradient given by (3.4), $|f_\mu - f| \le \frac{\mu^2}{2}Ln$ (3.5), the gradient bound (3.6), and the second-moment bound (3.7). Three of these are already on the platform and are referenced. Two consequences follow, (3.9) and (3.11).
Unbiasedness, (3.14): the estimator $G_\mu$ is unbiased for $\nabla f_\mu$ .
The proof chain of Theorem 3.2. The pathwise descent inequality (3.19), the martingale identity (3.20) and the conditional second-moment bound (3.21) combine into the weighted bound (3.23). The $R$ -weighting identity converts (3.23) into (3.16).

Significance

The theorem shows that function values alone suffice to find approximately stationary points of nonconvex stochastic programs. The price is a factor of the dimension $n$ : with constant stepsizes the RSGF method needs $O(n/\epsilon^2)$ iterations, against $O(1/\epsilon^2)$ for the first-order RSG method. The randomized output rule and the analysis through $f_\mu$ are reused in later zeroth-order methods, including two-phase variants, mirror-descent variants and variance-reduced schemes.

The result is proved in the paper. It is not formalized anywhere known to this mission. The platform already holds parts of the Gaussian-smoothing theory from the Nesterov–Spokoiny series, but only for convex problems with exact function values. This mission adds:

the nonconvex form of the second-moment bound (3.7);
the gradient-approximation bound (3.6);
the stochastic sampling model with conditional expectations;
the first machine-checkable statement of a nonconvex stochastic zeroth-order rate.

Difficulty

The first idea is to treat the RSGF method as the first-order RSG method run on $f_\mu$ with the unbiased estimator $G_\mu$ , and to quote the RSG bound. This fails, because the variance $\mathbb E\|G_\mu - \nabla f_\mu\|^2$ has no uniform bound: by (3.7) it grows with $\|\nabla f(x_k)\|^2$ at the random iterate. The analysis has to carry that term along and absorb it into the left side, which is where the weights $\gamma_k - 2L(n+4)\gamma_k^2$ come from. It must also move between $\nabla f_\mu$ and $\nabla f$ through (3.6) at a cost polynomial in $n$ .

On the formal side, three obstacles stand out.

The Gaussian moment estimates behind (3.6) and (3.7) need bounds on $\mathbb E\|u\|^p$ up to $p = 6$ for a standard Gaussian vector.
Conditional expectations with respect to $\sigma(\zeta_{[k-1]})$ are taken at random iterates that depend on the past, so independence of the fresh samples must be used carefully.
Integrability must be established for every quantity before expectations can be manipulated.

Formalization scope

Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The constants $(n+3)$ , $(n+4)$ , $(n+6)$ use the same natural number $n$ . The Gaussian is Mathlib's stdGaussian.
Iterates. They are indexed from $1$ , and $R$ takes values in $\{1,\dots,N\}$ .
Optimal values. $f^*$ is the infimum of $f$ (IsGLB), with $f$ bounded below. The paper's $f^*_\mu := \min f_\mu$ (3.10) is read as an infimum, since the minimum need not be attained.
Smoothness. $F(\cdot,\xi) \in \mathcal C^{1,1}_L$ is required for $P$ -almost every $\xi$ , as on the page.
Assumption A1 is stated at every point $x$ for $G = \nabla_x F$ .
Assumption A3 is the definition of $f$ , with $F(x,\cdot)$ integrable.

The following are explicit additions; the paper leaves them implicit.

Sampling. The samples $\xi_k \sim P$ and $u_k \sim \mathcal N(0,I_n)$ are measurable and mutually independent, and $R$ is independent of all of them.
Measurability and integrability. $F$ is jointly measurable, and $\nabla_x F(x,\cdot)$ is integrable.
Stepsizes are positive.
Corollary 3.3 assumes $\sigma > 0$ .

Every conclusion about an expectation also asserts the integrability of its integrand. A non-integrable function has Lean integral $0$ , so a bound without this conjunct could hold for the wrong reason.

The goal is stated about the objects of the method only: $F$ , $P$ , $f$ , the run (3.12)–(3.13), $R$ and the constants. It does not mention $f_\mu$ , $\Delta_k$ or the filtration, so it cannot be discharged by choosing an auxiliary object.

A complete development needs:

Gaussian moment bounds and differentiation under the Gaussian integral;
conditional expectation with respect to the natural filtration of an independent sequence;
the descent lemma for $\mathcal C^{1,1}_L$ functions.

The Gaussian-smoothing lemmas (3.6), (3.7) and (3.9) are reusable by any zeroth-order mission. Contributions of proofs of individual milestones are welcome, as are alternative proofs of (3.7) without Nesterov's bound.

Selected references

S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4):2341–2368, 2013. Preprint arXiv:1309.5549v1, the version cited here. https://arxiv.org/abs/1309.5549
Y. Nesterov and V. Spokoiny, Random gradient-free minimization of convex functions, Found. Comput. Math. 17:527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23(3):462–466, 1952. https://doi.org/10.1214/aoms/1177729392

18 thms4 active usersReviewed

Completed

Probability Statistics·Captain: mikedeng1

Distribution-Free, Risk-Controlling Prediction Sets II: The Waudby-Smith–Ramdas Betting Bound Is a (1 − δ) Upper Confidence Bound for the Mean Loss (Proposition 5)Research Paper

Motivation

A risk-controlling prediction set is a set-valued predictor $\mathcal T$ that, with probability at least $1-\delta$ over a calibration sample, has expected loss at most a target level $\alpha$ . Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 2021) build such sets for any black-box predictor and any bounded loss by a procedure called upper confidence bound (UCB) calibration: for each value of a tuning parameter $\lambda$ , compute from the calibration data an upper confidence bound $\widehat R^+(\lambda)$ for the risk $R(\lambda)$ , and pick the smallest $\lambda$ beyond which all these bounds sit below $\alpha$ . The guarantee of the procedure (their Theorem 1) holds for any choice of the pointwise bound, so the size of the resulting sets is governed by how tight that bound is.

The paper compares several such bounds: Hoeffding, Bentkus, the empirical Bernstein bound of Maurer and Pontil, and a bound adapted from the hedged capital confidence interval of Waudby-Smith and Ramdas (arXiv:2010.09686). The last one, the Waudby-Smith–Ramdas (WSR) bound, adapts to the unknown variance of the loss and is the one the authors recommend for non-binary losses; their experiments use it throughout. Proposition 5 of the paper states that the WSR bound is a valid $(1-\delta)$ upper confidence bound for the mean of a $[0,1]$ -valued loss. This mission formalizes that proposition.

Timeline: Ville (1939) proved the maximal inequality for nonnegative supermartingales that underlies all betting-based confidence bounds. Waudby-Smith and Ramdas (2020) introduced the hedged capital process and its confidence sequences for bounded means. Bates et al. (2021) extracted the one-sided, fixed-sample variant stated as Proposition 5, with the explicit betting fractions $\nu_i$ below.

Setting

Fix the tuning parameter $\lambda$ ; it is dropped from the notation. The calibration losses $L_1, \dots, L_n$ are independent and identically distributed with law $Q$ on $[0,1]$ (the loss is nonnegative and, by the standing assumption of §3.1 of the paper, bounded by one), and their mean is the risk

R = \int x \, dQ(x).

Fix a level $\delta \in (0,1)$ . For $i \ge 0$ define the running mean and variance

\hat\mu_i = \frac{1/2 + \sum_{j=1}^{i} L_j}{1+i}, \qquad \hat\sigma^2_i = \frac{1/4 + \sum_{j=1}^{i} (L_j - \hat\mu_j)^2}{1+i},

so $\hat\sigma^2_0 = 1/4$ , and for $i \ge 1$ the betting fraction

\nu_i = \min\left\{1, \sqrt{\frac{2\log(1/\delta)}{n\,\hat\sigma^2_{i-1}}}\right\},

which depends only on $L_1, \dots, L_{i-1}$ . For a candidate mean $R' \in \mathbb R$ , the capital process is

\mathcal K_i(R') = \prod_{j=1}^{i} \bigl\{1 - \nu_j (L_j - R')\bigr\}, \qquad \mathcal K_0(R') = 1,

the wealth of a gambler who, starting with one unit, bets the fraction $\nu_j$ of their wealth against the hypothesis that the mean is $R'$ . The WSR bound is

\widehat R^+_{\mathrm{WSR}} = \inf\Bigl\{R' \ge 0 : \max_{i=1,\dots,n} \mathcal K_i(R') > \frac1\delta\Bigr\},

the smallest candidate mean the gambler has discredited by multiplying their wealth by more than $1/\delta$ . In Lean these are obs, muHat, sigmaSqHat, nu, K and wsrUCB in the namespace RiskControl.WSR, and $\mathcal F_i = \sigma(L_1,\dots,L_i)$ is filt n.

Formalization targets

Goal: Proposition 5 (p. 7)

For $n \ge 1$ and $\delta \in (0,1)$ ,

\mathbb P\bigl(\widehat R^+_{\mathrm{WSR}} < R\bigr) \le \delta, \qquad\text{that is}\qquad \mathbb P\bigl(R \le \widehat R^+_{\mathrm{WSR}}\bigr) \ge 1-\delta,

the probability being the product law $Q^{\otimes n}$ of the sample.

Milestones (proof of Proposition 5, p. 26)

Nonnegative factors. $\nu_i \in [0,1]$ , and for losses in $[0,1]$ and $R \in [0,1]$ , $1 - \nu_j(L_j - R) \ge 0$ .
Martingale. At the true mean, $i \mapsto \mathcal K_{\min(i,n)}(R)$ is a martingale for $(\mathcal F_i)$ :

\mathbb E\bigl[\mathcal K_i(R) \mid \mathcal F_{i-1}\bigr] = \mathcal K_{i-1}(R).

Ville's inequality (referenced, already proved on the platform): a nonnegative supermartingale started at most $1$ exceeds $1/\delta$ with probability at most $\delta$ .
Monotonicity. For losses in $[0,1]$ , $R' \mapsto \mathcal K_i(R')$ is nondecreasing on $[0,\infty)$ .
Inclusion. For losses in $[0,1]$ and $R \ge 0$ , $\widehat R^+_{\mathrm{WSR}} < R$ implies $\max_{i \le n} \mathcal K_i(R) \ge 1/\delta$ .

Significance

The result is the validity half of the WSR bound: with it, UCB calibration (Theorem 1 of the paper) applied to $\widehat R^+_{\mathrm{WSR}}$ gives the paper's Theorem 4, a risk-controlling prediction set built from the variance-adaptive bound that the experiments of the paper use for classification, segmentation and protein-structure tasks. It is also a self-contained instance of the betting approach to confidence bounds for bounded means, which now underlies a family of nonasymptotic, variance-adaptive procedures in statistics and machine learning.

The proposition is proved in the paper (p. 26), following the proof of Theorem 4 of Waudby-Smith and Ramdas. To our knowledge neither it nor the hedged capital construction has a machine-checked proof. The mission produces one: a Lean statement of the WSR bound with its exact constants, and a proof that reuses the platform's Ville inequality. The capital process and its martingale property are the reusable part; the same construction with other predictable betting fractions gives other confidence bounds.

Difficulty

The bound is not obtained by inverting a tail inequality for the empirical mean, so Hoeffding- or Bernstein-type arguments do not apply. The probabilistic core is the martingale step: one must show that $\nu_i$ is a measurable function of $L_1,\dots,L_{i-1}$ only (it involves $\hat\sigma^2_{i-1}$ , which involves every $\hat\mu_j$ for $j < i$ ), and compute a conditional expectation on the product space $\mathbb R^n$ using independence of the coordinates. Ville's inequality then holds only at the true mean $R$ , a single unknown point, while $\widehat R^+_{\mathrm{WSR}}$ is an infimum over all candidate means; the passage between them needs the monotonicity of $\mathcal K_i$ in its argument, which fails without the bound $L_j \le 1$ (a factor can turn negative). A union bound over candidate means, the first idea, gives nothing here.

Formalization scope

The sample is $\omega : \mathrm{Fin}\,n \to \mathbb R$ under Measure.pi (fun _ => Q), with $L_j = \omega(j-1)$ for $1 \le j \le n$ (1-based indices as on the page). $Q$ is the law of the loss $L(Y, \mathcal T_\lambda(X))$ for the fixed $\lambda$ , assumed concentrated on $[0,1]$ : this is the §3.1 standing assumption together with $L \ge 0$ . The goal adds two hypotheses implicit on the page: $n \ge 1$ and $0 < \delta < 1$ (so that $\log(1/\delta) > 0$ ). The empty sum gives $\hat\sigma^2_0 = 1/4$ ; " $\max_{i=1,\dots,n} \mathcal K_i > 1/\delta$ " is written as an existential over $i \in \{1,\dots,n\}$ ; the infimum is an extended-real infimum, equal to $+\infty$ when no candidate qualifies. The failure probability is bounded through the outer measure of $\{\widehat R^+_{\mathrm{WSR}} < R\}$ , which equals the page's statement for a measurable event. The martingale is extended constantly past time $n$ so that it is indexed by $\mathbb N$ .

Two printed slips are corrected: the proof's "then $P(\max_i \mathcal K_i \ge 1/\delta)$ " (a stray $P$ ) is stated as the event, and "increasing in $R$ " is stated as nondecreasing on $R \ge 0$ .

The infimum must not be a real infimum: a real sInf of an empty set is $0$ , which would make $\widehat R^+_{\mathrm{WSR}} < R$ true for every positive mean and the goal false; with the extended-real infimum the empty case gives $+\infty$ , and the goal is the paper's proposition, not a vacuous one.

Contributions welcome: the measurability of $\nu_i$ with respect to $\mathcal F_{i-1}$ , conditional expectations of products of independent coordinates under Measure.pi, and a finite-horizon form of Ville's inequality (Mathlib's Doob maximal inequality MeasureTheory.maximal_ineq is an alternative route).

Selected references

S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, J. ACM 68(6), 2021. arXiv:2101.02703v3
I. Waudby-Smith, A. Ramdas, Estimating means of bounded random variables by betting, J. R. Stat. Soc. B, 2024. arXiv:2010.09686
J. Ville, Étude critique de la notion de collectif, Gauthier-Villars, 1939.
A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009. arXiv:0907.3740

7 thms4 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research+1·Captain: mikedeng1

Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation: The Worst-Case Risk over an RKHS Ambiguity Set Equals Its Support-Function DualResearch Paper

Motivation

Distributionally robust optimization (DRO) chooses a decision $\theta$ that minimizes the expected loss under the worst distribution in an ambiguity set $\mathcal K$ of plausible distributions, $\min_\theta\sup_{P\in\mathcal K}\int l(\theta,\xi)\,dP(\xi)$ . It sits between stochastic optimization, which trusts a single distribution, and worst-case robust optimization, which trusts none. The inner supremum is a problem of moments, studied since Stieltjes and made computable by duality (Isii 1962; Shapiro 2001; Bertsimas and Popescu 2005). Existing tractable reformulations require the ambiguity set to be described by finitely many moments, a $\phi$ -divergence or a Wasserstein ball, and they usually require a structural property of the loss: affine or quadratic form, or a known Lipschitz constant.

Zhu, Jitkrittum, Diehl and Schölkopf (AISTATS 2021; arXiv:2006.06981) describe the ambiguity set through kernel mean embeddings: a distribution is represented by its mean in a reproducing kernel Hilbert space, and the ambiguity set is the set of distributions whose embedding lies in a convex set $\mathcal C$ of that space. Moment sets, MMD balls, scenario polytopes and the whole space (worst-case RO) all arise for suitable kernels and sets $\mathcal C$ . Their Generalized Duality Theorem (Theorem 3.1) turns the inner worst-case problem into a minimization over a function of the RKHS that majorizes the loss, with no assumption on the loss beyond upper semicontinuity.

Setting

Let $\mathcal X$ be a compact metric space (in the paper, a compact $\mathcal X\subset\mathbb R^d$ ) with its Borel $\sigma$ -algebra, and $\mathcal P$ the set of Borel probability measures on $\mathcal X$ . Let $\mathcal H$ be a real Hilbert space and $\varphi:\mathcal X\to\mathcal H$ a continuous feature map; $k(x,y)=\langle\varphi(x),\varphi(y)\rangle_{\mathcal H}$ is then a continuous positive definite kernel, and an element $f\in\mathcal H$ acts on $\mathcal X$ by the reproducing property $f(\xi)=\langle f,\varphi(\xi)\rangle_{\mathcal H}$ (rkhsEval).

The mean embedding of $P\in\mathcal P$ is $\mu_P=\int\varphi\,dP\in\mathcal H$ (meanEmbedding).
For $\mathcal C\subseteq\mathcal H$ , the ambiguity set is $\mathcal K_{\mathcal C}=\{P\in\mathcal P:\mu_P\in\mathcal C\}$ (ambiguitySet).
The support function of $\mathcal C$ is $\delta^*_{\mathcal C}(f)=\sup_{\mu\in\mathcal C}\langle f,\mu\rangle_{\mathcal H}\in[-\infty,\infty]$ (supportFun).
A loss is a function $l:\Theta\times\mathcal X\to[-\infty,\infty)$ , where $\Theta$ is an arbitrary set of decisions; $\int l\,dP$ is the extended-real expectation.

For fixed $\theta$ (written $l=l(\theta,\cdot)$ ), the primal inner problem (11) and the dual inner problem (12) are

\mathrm{(P)}_\theta=\sup_{P\in\mathcal K_{\mathcal C}}\int l\,dP,\qquad \mathrm{(D)}_\theta=\inf\Big\{f_0+\delta^*_{\mathcal C}(f):\ f_0\in\mathbb R,\ f\in\mathcal H,\ l(\xi)\le f_0+f(\xi)\ \forall\xi\in\mathcal X\Big\}

(primalValue, dualValue, with the constraint IsDualFeasible). Assumption 3.1 of the paper asks that each $l(\theta,\cdot)$ be proper (not identically $-\infty$ ) and upper semicontinuous, that $\mathcal C$ be closed and convex, and that $\mathrm{ri}(\mathcal K_{\mathcal C})\neq\emptyset$ .

The PDF prints no page numbers; every page cited in this mission is the PDF page of arXiv:2006.06981v3.

Formalization targets

Goal: Theorem 3.1 (Generalized Duality), p. 5

Under the hypotheses above, with $\mathcal K_{\mathcal C}\ne\emptyset$ ,

\forall\theta\in\Theta:\quad \sup_{P\in\mathcal K_{\mathcal C}}\int l(\theta,\xi)\,dP(\xi)=\inf_{\substack{f_0\in\mathbb R,\,f\in\mathcal H\\ l(\theta,\cdot)\le f_0+f}}f_0+\delta^*_{\mathcal C}(f),

and consequently $\mathrm{(P)}=\inf_\theta\mathrm{(P)}_\theta=\inf_\theta\mathrm{(D)}_\theta=\mathrm{(D)}$ , the equality of the Kernel DRO problem (2) and its dual (4).

Milestones (the proof of Proposition A.1, pp. 13–15, and Appendix D, pp. 22–23)

The reproducing identity $\int f\,dP=\langle f,\mu_P\rangle_{\mathcal H}$ (p. 13).
Lemma D.1: $\int(l-f_0-f)\,dP\le0$ for all $P$ iff $l\le f_0+f$ on $\mathcal X$ .
Weak duality: $\int l\,dP\le f_0+\delta^*_{\mathcal C}(f)$ for $P\in\mathcal K_{\mathcal C}$ and feasible $(f_0,f)$ (p. 6).
Lemmas D.2–D.4: $\mathcal T(\mathcal P)=\{\mu_P\}$ , $\mathcal C\cap\mathcal T(\mathcal P)$ and $\mathcal K_{\mathcal C}$ are compact.
Primal attainment (p. 15), via the upper semicontinuity of $P\mapsto\int l\,dP$ (a supporting lemma the paper uses without stating).
The separation (14), the sign $\tau<0$ with the rescaled dual feasible point, and $\mathrm{(D)}\le\mathrm{(P)}+\epsilon$ (p. 15).
Proposition A.1: $\mathrm{(P)}_\theta=\mathrm{(D)}_\theta$ (p. 13).

Companions

Lemma A.2 (complementarity (19)), Corollary 3.1.3 (the optimal majorant interpolates $l$ $P^*$ -a.e.), the support function $\frac1N\sum_i f(\xi_i)+\epsilon\|f\|_{\mathcal H}$ of the RKHS norm ball (Table 1), and the weak-duality content of Corollary 3.1.1 for integral probability metrics.

Significance

The theorem replaces an optimization over probability measures by a semi-infinite program over $(f_0,f)\in\mathbb R\times\mathcal H$ , whose objective is explicit for the common choices of $\mathcal C$ (Table 1). The majorant $f_0+f$ needs no Lipschitz constant and no parametric form of the loss, and the dual variable $f^*$ doubles as a witness function for the MMD. This is the basis of the paper's batch and stochastic functional gradient algorithms, and it places moment-based DRO, scenario optimization, MMD-ball DRO and worst-case RO in one framework.

The result is proved on paper; it has no machine-checked proof that we know of. Formalizing it builds the duality theory of moment problems with infinitely many moment constraints, on top of Mathlib's Hilbert spaces, Bochner integrals and the weak topology on probability measures. The formal statements also fix points the paper leaves loose: the infimum in place of the printed "min", the reading of the Slater condition, and the role of the continuity of the kernel.

Difficulty

Weak duality is a two-line computation. The work is strong duality. The paper's route separates the cone $A=\{(\int1\,dP,\int\varphi\,dP,\int l\,dP):P\in\mathrm{co}(\mathcal P)\}$ from $B_\epsilon=\{(1,\mu,t+\epsilon):\mu\in\mathcal C\}$ in $\mathbb R\times\mathcal H\times\mathbb R$ . A Hahn–Banach strict separation needs one set compact or the two at positive distance, and $A$ is neither obviously closed nor bounded. The step goes through only because $\mathcal K_{\mathcal C}$ is compact in the weak topology and $P\mapsto\int l\,dP$ is upper semicontinuous, which also gives primal attainment and the sign $\tau<0$ . The loss may take the value $-\infty$ , so every expectation lives in $[-\infty,\infty)$ . The infinite primal case also needs an argument of its own.

Formalization scope

$\mathcal X$ is a compact metric space with a Borel $\sigma$ -algebra; a compact subset of $\mathbb R^d$ is an instance. $\mathcal P$ is ProbabilityMeasure X with its topology of weak convergence; the paper's MMD topology agrees with it for a universal continuous kernel.
The RKHS is in feature-map form: a real Hilbert space $\mathcal H$ and a continuous $\varphi$ . Continuity of the kernel is not written in Assumption 3.1 but is used by Appendix D.
Losses are X → EReal, upper semicontinuous, never $+\infty$ , and not identically $-\infty$ . Expectations use the published definition WassersteinDRO.Duality.erealExpectation, which for such losses is the usual $\int l\,dP\in[-\infty,\infty)$ .
Support function, primal and dual values are extended reals. $\delta^*_\emptyset=-\infty$ ; $\delta^*_{\mathcal H}(f)=+\infty$ for $f\ne0$ ; an empty ambiguity set gives primal value $-\infty$ ; an infeasible dual gives $+\infty$ . The sum $f_0+\delta^*_{\mathcal C}(f)$ adds a real to an extended real, so $+\infty+(-\infty)$ never occurs.
The Slater clause $\mathrm{ri}(\mathcal K_{\mathcal C})\ne\emptyset$ names no topology on measures and is used only to obtain a primal solution (p. 15). It is read as $\mathcal K_{\mathcal C}\ne\emptyset$ , which it implies under any reading, so the formal goal is at least as strong as the paper's.
Every printed "min" is read as an infimum. Dual attainment is not proved and can fail: for $\mathcal X=[0,1]$ , $\varphi(x)=x$ , $\mathcal C=(-\infty,0]$ and $l(x)=\sqrt x$ , the dual infimum $0$ is not attained.
The dual variable ranges over $\mathcal H$ , never over arbitrary functions on $\mathcal X$ . Over all bounded functions, the choice $f=l$ would make the duality trivial (Example 3.3). The goal is also not closed by unfolding: for $\mathcal C=\mathcal H$ it says $\sup_P\int l\,dP=\sup_\xi l(\xi)$ , worst-case RO.
Corollary 3.1.2 (p. 6) is not stated: it is false under Assumption 3.1 alone (for $\mathcal C=\mathcal H$ and $l=\mathbf 1_{\{0\}}$ , (2) equals $1$ while (6) equals $0$ ).

Reusable pieces: the kernel mean embedding and its continuity on ProbabilityMeasure X, compactness of RKHS ambiguity sets, and the upper semicontinuity of $P\mapsto\int l\,dP$ for upper semicontinuous $l$ (a portmanteau-type fact not yet in Mathlib). Proofs of any milestone are welcome. So are support-function computations for the other rows of Tables 1 and 3.

Selected references

J.-J. Zhu, W. Jitkrittum, M. Diehl, B. Schölkopf, Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation, AISTATS 2021 (PMLR 130); cited here as arXiv:2006.06981v3, 2021. https://arxiv.org/abs/2006.06981
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14, 1962. https://doi.org/10.1007/BF02868641
D. Bertsimas, I. Popescu, Optimal inequalities in probability theory: a convex optimization approach, SIAM Journal on Optimization 15(3), 2005. https://doi.org/10.1137/S1052623401399903
A. Gretton, K. Borgwardt, M. Rasch, B. Schölkopf, A. Smola, A kernel two-sample test, Journal of Machine Learning Research 13, 2012. https://jmlr.org/papers/v13/gretton12a.html
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

15 thms4 active usersReviewed

Completed

Information Theory Probability Statistics·Captain: mikedeng1

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms I: The Expected Generalization Error Is at Most √(2σ²I(S;W)/n) (Theorem 1)Research Paper

Motivation

A learning algorithm trained on a finite sample generalizes when its empirical risk on that sample is close to its risk on fresh data. Classical guarantees come from uniform convergence over the hypothesis class (VC dimension, Rademacher complexity) or from algorithmic stability, such as uniform stability (Bousquet and Elisseeff, 2002) and on-average stability (Shalev-Shwartz et al., 2010). Both families look at the class or at the algorithm's worst-case sensitivity, not at how much the trained hypothesis actually depends on the data it was trained on.

Russo and Zou (arXiv:1511.05219, 2016) bounded the bias of adaptive data analysis by mutual information, and Xu and Raginsky (arXiv:1705.07809, NIPS 2017) turned this into a generalization bound for learning algorithms: the expected generalization error is at most $\sqrt{2\sigma^2 I(S;W)/n}$ , where $I(S;W)$ is the mutual information between the training sample and the output hypothesis. This bound started the line of information-theoretic generalization bounds, later refined to individual-sample mutual information (Bu, Zou and Veeravalli, 2020), conditional mutual information (Steinke and Zakynthinou, 2020) and chaining variants (Asadi, Abbe and Verdú, 2018).

Timeline:

2016, Russo and Zou: bias of adaptive analysis bounded by $I(\Lambda_{\mathsf W}(S);W)$ , the information carried by the vector of empirical risks, for a finite hypothesis space.
2017, Xu and Raginsky: the bound with the input–output mutual information $I(S;W)$ , for arbitrary hypothesis spaces (Theorem 1); high-probability versions and an analysis of the Gibbs algorithm.
2018–2020: chaining, individual-sample and conditional mutual information refinements.

Setting

There is an instance space $\mathsf Z$ , a hypothesis space $\mathsf W$ and a nonnegative loss $\ell:\mathsf W\times\mathsf Z\to\mathbb R_+$ , written ℓ : W → Z → ℝ in Lean. Data are drawn from an unknown probability measure $\mu$ on $\mathsf Z$ ; a dataset of size $n$ is an i.i.d. sample $S=(Z_1,\dots,Z_n)\sim\mu^{\otimes n}$ (sampleLaw μ n).

A learning algorithm is a Markov kernel $P_{W|S}$ (κ : Kernel (Fin n → Z) W): given the dataset, it outputs a random hypothesis $W$ . The pair $(S,W)$ has joint law $P_{S,W}=\mu^{\otimes n}\otimes P_{W|S}$ (sampleLaw μ n ⊗ₘ κ), with marginals $P_S=\mu^{\otimes n}$ and $P_W$ .

The population risk and the empirical risk of a hypothesis $w$ are

L_\mu(w)=\int_{\mathsf Z}\ell(w,z)\,\mu(dz),\qquad L_S(w)=\frac1n\sum_{i=1}^n \ell(w,Z_i)

(risk ℓ μ w, empRisk ℓ s w). The expected generalization error is

\mathrm{gen}(\mu,P_{W|S})=\mathbb E\big[L_\mu(W)-L_S(W)\big],

the expectation taken under $P_{S,W}$ (genError ℓ μ κ).

The mutual information of a pair $(X,Y)$ with joint law $P_{X,Y}$ is the relative entropy $I(X;Y)=D(P_{X,Y}\,\|\,P_X\otimes P_Y)\in[0,\infty]$ (mutualInfo). A real random variable $U$ is $\sigma$ -subgaussian if $\log\mathbb E[e^{\lambda(U-\mathbb EU)}]\le\lambda^2\sigma^2/2$ for all $\lambda\in\mathbb R$ .

Formalization targets

Goal: Theorem 1 (p. 4)

If $\ell(w,Z)$ is $\sigma$ -subgaussian under $\mu$ for every $w\in\mathsf W$ , then

\big|\mathrm{gen}(\mu,P_{W|S})\big|\le\sqrt{\frac{2\sigma^2}{n}\,I(S;W)} .

The statement fixes no structure on $\mathsf W$ (it may be uncountable) and no bound on the loss beyond subgaussianity.

Milestones

(A.1), Donsker–Varadhan (p. 11), the inequality $\int F\,d\pi-D(\pi\|\rho)\le\log\int e^F\,d\rho$ . Already proved on the platform and referenced.
Lemma 1 (p. 3), the decoupling estimate: if $f(\bar X,\bar Y)$ is $\sigma$ -subgaussian under $P_X\otimes P_Y$ , then

\big|\mathbb E f(X,Y)-\mathbb E f(\bar X,\bar Y)\big|\le\sqrt{2\sigma^2 I(X;Y)} .

Subgaussianity of the empirical risk (§3.2, p. 4): for every $w$ , $L_S(w)-L_\mu(w)$ is $\sigma/\sqrt n$ -subgaussian under $\mu^{\otimes n}$ .
The mixture step (§3.2, p. 4, corrected): under $P_S\otimes P_W$ , $f(\bar S,\bar W)=L_{\bar S}(\bar W)-L_\mu(\bar W)$ is $\sigma/\sqrt n$ -subgaussian with mean $0$ .

Significance

The result. Theorem 1 makes generalization a property of the dependence between data and output rather than of the size of the hypothesis class. It applies to randomized algorithms on uncountable or infinite-dimensional hypothesis spaces, where uniform convergence gives nothing, and to unbounded subgaussian losses. Any mechanism that limits $I(S;W)$ , such as noise injection, differential privacy, compression or relative-entropy regularization, inherits a generalization guarantee. A loss with values in $[a,b]$ is $(b-a)/2$ -subgaussian for every $\mu$ , so the theorem covers all bounded losses. The bound is also the template for the later refinements listed above, which share Lemma 1's decoupling argument.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formalization supplies a reusable statement of mutual information as a relative entropy of a joint law on general measurable spaces, a decoupling lemma for subgaussian functions, and the mixture argument for subgaussian families, all of which recur in the later literature. It also settles a point the paper leaves loose: the printed proof applies Lemma 1 to the uncentred empirical risk, which is not subgaussian in general; the milestones state the corrected step.

Difficulty

The two halves of the proof are short on paper, but each step that "follows" uses a fact the page does not state. The decoupling estimate needs $\mathbb E f(X,Y)$ to be finite, which holds only because finite relative entropy and exponential integrability under the product together force integrability under the joint law. The mixture step needs the moment-generating-function bound of each section $w\mapsto f(\cdot,w)$ to integrate over $P_W$ , which requires joint measurability and the centring of every section at its own mean: the uncentred empirical risk $L_{\bar S}(\bar W)$ mixes laws with different means and is not subgaussian.

A natural first attempt applies Lemma 1 directly to $f(s,w)=L_s(w)$ as printed; it fails on the example $\ell(w,z)=w$ with $W$ uniform on $\{0,1\}$ and independent of $S$ .

Formalization scope

Objects. The sample law, $L_\mu$ and $L_S$ are reused from the published LearnStability.Characterization.Setting. This mission defines mutualInfo P := klDiv P (P.fst.prod P.snd) (values in $[0,\infty]$ ) and genError, the integral of the pointwise difference $L_\mu(w)-L_s(w)$ under sampleLaw μ n ⊗ₘ κ. Samples are Fin n → Z; the algorithm is a Markov kernel.
Subgaussianity is Mathlib's HasSubgaussianMGF of the centred variable, whose parameter is the variance proxy: $\sigma^2$ for the loss, $\sigma^2/n$ for the empirical risk.
Added hypotheses, all implicit on the page: $n\ge1$ (the bound divides by $n$ ); joint measurability of $\ell$ (so that $L_\mu(W)$ and $L_S(W)$ are random variables); and $I\ne\infty$ in Lemma 1 and Theorem 1, because Lean's conversion of $\infty$ to a real number gives $0$ , which would turn the page's vacuous bound into a false claim. The page's nonnegativity of $\ell$ is kept. No integrability hypothesis on $f$ or on the losses is assumed beyond subgaussianity.
Correction of the print. The page says that $f(\bar S,\bar W)=L_{\bar S}(\bar W)$ is $\sigma/\sqrt n$ -subgaussian; milestone 4 states it for the centred $L_{\bar S}(\bar W)-L_\mu(\bar W)$ , together with its mean being $0$ . Equation (9) is not posed separately.
Ruled out. The goal is stated for genError and the mutual information of the algorithm's own joint law; a version through Lemma 1's abstract pair $(\bar X,\bar Y)$ , through $I(\Lambda_{\mathsf W}(S);W)$ (Theorem 2, out of scope), or with $I$ truncated to a real number would not be this theorem.
Infrastructure. Integrability transfer from $P_X\otimes P_Y$ to $P_{X,Y}$ under finite relative entropy; sums of independent subgaussian variables on Measure.pi (Mathlib has HasSubgaussianMGF.sum_of_iIndepFun); mixtures of mean-zero subgaussian families under a product measure. These are reusable beyond this mission, and contributions of each are welcome.

Selected references

A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NIPS 2017; arXiv:1705.07809v2. https://arxiv.org/abs/1705.07809
D. Russo, J. Zou, Controlling bias in adaptive data analysis using information theory, AISTATS 2016. https://arxiv.org/abs/1511.05219
S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, JMLR 11, 2010. https://jmlr.org/papers/v11/shalev-shwartz10a.html
O. Bousquet, A. Elisseeff, Stability and generalization, JMLR 2, 2002. https://www.jmlr.org/papers/v2/bousquet02a.html
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013 (Donsker–Varadhan, Cor. 4.15). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
A. Asadi, E. Abbe, S. Verdú, Chaining mutual information and tightening generalization bounds, NeurIPS 2018. https://arxiv.org/abs/1806.03803
Y. Bu, S. Zou, V. Veeravalli, Tightening mutual information based bounds on generalization error, IEEE JSAIT 2020. https://arxiv.org/abs/1901.04609
T. Steinke, L. Zakynthinou, Reasoning about generalization via conditional mutual information, COLT 2020. https://arxiv.org/abs/2001.09122

7 thms4 active usersReviewed

Completed

Convex Optimization·Captain: mikedeng1

Online Learning and Online Convex Optimization 2: Normalized Exponentiated Gradient Has Regret at Most log(d)/η + η Σₜ Σᵢ wₜ[i]zₜ[i]² When ηzₜ[i] ≥ −1Research Paper

Motivation

Learning with expert advice and online linear optimization over the probability simplex are the basic models behind boosting, multiplicative-weights methods for linear programming and zero-sum games, and adversarial bandit algorithms. The algorithm that solves them, under the names Weighted Majority, Hedge and Exponentiated Gradient (EG), keeps a probability vector over $d$ coordinates and multiplies each weight by $e^{-\eta z_t[i]}$ after observing the loss vector $z_t$ .

Littlestone and Warmuth (1994) introduced Weighted Majority for predicting with expert advice (doi:10.1006/inco.1994.1009).
Freund and Schapire (1997) analysed the same update as Hedge, for losses in $[0,1]$ (doi:10.1006/jcss.1997.1504).
Kivinen and Warmuth (1997) introduced Exponentiated Gradient as an online algorithm for linear prediction (doi:10.1006/inco.1996.2612).
Beck and Teboulle (2003) identified the update as mirror descent with the entropy on the simplex (doi:10.1016/S0167-6377(02)00231-6).
Shalev-Shwartz's survey (2011/2012) derives it as Online Mirror Descent with a normalized-entropy regularizer and proves, by Fenchel duality, a regret bound in which each round contributes a local norm of the loss vector instead of its sup norm (doi:10.1561/2200000018, §2.8).

The local-norm form is the one needed when loss vectors are large on coordinates of small weight, which is the situation of importance-weighted loss estimates in adversarial bandits.

Setting

Fix a dimension $d \ge 1$ and a learning rate $\eta > 0$ . In round $t = 1, 2, \dots$ the learner plays a vector $w_t$ in the probability simplex $S = \{w \in \mathbb R^d : w \ge 0,\ \sum_i w[i] = 1\}$ , then observes a loss vector $z_t \in \mathbb R^d$ and suffers the linear loss $\langle w_t, z_t\rangle$ . Write $z_{1:t} = z_1 + \dots + z_t$ .

Normalized EG starts from $w_1 = (1/d, \dots, 1/d)$ and updates

w_{t+1}[i] = \frac{w_t[i]\, e^{-\eta z_t[i]}}{\sum_j w_t[j]\, e^{-\eta z_t[j]}}, \qquad\text{equivalently}\qquad w_t[i] = \frac{e^{-\eta z_{1:t-1}[i]}}{\sum_j e^{-\eta z_{1:t-1}[j]}} .

Its regret against a comparator $u \in S$ after $T$ rounds is $\sum_{t=1}^T \langle w_t - u, z_t\rangle$ .

The analysis is phrased for general Online Mirror Descent (OMD): given a link function $g$ , predict $w_t = g(-z_{1:t-1})$ . For a regularizer $R$ on a set $S$ (equal to $+\infty$ off $S$ ), the Fenchel conjugate is $R^\star(\theta) = \sup_{w\in S} (\langle w,\theta\rangle - R(w))$ , and the Bregman divergence of a differentiable $F$ is $D_F(a\,\|\,b) = F(a) - F(b) - \langle \nabla F(b), a - b\rangle$ . Normalized EG is OMD with $g = \nabla R^\star$ for the normalized entropy $R(w) = \frac1\eta\sum_i w[i]\log w[i]$ on $S$ , whose conjugate is $R^\star(\theta) = \frac1\eta\log\sum_i e^{\eta\theta[i]}$ and whose gradient is the softmax.

Formalization targets

Goal: Theorem 2.22 (p. 153)

If $\eta z_t[i] \ge -1$ for all $t$ and $i$ , then for every $T$ and every $u \in S$ ,

\sum_{t=1}^T \langle w_t - u, z_t\rangle \le \frac{\log d}{\eta} + \eta \sum_{t=1}^T \sum_{i=1}^d w_t[i]\, z_t[i]^2 .

The comparator is unquantified on the page; it ranges over the simplex $S$ , the competing set of the normalized-entropy regularizer. The bound fails for $u$ outside $S$ .

Milestones, in proof order

Lemma 2.20 (p. 150). OMD with link $g = \nabla R^\star$ satisfies, for every $u \in S$ ,

\sum_{t=1}^T \langle w_t - u, z_t\rangle \le R(u) - R(w_1) + \sum_{t=1}^T D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}),

with equality for a minimizer of $R(u) + \sum_t\langle u, z_t\rangle$ over $S$ . 2. (2.16)–(2.18) (p. 153). For $R^\star(\theta) = \frac1\eta\log\sum_i e^{\eta\theta[i]}$ , the gradient is the softmax, $w_t = \nabla R^\star(-z_{1:t-1})$ , and

D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}) = \frac1\eta \log\Big(\sum_i w_t[i]\, e^{-\eta z_t[i]}\Big) + \langle w_t, z_t\rangle .

The per-round bound (pp. 153–154). If $\eta z_t[i] \ge -1$ for every $i$ , then $D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}) \le \eta\sum_i w_t[i]\, z_t[i]^2$ .

Significance

The result. Since $\sum_i w_t[i] z_t[i]^2 \le \|z_t\|_\infty^2$ , Theorem 2.22 improves the standard bound $\log(d)/\eta + \eta\sum_t\|z_t\|_\infty^2$ of normalized EG. The improvement matters when a coordinate with tiny weight carries a huge loss: the local norm weights that loss by its probability. This is what gives the $O(\sqrt{dT\log d})$ regret of Exp3-type bandit algorithms, whose loss estimates are of order $1/w_t[i]$ . The theorem allows negative losses down to $-1/\eta$ , so it also applies to gains and to centred or shifted losses.

Formalizing it. The theorem is proved in the survey; no machine-checked proof of it is known. The platform has a proved Hedge bound for non-negative losses compared with a single expert (Hazan, Introduction to Online Convex Optimization, Theorem 1.5). It does not imply Theorem 2.22: the latter allows negative losses, and its local-norm term is not invariant under shifting $z_t$ by a constant vector, so the shift that reduces signed losses to non-negative ones changes the bound. Lemma 2.20 is a general duality identity for OMD and is reusable for every OMD instance (Euclidean, $p$ -norm, unnormalized entropy).

Difficulty

The obvious argument for Hedge tracks the potential $\log\sum_i e^{-\eta z_{1:t}[i]}$ and bounds the one-step increase using $e^{-a} \le 1 - a + a^2/2$ for $a \ge 0$ . With negative losses that inequality fails. The weaker form $e^{-a} \le 1 - a + a^2$ is valid only for $a \ge -1$ , which is where the hypothesis $\eta z_t[i] \ge -1$ comes from. The bound is also stated against the whole simplex, not against single experts, so the potential argument has to be combined with an entropy bound for a general comparator.

Formalization scope

Vectors are Fin d → ℝ, with 0 < d and 0 < η. Rounds are numbered from $0$ in Lean, so index $t$ is the paper's round $t+1$ and sums over rounds run over Finset.range T.
The algorithm is the published definition UnderstandingML.wmWeights η z t (reference item UnderstandingML_Online), which is exactly the closed form of normalized EG for arbitrary real loss vectors; wmWeights η z 0 is the uniform vector $w_1$ .
The comparator in the goal ranges over the probability simplex (0 ≤ u i, ∑ i, u i = 1). A statement over all $u \in \mathbb R^d$ is false, and a statement over vertices only would be the weaker expert bound; both are ruled out.
$\log$ is the natural logarithm; all its arguments in the statements are positive.
Lemma 2.20 is stated on a real Hilbert space $E$ with a real-valued $R$ and a set $S$ . " $g = \nabla R^\star$ " is three hypotheses: $g$ maps into $S$ , $g(\theta)$ attains the supremum defining $R^\star(\theta)$ , and $R^\star$ has gradient $g(\theta)$ at $\theta$ . Differentiability of $R^\star$ is the paper's consequence of Lemma 2.19, which is cited to the literature and is assumed here. These hypotheses are satisfiable; a sorry-free check on $E = \mathbb R$ with $R(w) = w^2/2$ accompanies the draft.
The Bregman divergence of the log-sum-exp conjugate on $\mathbb R^d$ is written with explicit coordinate sums, and its gradient is stated as a Fréchet derivative, because Fin d → ℝ carries the sup norm in Mathlib.
The theorem has no $O(\cdot)$ ; all constants are the paper's.
Not included: Theorem 2.15 and Corollary 2.16 (the $\|z_t\|_\infty^2$ bound via strong convexity), Theorem 2.21 (which rests on Lemma 2.19), Theorem 2.23 (unnormalized EG, in the Winnow mission of this series), Theorem 3.1 and Corollary 4.2.

Welcome contributions: proofs of the three milestones and of the goal, and general Mathlib-style lemmas on the gradient of log-sum-exp and on the Fenchel–Young inequality for conjugates defined as suprema over a set.

Selected references

S. Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning 4(2), 107–194, 2011 (© 2012). doi:10.1561/2200000018
J. Kivinen and M. K. Warmuth, Exponentiated gradient versus gradient descent for linear predictors, Information and Computation 132(1), 1–63, 1997. doi:10.1006/inco.1996.2612
Y. Freund and R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. doi:10.1006/jcss.1997.1504
N. Littlestone and M. K. Warmuth, The weighted majority algorithm, Information and Computation 108(2), 212–261, 1994. doi:10.1006/inco.1994.1009
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3), 167–175, 2003. doi:10.1016/S0167-6377(02)00231-6
E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press, 2022. arXiv:1909.05207

6 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization 1: SGD with α-Suffix Averaging Attains E[F(w̄ᵅ_T)] − F(w*) ≤ (2 + 2.5 log(1/(1−α)))G²/(αλT)Research Paper

Motivation

Stochastic gradient descent (SGD) is the default method for minimizing an expected loss $F(w)=\mathbb E_z[\ell(w,z)]$ when only noisy gradients are available, which is the situation of nearly every large-scale learning problem. When $F$ is strongly convex (for instance, any convex loss with an $\ell_2$ regularizer), information-theoretic lower bounds show that no method using $T$ noisy gradients can guarantee an error better than order $1/T$ , and some algorithms achieve this rate.

For plain SGD with step sizes $\eta_t=1/(\lambda t)$ and the standard averaged output, however, the classical analysis gives only $O(\log T/T)$ . Rakhlin, Shamir and Sridharan (arXiv:1109.5647, ICML 2012) showed that the logarithm is real for full averaging on non-smooth problems, and that a minimal change to the output, averaging only the last fraction $\alpha$ of the iterates, restores the optimal $O(1/T)$ rate. This mission formalizes that positive result, the paper's main theorem.

Timeline of the relevant results:

2007. Hazan, Agarwal and Kale (Machine Learning 69) prove an $O(\log T)$ regret bound for online gradient descent on strongly convex losses, which by online-to-batch conversion gives $O(\log T/T)$ for averaged SGD.
2009. Nemirovski, Juditsky, Lan and Shapiro (SIAM J. Optim. 19) show an $O(1/T)$ rate for the last SGD iterate when $F$ is in addition smooth.
2011. Hazan and Kale (COLT 2011) obtain $O(1/T)$ for non-smooth strongly convex problems with a different, epoch-based algorithm.
2012. Rakhlin, Shamir and Sridharan prove that SGD with full averaging can suffer $\Omega(\log T/T)$ , and that α-suffix averaging achieves $O(1/T)$ (Theorem 5).

Setting

Let $W\subseteq\mathbb R^d$ be a closed convex set containing $0$ , and let $F:\mathbb R^d\to\mathbb R$ . The function $F$ is $\lambda$ -strongly convex on $W$ ( $\lambda>0$ ) if

F(\theta x+(1-\theta)y)\le\theta F(x)+(1-\theta)F(y)-\tfrac\lambda2\theta(1-\theta)\|x-y\|^2\qquad(x,y\in W,\ \theta\in[0,1]).

A point $w^*\in W$ is a minimizer of $F$ over $W$ .

Information about $F$ comes from a stochastic gradient oracle $g(w,z)$ : at a query point $w$ , a sample $z\sim D$ is drawn and $\hat g=g(w,z)$ is returned. The oracle is unbiased in the sense that its mean $\bar g(w)=\mathbb E_{z\sim D}\,g(w,z)$ is a subgradient of $F$ relative to $W$ : $F(u)\ge F(w)+\langle u-w,\bar g(w)\rangle$ for all $u\in W$ . Its second moment is bounded: $\mathbb E_z\|g(w,z)\|^2\le G^2$ at every $w\in W$ .

Projected SGD with step sizes $\eta_t=1/(\lambda t)$ runs on an i.i.d. sample $z_1,\dots,z_T\sim D$ :

w_1=0,\qquad w_{t+1}=\Pi_W\big(w_t-\eta_t\,g(w_t,z_t)\big),

where $\Pi_W$ is the Euclidean projection onto $W$ . For $\alpha\in(0,1)$ with $(1-\alpha)T$ an integer, the α-suffix average is

\bar w^\alpha_T=\frac{w_{(1-\alpha)T+1}+\dots+w_T}{\alpha T}.

In Lean the iterates are UnderstandingML.sgdStrongIterates lam W g S, the oracle mean is oracleMean D g, the suffix average is suffixAverage lam W g S k with $k=(1-\alpha)T$ , and expectations are integrals against the product law UnderstandingML.iidLaw D T.

Formalization targets

Goal: Theorem 5

\mathbb E\big[F(\bar w^\alpha_T)-F(w^*)\big]\ \le\ \frac{2+2.5\log\frac1{1-\alpha}}{\alpha}\cdot\frac{G^2}{\lambda T},

together with the finiteness of $\mathbb E\,F(\bar w^\alpha_T)$ . The constants are the paper's.

Milestones, in the order the proof uses them

Lemma 2 (p. 12): $\mathbb E_z\|g(w,z)\|^2\le G^2$ at $w\in W$ implies $\|w-w^*\|^2\le 4G^2/\lambda^2$ .
Lemma 1 (p. 4): $\mathbb E\|w_t-w^*\|^2\le 4G^2/(\lambda^2t)$ for every $t\ge1$ .
(3) (p. 6): $\sum_{t=k+1}^T\mathbb E\langle g_t,w_t-w^*\rangle\le\sum_{t=k+1}^T\frac{\eta_tG^2}2+\sum_{t=k+1}^T\frac{\mathbb E\|w_t-w^*\|^2-\mathbb E\|w_{t+1}-w^*\|^2}{2\eta_t}$ .
App. B.6, convexity display (p. 18): $\sum_{t}\mathbb E\langle g_t,w_t-w^*\rangle\ge\sum_t\mathbb E[F(w_t)-F(w^*)]\ge\alpha T\,\mathbb E[F(\bar w^\alpha_T)-F(w^*)]$ .
App. B.6, penultimate bound (p. 18): $\mathbb E[F(\bar w^\alpha_T)-F(w^*)]\le\frac{2G^2}{\alpha T\lambda}(1+H)+\frac{G^2}{2\alpha T\lambda}H$ with $H=\sum_{t=(1-\alpha)T+1}^T 1/t$ .
App. B.6, harmonic bound (p. 18): $H\le\log\frac1{1-\alpha}$ .

Significance

Theorem 5 shows that the suboptimal $\log T$ factor of averaged SGD on non-smooth strongly convex problems is an artifact of which iterates are averaged, not of the gradient steps themselves: the same iterates, averaged over a constant fraction at the end, reach the minimax-optimal $O(G^2/(\lambda T))$ rate up to constants. This matches Hazan and Kale's guarantee with an unmodified algorithm, and the same paper's lower bound shows that full averaging cannot match it.

The result is proved in the paper; nothing in it is formalized. The platform holds the Understanding Machine Learning SGD model and its $O(\log T/T)$ bound for full averaging (UnderstandingML.sgd_strongly_convex), but no $O(1/T)$ rate for SGD on a non-smooth objective. The mission produces a machine-checked proof of Theorem 5 with its explicit constants and, along the way, of Lemma 1 (the $O(1/t)$ mean-square convergence of the last iterate), which is reused by every $O(1/T)$ analysis of SGD with step sizes $1/(\lambda t)$ , including the paper's smooth-case Theorems 1 and 2.

Difficulty

The obvious argument, the online-gradient-descent regret bound summed over all rounds and divided by $T$ , produces $\sum_{t\le T}\eta_t G^2\approx G^2\log T/\lambda$ and so cannot avoid the logarithm. Discarding early iterates does not by itself help: the resulting bound depends on the distance $\mathbb E\|w_t-w^*\|^2$ of the iterate at which the suffix starts, at the scale $1/t$ , and the regret analysis says nothing about individual iterates of a non-smooth problem.

The formal difficulties are probabilistic. The iterates are random vectors built by composing a measurable oracle with a projection defined by choice; conditioning on the past to evaluate $\mathbb E\langle g(w_t,z_t),w_t-w^*\rangle$ requires the product structure of the sample; and every expectation must be shown finite, including that of $F(\bar w^\alpha_T)$ with $F$ not assumed measurable.

Formalization scope

Space. $\mathbb R^d$ with the Euclidean inner product (UnderstandingML.Vec d); the paper allows any Hilbert space.
Domain. W closed and convex with 0 ∈ W (the paper's $w_1=0\in W$ ; closedness makes $\Pi_W$ well defined).
Strong convexity. Mathlib's StrongConvexOn W lam F with modulus $\frac\lambda2\|x-y\|^2$ , equivalent to the paper's (1) when subgradients relative to $W$ exist at every point, which the oracle provides.
Oracle. IsSubgradientOracleOn W F D g: for $w\in W$ , $g(w,\cdot)$ is integrable and its mean is a subgradient of $F$ relative to $W$ . The oracle is jointly measurable and $D$ is a probability measure. The subgradient condition is not global: $F$ is only assumed convex on $W$ .
Second moment. $\int^{-}\|g(w,z)\|^2\,dD\le G^2$ at every $w\in W$ (the paper's "regardless of how the iterates evolve"). Theorem 5's statement on p. 6 prints $\mathbb E\|\hat g_t\|^2\le G$ ; the standing assumption on p. 3 and the proof use $G^2$ , which is what is formalized.
Indices. sgdStrongIterates … t is the paper's $w_{t+1}$ ; the suffix average runs over indices $k,\dots,T-1$ , $k=(1-\alpha)T$ , passed as a natural number with $(k:\mathbb R)=(1-\alpha)T$ , which encodes that $\alpha T$ and $(1-\alpha)T$ are integers.
Logarithm. Real.log, the natural logarithm.
Expectations. Every Bochner integral in a conclusion is accompanied by an integrability conjunct, and nonnegative quantities in Lemma 1 are lower Lebesgue integrals, so no bound holds through Lean's default value $0$ for non-integrable functions. The bounds are stated for the expectation over $S\sim D^T$ ; a pathwise version, or one in which $\hat g$ itself (rather than its mean) is a subgradient, would be a different and false or easier theorem.

Infrastructure a complete development needs: measurability of the projected iterates in the sample, the one-step conditional-expectation identity $\mathbb E\langle g(w_t,z_t),w_t-w^*\rangle=\mathbb E\langle\bar g(w_t),w_t-w^*\rangle$ for the product law, and the integral comparison $\sum_{t=k+1}^T 1/t\le\log(T/k)$ . The first two are reusable for the companion missions on the same paper and for any SGD analysis built on sgdStrongIterates. Proofs of any milestone, and of reusable lemmas about iidLaw and sgdStrongIterates, are welcome.

Selected references

A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7, 2012. https://arxiv.org/abs/1109.5647
E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011. https://proceedings.mlr.press/v19/hazan11a.html
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19 (2009) 1574–1609. https://doi.org/10.1137/070704277
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Ch. 14. https://doi.org/10.1017/CBO9781107298019

10 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets 1: SAG with Step Size 1/(2nL) Converges Linearly at Rate (1 − μ/(8Ln))ᵏResearch Paper

Motivation

Many problems in machine learning and statistics minimize an average of $n$ smooth losses, one per training example: regularized least squares, logistic regression, and other forms of empirical risk minimization. Two classical families of methods attack such finite sums. The full gradient method evaluates all $n$ component gradients per iteration and converges linearly for strongly convex objectives, but each iteration costs $n$ gradient evaluations. The stochastic gradient method evaluates a single component gradient per iteration, so its iterations are cheap, but it converges only sublinearly, at rate $O(1/k)$ , even under strong convexity.

Le Roux, Schmidt and Bach (arXiv:1202.6258, NIPS 2012) introduced the stochastic average gradient (SAG) method, which keeps a table of the most recently evaluated gradient of every component and moves along their average. It evaluates one component gradient per iteration, like the stochastic gradient method, and the paper proves that it nevertheless converges linearly in expectation. SAG was among the first of the variance-reduced incremental methods; SAGA (Defazio, Bach & Lacoste-Julien, 2014), SVRG (Johnson & Zhang, 2013) and their accelerated variants followed. Its predecessor, the incremental aggregated gradient method of Blatt, Hero & Gauchman (2007), selects the components cyclically and had a linear rate only for strongly convex quadratics, without an explicit constant.

This mission covers the paper's first main result, Proposition 1, which uses the step size $1/(2nL)$ . The second result, Proposition 2, for the larger step size $1/(2n\mu)$ , is a separate mission of this series.

Setting

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

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

Each $f_i$ is convex and differentiable, and its gradient $f'_i$ is Lipschitz continuous with constant $L>0$ : $\|f'_i(x)-f'_i(y)\|\le L\|x-y\|$ for all $x,y$ . The average $g$ is strongly convex with constant $\mu>0$ : the function $x\mapsto g(x)-\frac\mu2\|x\|^2$ is convex. Then $g$ has a unique minimizer $x^*$ . The gradient variance at the optimum is $\sigma^2=\frac1n\sum_{i=1}^n\|f'_i(x^*)\|^2$ .

The SAG iteration with step size $\alpha$ maintains a state $\theta^k=(y^k_1,\dots,y^k_n,x^k)$ . Starting from $x^0$ and the zero table $y^0_i=0$ , for $k\ge1$ an index $i_k$ is drawn uniformly from $\{1,\dots,n\}$ , independently of the past, and

y^k_i=\begin{cases}f'_i(x^{k-1}) & i=i_k,\\ y^{k-1}_i & \text{otherwise,}\end{cases} \qquad x^k=x^{k-1}-\frac{\alpha}{n}\sum_{i=1}^n y^k_i .

The table is refreshed before the iterate moves, so $x^k$ uses the new gradient. Expectations are over the indices $i_1,\dots,i_k$ only; the data are fixed.

Formalization targets

Goal: Proposition 1 (p. 5)

With the constant step size $\alpha=\frac1{2nL}$ , for every $k\ge1$ ,

\mathbb E\big[\|x^k-x^*\|^2\big]\le\Big(1-\frac{\mu}{8Ln}\Big)^k\Big[3\|x^0-x^*\|^2+\frac{9\sigma^2}{4L^2}\Big].

The constants are those printed in the paper.

Milestones (the steps of the proof in §A.5, pp. 16–23)

The proof tracks a quadratic Lyapunov function $Q(\theta)=(\theta-\theta^*)^\top P(\theta-\theta^*)$ with $\theta^*=(f'_1(x^*),\dots,f'_n(x^*),x^*)$ and an explicit block matrix $P$ (p. 19). The milestones, in the order the proof uses them, are:

Lemma 1 (p. 16): an exact formula for $\mathbb E[(\theta^k-\theta^*)^\top P(\theta^k-\theta^*)\mid\mathcal F_{k-1}]$ for an arbitrary block matrix $P$ with symmetric diagonal blocks.
Summed co-coercivity (p. 20): $\sum_i\|f'_i(x)-f'_i(x^*)\|^2\le nL\,(g'(x)-g'(x^*))^\top(x-x^*)$ .
Completing the square (p. 21): $s^\top Ms+s^\top t\le-\frac14t^\top M^{-1}t$ for symmetric negative definite $M$ .
The one-step difference bound for $0\le\delta\le\frac1{3n}$ and any $\alpha>0$ (p. 21).
The one-step contraction $\mathbb E[Q(\theta^k)\mid\mathcal F_{k-1}]\le(1-\frac{\mu}{8nL})Q(\theta^{k-1})$ at $\alpha=\frac1{2nL}$ (p. 22).
$\mathbb EQ(\theta^k)\le(1-\frac{\mu}{8nL})^kQ(\theta^0)$ (p. 22).
$Q(\theta)\ge\frac13\|x-x^*\|^2$ (pp. 22–23).
$Q(\theta^0)=\frac{3\sigma^2}{4L^2}+\|x^0-x^*\|^2$ for $y^0=0$ (p. 23).

Significance

Proposition 1 gives a linear rate for a method whose per-iteration cost does not depend on $n$ . Measured in passes through the data, its rate $(1-\frac{\mu}{8Ln})^{n}\approx e^{-\mu/(8L)}$ per pass is comparable to the full gradient method's, while each pass of SAG touches every component only once on average. The bound depends on the initial point only through $\|x^0-x^*\|^2$ and on the data only through $\sigma^2$ , which is zero when every component is minimized at $x^*$ .

The result is proved in the paper and has been widely re-derived, but it has no machine-checked proof that this mission is aware of. A formalization would be the first verified linear-rate theorem for SAG. Lemma 1 is an exact identity, valid for every quadratic Lyapunov function of the same block form, and is reused verbatim in the proof of Proposition 2. Milestones 2, 3 and 7 are general facts (co-coercivity, completing the square, a Schur-complement domination) that recur throughout the analysis of incremental methods.

Difficulty

The iterate $x^k$ alone is not a Markov chain: its evolution depends on the stale gradients in the table, so neither $\|x^k-x^*\|^2$ nor $g(x^k)-g(x^*)$ decreases in expectation from one step to the next. The obvious first idea, bounding $\mathbb E[\|x^k-x^*\|^2\mid\mathcal F_{k-1}]$ in terms of $\|x^{k-1}-x^*\|^2$ as for the stochastic gradient method, fails because the cross terms between the table error $y^{k-1}-f'(x^*)$ and the iterate error have no sign. The analysis must therefore control the table and the iterate jointly, through a function of the whole state $\theta^k$ ; the exact expected one-step change of a general quadratic form in $\theta^k$ (Lemma 1) is the computation everything else rests on, and it requires careful bookkeeping of block matrices.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p) and the components are indexed by Fin n with $n\ge1$ . The components $f_i$ and their gradients $f'_i$ are both given, tied by HasGradientAt; each $f_i$ is convex (§A.1, p. 13), which the proof's co-coercivity step needs; $g$ and $g'$ are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. Strong convexity is stated literally as on p. 5, as convexity of $g-\frac\mu2\|\cdot\|^2$ . The point $x^*$ is any minimizer of $g$ ; uniqueness and $g'(x^*)=0$ are consequences. The restriction $\mu\le L$ used in the proof is not assumed, since it follows from the hypotheses when $p\ge1$ .

The SAG state is a pair (table, iterate); SAG.SmallStep.step refreshes the table entry and then moves the iterate, and SAG.SmallStep.runFrom applies the steps for a given index sequence. The goal starts from the zero table and fixes the step size $\frac1{2nL}$ . The expectation is SAGA.Convex.expectIdx n k, the uniform average over all $n^k$ index sequences, which is exactly the law of $k$ independent uniform indices; a conditional expectation given $\mathcal F_{k-1}$ is the average over the next index from an arbitrary current state. Block matrices are families of $p\times p$ blocks (continuous linear maps), and Lemma 1 makes explicit the symmetry of $A$ and $c$ and the identity $\sum_if'_i(x^*)=0$ that its proof uses. The domination $Q\ge\frac13\|x-x^*\|^2$ is stated for every $n\ge1$ : the page's closing remark "for $n\ge2$ " is stronger than its own computation needs.

The goal bounds the average over all index sequences; a bound for each fixed sequence would be false, and a bound for one sequence would be a different, weaker statement. Proposition 1 is not to be formalized with a free step size, an arbitrary initial table, or a variance quantity other than $\sigma^2$ at $x^*$ : each of these changes the constant $9\sigma^2/(4L^2)$ .

Needed infrastructure: algebra of finite sums of inner products over block families, the tower property for the uniform average over index sequences, co-coercivity of convex smooth functions (published on the platform as ConvexOptAlg.SmoothGD.eq_3_6), and strong-convexity monotonicity of the gradient. Proofs of individual milestones are welcome, as are alternative proofs of the goal that bypass the Lyapunov function.

Selected references

N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012; arXiv:1202.6258v4, 2013. https://arxiv.org/abs/1202.6258
D. Blatt, A. O. Hero, H. Gauchman, A Convergent Incremental Gradient Method with a Constant Step Size, SIAM J. Optim. 18(1), 2007. 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. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method with Support for Non-Strongly Convex Composite Objectives, NIPS 2014. https://arxiv.org/abs/1407.0202
R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. https://papers.nips.cc/paper/4937

14 thms4 active usersReviewed

Probability Theoretical Computer Science·Captain: mikedeng1

What Can We Learn Privately? II: Parity Functions Are Privately PAC Learnable from O(d log(1/β)/(εα)) ExamplesResearch Paper

Learning parities under differential privacy

Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) requires a randomized algorithm's output distribution to change little when one individual's record is changed. PAC learning asks an algorithm to output, from i.i.d. labeled examples, a hypothesis whose error is small with high probability. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith (arXiv:0803.0924v3; SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090) asked which concept classes can be learned under both requirements at once. All theorem, page and display numbers in this mission are those of the arXiv v3.

Their generic learner (§3, the subject of mission I of this series) learns every finite class privately with a polynomial number of examples, but its running time is exponential in the representation size for classes such as parity. Parity functions are the standard example of a class that is learnable efficiently by linear algebra and not learnable with statistical queries (Kearns, 1998; Blum et al., 1994), a model that was then the main known source of efficient private learners (Blum, Dwork, McSherry and Nissim, 2005). Section 4 of the paper gives an efficient private PAC learner for parity. The result separates efficient private learning from statistical-query learning, and the local (randomized-response) model from the centralized one (missions III–V).

Setting

For $d \ge 1$ and $r \in \{0,1\}^d$ , the parity function $c_r(x) = r \odot x$ is the inner product of $r$ and $x$ modulo 2; PARITY is $\{c_r : r \in \{0,1\}^d\}$ . A database is $z = (z_1,\dots,z_n)$ with $z_i = (x_i, y_i) \in \{0,1\}^d \times \{0,1\}$ . Two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$ , identified with the law $A(z)$ of its output, is $\varepsilon$ -differentially private if $\Pr[A(z) \in S] \le e^{\varepsilon}\Pr[A(z') \in S]$ for all neighbors $z, z'$ and all sets $S$ of outputs. $\mathrm{Lap}(s)$ is the Laplace distribution with density $\frac{1}{2s}e^{-|x|/s}$ .

For $S \subseteq [n]$ , $V_S \subseteq \mathbb Z_2^d$ is the solution space of the linear system $\{x_i \odot r = y_i : i \in S\}$ . The basic learner $\mathcal A(z,\varepsilon)$ outputs $\bot$ with probability $1/2$ ; otherwise it puts each $i \in [n]$ into $S$ independently with probability $p = \varepsilon/4$ and outputs $c_{r^*}$ for $r^*$ uniform in $V_S$ , or $\bot$ if $V_S = \emptyset$ .

The amplified learner $\mathcal A^*(z,\varepsilon,\alpha,\beta)$ sets $\beta' = \beta/2$ , $\alpha' = \alpha/5$ , $k = \lceil\log_{4/3}(1/\beta')\rceil$ , $n' = \lceil cd/(\varepsilon\alpha')\rceil$ , $s = \lceil (c'k/(\alpha'\varepsilon))\log_2(k/\beta')\rceil$ for constants $c, c'$ . If $n \le kn' + s$ it returns "insufficient samples". Otherwise it runs $\mathcal A$ on $k$ disjoint blocks of $n'$ examples, obtaining $h_1,\dots,h_k$ . It perturbs each training error on the next $s$ examples by independent $\mathrm{Lap}(k/(s\varepsilon))$ noise and outputs the $h_j$ with the least perturbed error.

For a distribution $\mathcal X$ on $\{0,1\}^d$ and a target $c_r$ , the error of $c_{r'}$ is $\mathrm{err}(c_{r'}) = \Pr_{x\sim\mathcal X}[c_{r'}(x) \ne c_r(x)]$ , and probabilities of the learner's success are over $x_1,\dots,x_n \sim \mathcal X$ i.i.d., $z_i = (x_i, c_r(x_i))$ , and the learner's coins.

Formalization targets

Goal: Theorem 4.4

There are constants $c, c', C > 0$ such that for all $d \ge 1$ , $0 < \varepsilon \le 1/2$ , $\alpha, \beta \in (0,1/2)$ : $\mathcal A^*(\cdot,\varepsilon,\alpha,\beta)$ is $\varepsilon$ -differentially private on databases of every size, and

n \ge C\,\frac{(d + \log_2(1/\beta))\log_2(1/\beta)}{\varepsilon\alpha} \implies \Pr\big[\mathcal A^* \text{ outputs } h^* \text{ with } \mathrm{err}(h^*) \le \alpha\big] \ge 1-\beta

for every distribution $\mathcal X$ and every target $c_r$ . When $\log_2(1/\beta) \le d$ the bound is the paper's $O(d\log(1/\beta)/(\varepsilon\alpha))$ . The constants are fixed before all other parameters. The goal is literally the conjunction of Lemma 4.5 and Lemma 4.6.

Milestones

\text{Thm 2.3 (Laplace mechanism)},\quad \text{Claim 2.2 (composition)},\quad \text{Thm A.1 (Chernoff)},\quad \text{Occam's razor for } |H| = 2^d,

\text{Lemma 4.1: } n \ge \tfrac{8}{\varepsilon\alpha}(d\ln 2 + \ln 4) \Rightarrow \Pr[\mathcal A(z,\varepsilon) = h,\ \mathrm{err}(h)\le\alpha] \ge \tfrac14,

|V_T| \le 2|V_{T\cup\{i\}}| \text{ if } V_{T\cup\{i\}} \ne \emptyset,\quad \text{Claim 4.3},\quad \text{Lemma 4.2 (}\mathcal A\text{ private)},\quad \text{Lemma 4.5 (}\mathcal A^*\text{ private)},\quad \text{Lemma 4.6 (}\mathcal A^*\text{ learns)}.

Significance

The theorem shows that the restriction to private algorithms does not separate efficient learnability from statistical-query learnability: parity is efficiently and privately PAC learnable, yet not SQ learnable. Its sample complexity exceeds the non-private $O((d + \ln(1/\beta))/\alpha)$ by a factor $O(\ln(1/\beta)/\varepsilon)$ (remark, p. 18). The private amplification step (private model selection with Laplace-perturbed test errors) is a general technique that converts any private learner with constant success probability into a private PAC learner.

The result is proved in the paper; none of it is machine-checked as far as we know. The mission produces a formal library of the basic privacy calculus (Laplace mechanism, composition and post-processing), the $\mathbb Z_2$ solution-space estimate behind the privacy of $\mathcal A$ , and the analysis of both learners. Formalizing it also repairs the paper's statement: the printed sample bound fails when $\log(1/\beta)$ is large compared with $d$ (see the scope section), and the base of the logarithm defining $k$ is misprinted.

Difficulty

The obvious private learner, "solve the linear system on all examples and output a random solution", is not private. One changed example can make the system inconsistent and turn every hypothesis output into failure, so the output law on neighboring databases differs by an unbounded factor. Two devices restore privacy: subsampling each example with probability $\varepsilon/4$ , and failing with probability $1/2$ unconditionally. The privacy proof then needs a quantitative fact about $\mathbb Z_2$ : adding one consistent equation at most halves the solution space. The proof must also handle databases labeled by no parity at all, where solution spaces are empty.

Utility has its own difficulty. The amplified learner selects among candidates through noisy test errors, so three failure events (no good candidate, unrepresentative test set, large Laplace noise) must be bounded together. The sizes $k$ , $n'$ , $s$ must also be shown to fit inside the claimed sample bound.

Formalization scope

Bits are ZMod 2; $\{0,1\}^d$ is Fin d → ZMod 2; $c_r(x)$ is dotProduct r x. Databases are Fin n → (Fin d → ZMod 2) × ZMod 2, with 0-based indices.
An algorithm is the law of its output. $\mathcal A$ 's output is Option (Fin d → ZMod 2) (none = $\bot$ ). $\mathcal A^*$ 's output is "insufficient samples", $\bot$ , or a hypothesis $c_r$ . Every set of outputs is measurable, and differential privacy is required for all measurable sets.
The distribution $\mathcal X$ is a PMF on the finite set $\{0,1\}^d$ . The probability over the examples is a finite sum weighted by $\prod_i \mathcal X(x_i)$ , and $\bot$ has error 1.
Corrections and explicit hypotheses. (1) $k = \lceil\log_{4/3}(1/\beta')\rceil$ : the printed base $3/4$ gives $k \le 0$ , and the proof needs $(3/4)^k \le \beta'$ . (2) Sizes are ceilings; $\log$ is base 2 and $\ln$ is natural, as on p. 8. (3) Privacy is stated for $0 < \varepsilon \le 1/2$ : the proof of Lemma 4.2 uses $\varepsilon \le 1/2$ , and its step $2p/(1-p) + 1 \le \varepsilon + 1$ fails beyond that. Utility statements need only $0 < \varepsilon \le 4$ , so that $p = \varepsilon/4$ is a probability. (4) The printed bound $O(d\log(1/\beta)/(\varepsilon\alpha))$ is false when $\log(1/\beta) \gg d$ , because $\mathcal A^*$ refuses unless $n > kn' + s$ and $s$ grows like $\log^2(1/\beta)/(\varepsilon\alpha)$ . Utility is therefore stated with the bound $C(d + \log_2(1/\beta))\log_2(1/\beta)/(\varepsilon\alpha)$ , the order of $kn' + s$ , which equals the printed order whenever $\log_2(1/\beta) \le d$ . The privacy conjunct does not depend on the sample bound. (5) A $\bot$ candidate does not take part in the argmin, and ties go to the least index. (6) Lemma 4.1 assumes $\alpha \le 1/2$ , which its proof uses. (7) Claim 4.3 is stated in product form (no division). (8) Theorem 2.3 takes any positive bound $\Delta$ on the global sensitivity.
"Efficiently" (polynomial running time) is not modelled.
Ruling out trivial readings. The constants $c, c', C$ are existentially quantified once, outside every other quantifier. A constant chosen after $d$ , $\varepsilon$ , $\alpha$ , $\beta$ would make the utility claim trivial. Success requires an actual hypothesis output, so "insufficient samples" and $\bot$ are failures. Privacy quantifies over all databases, not only consistently labeled ones.
Reused results: ComputationalLearning.chernoff_bounds (Theorem A.1) and ComputationalLearning.occam_cardinality (Occam's razor), both proved on the platform.
Contributions welcome: proofs of the privacy calculus (Theorem 2.3, Claim 2.2) for general use, the $\mathbb Z_2$ halving lemma, and the utility analysis. The first two are reusable well beyond this mission.

Selected references

S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090
C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. DOI 10.1007/11681878_14
A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical Privacy: The SuLQ Framework, PODS 2005. DOI 10.1145/1065167.1065184
M. Kearns, Efficient Noise-Tolerant Learning from Statistical Queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351
A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly Learning DNF and Characterizing Statistical Query Learning Using Fourier Analysis, STOC 1994. DOI 10.1145/195058.195147
M. Kearns, U. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994. DOI 10.7551/mitpress/3897.001.0001

14 thms4 active usersReviewed

Completed

Convex Optimization Linear algebra Statistics·Captain: mikedeng1

Nuclear-Norm Penalization and Optimal Rates for Noisy Low-Rank Matrix Completion 1: If λ ≥ 2‖M‖∞, the Nuclear-Norm Penalized Estimator Obeys Sharp Oracle Inequalities with Leading Constant 1Research Paper

Motivation

Many estimation problems in statistics and machine learning ask for an unknown matrix observed only through noisy linear measurements: matrix completion (recover a large matrix from a few noisy entries, as in collaborative filtering), multi-task regression, and quantum state tomography. A common structural prior is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of the singular values. Penalizing a least-squares criterion by the nuclear norm gives an estimator that can be computed by convex optimization.

Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a nuclear-norm penalized estimator in the general trace regression model and prove that it satisfies sharp oracle inequalities: the excess prediction error is bounded by the best approximation error over a class of matrices with leading constant exactly $1$ , plus a remainder governed by either the nuclear norm ("slow rate") or the rank ("fast rate") of the approximating matrix. A distinctive feature of their estimator is that it uses the known design distribution $\Pi$ , which the empirical-risk estimators of the earlier literature (Candès and Plan 2010; Rohde and Tsybakov 2011; Negahban and Wainwright 2011) do not exploit; for noisy matrix completion the previously available bounds were suboptimal. Their Theorem 1 is the deterministic core from which the paper's matrix completion rates (Theorem 4) follow by bounding one random matrix in operator norm.

Setting

Let $(X_i,Y_i)$ , $i=1,\dots,n$ , be random pairs, $X_i$ a real $m_1\times m_2$ matrix and $Y_i$ a real number, satisfying the trace regression model

\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle,\qquad \langle A,B\rangle=\operatorname{tr}(A^\top B),

for an unknown matrix $A_0$ . Let $\Pi_i$ be the law of $X_i$ and $\Pi=\frac1n\sum_i\Pi_i$ . The $L_2(\Pi)$ inner product and semi-norm are

\langle A,B\rangle_{L_2(\Pi)}=\frac1n\sum_{i=1}^n\mathbb E\big(\langle A,X_i\rangle\langle B,X_i\rangle\big),\qquad \|A\|^2_{L_2(\Pi)}=\langle A,A\rangle_{L_2(\Pi)}.

For a matrix $A$ with singular values $\sigma_j(A)$ , $\|A\|_1=\sum_j\sigma_j(A)$ is the nuclear norm, $\|A\|_2$ the Frobenius norm, and $\|A\|_\infty=\sigma_1(A)$ the operator norm. If $A=\sum_{j=1}^r\sigma_ju_jv_j^\top$ is a singular value decomposition, the pair $(S_1,S_2)=(\operatorname{span}\{u_j\},\operatorname{span}\{v_j\})$ is the support of $A$ , and $P_S$ is the orthogonal projector onto $S$ .

Given a set $\mathbb A$ of matrices and $\lambda>0$ , the estimator is

\hat A^\lambda\in\operatorname*{argmin}_{A\in\mathbb A}L_n(A),\qquad L_n(A)=\|A\|^2_{L_2(\Pi)}-\Big\langle\frac2n\sum_{i=1}^nY_iX_i,A\Big\rangle+\lambda\|A\|_1 .

The random matrix

\mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big)

carries all the noise. Assumption 1 asks for a constant $\mu>0$ with $\|A\|^2_{L_2(\Pi)}\ge\mu^{-2}\|A\|_2^2$ for all $A\in\mathbb A-\mathbb A$ .

Formalization targets

Goal: Theorem 1

If $\lambda\ge2\|\mathbf M\|_\infty$ , then for any set $\mathbb A$

\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}\le\inf_{A\in\mathbb A}\Big[\|A-A_0\|^2_{L_2(\Pi)}+2\lambda\|A\|_1\Big],\tag{2.3}

and if moreover $\mathbb A$ is convex and Assumption 1 holds,

\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}\le\inf_{A\in\mathbb A}\Big[\|A-A_0\|^2_{L_2(\Pi)}+\Big(\tfrac{1+\sqrt2}{2}\Big)^2\mu^2\lambda^2\operatorname{rank}(A)\Big],\tag{2.4}

and, for every $A\in\mathbb A$ with support $(S_1,S_2)$ ,

\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}+(\lambda-2\|\mathbf M\|_\infty)\|P_{S_1^\perp}\hat A^\lambda P_{S_2^\perp}\|_1\le\|A-A_0\|^2_{L_2(\Pi)}+\Big(\tfrac{1+\sqrt2}{2}\Big)^2\mu^2\lambda^2\operatorname{rank}(A).\tag{2.5}

The theorem is deterministic: it holds at every realization of the sample at which $\lambda\ge2\|\mathbf M\|_\infty$ .

Milestones

The milestones follow the paper's proof: the subdifferential of the nuclear norm (2.1); the basic inequality of p. 7 and the slow-rate bound (2.3); the first-order condition (2.6); the identity (2.9) and the facts (2.10); the inequality (2.11); the decomposition bound (2.12)–(2.14); the bound on $\Lambda$ via (2.15); and the combined inequality (2.17). The rank bound (2.16) is included as a supporting statement (not a milestone).

Significance

Theorem 1 separates the statistical problem into a deterministic oracle inequality and a single probabilistic estimate, $\|\mathbf M\|_\infty\le\lambda/2$ . Any concentration bound for $\|\mathbf M\|_\infty$ (matrix Bernstein for uniform sampling, Gaussian bounds for fixed designs) then gives a rate. The paper uses it to obtain matrix completion rates which its minimax lower bounds show to be optimal up to logarithmic factors on the class of matrices of rank at most $r$ with entries bounded by $a$ . The leading constant $1$ means the bounds remain informative when $A_0$ is not low rank but only well approximated by low-rank matrices.

The result has been proved on paper since 2011; to our knowledge no machine-checked proof exists. A formal proof requires the subdifferential of the nuclear norm and its interplay with the singular-subspace projections, which are reusable for every nuclear-norm method (singular value thresholding, robust PCA, multi-task learning).

Difficulty

The slow-rate bound (2.3) is a short computation from the definition of a minimizer and trace duality. The fast-rate bounds (2.4)–(2.5) are not: a minimizer comparison alone gives only $\lambda\|\hat A^\lambda-A\|_1$ as remainder, which does not scale with $\operatorname{rank}(A)$ . One needs the variational inequality (2.6) over the convex set $\mathbb A$ , the exact description (2.1) of the nuclear-norm subdifferential at an arbitrary comparison matrix $A$ , and a decomposition of $\langle\mathbf M,\hat A^\lambda-A\rangle$ along the support of $A$ in which the component orthogonal to the support is controlled in operator norm and the rest in Frobenius norm. Formally, (2.1) itself requires identifying the abstract singular values with a given decomposition and characterizing the operator-norm ball as the dual of the nuclear norm.

Formalization scope

Matrices are RealMatrix m₁ m₂ = Matrix (Fin m₁) (Fin m₂) ℝ, with the published MatrixCompletion definitions supplying the Frobenius inner product matrixInner, nuclearNorm (sum of Mathlib's singular values), spectralNorm (operator norm), frobeniusNorm, SVD data SVD A r and the projections twoSidedSingularProjection ( $P_{S_1}\cdot P_{S_2}$ ), tangentProjection ( $\mathcal P_A$ ) and normalProjection ( $P_{S_1^\perp}\cdot P_{S_2^\perp}$ ). The sample lives on a probability space (Ω, P) with 0 < n; expectations of matrices are entrywise. Conventions committed to:

Realization-wise statements. $\omega$ is fixed; $\hat A$ is any matrix with $\hat A\in\mathbb A$ and $L_n(\hat A)\le L_n(A)$ for all $A\in\mathbb A$ . Existence of a minimizer is not asserted.
Infima are stated as the bound for every $A\in\mathbb A$ (equivalent; no real sInf is used).
The model (1.1) is the conditional expectation of $Y_i$ given the $\sigma$ -algebra generated by the entries of $X_i$ .
Added regularity, not printed in the paper: every entry of $X_i$ is measurable and square integrable, $Y_i$ is measurable and integrable, and $Y_i(X_i)_{jk}$ is integrable. Without these, Lean's Bochner integral returns $0$ and $\|\cdot\|_{L_2(\Pi)}$ and $\mathbf M$ would be meaningless.
Independence of the pairs is not assumed; the proof does not use it.
Supports are given by SVD data; bounds use A.rank.
Corrected statement. The first fact of (2.10), $\|\sum_ju_jv_j^\top\|_\infty=1$ , is false for $A=0$ (empty sum); the milestone assumes $r>0$ .
Steps the paper states for $\hat A^\lambda$ or $\mathbf M$ but which hold for arbitrary matrices ((2.9), (2.10), (2.12)–(2.16)) are stated for arbitrary matrices.

Ruling out trivializations: the goal states (2.3)–(2.5) with the paper's constants and remainder terms, not the intermediate bound (2.17), and $\hat A$ is pinned down as a minimizer over $\mathbb A$ , not an arbitrary matrix.

Welcome contributions: proofs of the nuclear-norm subdifferential (2.1) and of the projection facts, which are reusable well beyond this mission, and the measure-theoretic identity $\frac1n\sum_i\mathbb E(Y_iX_i)=\frac1n\sum_i\mathbb E(\langle A_0,X_i\rangle X_i)$ from the model.

Selected references

V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (the source of this mission); Ann. Statist. 39(5), 2302–2329, 2011. https://arxiv.org/abs/1011.6256, https://doi.org/10.1214/11-AOS894
G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992 (reference [28] of the source; the description (2.1) of the nuclear-norm subdifferential). https://doi.org/10.1016/0024-3795(92)90407-2
E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 925–936, 2010. https://doi.org/10.1109/JPROC.2009.2035722
A. Rohde, A. B. Tsybakov, Estimation of high-dimensional low-rank matrices, Ann. Statist. 39(2), 887–930, 2011. https://doi.org/10.1214/10-AOS860
S. Negahban, M. J. Wainwright, Estimation of (near) low-rank matrices with noise and high-dimensional scaling, Ann. Statist. 39(2), 1069–1097, 2011. https://doi.org/10.1214/10-AOS850

19 thms4 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Pegasos: Primal Estimated Sub-Gradient Solver for SVM: Mini-Batch Pegasos Has Average Instantaneous Objective Within c(1+ln T)/(2λT) of the SVM Optimum'sResearch Paper

Motivation

The support vector machine (SVM) is a linear classifier trained by minimising a regularised hinge loss. For training sets with millions of examples, solving the SVM problem to high accuracy by interior-point or dual decomposition methods is too slow, and what is needed is an algorithm whose cost per iteration does not grow with the number of examples. Pegasos (Primal Estimated sub-GrAdient SOlver for SVM), introduced by Shalev-Shwartz, Singer and Srebro in 2007 and analysed in its final form by Shalev-Shwartz, Singer, Srebro and Cotter in Mathematical Programming (2011, doi:10.1007/s10107-010-0420-4), is a stochastic sub-gradient method on the primal SVM objective with step size $1/(\lambda t)$ . Its analysis showed that the number of iterations needed for accuracy $\epsilon$ is $\tilde O(1/(\lambda\epsilon))$ , independent of the training-set size, and the method became a standard baseline for large-scale linear SVM training.

The analysis rests on a logarithmic-regret bound for online gradient descent on strongly convex functions, due to Hazan, Agarwal and Kale (Machine Learning 69, 2007), which the paper re-proves for non-smooth functions as its Lemma 1 and then applies to the Pegasos iterates in its Theorem 1.

Setting

A training set consists of $m$ examples $(x_i, y_i)$ , $i\in[m]$ , with $x_i\in\mathbb R^n$ and labels $y_i\in\{+1,-1\}$ . The hinge loss of a weight vector $w$ on $(x,y)$ is $\ell(w;(x,y)) = \max\{0,\,1 - y\langle w, x\rangle\}$ . For a regularisation parameter $\lambda>0$ , the SVM objective (Eq. (1)) is

f(w) = \frac\lambda2\|w\|^2 + \frac1m\sum_{i=1}^m \ell(w;(x_i,y_i)),

and $w^\star$ denotes a minimiser of $f$ (Eq. (9)). For a mini-batch $A$ of $k\ge1$ example indices, the instantaneous objective (Eq. (7)) is

f(w;A) = \frac\lambda2\|w\|^2 + \frac1k\sum_{i\in A}\ell(w;(x_i,y_i)).

Mini-batch Pegasos (Fig. 2 of the paper) starts at $w_1 = 0$ . At each round $t = 1, 2, \dots$ it receives a mini-batch $A_t$ , forms the sub-gradient

\nabla_t = \lambda w_t - \frac1k\sum_{i\in A_t}\mathbb 1\bigl[y_i\langle w_t, x_i\rangle < 1\bigr]\,y_i x_i \qquad (8)

of $f(\cdot;A_t)$ at $w_t$ , and sets $w_{t+1} = w_t - \eta_t\nabla_t$ with $\eta_t = 1/(\lambda t)$ . Optionally it then applies the projection step (6), $w_{t+1}\leftarrow\min\{1,(1/\sqrt\lambda)/\|w_{t+1}\|\}\,w_{t+1}$ , which maps $w_{t+1}$ to the closest point of the Euclidean ball of radius $1/\sqrt\lambda$ . A function $g$ is $\lambda$ -strongly convex if $g(w) - \frac\lambda2\|w\|^2$ is convex, and $v$ is a sub-gradient of a convex $g$ at $w_0$ if $g(w) - g(w_0)\ge\langle v, w - w_0\rangle$ for every $w$ .

In the Lean development these objects are svmObj, instObj, subgrad, projBall and run in the namespace Pegasos.Analysis; the hinge loss is UnderstandingML.hingeLoss, sub-gradients are UnderstandingML.IsSubgradient, and " $z$ is the projection of $v$ onto $B$ " is LogRegretOCO.OGD.IsProj B v z.

Formalization targets

Goal: Theorem 1

Assume $\|x_i\|\le R$ for every $i$ , and set $c = (\sqrt\lambda + R)^2$ when the projection step is performed and $c = 4R^2$ when it is not. Then for every sequence of mini-batches and every $T\ge3$ ,

\frac1T\sum_{t=1}^T f(w_t;A_t) \;\le\; \frac1T\sum_{t=1}^T f(w^\star;A_t) + \frac{c\,(1+\ln T)}{2\lambda T}.

The constants are the paper's and are stated exactly; a version with a single constant for both variants, or with an unspecified constant, is a weaker theorem.

Milestones

Eq. (10): for $\lambda$ -strongly convex $g$ with sub-gradient $v$ at $w$ , $\langle w - u, v\rangle\ge g(w) - g(u) + \frac\lambda2\|w-u\|^2$ .
Eq. (11): one projected step satisfies $\langle w_t - u,\nabla_t\rangle\le\frac{\|w_t-u\|^2 - \|w_{t+1}-u\|^2}{2\eta_t} + \frac{\eta_t}2G^2$ (an already-proved platform theorem, stated with a factor 2).
Lemma 1: projected sub-gradient steps $\eta_t = 1/(\lambda t)$ on $\lambda$ -strongly convex $f_t$ with $\|\nabla_t\|\le G$ satisfy $\frac1T\sum f_t(w_t)\le\frac1T\sum f_t(u) + \frac{G^2(1+\ln T)}{2\lambda T}$ for all $u\in B$ .
The vector (8) is a sub-gradient of $f(\cdot;A)$ ; $f(\cdot;A)$ is $\lambda$ -strongly convex; the projection step (6) is the projection onto the ball of radius $1/\sqrt\lambda$ .
The gradient bounds: $\|\nabla_t\|\le\sqrt\lambda + R$ with projection; Eq. (13), $w_{t+1} = \frac1{\lambda t}\sum_{i\le t}v_i$ , and $\|\nabla_t\|\le 2R$ without.
$\|w^\star\|\le 1/\sqrt\lambda$ .

Significance

Theorem 1 is the deterministic core of every guarantee in the paper. Taking expectations over uniformly random mini-batches turns its left side into the expected objective of the iterates and its right side into $f(w^\star)$ plus the rate, which yields the $\tilde O(1/(\lambda\epsilon))$ iteration bound and, via Markov-type arguments, the high-probability bounds of the later sections. Because the bound holds for every sequence of mini-batches, it is also an online-learning regret bound for the sequence of instantaneous objectives.

The result is proved in the paper and is classical. To our knowledge it has no machine-checked proof. Formalizing it produces a verified logarithmic-regret lemma for non-smooth strongly convex sub-gradient descent with an arbitrary closed convex feasible set (the platform currently has the twice-differentiable version with a bounded feasible set), a verified sub-gradient calculus for the regularised hinge loss, and an exact treatment of the Pegasos iteration including both the projected and unprojected variants.

Difficulty

The obvious argument applies Lemma 1 with $B$ the ball of radius $1/\sqrt\lambda$ in both variants and $G$ the sup of $\|\nabla_t\|$ over that ball. This fails twice. Without the projection step the iterates are not confined to that ball, so a separate argument (the closed form (13)) is needed to bound them, and it gives the different constant $4R^2$ . With projection, Lemma 1 requires the comparator $w^\star$ to lie in the ball, and $\|w^\star\|\le1/\sqrt\lambda$ is not implied by the elementary comparison $f(w^\star)\le f(0)\le1$ , which only gives $\|w^\star\|\le\sqrt{2/\lambda}$ ; the paper obtains the sharp radius through duality. In Lemma 1 itself, the telescoping only closes because the step size $1/(\lambda t)$ is matched exactly to the strong-convexity modulus; any off-by-one in the step indexing breaks the cancellation.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), examples are indexed by Fin m, labels are real numbers with the hypothesis $y_i\in\{+1,-1\}$ , and $\lambda>0$ , $k\ge1$ are hypotheses. A mini-batch is a $k$ -tuple Fin k → Fin m: an injective tuple is a subset of size $k$ as in Fig. 2, a non-injective one is the multi-set with repetitions the paper also allows. The theorem is stated for every sequence of mini-batches A : ℕ → Fin k → Fin m; no probability space appears, because the proof never uses that the batches are random. Iterations are 1-based: run … 1 = 0, the step producing $w_{t+1}$ uses $\eta_t = 1/(\lambda t)$ and the batch $A_t$ only, and index 0 is unused. The variant is selected by a Boolean flag, and $c$ depends on it. $w^\star$ is any $w$ with $f(w^\star)\le f(w)$ for all $w$ , minimising the full objective (1), not the instantaneous ones. Strong convexity is the paper's own definition, convexity of $g - \frac\lambda2\|\cdot\|^2$ . At $w = 0$ the projection formula is evaluated with Lean's $a/0 = 0$ , which gives the intended value $0$ . The paper's display (12) has two printed slips (the sign of the $v_t$ term and $x_t$ for $x_i$ ); the Lean states the correct update, and Eq. (13) is correct as printed.

A trivializing formalization is ruled out: the goal is stated for the concrete iteration run, not for an abstract sequence assumed to be sub-gradient steps or projections, and those facts are separate milestones.

A complete development needs the sub-differential sum rule for a convex function plus a quadratic, convexity of the hinge loss, the variational characterisation of the projection onto a ball, the harmonic-sum bound $\sum_{t\le T}1/t\le1+\ln T$ , and a proof of $\|w^\star\|\le1/\sqrt\lambda$ (through duality or a direct optimality argument). Lemma 1 and the sub-gradient lemmas are reusable for any strongly convex stochastic sub-gradient method. Proofs of any milestone, and alternative proofs of the bound on $\|w^\star\|$ that avoid the dual problem, are welcome.

Selected references

S. Shalev-Shwartz, Y. Singer, N. Srebro, A. Cotter, Pegasos: primal estimated sub-gradient solver for SVM, Mathematical Programming Ser. B 127 (2011) 3–30. https://doi.org/10.1007/s10107-010-0420-4
E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
S. Shalev-Shwartz, Y. Singer, N. Srebro, Pegasos: primal estimated sub-gradient solver for SVM, ICML 2007. https://doi.org/10.1145/1273496.1273598

15 thms4 active usersReviewed

Completed

Algorithmic Game Theory Probability·Captain: mikedeng1

A Simple Adaptive Procedure Leading to Correlated Equilibrium 2: Playing an Invariant Vector of the Regret Matrix (3.1) Drives Every Regret R_t(j,k) to Zero Almost SurelyResearch Paper

Motivation

A correlated equilibrium (Aumann, 1974) is a probability distribution over the strategy profiles of a game such that no player gains by deviating from the strategy it recommends. It is the natural solution concept for repeated play by adaptive agents, because the set of correlated equilibria is a polytope described by linear inequalities and, as Hart and Mas-Colell showed, it can be reached by simple learning rules that use only a player's own past payoffs and regrets.

Hart and Mas-Colell's paper (Econometrica 68 (2000) 1127–1150) has two procedures. Its Main Theorem concerns regret matching (2.2), in which a player switches away from its last strategy with probabilities proportional to its regrets; it is the subject of a companion mission. Section 3 studies a variant in which, at every period, the player plays an invariant vector of the regret matrix, and proves with Blackwell's approachability theorem (Blackwell, 1956) that the player's regrets vanish almost surely, whatever the other players do. This result, Theorem A, is the target of this mission. It is the conditional ("internal") counterpart of Hannan's no-regret property (Hannan, 1957) and the template for later internal-regret algorithms in online learning (Cesa-Bianchi and Lugosi, 2006).

Timeline. Hannan (1957) gave a procedure with vanishing unconditional regret; Blackwell (1956) proved the approachability theorem and derived a universally consistent procedure from it; Foster and Vohra (1997) obtained convergence to correlated equilibria through calibrated forecasts; Fudenberg and Levine (1995, 1999) introduced universal consistency and calibrated smooth fictitious play; Hart and Mas-Colell (2000) gave Theorem A and regret matching.

Setting

A finite game $\Gamma=(N,(S^i)_{i\in N},(u^i)_{i\in N})$ has a finite set $N$ of players, a finite nonempty strategy set $S^i$ for each player, and payoffs $u^i:S\to\mathbb R$ on $S=\prod_i S^i$ . For $s\in S$ and $k\in S^i$ , $u^i(k,s^{-i})$ is $i$ 's payoff when $i$ 's coordinate of $s$ is replaced by $k$ .

The game is played at $t=1,2,\dots$ . After the history $h_t=(s_1,\dots,s_t)$ each player chooses a mixed action, and given $h_t$ the players randomize independently. For $j\ne k$ in $S^i$ the regret of player $i$ for not having played $k$ whenever it played $j$ is

D^i_t(j,k)=\frac1t\sum_{\tau\le t:\,s^i_\tau=j}\big[u^i(k,s^{-i}_\tau)-u^i(s_\tau)\big],\qquad R^i_t(j,k)=\max\{D^i_t(j,k),0\}.

With $R^i_t(j,j):=0$ , a probability vector $q^i_t\in\Delta(S^i)$ satisfies (3.1) if

\sum_{k\in S^i}q^i_t(k)R^i_t(k,j)=q^i_t(j)\sum_{k\in S^i}R^i_t(j,k)\qquad\text{for every }j\in S^i,

i.e. $q^i_t$ is an invariant distribution of the transition matrix of regret matching. The empirical distribution of play is $z_t(s)=\frac1t|\{\tau\le t: s_\tau=s\}|$ .

Formalization targets

Goal: Theorem A (p. 1133)

If at every period $t+1$ player $i$ plays a probability vector satisfying (3.1), then, whatever the other players do,

R^i_t(j,k)\xrightarrow[t\to\infty]{}0\quad\text{almost surely, for all }j\ne k\text{ in }S^i.

Milestones (the proof of Theorem A, pp. 1135–1138)

(3.5): the nonnegative matrix with entries $\lambda(j,k)$ off the diagonal and $0$ on it has an invariant vector $q_\lambda\in\Delta(S^i)$ .
(3.4a)–(3.4b): for the vector payoff $v(s^i,s^{-i})\in\mathbb R^L$ , $L=\{(j,k):j\ne k\}$ , the quantity $\lambda\cdot v(q,s^{-i})$ equals $\sum_j\alpha(j)u^i(j,s^{-i})$ .
Blackwell's condition for $\mathbb R^L_-$ : for $\lambda\ge0$ and $q_\lambda$ solving (3.5), $\lambda\cdot v(q_\lambda,s^{-i})=0$ for every $s^{-i}$ .
Support function: $w_{\mathbb R^L_-}(\lambda)=0$ on $\mathbb R^L_+$ and $+\infty$ elsewhere.
Closest point: $D_t$ has coordinates $D^i_t(j,k)$ , the projection onto $\mathbb R^L_-$ is $[D_t]^-$ , and $\lambda(D_t)=[D_t]^+$ is the regret vector.
Blackwell's approachability theorem, "Moreover" part: the Blackwell procedure drives $\operatorname{dist}(D_t,\mathcal C)$ to $0$ almost surely against any opponent.

Companions

The Corollary (p. 1134): if every player follows (3.1), $z_t$ converges almost surely to the set of correlated equilibria. The equivalence of (3.1) with invariance for the (2.2) matrix (p. 1133). Theorem B (p. 1139): the procedure proportional to unconditional regrets $[D^i_t(k)]^+$ satisfies Hannan's universal consistency (4.1).

Significance

Theorem A shows that conditional regrets can be driven to zero by a stationary rule of fixed size $m^i\times m^i$ , with no assumption on the other players beyond conditional independence. Combined with the Proposition of §3 it gives the Corollary: if all players follow such a rule, play converges to the set of correlated equilibria. The same argument with a different vector payoff yields Theorem B, a short proof of Hannan consistency. The approachability reduction used here is the standard route from vector-valued games to no-regret learning.

Theorem A and Blackwell's theorem are proved results. What this mission adds is a machine-checked development: a formal statement of Theorem A for arbitrary opponents, a formal statement of Blackwell's procedure in Hart and Mas-Colell's form (condition (3.2) via the support function, opponents that see the whole history), and the algebra connecting the two. Prove2Me already has Blackwell's original THEOREM 1 (strategies depending only on past payoff vectors, geometric separation condition); it is a different statement, and deriving this one from it, or proving it directly, is part of the work.

Difficulty

The algebra (milestones 1–5) is finite-dimensional and elementary, apart from the existence of an invariant vector, which needs a fixed-point or Perron–Frobenius type argument for a matrix that is not stochastic. The probabilistic core is milestone 6. The geometric picture of the paper (Figure 1) shows that the expected next average payoff moves closer to $\mathcal C$ , but that controls only $\operatorname{dist}(E[D_{t+1}\mid h_t],\mathcal C)$ , not the realized averages (footnote 15 of the paper); the opponent adapts to the whole history, so the increments are neither independent nor identically distributed, and the almost-sure statement has to be obtained on a measure known only through its conditional laws given each history.

Formalization scope

The game is finite with nonempty strategy sets; payoffs are real. $\Delta(Q)$ is Mathlib's stdSimplex. $\mathbb R^L$ is EuclideanSpace ℝ L with its inner product and Euclidean distance.
Time is 0-based in Lean (play τ is $s_{\tau+1}$ ); every regret quantity is a function of a finite history Fin t → S, and every statement uses histories of length $t+1\ge1$ .
A behaviour profile assigns a probability vector to every player, period and history. A play is any sequence of random variables on any probability space such that, given each history of positive probability, the next profile has the product law of the players' mixed actions. Theorem A constrains only player $i$ , and only from period 2 on; the other players are arbitrary.
The zero diagonal of (3.1) is explicit. The support function's value $+\infty$ is never computed in the reals: (3.2) is encoded as " $\lambda\cdot v(q_\lambda,b)\le M$ for every real upper bound $M$ of $\lambda\cdot\mathcal C$ ", and milestone 4 uses IsLUB/¬ BddAbove.
In Blackwell's theorem, nonemptiness of $\mathcal C$ is stated explicitly (it is implicit in the existence of the closest point), and the choices $\lambda\mapsto q_\lambda$ and the projection $F$ are given as functions with the stated properties.
Requiring $q^i_t$ to be a probability vector rules out the trivial solution $q=0$ of (3.1); the goal mentions neither $v$ , $\mathbb R^L_-$ nor Blackwell, so it cannot be discharged by its own milestones' definitions.

Useful infrastructure, reusable beyond this mission: the existence of invariant vectors of nonnegative matrices, projections onto orthants, and a general Blackwell approachability theorem for history-dependent opponents. Proofs of any milestone, of the companions, and alternative proofs of Theorem A are welcome.

Selected references

S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5) (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153
D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6 (1956), 1–8. https://doi.org/10.2140/pjm.1956.6.1
R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III (1957), 97–139. https://doi.org/10.1515/9781400882151-006
D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
N. Cesa-Bianchi and G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

9 thms4 active usersReviewed

Missions

Phase Transitions in Bandits with Switching Constraints: every policy with at most S switches has regret at least the phase-dependent rate up to a logarithmic factorResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 21)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Efficient Online Linear Optimization with Approximation Algorithms: Online Gradient Descent with Infeasible Projections onto CH(αK) Has Expected α-Regret at Most α²R²/(Tη) + ηF²/2 + 3FεResearch Paper

Online learning with an approximation algorithm

Setting

Formalization targets

Goal: Theorem 1 (regret bound)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Nature of Statistical Learning Theory I: The Key Theorem of Learning TheoryTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.1, the key theorem (p. 38)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low VI: A BIC-Type Choice of the Model Size Yields Oracle Inequalities for the Expected Prediction ErrorResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5 (p. 21)

Milestones (proof of Theorem 5, B.13, and B.5)

Significance

Difficulty

Formalization scope

Selected references

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 2: The Conservative Model-Based Policy Is ε-Optimal w.p. 1−δ at the Sample Size of Theorem 1Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distribution-Free Contextual Dynamic Pricing 1: The DIP Policy Has Expected Regret at Most C T^(2/3) log T Plus 4 p_max L Times the Episode-Weighted ℓ₁ Estimation ErrorsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 with the O~\tilde OO~ pinned

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Modern Introduction to Online Learning VII: The Perceptron's Mistakes Exceed the Competitor's Hinge-Power Loss by at Most q²R²‖u‖²/2 + qR‖u‖√(q²R²‖u‖²/4 + L_q)Textbook

Motivation

Setting

Formalization targets

Perceptron mistake guarantee

Milestone statements

Significance

Difficulty

Formalization scope

Selected references

A Modern Introduction to Online Learning III: Adaptive Online Subgradient Descent on s-Self-Bounded Losses Has Regret 4sD² + 2D√(s Σ_t ℓ_t(u))Textbook

Motivation

Setting

Formalization targets

Adaptive gradient bound

Self-bounded loss bound

Significance

Difficulty

Goal: Theorem 1 with the $\tilde O$ pinned