diff --git a/LMLRoadmaps/Bandits/README.md b/LMLRoadmaps/Bandits/README.md
index 57e557f..9fbcbbb 100644
--- a/LMLRoadmaps/Bandits/README.md
+++ b/LMLRoadmaps/Bandits/README.md
@@ -2,23 +2,25 @@
 
 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.
+many arms and with expert advice, online linear and convex optimization, and stochastic and
+adversarial linear bandits. The headline results are the regret bounds of MOSS, asymptotically
+optimal UCB, KL-UCB and Thompson sampling for exponential families, Exp3, Exp3-IX and Exp4 against
+adaptive adversaries, 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.
+relative entropy and the upper confidence levels of exponential families, the Bretagnolle–Huber
+inequality, Legendre functions and Bregman projections, follow-the-regularized-leader and mirror
+descent with time-varying regularizers and local norms, regularized and unregularized 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
+online linear and convex 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
@@ -27,22 +29,28 @@ 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.
+adversarial bandits with a finite set of arms against adaptive adversaries, oblivious reward tables
+included, and bandits with expert advice; online linear and convex 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/` |
+| Means of the feedback laws along a run | LML `SequentialLearning/Means.lean` (`Environment.means`) |
 | 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/` |
+| Exponential families: members, means, natural parameters, divergence and Cramér–Chernoff rate function; the Cramér–Chernoff bound under domination by a member | Identification roadmap, Layer 1.2 (`expFamily`, `expFamilyMeans`, `natParam`, `expFamilyDiv`) |
+| Conditional MGF domination, its supermartingale and time-uniform bound; σ²-sub-Gaussian laws are dominated by the Gaussian family | Identification roadmap, Layer 4.2 |
+| Transfer of events about the first `s` rewards of each arm from runs to the reward-stream model | Identification roadmap, Layer 4.1 |
 | 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` |
+| Moore–Penrose inverse | Tau Ceti `Analysis/InnerProductSpace/MoorePenrose.lean` |
+| Finitely supported probability measures | Mathlib `Geometry/Convex/ConvexSpace/Defs.lean` (`Convexity.StdSimplex`) |
 
 Build missing material in this roadmap where it is listed as a target, and consume existing
 implementations directly.
@@ -51,7 +59,8 @@ Outside this roadmap: pure exploration and best-arm identification (LML's `Ident
 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
+and bandit convex optimization (convex losses with bandit feedback). AdaHedge and its regret bounds
+belong to the Identification roadmap (Layer 6.1). Scalar Bernstein, McDiarmid and matrix
 concentration inequalities belong to Tau Ceti's `RandomMatrices` roadmap; nothing here needs them.
 
 ## Conventions
@@ -73,8 +82,8 @@ 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
+Online linear and convex 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
@@ -85,10 +94,23 @@ bounded rewards are `∀ a, ∀ᵐ x ∂(ν a), x ∈ Set.Icc 0 1`. Where [LS] a
 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<n}\Delta_{A_t}$. The adversarial regret against an oblivious reward
-table $x:\mathbb N\to\alpha\to\mathbb R$ is
-$R_n(x)=\max_a\sum_{t<n}x_t(a)-\mathbb E\big[\sum_{t<n}x_t(A_t)\big]$ [LS, (11.1)]. Linear regrets are
-defined in Layer 9 and Layer 10.
+of $\sum_{t<n}\Delta_{A_t}$. An adversarial bandit with finitely many arms is a
+run against an arbitrary environment `env : Environment 𝓞 α ℝ`, an *adaptive adversary*: the
+reward law of round $t$ may depend on the history and on the observation of round $t$. Its *mean
+table* $m_t(a)$ is LML's `env.means O A Y a t`, the mean reward of arm $a$ at round $t$ given the
+past. The *pseudo-regret* is $\bar R_n=\max_a\mathbb E\big[\sum_{t<n}(m_t(a)-Y_t)\big]$
+[BCB12, Section 3] and the *random regret* is $\hat R_n=\max_a\sum_{t<n}(m_t(a)-Y_t)$. Against an
+oblivious reward table $x:\mathbb N\to\alpha\to\mathbb R$ (`onlineEvalEnv x _`), $m_t(a)=x_t(a)$ and
+$\bar R_n$ is the adversarial regret
+$R_n(x)=\max_a\sum_{t<n}x_t(a)-\mathbb E\big[\sum_{t<n}x_t(A_t)\big]$ [LS, (11.1)]; against
+`stationaryEnv ν` it is the expected stochastic regret. Linear regrets are defined in Layer 9 and
+Layer 10.
+
+**Learning rates.** Learning rates and implicit-exploration parameters are sequences
+`η γ : ℕ → ℝ` fixed in advance, nonincreasing, with $\eta_t>0$ and $\gamma_t\ge0$ used at Lean
+round $t$. A rate tuned for the horizon $n$ is a constant sequence; an anytime rate does not depend
+on the horizon, for example $\eta_t=c/\sqrt{t+1}$. Bounds after $n$ rounds involve $\eta_{n-1}$,
+the rate of the last round played.
 
 **Theorem shapes.** Upper bounds quantify over runs: for every `IsAlgEnvSeq O A Y alg env P`, a
 bound on an expectation or a probability under `P`. Lower bounds quantify over algorithms and
@@ -101,8 +123,9 @@ constant when the proof gives one; otherwise state `∃ C > 0, ∀ …` with `C`
 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.
+book's special cases (`Fin K`, unit variance, Gaussian or Bernoulli arms where an exponential family
+works, oblivious tables, learning rates tuned to the horizon, $\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
@@ -117,7 +140,8 @@ dependency versions used to check the interfaces (LML `53be244`, Mathlib `2e318f
 
 | 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`) |
+| Interaction protocol and law of a run | [LML `Algorithm.lean`][lml-alg] (`Algorithm`, `Environment`, `IsAlgEnvSeq`, `history`, `IsAlgEnvSeq.filtration`, `IsAlgEnvSeq.filtrationObs`: the history before round `t` and the observation of round `t`), [`IonescuTulceaSpace.lean`][lml-it] (`trajMeasure`, `IT.isAlgEnvSeq_trajMeasure`, `IsAlgEnvSeq.map_trajectory`) |
+| Means of the feedback laws | [LML `Means.lean`][lml-means] (`Environment.means`, `IsAlgEnvSeq.condExp_feedback`, `means_bandit`) |
 | 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) |
@@ -127,7 +151,9 @@ dependency versions used to check the interfaces (LML `53be244`, Mathlib `2e318f
 | Sub-Gaussian concentration and martingales | Mathlib [`SubGaussian.lean`][ml-subg] (`HasSubgaussianMGF`, `HasCondSubgaussianMGF`, `hasSubgaussianMGF_of_mem_Icc`, `measure_sum_ge_le_of_iIndepFun`, `measure_sum_ge_le_of_hasCondSubgaussianMGF`), [`OptionalStopping.lean`][ml-os] (`maximal_ineq`), `Supermartingale` |
 | Laws | Mathlib `gaussianReal`, `bernoulliMeasure`, `multivariateGaussian`; Tau Ceti [`Gaussian/Cdf.lean`][tc-gauss] (`measureReal_Ioi_gaussianReal`) |
 | Convex analysis | LML [`Bregman/Basic.lean`][lml-breg] (`bregDiv`, notation `D_[f](x, y, J)`, `bregDiv_three_point`), [`Subgradient/`][lml-subgrad]; Tau Ceti [`Conjugate.lean`][tc-conj] (`fenchelConjugate`, for a bilinear pairing), [`Strong.lean`][tc-strong] (`StrongConvexOn.add_add_le_of_hasFDerivWithinAt`); Mathlib `StrongConvexOn`, `PiLp`; LMLExplore `simplex` (`Analysis/Convex/Simplex.lean`) |
-| Linear algebra | Mathlib `ContinuousLinearMap.IsPositive` and its Loewner order, `LinearMap.det`, `Matrix.det_one_add_replicateCol_mul_replicateRow`, `Matrix.add_mul_mul_inv_eq_sub`; Tau Ceti [`Frame.lean`][tc-frame] (`frameOperator`) and [`AffineNormalization.lean`][tc-affine] (`IsCompact.exists_affineBasis_abs_coord_le_one`) |
+| Linear algebra | Mathlib `ContinuousLinearMap.IsPositive` and its Loewner order, `LinearMap.det`, `Matrix.det_one_add_replicateCol_mul_replicateRow`, `Matrix.add_mul_mul_inv_eq_sub`; Tau Ceti [`Frame.lean`][tc-frame] (`frameOperator`), [`AffineNormalization.lean`][tc-affine] (`IsCompact.exists_affineBasis_abs_coord_le_one`) and [`MoorePenrose.lean`][tc-mp] (`LinearMap.moorePenroseInverse`, `LinearMap.IsMoorePenroseInverse`, `LinearEquiv.moorePenroseInverse_eq_symm`) |
+| Designs | Mathlib `Convexity.StdSimplex` (finitely supported probability weights; `StdSimplex.map`, `StdSimplex.range_toFun_comp_weights`) |
+| LMLExplore material that the general forms below extend | exponential families (`Probability/Distributions/ExponentialFamily/`: `Measure.expFamily`, `expFamilyMeans`, `natParam`, `expFamilyDiv`), MGF domination (`MGFDominatedAbove`, `MGFDominatedBelow`, `mgfDominatedAbove_bernoulliMeasure`, `mgfDominatedBelow_bernoulliMeasure`), the Bandits algorithms `ucbF`, `klucb`, `gaussianTS`, `exp3`, `exp3IX`, `exp4` and the lower-bound files, follow-the-perturbed-leader policies (`perturbedLeaderAlgorithm`, `PerturbedLeader.lintegral_pullCount_le`), the FTRL lemma `sum_apply_sub_le_ftrl` (time-varying regularizers), `ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le` (second-order Bregman bound), `softmax_regret_le`, `IsUnbiasedRound`, `designOp`, `ridgeEstimate` |
 
 The [Kiefer–Wolfowitz formalization in `colt-2026-83`][kw] (Apache-2.0, no `sorry`) proves the
 existence of G-optimal designs for compact spanning subsets of `EuclideanSpace ℝ ι`
@@ -146,12 +172,12 @@ dependency sync that brings the rename updates this roadmap and the code togethe
 | Layer | Content | Prerequisites |
 | --- | --- | --- |
 | 0 | Instances, binary relative entropy, policies, regret notions | LML framework |
-| 1 | Concentration and maximal inequalities | Layer 0 |
+| 1 | Concentration and maximal inequalities | Layer 0; Identification roadmap Layers 1.2, 4.1 and 4.2 |
 | 2 | UCB-type algorithms for sub-Gaussian rewards | Layers 0–1; LML UCB |
-| 3 | KL-UCB for rewards in $[0,1]$ | Layers 0–1 |
-| 4 | Lower bounds for finitely many arms | Layer 0; LML divergence decomposition |
-| 5 | Thompson sampling | Layers 0–1; Layer 4 for asymptotic optimality |
-| 6 | Convex analysis and online linear optimization | Layer 0 |
+| 3 | KL-UCB for exponential families | Layers 0–1; Identification roadmap Layer 1.2 |
+| 4 | Lower bounds for finitely many arms | Layer 0; LML divergence decomposition; Layers 2–3 for item 5 |
+| 5 | Thompson sampling | Layers 0–1; Identification roadmap Layer 1.2; Layer 4 for asymptotic optimality |
+| 6 | Convex analysis, online linear and convex optimization | Layer 0 |
 | 7 | Adversarial bandits with finitely many arms and expert advice | Layers 0, 6; Layer 4.5 for the lower bound |
 | 8 | Least squares, self-normalized bounds, optimal design | Layer 1 |
 | 9 | Stochastic linear bandits | Layers 0, 8; Layer 4 tools for lower bounds |
@@ -187,17 +213,31 @@ dependency sync that brings the rename updates this roadmap and the code togethe
    $A_t=a$ then $I_t(a)\ge I_t(b)$ for all $b$; an arm with index $+\infty$ is pulled before any arm
    with a finite index; under an index that is $+\infty$ exactly on unpulled arms, every arm is
    pulled once during the first $k$ rounds.
-5. **Adversarial and expert regrets.** Define the adversarial regret $R_n(x)$ of the Conventions for
-   runs against `onlineEvalEnv x _`, and for bandits with expert advice the regret
-   $R_n=\mathbb E\big[\max_{m}\sum_{t<n}\langle E^{(t)}_m,x_t\rangle-\sum_{t<n}x_t(A_t)\big]$ of
-   [LS, (18.6)], where the advice $E^{(t)}\in\Delta(\alpha)^M$ is the observation of round $t$ of an
-   environment with deterministic observations and bandit feedback. Construct that environment.
-   Prove that for i.i.d. reward tables the expected adversarial regret dominates the stochastic
-   regret (used in Layer 4.5).
+5. **Adversarial and expert regrets.** Define the pseudo-regret $\bar R_n$ and the random regret
+   $\hat R_n$ of the Conventions for runs against any environment `env : Environment 𝓞 α ℝ` with
+   integrable feedback laws, and prove $\bar R_n\le\mathbb E[\hat R_n]$. Prove that against
+   `onlineEvalEnv x _` the pseudo-regret is the adversarial regret $R_n(x)$ and the random regret
+   is $\max_a\sum_{t<n}(x_t(a)-x_t(A_t))$ [LS, Chapter 12], and that against `stationaryEnv ν` with
+   integrable arms the pseudo-regret is `P[regret ν A n]`. Construct the environment of a
+   deterministic adaptive adversary, whose feedback at round $t$ is $x_t(h,o)(a)$ for measurable
+   tables $x_t:\mathrm{Hist}_t\times\mathcal O\to(\alpha\to\mathbb R)$; `onlineEvalEnv x _` is the
+   case of tables that do not depend on $(h,o)$. For bandits with expert advice, the advice
+   $E_t\in\Delta(\alpha)^M$ of round $t$ is a measurable function of the observation of round $t$,
+   and the expert pseudo-regret and random regret are
+   $\bar R^E_n=\max_m\mathbb E\big[\sum_{t<n}(\langle E_t(m),m_t\rangle-Y_t)\big]$ and
+   $\hat R^E_n=\max_m\sum_{t<n}(\langle E_t(m),m_t\rangle-Y_t)$ ([LS, (18.6)] for advice and
+   tables fixed in advance); with the $k$ experts that each recommend one arm they are $\bar R_n$
+   and $\hat R_n$. Construct the environment with
+   deterministic observations (the advice) and bandit feedback. Prove that for i.i.d. reward tables
+   the expected adversarial regret dominates the stochastic regret: the law of the first $n$ rounds
+   against `stationaryEnv ν` is the mixture, over tables $x$ whose rows $x_t$ are independent with
+   law $\bigotimes_a\nu_a$, of the laws against `onlineEvalEnv x _`, so that
+   $\mathbb E_x[R_n(x)]\ge\mathbb E_\nu[R_n]$ (used in Layer 4.5).
 
 Completion examples: a one-armed bandit has zero regret for every algorithm; Gaussian and Bernoulli
 instances satisfy the sub-Gaussian and boundedness hypotheses used later;
-$U(p,0)=p$, $U(1,c)=1$, and $U(p,c)\to1$ as $c\to\infty$.
+$U(p,0)=p$, $U(1,c)=1$, and $U(p,c)\to1$ as $c\to\infty$; the pseudo-regret of every algorithm
+against an environment with a single arm is $0$.
 
 ## Layer 1: Concentration and maximal inequalities
 
@@ -210,22 +250,30 @@ $U(p,0)=p$, $U(1,c)=1$, and $U(p,c)\to1$ as $c\to\infty$.
    $\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
+3. **Per-arm statements on runs.** The transfer of events about the first $s$ rewards of each arm
+   from a run of any algorithm against `stationaryEnv ν` to LML's reward-stream model, for all $s$
+   simultaneously, is the Identification roadmap's Layer 4.1. Its single-arm counting form for real
+   rewards bounds
    $\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
+   by the corresponding i.i.d. quantity; the lemmas of item 5 and of Layer 3.2 are proved in the
+   stream model and transferred to runs by it.
+4. **Chernoff bounds in rate-function form.** The Cramér–Chernoff bound under domination by a member
+   of an exponential family, at every level through the rate function, is the Identification
+   roadmap's Layer 1.2. Its conditional, time-uniform form (conditional MGF domination, the
+   supermartingale $\exp(\lambda S_t-\psi(\lambda)N_t)$ of a sum sampled along a predictable
+   sequence, and Ville's inequality, as in the proof of [GC11, Theorem 10]) is that roadmap's
+   Layer 4.2. Prove here the bounded instance: a random variable with values in $[0,1]$ whose
+   conditional mean given a σ-algebra is at most (at least) $m$ is conditionally dominated above
+   (below) by $\mathcal B(m)$ [GC11, Lemma 9; LS, Note 10.3.1], and the rate function of
+   $\mathcal B(m)$ at a level $p\in[0,1]$ is `klBer p m`. Deduce for i.i.d. $X_i\in[0,1]$ with mean
+   $\mu$ [LS, Lemma 10.3]: $P(\hat\mu_n\ge\mu+\varepsilon)\le\exp(-n\,d(\mu+\varepsilon,\mu))$ for
+   $\varepsilon\in[0,1-\mu]$ and the lower tail, the boundary levels $0$ and $1$ included, and
    [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.
+   e^{-s\varepsilon^2/(2\sigma^2)}\le 5\sigma^2/\varepsilon^2$ of [LS, Exercise 8.1]. Scale the
+   constants with $\sigma^2$ as in Layer 2. The lemmas of KL-UCB, [LS, Lemmas 10.7 and 10.8], are
+   Layer 3.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.
@@ -244,11 +292,14 @@ unpulled arms are $+\infty$.
    $\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
+2. **Asymptotically optimal UCB.** Define the index policy `ucbF σ2` 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$.
+   This index is the KL-UCB index of the Gaussian family of variance $\sigma^2$ (Layer 3.3), and the
+   eventual form is also the Gaussian instance of Layer 3.4; the explicit constants above keep the
+   proof through [LS, Lemma 8.2].
 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$.
@@ -257,18 +308,82 @@ Generalization: arbitrary finite arm types and variance proxies, where [LS] has
 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]:
+## Layer 3: KL-UCB for exponential families
+
+Throughout, a *family* is an exponential family of the Identification roadmap's Layer 1.2 with the
+identity statistic, since rewards are real (a family $(\rho,T)$ enters through the natural family
+of `ρ.map T`, which has the same means and divergence): a probability measure $\rho$ on
+$\mathbb R$, its members $\rho_\theta=$ `ρ.expFamily id θ` for $\theta$ in the interior
+$\Theta_\rho$ of `integrableExpSet id ρ`, its open interval of means $M_\rho=$
+`ρ.expFamilyMeans id`, the member $\rho_{(q)}$ of mean $q\in M_\rho$ (natural parameter
+$\eta_\rho(q)=$ `ρ.natParam id q`), the divergence $d_\rho(x,q)=$ `ρ.expFamilyDiv id x q` on
+$M_\rho\times M_\rho$, and its extension $\bar d_\rho(x,q)\in[0,\infty]$ to every level
+$x\in\mathbb R$, the Cramér–Chernoff rate function of $\rho_{(q)}$ at $x$. Each arm $a$ has its
+own family $\rho_a$. Arm $a$ is *dominated by its family* if its mean $\mu_a$ lies in
+$M_{\rho_a}$ and its law $\nu_a$ is MGF-dominated above and below by $\rho_{a,(\mu_a)}$
+(LMLExplore's `MGFDominatedAbove`, `MGFDominatedBelow`). Laws on $[0,1]$ with mean in $(0,1)$ are
+dominated by the Bernoulli family (`mgfDominatedAbove_bernoulliMeasure`,
+`mgfDominatedBelow_bernoulliMeasure`), σ²-sub-Gaussian laws by the Gaussian family of variance
+$\sigma^2$ (Identification roadmap, Layer 4.2), and the members of a family by the family itself.
+
+1. **Upper confidence levels.** For a family $\rho$, $x\in\mathbb R$ and $c\in[0,\infty]$, define
+   $U_\rho(x,c)=\sup\big(\{x\}\cup\{q\in M_\rho:x\le q,\ \bar d_\rho(x,q)\le c\}\big)$ in `EReal`.
+   Prove that it is measurable in $(x,c)$, monotone in both arguments and at least $x$, and that
+   $q\le U_\rho(x,c)$ iff $\bar d_\rho(x,q)\le c$ for $x\le q\in M_\rho$, since
+   $q\mapsto \bar d_\rho(x,q)$ is continuous and increasing on $M_\rho\cap[x,\infty)$. Prove the
+   three-point identity
+   $\bar d_\rho(x,\mu)=\bar d_\rho(x,q)+d_\rho(q,\mu)+(q-x)(\eta_\rho(\mu)-\eta_\rho(q))$ for
+   $x\in\mathbb R$ and $q,\mu\in M_\rho$, whose last term is nonnegative for $x\le q\le\mu$ (for
+   Bernoulli laws this gives the inequality $d(p,q-\varepsilon)\le d(p,q)-d(q-\varepsilon,q)$ of
+   Layer 0.2). Instances: for the Bernoulli family, $\bar d_\rho(x,q)=$ `klBer x q` for
+   $x\in[0,1]$ (Layer 1.4) and $U_\rho(x,c)$ is the level $U(x,c)$ of Layer 0.2 for $x\in[0,1]$; for the Gaussian family of
+   variance $\sigma^2\ne0$, $\bar d_\rho(x,q)=(x-q)^2/(2\sigma^2)$ and
+   $U_\rho(x,c)=x+\sqrt{2\sigma^2c}$ for finite $c$.
+2. **Concentration lemmas.** Let $X_1,X_2,\dots$ be independent and dominated by the member
+   $\rho_{(\mu)}$ of a family, with empirical mean $\hat\mu_s$ after $s$ samples. Prove the
+   generalization of [LS, Lemma 10.8]: for $\varepsilon>0$ and $\mu+\varepsilon<c$ with
+   $\mu+\varepsilon,c\in M_\rho$, and $L\ge0$,
+   $\sum_{s<n}P\big(s=0\ \lor\ c\le\hat\mu_s\ \lor\ s\,\bar d_\rho(\hat\mu_s,c)\le L\big)\le
+   1+\frac{L}{d_\rho(\mu+\varepsilon,c)}+\frac1{d_\rho(\mu+\varepsilon,\mu)}$. Prove the
+   generalization of [LS, Lemma 10.7]: for $\varepsilon>0$ with $\mu-\varepsilon\in M_\rho$ and
+   $s\ge1$, $P\big(U_\rho(\hat\mu_s,L/s)\le\mu-\varepsilon\big)\le e^{-L}e^{-s\,d_\rho(\mu-\varepsilon,\mu)}$,
+   by the three-point identity and the Chernoff bound of Layer 1.4; and in a run of any algorithm
+   against `stationaryEnv ν`, with the exploration level $\log f(t+1)$ at Lean round $t$, the
+   expected number of rounds at which an arm with law $\nu_a$ dominated by $\rho_{(\mu)}$ has been
+   pulled and has index $U_\rho(\hat\mu_a,\log f(t+1)/T_a)\le\mu-\varepsilon$ is at most
+   $3/(2\,d_\rho(\mu-\varepsilon,\mu))$. For rewards in $[0,1]$ with mean in $(0,1)$, Pinsker's
+   inequality $d(p,q)\ge2(p-q)^2$ (Layer 0.2) turns these into [LS, Lemmas 10.7 and 10.8], with the
+   constants $3/(4\varepsilon^2)$ and $1/(2\varepsilon^2)$.
+3. **Algorithm.** Define KL-UCB for families $(\rho_a)_a$ [LS, Algorithm 8; GC11, Section 4]: the
+   index policy with index $U_{\rho_a}(\hat\mu_a,\log f(t)/T_a)$, $f(t)=1+t\log^2t$, and $+\infty$
+   for unpulled arms. Define `klucb`, KL-UCB for rewards in $[0,1]$, as the instance with the
+   Bernoulli family on every arm, and prove that its index is the index
+   $U(\hat\mu_a,\log f(t)/T_a)$ of [LS, Algorithm 8] (with $U$ of Layer 0.2) at empirical means in
+   $[0,1]$. Prove that `ucbF σ2` (Layer 2.2) is the instance with the Gaussian family of variance
+   $\sigma^2$ on every arm.
+4. **Regret.** Let every arm be dominated by its family, let $a^*$ be an optimal arm and $a$ an
+   arm with $\Delta_a>0$. For $\varepsilon_1,\varepsilon_2>0$ with
+   $\varepsilon_1+\varepsilon_2<\Delta_a$, $\mu_a+\varepsilon_1,\mu^*-\varepsilon_2\in M_{\rho_a}$
+   and $\mu^*-\varepsilon_2\in M_{\rho_{a^*}}$, prove
+   $$\mathbb E[T_a(n)]\le1+\frac{\log f(n)}{d_{\rho_a}(\mu_a+\varepsilon_1,\mu^*-\varepsilon_2)}+\frac1{d_{\rho_a}(\mu_a+\varepsilon_1,\mu_a)}+\frac3{2\,d_{\rho_{a^*}}(\mu^*-\varepsilon_2,\mu^*)},$$
+   the resulting bound on $\mathbb E[R_n]$, and, when $\mu^*\in M_{\rho_a}$ for every arm $a$ with
+   $\Delta_a>0$, the eventual form
+   $\limsup_n\mathbb E[R_n]/\log n\le\sum_{a:\Delta_a>0}\Delta_a/d_{\rho_a}(\mu_a,\mu^*)$
+   [GC11; CGMMS13]. Deduce, as the Bernoulli instance, [LS, Theorem 10.6] for rewards in $[0,1]$
+   almost surely:
    $$\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.
+   and $\limsup_n\mathbb E[R_n]/\log n\le\sum_{a:\Delta_a>0}\Delta_a/d(\mu_a,\mu^*)$, arms with
+   mean $0$ or $1$ (Dirac laws, outside the open Bernoulli family) being treated directly (the book
+   leaves this limit to its Exercise 10.2; its proof writes $f(n)$ for $\log f(n)$ in the last
+   line). Deduce, as the Gaussian instance, the eventual form of Layer 2.2 for σ²-sub-Gaussian
+   rewards.
+
+Generalization: one exponential family per arm and reward laws dominated by their family members,
+where [LS] states Bernoulli rewards and [GC11, CGMMS13] one family whose members are the reward
+laws. Completion examples: arms with means $0$ or $1$ in the $[0,1]$ instance; a two-armed Bernoulli
+bandit; the boundary empirical means of the Bernoulli family, $U(0,c)=1-e^{-c}$ and $U(1,c)=1$;
+exponential rewards (`expMeasure`, $d(x,q)=x/q-1-\log(x/q)$); Gaussian arms with different known
+variances.
 
 ## Layer 4: Lower bounds for finitely many arms
 
@@ -291,42 +406,69 @@ examples: arms with means $0$ or $1$ (the singular values of $d$), and a two-arm
    $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
+   with the sum in `ℝ≥0∞`. Compute $d_{\inf}$ for exponential families [BK96]: for a family
+   $\rho$ of Layer 3 with members $\mathcal M_\rho=\{\rho_\theta:\theta\in\Theta_\rho\}$,
+   $\mu\in M_\rho$ and $m\ge\mu$, $d_{\inf}(\rho_{(\mu)},m,\mathcal M_\rho)=d_\rho(\mu,m)$ if
+   $m\in M_\rho$ and $\infty$ if $m\ge\sup M_\rho$. The Gaussian (known variance) and Bernoulli
+   entries of [LS, Table 16.1] are instances. 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
+5. **Asymptotic optimality and the adversarial lower bound.** For families $(\rho_a)_a$ with a
+   common set of means $M$ (one family for all arms, or Gaussian families with different
+   variances), prove that KL-UCB (Layer 3) is consistent over the bandits whose arm $a$ has a law in
+   $\mathcal M_{\rho_a}$ and attains the Lai–Robbins constant there: its expected regret is
+   $c^*\log n+o(\log n)$ with $c^*=\sum_{a:\Delta_a>0}\Delta_a/d_{\rho_a}(\mu_a,\mu^*)$. The
+   algorithms of Layers 2.2 and 3 on Gaussian arms and on Bernoulli arms are instances, Bernoulli
+   arms with mean $0$ or $1$ being treated directly. 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.
+Generalization: the minimax bound for a family of laws rather than unit-variance Gaussians;
+$d_{\inf}$ and asymptotic optimality for every exponential family rather than Gaussian and
+Bernoulli arms.
 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].
+1. **Algorithm.** For families $(\rho_a)_a$ of Layer 3 with log-partition functions
+   $\psi_a=$ `cgf id (ρ a)` and priors $\pi_a$, σ-finite measures on $\Theta_{\rho_a}$, define
+   Thompson sampling. At each round, for each arm $a$ pulled $s\ge1$ times with reward sum $S$,
+   draw independently a natural parameter $\theta_a$ from the posterior, the probability measure
+   proportional to $e^{\theta S-s\psi_a(\theta)}\,\pi_a(d\theta)$, and take its mean
+   $\psi_a'(\theta_a)$ as the perturbation of $a$ (the perturbation is $+\infty$ where the
+   normalizing constant is $0$ or infinite, and for unpulled arms); play `argmax`. This is a
+   follow-the-perturbed-leader policy whose laws depend on the history only through the number of
+   pulls and the reward sum of each arm (LMLExplore's `perturbedLeaderAlgorithm`). The Jeffreys
+   prior is $\pi_J(d\theta)=\sqrt{\psi''(\theta)}\,d\theta$ on $\Theta_\rho$ [KKM13, Section 2].
+   Gaussian Thompson sampling with variance proxy $\sigma^2$ and flat prior (LMLExplore's
+   `gaussianTS`: $\theta_a\sim\mathcal N(\hat\mu_a,\sigma^2/T_a)$) is the instance with the
+   Gaussian family of variance $\sigma^2$ and its Jeffreys prior, a constant multiple of Lebesgue
+   measure; define it as that instance. 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_{s<n}(1/G_{a^*s}-1)\big]+\mathbb E\big[\sum_{s<n}\mathbb 1\{G_{as}>1/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
+3. **Frequentist regret.** Let one family $\rho$ serve all arms, with Jeffreys posteriors that are
+   finite measures after every number $s\ge1$ of pulls, for almost every sum of $s$ independent
+   draws from $\rho$. For bandits whose arm laws are members of $\rho$, prove that Thompson sampling
+   with the Jeffreys prior satisfies
+   $\mathbb E[R_n]/\log n\to\sum_{a:\Delta_a>0}\Delta_a/d_\rho(\mu_a,\mu^*)$ [KKM13, Theorem 1]
+   (upper bound in eventual form, matched by Layer 4.4). For Gaussian bandits with variance
+   $\sigma^2$ this is the asymptotic part of [LS, Theorem 36.3]; prove its minimax part
    $\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
+Generalization: exponential families and priors on the natural parameter, arbitrary variance proxy
+and finite arm type, where [LS] treats Gaussian arms. 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.
+a prior over environments); do not restate its results. Completion example: for Bernoulli arms the
+Jeffreys prior on the mean is $\mathrm{Beta}(1/2,1/2)$, with posterior
+$\mathrm{Beta}(1/2+S,1/2+s-S)$ [KKM13, Figure 1].
 
-## Layer 6: Convex analysis and online linear optimization
+## Layer 6: Convex analysis, online linear and convex optimization
 
 Work in a finite-dimensional real normed space `E`, paired with its dual `E →L[ℝ] ℝ` by
 `(x, y) ↦ y x`; this is the bilinear pairing that Tau Ceti's `fenchelConjugate` takes. Losses and
@@ -335,7 +477,8 @@ against `u` after `n` rounds is $\sum_{t<n}y_t(a_t-u)$. Strong convexity refers
 (Mathlib's `StrongConvexOn`), and the norm of a loss is its operator norm, the dual norm. Losses
 are minimized. Statements whose proofs do not use the dimension, such as the FTRL bounds of item 3,
 are stated without it. The merged FTRL development of LMLExplore is restated in this generality by
-the [Refactors](../../Completed/Refactors/README.md) roadmap, Layer 0.1.
+the [Refactors](../../Completed/Refactors/README.md) roadmap, Layer 0.1. Learning rates follow the
+Conventions; [Ora] is cited by the numbering of its tenth arXiv version.
 
 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
@@ -353,80 +496,180 @@ the [Refactors](../../Completed/Refactors/README.md) roadmap, Layer 0.1.
    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$,
+   from past actions. Then let the regularizer change over the rounds:
+   - *Time-varying regularizers.* For regularizers $\psi_t$ nondecreasing in $t$ on $\mathcal A$,
+     plays $a_t\in\mathcal A$ minimizing $\sum_{s<t}y_s+\psi_t$ over $\mathcal A$, and derivatives
+     $\psi'_t$ of $\psi_t$ within $\mathcal A$ at $a_t$, prove
+     $\sum_{t<n}y_t(a_t-u)\le\psi_n(u)-\psi_0(a_0)+\sum_{t<n}\big(y_t(a_t-a_{t+1})-D_{\psi_t}(a_{t+1},a_t)\big)$
+     for $u\in\mathcal A$, from LMLExplore's FTRL lemma `sum_apply_sub_le_ftrl` [Ora, Lemma 7.1].
+     For $\psi_t=F/\eta_t$ with $F\ge0$ on $\mathcal A$ and nonincreasing $\eta_t>0$ this is the
+     anytime form of [LS, Theorem 28.5]; for $F$ $m$-strongly convex deduce
+     $\sum_{t<n}y_t(a_t-u)\le F(u)/\eta_{n-1}+\sum_{t<n}\eta_t\|y_t\|^2/(2m)$ [Ora, Corollary 7.6].
+   - *Mirror descent with nonincreasing learning rates.* For $F$ $m$-strongly convex and
+     $D_F(u,a_t)\le D$ for $t<n$, prove
+     $\sum_{t<n}y_t(a_t-u)\le D/\eta_{n-1}+\sum_{t<n}\eta_t\|y_t\|^2/(2m)$ [Ora, Theorem 6.11].
+   - *Local norms* [LS, Theorem 26.13; Ora, Lemma 7.15]. Bound each stability term
+     $y_t(a_t-a_{t+1})-D_F(a_{t+1},a_t)/\eta_t$ through the Hessian of $F$ (item 2, LMLExplore's
+     `ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le`): it is at most $\eta_tc_t/2$ for
+     every $c_t\ge0$ with $y_t(v)^2\le c_t\,\nabla^2F(z_t)(v,v)$ for all $v$, at some
+     $z_t\in[a_t,a_{t+1}]$. Deduce the FTRL and mirror descent bounds with these local norms in
+     place of $\|y_t\|^2$, which is unbounded for importance-weighted estimates.
+4. **Instances.** Prove [LS, Proposition 28.6] (unit ball, $F=\tfrac12\|a\|^2$,
    $\eta=n^{-1/2}$: $R_n\le\sqrt n$) on a real inner product space, with the losses
    `InnerProductSpace.toDual ℝ E g` of vectors of norm at most `1`. Prove [LS, Proposition 28.7]
    (simplex, unnormalized negative entropy, $\eta=\sqrt{2\log(d)/n}$: $R_n\le\sqrt{2n\log d}$)
    on `E = PiLp 1 (fun _ : α ↦ ℝ)`, whose dual norm is the sup norm, from the `1`-strong convexity
    of the negative entropy on the simplex for the `ℓ¹` norm (Pinsker's inequality). Identify the
    latter with exponential weights over a finite set, stated on `α → ℝ` with LMLExplore's
-   `simplex α`.
-
-Generalization: a normed space with losses in its dual, rather than $\mathbb R^d$ with the
-Euclidean pairing; the instances are corollaries.
+   `simplex α`. For nonnegative losses and nonincreasing learning rates, prove the local-norm bound
+   of exponential weights $p_t=\mathrm{softmax}(-\eta_t\sum_{s<t}y_s)$ [Ora, Section 7.5;
+   BCB12, proof of Theorem 3.1]: for $p\in$ `simplex α`, $y\ge0$ and $\eta\ge0$,
+   $\sum_ap_a(e^{-\eta y_a}-1+\eta y_a)\le\frac{\eta^2}2\sum_ap_ay_a^2$; the stability term of FTRL
+   with the negative entropy at $p$ and a nonnegative loss $y$,
+   $\sup_{q}\big(\langle p-q,y\rangle-\mathrm{KL}(q,p)/\eta\big)=\langle p,y\rangle+\frac1\eta\log\sum_ap_ae^{-\eta y_a}$
+   over `simplex α`, is at most $\frac1\eta\sum_ap_a(e^{-\eta y_a}-1+\eta y_a)$; hence, by item 3,
+   $\sum_{t<n}(\langle p_t,y_t\rangle-y_t(a))\le\frac{\log k}{\eta_{n-1}}+\sum_{t<n}\frac{\eta_t}2\langle p_t,y_t^2\rangle$.
+   LMLExplore's `softmax_regret_le` is its constant case.
+5. **Estimated losses.** Prove [LS, Theorem 28.10] for losses chosen by an adaptive adversary.
+   Given, for each round $t$, a σ-algebra $\mathcal G_t$ for which the play $a_t$ and the loss
+   $y_t$ are measurable, an action $A_t$ with conditional mean $a_t$ given $\mathcal G_t$, and an
+   estimate $\hat Y_t$ with conditional mean $y_t$ given $\mathcal G_t$:
+   $\mathbb E\big[\sum_{t<n}y_t(A_t-u)\big]=\mathbb E\big[\sum_{t<n}\hat Y_t(a_t-u)\big]$ for
+   $u\in E$, so that pathwise bounds of items 3–4 on the estimated losses bound the expected
+   regret. Deterministic losses (LMLExplore's `IsUnbiasedRound`) are the oblivious case.
+6. **Online convex optimization.** For convex losses $f_t:E\to\mathbb R$ and plays
+   $a_t\in\mathcal A$ with a subgradient $g_t$ of $f_t$ within $\mathcal A$ at $a_t$ (LML's
+   `HasSubgradientWithinAt`), $\sum_{t<n}(f_t(a_t)-f_t(u))\le\sum_{t<n}g_t(a_t-u)$ for
+   $u\in\mathcal A$, so FTRL and mirror descent run on the linearized losses $g_t$, which are chosen
+   from the past plays, inherit the bounds of items 3–4 [Ora, Section 2.3]. Prove the Euclidean
+   instance, projected online subgradient descent [Zin03; Ora, Section 2.2]: on a convex set of
+   diameter $D$ in a real inner product space, with $\|g_t\|\le G$ and $\eta_t=D/(G\sqrt{t+1})$,
+   the regret is at most $\frac32DG\sqrt n$.
+
+Generalization: a normed space with losses in its dual, time-varying regularizers, adaptively chosen
+losses and convex losses through their subgradients, rather than $\mathbb R^d$ with the Euclidean
+pairing, a fixed learning rate and linear losses; 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_{t<n}(y_t(A_t)-y_t(a))$, $y=1-x$.
-4. **Exp4.** Define Exp4 [LS, Algorithm 11] for $M$ experts and prove [LS, Lemma 18.2] and
-   [LS, Theorem 18.1]: with $\gamma=0$ and $\eta=\sqrt{2\log(M)/(nk)}$, $R_n\le\sqrt{2nk\log M}$.
-   Show that Exp3 is Exp4 with the $k$ experts that each recommend one arm.
-
-Completion checks: for $k=1$ every bound is $0$; the lower bound of Layer 4.5 shows the order
-$\sqrt{nk}$ of item 2 is attained up to $\sqrt{\log k}$.
+Runs against an environment `env : Environment 𝓞 α ℝ` whose feedback laws are supported in
+$[0,1]$: an adaptive adversary (Conventions), which includes oblivious tables `onlineEvalEnv x _`
+with $x_t(a)\in[0,1]$ and stochastic bandits `stationaryEnv ν` with rewards in $[0,1]$.
+Expectation bounds are on the pseudo-regret $\bar R_n$, high-probability bounds on the random
+regret $\hat R_n$ (Layer 0.5). Learning rates $\eta_t>0$ and implicit-exploration parameters
+$\gamma_t\ge0$ are nonincreasing sequences (Conventions).
+
+1. **Importance-weighted estimators.** For a weight-based policy (Layer 0.3) with weights $P_t$,
+   define the standard and loss-based estimators [LS, (11.3), (11.6)] and the implicit-exploration
+   estimator $\hat Y_t(a)=\mathbb 1\{A_t=a\}(1-Y_t)/(P_t(a)+\gamma_t)$ [LS, (12.4); Neu15, (3)].
+   Conditionally on the history before round $t$ and the observation of round $t$ (LML's
+   `IsAlgEnvSeq.filtrationObs`), prove unbiasedness for $\gamma_t=0$ and positive weights,
+   $\mathbb E[\hat Y_t(a)\mid\cdot]=1-m_t(a)$, the bias bound
+   $\mathbb E[\hat Y_t(a)\mid\cdot]\le1-m_t(a)$ for $\gamma_t\ge0$, and the conditional variance
+   formulas [LS, (11.4), (11.5)].
+2. **Exp4-IX.** For a finite set of $M$ experts and a measurable advice map from observations to
+   advice $E_t\in\Delta(\alpha)^M$, define Exp4-IX [Neu15, Section 3.2] with learning rates $\eta_t$
+   and implicit exploration $\gamma_t$: expert weights
+   $Q_t=\mathrm{softmax}\big(-\eta_t\sum_{s<t}E_s\hat Y_s\big)$, where
+   $(E_s\hat Y_s)(m)=\langle E_s(m),\hat Y_s\rangle$, the arm drawn from
+   $P_t=\sum_mQ_t(m)E_t(m)$, and the estimates $\hat Y_t$ of item 1. Define Exp4
+   [LS, Algorithm 11] as the case $\gamma=0$, and Exp3-IX [LS, Algorithm 10] and Exp3
+   [LS, Algorithm 9] as the cases with the experts $\alpha$, expert $b$ advising $\delta_b$ at every
+   observation, with arbitrary $\gamma$ and with $\gamma=0$ respectively; LMLExplore's `exp4`,
+   `exp3IX` and `exp3` become these instances. Prove that the expert weights $Q_t$ are the
+   exponential weights of Layer 6.4 on the estimated expert losses $E_s\hat Y_s$, so that its
+   local-norm bound holds pathwise ([LS, Lemma 18.2] for a constant rate).
+3. **Pseudo-regret.** For $\gamma=0$, prove
+   $\bar R^E_n\le\frac{\log M}{\eta_{n-1}}+\frac k2\sum_{t<n}\eta_t$ for Exp4, from item 2, item 1
+   and Layer 6.5, and the same bound with $M=k$ for $\bar R_n$ of Exp3. Deduce [LS, Theorem 18.1]
+   ($\eta=\sqrt{2\log(M)/(nk)}$: $\bar R^E_n\le\sqrt{2nk\log M}$), [LS, Theorem 11.2]
+   ($\eta=\sqrt{2\log(k)/(nk)}$: $\bar R_n\le\sqrt{2nk\log k}$) and [BCB12, Theorem 3.1]
+   ($\eta_t=\sqrt{\log(k)/(k(t+1))}$: $\bar R_n\le2\sqrt{nk\log k}$).
+4. **High-probability bounds.** Prove [LS, Lemmas 12.2–12.4] and both bounds of
+   [LS, Theorem 12.1] for Exp3-IX. Prove the concentration of the implicit-exploration estimates
+   [Neu15, Lemma 1]: for nonnegative weights $\alpha_{t,a}\le2\gamma_t$ measurable for the history
+   before round $t$ and the observation of round $t$, with probability at least $1-\delta$,
+   $\sum_{t<n}\sum_a\alpha_{t,a}\big(\hat Y_t(a)-(1-m_t(a))\big)\le\log(1/\delta)$. Deduce
+   [Neu15, Theorem 1] for anytime rates: with $\eta_t=2\gamma_t=\sqrt{\log(k)/(k(t+1))}$, Exp3-IX
+   has $\hat R_n\le4\sqrt{nk\log k}+\big(2\sqrt{nk/\log k}+1\big)\log(2/\delta)$ with probability at
+   least $1-\delta$; and [Neu15, Theorem 2] for Exp4-IX: with
+   $\eta_t=2\gamma_t=\sqrt{2\log(M)/(nk)}$,
+   $\hat R^E_n\le2\sqrt{2nk\log M}+\big(\sqrt{2nk/\log M}+1\big)\log(2/\delta)$ with probability at
+   least $1-\delta$.
+
+Generalization: adaptive adversaries, expert advice that depends on the history, anytime learning
+rates and a single algorithm for Exp3, Exp3-IX and Exp4, where [LS] fixes an oblivious table, a
+known horizon and three algorithms. Completion checks: for $k=1$ every bound is $0$; the lower bound
+of Layer 4.5 shows the order $\sqrt{nk}$ of item 3 is attained up to $\sqrt{\log k}$; with a single
+expert the expert pseudo-regret of Exp4 is nonpositive; against `stationaryEnv ν` with rewards in
+$[0,1]$, item 3 bounds the expected stochastic regret of Exp3 with anytime rates by
+$2\sqrt{nk\log k}$.
 
 ## Layer 8: Least squares, self-normalized bounds and optimal design
 
 Work in a finite-dimensional real inner product space `E` of dimension $d$, with linear operators
-`E →L[ℝ] E`; give matrix corollaries on `EuclideanSpace ℝ ι`.
-
-1. **Design operators.** For $\lambda\ge0$ and $x_0,x_1,\ldots\in E$, define
-   $V_t(\lambda)=\lambda\,\mathrm{id}+\sum_{s<t}x_s\otimes x_s$ (with $x\otimes x$ the operator
-   $v\mapsto\langle x,v\rangle x$, Tau Ceti's `frameOperator` for finite families), and the weighted
-   norm $\|v\|^2_{V^{-1}}=\langle v,V^{-1}v\rangle$. Prove positivity, invertibility for
-   $\lambda>0$, the rank-one update of the inverse (Sherman–Morrison) and of the determinant
+`E →L[ℝ] E`; give matrix corollaries on `EuclideanSpace ℝ ι`. Weighted norms use the inverse
+$V^{-1}$ (`Ring.inverse`) of operators that are invertible ($\lambda>0$, positive definite $V_0$)
+and the Moore–Penrose inverse $V^+$ (Tau Ceti's `LinearMap.moorePenroseInverse`) of operators that
+may be singular (unregularized least squares, designs).
+
+1. **Design operators.** For a positive operator $V_0$ and $x_0,x_1,\ldots\in E$, define
+   $V_t(V_0)=V_0+\sum_{s<t}x_s\otimes x_s$ (with $x\otimes x$ the operator
+   $v\mapsto\langle x,v\rangle x$, Tau Ceti's `frameOperator` for finite families), and
+   $V_t(\lambda)=V_t(\lambda\,\mathrm{id})$ for $\lambda\ge0$ (LMLExplore's `designOp`). Define
+   the weighted norms $\|v\|^2_{V^{-1}}=\langle v,V^{-1}v\rangle$ and
+   $\|v\|^2_{V^+}=\langle v,V^+v\rangle$. Prove $V^+=V^{-1}$ for invertible $V$, and, for positive
+   $V$, that $V^+$ is positive and $VV^+$ is the orthogonal projection onto the range of $V$ (for
+   $V_t(0)$, the span of $x_0,\dots,x_{t-1}$). Prove positivity, invertibility for positive
+   definite $V_0$ (in particular $\lambda>0$), 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<n}\min\{1,\|x_t\|^2_{V_t^{-1}}\}\le2\log\frac{\det V_n}{\det V_0}\le
    2d\log\frac{\operatorname{trace}V_0+nL^2}{d\det(V_0)^{1/d}}$.
-3. **Regularized least squares.** Define the ridge estimator
-   $\hat\theta_t=V_t(\lambda)^{-1}\sum_{s<t}x_sY_s$ and prove it minimizes the regularized squared
-   loss [LS, (19.4)–(19.6)].
+3. **Least squares.** For $\lambda\ge0$, define the estimator
+   $\hat\theta_t=V_t(\lambda)^+\sum_{s<t}x_sY_s$ and prove that it minimizes the regularized squared
+   loss [LS, (19.4)–(19.6)], and for $\lambda=0$ that it is the least-squares solution of minimal
+   norm. For $\lambda>0$ it is the ridge estimator $V_t(\lambda)^{-1}\sum_{s<t}x_sY_s$
+   (LMLExplore's `ridgeEstimate`).
 4. **Self-normalized bound.** On a filtered probability space, for an $E$-valued predictable
    sequence $x_t$ and real noise $\eta_t$ that is conditionally σ²-sub-Gaussian given the past and
    $x_t$, with $S_t=\sum_{s<t}\eta_sx_s$: prove that $\exp(\langle v,S_t\rangle-\frac{\sigma^2}2\|v\|^2_{V_t(0)})$
    is a supermartingale [LS, Lemma 20.2], its mixtures over probability measures are
-   supermartingales [LS, Lemma 20.3], and [LS, Theorem 20.4] with σ²:
-   $P\big(\exists t,\ \|S_t\|^2_{V_t(\lambda)^{-1}}\ge2\sigma^2\log\frac1\delta+\sigma^2\log\frac{\det V_t(\lambda)}{\lambda^d}\big)\le\delta$,
-   by the Gaussian mixture of covariance $(\lambda\,\mathrm{id})^{-1}$ and Ville's inequality.
+   supermartingales [LS, Lemma 20.3], and, for every positive definite $V_0$ [AYPS11, Theorem 1],
+   $P\big(\exists t,\ \|S_t\|^2_{V_t(V_0)^{-1}}\ge2\sigma^2\log\frac1\delta+\sigma^2\log\frac{\det V_t(V_0)}{\det V_0}\big)\le\delta$,
+   by the Gaussian mixture of covariance $V_0^{-1}$ and Ville's inequality. [LS, Theorem 20.4]
+   with σ² is the case $V_0=\lambda\,\mathrm{id}$, $\det V_0=\lambda^d$.
 5. **Confidence sets.** For $Y_t=\langle\theta_*,x_t\rangle+\eta_t$, prove [LS, Theorem 20.5] with
-   σ² and the bound $\det V_t(\lambda)/\lambda^d\le(1+nL^2/(\lambda d))^d$ [LS, (20.9)]; for a
-   fixed design and independent noise, prove [LS, (20.2)].
-6. **Kiefer–Wolfowitz.** For a design $\pi$ (a finitely supported probability on a set
-   $\mathcal A\subseteq E$), define $V(\pi)=\sum_a\pi(a)\,a\otimes a$ and
-   $g(\pi)=\sup_{a\in\mathcal A}\|a\|^2_{V(\pi)^{-1}}$. For compact $\mathcal A$ spanning $E$, prove
+   σ² and the bound $\det V_t(\lambda)/\lambda^d\le(1+nL^2/(\lambda d))^d$ [LS, (20.9)]. For a
+   fixed design $x_0,\dots,x_{t-1}$, whose operator $V=V_t(0)$ may be singular, independent
+   σ²-sub-Gaussian noise and the estimator $\hat\theta=V^+\sum_{s<t}x_sY_s$ of item 3, prove [LS, (20.2)]:
+   $P\big(\langle x,\hat\theta-\theta_*\rangle\ge\sqrt{2\sigma^2\|x\|^2_{V^+}\log(1/\delta)}\big)\le\delta$
+   for every $x$ in the span of the design.
+6. **Kiefer–Wolfowitz.** A design on a set $\mathcal A\subseteq E$ is a finitely supported
+   probability measure $\pi$ on $E$ with support in $\mathcal A$, an element of Mathlib's
+   `Convexity.StdSimplex ℝ E`; finite support is what compact infinite sets need
+   [LS, Exercise 21.3]. Define $V(\pi)=\sum_a\pi(a)\,a\otimes a$ and
+   $g(\pi)=\sup_{a\in\mathcal A}\|a\|^2_{V(\pi)^+}$. For compact $\mathcal A$ spanning $E$, prove
    [LS, Theorem 21.1] (minimizing $g$, maximizing $\log\det V$, and $g=d$ are equivalent, and a
    minimizer with support of size at most $d(d+1)/2$ exists) for compact sets, not only finite ones
-   [LS, Exercise 21.3]; and the non-spanning version: if $\dim\operatorname{span}\mathcal A=m$,
-   there is a design with support at most $m(m+1)/2$ and $\sup_{a}\|a\|^2_{V(\pi)^{+}}=m$, using
-   the inverse on the span [LS, Exercise 21.6]. Prove $\|a\|^2_{V(\pi^*)^{-1}}=d$ on the support
-   [LS, Exercise 21.5].
-
-Generalization: operators on an inner product space and σ²-sub-Gaussian noise. Completion examples:
+   [LS, Exercise 21.3]; and the non-spanning version: if $\dim\operatorname{span}\mathcal A=m\ge1$,
+   there is a design with support at most $m(m+1)/2$ and $g(\pi)=m$ [LS, Exercise 21.6]. Prove
+   $\|a\|^2_{V(\pi^*)^{-1}}=d$ on the support [LS, Exercise 21.5]. For designs on finitely many
+   arms with a feature map $\varphi:\alpha\to E$, prove LMLExplore's
+   `simplex α = Set.range (fun q : StdSimplex ℝ α ↦ ⇑q.weights)` (from Mathlib's
+   `StdSimplex.range_toFun_comp_weights`) and
+   $V(\varphi_*w)=\sum_aw_a\,\varphi(a)\otimes\varphi(a)$ for the image design
+   $\varphi_*w=$ `StdSimplex.map φ w`, so that allocations $w\in$ `simplex α` (Layer 10.1, the
+   Identification roadmap's Layer 9) are designs.
+
+Generalization: operators on an inner product space, any positive definite regularizer $V_0$,
+singular designs through the Moore–Penrose inverse, and σ²-sub-Gaussian noise. Completion examples:
 for the standard basis of $\mathbb R^d$ the uniform design is G-optimal with $g=d$; for the unit
-sphere the uniform distribution on an orthonormal basis is G-optimal.
+sphere the uniform distribution on an orthonormal basis is G-optimal; for $\lambda=0$ and data
+spanning a proper subspace, $\hat\theta_t$ lies in that subspace and $\|x\|^2_{V_t(0)^+}>0$ for
+every nonzero $x$ in it.
 
 ## Layer 9: Stochastic linear bandits
 
@@ -448,7 +691,8 @@ sphere the uniform distribution on an orthonormal basis is G-optimal.
 3. **Phased elimination.** For a finite action set $\mathcal A\subseteq E$ and gaps at most $1$,
    define phased elimination with G-optimal designs [LS, Algorithm 12] and prove [LS, Theorem 22.1]
    via [LS, Exercise 22.1], with an explicit constant. Do not assume that the surviving sets span
-   $E$: use the non-spanning design of Layer 8.6 on their span.
+   $E$: use the non-spanning design of Layer 8.6 on their span, and the least-squares estimator of
+   Layer 8.3 with $\lambda=0$ and its fixed-design bound (Layer 8.5).
 4. **Lower bounds.** With Gaussian noise, prove [LS, Theorem 24.1] (hypercube
    $[-1,1]^d$: some $\theta\in\{\pm n^{-1/2}\}^d$ gives $R_n\ge\frac{e^{-2}}8d\sqrt n$) and
    [LS, Theorem 24.2] (unit ball, $d\le2n$: some $\theta$ with $\|\theta\|^2=d^2/(48n)$ gives
@@ -461,15 +705,19 @@ OFUL bound applies to them.
 
 ## Layer 10: Adversarial linear bandits
 
-Losses $y_t\in E$ are chosen obliviously; the learner observes $\langle A_t,y_t\rangle$.
-
-1. **Exp3 with exploration.** For a finite spanning action set with
-   $\sup_a|\langle a,y_t\rangle|\le1$, define [LS, Algorithm 15] and prove [LS, Theorem 27.1]:
-   $R_n\le2\sqrt{(2g(\pi)+d)\,n\log k}$ for every exploration design $\pi$, hence
-   $R_n\le2\sqrt{3dn\log k}$ with the Kiefer–Wolfowitz design of Layer 8.6.
-2. **Mirror descent with bandit feedback.** Prove [LS, Theorem 28.10] for the scheme of
-   [LS, Algorithm 16] with unbiased estimates, and [LS, Theorem 28.11] for the unit ball:
-   with $\|y_t\|\le1$, $r=1-2\eta d$ and $\eta=\sqrt{\log(n)/(3dn)}$, $R_n\le2\sqrt{3nd\log n}$.
+Losses $y_t\in E$ are chosen by an adaptive adversary: $y_t$ is a measurable function of the
+history before round $t$ and of the observation of round $t$, and the learner observes
+$\langle A_t,y_t\rangle$; oblivious losses are the deterministic case. The regret is the
+pseudo-regret $R_n=\max_{u\in\mathcal A}\mathbb E\big[\sum_{t<n}\langle A_t-u,y_t\rangle\big]$.
+
+1. **Exp3 with exploration.** For a finite spanning action set, given by a feature map on a finite
+   type of arms, with $\sup_a|\langle a,y_t\rangle|\le1$, define [LS, Algorithm 15] and prove
+   [LS, Theorem 27.1]: $R_n\le2\sqrt{(2g(\pi)+d)\,n\log k}$ for every exploration design $\pi$,
+   hence $R_n\le2\sqrt{3dn\log k}$ with the Kiefer–Wolfowitz design of Layer 8.6.
+2. **Mirror descent with bandit feedback.** Deduce [LS, Theorem 28.10] for the scheme of
+   [LS, Algorithm 16] with unbiased estimates from Layer 6.5, and prove [LS, Theorem 28.11] for the
+   unit ball: with $\|y_t\|\le1$, $r=1-2\eta d$ and $\eta=\sqrt{\log(n)/(3dn)}$,
+   $R_n\le2\sqrt{3nd\log n}$.
    The exploration direction $U_t$ is uniform on $\{\pm e_1,\dots,\pm e_d\}$ for an orthonormal
    basis $(e_i)$ of $E$ (the box of [LS, Algorithm 17] omits the signs).
 
@@ -480,12 +728,16 @@ algorithm with its run lemma (the conditional law of its action given the histor
 regret theorems apply to all runs. Check in particular:
 
 * Index policies pull every arm once before comparing finite indices; the asymptotic constants of
-  Layers 2.2, 3 and 5 coincide with the Lai–Robbins constants of Layer 4.4 for Gaussian and
-  Bernoulli arms.
-* The minimax lower bounds of Layers 4.3, 4.5 and 9.4 match the upper bounds of Layers 2.3, 7.2 and
+  Layers 3 and 5 coincide with the Lai–Robbins constants of Layer 4.4 for every exponential
+  family, in particular for Gaussian and Bernoulli arms, where `ucbF` and `klucb` are the instances
+  of KL-UCB.
+* The minimax lower bounds of Layers 4.3, 4.5 and 9.4 match the upper bounds of Layers 2.3, 7.3 and
   9.2 up to the logarithmic and constant factors stated.
-* Exponential weights from Layer 6.4, Exp3 and Exp4 agree on the instances where their definitions
-  coincide.
+* Exp3, Exp3-IX and Exp4 are instances of Exp4-IX (Layer 7.2), whose expert weights are the
+  exponential weights of Layer 6.4; their bounds hold against oblivious tables, adaptive
+  adversaries and stochastic bandits alike.
+* The constant-rate FTRL and mirror descent bounds of Layer 6.3 are the constant cases of the
+  time-varying ones.
 * The Kiefer–Wolfowitz theorem applies to the finite action sets of Layers 9.3 and 10.1, including
   sets that do not span $E$.
 
@@ -499,14 +751,30 @@ Chapters 4–22, 24, 26–28 and 36, is the main source; the layers cite its num
 
 Original sources: P. Auer, N. Cesa-Bianchi, Y. Freund and R. Schapire, *The nonstochastic
 multiarmed bandit problem* (SIAM J. Comput., 2002) for Exp3 and Exp4; J.-Y. Audibert and S. Bubeck,
-*Minimax policies for adversarial and stochastic bandits* (COLT 2009) for MOSS; A. Garivier and
-O. Cappé, *The KL-UCB algorithm for bounded stochastic bandits and beyond* (COLT 2011);
+*Minimax policies for adversarial and stochastic bandits* (COLT 2009) for MOSS;
 T. L. Lai and H. Robbins, *Asymptotically efficient adaptive allocation rules* (Adv. Appl. Math.,
-1985) and A. N. Burnetas and M. N. Katehakis, *Optimal adaptive policies for sequential allocation
-problems* (Adv. Appl. Math., 1996) for Layer 4.4; G. Neu, *Explore no more* (NeurIPS 2015) for
-Exp3-IX; Y. Abbasi-Yadkori, D. Pál and Cs. Szepesvári, *Improved algorithms for linear stochastic
-bandits* (NeurIPS 2011) for Layers 8.4–9.2; J. Kiefer and J. Wolfowitz, *The equivalence of two
-extremum problems* (Canad. J. Math., 1960).
+1985) for Layer 4.4; J. Kiefer and J. Wolfowitz, *The equivalence of two extremum problems*
+(Canad. J. Math., 1960). The layers cite by key:
+
+- [AYPS11] Y. Abbasi-Yadkori, D. Pál and Cs. Szepesvári, *Improved algorithms for linear stochastic
+  bandits*, NeurIPS 2011 (Layers 8.4–9.2).
+- [BCB12] S. Bubeck and N. Cesa-Bianchi, *Regret analysis of stochastic and nonstochastic
+  multi-armed bandit problems*, Foundations and Trends in Machine Learning 5(1), 2012.
+- [BK96] A. N. Burnetas and M. N. Katehakis, *Optimal adaptive policies for sequential allocation
+  problems*, Adv. Appl. Math. 17 (1996).
+- [CGMMS13] O. Cappé, A. Garivier, O.-A. Maillard, R. Munos and G. Stoltz, *Kullback–Leibler upper
+  confidence bounds for optimal sequential allocation*, Ann. Statist. 41(3), 2013.
+- [GC11] A. Garivier and O. Cappé, *The KL-UCB algorithm for bounded stochastic bandits and
+  beyond*, COLT 2011.
+- [KKM13] N. Korda, E. Kaufmann and R. Munos, *Thompson sampling for 1-dimensional exponential
+  family bandits*, NeurIPS 2013.
+- [Neu15] G. Neu, *Explore no more: improved high-probability regret bounds for non-stochastic
+  bandits*, NeurIPS 2015.
+- [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*,
+  arXiv:1912.13213v10, 2026 (earlier versions are titled *A modern introduction to online
+  learning*).
+- [Zin03] M. Zinkevich, *Online convex programming and generalized infinitesimal gradient ascent*,
+  ICML 2003.
 
 [ls]: https://tor-lattimore.com/downloads/book/book.pdf
 [kw]: https://github.com/RemyDegenne/colt-2026-83/blob/3f6c0f296a3b7e4aa8fe333225505f5b2f61f9e0/Maiti2026Power/MXJ2026/OptimalDesign.lean
@@ -524,6 +792,7 @@ extremum problems* (Canad. J. Math., 1960).
 [lml-etc]: https://github.com/LeanMachineLearning/LML/blob/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/Online/Bandit/Algorithms/Regret/ETC.lean
 [lml-ts]: https://github.com/LeanMachineLearning/LML/blob/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
 [lml-div]: https://github.com/LeanMachineLearning/LML/blob/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
+[lml-means]: https://github.com/LeanMachineLearning/LML/blob/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/SequentialLearning/Means.lean
 [lml-chain]: https://github.com/LeanMachineLearning/LML/blob/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean
 [lml-breg]: https://github.com/LeanMachineLearning/LML/blob/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/Basic.lean
 [lml-subgrad]: https://github.com/LeanMachineLearning/LML/tree/53be244591a865c51ea10fa09403189ee060f116/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient
@@ -536,3 +805,4 @@ extremum problems* (Canad. J. Math., 1960).
 [tc-strong]: https://github.com/TauCetiProject/TauCeti/blob/cebc9b6046b14d2bd8d1c1088707109cdbac3a77/TauCeti/Analysis/Convex/Strong.lean
 [tc-frame]: https://github.com/TauCetiProject/TauCeti/blob/cebc9b6046b14d2bd8d1c1088707109cdbac3a77/TauCeti/Analysis/InnerProductSpace/Frame.lean
 [tc-affine]: https://github.com/TauCetiProject/TauCeti/blob/cebc9b6046b14d2bd8d1c1088707109cdbac3a77/TauCeti/Analysis/Convex/AffineNormalization.lean
+[tc-mp]: https://github.com/TauCetiProject/TauCeti/blob/cebc9b6046b14d2bd8d1c1088707109cdbac3a77/TauCeti/Analysis/InnerProductSpace/MoorePenrose.lean
diff --git a/LMLRoadmaps/Bandits/Suggested.lean b/LMLRoadmaps/Bandits/Suggested.lean
index 96ac42d..5aba8d6 100644
--- a/LMLRoadmaps/Bandits/Suggested.lean
+++ b/LMLRoadmaps/Bandits/Suggested.lean
@@ -1,8 +1,13 @@
+import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
 import Mathlib.Analysis.InnerProductSpace.Positive
+import Mathlib.Geometry.Convex.ConvexSpace.Defs
 import Mathlib.InformationTheory.KullbackLeibler.Basic
+import Mathlib.MeasureTheory.Measure.Tilted
 import Mathlib.Probability.Distributions.Bernoulli
 import Mathlib.Probability.Distributions.Gaussian.Real
 import Mathlib.Probability.Martingale.Basic
+import Mathlib.Probability.Moments.Basic
+import Mathlib.Probability.Moments.IntegrableExpMul
 import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic
 import LeanMachineLearning.ForMathlib.MeasureTheory.Order.MeasurableArg
 import LeanMachineLearning.Online.Bandit.Algorithms.Regret.UCB
@@ -11,8 +16,10 @@ import LeanMachineLearning.SequentialLearning.Deterministic
 import LeanMachineLearning.SequentialLearning.EvaluationEnv
 import LeanMachineLearning.SequentialLearning.FiniteActions
 import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
+import LeanMachineLearning.SequentialLearning.Means
 import LeanMachineLearning.SequentialLearning.StationaryEnv
 import LeanMachineLearning.SequentialLearning.SumRewards
+import TauCeti.Analysis.InnerProductSpace.MoorePenrose
 
 /-!
 # Bandit algorithms and their regret: suggested target signatures
@@ -25,7 +32,9 @@ admitted definitions: constructing them, with their run lemmas, is a target, and
 and the README specify them.
 
 The names of the LML framework (`stationaryEnv`, `onlineEvalEnv`, `detAlgorithm`, ...) are those
-of the LML version pinned by LMLExplore.
+of the LML version pinned by LMLExplore. Exponential families are written here through their
+natural parameters with Mathlib's `Measure.tilted` and `cgf`; the mean parametrization and the
+rate function are the Identification roadmap's (Layer 1.2).
 -/
 
 noncomputable section
@@ -99,6 +108,36 @@ def indexAlgorithm {𝓞 𝓨 : Type*} [MeasurableSpace 𝓞] [MeasurableSpace 
 def advRegret (x : ℕ → α → ℝ) (A : ℕ → Ω → α) (P : Measure Ω) (n : ℕ) : ℝ :=
   (⨆ a, ∑ t ∈ range n, x t a) - P[fun ω ↦ ∑ t ∈ range n, x t (A t ω)]
 
+/-- The pseudo-regret of a run against an adaptive adversary `env` (README Conventions and
+Layer 0.5): `max_a E[∑_{t < n} (m_t(a) - Y t)]`, with `m_t(a) = env.means O A Y a t` the mean reward
+of arm `a` at round `t` given the past. -/
+def pseudoRegret {𝓞 : Type*} [MeasurableSpace 𝓞] (env : Environment 𝓞 α ℝ) (O : ℕ → Ω → 𝓞)
+    (A : ℕ → Ω → α) (Y : ℕ → Ω → ℝ) (P : Measure Ω) (n : ℕ) : ℝ :=
+  ⨆ a, P[fun ω ↦ ∑ t ∈ range n, (env.means O A Y a t ω - Y t ω)]
+
+/-- The random regret of a run against an adaptive adversary `env`:
+`max_a ∑_{t < n} (m_t(a) - Y t)`. -/
+def randomRegret {𝓞 : Type*} [MeasurableSpace 𝓞] (env : Environment 𝓞 α ℝ) (O : ℕ → Ω → 𝓞)
+    (A : ℕ → Ω → α) (Y : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
+  ⨆ a, ∑ t ∈ range n, (env.means O A Y a t ω - Y t ω)
+
+/-- Against an oblivious reward table, the pseudo-regret is the adversarial regret `R_n(x)`. -/
+theorem pseudoRegret_onlineEvalEnv (x : ℕ → α → ℝ) {alg : Algorithm Unit α ℝ}
+    {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} {Y : ℕ → Ω → ℝ}
+    (h : IsAlgEnvSeq O A Y alg (onlineEvalEnv x fun t ↦ measurable_of_countable (x t)) P)
+    (n : ℕ) :
+    pseudoRegret (onlineEvalEnv x fun t ↦ measurable_of_countable (x t)) O A Y P n =
+      advRegret x A P n :=
+  sorry
+
+/-- Against a stochastic bandit, the pseudo-regret is the expected stochastic regret. -/
+theorem pseudoRegret_stationaryEnv {ν : Kernel α ℝ} [IsMarkovKernel ν]
+    (hν : ∀ a, Integrable id (ν a)) {alg : Algorithm Unit α ℝ}
+    {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} {Y : ℕ → Ω → ℝ}
+    (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) (n : ℕ) :
+    pseudoRegret (stationaryEnv ν) O A Y P n = P[Bandits.regret ν A n] :=
+  sorry
+
 /-! ## Layer 1: concentration and maximal inequalities -/
 
 /-- Ville's inequality for a nonnegative supermartingale. -/
@@ -132,7 +171,8 @@ def ucbFIndex (σ2 : ℝ≥0) (n : ℕ) (h : Hist Unit α ℝ n) (a : α) : ERea
     ((empMean' n h a +
       √(2 * σ2 * log (1 + (n + 1) * log (n + 1) ^ 2) / pullCount' n h a) : ℝ) : EReal)
 
-/-- Asymptotically optimal UCB [LS, Algorithm 6]. -/
+/-- Asymptotically optimal UCB [LS, Algorithm 6]: KL-UCB for the Gaussian family of variance
+`σ2` (`klucbFam_gaussianReal`). -/
 def ucbF (σ2 : ℝ≥0) : Algorithm Unit α ℝ :=
   indexAlgorithm (fun n x ↦ ucbFIndex σ2 n x.1) (fun n ↦ sorry)
 
@@ -159,17 +199,78 @@ theorem moss_regret_le (n : ℕ) (h : IsAlgEnvSeq O A R (moss σ2 n) (stationary
     P[Bandits.regret ν A n] ≤ 39 * √(σ2 * Fintype.card α * n) + ∑ a, Bandits.gap ν a :=
   sorry
 
-/-! ## Layer 3: KL-UCB -/
+/-! ## Layer 3: KL-UCB for exponential families -/
+
+/-- The KL-UCB upper confidence level `U_ρ(x, c)` of the natural exponential family of `ρ`
+(README Layer 3.1), written through the natural parameters with `ψ = cgf id ρ`: the supremum of
+`x` and of the means `ψ'(θ) ≥ x` of the members `ρ.tilted (θ * ·)` whose Cramér–Chernoff rate
+function at `x`, `sup_{θ'} ((θ' - θ) x - ψ(θ') + ψ(θ))`, is at most `c`. -/
+def expFamilyUpper (ρ : Measure ℝ) (x : ℝ) (c : ℝ≥0∞) : EReal :=
+  sSup (insert (x : EReal) ((fun θ ↦ ((deriv (cgf id ρ) θ : ℝ) : EReal)) ''
+    {θ | θ ∈ interior (integrableExpSet id ρ) ∧ x ≤ deriv (cgf id ρ) θ ∧
+      (⨆ θ' ∈ integrableExpSet id ρ,
+        ENNReal.ofReal ((θ' - θ) * x - cgf id ρ θ' + cgf id ρ θ)) ≤ c}))
+
+/-- The Gaussian level: `U(x, c) = x + √(2 σ² c)`. -/
+theorem expFamilyUpper_gaussianReal {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) (x : ℝ) (c : ℝ≥0) :
+    expFamilyUpper (gaussianReal 0 σ2) x c = ((x + √(2 * σ2 * c) : ℝ) : EReal) :=
+  sorry
+
+/-- The index of KL-UCB for the families `ρ a` [LS, Algorithm 8; GC11, Section 4] at Lean
+round `n`. -/
+def klucbFamIndex (ρ : α → Measure ℝ) (n : ℕ) (h : Hist Unit α ℝ n) (a : α) : EReal :=
+  if pullCount' n h a = 0 then ⊤ else
+    expFamilyUpper (ρ a) (empMean' n h a)
+      (ENNReal.ofReal (log (1 + (n + 1) * log (n + 1) ^ 2) / pullCount' n h a))
+
+/-- KL-UCB for the natural exponential families `ρ a` (README Layer 3.3). -/
+def klucbFam (ρ : α → Measure ℝ) : Algorithm Unit α ℝ :=
+  indexAlgorithm (fun n x ↦ klucbFamIndex ρ n x.1) (fun n ↦ sorry)
+
+/-- Asymptotically optimal UCB is KL-UCB for the Gaussian family of variance `σ2`. -/
+theorem klucbFam_gaussianReal {σ2 : ℝ≥0} (hσ2 : σ2 ≠ 0) :
+    klucbFam (fun _ : α ↦ gaussianReal 0 σ2) = ucbF σ2 :=
+  sorry
+
+/-- The asymptotic regret of KL-UCB for arms dominated by members of their families
+(README Layer 3.4): arm `a` has its exponential moments bounded by those of the member of natural
+parameter `θ a`, and `θ' a` is the natural parameter of the largest mean in the family of `a`. -/
+theorem klucbFam_regret_eventually_le (ρ : α → Measure ℝ) [∀ a, IsProbabilityMeasure (ρ a)]
+    {ν : Kernel α ℝ} [IsMarkovKernel ν] {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} {R : ℕ → Ω → ℝ}
+    (h : IsAlgEnvSeq O A R (klucbFam ρ) (stationaryEnv ν) P)
+    (θ : α → ℝ) (hθ : ∀ a, θ a ∈ interior (integrableExpSet id (ρ a)))
+    (hdom : ∀ a, ∀ t ∈ integrableExpSet id ((ρ a).tilted fun x ↦ θ a * x),
+      t ∈ integrableExpSet id (ν a) ∧ mgf id (ν a) t ≤ mgf id ((ρ a).tilted fun x ↦ θ a * x) t)
+    (θ' : α → ℝ) (hθ' : ∀ a, θ' a ∈ interior (integrableExpSet id (ρ a)) ∧
+      deriv (cgf id (ρ a)) (θ' a) = ⨆ b, (ν b)[id])
+    {c : ℝ} (hc : ∑ a ∈ univ.filter (fun a ↦ 0 < Bandits.gap ν a),
+      Bandits.gap ν a / (klDiv ((ρ a).tilted fun x ↦ θ a * x)
+        ((ρ a).tilted fun x ↦ θ' a * x)).toReal < c) :
+    ∀ᶠ n : ℕ in atTop, P[Bandits.regret ν A n] ≤ c * log n :=
+  sorry
 
-/-- The KL-UCB index [LS, Algorithm 8] at Lean round `n`. -/
+section KLUCB
+
+variable {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} {R : ℕ → Ω → ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν]
+
+/-- The KL-UCB index for rewards in `[0, 1]` [LS, Algorithm 8] at Lean round `n`. -/
 def klucbIndex (n : ℕ) (h : Hist Unit α ℝ n) (a : α) : EReal :=
   if pullCount' n h a = 0 then ⊤ else
     ((klUpper (empMean' n h a)
       (ENNReal.ofReal (log (1 + (n + 1) * log (n + 1) ^ 2) / pullCount' n h a)) : ℝ) : EReal)
 
-/-- KL-UCB [LS, Algorithm 8]. -/
+/-- At empirical means in `[0, 1]`, the KL-UCB index of the Bernoulli family is the index of
+[LS, Algorithm 8]. -/
+theorem klucbFamIndex_bernoulli {n : ℕ} {h : Hist Unit α ℝ n} {a : α}
+    (hmean : empMean' n h a ∈ Set.Icc 0 1) :
+    klucbFamIndex (fun _ : α ↦ bernoulliMeasure (1 : ℝ) 0 ⟨2⁻¹, by norm_num, by norm_num⟩) n h a =
+      klucbIndex n h a :=
+  sorry
+
+/-- KL-UCB for rewards in `[0, 1]` [LS, Algorithm 8]: KL-UCB for the Bernoulli family on every
+arm (README Layer 3.3). -/
 def klucb : Algorithm Unit α ℝ :=
-  indexAlgorithm (fun n x ↦ klucbIndex n x.1) (fun n ↦ sorry)
+  klucbFam fun _ ↦ bernoulliMeasure (1 : ℝ) 0 ⟨2⁻¹, by norm_num, by norm_num⟩
 
 /-- The asymptotic part of [LS, Theorem 10.6], for rewards in `[0, 1]`. -/
 theorem klucb_regret_eventually_le (h : IsAlgEnvSeq O A R klucb (stationaryEnv ν) P)
@@ -179,6 +280,8 @@ theorem klucb_regret_eventually_le (h : IsAlgEnvSeq O A R klucb (stationaryEnv 
     ∀ᶠ n : ℕ in atTop, P[Bandits.regret ν A n] ≤ c * log n :=
   sorry
 
+end KLUCB
+
 end UCB
 
 /-! ## Layer 4: lower bounds for finitely many arms -/
@@ -216,6 +319,17 @@ theorem exists_sqrt_le_integral_regret_gaussianBandit (alg : Algorithm Unit α 
 def dInf (M : Set (Measure ℝ)) (Pa : Measure ℝ) (m : ℝ) : ℝ≥0∞ :=
   ⨅ Q ∈ {Q ∈ M | m < Q[id]}, klDiv Pa Q
 
+/-- `d_inf` for a natural exponential family [BK96]: for members of natural parameters `θ ≤ θ'`,
+the infimum over the members with mean above the mean `ψ'(θ')` is the divergence from the member
+of parameter `θ` to that of parameter `θ'`. -/
+theorem dInf_range_tilted (ρ : Measure ℝ) [IsProbabilityMeasure ρ] (hρ : ∀ x, ρ ≠ Measure.dirac x)
+    {θ θ' : ℝ} (hθ : θ ∈ interior (integrableExpSet id ρ))
+    (hθ' : θ' ∈ interior (integrableExpSet id ρ)) (hle : θ ≤ θ') :
+    dInf (Set.range fun η : interior (integrableExpSet id ρ) ↦ ρ.tilted fun x ↦ η * x)
+        (ρ.tilted fun x ↦ θ * x) (deriv (cgf id ρ) θ') =
+      klDiv (ρ.tilted fun x ↦ θ * x) (ρ.tilted fun x ↦ θ' * x) :=
+  sorry
+
 /-- An algorithm is consistent over Gaussian bandits with variance `σ2` if its regret is
 `o(n ^ p)` for every `p > 0` [LS, Definition 16.1]. -/
 def IsConsistentGaussian (alg : Algorithm Unit α ℝ) (σ2 : ℝ≥0) : Prop :=
@@ -233,6 +347,20 @@ theorem lai_robbins_gaussian {alg : Algorithm Unit α ℝ} {σ2 : ℝ≥0}
       ∂(trajMeasure alg (stationaryEnv (gaussianBandit μ σ2))) :=
   sorry
 
+/-! ## Layer 5: Thompson sampling -/
+
+/-- The Jeffreys prior `√ψ''(θ) dθ` of the natural exponential family of `ρ`, on the interior of
+its natural-parameter set [KKM13, Section 2]. -/
+def jeffreysPrior (ρ : Measure ℝ) : Measure ℝ :=
+  (volume.restrict (interior (integrableExpSet id ρ))).withDensity
+    fun θ ↦ ENNReal.ofReal √(iteratedDeriv 2 (cgf id ρ) θ)
+
+/-- Thompson sampling for the natural exponential families `ρ a` with priors `prior a` on the
+natural parameters (README Layer 5.1): a follow-the-perturbed-leader policy that samples the mean
+of a natural parameter drawn from the posterior of each pulled arm, `+∞` for unpulled arms. -/
+def expFamilyTS (ρ prior : α → Measure ℝ) : Algorithm Unit α ℝ :=
+  sorry
+
 /-! ## Layer 6: online linear optimization -/
 
 section OnlineLinear
@@ -252,21 +380,47 @@ theorem ftrl_regret_le {F : E → ℝ} {K : Set E} (hK : Convex ℝ K) {η : ℝ
         (∑ t ∈ range n, bregDiv F (a (t + 1)) (a t) (F' t)) / η :=
   sorry
 
+/-- The regret bound of follow-the-regularized-leader with regularizers `ψ t` nondecreasing in `t`
+on `K` (README Layer 6.3); each play `a t ∈ K` minimizes `b ↦ ∑_{s<t} y s b + ψ t b` over `K`.
+With `ψ t = F / η t` this is the anytime form of `ftrl_regret_le`. -/
+theorem ftrl_regret_le_of_monotone {ψ : ℕ → E → ℝ} {K : Set E} (hK : Convex ℝ K)
+    (hψ : ∀ t, ∀ b ∈ K, ψ t b ≤ ψ (t + 1) b)
+    (y : ℕ → E →L[ℝ] ℝ) (a : ℕ → E) {n : ℕ} (ha_mem : ∀ t ≤ n, a t ∈ K)
+    (ha : ∀ t ≤ n, IsMinOn (fun b ↦ ∑ s ∈ range t, y s b + ψ t b) K (a t))
+    (ψ' : ℕ → E →L[ℝ] ℝ) (hψ' : ∀ t < n, HasFDerivWithinAt (ψ t) (ψ' t) K (a t)) {u : E}
+    (hu : u ∈ K) :
+    ∑ t ∈ range n, y t (a t - u) ≤
+      ψ n u - ψ 0 (a 0) +
+        ∑ t ∈ range n, (y t (a t - a (t + 1)) - bregDiv (ψ t) (a (t + 1)) (a t) (ψ' t)) :=
+  sorry
+
 end OnlineLinear
 
 /-! ## Layer 7: adversarial bandits with finitely many arms -/
 
-/-- Exp3 with learning rate `η` [LS, Algorithm 9]: a weight-based policy with the exponential
-weights of the loss-based importance-weighted reward estimates. -/
-def exp3 (η : ℝ) : Algorithm Unit α ℝ := sorry
+/-- Exp4-IX [Neu15] with the advice map `adv` from observations to the advice of the experts `β`,
+learning rates `η` and implicit-exploration parameters `γ` (README Layer 7.2): exponential
+weights on the experts of their estimated losses, and the arm drawn from the mixture of their
+advice. -/
+def exp4IX {𝓞 β : Type*} [MeasurableSpace 𝓞] [Fintype β] (adv : 𝓞 → β → α → ℝ)
+    (hadv : Measurable adv) (η γ : ℕ → ℝ) : Algorithm 𝓞 α ℝ :=
+  sorry
 
-/-- The regret of Exp3 for an arbitrary learning rate; `η = √(2 log k / (n k))` gives
-[LS, Theorem 11.2]. -/
-theorem exp3_advRegret_le (x : ℕ → α → ℝ) (hx : ∀ t a, x t a ∈ Set.Icc 0 1) {η : ℝ} (hη : 0 < η)
-    {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} {R : ℕ → Ω → ℝ}
-    (h : IsAlgEnvSeq O A R (exp3 η) (onlineEvalEnv x fun t ↦ measurable_of_countable (x t)) P)
-    (n : ℕ) :
-    advRegret x A P n ≤ log (Fintype.card α) / η + η * n * Fintype.card α / 2 :=
+/-- Exp3 with learning rates `η` [LS, Algorithm 9]: Exp4-IX with the experts `α`, expert `b`
+advising the arm `b`, and no implicit exploration. -/
+def exp3 {𝓞 : Type*} [MeasurableSpace 𝓞] (η : ℕ → ℝ) : Algorithm 𝓞 α ℝ :=
+  exp4IX (fun _ b ↦ Pi.single b 1) measurable_const η 0
+
+/-- The pseudo-regret of Exp3 against an adaptive adversary with feedback in `[0, 1]`, for
+nonincreasing learning rates (README Layer 7.3); a constant `η = √(2 log k / (n k))` gives
+[LS, Theorem 11.2] and `η t = √(log k / (k (t + 1)))` gives [BCB12, Theorem 3.1]. -/
+theorem exp3_pseudoRegret_le {𝓞 : Type*} [MeasurableSpace 𝓞] {env : Environment 𝓞 α ℝ}
+    (henv : ∀ n x, ∀ᵐ y ∂(env.feedback n x), y ∈ Set.Icc (0 : ℝ) 1)
+    {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) (hη_anti : Antitone η)
+    {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → α} {Y : ℕ → Ω → ℝ}
+    (h : IsAlgEnvSeq O A Y (exp3 η) env P) (n : ℕ) :
+    pseudoRegret env O A Y P n ≤
+      log (Fintype.card α) / η (n - 1) + Fintype.card α / 2 * ∑ t ∈ range n, η t :=
   sorry
 
 /-! ## Layer 8: least squares, self-normalized bounds and optimal design -/
@@ -275,42 +429,54 @@ section Linear
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
-/-- The design operator `V_t(λ) = λ • id + ∑_{s < t} x s ⊗ x s`. -/
-def designOp (lam : ℝ) (x : ℕ → E) (t : ℕ) : E →L[ℝ] E :=
-  lam • ContinuousLinearMap.id ℝ E + ∑ s ∈ range t, (innerSL ℝ (x s)).smulRight (x s)
+/-- The design operator `V_t(V₀) = V₀ + ∑_{s < t} x s ⊗ x s`; `V_t(λ)` is
+`designOp (lam • ContinuousLinearMap.id ℝ E) x t`. -/
+def designOp (V₀ : E →L[ℝ] E) (x : ℕ → E) (t : ℕ) : E →L[ℝ] E :=
+  V₀ + ∑ s ∈ range t, (innerSL ℝ (x s)).smulRight (x s)
 
 /-- The elliptical potential lemma [LS, Lemma 19.4] for `V_0 = λ • id`. -/
 theorem sum_min_one_inner_inverse_designOp_le {lam : ℝ} (hlam : 0 < lam) (x : ℕ → E) {L : ℝ}
     (hx : ∀ t, ‖x t‖ ≤ L) (n : ℕ) :
-    ∑ t ∈ range n, min 1 ⟪x t, Ring.inverse (designOp lam x t) (x t)⟫_ℝ ≤
+    ∑ t ∈ range n, min 1
+        ⟪x t, Ring.inverse (designOp (lam • ContinuousLinearMap.id ℝ E) x t) (x t)⟫_ℝ ≤
       2 * Module.finrank ℝ E * log (1 + n * L ^ 2 / (Module.finrank ℝ E * lam)) :=
   sorry
 
-/-- The self-normalized bound for vector-valued martingales [LS, Theorem 20.4], with
-conditionally σ²-sub-Gaussian noise. -/
+/-- The self-normalized bound for vector-valued martingales [AYPS11, Theorem 1], with a positive
+definite regularizer `V₀` and conditionally σ²-sub-Gaussian noise; [LS, Theorem 20.4] is the case
+`V₀ = λ • id`. -/
 theorem measure_exists_inner_inverse_designOp_ge_le [StandardBorelSpace Ω]
     {𝓕 : Filtration ℕ mΩ} {x : ℕ → Ω → E} {η : ℕ → Ω → ℝ} {σ2 : ℝ≥0}
     (hx : ∀ t, StronglyMeasurable[𝓕 t] (x t)) (hη : ∀ t, StronglyMeasurable[𝓕 (t + 1)] (η t))
     (hsub : ∀ t, HasCondSubgaussianMGF (𝓕 t) (𝓕.le t) (η t) σ2 P)
-    {lam δ : ℝ} (hlam : 0 < lam) (hδ : δ ∈ Set.Ioo 0 1) :
+    {V₀ : E →L[ℝ] E} (hV₀ : V₀.IsPositive) (hV₀_unit : IsUnit V₀) {δ : ℝ} (hδ : δ ∈ Set.Ioo 0 1) :
     P {ω | ∃ t, 2 * σ2 * log (1 / δ) +
-        σ2 * log (LinearMap.det (designOp lam (fun s ↦ x s ω) t).toLinearMap /
-          lam ^ Module.finrank ℝ E) ≤
+        σ2 * log (LinearMap.det (designOp V₀ (fun s ↦ x s ω) t).toLinearMap /
+          LinearMap.det V₀.toLinearMap) ≤
       ⟪∑ s ∈ range t, η s ω • x s ω,
-        Ring.inverse (designOp lam (fun s ↦ x s ω) t) (∑ s ∈ range t, η s ω • x s ω)⟫_ℝ} ≤
+        Ring.inverse (designOp V₀ (fun s ↦ x s ω) t) (∑ s ∈ range t, η s ω • x s ω)⟫_ℝ} ≤
       ENNReal.ofReal δ :=
   sorry
 
-/-- The design operator `V(w) = ∑_a w a • a ⊗ a` of a finitely supported design. -/
-def designOperator (w : E →₀ ℝ) : E →L[ℝ] E :=
-  w.sum fun a c ↦ c • (innerSL ℝ a).smulRight a
+/-- The design operator `V(w) = ∑_a w a • a ⊗ a` of a finitely supported design `w` on `E`. -/
+def designOperator (w : Convexity.StdSimplex ℝ E) : E →L[ℝ] E :=
+  w.weights.sum fun a c ↦ c • (innerSL ℝ a).smulRight a
+
+/-- The design operator of the image of a design on finitely many arms by a feature map. -/
+theorem designOperator_map {ι : Type*} [Fintype ι] (φ : ι → E) (w : Convexity.StdSimplex ℝ ι) :
+    designOperator (w.map φ) = ∑ i, w.weights i • (innerSL ℝ (φ i)).smulRight (φ i) :=
+  sorry
 
-/-- The Kiefer–Wolfowitz theorem [LS, Theorem 21.1]: a G-optimal design with small support. -/
-theorem exists_design_inner_inverse_le_finrank {𝒜 : Set E} (h𝒜 : IsCompact 𝒜)
-    (hspan : Submodule.span ℝ 𝒜 = ⊤) :
-    ∃ w : E →₀ ℝ, (w.support : Set E) ⊆ 𝒜 ∧ (∀ a, 0 ≤ w a) ∧ (w.sum fun _ c ↦ c) = 1 ∧
-      w.support.card ≤ Module.finrank ℝ E * (Module.finrank ℝ E + 1) / 2 ∧
-      ∀ a ∈ 𝒜, ⟪a, Ring.inverse (designOperator w) a⟫_ℝ ≤ Module.finrank ℝ E :=
+/-- The Kiefer–Wolfowitz theorem on the span of a compact set [LS, Theorem 21.1, Exercises 21.3
+and 21.6]: a design with small support whose G-value, computed with the Moore–Penrose inverse, is
+the dimension of the span. -/
+theorem exists_design_inner_moorePenroseInverse_le_finrank {𝒜 : Set E} (h𝒜 : IsCompact 𝒜)
+    (h𝒜_ne : ∃ a ∈ 𝒜, a ≠ 0) :
+    ∃ w : Convexity.StdSimplex ℝ E, (w.weights.support : Set E) ⊆ 𝒜 ∧
+      w.weights.support.card ≤
+        Module.finrank ℝ (Submodule.span ℝ 𝒜) * (Module.finrank ℝ (Submodule.span ℝ 𝒜) + 1) / 2 ∧
+      ∀ a ∈ 𝒜, ⟪a, (designOperator w : E →ₗ[ℝ] E).moorePenroseInverse a⟫_ℝ ≤
+        Module.finrank ℝ (Submodule.span ℝ 𝒜) :=
   sorry
 
 /-! ## Layer 9: stochastic linear bandits -/