From 0ae23067cac95cf871f538538ce3a4847dd3d757 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 31 Oct 2026 00:12:55 +0100 Subject: [PATCH] Add the Identification roadmap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A roadmap for bandit identification (pure exploration): identification tasks with arbitrary models and multiple correct answers, natural exponential families, the change of measure at stopping times and the lower bounds, the pure exploration game, GLR stopping rules and their thresholds, Track-and-Stop and Sticky Track-and-Stop, game-based, Top Two and Frank–Wolfe sampling, elimination and LUCB algorithms, fixed-budget identification, and linear identification. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMTTvboLE9rrbLUFss1 --- LMLRoadmaps/Identification/README.md | 668 ++++++++++++++++++++++ LMLRoadmaps/Identification/Suggested.lean | 188 ++++++ LMLRoadmaps/Identification/metadata.toml | 1 + 3 files changed, 857 insertions(+) create mode 100644 LMLRoadmaps/Identification/README.md create mode 100644 LMLRoadmaps/Identification/Suggested.lean create mode 100644 LMLRoadmaps/Identification/metadata.toml diff --git a/LMLRoadmaps/Identification/README.md b/LMLRoadmaps/Identification/README.md new file mode 100644 index 0000000..93ff562 --- /dev/null +++ b/LMLRoadmaps/Identification/README.md @@ -0,0 +1,668 @@ +# Roadmap: Bandit identification + +Develop the theory of identification in stochastic bandits (pure exploration): an algorithm samples +arms adaptively, stops, and answers a question about the unknown bandit, such as which arm has the +largest mean. In the *fixed-confidence* setting the answer must be correct with probability at +least $1-\delta$ and the expected number of samples is minimized. In the *fixed-budget* setting +the number of samples is fixed and the probability of error is minimized. The headline results +are: +- the universal lower bound $\mathbb E[\tau]\ge T^*(\theta)\,\mathrm{kl}(\delta,1-\delta)$ and the + pure exploration game that defines $T^*$; +- $\delta$-correctness of generalized likelihood ratio stopping rules for every sampling rule; +- asymptotic optimality of Track-and-Stop and Sticky Track-and-Stop; +- non-asymptotic guarantees of game-based and Top Two sampling rules, and asymptotic optimality of + Frank–Wolfe sampling; +- the elimination algorithms with gap-dependent guarantees; +- successive rejects and sequential halving with the fixed-budget lower bounds, including the + non-existence of a complexity in fixed-budget best arm identification; +- the characteristic time and asymptotically optimal algorithms of linear identification. + +Build the surrounding library at the generality the research literature uses, so that papers in +the area can be written on top of it: +- identification tasks with arbitrary models, answer sets and multiple correct answers; +- natural exponential families; +- the change of measure at stopping times; +- transportation costs and their continuity (Berge's maximum theorem, Sion's minimax theorem); +- generalized likelihood ratio statistics and their time-uniform deviation inequalities; +- tracking lemmas, a generic sample-complexity reduction, AdaHedge; +- large deviations of empirical means under static allocations. + +`README.md` is the definitive specification; `Suggested.lean` records selected interfaces and is +not an exhaustive checklist. + +Suggested homes: `LMLExplore/Identification/` for identification material (namespace +`LMLExplore.Identification`), and the mathematical home of each general tool (for example +`LMLExplore/Probability/Distributions/ExponentialFamily/` for natural exponential families, +`LMLExplore/Probability/LargeDeviations/` for Cramér-type bounds, +`LMLExplore/Topology/Semicontinuous/` for Berge's maximum theorem, `LMLExplore/OnlineLearning/` for +AdaHedge). + +## Scope and dependencies + +This roadmap owns identification in stochastic bandits with a finite set of arms (pure +exploration): fixed-confidence and fixed-budget identification for arbitrary identification +tasks, with single or multiple correct answers, in unstructured models and in linear models. + +| Material | Owner and interface consumed here | +| --- | --- | +| Interaction protocol, runs, trajectory measure, stationary environments | LML `SequentialLearning/`: `Algorithm`, `Environment`, `IsAlgEnvSeq`, `trajMeasure`, `stationaryEnv` | +| Identification algorithms: sampling, stopping and output rules, stopping time, stopped history, law of the output, PAC property | LML `SequentialLearning/IdentificationAlg.lean` (`IdentAlg`, `IdentAlg.stoppingTime`, `IdentAlg.stoppedHist`, `IdentAlg.outputMeasure`, `IdentAlg.IsRun`, `IdentAlg.IsPAC`), `SequentialLearning/StoppedHistory.lean` (`sigmaHistory`, `stoppedHistMeasure`) | +| Pull counts, reward sums, empirical means | LML `SequentialLearning/FiniteActions.lean`, `SumRewards.lean` | +| KL divergence of histories at a fixed horizon | LML `SequentialLearning/DivergenceDecomposition.lean`; LMLExplore `Learning.IsAlgEnvSeq.klDiv_map_history_eq_sum_pullCount` | +| Binary relative entropy, Bretagnolle–Huber, Ville's inequality, mixtures of supermartingales, time-uniform sub-Gaussian bounds, Chernoff bounds in relative-entropy form | LMLExplore (Bandits roadmap, Layers 0.2, 1 and 4): `klBer`, `klBerReal`, `exp_neg_klDiv_div_two_le`, `MeasureTheory.Supermartingale.measure_exists_le_le`, `supermartingale_integral_of_integrable`, `supermartingale_exp_sum_mul_of_hasCondSubgaussianMGF`, `measureReal_sum_ge_le_exp_klBerReal` | +| Design operators, self-normalized bounds, G-optimal designs | Bandits roadmap, Layer 8 (`designOp`, the self-normalized bound, the Kiefer–Wolfowitz theorem) | +| Exponential weights, regret of online linear optimization | Bandits roadmap, Layer 6 | +| KL divergence, chain rule, data processing, exponential tilting, cumulant generating functions | Mathlib `InformationTheory/KullbackLeibler/`, `MeasureTheory/Measure/Tilted.lean`, `MeasureTheory/Measure/LogLikelihoodRatio.lean`, `Probability/Moments/` (`cgf`, `integrableExpSet`, `deriv_cgf`, `iteratedDeriv_two_cgf`) | +| Minimax theorems, continuity of suprema over compact sets | Mathlib `Topology/Sion.lean` (`Sion.minimax`, `Sion.exists_isSaddlePointOn`), Tau Ceti `Topology/Sion.lean`, Mathlib `Topology/Order/Compact.lean` (`IsCompact.continuous_sSup`, `IsCompact.continuous_sInf`) | + +Build missing material in this roadmap where it is listed as a target, and consume existing +implementations directly. The Bandits roadmap and this one do not overlap: regret minimization, +the fixed-horizon divergence decomposition and the binary relative entropy belong to the Bandits +roadmap. The change of measure at stopping times, exponential families and everything specific to +identification belong here. + +Outside this roadmap: +- best policy identification in Markov decision processes; +- combinatorial and semi-bandit identification beyond what the general tasks of Layer 1 express; +- dueling bandits, contextual and multi-fidelity identification; +- Bayesian (posterior-based) guarantees: Top Two algorithms are analyzed here with frequentist + guarantees only; +- nonparametric identification with $\mathrm K_{\inf}$ or $\mathrm{KL}_{\inf}$ (bounded or + heavy-tailed arms), including the bounded-arm Top Two results of [JDBdHK22]. + +## Conventions + +**Sources and numbering.** Statements cite the original papers by the keys of the References +section, with their theorem numbers, and [LS, Chapter 33] for the textbook account. Rounds are +numbered from 0, as in LML: after $n$ rounds the actions $A_0,\dots,A_{n-1}$ have been played, and +the stopping time $\tau$ is the number of rounds played. A paper's round $t$ is Lean round $t-1$. + +**Arms and observations.** A finite set of arms is a type `α` with `[Fintype α] [Nonempty α] +[DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α]`, and $K$ is `Fintype.card α`. Do +not specialize to `Fin K`. Observations live in a measurable space `𝓨`. The framework, the lower +bounds and the pure exploration game (Layers 0–3) are stated for general `𝓨`. Exponential-family +material and the algorithms built on empirical means use `𝓨 = ℝ`. The observation type of the +sampling rule is `Unit`, as for LML's `stationaryEnv`. + +**Models and tasks.** An identification task (Layer 1.1) has a type `Θ` of models with a Markov +kernel `ν θ : Kernel α 𝓨` for each model, a set `M : Set Θ` of admissible models, a type `ℐ` of +answers and a set-valued correct-answer function `correct : Θ → Set ℐ`. Single-answer tasks have +`correct θ = {answer θ}` on `M`. A model is not required to be a vector of means: means of +exponential families (Layer 1.2), parameters of linear models (Layer 9) and pairs (mean, variance) +are all models. + +**Divergences and allocations.** Divergences between arm laws are Mathlib's `klDiv`, valued in +`ℝ≥0∞`. Allocations (proportions of samples) are vectors `w : α → ℝ` with nonnegative entries +summing to `1`, the set $\Delta_K$, stated directly: Mathlib's set `stdSimplex` is deprecated, and +its replacement `Convexity.StdSimplex` is a type of finitely supported distributions, not a subset +of `α → ℝ` with its topology. Transportation costs, the game value and the characteristic time are +`ℝ≥0∞`-valued: +$$\mathrm{cost}_\theta(w,\lambda)=\sum_a w_a\,\mathrm{KL}(\nu_a(\theta),\nu_a(\lambda)),\qquad +D(\theta,w,\neg i)=\inf_{\lambda\in\neg i}\mathrm{cost}_\theta(w,\lambda),$$ +$$D(\theta,\neg i)=\sup_{w\in\Delta_K}D(\theta,w,\neg i),\qquad +D(\theta)=\max_{i\in i^*(\theta)}D(\theta,\neg i),\qquad T^*(\theta)=D(\theta)^{-1},$$ +with $\neg i=\{\lambda\in M: i\notin i^*(\lambda)\}$ the alternatives to $i$, written with +`ENNReal.ofReal (w a) * klDiv …`. Real-valued versions are corollaries for models at finite +divergence. The fixed-confidence quantities put the true model first, +$\mathrm{KL}(\nu_a(\theta),\nu_a(\lambda))$. The fixed-budget exponents of Layer 8 put the +alternative first; they are the same costs applied to the swapped pair, not new definitions. The +two orders agree for Gaussian arms with known variance and differ in general, which is why fixed +budget can be strictly easier than fixed confidence [KCG16, Theorem 14]. + +**Guarantees.** +- An identification algorithm is `IdentAlg Unit α 𝓨 ℐ`. +- It is *$\delta$-correct* on a task [DK19] if on every model $\theta\in M$, with probability at + least $1-\delta$, it stops and outputs a correct answer. +- It is *$\delta$-PAC* if moreover it stops almost surely on every model of $M$. +- Both properties are stated on the laws of the runs, which the algorithm and the environment + determine: the joint law of the stopped history and the output, built from LML's + `stoppedHistMeasure` and the output kernel, and the law `IdentAlg.outputMeasure`. +- The sample complexity is $\mathbb E_\theta[\tau]$, the `ℝ≥0∞`-valued lower integral of the + stopping time under `trajMeasure A.alg (stationaryEnv (ν θ))`. +- A fixed-budget algorithm with budget $T$ stops after exactly $T$ rounds; its probability of + error on $\theta$ is the `outputMeasure`-mass of the incorrect answers. + +**Families of algorithms and asymptotics.** Fixed-confidence algorithms are families +`A : ℝ → IdentAlg …` indexed by the confidence level. Fixed-budget algorithms are families indexed +by the budget. Asymptotic statements are eventual inequalities. For example +"$\limsup_{\delta\to0}\mathbb E[\tau_\delta]/\log(1/\delta)\le T^*$" is +`∀ c > T*, ∀ᶠ δ in 𝓝[>] 0, E[τ_δ] ≤ c * log (1/δ)`, and fixed-budget rates are stated with +`∀ᶠ T in atTop`. Never use `limsup`/`liminf` of real sequences as the primary form. + +**Theorem shapes.** Upper bounds quantify over runs: for every `IdentAlg.IsRun A env O X Y out P`, +a bound on an expectation or a probability under `P`. Lower bounds and correctness properties are +stated on the laws (`trajMeasure`, `stoppedHistMeasure`, `outputMeasure`) and transferred to every +run with LML's law-uniqueness lemmas. Where a paper states a universal constant, state the +explicit constant when the proof gives one. + +**Generality.** Each layer says where its statements generalize the papers. Do not reintroduce +special cases (`Fin K`, Bernoulli or Gaussian arms only, unit variance, a single correct answer) as +the primary statements; derive them as corollaries. + +**Namespaces.** Identification definitions live in `LMLExplore.Identification`, exponential +families in `LMLExplore` (or the namespace of the type they act on), and LML's definitions keep +their names (`Learning.IdentAlg`, `Learning.stationaryEnv`, …). + +## Existing formalizations + +The LMLPapers project of the same author (Apache-2.0, unpublished) contains formalizations of +[GK16], [DK19], [DKM19] and [D23] together with an identification library on top of LML's +`IdentAlg`: +- identification tasks, multiple-answer tasks and transportation costs; +- the change of measure at stopping times; +- GLRT stopping rules; +- C- and D-tracking, Track-and-Stop and Sticky Track-and-Stop; +- the pure-exploration game algorithm; +- successive elimination, median elimination, sequential halving and fixed-budget algorithms; +- one-parameter exponential families and large deviation principles. + +It states tasks on `Fin K` with means in exponential families. The roadmap asks for the general +forms above, and that development may be adapted to them. + +## Layers and dependencies + +| Layer | Content | Prerequisites | +| --- | --- | --- | +| 0 | Identification algorithms, correctness and sample complexity | LML `IdentAlg` | +| 1 | Identification tasks and natural exponential families | Layer 0 | +| 2 | Change of measure and lower bounds | Layers 0–1; Bandits roadmap Layer 4 | +| 3 | The pure exploration game | Layer 1 | +| 4 | Deviation inequalities and GLR stopping rules | Layers 1, 3; Bandits roadmap Layer 1 | +| 5 | Tracking and asymptotically optimal sampling rules | Layers 2–4 | +| 6 | Game-based, Top Two and Frank–Wolfe sampling rules | Layers 3–5; Bandits roadmap Layer 6 | +| 7 | Elimination and confidence-bound algorithms | Layers 0–2, 4 | +| 8 | Fixed-budget identification | Layers 0–3 | +| 9 | Linear identification | Layers 2–6; Bandits roadmap Layer 8 | + +## Layer 0: Identification algorithms, correctness and sample complexity + +1. **Constructions and canonical runs.** + - Construct an identification algorithm from per-length rules: a sampling rule, measurable + stopping predicates `stop n : Hist … n → Prop` and output kernels `output n`. + - Prove the characterizations of its stopping time (equal to $n$ iff the first $n$-round + history satisfying the rule is the $n$-round one; infinite iff no history does), measurability + of the stopping time and of the stopped history, and that the stopped history belongs to the + stopping rule iff the stopping time is finite. + - Construct the canonical run of every identification algorithm in every environment (the + trajectory measure times the output kernel at the stopped history), and transport runs along + measure-preserving maps. +2. **Correctness notions.** + - Define the joint law of the stopped history and the output, almost-sure stopping, $\delta$-PAC + and $\delta$-correct algorithms for a family of environments and a badness predicate, with + their task versions in Layer 1. + - Prove $\delta$-PAC $\Rightarrow$ $\delta$-correct $\Rightarrow$ LML's `IsPAC` at level $\delta$, + monotonicity in $\delta$ and in the badness predicate, restriction to subfamilies, and the + run forms of each property. +3. **Sample complexity.** + - Define $\mathbb E_{\mathrm{env}}[\tau]$ and prove it is the same along every run. + - For stationary environments on finite arms, prove Wald's identities at the stopping time: + $\mathbb E[\tau]=\sum_a\mathbb E[N_a(\tau)]$, and + $\mathbb E\big[\sum_{t<\tau}f(A_t)\big]=\sum_a\mathbb E[N_a(\tau)]f(a)$ for $f\ge0$ (LMLExplore's + `sum_lintegral_pullCount_mul` is the version for a measurable random time). + - Prove $\mathbb E\big[\sum_{t<\tau}Y_t\big]=\sum_a\mathbb E[N_a(\tau)]\,\mu_a$ for integrable + rewards when $\mathbb E[\tau]<\infty$. +4. **Fixed-budget algorithms.** + - Define fixed-budget algorithms (stop after exactly $T$ rounds) and the fixed-budget constructor + from a sampling rule and an output kernel on $T$-round histories. + - Prove that their stopped history is the $T$-round history, that they stop almost surely, and + that their output law is the output kernel composed with the law of the $T$-round history. + - Define static (fixed-design) sampling rules, which play a fixed sequence of arms. + +## Layer 1: Identification tasks and natural exponential families + +1. **Tasks.** + - Define identification tasks (Conventions): alternatives $\neg i$, answer sets + $\{\theta\in M: i\in i^*(\theta)\}$, single-answer tasks, and the bandit environment + `stationaryEnv (ν θ)` of a model. + - Define $\delta$-correct and $\delta$-PAC algorithms for a task. + - Define the classical tasks on vectors of means `α → ℝ`: + - best arm identification on models with a unique best arm; + - top-$m$ identification (the set of the $m$ largest means, on models where it is unique); + - $\varepsilon$-best arm identification (additive: correct answers are the arms within + $\varepsilon$ of the best); + - thresholding (the set of arms with mean above $\gamma$, on models with no mean equal to + $\gamma$); + - the minimum-threshold task (is the smallest mean below $\gamma$?); + - the multiple-answer task *Any Low Arm* [DK19, Example 1] (an arm with mean below $\gamma$, + or "none"); + - half-space identification (the sign of $\langle u,\mu\rangle$). + - For best arm identification, prove that the alternatives to the best arm $a^*$ have closure + $\{\lambda:\exists b\ne a^*,\ \lambda_b\ge\max_c\lambda_c\}$ within the models whose means lie + in the families' mean sets. Prove that the transportation infimum over $\neg a^*$ equals the + infimum over this closed set when the divergences are continuous. +2. **Natural exponential families.** + - For a probability measure $\rho$ on $\mathbb R$ with nonempty open natural-parameter set + $\Theta_\rho=\operatorname{interior}(\texttt{integrableExpSet id }\rho)$, define the family of + tilts $\rho_\eta=$ `ρ.tilted (η * ·)`, $\eta\in\Theta_\rho$. + - Define the log-partition function $\psi=$ `cgf id ρ`, the mean map $\psi'$ (`deriv_cgf`), and + its strict monotonicity when $\rho$ is not a Dirac mass (variance `iteratedDeriv_two_cgf` > 0). + - Define the open interval of means and the mean parametrization $\mu\mapsto\rho_{\eta(\mu)}$. + - Prove the closed form + $\mathrm{KL}(\rho_{\eta(\mu)},\rho_{\eta(\mu')})=d(\mu,\mu') + =\psi(\eta')-\psi(\eta)-\mu(\eta'-\eta)$ (from `llr_tilted_left`), and that $d$ is + nonnegative, zero exactly on the diagonal, continuous on (means)$^2$, strictly convex in its + first argument, and monotone in each argument on each side of the other (it is not convex in + its second argument in general: the exponential family is a counterexample). + - Prove the Cramér–Chernoff bound $\rho_{\eta(\mu)}^{\otimes n}(\hat\mu_n\ge x)\le + \exp(-n\,d(x,\mu))$ for $x\ge\mu$ (and the lower tail), generalizing the Bandits roadmap's + Layer 1.4 bound. + - Prove the sub-Gaussian comparison: $d(\mu,\mu')\ge(\mu-\mu')^2/(2\sigma^2)$ when the family has + variance at most $\sigma^2$ on the segment. + - Prove that the Gaussian family with variance $\sigma^2$ + ($d(\mu,\mu')=(\mu-\mu')^2/(2\sigma^2)$), the Bernoulli family ($d=$ `klBer`, by the Bandits + roadmap's `klDiv_bernoulliMeasure`), the Poisson family (Mathlib's `poissonMeasure`, pushed + forward to `ℝ`) and the exponential family (`expMeasure`) are natural exponential families in + this sense, with their divergences. + - Define the bandit of a mean vector, with arm laws in per-arm exponential families. Define the + generalized log-likelihood ratio extension of $d$ to empirical means at the boundary of the + mean interval (for Bernoulli arms, $\hat\mu\in\{0,1\}$), with its continuity. +3. **Gaussian arms with unknown variances.** Define the two-parameter Gaussian model + $\theta=(\mu_a,\sigma_a^2)_a$ and prove + $\mathrm{KL}(\mathcal N(\mu,\sigma^2),\mathcal N(\mu',\sigma'^2))= + \tfrac12\big(\log\tfrac{\sigma'^2}{\sigma^2}+\tfrac{\sigma^2+(\mu-\mu')^2}{\sigma'^2}-1\big)$. + +Generalization: arbitrary models and answer types, multiple correct answers and observations in any +measurable space, where [GK16, DK19] use vectors of means in one exponential family and finitely +many answers. + +## Layer 2: Change of measure and lower bounds + +1. **Divergence decomposition at a stopping time.** + - For two runs of the same identification algorithm in `stationaryEnv ν` and `stationaryEnv ν'` + on finite arms, with $\tau$ almost surely finite under the first run, prove + $\mathrm{KL}(\text{law of the stopped history under }\nu,\text{ under }\nu') + \le\sum_a\mathbb E_\nu[N_a(\tau)]\,\mathrm{KL}(\nu_a,\nu'_a)$, with equality when $\tau$ is also + almost surely finite under $\nu'$. + - Prove the same bound for the joint law of the stopped history and the output: the output + kernel is common (Mathlib's `klDiv_compProd_left`). + - The fixed-horizon case is LML's `IsAlgEnvSeq.klDiv_map_history`. +2. **Transportation lemma** [KCG16, Lemma 1]. + - Prove the data-processing inequality + $\mathrm{kl}(P(E),Q(E))\le\mathrm{KL}(P,Q)$ for measurable $E$, with `klBer`, from Mathlib's + `klDiv_map_le`. + - Deduce + $\sum_a\mathbb E_\nu[N_a(\tau)]\,\mathrm{KL}(\nu_a,\nu'_a)\ge + \mathrm{kl}(P_\nu(E),P_{\nu'}(E))$ for every event $E$ of the stopped history and the output, + by data processing from Layer 2.1 as in [GMS19]. No mutual absolute continuity is assumed: the + inequality holds in `ℝ≥0∞`. +3. **Fixed-confidence lower bounds.** + - For a single-answer task and a $\delta$-correct algorithm with $\delta\in(0,1/2)$, prove + $\mathbb E_\theta[\tau]\ge T^*(\theta)\,\mathrm{kl}(\delta,1-\delta)$ for every + $\theta\in M$ [GK16, Theorem 1]. + - Prove $\mathrm{kl}(\delta,1-\delta)\ge\log\frac1{2.4\delta}$ [KCG16], and the + Bretagnolle–Huber variant $\mathbb E_\theta[\tau]\ge T^*(\theta)\log\frac1{4\delta}$ + [LS, Theorem 33.5]. + - Prove the allocation form: the normalized expected counts + $\big(\mathbb E_\theta[N_a(\tau)]/\mathbb E_\theta[\tau]\big)_a$ satisfy + $\mathbb E_\theta[\tau]\,D(\theta,w,\neg i^*(\theta))\ge\mathrm{kl}(\delta,1-\delta)$. + - For multiple-answer tasks with finitely many answers, prove + $\liminf_{\delta\to0}\mathbb E_\theta[\tau_\delta]/\log(1/\delta)\ge T^*(\theta)$ for every + family of $\delta$-correct algorithms [DK19, Theorem 1, Proposition 18, Lemma 19], in the + eventual form of the Conventions. +4. **Fixed-budget lower bounds.** + - For two models $\theta,\lambda$ without a common correct answer and an algorithm with budget + $T$, prove + $P_\theta(\text{error})+P_\lambda(\text{error})\ge\tfrac12\exp\!\big(-\sum_a\mathbb + E_\theta[N_a(T)]\,\mathrm{KL}(\nu_a(\theta),\nu_a(\lambda))\big)$ (Bretagnolle–Huber). + - Prove its consequence: some model of every finite family has error at least + $\tfrac14\exp(-T\max_a\mathrm{KL})$. + - The minimax lower bounds of Layer 8.4 build on this. + +Generalization: arbitrary tasks and observation spaces, where [KCG16, GK16] treat best arm +identification in exponential families. + +## Layer 3: The pure exploration game + +1. **Transportation costs.** + - Define the quantities of the Conventions and the set $w^*(\theta,\neg i)$ of optimal + allocations. + - Prove that $w\mapsto D(\theta,w,\neg i)$ is concave and positively homogeneous on + $[0,\infty)^\alpha$ and monotone (antitone in the alternative set), so $w^*(\theta,\neg i)$ is + convex. + - Prove that the value is $0$ when $\theta\in\neg i$, and that $T^*(\theta)<\infty$ iff some + correct answer has alternatives at positive cost for some allocation. + - Prove measurability of $(\theta,w)\mapsto D(\theta,w,\neg i)$ for vectors of means with + continuous divergences (an infimum of continuous functions). +2. **Game and minimax forms.** + - Prove $D(\theta,\neg i)=\inf_{q}\max_a\mathbb E_{\lambda\sim q}[\mathrm{KL}(\nu_a(\theta), + \nu_a(\lambda))]$ over finitely supported distributions $q$ on $\neg i$ [DK19, Lemma 2; + DKM19, Section 2], from Mathlib's `Sion.minimax` on the simplex. + - Prove $T^*(\theta)^{-1}=\max_{i\in i^*(\theta)}D(\theta,\neg i)$, the characteristic-time + identity of multiple-answer tasks. +3. **Continuity** [DK19, Appendix F]. + - Prove Berge's maximum theorem for upper hemicontinuous compact-valued correspondences, in the + generality of [DK19, Theorems 22–23], from Mathlib's `IsCompact.continuous_sSup`/`continuous_sInf`. + - For vectors of means with continuous divergences, deduce: + - continuity of $(\theta,w)\mapsto D(\theta,w,\neg i)$ on positive allocations when + $\neg i$ is compact or under [DK19, Lemma 25]'s conditions; + - continuity of $\theta\mapsto D(\theta,\neg i)$ and of $D(\theta)$; + - upper hemicontinuity with compact convex values of $\theta\mapsto w^*(\theta,\neg i)$; + - upper hemicontinuity of the oracle answers $i_F(\theta)=\operatorname{argmax}_i + D(\theta,\neg i)$ and of $w^*(\theta)=\bigcup_{i\in i_F(\theta)}w^*(\theta,\neg i)$ + [DK19, Theorem 4, Lemmas 24–30]. + - Prove the convexity of $w^*(\theta,\neg i)$ and give a model where $w^*(\theta)$ is not + convex [DK19, Proposition 5]. +4. **Best arm identification in exponential families** [GK16, Section 2]. + - Prove that $D(\mu,w,\neg a^*)=\min_{b\ne a^*}\big(w_{a^*}d(\mu_{a^*},m)+w_bd(\mu_b,m)\big)$ + with $m$ the $w$-weighted mean of $\mu_{a^*}$ and $\mu_b$ [GK16, Lemma 3]. + - Prove that $w^*(\mu)$ is a singleton with positive entries equalizing the transportation + costs [GK16, Lemma 4]. Prove its characterization through the scalar equation of + [GK16, Theorem 5], and its continuity in $\mu$ [GK16, Proposition 6]. + - Prove the Gaussian bounds $H(\mu)\le T^*(\mu)\le 2H(\mu)$ with + $H(\mu)=\sum_a2\sigma^2/\Delta_a^2$ and $\Delta_{a^*}=\min_{b\ne a^*}\Delta_b$ + [GK16, Section 2.2]. + - Prove the two-armed values: $T^*(\mu)^{-1}=d(\mu_1,z^*)=d(\mu_2,z^*)$ for the $z^*$ between + the two means at which these divergences are equal [KCG16, Section 3, Theorem 6], and in + particular $T^*(\mu)=8\sigma^2/\Delta^2$ with $w^*=(\tfrac12,\tfrac12)$ for Gaussian arms + with a common variance. +5. **Top Two allocations.** + - Define the $\beta$-optimal allocations: maximize $D(\theta,w,\neg i^*)$ under $w_{a^*}=\beta$, + with value $T^*_\beta(\theta)^{-1}$ [R16; JDBdHK22]. + - Prove $T^*_{1/2}(\theta)\le2T^*(\theta)$, uniqueness of the $\beta$-optimal allocation for + best arm identification in exponential families, and its equalization property. +6. **Closed forms for Gaussian tasks.** Prove the divergences to half-spaces, to minimum-threshold + sets and to spheres for Gaussian arms [DK19, Lemmas 36–39]. Prove the characteristic time + $\sum_a 2\sigma^2/(\mu_a-\gamma)^2$ of Gaussian thresholding. + +Generalization: arbitrary models and divergences in `ℝ≥0∞`, where [GK16] works with exponential +families and real divergences. + +## Layer 4: Deviation inequalities and GLR stopping rules + +1. **Empirical means along a run.** + - Define the per-arm sums, counts and empirical means of a run (from LML's `SumRewards`), and + the sum-count statistic of a history. + - Transfer statements about the i.i.d. reward stream of an arm to its empirical mean after each + number of pulls, as in the Bandits roadmap's Layer 1.3. +2. **Deviation inequalities for exponential families.** + - Prove the per-arm time-uniform bound + $P\big(\exists t,\ N_a(t)\,d(\hat\mu_a(t),\mu_a)\ge x+c\log(1+\log N_a(t))\big)$ for the + constants of [KK21] (from Ville's inequality and mixtures of tilted supermartingales). + - Prove the joint bound for any set $S$ of arms and any sampling rule, + $P\big(\exists t,\ \sum_{a\in S}\big[N_a(t)\,d(\hat\mu_a(t),\mu_a)-3\log(1+\log N_a(t))\big]^+ + \ge|S|\,\mathcal C^{\exp}(x/|S|)\big)\le e^{-x}$ [KK21, Theorem 7]. Here + $\mathcal C^{\exp}$ is defined through the inverse of $u\mapsto u-\log u$ on $[1,\infty)$ + (a branch of the Lambert function). Build that inverse and the estimate + $\mathcal C^{\exp}(x)=x+O(\log(1+x))$ with explicit constants. + - Deduce the threshold $\beta(t,\delta)=3\sum_a\log(1+\log N_a(t))+K\,\mathcal C^{\exp} + (\log(1/\delta)/K)$ for general identification [KK21, Proposition 15]. + - Prove the union-bound thresholds of [GK16, Proposition 12] ($\log(Ct^\alpha/\delta)$, $\alpha>1$, + with an explicit $C(\alpha,K)$), of [GK16, Theorem 10] (Bernoulli arms only, + $\log(2t(K-1)/\delta)$, through the Krichevsky–Trofimov mixture of [GK16, Lemma 11]) and of + [LS, Lemmas 33.7–33.8, Proposition 33.9], and the uniform deviation bound of [MCP14] used by + [DK19, Lemma 32]. +3. **GLR statistics and stopping rules.** + - Define the GLR statistic of an answer, + $\mathrm{GLR}_t(\neg i)=\inf_{\lambda\in\neg i}\sum_aN_a(t)\,d(\hat\mu_a(t),\lambda_a) + =t\,D(\hat\mu(t),N(t)/t,\neg i)$, its measurability, and the GLRT stopping and recommendation + rules with thresholds $\beta(t,\delta)$ on top of any sampling rule. + - Prove that if $\beta$ satisfies $P_\mu(\exists t,\ \sum_aN_a(t)d(\hat\mu_a(t),\mu_a)>\beta(t,\delta)) + \le\delta$, then the GLRT rules are $\delta$-correct on every task, for every sampling rule + [GK16, Proposition 12; DKM19, Theorem 1; DK19, Theorem 10]. +4. **Generic sample-complexity reductions.** + - Asymptotic: if, on events $E_T$ with $\sum_TP(E_T^c)<\infty$, the statistic + $\mathrm{GLR}_t(\neg i^*)$ exceeds $t\,(T^*(\mu)^{-1}-\varepsilon)$ for $\sqrt T\le t\le T$, then + $\limsup_{\delta\to0}\mathbb E[\tau_\delta]/\log(1/\delta)\le(T^*(\mu)^{-1}-\varepsilon)^{-1}$ + for every threshold with $\beta(t,\delta)\le\log(Ct^\alpha/\delta)$ [GK16, proof of + Theorem 14]. + - Non-asymptotic: + $\mathbb E[\tau]\le T_0(\delta)+\sum_tP(E_t^c)$ where $T_0(\delta)$ solves the stopping + inequality [DKM19, Lemmas 1–2; DK19, Lemma 13]. + - State both for arbitrary tasks, so that each sampling rule below only proves the convergence + of its allocations. +5. **Unknown variances.** For the Gaussian model with unknown variances (Layer 1.3), prove that + the cost of the alternatives with a common mean $\lambda$ for two arms is + $\sum_c\frac{w_c}2\log\big(1+\frac{(\mu_c-\lambda)^2}{\sigma_c^2}\big)$, define the GLR statistic, + and prove the $\delta$-correctness of its stopping rule with the thresholds of [JDK23a]. The + lower bound of this model is Layer 2.3. + +Generalization: arbitrary tasks with exponential-family arms, where [GK16] treats best arm +identification. + +## Layer 5: Tracking and asymptotically optimal sampling rules + +1. **Tracking.** + - Prove the guarantees of C-tracking ($|N_a(t)-\sum_{s] 0, expectedStoppingTime + (trackAndStop κ meanSet (fun δ t ↦ log (r t / δ)) δ) + (stationaryEnv ((baiTask κ meanSet).ν μ)) ≤ c * ENNReal.ofReal (log (1 / δ)) := + sorry + +end LMLRoadmaps.Identification diff --git a/LMLRoadmaps/Identification/metadata.toml b/LMLRoadmaps/Identification/metadata.toml new file mode 100644 index 0000000..151aa3a --- /dev/null +++ b/LMLRoadmaps/Identification/metadata.toml @@ -0,0 +1 @@ +topic = "math.ST"