From 747cdcdef91fab4506efea250a5c73a4845c136c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 30 Oct 2026 16:49:33 +0100 Subject: [PATCH] Add the Bandits roadmap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Regret theory of stochastic, adversarial and linear bandits, following Lattimore and Szepesvári, Bandit Algorithms: UCB variants, KL-UCB, Thompson sampling, minimax and Lai-Robbins lower bounds, Exp3, Exp3-IX, Exp4, FTRL and mirror descent, OFUL, phased elimination with optimal designs, and adversarial linear bandits, built on LML's interaction framework and existing bandit results. Co-Authored-By: Claude Opus 5.5 --- LMLRoadmaps/Bandits/README.md | 526 +++++++++++++++++++++++++++++ LMLRoadmaps/Bandits/Suggested.lean | 326 ++++++++++++++++++ LMLRoadmaps/Bandits/metadata.toml | 1 + 3 files changed, 853 insertions(+) create mode 100644 LMLRoadmaps/Bandits/README.md create mode 100644 LMLRoadmaps/Bandits/Suggested.lean create mode 100644 LMLRoadmaps/Bandits/metadata.toml diff --git a/LMLRoadmaps/Bandits/README.md b/LMLRoadmaps/Bandits/README.md new file mode 100644 index 0000000..5051a17 --- /dev/null +++ b/LMLRoadmaps/Bandits/README.md @@ -0,0 +1,526 @@ +# Roadmap: Bandit algorithms and their regret + +Develop the regret theory of multi-armed and linear bandits: stochastic bandits with finitely +many arms, their minimax and instance-dependent lower bounds, adversarial bandits with finitely +many arms and with expert advice, online linear optimization, and stochastic and adversarial +linear bandits. The headline results are the regret bounds of MOSS, asymptotically optimal UCB, +KL-UCB, Thompson sampling, Exp3, Exp3-IX, Exp4, OFUL, phased elimination with G-optimal designs, +and mirror descent with bandit feedback, matched by the minimax lower bounds and the Lai–Robbins +lower bound. + +Build the surrounding library at the generality the proofs support: index policies and +weight-based randomized policies, Ville's inequality and time-uniform concentration, the binary +relative entropy, the Bretagnolle–Huber inequality, Legendre functions and Bregman projections, +follow-the-regularized-leader and mirror descent, regularized least squares with self-normalized +confidence sets, the elliptical potential lemma, and the Kiefer–Wolfowitz theorem. + +`README.md` is the definitive specification; `Suggested.lean` records selected interfaces and is +not an exhaustive checklist. + +Suggested homes: `LMLExplore/Bandits/` for bandit material, `LMLExplore/OnlineLearning/` for +online linear optimization, and the mathematical home of each general tool (for example +`LMLExplore/Probability/Martingale/` for Ville's inequality, `LMLExplore/InformationTheory/` for +the binary relative entropy and Bretagnolle–Huber, `LMLExplore/Analysis/Convex/` for Legendre +functions, `LMLExplore/Analysis/InnerProductSpace/` for design operators and the Kiefer–Wolfowitz +theorem). + +## Scope and dependencies + +This roadmap owns regret minimization for: stochastic bandits with a finite set of arms; +adversarial bandits with a finite set of arms against an oblivious reward table, including bandits +with expert advice; online linear optimization with full information; stochastic linear bandits +with possibly changing decision sets; and adversarial linear bandits with finite action sets or the +Euclidean unit ball. + +| Material | Owner and interface consumed here | +| --- | --- | +| Interaction protocol, runs, trajectory measure, stochastic and oblivious environments | LML `SequentialLearning/`: `Algorithm`, `Environment`, `IsAlgEnvSeq`, `trajMeasure`, `stationaryEnv`, `obliviousEnv`, `onlineEvalEnv`, `detAlgorithm` | +| Pull counts, reward sums, empirical means, the per-arm reward stream model | LML `SequentialLearning/FiniteActions.lean`, `SumRewards.lean`, `Online/Bandit/ArrayProbSpace.lean`, `Online/Bandit/RewardByCountMeasure.lean` | +| Stochastic regret, gaps, regret decomposition; regret of explore-then-commit, UCB and Bayesian Thompson sampling | LML `Online/Bandit/Regret.lean` and `Online/Bandit/Algorithms/` | +| KL divergence of interaction histories (time-sum form) | LML `SequentialLearning/DivergenceDecomposition.lean` | +| KL divergence, chain rule, data processing, Pinsker, Donsker–Varadhan | Mathlib `InformationTheory/KullbackLeibler/`, LML `ForMathlib/InformationTheory/KullbackLeibler/`, Tau Ceti `InformationTheory/KullbackLeibler/` | +| Sub-Gaussian random variables, Hoeffding and Azuma–Hoeffding, Doob's maximal inequality | Mathlib `Probability/Moments/SubGaussian.lean`, `Probability/Martingale/` | +| Bregman divergence and subgradients | LML `ForMathlib/Analysis/Convex/Bregman/`, `ForMathlib/Analysis/Convex/Subgradient/` | +| Fenchel conjugate, strong convexity first-order bound | Tau Ceti `Analysis/Convex/Conjugate.lean`, `Analysis/Convex/Strong.lean` | +| Positive operators, Loewner order, matrix determinant lemma, Woodbury identity | Mathlib `Analysis/InnerProductSpace/Positive.lean`, `LinearAlgebra/Matrix/SchurComplement.lean`, `LinearAlgebra/Matrix/NonsingularInverse.lean` | + +Build missing material in this roadmap where it is listed as a target, and consume existing +implementations directly. + +Outside this roadmap: pure exploration and best-arm identification (LML's `IdentAlg` framework), +sparse linear bandits, combinatorial and semi-bandits, non-stationary bandits, ranking, partial +monitoring, Markov decision processes, Bayesian-optimal policies and Gittins indices, Bayesian regret +beyond what LML proves, high-probability lower bounds, asymptotic lower bounds for linear bandits, +and online convex optimization with nonlinear losses. Scalar Bernstein, McDiarmid and matrix +concentration inequalities belong to Tau Ceti's `RandomMatrices` roadmap; nothing here needs them. + +## Conventions + +**Sources and numbering.** Statements follow Lattimore and Szepesvári, *Bandit Algorithms* +(Cambridge University Press, 2020), cited as [LS] with chapter and theorem numbers. The book's +rounds are numbered from 1; Lean rounds are numbered from 0, as in LML. Book round $t$ is Lean round +$t-1$: a quantity the book computes at round $t$ from $t-1$ past rounds is computed in Lean at round +$t-1$ from the history of length $t-1$, and a book horizon $n$ is the Lean horizon $n$ (rounds +$0,\dots,n-1$). For example the index $f(t)=1+t\log^2 t$ of [LS, Chapter 8] is evaluated at $t=m+1$ +in Lean round $m$. + +**Arms.** A finite set of arms is a type `α` with `[Fintype α] [Nonempty α] [DecidableEq α] +[MeasurableSpace α] [MeasurableSingletonClass α]`, and $k$ is `Fintype.card α`. Do not specialize +algorithms or theorems to `Fin K`. Algorithms never rely on an enumeration of the arms: an arm not +pulled yet has index $+\infty$, so "pull each arm once" is the behaviour of the index policy itself. +LML's existing algorithms (`etcAlgorithm`, `ucbAlgorithm`) are stated on `Fin K`; consume them as +they are. + +**Rewards and losses.** Stochastic bandits, adversarial bandits with finitely many arms and bandits +with expert advice use rewards and maximization, as LML's `regret` and [LS, Chapters 4–18] do. +Online linear optimization and adversarial linear bandits use losses and minimization, as [LS, +Chapters 26–28] and convex analysis do. Where the analysis of a reward-based algorithm passes +through a loss-based tool, state the translation $y = 1 - x$ (or $y=-x$) once as a lemma. + +**Stochastic bandits.** A stochastic bandit is a Markov kernel `ν : Kernel α ℝ` and its environment +is LML's `stationaryEnv ν`. The mean of arm $a$ is `(ν a)[id]`. Noise assumptions are stated per +arm, as in LML: σ²-sub-Gaussian rewards are +`∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) σ2 (ν a)` with `σ2 : ℝ≥0` the variance proxy, and +bounded rewards are `∀ a, ∀ᵐ x ∂(ν a), x ∈ Set.Icc 0 1`. Where [LS] assumes 1-subgaussian rewards, +state the result for σ²-sub-Gaussian rewards; the constants below include $\sigma^2$. + +**Regret.** The expected stochastic regret is `P[regret ν A n]` with LML's `regret`, the expectation +of the pseudo-regret $\sum_{t c, ∀ᶠ n in atTop, R n ≤ c' * log n`, and lower bounds +quantify over `c' < c`. Where [LS] states a universal constant $C$, state an explicit numerical +constant when the proof gives one; otherwise state `∃ C > 0, ∀ …` with `C` quantified before every +problem parameter. + +**Generality.** Each layer lists where its statements generalize [LS]. Do not reintroduce the +book's special cases (`Fin K`, unit variance, $\mathbb R^d$ instead of an inner product space) as +the primary statements; derive them as corollaries when useful. + +**Namespaces.** Bandit definitions live in `LMLExplore.Bandits`, online-learning definitions in +`LMLExplore.OnlineLearning`, general tools in `LMLExplore` or in the namespace of the type they act +on (dot notation). LML's definitions keep their names (`Learning.stationaryEnv`, `Bandits.regret`, +…). + +## Existing library and design guidance + +Consume these modules and extend their APIs rather than restating them. The links pin the +dependency versions used to check the interfaces (LML `53be244`, Mathlib `2e318fae`, Tau Ceti +`v4.36.0-rc1`). + +| Foundation | Existing source | +| --- | --- | +| Interaction protocol and law of a run | [LML `Algorithm.lean`][lml-alg] (`Algorithm`, `Environment`, `IsAlgEnvSeq`, `history`, `IsAlgEnvSeq.filtration`), [`IonescuTulceaSpace.lean`][lml-it] (`trajMeasure`, `IT.isAlgEnvSeq_trajMeasure`, `IsAlgEnvSeq.map_trajectory`) | +| Stochastic and oblivious environments | [LML `StationaryEnv.lean`][lml-env] (`stationaryEnv`, `obliviousEnv`, `IsObliviousEnv`), [`EvaluationEnv.lean`][lml-eval] (`onlineEvalEnv g hg`, the oblivious adversary with bandit feedback) | +| Deterministic algorithms and measurable argmax | [LML `Deterministic.lean`][lml-det] (`detAlgorithm`), [`MeasurableArg.lean`][lml-argmax] (`argmax`, `measurable_argmax`) | +| Counts, sums, empirical means, per-arm reward streams | [LML `FiniteActions.lean`][lml-fa] (`pullCount`, `pullCount'`, `rewardByCount`), [`SumRewards.lean`][lml-sum] (`sumRewards`, `empMean`, `empMean'`), [`Online/Bandit/SumRewards.lean`][lml-conc] (`prob_sumRewards_sub_pullCount_mul_ge_le` and the transfer to the i.i.d. stream model) | +| Stochastic regret and existing regret bounds | [LML `Regret.lean`][lml-regret] (`regret`, `gap`, `integral_regret_le_of_forall_integral_pullCount_le`), [`Regret/UCB.lean`][lml-ucb] (`UCB.expectation_pullCount_le`, `UCB.regret_le_of_gt_two'`), [`Regret/ETC.lean`][lml-etc], [`Regret/BayesRegretTS.lean`][lml-ts] | +| KL divergence of histories | [LML `DivergenceDecomposition.lean`][lml-div] (`IsAlgEnvSeq.klDiv_map_history`: the time-sum $\sum_{t0$: + $P(\exists t,\ M_t\ge c)\le \mathbb E[M_0]/c$. Derive it from Doob's maximal inequality + (`maximal_ineq` is stated for submartingales; add the supermartingale form) by monotone + convergence in the horizon. +2. **Time-uniform sub-Gaussian bounds.** For a process adapted to a filtration whose increments are + conditionally σ²-sub-Gaussian (`HasCondSubgaussianMGF`), prove that + $\exp(\lambda S_t-\lambda^2\sigma^2t/2)$ is a supermartingale, the maximal inequality + $P(\exists t\le n,\ S_t\ge\varepsilon)\le\exp(-\varepsilon^2/(2n\sigma^2))$ [LS, Theorem 9.2], + and its time-uniform union-bound consequences used by Layers 2 and 8. +3. **Per-arm statements on runs.** For a run of any algorithm against `stationaryEnv ν`, transfer + statements about the i.i.d. stream of rewards of one arm to statements about the empirical mean + after its $s$-th pull, for all $s$ simultaneously, using LML's per-arm stream model. State the + version that the lemmas below need: a bound on + $\mathbb E\big[\sum_{s}\mathbb 1\{\text{event about the first } s \text{ rewards of arm } a\}\big]$ + in terms of the corresponding i.i.d. quantity. +4. **Chernoff bounds in relative-entropy form.** For i.i.d. $X_i\in[0,1]$ with mean $\mu$ (not only + Bernoulli, [LS, Note 10.3.1]): + $P(\hat\mu_n\ge\mu+\varepsilon)\le\exp(-n\,d(\mu+\varepsilon,\mu))$ for + $\varepsilon\in[0,1-\mu]$, and the lower tail [LS, Lemma 10.3], with + [LS, Corollary 10.4] for the confidence levels $U$ and $L$. +5. **Lemmas for the index policies.** Prove, for σ²-sub-Gaussian streams, [LS, Lemma 8.2] and + [LS, Lemma 9.3], and the summation bound $\sum_{t\le n}\frac1{f(t)}\sum_{s\le n} + e^{-s\varepsilon^2/(2\sigma^2)}\le 5\sigma^2/\varepsilon^2$ of [LS, Exercise 8.1]; for + $[0,1]$-valued streams, [LS, Lemma 10.7] and [LS, Lemma 10.8]. Scale the constants with + $\sigma^2$ as in Layer 2. +6. **Gaussian tails.** For $Z\sim\mathcal N(0,1)$ and $x>0$: + $\frac{x}{x^2+1}\varphi(x)\le P(Z\ge x)\le\min\{\varphi(x)/x,\ \tfrac12e^{-x^2/2}\}$, with + $\varphi$ the standard Gaussian density. + +Completion checks: Ville's inequality is sharp for the martingale $M_t=1$; the per-arm transfer of +item 3 applied to LML's existing union bound recovers `prob_sumRewards_sub_pullCount_mul_ge_le`. + +## Layer 2: UCB-type algorithms for sub-Gaussian rewards + +Throughout, rewards are σ²-sub-Gaussian with `σ2 ≠ 0`, $\Delta_a$ is `gap ν a`, and indices of +unpulled arms are $+\infty$. + +1. **Minimax bound for LML's UCB.** From `UCB.expectation_pullCount_le` and + `integral_regret_le_of_forall_integral_pullCount_le`, prove for `ucbAlgorithm K c` with + $c>2\sigma^2$: + $\mathbb E[R_n]\le 2\sqrt{8cKn\log(n+1)}+\big(4+\frac{2\sigma^2}{c-2\sigma^2}\big)\sum_a\Delta_a$, + by splitting the arms according to whether $\Delta_a$ is below $\sqrt{8cK\log(n+1)/n}$ + (the analogue of [LS, Theorem 7.2]). +2. **Asymptotically optimal UCB.** Define the index policy with index + $\hat\mu_a+\sqrt{2\sigma^2\log f(t)/T_a}$, $f(t)=1+t\log^2 t$ [LS, Algorithm 6]. Prove + [LS, Theorem 8.1] for σ²-sub-Gaussian rewards: + $$\mathbb E[R_n]\le\sum_{a:\Delta_a>0}\inf_{\varepsilon\in(0,\Delta_a)}\Delta_a\Big(1+\frac{5\sigma^2}{\varepsilon^2}+\frac{2\sigma^2\big(\log f(n)+\sqrt{\pi\log f(n)}+1\big)}{(\Delta_a-\varepsilon)^2}\Big),$$ + and, in eventual form, $\limsup_n\mathbb E[R_n]/\log n\le\sum_{a:\Delta_a>0}2\sigma^2/\Delta_a$. +3. **MOSS.** Define the horizon-dependent index policy with index + $\hat\mu_a+\sqrt{\frac{4\sigma^2}{T_a}\log^+\frac{n}{kT_a}}$ [LS, Algorithm 7] and prove + [LS, Theorem 9.1]: $\mathbb E[R_n]\le 39\sqrt{\sigma^2kn}+\sum_a\Delta_a$. + +Generalization: arbitrary finite arm types and variance proxies, where [LS] has $[k]$ and +1-subgaussian rewards. Completion examples: for two Gaussian arms with gap $\Delta$, the bounds of +items 2 and 3 are finite and the asymptotic constant is $2\sigma^2/\Delta$. + +## Layer 3: KL-UCB for rewards in [0,1] + +1. **Algorithm.** Define KL-UCB [LS, Algorithm 8]: the index policy with index + $U(\hat\mu_a,\log f(t)/T_a)$ for the level $U$ of Layer 0.2 and $f(t)=1+t\log^2t$. +2. **Regret.** For rewards in $[0,1]$ almost surely, prove [LS, Theorem 10.6]: + $$\mathbb E[R_n]\le\sum_{a:\Delta_a>0}\inf_{\substack{\varepsilon_1,\varepsilon_2>0\\\varepsilon_1+\varepsilon_2<\Delta_a}}\Delta_a\Big(\frac{\log f(n)}{d(\mu_a+\varepsilon_1,\mu^*-\varepsilon_2)}+\frac1{2\varepsilon_1^2}+\frac2{\varepsilon_2^2}\Big),$$ + and, in eventual form, $\limsup_n\mathbb E[R_n]/\log n\le\sum_{a:\Delta_a>0}\Delta_a/d(\mu_a,\mu^*)$ + (the book leaves this limit to its Exercise 10.2; its proof writes $f(n)$ for $\log f(n)$ in the + last line). + +Generalization: rewards with any law on $[0,1]$, where [LS] states Bernoulli rewards. Completion +examples: arms with means $0$ or $1$ (the singular values of $d$), and a two-armed Bernoulli bandit. + +## Layer 4: Lower bounds for finitely many arms + +1. **Divergence decomposition.** For an algorithm run against two stationary environments `ν`, `ν'` + on a finite arm type, prove [LS, Lemma 15.1] in `ℝ≥0∞`: + $D(P_{\nu}^{(n)},P_{\nu'}^{(n)})=\sum_a\mathbb E_\nu[T_a(n)]\,D(\nu_a,\nu'_a)$, where + $P^{(n)}$ is the law of the history of length $n$, by regrouping LML's + `IsAlgEnvSeq.klDiv_map_history` along the pulled arm. +2. **Bretagnolle–Huber.** For probability measures $P,Q$ and every measurable $A$: + $P(A)+Q(A^c)\ge\tfrac12\exp(-D(P,Q))$ [LS, Theorem 14.2], through the stronger + $\int\min(p,q)\ge\tfrac12\exp(-D(P,Q))$ for densities with respect to $P+Q$ [LS, (14.8)]. +3. **Minimax lower bound.** Generalize [LS, Theorem 15.2] to a family $(P_x)_{x\in[b,b+h]}$ of + reward laws with means $x$ and $D(P_x,P_y)\le(x-y)^2/(2\sigma^2)$: for $k\ge2$ and + $n\ge\sigma^2(k-1)/h^2$, every algorithm has a mean vector $\mu\in[b,b+h]^\alpha$ with + $\mathbb E[R_n]\ge\frac1{27}\sigma\sqrt{(k-1)n}$ on the bandit $(P_{\mu_a})_a$. Corollaries: the + Gaussian case ($[0,1]$, variance $\sigma^2$), which is [LS, Theorem 15.2] for $\sigma=1$, and the + Bernoulli case ($[1/4,3/4]$, $\sigma^2=3/32$, from Layer 0.2's bound on $d$). +4. **Lai–Robbins.** Define consistency of an algorithm over a class of bandits [LS, Definition 16.1] + and, for a set $\mathcal M$ of integrable laws on $\mathbb R$, + $d_{\inf}(P,\mu^*,\mathcal M)=\inf\{D(P,P'):P'\in\mathcal M,\ \mu(P')>\mu^*\}$ in `ℝ≥0∞`. Prove + [LS, Theorem 16.2] for the unstructured class $\prod_a\mathcal M_a$: + $\liminf_n\mathbb E[R_n]/\log n\ge\sum_{a:\Delta_a>0}\Delta_a/d_{\inf}(\nu_a,\mu^*,\mathcal M_a)$, + with the sum in `ℝ≥0∞`. Compute $d_{\inf}$ for Gaussian laws with known variance and for + Bernoulli laws [LS, Table 16.1]. Prove [LS, Lemma 16.3] and the finite-time bound + [LS, Theorem 16.4], for Gaussian bandits with variance $\sigma^2$. +5. **Asymptotic optimality and the adversarial lower bound.** Prove that the algorithms of Layers 2.2 + and 3 are consistent and attain the Lai–Robbins constant (Gaussian arms and Bernoulli arms + respectively): their expected regret is $c^*\log n+o(\log n)$. Prove the adversarial minimax lower + bound: for every algorithm and $n\ge 3(k-1)/8$ there is a table $x\in\{0,1\}^{n\times\alpha}$ with + $R_n(x)\ge\frac1{27}\sqrt{3(k-1)n/32}$, by averaging the Bernoulli case of item 3 over i.i.d. + tables (Layer 0.5). + +Generalization: the minimax bound for a family of laws rather than unit-variance Gaussians. +Completion checks: the divergence decomposition is zero for identical environments; the Lai–Robbins +constant is $+\infty$ when some $d_{\inf}$ vanishes, and the theorem then states that the regret of +every consistent policy eventually exceeds every multiple of $\log n$. + +## Layer 5: Thompson sampling + +1. **Algorithm.** Define Gaussian Thompson sampling with variance proxy $\sigma^2$ and flat prior: + at each round, sample independently $\theta_a\sim\mathcal N(\hat\mu_a,\sigma^2/T_a)$ (and + $\theta_a=+\infty$ for unpulled arms) and play `argmax θ`. The book's update writes the variance + $1/t$; the intended variance after $s$ samples of the arm is $1/s$ [LS, Theorem 36.3]. +2. **Generic bound.** Prove [LS, Theorem 36.2] for the follow-the-perturbed-leader scheme of + [LS, Algorithm 24]: with arm $a^*$ optimal, $a\ne a^*$, $\varepsilon\in\mathbb R$ and + $G_{as}=1-F_{as}(\mu^*-\varepsilon)$, + $\mathbb E[T_a(n)]\le1+\mathbb E\big[\sum_{s1/n\}\big]$. +3. **Frequentist regret.** For Gaussian bandits with variance $\sigma^2$, prove + [LS, Theorem 36.3]: $\mathbb E[R_n]/\log n\to\sum_{a:\Delta_a>0}2\sigma^2/\Delta_a$ (upper bound + in eventual form, matched by Layer 4.4), and + $\mathbb E[R_n]\le C\sqrt{\sigma^2kn\log n}+\sum_a\Delta_a$ for an absolute constant $C$, through + the steps of [LS, Exercise 36.6] and the Gaussian tails of Layer 1.6. + +Generalization: arbitrary variance proxy and finite arm type. LML's Bayesian Thompson sampling +(`tsAlgorithm`, `TS.integral_regret_le`) is a different algorithm (it samples from the posterior of +a prior over environments); do not restate its results. + +## Layer 6: Convex analysis and online linear optimization + +Work in a finite-dimensional real inner product space `E`. Losses are minimized. + +1. **Legendre functions.** For a convex function $F$ with domain $D$ (represent it as `F : E → ℝ` + with a convex set `D`, or as `E → EReal`; choose one representation and give conversions to + Tau Ceti's `fenchelConjugate`), define Legendre functions [LS, §26.4]: nonempty interior of the + domain, differentiable and strictly convex on the interior, gradient norm tending to infinity at + the boundary. Prove [LS, Theorem 26.6] (the gradient is a bijection between interiors with + inverse $\nabla F^*$, $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$, and $F^*$ is Legendre), + [LS, Corollary 26.8] and [LS, Proposition 26.14]. +2. **Bregman divergence and projections.** On LML's `bregDiv`, prove [LS, Theorem 26.3], the Bregman + projection theorem [LS, Theorem 26.15], the generalized Pythagorean inequality + $D_F(x,y)\ge D_F(x,z)+D_F(z,y)$ for $z=\Pi_{A,F}(y)$ and $x\in A$ [LS, Exercise 26.13], and the + Hessian forms [LS, Theorems 26.12 and 26.13]. +3. **FTRL and mirror descent.** Define follow-the-regularized-leader and mirror descent on a convex + set $\mathcal A\subseteq E$ with potential $F$ and learning rate $\eta$ [LS, (28.1)–(28.3)] for + arbitrary loss sequences, including the two-step form of mirror descent [LS, (28.7)–(28.9)]. + Prove [LS, Theorem 28.4] (both bounds and (28.11)), [LS, Theorem 28.5] for convex $F$ with + directional derivatives, and [LS, Corollary 28.8]. The bounds hold for losses chosen adaptively + from past actions. +4. **Two instances.** Prove [LS, Proposition 28.6] (unit ball, $F=\tfrac12\|a\|^2$, + $\eta=n^{-1/2}$: $R_n\le\sqrt n$) and [LS, Proposition 28.7] (simplex, unnormalized negative + entropy, $\eta=\sqrt{2\log(d)/n}$: $R_n\le\sqrt{2n\log d}$). Identify the latter with exponential + weights over a finite set, stated on `α → ℝ` with `stdSimplex`. + +Generalization: an inner product space rather than $\mathbb R^d$; the instances are corollaries. + +## Layer 7: Adversarial bandits with finitely many arms and expert advice + +Rewards $x_t(a)\in[0,1]$; runs against `onlineEvalEnv x _`. + +1. **Importance-weighted estimators.** For a weight-based policy with weights bounded away from + zero, define the standard and loss-based estimators [LS, (11.3), (11.6)] and prove conditional + unbiasedness and the conditional variance formulas [LS, (11.4), (11.5)]. +2. **Exp3.** Define Exp3 [LS, Algorithm 9] as a weight-based policy using the loss-based estimator. + Prove, for every $\eta>0$, $R_n(x)\le\frac{\log k}{\eta}+\frac{\eta nk}{2}$, and + [LS, Theorem 11.2]: with $\eta=\sqrt{2\log(k)/(nk)}$, $R_n(x)\le\sqrt{2nk\log k}$. +3. **Exp3-IX.** Define Exp3-IX [LS, Algorithm 10] and prove [LS, Lemmas 12.2–12.4] and both + high-probability bounds of [LS, Theorem 12.1] for the random regret + $\hat R_n=\max_a\sum_{t0$, the rank-one update of the inverse (Sherman–Morrison) and of the determinant + $\det V_{t+1}=\det V_t\,(1+\|x_t\|^2_{V_t^{-1}})$ [LS, (19.9)], and + $\det V\le(\operatorname{trace}V/d)^d$ for positive $V$. +2. **Elliptical potential.** Prove [LS, Lemma 19.4]: for positive definite $V_0$ and $\|x_t\|\le L$, + $\sum_{t 0` [LS, Definition 16.1]. -/ +def IsConsistentGaussian (alg : Algorithm Unit α ℝ) (σ2 : ℝ≥0) : Prop := + ∀ μ : α → ℝ, ∀ p : ℝ, 0 < p → + Tendsto (fun n : ℕ ↦ (∫ ω, Bandits.regret (gaussianBandit μ σ2) IT.action n ω + ∂(trajMeasure alg (stationaryEnv (gaussianBandit μ σ2)))) / (n : ℝ) ^ p) atTop (𝓝 0) + +/-- The Lai–Robbins lower bound for Gaussian bandits ([LS, Theorem 16.2] with +[LS, Table 16.1]), in eventual form. -/ +theorem lai_robbins_gaussian {alg : Algorithm Unit α ℝ} {σ2 : ℝ≥0} + (h : IsConsistentGaussian alg σ2) (hσ2 : σ2 ≠ 0) (μ : α → ℝ) {c : ℝ} + (hc : c < ∑ a ∈ univ.filter (fun a ↦ 0 < Bandits.gap (gaussianBandit μ σ2) a), + 2 * σ2 / Bandits.gap (gaussianBandit μ σ2) a) : + ∀ᶠ n : ℕ in atTop, c * log n ≤ ∫ ω, Bandits.regret (gaussianBandit μ σ2) IT.action n ω + ∂(trajMeasure alg (stationaryEnv (gaussianBandit μ σ2))) := + sorry + +/-! ## Layer 6: online linear optimization -/ + +section OnlineLinear + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] + +/-- The regret bound of follow-the-regularized-leader [LS, Theorem 28.5], for a potential that is +differentiable at the iterates; `a t` minimizes `η ⟪·, ∑_{s