1 Setting

An exponential family \((\nu _\theta )_\theta \) on \(\mathbb {R}\), with densities \(\exp (\theta x - b(\theta ))\) with respect to a measure \(\xi \), is parameterized by its means, and \(d(\mu , \mu ')\) is the Kullback–Leibler divergence between its members of means \(\mu \) and \(\mu '\). A bandit model is a vector of means \(\mu = (\mu _1, \dots , \mu _K)\) of arms in the family, and \(\mathcal{S}\) is the set of those with a unique best arm \(a^*(\mu )\). For \(\mu \in \mathcal{S}\), \(\mathrm{Alt}(\mu )\) is the set of models of \(\mathcal{S}\) with another best arm, \(\Sigma _K\) the simplex, and the characteristic time is

\[ T^*(\mu )^{-1} = \sup _{w \in \Sigma _K} \inf _{\lambda \in \mathrm{Alt}(\mu )} \sum _{a=1}^K w_a d(\mu _a, \lambda _a). \]

The maximizers \(w^*(\mu )\) are the optimal allocations. In Lean, \(\mathcal{S}\) is LMLExplore’s best arm identification task restricted to the vectors of means of the family \((\rho , \mathrm{id})\), the arm laws \(\nu \) being its members. A strategy is an identification algorithm (sampling rule, stopping rule, recommendation); it is \(\delta \)-PAC if on every \(\mu \in \mathcal{S}\) it stops almost surely and recommends \(a^*(\mu )\) with probability at least \(1 - \delta \).