diff --git a/LMLRoadmaps/Identification/README.md b/LMLRoadmaps/Identification/README.md index 9670f19..bd29691 100644 --- a/LMLRoadmaps/Identification/README.md +++ b/LMLRoadmaps/Identification/README.md @@ -19,12 +19,18 @@ are: 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; -- exponential families with a sufficient statistic, on any measurable space; -- 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; +- identification tasks with arbitrary models, answer sets and multiple correct answers, asking + about the arm means through a mean functional; +- product models and their $\mathrm K_{\inf}$ transportation costs; +- exponential families with a real or vector sufficient statistic, on any measurable space, and + the Cramér–Chernoff rate function; +- the change of measure at stopping times, for any two algorithm-environment pairs; +- transportation costs and their continuity (Berge's maximum theorem, with non-compact + alternatives; Sion's minimax theorem); +- conditional domination of moment generating functions, exponential supermartingales, + generalized likelihood ratio statistics and their time-uniform deviation inequalities; +- tracking lemmas, a generic sample-complexity reduction, a phased-elimination template, + AdaHedge; - large deviations of empirical means under static allocations. `README.md` is the definitive specification; `Suggested.lean` records selected interfaces and is @@ -33,7 +39,10 @@ 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 exponential families, +`LMLExplore/Probability/Moments/` for rate functions and bounds on moment generating functions, +`LMLExplore/Probability/Martingale/` for exponential supermartingales, `LMLExplore/Probability/LargeDeviations/` for Cramér-type bounds, +`LMLExplore/SequentialLearning/` for the change of measure and the run-to-stream transfer, `LMLExplore/Topology/Semicontinuous/` for Berge's maximum theorem, `LMLExplore/OnlineLearning/` for AdaHedge). @@ -42,24 +51,39 @@ AdaHedge). 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. +It also owns three sequential-learning tools that the Bandits and ReinforcementLearning roadmaps +build on: the chain rule for the divergence of stopped histories (Layer 2.1), the transfer from +runs to the per-arm observation streams (Layer 4.1), and conditional domination of moment +generating functions with its exponential supermartingales (Layer 4.2). | 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` | +| Interaction protocol, runs, trajectory measure, stationary environments | LML `SequentialLearning/`: `Algorithm`, `Environment`, `IsAlgEnvSeq`, `trajMeasure`, `stationaryEnv`, `stepKernel`, `IsAlgEnvSeq.filtrationAction` | +| 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`); LMLExplore `SequentialLearning/StoppedHistory.lean` (`Learning.notStoppedSet`, `Learning.stoppedHistMeasure_congr`) | +| Pull counts, reward sums, empirical means, per-arm reward streams | LML `SequentialLearning/FiniteActions.lean` (`pullCount`, `rewardByCount`), `SumRewards.lean`, `Online/Bandit/ArrayProbSpace.lean` (`streamMeasure`); LMLExplore `SequentialLearning/SumRewards.lean` | +| Conditional means of the feedback and their martingale | LML `SequentialLearning/Means.lean` (`Environment.means`, `IsAlgEnvSeq.condExp_feedback`), `FeedbackMartingale.lean` (`noiseSum`, `IsAlgEnvSeq.martingale_noiseSum`) | +| KL divergence of histories at a fixed horizon | LML `SequentialLearning/DivergenceDecomposition.lean` (`IsAlgEnvSeq.klDiv_map_history_stepKernel`, for any two algorithm-environment pairs); LMLExplore `Learning.IsAlgEnvSeq.klDiv_map_history_eq_sum_pullCount`, `Learning.klDiv_stoppedHistMeasure_le` | | 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) | +| Sub-Gaussian and sub-exponential random variables, unconditional and conditional | Mathlib `Probability/Moments/SubGaussian.lean` (`HasSubgaussianMGF`, `Kernel.HasSubgaussianMGF`, `HasCondSubgaussianMGF`), LML `ForMathlib/Probability/Moments/SubExponential.lean` (`HasSubexponentialMGF`, `HasCondSubexponentialMGF`); LMLExplore `Probability/Moments/MGFDominated.lean` (`MGFDominatedAbove`, `MGFDominatedBelow`) | +| Design operators, self-normalized bounds, G-optimal designs | Bandits roadmap, Layer 8 (`designOp`, the design operator $V(\pi)$ of a design, the self-normalized bound, the Kiefer–Wolfowitz theorem); Tau Ceti `Analysis/InnerProductSpace/Frame.lean` (`frameOperator`) | | 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`) | +| Tilts and transforms of standard laws | Tau Ceti `Probability/Distributions/Tilted.lean` (`gammaMeasure_tilted_mul`, `gaussianReal_tilted_mul`, `poissonMeasure_tilted_mul`), `Probability/Distributions/Gaussian/ChiSquared.lean` (`gaussianReal_map_sq`) | +| Fenchel conjugates, Bregman divergences | Tau Ceti `Analysis/Convex/Conjugate.lean` (`fenchelConjugate`, for a bilinear pairing), LML `ForMathlib/Analysis/Convex/Bregman/Basic.lean` (`bregDiv`) | | 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. +identification belong here, and so do three general sequential-learning tools: the chain rule at +a stopping time for any two algorithm-environment pairs, the transfer of events about the +observations of each arm from runs to the per-arm streams (whose single-arm form for real rewards +the Bandits roadmap's Layer 1.3 uses), and conditional domination of moment generating +functions with its exponential supermartingales and Ville bounds. The ReinforcementLearning +roadmap's Layer 6 regroups the first two by the keys of key-determined environments; the Bandits +and ReinforcementLearning roadmaps derive their time-uniform concentration inequalities from the +third. Outside this roadmap: - best policy identification in Markov decision processes; @@ -67,8 +91,11 @@ Outside this roadmap: - 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]. +- stopping thresholds, deviation inequalities and sampling rules built on $\mathrm K_{\inf}$ or + $\mathrm{KL}_{\inf}$ for nonparametric classes (bounded or heavy-tailed arms), including the + bounded-arm Top Two results of [JDBdHK22]. The $\mathrm K_{\inf}$ transportation costs of these + classes (Layer 1.4), their lower bounds (Layer 2.3) and the elimination algorithms for + sub-Gaussian or bounded arms (Layers 7, 8.1–8.2) are in scope. ## Conventions @@ -80,16 +107,21 @@ the stopping time $\tau$ is the number of rounds played. A paper's round $t$ is **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`. +bounds, the pure exploration game and the run-to-stream transfer (Layers 0–3 and 4.1) are stated +for general `𝓨`. Exponential families live on any measurable space, with a real or vector +statistic; the algorithms built on empirical means use `𝓨 = ℝ`, or the statistic of an +exponential family on `𝓨`. 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. +exponential families (Layer 1.2), parameters of linear models (Layer 9), pairs (mean, variance) +(Layer 1.3) and the arm laws themselves (Layer 1.1) are all models. The classical tasks ask about +the arm means through a *mean functional* `mean : Θ → α → ℝ`; the tasks on vectors of means are +the case `Θ = α → ℝ`, `mean = id`. A *product model* (Layer 1.4) has models `θ : α → Θ₀`, arm `a` +of `θ` depending on `θ a` only. **Divergences and allocations.** Divergences between arm laws are Mathlib's `klDiv`, valued in `ℝ≥0∞`. Allocations (proportions of samples) are vectors `w : α → ℝ` with nonnegative entries @@ -107,7 +139,9 @@ 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]. +budget can be strictly easier than fixed confidence [KCG16, Theorem 14]. The divergence from an +empirical mean outside the open interval of means of an exponential family is the value of the +Cramér rate function (Layer 1.2), also `ℝ≥0∞`-valued. **Guarantees.** - An identification algorithm is `IdentAlg Unit α 𝓨 ℐ`. @@ -127,7 +161,10 @@ budget can be strictly easier than fixed confidence [KCG16, Theorem 14]. 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. +`∀ᶠ T in atTop`. Never use `limsup`/`liminf` of real sequences as the primary form. Stopping +thresholds are `ℝ≥0∞`-valued functions `β n h` of the round `n` and of the history +`h : Hist Unit α 𝓨 n`, for each confidence level, so that thresholds depending on the pull counts +[KK21] are covered; thresholds depending on the round only are the special case. **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 @@ -163,10 +200,10 @@ forms above, and that development may be adapted to them. | Layer | Content | Prerequisites | | --- | --- | --- | -| 0 | Identification algorithms, correctness and sample complexity | LML `IdentAlg` | -| 1 | Identification tasks and exponential families | Layer 0 | +| 0 | Identification algorithms, correctness, sample complexity and phased elimination | LML `IdentAlg` | +| 1 | Identification tasks, exponential families and product models | Layer 0 | | 2 | Change of measure and lower bounds | Layers 0–1; Bandits roadmap Layer 4 | -| 3 | The pure exploration game | Layer 1 | +| 3 | The pure exploration game | Layer 1; Bandits roadmap Layer 8 (design operators) | | 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 | @@ -174,7 +211,7 @@ forms above, and that development may be adapted to them. | 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 +## Layer 0: Identification algorithms, correctness, sample complexity and phased elimination 1. **Constructions and canonical runs.** - Construct an identification algorithm from per-length rules: a sampling rule, measurable @@ -199,37 +236,95 @@ forms above, and that development may be adapted to them. $\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$. + - For every environment, every run with real feedback and every stopping time $\tau$ of LML's + `IsAlgEnvSeq.filtrationAction` (the event $\{t<\tau\}$ is known when $A_t$ is chosen) with + $\mathbb E[\tau]<\infty$, prove Wald's identity for the feedback + $\mathbb E\big[\sum_{t<\tau}Y_t\big]=\mathbb E\big[\sum_{t<\tau}m_t(A_t)\big]$, where $m_t(a)$ + is LML's conditional mean `env.means O A Y a t`, when the conditional absolute means + $\int|y|\,d\big(\texttt{env.measure O A Y t}\big)(A_t)$ are bounded by a constant. The proof + stops the martingale $\sum_{t 0). - Define the open interval of means `ρ.expFamilyMeans T`, the natural parameter `ρ.natParam T μ` of a mean, and the mean parametrization $\mu\mapsto\rho_{\eta(\mu)}$. + - Prove that the means and the divergence $d$ below do not change, and the natural parameters + shift by $\eta_0$, when $\rho$ is replaced by a member $\rho_{\eta_0}$ + (`expFamily_expFamily`), and that they depend on $(\rho,T)$ only through the law + `ρ.map T` of the statistic: the family of $(\rho,T)$ and the natural exponential family of + `ρ.map T` have the same log-partition function, means and divergence. - Prove the closed form $\mathrm{KL}(\rho_{\eta(\mu)},\rho_{\eta(\mu')})=d(\mu,\mu') =\psi(\eta')-\psi(\eta)-\mu(\eta'-\eta)$ (`ρ.expFamilyDiv T μ μ'`, 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 - $P\big(\sum_{i0$ (`gammaMeasure a r`, `T = id`, the family of + `gammaMeasure a 1` with natural parameter $1-r$, by Tau Ceti's `gammaMeasure_tilted_mul`), + with means $a/r$ and $d(\mu,\mu')=a\big(\tfrac\mu{\mu'}-1-\log\tfrac\mu{\mu'}\big)$; + - the exponential laws (`expMeasure r = gammaMeasure 1 r`), the shape $a=1$; - the Gaussian laws of known mean $m$: $\rho=\mathcal N(m,1)$, $T(x)=(x-m)^2$, members - $\mathcal N(m,v)$ with natural parameter $(1-1/v)/2$, means the variances $v>0$, and - $d(v,v')=\tfrac12\big(\tfrac v{v'}-1-\log\tfrac v{v'}\big)$. + $\mathcal N(m,v)$ with natural parameter $(1-1/v)/2$, means the variances $v>0$. The law of + $T$ under $\rho$ is the gamma law of shape and rate $\tfrac12$ (Tau Ceti's + `gaussianReal_map_sq`), so by the invariance above + $d(v,v')=\tfrac12\big(\tfrac v{v'}-1-\log\tfrac v{v'}\big)$ is the shape-$\tfrac12$ case. + + LMLExplore's direct proofs for the exponential laws and the Gaussian laws of known mean + (`ExponentialFamily/Exponential.lean`, `expFamilyDiv_sub_sq_gaussianReal`) become these + corollaries. - Define the bandit of a mean vector, whose arm `a` has the law of mean $\mu_a$ in the - exponential family $(\rho_a,T_a)$ on a common observation space `𝓨`. 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. + exponential family $(\rho_a,T_a)$ on a common observation space `𝓨`: the product model of + Layer 1.4 with these families. - The merged natural-exponential-family development of LMLExplore is restated in this generality by the Refactors roadmap, Layer 0.2. -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)$. +3. **Exponential families with a vector statistic, and Gaussian arms with unknown variances.** + - For a finite-dimensional real inner product space `E`, a probability measure $\rho$ on `𝓧` and + a measurable statistic `T : 𝓧 → E` whose natural-parameter set, the interior of + $\{\eta:\exp\langle\eta,T\rangle\text{ is }\rho\text{-integrable}\}$, is nonempty, define the + family of tilts $\rho_\eta=$ `ρ.tilted (fun x ↦ ⟪η, T x⟫)` and the log-partition function + $\psi(\eta)=\log\int\exp\langle\eta,T\rangle\,d\rho$ [Bro86, Chapter 1; BN78; WJ08, + Section 3]. For `E = ℝ` these are the families of item 2. + - Prove: the natural-parameter set and $\psi$ are convex; tilting $\rho_\eta$ by + $\langle\eta',T\rangle$ gives $\rho_{\eta+\eta'}$; on each line, + $t\mapsto\psi(\eta+tu)-\psi(\eta)$ is `cgf (fun x ↦ ⟪u, T x⟫) ρ_η`, so item 2 applies to + $\langle u,T\rangle$; $\psi$ is differentiable on the natural-parameter set with gradient the + mean of $T$ under $\rho_\eta$; the log-likelihood ratio of $\rho_\eta$ against $\rho_{\eta'}$ + is $\langle\eta-\eta',T\rangle+\psi(\eta')-\psi(\eta)$, $\rho_\eta$-almost everywhere; and + $\mathrm{KL}(\rho_\eta,\rho_{\eta'})=\psi(\eta')-\psi(\eta)-\langle\nabla\psi(\eta),\eta'-\eta\rangle$, + LML's `bregDiv ψ η' η (fderiv ℝ ψ η)` [BMDG05]. + - Prove that, for independent observations of law $\rho_\eta$, the likelihood ratio process + $\exp\big(\langle\eta'-\eta,\sum_{i0$, are the family of + $\mathcal N(0,1)$ with $T(x)=(x,x^2)$ in `EuclideanSpace ℝ (Fin 2)`, with natural parameter + $(\mu/\sigma^2,(1-1/\sigma^2)/2)$. Their divergence + $\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)$ + is LMLExplore's `klDiv_gaussianReal_gaussianReal`. + - The two-parameter Gaussian model $\theta=(\mu_a,\sigma_a^2)_a$ is LMLExplore's + `gaussianMeanVarBandit`, a product model (Layer 1.4) whose mean functional is the means; the + sufficient statistics of an arm are its sums of $Y$ and $Y^2$ (Layer 4.5). +4. **Product models and $\mathrm K_{\inf}$.** + - A *product model* is given by a type `Θ₀` of arm parameters, arm laws + `κ : α → Θ₀ → Measure 𝓨` (probability measures), per-arm admissible sets $S_a\subseteq$ `Θ₀` + and per-arm means $m_a:$ `Θ₀ → ℝ`. Its models are `θ : α → Θ₀`, with + `ν θ a = κ a (θ a)` and mean functional $\theta\mapsto(m_a(\theta_a))_a$, and its + transportation cost is $\sum_aw_a\,\mathrm{KL}(\kappa_a(\theta_a),\kappa_a(\lambda_a))$, a + function of the per-arm divergences only. Instances: vectors of means of per-arm exponential + families (`Θ₀ = ℝ`, $S_a$ the means of $(\rho_a,T_a)$, $m_a=$ `id`); Gaussian arms with known + per-arm variances; the two-parameter Gaussian model (`Θ₀ = ℝ × ℝ≥0`, + $m_a(\mu,\sigma^2)=\mu$); and the model of all bandits with real observations of Layer 1.1 + (`Θ₀ = ProbabilityMeasure ℝ`, $\kappa_a(P)=P$, $m_a(P)=\int x\,dP$), with $S_a$ a class of + laws such as the laws on $[0,1]$ or the σ²-sub-Gaussian laws. + - Define, in `ℝ≥0∞`, + $\mathrm K^-_a(x,u)=\inf\{\mathrm{KL}(\kappa_a(x),\kappa_a(y)):y\in S_a,\ m_a(y)\le u\}$ and + $\mathrm K^+_a(x,u)=\inf\{\mathrm{KL}(\kappa_a(x),\kappa_a(y)):y\in S_a,\ m_a(y)\ge u\}$ + [AJG20; JDK23a, (1)]. Prove that $\mathrm K^-_a(x,\cdot)$ is antitone and zero from + $m_a(x)$ on, and $\mathrm K^+_a(x,\cdot)$ monotone and zero up to $m_a(x)$ for $x\in S_a$. + LMLExplore's `dInf` (the Bandits roadmap's Layer 4.4) is $\mathrm K^+$ with a strict + inequality on the mean. + - For best arm identification on a product model, a model $\theta\in\prod_cS_c$ with best arm + $a$ and an allocation with positive entries, prove + $\inf\{\mathrm{cost}_\theta(w,\lambda):\lambda\in\prod_cS_c,\ \exists b\ne a,\ + m_b(\lambda_b)\ge m_a(\lambda_a)\}=\min_{b\ne a}\inf_u\big(w_a\mathrm K^-_a(\theta_a,u)+ + w_b\mathrm K^+_b(\theta_b,u)\big)$ [AJG20; JDK23a, (1)], which is $D(\theta,w,\neg a)$ when the + closure property of Layer 1.1 holds. Prove the analogous formulas for top-$m$ identification + (pairs $a\in S$, $b\notin S$) and for thresholding + ($\min\big(\min_{a\in S}w_a\mathrm K^-_a(\theta_a,\gamma),\min_{a\notin S} + w_a\mathrm K^+_a(\theta_a,\gamma)\big)$ for the answer $S$). + - Prove the instances: for exponential families in the mean parametrization, + $\mathrm K^-_a(\mu,u)=d_a(\mu,u)$ for means $u\le\mu$ (and symmetrically for $\mathrm K^+$); + for the two-parameter Gaussian model, + $\mathrm K^-_a((\mu,\sigma^2),u)=\tfrac12\log\big(1+(\mu-u)^2/\sigma^2\big)$ for $u\le\mu$ + [JDK23a, Lemma 3] (from LMLExplore's `iInf_klDiv_gaussianReal_gaussianReal`); for laws on + $[0,1]$, $\mathrm K^+(P,u)\ge$ `klBer` $(m(P), u)$ for $u\ge m(P)$ and + $\mathrm K^-(P,u)\ge$ `klBer` $(m(P), u)$ for $u\le m(P)$, with equality for Bernoulli laws + (data processing through the kernel $x\mapsto\mathcal B(x)$). + - State the alternative-cost lemmas of LMLExplore's `Identification/Task/ExpFamily.lean`, and + those of best arm identification, thresholding, minimum threshold and Any Low Arm in Layer 3, + for product models with `Θ₀ = ℝ` whose per-arm divergences + $(x,y)\mapsto\mathrm{KL}(\kappa_a(x),\kappa_a(y))$ are continuous on $S_a\times S_a$, zero + exactly on the diagonal and monotone in each argument on each side of the other: their proofs + use nothing else. Exponential families are the instance. 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. +many answers; questions about the means of arbitrary models through a mean functional, and +product models with $\mathrm K_{\inf}$ costs [AJG20, JDK23a]. ## 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 + - For any two algorithm-environment pairs `(alg, env)` and `(alg', env')`, a measurable + stopping rule $S$ and its hitting time $\tau$, almost surely finite under the first pair, + prove the chain rule at the stopping time [GMS19, Section 2; KCG16, Lemma 1]: + $$\mathrm{KL}\big(\texttt{stoppedHistMeasure alg env S},\texttt{stoppedHistMeasure alg' env' S}\big) + \le\sum_t\mathrm{KL}\big(\mu_t\otimes_m\texttt{stepKernel alg env }t,\ + \mu_t\otimes_m\texttt{stepKernel alg' env' }t\big),$$ + with $\mu_t$ the law of the $t$-round history under the first pair restricted to LMLExplore's + `notStoppedSet S t`, that is, + $\mathbb E\big[\sum_{t<\tau}\mathrm{KL}(\text{step}_t(H_t)\,\|\,\text{step}'_t(H_t))\big]$ when the + spaces are countably generated (LML's `klDiv_compProd_right_eq_lintegral`), with equality + when $\tau$ is also almost surely finite under the second pair. The fixed-horizon case is + LML's `IsAlgEnvSeq.klDiv_map_history_stepKernel`; the proof changes both pairs after the + stopping time (LMLExplore's `stoppedHistMeasure_congr`). + - Prove the same bound for the joint law of the stopped history and the output when the output + kernel is common (Mathlib's `klDiv_compProd_left`). + - For one algorithm run in `stationaryEnv ν` and `stationaryEnv ν'` on finite arms, deduce $\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`. + almost surely finite under $\nu'$. LMLExplore's `klDiv_stoppedHistMeasure_le` becomes this + corollary; the fixed-horizon case is LML's `IsAlgEnvSeq.klDiv_map_history_stepKernel`. + - The regrouping by the keys of key-determined environments is the ReinforcementLearning + roadmap's Layer 6.2, built on the first bullet. 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 @@ -299,19 +510,20 @@ many answers. 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]. + - For any task, a $\delta$-correct algorithm with $\delta\in(0,1/2)$ and an admissible model + $\theta$ with a single correct answer, prove + $\mathbb E_\theta[\tau]\ge T^*(\theta)\,\mathrm{kl}(\delta,1-\delta)$ [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. + - For tasks with finitely many answers, prove + $\liminf_{\delta\to0}\mathbb E_\theta[\tau_\delta]/\log(1/\delta)\ge T^*(\theta)$ at every + admissible model $\theta$, whatever its number of correct answers, for every family of + $\delta$-correct algorithms [DK19, Theorem 1, Proposition 18, Lemma 19], in the eventual form + of the Conventions. At a model with a single correct answer it follows from the first bullet. 4. **Fixed-budget lower bounds.** - For two models $\theta,\lambda$ without a common correct answer and an algorithm with budget $T$, prove @@ -322,7 +534,9 @@ many answers. - 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. +identification in exponential families; the chain rule at a stopping time for any two +algorithm-environment pairs, where [KCG16, GMS19] treat one algorithm against two stationary +bandits. ## Layer 3: The pure exploration game @@ -334,8 +548,15 @@ identification in exponential families. 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). + - Prove that $(\theta,w)\mapsto D(\theta,w,\neg i)$ is upper semicontinuous, hence measurable, + on every topological space of models on which $\theta\mapsto\mathrm{KL}(\nu_a(\theta), + \nu_a(\lambda))$ is real-valued and continuous for every arm and every alternative $\lambda$ + (an infimum of continuous functions). + - For a pullback `task.comap f` (Layer 1.1), prove + $\mathrm{cost}_\theta(w,\lambda)=\mathrm{cost}_{f\theta}(w,f\lambda)$ and + $D(\theta,w,\neg i)\ge D(f\theta,w,\neg i)$, with equality when the range of $f$ contains the + alternatives to $i$ of `task`; deduce $T^*_{\texttt{comap}}(\theta)\le T^*(f\theta)$, with + equality under the same condition for every answer. 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; @@ -343,94 +564,251 @@ identification in exponential families. - 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; + - Prove Berge's maximum theorem for upper hemicontinuous compact-valued correspondences + [DK19, Theorem 22], from Mathlib's `IsCompact.continuous_sSup`/`continuous_sInf`. + - Prove the joint continuity of $(\theta,w)\mapsto D(\theta,w,A)=\inf_{\lambda\in A} + \mathrm{cost}_\theta(w,\lambda)$ on $\prod_aS_a\times[0,\infty)^\alpha$, for every set + $A\subseteq\prod_aS_a$ of alternatives, compact or not, for a product model (Layer 1.4) with + topological spaces $S_a$ such that each per-arm divergence + $k_a(x,y)=\mathrm{KL}(\kappa_a(x),\kappa_a(y))$ is real-valued and continuous on + $S_a\times S_a$, and every $x\in S_a$ has a neighbourhood $U$ such that + $\{y\in S_a:\exists x'\in U,\ k_a(x',y)\le r\}$ is relatively compact in $S_a$ for every $r$: + the non-compact setting of [FKV14; DK19, Theorem 23, Lemmas 24–27]. Upper semicontinuity is + Layer 3.1. For lower semicontinuity at $(\theta,w)$, near-optimal alternatives at nearby points + have their coordinates of positive weight in a compact set, on which $k_a$ is uniformly close + to $k_a(\theta_a,\cdot)$. Prove also the joint continuity on $M\times[0,\infty)^\alpha$ for any + topological space of models with real-valued divergences continuous on $M\times M$ when the + closure of $\neg i$ in $M$ is compact [DK19, Theorem 22]. Prove that the per-arm hypotheses + hold for exponential families in the mean parametrization whose divergence $d(x,y)$ tends to + $+\infty$ as $y$ tends to an endpoint of the means (every instance of Layer 1.2), and for the + two-parameter Gaussian model on `ℝ × (0, ∞)`. + - Deduce, under either hypothesis, for every task with finitely many answers: - 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]. + [DK19, Theorem 4, Lemmas 28–30]. + + LMLExplore's `Identification/Task/Continuity.lean` and `Identification/Task/Oracle.lean` + prove these consequences from the joint continuity, which LMLExplore derives for best arm + identification with one exponential family only (`continuousOn_altCost_baiTask_restrict`); + the theorem above discharges it for every task on these product models. - 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]. +4. **Best arm identification in exponential families** [GK16, Section 2], with arm $a$ in its own + exponential family $(\rho_a,T_a)$ with divergence $d_a$, all families having the same open + interval of means. + - Prove that $D(\mu,w,\neg a^*)=\min_{b\ne a^*}\inf_x\big(w_{a^*}d_{a^*}(\mu_{a^*},x)+ + w_bd_b(\mu_b,x)\big)$, the infimum over the means $x$ between $\mu_b$ and $\mu_{a^*}$ + (Layer 1.4), and that when $a^*$ and $b$ have the same family it is attained at 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 costs of the pairs + $(a^*,b)$ [GK16, Lemma 4, Theorem 5, Proposition 6]. For distinct families, uniqueness comes + from the strict concavity of each pair cost along segments that are not on a ray, the + minimizer of the inner infimum moving with the weights. Prove the scalar equation of + [GK16, Theorem 5] when the inner infimum has a unique minimizer for all weights, in particular + for a common family and for Gaussian arms with arm-dependent known variances. Prove the + continuity of $w^*$ 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. + $H(\mu)=\sum_a2\sigma^2/\Delta_a^2$ and $\Delta_{a^*}=\min_{b\ne a^*}\Delta_b$, for a common + variance $\sigma^2$ [GK16, Section 2.2]. + - Prove the two-armed values for a common family: $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. + - Prove $T^*_{1/2}(\theta)\le2T^*(\theta)$, and the uniqueness and the equalization property of + the $\beta$-optimal allocation for best arm identification with the per-arm exponential + families of item 4. +6. **Closed forms for Gaussian arms.** Let arm $a$ have Gaussian observations of known variance + $\sigma_a^2>0$ and mean $\langle\varphi(a),\theta\rangle$, for $\theta$ in a finite-dimensional + real inner product space `E` and features $\varphi:\alpha\to E$; the unstructured model is + `E = EuclideanSpace ℝ α` with $\varphi(a)$ the basis vectors. + - Prove $\mathrm{cost}_\theta(w,\lambda)=\tfrac12\|\theta-\lambda\|^2_{V_w}$ for the design + operator $V_w=\sum_aw_a\sigma_a^{-2}\,\varphi(a)\otimes\varphi(a)$ (the operator $V(\pi)$ of + the Bandits roadmap's Layer 8.6, Tau Ceti's `frameOperator` of the vectors + $\sqrt{w_a}\,\sigma_a^{-1}\varphi(a)$). + - For an affine half-space $H=\{\lambda:\langle y,\lambda\rangle\le c\}$ and + $\langle y,\theta\rangle>c$, prove + $\inf_{\lambda\in H}\mathrm{cost}_\theta(w,\lambda)=(\langle y,\theta\rangle-c)^2/ + (2\|y\|^2_{V_w^{-1}})$, with $\|y\|^2_{V_w^{-1}}=\sup_x\big(2\langle y,x\rangle- + \langle x,V_wx\rangle\big)\in[0,\infty]$, which is $\langle y,V_w^+y\rangle$ for $y$ in the + range of $V_w$ and $\infty$ otherwise (the cost is then $0$). The infimum over a finite union + of half-spaces is the minimum of these values [FJJR19, Theorem 1]. + - The closures of the alternatives of best arm identification, top-$m$ identification, + thresholding, half-space identification, the answer "none" of Any Low Arm and the answer + "every mean is above $\gamma$" of the minimum-threshold task are finite unions of half-spaces. + Deduce their costs with arm-dependent variances, among them + $D(\mu,w,\neg a)=\min_{b\ne a}(\mu_a-\mu_b)^2/\big(2(\sigma_a^2/w_a+\sigma_b^2/w_b)\big)$, the + characteristic time $\sum_a2\sigma_a^2/(\mu_a-\gamma)^2$ of thresholding, and for half-space + identification the unique optimal allocation proportional to $\sigma_a|u_a|$ and + $T^*(\mu)=2\big(\sum_a\sigma_a|u_a|\big)^2/\langle u,\mu\rangle^2$ [DK19, Lemma 36]. + - Prove the remaining closed forms of [DK19, Lemmas 37–39]: the answer "some mean is below + $\gamma$" of the minimum-threshold task (an orthant, with arm-dependent variances) and the + spheres (for a common variance). + - The characteristic time of linear identification (Layer 9.2) is the case of the half-spaces + $\{\lambda:\langle z^*-z,\lambda\rangle\le0\}$. Generalization: arbitrary models and divergences in `ℝ≥0∞`, where [GK16] works with exponential -families and real divergences. +families and real divergences; per-arm families, continuity on product models with non-compact +alternatives, and Gaussian costs with arm-dependent variances in design-operator form. ## Layer 4: Deviation inequalities and GLR stopping rules -1. **Empirical means along a run.** +1. **Empirical statistics along a run and the per-arm streams.** - 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.** + - For a run of any algorithm against `stationaryEnv ν`, with `ν : Kernel α 𝓨` on any measurable + space `𝓨`, and a predicate $q$ on the numbers of pulls `s : α → ℕ` and the first $s_a$ + observations of each arm (an element of `(a : α) → Fin (s a) → 𝓨`), prove the event transfer + to LML's per-arm stream model `streamMeasure ν` (the stack-of-rewards model + [LS, Section 4.6]): the probability that $q$ holds at some round for the pull counts and the + observations of each arm so far is at most the `streamMeasure ν`-probability that $q$ holds + for some `s` and the first $s_a$ stream observations of each arm. Prove its form up to a + horizon, its single-arm form, and the counting form: the expected number of rounds $t\mu,\ N(t)\,\bar d(\hat\mu(t),\mu)\ge x\big)\le + e\lceil x\log n\rceil e^{-x}$, by peeling over a geometric grid of $N(t)$; and the lower tail. - 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). + $P\big(\exists t,\ N_a(t)\,\bar d(\hat\mu_a(t),\mu_a)\ge x+c\log(1+\log N_a(t))\big)$ for the + constants of [KK21] (from these supermartingales, their mixtures (LMLExplore's + `supermartingale_integral_of_integrable`) and Ville's inequality). - 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]^+ + $P\big(\exists t,\ \sum_{a\in S}\big[N_a(t)\,\bar 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]. + (\log(1/\delta)/K)$ for general identification [KK21, Proposition 15], and, from the case + $|S|=2$ and a union bound over the $K-1$ pairs containing the best arm, the pairwise thresholds + $\beta_{a,b}(t,\delta)=3\sum_{c\in\{a,b\}}\log(1+\log N_c(t))+2\,\mathcal C^{\exp} + \big(\log((K-1)/\delta)/2\big)$, of order $\log(K/\delta)+O(\log\log t)$, for the covers of + item 3. - 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, + with an explicit $C(\alpha,K)$, from the two-sided bound of Layer 1.2, for arms dominated by + any exponential families), 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]. + [DK19, Lemma 32]. LMLExplore's thresholds for Gaussian arms (`unionBoundThreshold`, + `Identification/GaussianThreshold.lean`) are the Gaussian case. 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]. + - Define the GLR statistic of an answer for an evidence function $Z_n(h,\lambda)\in[0,\infty]$, + $\mathrm{GLR}_n(h,\neg i)=\inf_{\lambda\in\neg i}Z_n(h,\lambda)$ (LMLExplore's + `IdentTask.glr`), and its plug-in instance for an estimator $\hat\theta_n$ from $n$-round + histories to models: $Z_n(h,\lambda)=\sum_aN_a(h)\,\mathrm{KL}(\nu_a(\hat\theta_n(h)), + \nu_a(\lambda))$, so that $\mathrm{GLR}_n(h,\neg i)=n\,D(\hat\theta_n(h),N(h)/n,\neg i)$. For + exponential-family arms and the empirical means it is + $\inf_{\lambda\in\neg i}\sum_aN_a\,\bar d(\hat\mu_a,\lambda_a)$, the generalized likelihood + ratio, with the extension $\bar d$ of Layer 1.2 for empirical means outside the means; for + the two-parameter Gaussian model and the empirical means and variances it is the statistic of + [JDK23a] (item 5). Prove its measurability. + - Define the GLRT stopping and recommendation rules on top of any sampling rule, with thresholds + $\beta_n(h)$ depending on the round and the history (Conventions). + - Prove that if $P_\theta\big(\exists n,\ \beta_n(H_n)\beta^{i,j}_n(h)$ + for every $j$. Prove that for every model $\theta$ and every choice of $j(i)$ with + $\theta\in A_{i,j(i)}$ for each answer $i$ incorrect for $\theta$, the probability that it + stops with an incorrect answer is at most + $P_\theta\big(\exists n,\ \exists i\notin i^*(\theta),\ + \beta^{i,j(i)}_n(H_n)(\inf_{w\in W}D(\theta,w,\neg i))^{-1}$, for every family of thresholds with + $\beta_t(h,\delta)\le\log(1/\delta)+f(t)$ for all histories and $f(t)=o(t)$ + [GK16, proof of Theorem 14]. The bound $\beta_t(h,\delta)\le\log(Ct^\alpha/\delta)$ is a + case. LMLExplore's `IdentTask.eventually_expectedStoppingTime_glrt_le` (linear growth of the + statistic on good events) is the step after the lower semicontinuity. + - Almost sure: with the same statistic, recommendation and thresholds, if almost surely + $\hat\theta_t\to\theta$ and the distance from $N(t)/t$ to $W$ tends to $0$, prove that + almost surely, for every $c>(\inf_{w\in W}D(\theta,w,\neg i))^{-1}$, + $\tau_\delta\le c\log(1/\delta)$ for all small $\delta$ [GK16, Proposition 13]. - 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. + - State them for arbitrary tasks, estimators and history-dependent thresholds, so that each + sampling rule below (D- and C-tracking, Sticky Track-and-Stop, the game-based, Top Two and + Frank–Wolfe rules) only proves the convergence of its allocations on such events, given the + concentration of the estimator under sufficient exploration (Layer 5.1). 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. + $\sum_c\frac{w_c}2\log\big(1+\frac{(\mu_c-\lambda)^2}{\sigma_c^2}\big)$ (Layer 1.4), define the + GLR statistic as the plug-in statistic of item 3 for the empirical means and variances, and + prove the $\delta$-correctness of its stopping rule with the thresholds of [JDK23a], through the + transfer of item 1 for events about the per-arm sums of $Y$ and $Y^2$. The lower bound of this + model is Layer 2.3. Generalization: arbitrary tasks with exponential-family arms, where [GK16] treats best arm -identification. +identification; plug-in statistics of any estimator, history-dependent thresholds and covers of +the alternatives, and conditional domination by any cumulant generating function. ## Layer 5: Tracking and asymptotically optimal sampling rules @@ -440,26 +818,42 @@ identification. convergence of the proportions when the targets converge) [GK16, Lemmas 7, 8, 15, 17, 20, Proposition 9]. - Prove cumulative tracking [DKM19, Lemma 7]. - - Prove the concentration of the empirical means under forced exploration - [GK16, Lemma 19]. + - **Sufficient exploration in event form** [GK16, Lemma 19]. For arms dominated by exponential + families and any sampling rule, prove: if on events $G_T$ every arm has at least $g(t)$ pulls + at every round $t\in[h(T),T]$, for a nondecreasing $g$, then the probability of $G_T$ and of + an empirical mean farther than $\xi$ from $\mu$ at some round $t\in[h(T),T]$ is at most + $B\exp(-C\,g(h(T)))$, for constants $B,C>0$ depending on $\xi$ and the families (from + LMLExplore's `measure_exists_le_pullCount_and_empMean_notMem_Ioo_le`). With $g(t)=\sqrt t-K/2$ + and $h(T)=T^{1/4}$ this is summable in $T$. The exploration is an event, not a deterministic + property of the sampling rule, so that Top Two rules, which explore only with high + probability, use it; D-tracking's forced exploration is the case $G_T=\Omega$. 2. **Track-and-Stop.** - - Define Track-and-Stop (C- or D-tracking of a measurable selection of $w^*(\hat\mu)$, GLRT - stopping) for single-answer tasks with exponential-family arms. - - Prove that it is $\delta$-PAC with the thresholds of Layer 4.2 and asymptotically optimal on - every single-answer task: with C-tracking whenever $w^*(\mu)$ is convex, in particular when it - is unique [DK19, Lemma 6, Theorem 7]; with D-tracking when $w^*(\mu)$ is a singleton and - continuous at $\mu$. For best arm identification this is - $\limsup_{\delta\to0}\mathbb E_\mu[\tau_\delta]/\log(1/\delta)\le\alpha T^*(\mu)$ for - $\beta(t,\delta)=\log(r(t)/\delta)$, $r(t)=O(t^\alpha)$, $\alpha\in[1,e/2]$ - [GK16, Theorem 14]; also prove the almost-sure version [GK16, Proposition 13]. + - Define Track-and-Stop for any single-answer task and an estimator $\hat\theta$ (C- or + D-tracking of a measurable selection of $w^*(\hat\theta)$, the plug-in GLRT stopping rule of + Layer 4.3 with history-dependent thresholds, and the answer of $\hat\theta$ as + recommendation). + - For per-arm exponential-family arms and the empirical means, prove that it is $\delta$-PAC + with the thresholds of Layer 4.2 on every single-answer task [GK16, Proposition 12], and + asymptotically optimal through Layer 4.4: with C-tracking whenever $w^*(\mu)$ is convex, in + particular when it is unique [DK19, Lemma 6, Theorem 7]; with D-tracking when $w^*(\mu)$ is a + singleton and continuous at $\mu$. For best arm identification this is + $\limsup_{\delta\to0}\mathbb E_\mu[\tau_\delta]/\log(1/\delta)\le T^*(\mu)$ for + $\beta(t,\delta)=\log(r(t)/\delta)$ and $r(t)=O(t^\alpha)$ with any $\alpha\ge1$, which + improves the constant $\alpha T^*(\mu)$, $\alpha\in[1,e/2]$, of [GK16, Theorem 14]; also + prove the almost-sure version [GK16, Proposition 13]. LMLExplore + proves these for Gaussian arms (`Identification/GaussianThreshold.lean`), which become a + corollary. + - For the two-parameter Gaussian model, prove that Track-and-Stop with the empirical means and + variances as estimator and the thresholds of Layer 4.5 is $\delta$-PAC and asymptotically + optimal for the characteristic time of that model [JDK23a]. - Prove that for multiple answers Track-and-Stop reaches only $\max_{w\in\mathrm{conv}\,w^*(\mu)}D(\mu,w)^{-1}$ [DK19, Theorems 7, 9]. 3. **Sticky Track-and-Stop** [DK19, Algorithm 1]. - Define the sticky answer: the least oracle answer of a model of a small confidence region, for a fixed linear order on $\mathcal I$. - Prove that Sticky Track-and-Stop is $\delta$-correct and asymptotically optimal on every - multiple-answer task with finitely many answers and continuous divergences - [DK19, Theorems 10–11, Corollary 12, Lemmas 13–17]. + multiple-answer task with finitely many answers whose costs satisfy either continuity + hypothesis of Layer 3.3 [DK19, Theorems 10–11, Corollary 12, Lemmas 13–17]. Generalization: arbitrary tasks, where [GK16] treats best arm identification. @@ -488,7 +882,8 @@ Generalization: arbitrary tasks, where [GK16] treats best arm identification. - Prove the generic reduction of [QKR17, Theorem 3] and [JDBdHK22]: a leader that is correct except with probability $o(n^{-\alpha})$ and a challenger that avoids over-sampled arms give convergence to the $\beta$-optimal allocation, hence, with GLR stopping, - $\limsup_{\delta\to0}\mathbb E_\mu[\tau_\delta]/\log(1/\delta)\le T^*_\beta(\mu)$. + $\limsup_{\delta\to0}\mathbb E_\mu[\tau_\delta]/\log(1/\delta)\le T^*_\beta(\mu)$, through + the reduction of Layer 4.4 and the sufficient exploration in event form of Layer 5.1. - Prove asymptotic $\beta$-optimality for Gaussian arms of TTTS and T3C [SdHMKV20, Theorem 1] and of the empirical-best leader with the transportation-cost challenger. - Prove the results of TTUCB, the UCB-leader Top Two algorithm with tracking: asymptotic @@ -505,19 +900,28 @@ Generalization: arbitrary tasks, where [GK16] treats best arm identification. ## Layer 7: Elimination and confidence-bound algorithms -1. **Successive elimination** [EMM02, Theorem 3; EMM06, Theorem 8]. For σ²-sub-Gaussian arms, define successive elimination - with the time-uniform confidence intervals of the Bandits roadmap's Layer 1.2. Prove that it is - $\delta$-PAC for best arm identification and that, with probability at least $1-\delta$, it stops - after at most $\sum_a c\,\sigma^2\Delta_a^{-2}\log(K/(\delta\Delta_a))$ samples, with the explicit - constant of the proof. -2. **Median elimination** [EMM02, Theorem 4; EMM06, Theorem 10]. Define median elimination and prove that it is - $(\varepsilon,\delta)$-PAC (outputs an $\varepsilon$-best arm with probability at least - $1-\delta$) with at most $c\,K\varepsilon^{-2}\log(1/\delta)$ samples for σ²-sub-Gaussian arms, - with the explicit constant. +Throughout, "σ²-sub-Gaussian arms" and "laws on $[0,1]$" are the restricted tasks on the model of +all bandits with real observations (Layer 1.1): the guarantees hold for every bandit of the class. + +1. **Successive elimination** [EMM02, Theorem 3; EMM06, Theorem 8]. For σ²-sub-Gaussian arms, + define successive elimination as a phased-elimination algorithm (Layer 0.5: each phase pulls + every active arm once) with the time-uniform confidence intervals of the Bandits roadmap's + Layer 1.2. Prove that it is $\delta$-PAC for best arm identification and that, with probability + at least $1-\delta$, it stops after at most $\sum_a c\,\sigma^2\Delta_a^{-2}\log(K/(\delta\Delta_a))$ + samples, with the explicit constant of the proof. +2. **Median elimination** [EMM02, Theorem 4; EMM06, Theorem 10]. Define median elimination as a + phased-elimination algorithm (Layer 0.5) and prove that it is $(\varepsilon,\delta)$-PAC + (outputs an $\varepsilon$-best arm with probability at least $1-\delta$) with at most + $c\,K\varepsilon^{-2}\log(1/\delta)$ samples for σ²-sub-Gaussian arms, with the explicit + constant. 3. **LUCB and KL-LUCB** [KTAS12; KK13]. Define LUCB and KL-LUCB for top-$m$ identification with - tolerance $\varepsilon$. + tolerance $\varepsilon$, for σ²-sub-Gaussian arms and for laws on $[0,1]$ respectively. - Prove that their stopping rule is correct for every sampling rule under the condition on the exploration rate of [KTAS12, Theorem 1]. + - Prove that the stopping rule of KL-LUCB is correct for every sampling rule with the + exploration rate $\log(k_1Kt^\alpha/\delta)+\log\log(k_1Kt^\alpha/\delta)$ and the constants + $\alpha,k_1$ of [KK13, Theorem 1], from the self-normalized deviations of Layer 4.2 + [GC11, Theorem 10]. - Prove $\mathbb E[\tau]<292\,H^{\varepsilon/2}\log(H^{\varepsilon/2}/\delta)+16$ for LUCB1 with $H^\gamma=\sum_a\max(\Delta_a,\gamma)^{-2}$ [KTAS12, Theorem 6]. - Prove the bound of KL-LUCB in terms of the Chernoff-information complexity $H^*_\varepsilon$ @@ -531,23 +935,35 @@ Generalization: arbitrary tasks, where [GK16] treats best arm identification. ## Layer 8: Fixed-budget identification -1. **Successive rejects** [ABM10]. Prove +Rewards in $[0,1]$ and σ²-sub-Gaussian rewards are the restricted tasks of Layer 1.1, as in +Layer 7. + +1. **Successive rejects** [ABM10]. Define successive rejects as a phased-elimination algorithm + (Layer 0.5) and prove $P(\text{error})\le\frac{K(K-1)}2\exp\!\big(-\frac{T-K}{\overline{\log}(K)H_2}\big)$ for rewards in $[0,1]$, with $\overline{\log}(K)=\frac12+\sum_{i=2}^K\frac1i$, $\Delta_{(1)}\le\dots\le \Delta_{(K)}$ the gaps in increasing order with $\Delta_{(1)}=\Delta_{(2)}$, and $H_2=\max_ii\,\Delta_{(i)}^{-2}$ [ABM10]. Prove $H_2\le H_1\le\overline{\log}(2K)H_2$ for $H_1=\sum_i\Delta_{(i)}^{-2}$. -2. **Sequential halving** [KKS13]. Prove +2. **Sequential halving** [KKS13]. Define sequential halving as a phased-elimination algorithm + (Layer 0.5) and prove $P(\text{error})\le3\log_2K\exp\!\big(-\frac{T}{8H_2\log_2K}\big)$ [KKS13] for rewards in $[0,1]$ ([LS, Theorem 33.10] proves it for 1-sub-Gaussian rewards with $16$ in place of $8$; state the σ²-sub-Gaussian version). 3. **Large deviations under static allocations.** - - For independent samples of exponential-family arms with fixed proportions $w$, prove the - large deviation upper and lower bounds for the vector of empirical means (Cramér's theorem - for each arm, from the Cramér–Chernoff bound and an exponential tilting lower bound). - - Deduce that the static-proportions algorithm recommending $i^*(\hat\mu)$ has error - exponent $\inf_{\lambda\in\neg i^*(\mu)}\sum_aw_a\,d(\lambda_a,\mu_a)$ (alternative first) - [GJ04; D23, Theorems 1, 12]. + - For independent samples with fixed proportions $w$ of arms with any laws on `ℝ` whose + cumulant generating function is finite on a neighbourhood of $0$, prove the large deviation + upper and lower bounds for the vector of empirical means, with the rate functions $I_a$ of + Layer 1.2: Cramér's theorem for each arm [DZ98, Theorem 2.2.3], the upper bound from the + Cramér–Chernoff bound and the lower bound by exponential tilting at the levels that are means + of the exponential family generated by the law and by truncation at the other levels of + finite rate, and independence across the arms. + - Deduce that the static-proportions algorithm recommending $i^*(\hat\mu)$, for a task asking + about the means (Layer 1.1), has error exponent the infimum of $\sum_aw_a\,I_a(x_a)$ over the + vectors of means $x$ for which $i^*(\mu)$ is not correct [GJ04]. For exponential-family arms, + $I_a(x)=d_a(x,\mu_a)$ on the means, and the exponent is + $\inf_{\lambda\in\neg i^*(\mu)}\sum_aw_a\,d(\lambda_a,\mu_a)$ (alternative first) + [D23, Theorems 1, 12]. - For two arms, deduce that the best static exponent is the Chernoff information $d(z,\mu_1)=d(z,\mu_2)$, and prove the matching lower bound for consistent algorithms [KCG16, Theorems 12–13]. @@ -568,20 +984,28 @@ Generalization: arbitrary tasks, where [GK16] treats best arm identification. ## Layer 9: Linear identification 1. **Linear tasks.** For a finite-dimensional real inner product space `E`, features - `φ : α → E`, a finite set `𝒵` of answers in `E` and noise σ²-sub-Gaussian or Gaussian, define - the linear model $\theta\in E$ with arm means $\langle\varphi(a),\theta\rangle$ and the - transductive best-answer task $\operatorname{argmax}_{z\in\mathcal Z}\langle z,\theta\rangle$ - [FJJR19]; best arm identification is the case $\mathcal Z=\varphi(\alpha)$. -2. **Characteristic time.** For Gaussian noise, prove + `φ : α → E` and noise σ²-sub-Gaussian or Gaussian, the linear model has models $\theta\in E$ + and mean functional $\theta\mapsto(\langle\varphi(a),\theta\rangle)_a$. Linear best arm + identification, thresholding and the other tasks of Layer 1.1 are the tasks of Layer 1.1 for + this mean functional, the pullbacks of the unstructured tasks along it when the noise law + depends on the mean only; make no separate definitions. For a finite set `𝒵` of answers in + `E`, define the transductive best-answer task + $\operatorname{argmax}_{z\in\mathcal Z}\langle z,\theta\rangle$ [FJJR19]; best arm + identification is the case $\mathcal Z=\varphi(\alpha)$. +2. **Characteristic time.** For Gaussian noise with known variances $\sigma_a^2$, prove $T^*(\theta)^{-1}=\max_{w\in\Delta_K}\min_{z\ne z^*} - \frac{\langle\theta,z^*-z\rangle^2}{2\sigma^2\|z^*-z\|^2_{V_w^{-1}}}$ with - $V_w=\sum_aw_a\varphi(a)\varphi(a)^\top$ (the Bandits roadmap's `designOperator`), with the - pseudo-inverse convention when $V_w$ is singular, equivalently - $\max_w\inf_{\lambda\in\neg z^*}\frac1{2\sigma^2}\|\theta-\lambda\|^2_{V_w}$ - [FJJR19, Theorem 1; DMSV20; JP20]. Compare it with the G-optimal and $\mathcal X\mathcal Y$ - allocations of [SLM14]. + \frac{\langle\theta,z^*-z\rangle^2}{2\|z^*-z\|^2_{V_w^{-1}}}$ with + $V_w=\sum_aw_a\sigma_a^{-2}\varphi(a)\otimes\varphi(a)$ and the convention of Layer 3.6 for + $\|\cdot\|^2_{V_w^{-1}}$, equivalently + $\max_w\inf_{\lambda\in\neg z^*}\frac12\|\theta-\lambda\|^2_{V_w}$ + [FJJR19, Theorem 1; DMSV20; JP20], as the case of the half-spaces + $\{\lambda:\langle z^*-z,\lambda\rangle\le0\}$ of Layer 3.6; for a common variance $\sigma^2$ + this is the form $\langle\theta,z^*-z\rangle^2/(2\sigma^2\|z^*-z\|^2_{V_w^{-1}})$ with + $V_w=\sum_aw_a\,\varphi(a)\otimes\varphi(a)$. Compare it with the G-optimal and + $\mathcal X\mathcal Y$ allocations of [SLM14]. 3. **Elimination with optimal designs.** Define RAGE (phased elimination with - $\mathcal X\mathcal Y$-optimal designs and rounding) and prove that it is $\delta$-PAC with + $\mathcal X\mathcal Y$-optimal designs and rounding) as a phased-elimination algorithm on the + active answers (Layer 0.5) and prove that it is $\delta$-PAC with sample complexity $O\big(\psi^*\log(1/\Delta_{\min})\log(|\mathcal Z|^2\log^2(1/\Delta_{\min})/\delta)\big)$, $\psi^*=2\sigma^2T^*(\theta)$ [FJJR19, Theorem 2]. Build the rounding of designs it uses. 4. **GLRT and asymptotically optimal algorithms.** @@ -604,7 +1028,22 @@ all runs. Check in particular: common tasks, and $T^*_{1/2}\le2T^*$ (Layer 3.5) bounds the loss of Top Two. - **Generality of the general statements:** the GLRT $\delta$-correctness theorem of Layer 4.3 applies to best arm identification, top-$m$, thresholding and Any Low Arm (Layer 1.1) without - task-specific proofs. + task-specific proofs, and the continuity theorem of Layer 3.3 discharges the continuity + hypotheses of Sticky Track-and-Stop (Layer 5.3) for Any Low Arm with exponential-family arms. +- **Mean functionals:** with `Θ = α → ℝ` and `mean = id`, the tasks of Layer 1.1 are LMLExplore's + tasks on vectors of means; the guarantees of successive elimination, median elimination and + LUCB (Layer 7) quantify over every σ²-sub-Gaussian bandit, with no auxiliary bandit; best arm + identification with unknown variances is `baiTask` for the two-parameter Gaussian model. +- **Vector families:** the Bregman form of Layer 1.3 for the two-parameter Gaussian family + recovers `klDiv_gaussianReal_gaussianReal`. +- **Rate function:** for Bernoulli arms $\bar d(1,\mu)=\log(1/\mu)$, and for Gaussian arms + $\bar d=d$ on $\mathbb R^2$; the Chernoff bound of Layer 1.2 at the level $1$ gives + $P(\hat\mu_n=1)\le\mu^n$ for Bernoulli arms. +- **Stopping times:** the chain rule of Layer 2.1 applied to one algorithm and two stationary + bandits gives `klDiv_stoppedHistMeasure_le`; Wald's identity of Layer 0.3 for a stationary + environment gives `IsAlgEnvSeq.integral_sum_feedback_eq_sum_integral_pullCount_mul`. +- **Phased elimination:** successive elimination, median elimination, successive rejects, + sequential halving and RAGE are all built with the constructor of Layer 0.5. - **Fixed budget:** the fixed-budget lower bound of Layer 8.4 and the upper bounds of Layers 8.1–8.2 agree up to the $\log K$ factors stated. @@ -615,10 +1054,22 @@ theorems or the completion of these milestones. T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press (2020), Chapter 33, is the textbook account [LS] (Theorem 33.5 for the lower bound, Theorem 33.6 for -Track-and-Stop, Lemmas 33.7–33.8 for GLR thresholds, Theorem 33.10 for sequential halving). +Track-and-Stop, Lemmas 33.7–33.8 for GLR thresholds, Theorem 33.10 for sequential halving), and +Section 4.6 describes the stack-of-rewards model. - [ABM10] J.-Y. Audibert, S. Bubeck and R. Munos, *Best arm identification in multi-armed bandits*, COLT 2010. +- [AJG20] S. Agrawal, S. Juneja and P. Glynn, *Optimal δ-correct best-arm selection for + heavy-tailed distributions*, ALT 2020. +- [BLM13] S. Boucheron, G. Lugosi and P. Massart, *Concentration Inequalities*, Oxford University + Press (2013), Section 2.2 (the Cramér–Chernoff method). +- [BMDG05] A. Banerjee, S. Merugu, I. S. Dhillon and J. Ghosh, *Clustering with Bregman + divergences*, JMLR 6 (2005), for the relative entropy of exponential families as a Bregman + divergence. +- [BN78] O. Barndorff-Nielsen, *Information and Exponential Families in Statistical Theory*, Wiley + (1978). +- [Bro86] L. D. Brown, *Fundamentals of Statistical Exponential Families*, IMS Lecture Notes 9 + (1986), Chapter 1. - [C59] H. Chernoff, *Sequential design of experiments*, Ann. Math. Statist. 30 (1959), the origin of the GLR stopping rule and of the game that defines the characteristic time. - [CL16] A. Carpentier and A. Locatelli, *Tight (lower) bounds for the fixed budget best arm @@ -631,6 +1082,8 @@ Track-and-Stop, Lemmas 33.7–33.8 for GLR thresholds, Theorem 33.10 for sequent games*, NeurIPS 2019. - [DMSV20] R. Degenne, P. Ménard, X. Shang and M. Valko, *Gamification of pure exploration for linear bandits*, ICML 2020. +- [DZ98] A. Dembo and O. Zeitouni, *Large Deviations Techniques and Applications*, 2nd ed., + Springer (1998), Section 2.2 (Cramér's theorem). - [dRvEGK14] S. de Rooij, T. van Erven, P. D. Grünwald and W. M. Koolen, *Follow the leader if you can, hedge if you must*, JMLR 15 (2014). - [EMM02] E. Even-Dar, S. Mannor and Y. Mansour, *PAC bounds for multi-armed bandit and Markov @@ -639,12 +1092,18 @@ Track-and-Stop, Lemmas 33.7–33.8 for GLR thresholds, Theorem 33.10 for sequent the multi-armed bandit and reinforcement learning problems*, JMLR 7 (2006). - [FJJR19] T. Fiez, L. Jain, K. Jamieson and L. Ratliff, *Sequential experimental design for transductive linear bandits*, NeurIPS 2019. +- [FKV14] E. A. Feinberg, P. O. Kasyanov and M. Voorneveld, *Berge's maximum theorem for + noncompact image sets*, J. Math. Anal. Appl. 413 (2014). +- [GC11] A. Garivier and O. Cappé, *The KL-UCB algorithm for bounded stochastic bandits and + beyond*, COLT 2011. - [GMS19] A. Garivier, P. Ménard and G. Stoltz, *Explore first, exploit next: the true shape of regret in bandit problems*, Math. Oper. Res. 44 (2019). - [GJ04] P. Glynn and S. Juneja, *A large deviations perspective on ordinal optimization*, Winter Simulation Conference 2004. - [GK16] A. Garivier and E. Kaufmann, *Optimal best arm identification with fixed confidence*, COLT 2016. +- [HRMS20] S. R. Howard, A. Ramdas, J. McAuliffe and J. Sekhon, *Time-uniform Chernoff bounds via + nonnegative supermartingales*, Probability Surveys 17 (2020). - [JD23] M. Jourdan and R. Degenne, *Non-asymptotic analysis of a UCB-based top two algorithm*, NeurIPS 2023. - [JDBdHK22] M. Jourdan, R. Degenne, D. Baudry, R. de Heide and E. Kaufmann, *Top two algorithms @@ -677,5 +1136,7 @@ Track-and-Stop, Lemmas 33.7–33.8 for GLR thresholds, Theorem 33.10 for sequent guarantees for Bayesian best-arm identification*, AISTATS 2020. - [SLM14] M. Soare, A. Lazaric and R. Munos, *Best-arm identification in linear bandits*, NeurIPS 2014. +- [WJ08] M. J. Wainwright and M. I. Jordan, *Graphical models, exponential families, and + variational inference*, Foundations and Trends in Machine Learning 1 (2008), Section 3. - [WTP21] P.-A. Wang, R.-C. Tzeng and A. Proutière, *Fast pure exploration via Frank–Wolfe*, NeurIPS 2021. diff --git a/LMLRoadmaps/Identification/Suggested.lean b/LMLRoadmaps/Identification/Suggested.lean index 9dff7a9..ac045c1 100644 --- a/LMLRoadmaps/Identification/Suggested.lean +++ b/LMLRoadmaps/Identification/Suggested.lean @@ -1,10 +1,21 @@ +import Mathlib.Analysis.InnerProductSpace.Basic import Mathlib.InformationTheory.KullbackLeibler.Basic +import Mathlib.MeasureTheory.Measure.ProbabilityMeasure import Mathlib.MeasureTheory.Measure.Tilted +import Mathlib.Probability.Martingale.Basic import Mathlib.Probability.Moments.MGFAnalytic +import Mathlib.Probability.Moments.SubGaussian +import Mathlib.Probability.Process.Stopping +import TauCeti.Analysis.Convex.Conjugate +import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic +import LeanMachineLearning.Online.Bandit.ArrayProbSpace +import LeanMachineLearning.SequentialLearning.Comap import LeanMachineLearning.SequentialLearning.FiniteActions import LeanMachineLearning.SequentialLearning.IdentificationAlg import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace +import LeanMachineLearning.SequentialLearning.Means import LeanMachineLearning.SequentialLearning.StationaryEnv +import LeanMachineLearning.SequentialLearning.SumRewards /-! # Bandit identification: suggested target signatures @@ -12,8 +23,8 @@ import LeanMachineLearning.SequentialLearning.StationaryEnv **This file is not the roadmap and is not exhaustive.** The definitive document is `README.md`. The statements here suggest Lean forms for particular milestones, so that contributors and reviewers converge on names and signatures; discharging all of them finishes neither a milestone -nor the roadmap. The admitted proofs are targets, not claimed implementations. The algorithms are -admitted definitions: constructing them as identification algorithms, with their run lemmas, is a +nor the roadmap. The admitted proofs are targets, not claimed implementations. The algorithms and +the helper `armObs` are admitted definitions: constructing them, with their run lemmas, is a target, and their docstrings and the README specify them. The names of the LML framework (`IdentAlg`, `stationaryEnv`, `stoppedHistMeasure`, ...) are those @@ -45,7 +56,21 @@ def histOutputMeasure (A : IdentAlg Unit α 𝓨 ℐ) (env : Environment Unit α def expectedStoppingTime (A : IdentAlg Unit α 𝓨 ℐ) (env : Environment Unit α 𝓨) : ℝ≥0∞ := ∫⁻ ω, (A.stoppingTime IT.obs IT.action IT.feedback ω : ℝ≥0∞) ∂(trajMeasure A.alg env) -/-! ## Layer 1: identification tasks and exponential families -/ +/-- **Wald's identity for the feedback**, for every environment (README Layer 0.3): for a stopping +time `τ` of the filtration of the actions with `E[τ] < ∞`, and conditional absolute means of the +feedback bounded by `C`, `E[∑_{t < τ} Y t] = E[∑_{t < τ} m_t(A t)]` with LML's conditional means +`env.means`. -/ +theorem integral_sum_feedback_eq_integral_sum_means {Ω 𝓞 𝓐 : Type*} [MeasurableSpace Ω] + [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] {P : Measure Ω} [IsProbabilityMeasure P] + {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → ℝ} {alg : Algorithm 𝓞 𝓐 ℝ} + {env : Environment 𝓞 𝓐 ℝ} (h : IsAlgEnvSeq O A Y alg env P) {τ : Ω → ℕ∞} + (hτ : IsStoppingTime h.filtrationAction τ) (hτ_int : ∫⁻ ω, (τ ω : ℝ≥0∞) ∂P ≠ ∞) {C : ℝ} + (hC : ∀ n, ∀ᵐ ω ∂P, ∫ y, |y| ∂(env.measure O A Y n ω (A n ω)) ≤ C) : + ∫ ω, ∑ t ∈ range (τ ω).toNat, Y t ω ∂P = + ∫ ω, ∑ t ∈ range (τ ω).toNat, env.means O A Y (A t ω) t ω ∂P := + sorry + +/-! ## Layer 1: identification tasks, exponential families and product models -/ /-- An identification task (README Conventions): models `Θ` with a bandit `ν θ` each, the admissible models `M` and the set `correct θ` of correct answers of each model. -/ @@ -81,6 +106,19 @@ def IsDeltaPAC (A : IdentAlg Unit α 𝓨 ℐ) (δ : ℝ) : Prop := ∀ᵐ ω ∂(trajMeasure A.alg (stationaryEnv (task.ν θ))), A.stoppingTime IT.obs IT.action IT.feedback ω ≠ ⊤ +/-- The pullback of a task along `f : Θ' → Θ` (README Layer 1.1): the bandit, the admissibility +and the correct answers of `θ'` are those of `f θ'`. -/ +def comap {Θ' : Type*} (f : Θ' → Θ) : IdentTask α Θ' ℐ 𝓨 where + M := f ⁻¹' task.M + ν := task.ν ∘ f + isMarkovKernel_ν θ' := task.isMarkovKernel_ν (f θ') + correct := task.correct ∘ f + +/-- A `δ`-correct algorithm for a task is `δ`-correct for its pullbacks (README Layer 1.1). -/ +theorem IsDeltaCorrect.comap {A : IdentAlg Unit α 𝓨 ℐ} {δ : ℝ} (h : task.IsDeltaCorrect A δ) + {Θ' : Type*} (f : Θ' → Θ) : (task.comap f).IsDeltaCorrect A δ := + sorry + /-! ### The pure exploration game (Layer 3) -/ /-- The transportation cost `∑ a, w a KL(ν_a(θ), ν_a(θ'))` from `θ` to `θ'` with allocation `w`. -/ @@ -111,17 +149,68 @@ theorem concaveOn_altCost (θ : Θ) (i : ℐ) : ConcaveOn ℝ≥0 (simplex α) (fun w ↦ task.altCost θ w i) := sorry +/-- Pulling a task back can only make the alternatives more expensive (README Layer 3.1). -/ +theorem altCost_le_altCost_comap {Θ' : Type*} (f : Θ' → Θ) (θ' : Θ') (w : α → ℝ) (i : ℐ) : + task.altCost (f θ') w i ≤ (task.comap f).altCost θ' w i := + sorry + end IdentTask -/-- Best arm identification on vectors of means with a unique best arm, for arm laws `κ a x` of -mean `x` in the set `meanSet a` (README Layer 1.1). Ties have no correct answer; the admissible -models have exactly one. -/ -def baiTask (κ : α → ℝ → Measure ℝ) [∀ a x, IsProbabilityMeasure (κ a x)] - (meanSet : α → Set ℝ) : IdentTask α (α → ℝ) α ℝ where - M := {μ | (∀ a, μ a ∈ meanSet a) ∧ ∃ a, ∀ b ≠ a, μ b < μ a} - ν μ := Kernel.ofFunOfCountable fun a ↦ κ a (μ a) - isMarkovKernel_ν μ := ⟨fun a ↦ (inferInstance : IsProbabilityMeasure (κ a (μ a)))⟩ - correct μ := {a | ∀ b ≠ a, μ b < μ a} +/-- Best arm identification for models `Θ` with bandits `ν` and mean functional `mean` +(README Layer 1.1): the correct answer of `θ` is the arm with the largest mean `mean θ a`, and the +admissible models are those where it is unique. The task on vectors of means is +`Θ = α → ℝ`, `mean = id`. -/ +def baiTask (ν : Θ → Kernel α 𝓨) [∀ θ, IsMarkovKernel (ν θ)] (mean : Θ → α → ℝ) : + IdentTask α Θ α 𝓨 where + M := {θ | ∃ a, ∀ b ≠ a, mean θ b < mean θ a} + ν := ν + isMarkovKernel_ν _ := inferInstance + correct θ := {a | ∀ b ≠ a, mean θ b < mean θ a} + +/-- The bandit of a product model (README Layer 1.4): arm `a` of the model `θ : α → Θ₀` has law +`κ a (θ a)`. -/ +def productBandit {Θ₀ : Type*} (κ : α → Θ₀ → Measure 𝓨) (θ : α → Θ₀) : Kernel α 𝓨 := + Kernel.ofFunOfCountable fun a ↦ κ a (θ a) + +instance {Θ₀ : Type*} (κ : α → Θ₀ → Measure 𝓨) [∀ a x, IsProbabilityMeasure (κ a x)] + (θ : α → Θ₀) : IsMarkovKernel (productBandit κ θ) := + ⟨fun a ↦ (inferInstance : IsProbabilityMeasure (κ a (θ a)))⟩ + +/-- Best arm identification on the model of all bandits with σ²-sub-Gaussian real observations +(README Layer 1.1): a model is the vector of the arm laws, and its mean functional their means. +The guarantees of the elimination algorithms (README Layer 7) are stated on this task. -/ +def subgaussianBaiTask (σ2 : ℝ≥0) : IdentTask α (α → ProbabilityMeasure ℝ) α ℝ where + M := (baiTask (productBandit fun _ (P : ProbabilityMeasure ℝ) ↦ (P : Measure ℝ)) + (fun θ a ↦ ∫ x, x ∂(θ a : Measure ℝ))).M ∩ + {θ | ∀ a, HasSubgaussianMGF (fun x ↦ x - ∫ y, y ∂(θ a : Measure ℝ)) σ2 (θ a : Measure ℝ)} + ν := productBandit fun _ (P : ProbabilityMeasure ℝ) ↦ (P : Measure ℝ) + isMarkovKernel_ν _ := inferInstance + correct θ := {a | ∀ b ≠ a, ∫ x, x ∂(θ b : Measure ℝ) < ∫ x, x ∂(θ a : Measure ℝ)} + +/-- `K⁻(x, u)`: the smallest divergence from `κ x` to a law `κ y`, `y ∈ S`, of mean `m y ≤ u` +(README Layer 1.4). -/ +def kInfLower {Θ₀ : Type*} (κ : Θ₀ → Measure 𝓨) (S : Set Θ₀) (m : Θ₀ → ℝ) (x : Θ₀) (u : ℝ) : + ℝ≥0∞ := + ⨅ y ∈ {y ∈ S | m y ≤ u}, klDiv (κ x) (κ y) + +/-- `K⁺(x, u)`: the smallest divergence from `κ x` to a law `κ y`, `y ∈ S`, of mean `m y ≥ u` +(README Layer 1.4). -/ +def kInfUpper {Θ₀ : Type*} (κ : Θ₀ → Measure 𝓨) (S : Set Θ₀) (m : Θ₀ → ℝ) (x : Θ₀) (u : ℝ) : + ℝ≥0∞ := + ⨅ y ∈ {y ∈ S | u ≤ m y}, klDiv (κ x) (κ y) + +/-- The cost of the alternatives of best arm identification on a product model, for a positive +allocation [AJG20; JDK23a, (1)] (README Layer 1.4): the infimum over the models where some arm +`b ≠ a` is at least as good as `a` is `min_{b ≠ a} inf_u (w a K⁻_a(θ a, u) + w b K⁺_b(θ b, u))`. -/ +theorem iInf_cost_baiTask_productBandit {Θ₀ : Type*} (κ : α → Θ₀ → Measure 𝓨) + [∀ a x, IsProbabilityMeasure (κ a x)] (S : α → Set Θ₀) (m : α → Θ₀ → ℝ) {θ : α → Θ₀} + (hθ : ∀ c, θ c ∈ S c) {w : α → ℝ} (hw : ∀ c, 0 < w c) (a : α) : + ⨅ θ' ∈ {θ' : α → Θ₀ | (∀ c, θ' c ∈ S c) ∧ ∃ b ≠ a, m a (θ' a) ≤ m b (θ' b)}, + (baiTask (productBandit κ) fun θ c ↦ m c (θ c)).cost w θ θ' = + ⨅ (b) (_ : b ≠ a), ⨅ u : ℝ, + (ENNReal.ofReal (w a) * kInfLower (κ a) (S a) (m a) (θ a) u + + ENNReal.ofReal (w b) * kInfUpper (κ b) (S b) (m b) (θ b) u) := + sorry /-- The exponential family of a measure `ρ` on `𝓧` with statistic `T`: the tilt of `ρ` with natural parameter `η` (README Layer 1.2). The natural exponential families of measures on `ℝ` @@ -139,8 +228,75 @@ theorem klDiv_expFamily {𝓧 : Type*} [MeasurableSpace 𝓧] (ρ : Measure 𝓧 ENNReal.ofReal (cgf T ρ η' - cgf T ρ η - deriv (cgf T ρ) η * (η' - η)) := sorry +/-- The Cramér rate function `I_X(x) = sup_t (t x - Λ_X(t))` of a real random variable `X` under +`P`, in `ℝ≥0∞` (README Layer 1.2). For the statistic of an exponential family under its member of +mean `μ`, it is the divergence `d(x, μ)` on the means and its generalized likelihood ratio +extension `d̄(x, μ)` elsewhere. -/ +def rateFunction {Ω : Type*} [MeasurableSpace Ω] (X : Ω → ℝ) (P : Measure Ω) (x : ℝ) : ℝ≥0∞ := + ⨆ t ∈ integrableExpSet X P, ENNReal.ofReal (t * x - cgf X P t) + +open Classical in +/-- The rate function is Tau Ceti's Fenchel conjugate, for the pairing `(t, x) ↦ t * x`, of the +cumulant generating function extended by `⊤` outside `integrableExpSet X P`. -/ +theorem coe_rateFunction_eq_fenchelConjugate {Ω : Type*} [MeasurableSpace Ω] (X : Ω → ℝ) + (P : Measure Ω) [IsProbabilityMeasure P] (x : ℝ) : + (rateFunction X P x : EReal) = TauCeti.fenchelConjugate (LinearMap.mul ℝ ℝ) + (fun t ↦ if t ∈ integrableExpSet X P then (cgf X P t : EReal) else ⊤) x := + sorry + +/-! ## Layer 1.3: exponential families with a vector statistic -/ + +section VectorStatistic + +variable {𝓧 E : Type*} [MeasurableSpace 𝓧] [NormedAddCommGroup E] [InnerProductSpace ℝ E] + [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] + +/-- The member of natural parameter `η` of the exponential family of `ρ` with a statistic `T` in +a finite-dimensional inner product space (README Layer 1.3). -/ +def vecExpFamily (ρ : Measure 𝓧) (T : 𝓧 → E) (η : E) : Measure 𝓧 := + ρ.tilted (fun x ↦ inner ℝ η (T x)) + +/-- The log-partition function `ψ(η) = log ∫ exp ⟪η, T⟫ dρ`. -/ +def vecLogPartition (ρ : Measure 𝓧) (T : 𝓧 → E) (η : E) : ℝ := + log (∫ x, exp (inner ℝ η (T x)) ∂ρ) + +/-- The relative entropy between two members of a vector exponential family is the Bregman +divergence of the log-partition function [BMDG05] (README Layer 1.3). -/ +theorem klDiv_vecExpFamily (ρ : Measure 𝓧) [IsProbabilityMeasure ρ] {T : 𝓧 → E} + (hT : Measurable T) {η η' : E} + (hη : η ∈ interior {η | Integrable (fun x ↦ exp (inner ℝ η (T x))) ρ}) + (hη' : η' ∈ interior {η | Integrable (fun x ↦ exp (inner ℝ η (T x))) ρ}) : + klDiv (vecExpFamily ρ T η) (vecExpFamily ρ T η') = + ENNReal.ofReal (bregDiv (vecLogPartition ρ T) η' η (fderiv ℝ (vecLogPartition ρ T) η)) := + sorry + +end VectorStatistic + /-! ## Layer 2: change of measure and lower bounds -/ +/-- The `t`-round histories along which the stopping rule `S` has not stopped: none of their +prefixes belongs to `S` (LMLExplore's `notStoppedSet`). -/ +def notStoppedSet {𝓞 𝓐 : Type*} (S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)) (t : ℕ) : + Set (Hist 𝓞 𝓐 𝓨 t) := + {h | ∀ m (hm : m ≤ t), (⟨m, fun i ↦ h (Fin.castLE hm i)⟩ : Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n) ∉ S} + +/-- **Chain rule at a stopping time** [GMS19; KCG16, Lemma 1] (README Layer 2.1), for any two +algorithm-environment pairs: the divergence between the laws of the stopped histories is at most +the sum over the rounds of the divergences of the step kernels at the histories not yet stopped. +Equality holds when the hitting time is also almost surely finite under the second pair. -/ +theorem klDiv_stoppedHistMeasure_le_tsum {𝓞 𝓐 : Type*} [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] + (alg alg' : Algorithm 𝓞 𝓐 𝓨) (env env' : Environment 𝓞 𝓐 𝓨) + {S : Set (Σ n : ℕ, Hist 𝓞 𝓐 𝓨 n)} (hS : MeasurableSet S) + (hτ : ∀ᵐ ω ∂(trajMeasure alg env), + hittingAfter (sigmaHistory IT.obs IT.action IT.feedback) S 0 ω ≠ ⊤) : + klDiv (stoppedHistMeasure alg env S) (stoppedHistMeasure alg' env' S) ≤ + ∑' t, klDiv + (((trajMeasure alg env).map (history IT.obs IT.action IT.feedback t)).restrict + (notStoppedSet S t) ⊗ₘ stepKernel alg env t) + (((trajMeasure alg env).map (history IT.obs IT.action IT.feedback t)).restrict + (notStoppedSet S t) ⊗ₘ stepKernel alg' env' t) := + sorry + /-- **Transportation lemma** [KCG16, Lemma 1], for an identification algorithm run against two stationary bandits: for every event `E` of the stopped history and the output, the expected transportation cost bounds the binary relative entropy of the probabilities of `E`. The binary @@ -157,7 +313,7 @@ theorem klDiv_bernoulli_le_sum_lintegral_pullCount [MeasurableSpace.CountablyGen sorry /-- **Lower bound on the sample complexity** [GK16, Theorem 1]: for a `δ`-correct algorithm with -`δ ≤ 1/2` and an admissible model with a single correct answer, +`δ ≤ 1/2` and an admissible model with a single correct answer, in any task, `E[τ] ≥ T*(θ) kl(δ, 1 - δ)`. -/ theorem charTime_mul_le_expectedStoppingTime [MeasurableSpace.CountablyGenerated 𝓨] [MeasurableSingletonClass ℐ] (task : IdentTask α Θ ℐ 𝓨) (A : IdentAlg Unit α 𝓨 ℐ) {δ : ℝ} @@ -167,27 +323,147 @@ theorem charTime_mul_le_expectedStoppingTime [MeasurableSpace.CountablyGenerated expectedStoppingTime A (stationaryEnv (task.ν θ)) := sorry +/-! ## Layer 3: continuity on product models -/ + +/-- **Continuity of the cost of any set of alternatives on a product model** (README Layer 3.3, +[DK19, Theorem 23, Lemmas 24–27]): if the per-arm divergences are finite and continuous on +`S a ×ˢ S a`, and their sublevel sets in the second argument are locally uniformly contained in +compact subsets of `S a`, then `(θ, w) ↦ inf_{θ' ∈ A} cost_θ(w, θ')` is continuous on the models +of `∏ a, S a` and the nonnegative allocations, for every set `A` of alternatives. -/ +theorem continuousOn_iInf_cost_productBandit {Θ₀ : Type*} [TopologicalSpace Θ₀] + (κ : α → Θ₀ → Measure 𝓨) [∀ a x, IsProbabilityMeasure (κ a x)] (S : α → Set Θ₀) + (hfin : ∀ a, ∀ x ∈ S a, ∀ y ∈ S a, klDiv (κ a x) (κ a y) ≠ ∞) + (hcont : ∀ a, ContinuousOn (fun p : Θ₀ × Θ₀ ↦ klDiv (κ a p.1) (κ a p.2)) (S a ×ˢ S a)) + (hcomp : ∀ a, ∀ x ∈ S a, ∃ U ∈ 𝓝[S a] x, ∀ r : ℝ≥0∞, r ≠ ∞ → + ∃ K, IsCompact K ∧ K ⊆ S a ∧ {y ∈ S a | ∃ x' ∈ U, klDiv (κ a x') (κ a y) ≤ r} ⊆ K) + (A : Set (α → Θ₀)) (hA : A ⊆ Set.univ.pi S) : + ContinuousOn (fun p : (α → Θ₀) × (α → ℝ) ↦ + ⨅ θ' ∈ A, ∑ a, ENNReal.ofReal (p.2 a) * klDiv (κ a (p.1 a)) (κ a (θ' a))) + (Set.univ.pi S ×ˢ {w | 0 ≤ w}) := + sorry + +/-! ## Layer 4: the per-arm streams, conditional domination and GLR stopping rules -/ + +/-- The observations of arm `a` before round `t`, in the order of the pulls (README Layer 4.1). -/ +def armObs {Ω : Type*} (A : ℕ → Ω → α) (Y : ℕ → Ω → 𝓨) (a : α) (t : ℕ) (ω : Ω) : + Fin (pullCount A a t ω) → 𝓨 := + sorry + +/-- **Event transfer to the per-arm streams** (README Layer 4.1): in a run of any algorithm +against a stationary bandit with observations in any measurable space, the probability that a +property `q` of the pull counts and of the observations of each arm so far holds at some round is +at most the probability that it holds for some numbers of pulls in the stream model. -/ +theorem measure_exists_armObs_le_streamMeasure {Ω : Type*} [MeasurableSpace Ω] + {P : Measure Ω} [IsProbabilityMeasure P] {O : ℕ → Ω → Unit} {A : ℕ → Ω → α} + {Y : ℕ → Ω → 𝓨} {alg : Algorithm Unit α 𝓨} {ν : Kernel α 𝓨} [IsMarkovKernel ν] + (h : IsAlgEnvSeq O A Y alg (stationaryEnv ν) P) + (q : (s : α → ℕ) → ((a : α) → Fin (s a) → 𝓨) → Prop) : + P {ω | ∃ t, q (fun a ↦ pullCount A a t ω) (fun a ↦ armObs A Y a t ω)} ≤ + Bandits.streamMeasure ν {x | ∃ s : α → ℕ, q s (fun a i ↦ x i a)} := + sorry + +section CondDomination + +variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} + +/-- The moment generating function of `X` under the kernel `κ` is bounded by `exp ψ` on `Λ`, +`ν`-almost everywhere (README Layer 4.2), in the pattern of Mathlib's `Kernel.HasSubgaussianMGF`. -/ +structure Kernel.HasCGFBound (X : Ω → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ) (κ : Kernel Ω' Ω) + (ν : Measure Ω') : Prop where + integrable_exp_mul : ∀ t ∈ Λ, Integrable (fun ω ↦ exp (t * X ω)) (κ ∘ₘ ν) + mgf_le : ∀ᵐ ω' ∂ν, ∀ t ∈ Λ, mgf X (κ ω') t ≤ exp (ψ t) + +/-- The moment generating function of `X` under `P` is bounded by `exp ψ` on `Λ`. With `ψ` the +cumulant generating function of `Y` under `Q` on `[0, ∞) ∩ integrableExpSet Y Q`, this is +LMLExplore's `MGFDominatedAbove X P Y Q`. -/ +structure HasCGFBound (X : Ω → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ) (P : Measure Ω) : Prop where + integrable_exp_mul : ∀ t ∈ Λ, Integrable (fun ω ↦ exp (t * X ω)) P + mgf_le : ∀ t ∈ Λ, mgf X P t ≤ exp (ψ t) + +/-- The conditional moment generating function of `X` given `m` is bounded by `exp ψ` on `Λ`, +`μ`-almost surely: the kernel version for `condExpKernel μ m`, as for `HasCondSubgaussianMGF`. -/ +def HasCondCGFBound {Ω₀ : Type*} (m : MeasurableSpace Ω₀) {mΩ₀ : MeasurableSpace Ω₀} + (hm : m ≤ mΩ₀) [StandardBorelSpace Ω₀] (X : Ω₀ → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ) + (μ : Measure Ω₀) [IsFiniteMeasure μ] : Prop := + Kernel.HasCGFBound X ψ Λ (condExpKernel μ m) (μ.trim hm) + +/-- Mathlib's conditionally sub-Gaussian random variables are the case `ψ t = c t² / 2`. -/ +theorem hasCondCGFBound_iff_hasCondSubgaussianMGF {Ω₀ : Type*} (m : MeasurableSpace Ω₀) + {mΩ₀ : MeasurableSpace Ω₀} (hm : m ≤ mΩ₀) [StandardBorelSpace Ω₀] (X : Ω₀ → ℝ) (c : ℝ≥0) + (μ : Measure Ω₀) [IsFiniteMeasure μ] : + HasCondCGFBound m hm X (fun t ↦ c * t ^ 2 / 2) Set.univ μ ↔ HasCondSubgaussianMGF m hm X c μ := + sorry + +/-- **Exponential supermartingale** [HRMS20] (README Layer 4.2): if `X n` is conditionally +`ψ`-bounded on `Λ` given `ℱ n` and `B n ∈ ℱ n` are predictable events (for bandits, +`{A n = a}`), then `exp (∑_{k < n, B k} (t X k - ψ t))` is a supermartingale for `t ∈ Λ`. -/ +theorem supermartingale_exp_sum_of_hasCondCGFBound [StandardBorelSpace Ω] {P : Measure Ω} + [IsProbabilityMeasure P] {ℱ : Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} {B : ℕ → Set Ω} + {ψ : ℝ → ℝ} {Λ : Set ℝ} (hX : ∀ n, StronglyMeasurable[ℱ (n + 1)] (X n)) + (hcond : ∀ n, HasCondCGFBound (ℱ n) (ℱ.le n) (X n) ψ Λ P) + (hB : ∀ n, MeasurableSet[ℱ n] (B n)) {t : ℝ} (ht : t ∈ Λ) : + Supermartingale + (fun n ω ↦ exp (∑ k ∈ range n, (B k).indicator (fun ω ↦ t * X k ω - ψ t) ω)) ℱ P := + sorry + +/-- **Cramér–Chernoff bound with the rate function** (README Layer 1.2), at every level above +the mean, for independent variables dominated above by `Y`. -/ +theorem measureReal_sum_ge_le_exp_of_le_rateFunction {P : Measure Ω} [IsProbabilityMeasure P] + {Q : Measure Ω'} [IsProbabilityMeasure Q] {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} (hY : Integrable Y Q) + (h_indep : iIndepFun X P) + (hdom : ∀ i, HasCGFBound (X i) (cgf Y Q) (Set.Ici 0 ∩ integrableExpSet Y Q) P) + (s : Finset ℕ) {x r : ℝ} (hx : ∫ y, Y y ∂Q ≤ x) (hr : ENNReal.ofReal r ≤ rateFunction Y Q x) : + P.real {ω | #s * x ≤ ∑ i ∈ s, X i ω} ≤ exp (-(#s * r)) := + sorry + +end CondDomination + /-! ## Layer 5: Track-and-Stop -/ -/-- Track-and-Stop with C-tracking of the optimal allocation of best arm identification at the -empirical means and the GLRT stopping rule with threshold `β δ` (README Layer 5.2). -/ -def trackAndStop (κ : α → ℝ → Measure ℝ) (meanSet : α → Set ℝ) (β : ℝ → ℕ → ℝ) (δ : ℝ) : - IdentAlg Unit α ℝ α := - sorry - -/-- **Asymptotic optimality of Track-and-Stop** [GK16, Theorem 14], for arms in exponential -families on `ℝ` with the identity statistic and the thresholds `β δ t = log (r t / δ)` with -`r t = O(t)`. -/ -theorem trackAndStop_asymptotic (ρ : α → Measure ℝ) [∀ a, IsProbabilityMeasure (ρ a)] - (κ : α → ℝ → Measure ℝ) [∀ a x, IsProbabilityMeasure (κ a x)] (meanSet : α → Set ℝ) - (hκ : ∀ a, ∀ x ∈ meanSet a, ∃ η ∈ interior (integrableExpSet id (ρ a)), - κ a x = expFamily (ρ a) id η) - (r : ℕ → ℝ) (hr : (r · : ℕ → ℝ) =O[atTop] (fun t ↦ (t : ℝ))) - {μ : α → ℝ} (hμ : μ ∈ (baiTask κ meanSet).M) {c : ℝ≥0} - (hc : (baiTask κ meanSet).charTime μ < c) : +/-- The empirical mean of the statistic `T a` over the observations of arm `a` in the history +`h` (zero if `a` was not pulled). -/ +def empMeanStat (T : α → 𝓨 → ℝ) (n : ℕ) (h : Hist Unit α 𝓨 n) (a : α) : ℝ := + empMean' n (Hist.map id id (T a) h) a + +/-- The generalized likelihood ratio evidence against the vector of means `l` for arms in per-arm +exponential families (README Layer 4.3): `∑ a, N_a d̄_a(μ̂_a, l a)`, where `d̄_a(x, l a)` is the +rate function of `T a` under the arm law `κ a (l a)` (README Layer 1.2). -/ +def expFamilyEvidence (κ : α → ℝ → Measure 𝓨) (T : α → 𝓨 → ℝ) (n : ℕ) (h : Hist Unit α 𝓨 n) + (l : α → ℝ) : ℝ≥0∞ := + ∑ a, (pullCount' n h a : ℝ≥0∞) * rateFunction (T a) (κ a (l a)) (empMeanStat T n h a) + +/-- Track-and-Stop (README Layers 4.3 and 5.2) for a task, an estimator `est n h` of the model, a +target map `w` (a measurable selection of the optimal allocations) and a recommendation `rec`: +C-tracking of `w (est n h)`, and the GLRT that stops after `n` rounds with history `h` when +`inf_{θ' ∈ ¬rec (est n h)} Z n h θ' > β δ n h`, with thresholds depending on the round and the +history, and answers `rec (est n h)`. -/ +def trackAndStop (task : IdentTask α Θ ℐ 𝓨) (est : (n : ℕ) → Hist Unit α 𝓨 n → Θ) + (w : Θ → α → ℝ) (rec : Θ → ℐ) (Z : (n : ℕ) → Hist Unit α 𝓨 n → Θ → ℝ≥0∞) + (β : ℝ → (n : ℕ) → Hist Unit α 𝓨 n → ℝ≥0∞) (δ : ℝ) : IdentAlg Unit α 𝓨 ℐ := + sorry + +/-- **Asymptotic optimality of Track-and-Stop** [GK16, Theorem 14; DK19, Theorem 7], on every +single-answer task whose models are vectors of means of per-arm exponential families `(ρ a, T a)` +on `𝓨`, with the empirical means of the statistics as estimator, the generalized likelihood ratio +evidence, a target map with values in the optimal allocations and the correct answer as +recommendation, for thresholds `β δ n h ≤ log (r n / δ)` with `r n = O(n ^ p)`, whatever the +history: `E[τ_δ] ≤ c log (1 / δ)` for small `δ`, for every `c > T*(μ)`. -/ +theorem trackAndStop_asymptotic (task : IdentTask α (α → ℝ) ℐ 𝓨) (ρ : α → Measure 𝓨) + [∀ a, IsProbabilityMeasure (ρ a)] (T : α → 𝓨 → ℝ) (hT : ∀ a, Measurable (T a)) + (κ : α → ℝ → Measure 𝓨) [∀ a x, IsProbabilityMeasure (κ a x)] (S : α → Set ℝ) + (hκ : ∀ a, ∀ x ∈ S a, ∃ η ∈ interior (integrableExpSet (T a) (ρ a)), + κ a x = expFamily (ρ a) (T a) η ∧ ∫ y, T a y ∂(κ a x) = x) + (hν : task.ν = productBandit κ) (hM : task.M ⊆ Set.univ.pi S) + (hsingle : ∀ θ ∈ task.M, ∃ i, task.correct θ = {i}) + (w : (α → ℝ) → α → ℝ) (hw_meas : Measurable w) (rec : (α → ℝ) → ℐ) + (hw : ∀ θ ∈ task.M, ∀ i ∈ task.correct θ, rec θ = i ∧ w θ ∈ task.optAlloc θ i) + (β : ℝ → (n : ℕ) → Hist Unit α 𝓨 n → ℝ≥0∞) {p : ℝ} (r : ℕ → ℝ) + (hr : r =O[atTop] (fun n ↦ (n : ℝ) ^ p)) + (hβ : ∀ δ n h, β δ n h ≤ ENNReal.ofReal (log (r n / δ))) + {μ : α → ℝ} (hμ : μ ∈ task.M) {c : ℝ≥0} (hc : task.charTime μ < c) : ∀ᶠ δ in 𝓝[>] 0, expectedStoppingTime - (trackAndStop κ meanSet (fun δ t ↦ log (r t / δ)) δ) - (stationaryEnv ((baiTask κ meanSet).ν μ)) ≤ c * ENNReal.ofReal (log (1 / δ)) := + (trackAndStop task (empMeanStat T) w rec (expFamilyEvidence κ T) β δ) + (stationaryEnv (task.ν μ)) ≤ c * ENNReal.ofReal (log (1 / δ)) := sorry end LMLRoadmaps.Identification