Bandit Algorithms

Motivation

A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.

Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than $n^{-1/2}$. Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to $M$ types with one inventory constraint.

Setting

There are $M\ge1$ consumer types, a season $[0,T]$ and an inventory $c$. When the firm charges price $p$ to type $m$, type-$m$ consumers arrive at rate $d_m(p)$. Prices range over $[0,p_\infty]$, where $p_\infty$ is a choke price with $d_m(p_\infty)=0$. Assumption 1 asks that each $d_m$ be strictly decreasing, bounded and Lipschitz, and that the revenue rate $r_m(\lambda)=\lambda d_m^{-1}(\lambda)$ be Lipschitz and twice differentiable, with $0<M_3\le-r_m''\le M_4$.

The fluid problem (2) maximizes $\sum_m\int_0^Tp_m(t)d_m(p_m(t))\,dt$ subject to $\sum_m\int_0^Td_m(p_m(t))\,dt\le c$. Its optimal value is $J^D(T,c)$. Its dual is one-dimensional. With

$$\mathcal R_m(z)=\max_{p}d_m(p)(p-z),\qquad \mathcal P_m(z)=\operatorname*{argmax}_pd_m(p)(p-z),\qquad g(z)=cz+T\sum_m\mathcal R_m(z),$$

the dual optimum is $z^*=\operatorname{argmin}_{z\ge0}g(z)$, and the optimal fluid prices are the constants $p^*_m=\mathcal P_m(z^*)$.

In the $n$-th system demand and inventory scale together: type $m$ arrives as a Poisson process with rate $n\,d_m(p)$, and the inventory is $nc$. The firm does not know $d_m$. It knows $T$, $c$, $n$, the constants of Assumption 1 and, by Assumption 2, intervals $[\underline p,\overline p]$ and $[0,\overline z]$ that contain every $p^*_m$ and $z^*$. A policy $\pi$ has expected revenue $J^\pi_n(T,c)$, and its regret is

$$R^\pi_n(T,c)=1-\frac{J^\pi_n(T,c)}{J^D_n(T,c)}.$$

Algorithm 1, the primal-dual learning algorithm, runs phases $k=1,\dots,K$ of shrinking lengths $\tau^{(k)}$. In each learning phase it tests a price grid inside the current interval estimators of every $p^*_m$. It then minimizes an empirical dual function on a grid of $z$ and re-centres the interval estimators of $z^*$ and $p^*_m$. In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to $nc$ (insufficient capacity). Its tuning depends on a constant $\epsilon>0$.

Formalization targets

Goal: Theorem 1 (p. 17)

For every $\delta>0$ one can choose $\epsilon>0$ and a constant $C$, independent of $n$, such that

$$R^\pi_n(T,c)\le C(\log n)^{2+\delta}n^{-1/2}\qquad\text{for all }n\ge3.$$

The two capacity regimes (Propositions 2–3)

$$z^*=0:\ R^\pi_n=O\big((\log n)^{2+16\epsilon}n^{-1/2}\big),\qquad z^*>0:\ R^\pi_n=O\big((\log n)^{2+18\epsilon}n^{-1/2}\big).$$

Milestones

• Proposition 1: the fluid problem is solved by the constant prices $p^*$, with complementary slackness; and the monotonicity, convexity and derivative of $\mathcal P_m$ and $\mathcal R_m$.
• Lemmas 9 and 10: a Poisson tail bound decaying faster than any power, and $\mathbb E|X-\lambda|\le\sqrt\lambda$.
• Lemmas 1 and 2: $K\le3\log n+3$, and the learning phases take at most half the season.
• Lemmas 3–5: the interval estimators contain $z^*$, $p^*_m$ and $\mathcal P_m$ on the dual interval, except with probability $O((\log n)^2/n)$.
• Lemmas 6–7: the sales at the start of the last phase are close to the fluid level.
• Lemma 8: when $z^*>0$, $\mathbb E|S(T)-nc|=O((\log n)^\epsilon n^{1/2})$.

Significance

Theorem 1 states that personalized pricing for $M$ types under a shared inventory constraint is learnable at the single-type rate $n^{-1/2}$, up to logarithms, with a constant independent of $n$. Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price $z^*$, instead of the joint optimum of an $M$-dimensional problem, is what avoids the curse of dimensionality.

The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.

Difficulty

The obvious argument estimates every $p^*_m$ directly and charges the estimate. With interval estimators of width $n^{-1/4}$ this loses revenue of order $n^{-1/4}$ per unit time when the inventory constraint binds ($z^*>0$), because $p^*_m$ is then not the unconstrained maximizer of $p\,d_m(p)$. The paper's (11) and (19) show the loss. The bound $n^{-1/2}$ requires steering the total sales to within $O(n^{1/2})$ of the inventory, which is Lemma 8, and a second-order expansion of the revenue around $p^*$ that uses the first-order condition $r_m'(d_m(p^*_m))=z^*$.

Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change $N_m(n\int_0^td_m(P_m(s))\,ds)$.

Formalization scope

All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.

• Model. Types are Fin M. Each $d_m:\mathbb R\to\mathbb R$ satisfies Assumption 1 on $[0,p_\infty]$ and is otherwise any extension with $0\le d_m\le M_1$; the last-phase prices $\underline p^{(K)}_m-\alpha$ and $\overline p^{(K)}_m+\alpha$ can leave $[0,p_\infty]$. $d_m(p_\infty)=0$ encodes the choke price. $\mathcal P_m$ and $z^*$ are fields carrying their optimality properties.
• Assumption 2 is read with $z^*\in[0,\overline z)$; the page prints $(0,\overline z)$, which would drop the case $z^*=0$ that Proposition 2 and Theorem 1 cover. The price interval is placed in the domain, $0\le\underline p<\overline p\le p_\infty$.
• Remark 2 assumes $M_3\le g''\le M_4$; this is read on $[0,\overline z]$, because globally it is unsatisfiable. Each $\mathcal P_m$ is $M_2$-Lipschitz.
• The fluid value $J^D$ is the supremum of (2) over measurable price paths. The identity $J^D=T\sum_mp^*_md_m(p^*_m)$ is Proposition 1.4, a milestone, and is not built into the definition.
• The algorithm. The grid sizes $N^{(k)}$, $N_z^{(k)}$ are rounded up. Grid spacing is $\Delta_m/N$ for prices and $\Delta_z/(N_z+1)$ for duals: the text and Table 1, respectively the text and line 15, agree on these, and Algorithm 1 line 7 and Table 1 print the other forms. Ties in (8)–(9) go to the smallest index. $\theta$ in (14) is projected onto $[0,1]$, with $\theta=0$ when (14) is degenerate. An empty $p^l$ period in step 4 follows the pseudo-code. The decision rules never take $d_m$, $\mathcal P_m$ or $z^*$ as arguments.
• The system. $M$ independent unit-rate Poisson processes (the published IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the $n$-th system is $\lfloor nc\rfloor$ units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).
• Asymptotics. "$O(f(n))$" is read as $\exists C$, independent of $n$ and the phase index, for all $n\ge3$. "Sufficiently small $\epsilon$" is read as every $\epsilon\in(0,\epsilon_0)$. The algorithm needs $n\ge3$ for $K$ to exist.
• Corrected misprints. Proposition 1.2 prints $\mathcal R_m'=-\sum_md_m(\mathcal P_m)$ with the index reused; the statement is $-d_m(\mathcal P_m(z))$. Proposition 1.3 and the global form of the bound in 1.1 fail at the kinks of $\mathcal P_m$. Part 1's derivative bound is stated as a Lipschitz bound, and part 3 is omitted. Lemmas 3–4 are stated in product form. Propositions 2–3 are stated through their regret conclusions. The printed comparison $\tilde J^\pi_n\le J^\pi_n$ (pp. 13–14) can fail when a last-phase price exceeds $\overline p$, so it is not used.

A formalization that lets the policy read the true demand, measures regret against anything other than $J^D_n$, ignores the stock-out in $J^\pi_n$, or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.

Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for $\mathcal R_m$, and the time-change construction of policy-driven Poisson sales.

Selected references

• N. Chen, G. Gallego, A Primal-dual Learning Algorithm for Personalized Dynamic Pricing with an Inventory Constraint, arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1812.09234
• O. Besbes, A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6), 2009. https://doi.org/10.1287/opre.1080.0640
• Z. Wang, S. Deng, Y. Ye, Close the Gaps: A Learning-While-Doing Algorithm for Single-Product Revenue Management Problems, Operations Research 62(2), 2014. https://doi.org/10.1287/opre.2013.1249
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24

Why early exploration needs a lower bound

A stochastic multi-armed bandit learner repeatedly selects one of finitely many arms and sees only the reward from the selected arm. The learner must gather information about uncertain rewards while trying to select high-mean arms. Expected regret summarizes the lost reward relative to always selecting an optimal arm, but regret alone does not explain how much sampling each particular arm must receive. Garivier, Ménard, and Stoltz study this allocation question directly in Explore First, Exploit Next: The True Shape of Regret in Bandit Problems. Their Section 3 gives lower bounds for small horizons, before the longer-run logarithmic behavior becomes dominant.

The paper's first small-horizon result concerns strategies that allocate at least a uniform share to every optimal arm, on every problem in a specified model. This requirement excludes a strategy that always selects one fixed label and succeeds only when that label happens to be best. Such a requirement still permits many adaptive policies; it constrains their performance on optimal arms rather than prescribing their decisions round by round. The result establishes a compulsory initial allocation to every arm, including one whose mean is below the best mean. It is Theorem 2 on page 10 of the pinned arXiv:1602.07182v3.

Bandit problems, models, and strategies

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ consists of $K$ probability laws on $\mathbb R$. At each round, a strategy $\psi$ chooses an arm using the observed past and randomization, then receives an independent reward drawn from that arm's law. The mean reward of arm $a$ is $\mu_a=\mathbb E_{\nu_a}[X]$. Write $\mu^*=\max_a\mu_a$, and call an arm optimal when $\mu_a=\mu^*$. The count $N_{\psi,a}(T)$ is the number of times arm $a$ is chosen during the first $T$ rounds. These objects and the information available to a strategy are specified in Section 1.1, pages 2–3.

A model $\mathcal D$ is a collection of possible arm laws, each a probability measure with an expectation. The notation $\underline\nu\in\mathcal D$ means that every arm law $\nu_a$ belongs to $\mathcal D$. A strategy is smarter than uniform on $\mathcal D$ when, for every bandit problem in the model, every optimal arm $a^*$, and every integer $T\ge1$, it satisfies

$$\mathbb E_{\underline\nu}[N_{\psi,a^*}(T)]\ge\frac{T}{K}.$$

This is Definition 2 on page 10. It imposes a lower bound on each optimal arm, even when several arms tie. The requirement is evaluated across the whole model, so a strategy cannot be declared smarter based only on its behavior on the one problem used in the theorem.

For a law $P$, a real threshold $x$, and the model $\mathcal D$, the information number $\mathcal K_{\inf}(P,x,\mathcal D)$ is the infimum of $\mathrm{KL}(P,Q)$ over those $Q\in\mathcal D$ whose mean exceeds $x$. The infimum is $+\infty$ if there is no such $Q$. This is the definition on page 4. It measures how close an arm law is, in Kullback–Leibler divergence, to another admissible law that would give it a mean above the present optimum.

Formalization targets

The main target is Theorem 2. For a model $\mathcal D$, a strategy $\psi$ smarter than uniform on it, a bandit problem $\underline\nu\in\mathcal D$, every arm $a$, and every integer $T\ge1$, the finite-$\mathcal K_{\inf}$ case states

$$\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\ge \frac{T}{K}\left(1-\sqrt{2T\mathcal K_{\inf}(\nu_a,\mu^*,\mathcal D)}\right).$$

The theorem includes optimal and suboptimal arms. Its printed companion says that when $T\le 1/(8\mathcal K_{\inf})$, the arm receives at least $T/(2K)$ expected selections. In the formal statement this threshold is $8T\mathcal K_{\inf}\le1$, which also expresses the intended case $\mathcal K_{\inf}=0$. Both claims come from Theorem 2, page 10.

The milestone list follows the source's intermediate claims. Lemma 6, page 20 bounds Bernoulli relative entropy using the maximum of $x(1-x)$ over an interval. The proof of Theorem 2 on page 11 states that Bernoulli relative entropy increases in its second argument on the interval starting at its first argument. The same page applies the paper's fundamental inequality (6) to the fraction of rounds spent on one arm, then states a lower bound against a single alternative arm law. These are the four curated milestones for the main theorem.

What the result supplies

The theorem turns a model-relative performance condition into a numerical constraint on early sampling. If an arm's law is close in divergence to a law that would make it best, then the bound keeps its expected pull count near the uniform allocation until the horizon is large enough for the term under the square root to matter. It identifies the divergence scale $1/\mathcal K_{\inf}$ at which this particular guarantee becomes weak. The paper contrasts this absolute bound with later relative and collective bounds that capture different dependencies on the number of arms in Section 3, pages 10–14.

The mathematical result is proved in the paper. The remaining work in this mission is a machine-checked development of the statement and its source-backed intermediate inequalities in the canonical stochastic-bandit model. The published bandit structure, policy kernels, and information number provide reusable foundations. Shared definitions supply the Bernoulli divergence, model predicate, and expected pull counts; the local strategy class makes the hypothesis of this particular theorem explicit. The Bernoulli inequalities and the pull-count change-of-measure statement can be reused in other lower-bound results.

Where the difficulty lies

A performance condition about optimal arms does not directly constrain an arm that is suboptimal in the problem of interest. The small-horizon bound must remain valid even though the strategy may adapt to observed rewards, and the relevant alternative arm laws can have divergences approaching an infimum without attaining it. The paper's lower bound is therefore sensitive to the exact orientation of the two bandit problems, the expected count multiplying their divergence, and the boundary conventions for Bernoulli relative entropy. Replacing the infimum with a chosen alternative or changing a divergence to an ordinary real with an arbitrary boundary value would alter the statement.

Formalization scope

Lean uses arms Fin K, indexed from zero; the paper indexes them from one. The horizon is a natural number, and counts are integrated against the probability measure on $T$-round histories generated by a stochastic kernel policy. Such kernels represent the arm-and-reward histories induced by the paper's strategies with auxiliary randomization. The model is a set of probability measures on $\mathbb R$ whose identity function is integrable. The published StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions supply the basic problem, history measure, pull count, means, and $\mathcal K_{\inf}$.

Bernoulli divergence and $\mathcal K_{\inf}$ take values in $[0,+\infty]$. The real square-root formula assumes $\mathcal K_{\inf}<+\infty$: when it is infinite, the paper's right-hand side is $-\infty$, while converting infinity directly to Lean's real value would produce a false numerical bound. The starting bandit problem is explicitly in $\mathcal D$, a condition needed for the proof's use of Definition 2 on a one-arm modification, although the printed quantifier on page 10 omits it. The arm parameter guarantees $K\ge1$; every target assumes $T\ge1$, so its real divisions by $K$ and $T$ have the stated meaning.

A faithful development must retain Definition 2's quantification over all model problems and each optimal arm, rather than only over the bandit problem used in the conclusion. It must use the full Bernoulli relative entropy, including infinite endpoint values, and the infimum over precisely those model laws with mean greater than $\mu^*$. The local instance of (6) also assumes integrable arm rewards in both bandit problems, as Section 1.1 requires. Contributions that establish the four milestones, the companion threshold claim, or reusable count-integrability and divergence facts are in scope.

Selected references

• Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; arXiv:1602.07182v3.
• Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020; DOI:10.1017/9781108571401. The published bandit definitions used here follow its canonical framework.

Motivation

Lower bounds for stochastic multi-armed bandits are usually stated for a large horizon: Lai and Robbins (1985) and Burnetas and Katehakis (1996) show that a consistent strategy pulls a suboptimal arm at least about $\ln T / \mathcal{K}_{\inf}$ times. These bounds say nothing about the small-horizon regime, the first rounds in which a strategy has not yet had time to separate the arms. Garivier, Ménard and Stoltz (arXiv:1602.07182v3, Mathematics of Operations Research, 2019) describe that regime through one information-theoretic inequality, their (6), and derive several lower bounds from it. This mission formalizes their relative lower bound, Theorem 3 (p. 11): under a mild symmetry assumption on the strategy, a suboptimal arm is either pulled at the uniform rate $T/K$ or, on average, almost as often as an optimal arm. It is the statement behind the title's claim that bandit strategies must first explore.

Setting

There are $K$ arms. A bandit problem $\underline{\nu} = (\nu_1, \dots, \nu_K)$ assigns to each arm $a$ a probability distribution $\nu_a$ on $\mathbb{R}$ with expectation $\mu_a$. The optimal mean is $\mu^\star = \max_a \mu_a$, the gap of arm $a$ is $\Delta_a = \mu^\star - \mu_a$; arm $a$ is optimal if $\Delta_a = 0$ and suboptimal if $\Delta_a > 0$.

A model $\mathcal{D}$ is a set of distributions on $\mathbb{R}$, each with an expectation; a bandit problem is in $\mathcal{D}$ when every $\nu_a$ belongs to $\mathcal{D}$.

At each round $t$ a strategy $\psi$ picks an arm $A_t$, possibly at random, as a function of the past arms and rewards, and receives a reward $Y_t$ drawn from $\nu_{A_t}$. The number of pulls of arm $a$ in the first $T$ rounds is

$$N_{\psi,a}(T) = \sum_{t=1}^{T} \mathbb{1}\{A_t = a\},$$

and $\mathbb{E}_{\underline{\nu}}$ denotes expectation when $\psi$ plays against $\underline{\nu}$. Write $N^+_{\psi,a}(T) = \max\{N_{\psi,a}(T), 1\}$.

Kullback–Leibler divergence. $\mathrm{KL}(P, Q) \in [0, +\infty]$ is the Kullback–Leibler divergence between distributions, and $\mathrm{kl}(p, q)$ the divergence between Bernoulli laws of parameters $p$ and $q$.

Pairwise symmetry (Definition 3, p. 11). A strategy $\psi$ is pairwise symmetric for optimal arms on $\mathcal{D}$ if for every bandit problem $\underline{\nu}$ in $\mathcal{D}$, every pair of optimal arms $a^\star, a_\star$ with $\nu_{a^\star} = \nu_{a_\star}$ and every $T \ge 1$, the pairs $(N_{\psi,a^\star}(T), N_{\psi,a_\star}(T))$ and $(N_{\psi,a_\star}(T), N_{\psi,a^\star}(T))$ have the same distribution. A strategy that uses only the observed payoffs, and not the labels of the arms, has this property.

Formalization targets

Goal: Theorem 3 (p. 11)

For every model $\mathcal{D}$, every strategy $\psi$ pairwise symmetric for optimal arms on $\mathcal{D}$, every bandit problem $\underline{\nu}$ in $\mathcal{D}$, every suboptimal arm $a$, every optimal arm $a^\star$ with $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$ and every $T \ge 1$,

$$\mathbb{E}_{\underline{\nu}}\big[N_{\psi,a}(T)\big] \ge \frac{T}{K} \quad\text{or}\quad \mathbb{E}_{\underline{\nu}}\left[\frac{N^+_{\psi,a}(T)}{N^+_{\psi,a^\star}(T)}\right] \ge 1 - 2\sqrt{\frac{2T\,\mathrm{KL}(\nu_a, \nu_{a^\star})}{K}} .$$

Companion: the "in particular" clause

For $T \le K / (32\,\mathrm{KL}(\nu_a, \nu_{a^\star}))$ the second alternative becomes $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}(T)/N^+_{\psi,a^\star}(T)] \ge 1/2$.

Milestones (p. 12)

1. The symmetry identity: for the alternative problem $\underline{\nu}'$ obtained by replacing $\nu_a$ by $\nu_{a^\star}$, $\mathbb{E}_{\underline{\nu}'}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] = 1/2$.
2. Inequality (12): $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a, \nu'_a) \ge \mathrm{kl}\big(\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})], 1/2\big)$.
3. The Jensen display: $\mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})] \le r/(1+r)$ with $r = \mathbb{E}_{\underline{\nu}}[N^+_{\psi,a}/N^+_{\psi,a^\star}]$.
4. The bound $r/(1+r) \ge 1/2 - \sqrt{T\,\mathrm{KL}(\nu_a,\nu'_a)/(2K)}$ in the case $\mathbb{E}_{\underline{\nu}}[N_{\psi,a}(T)] \le T/K$, $r \le 1$.

Significance

The theorem shows that in the initial phase a symmetric strategy cannot discard a suboptimal arm quickly: unless the arm is already sampled at the uniform rate, it is sampled, in ratio, nearly as often as an optimal arm, as long as $T$ is small compared with $K / \mathrm{KL}(\nu_a, \nu_{a^\star})$. Together with Theorem 2 (absolute lower bound) and Theorem 4 (collective lower bound) it describes the regret curve before the logarithmic regime: roughly linear growth, then a transition. It requires no assumption on the model beyond the existence of expectations, and it involves the divergence between the two arms themselves rather than the model-dependent quantity $\mathcal{K}_{\inf}$.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean statement of Theorem 3 on the canonical bandit model already used on the platform (StochasticBandit, BanditPolicy), a formal version of the symmetry assumption that sibling missions reuse (mission V, the collective lower bound, uses the same Definition 3), and the four intermediate steps of the proof as separate targets.

Difficulty

The proof compares $\underline{\nu}$ with an alternative problem $\underline{\nu}'$ that differs from it only in arm $a$, and transfers information between them through the fundamental inequality (6) of §2, a data-processing argument on the law of the whole history. The step specific to Theorem 3 is the choice of the test variable: the expectation of $N^+_{\psi,a}/(N^+_{\psi,a} + N^+_{\psi,a^\star})$ is known exactly under $\underline{\nu}'$ only because the strategy is pairwise symmetric, and the symmetry is a statement about joint laws of pull counts, not about their expectations. A version of the assumption that only equates expected pull counts does not determine the expectation of this ratio. The ratio expectation then has to be extracted from a bound on $\mathbb{E}[x/(1+x)]$, which needs Jensen's inequality in the right direction and a case split on whether $r \le 1$.

Formalization scope

Arms are Fin K (0-based). The horizon $T$ is a natural number. A strategy is a published BanditPolicy: a family of Markov kernels from the observed history of (arm, reward) pairs to the next arm. Every strategy of the paper, which may use auxiliary uniform random variables, induces such a kernel with the same law of arms and rewards. The law of the history is the published banditMeasure, and $N_{\psi,a}(T)$ is the published armPullCount. The model is a set of measures on $\mathbb{R}$, and every statement assumes the paper's standing hypothesis (§1.1, p. 3) that each member is a probability measure with an integrable identity, together with $\underline{\nu}$ in $\mathcal{D}$.

Committed conventions:

• $\mathrm{KL}$ and $\mathrm{kl}$ take values in $[0, +\infty]$; the Bernoulli divergence is the Kullback–Leibler divergence of two Bernoulli laws on $\mathbb{R}$, not a real formula with finite values at $q \in \{0, 1\}$.
• Theorem 3 adds the hypothesis $\mathrm{KL}(\nu_a, \nu_{a^\star}) < \infty$. When the divergence is infinite the paper's bound reads $\ge -\infty$ and is empty; reading $+\infty$ as the real number $0$ would make the statement false.
• The "in particular" clause is stated as $32\,T\,\mathrm{KL}(\nu_a,\nu_{a^\star}) \le K$ in $[0, +\infty]$, which needs no finiteness assumption.
• Definition 3 is an equality of joint laws (push-forwards of the history law), for every $T \ge 1$, only for optimal arms of problems in $\mathcal{D}$ with equal distributions. Invariance under all permutations of the arms would strengthen the hypothesis and weaken the theorem.
• Ratios use $\max\{N, 1\}$ as real numbers, so no division by zero occurs; all integrands are bounded by $T$.

A formalization in which the symmetry assumption equates only expected pull counts, in which the divergence is a real number with junk value $0$ at $+\infty$, or in which the disjunction is replaced by its second alternative, is not this theorem.

The mission builds on the published definitions StochasticBandit and BanditPolicy. A complete development needs the fundamental inequality (6) for kernel policies (the divergence decomposition, published as BanditAlgorithm.bandit_divergence_decomposition, plus data processing for the Bernoulli test), Pinsker's inequality for Bernoulli laws (proved on the platform as BanditAlgorithm.bernoulli_relative_entropy_pinsker), Jensen's inequality for concave functions (Mathlib), and a lemma that the law of the history is unchanged in distribution when two identically distributed optimal arms are relabelled. The measurability of pull counts and the relation between the extended-real and real Bernoulli divergences are reusable beyond this mission. Proofs of any milestone, and of the general fundamental inequality, are welcome.

Selected references

• A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019. arXiv:1602.07182v3, doi:10.1287/moor.2017.0928
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6(1), 1985. doi:10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17(2), 1996. doi:10.1006/aama.1996.0007
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. doi:10.1017/9781108571401

Why this lower bound matters

In a stochastic multi-armed bandit, a player repeatedly chooses one of finitely many arms and sees only the reward from the chosen arm. To earn a high reward, the player must favor arms that appear best. Yet an arm that currently appears inferior might be best under another plausible reward law. That uncertainty forces any strategy with uniformly strong long-run performance to keep testing apparently inferior arms. The asymptotic number of tests is a basic benchmark for comparing bandit algorithms: an algorithm that matches the bound uses no more exploration than the information in the model demands. Garivier, Ménard, and Stoltz restate this general benchmark as Theorem 1 and derive it within their analysis of the shape of regret Garivier–Ménard–Stoltz, §2.2.

The quantity controlling the benchmark comes from Burnetas and Katehakis. It measures the least information needed to replace one suboptimal arm by a plausible arm that is strictly better than the current best. The paper cites their quantity on page 4, and its Theorem 1 applies it to every suboptimal arm separately Garivier–Ménard–Stoltz, pp. 4, 9. This per-arm form matters when different arms have different reward laws and different amounts of information are needed to rule them out.

Bandit setting and notation

A bandit problem $\underline\nu=(\nu_a)_{a=1}^K$ has $K$ arms. Each $\nu_a$ is a probability distribution on real rewards with a finite expectation $\mu_a=\mathbb E_{\nu_a}X$. A strategy $\psi$ chooses an arm at each round using the preceding chosen arms and observed rewards, and it may randomize. Let $N_{\psi,a}(T)$ be the number of times arm $a$ is chosen in the first $T$ rounds. The optimal mean is $\mu^\star=\max_a\mu_a$, and the gap of arm $a$ is $\Delta_a=\mu^\star-\mu_a$. An arm is suboptimal when $\Delta_a>0$. These are the objects of §1.1 of the paper Garivier–Ménard–Stoltz, pp. 2–3.

A model $\mathcal D$ is a collection of possible real-valued reward distributions, each with a finite expectation. A bandit problem belongs to $\mathcal D$ when every one of its arm laws does. The Kullback–Leibler divergence $\mathrm{KL}(P,Q)$ measures the information discrepancy from one reward law $P$ to another $Q$; it may be infinite. For an arm law $P$ and a real threshold $x$, define the minimal information cost

$$\mathcal K_{\inf}(P,x,\mathcal D) =\inf\{\mathrm{KL}(P,Q):Q\in\mathcal D,\ \mathbb E_QX>x\}.$$

The infimum is $+\infty$ if there is no qualifying alternative. The strict inequality in the set matters: the replacement law must make the arm better than the original optimal mean, not merely tied with it Garivier–Ménard–Stoltz, p. 4.

Definition 1 calls $\psi$ uniformly fast convergent on $\mathcal D$ when, on every bandit problem in the model, the expected draw count of every suboptimal arm grows more slowly than $T^\alpha$ for each $0<\alpha\le1$:

$$\mathbb E_{\underline\nu}N_{\psi,a}(T)=o(T^\alpha).$$

Here $T$ tends to infinity through integer horizons. This condition is uniform in which problem and suboptimal arm are considered; it does not mean one numerical convergence rate is shared by all problems Garivier–Ménard–Stoltz, p. 9, Definition 1.

Formalization target

The goal is the paper's Theorem 1: for every model $\mathcal D$, every uniformly fast convergent strategy $\psi$, every bandit problem $\underline\nu$ in the model, and every suboptimal arm $a$,

$$\liminf_{T\to\infty} \frac{\mathbb E_{\underline\nu}N_{\psi,a}(T)}{\ln T} \ge\frac1{\mathcal K_{\inf}(\nu_a,\mu^\star,\mathcal D)}.$$

The bound states the minimum logarithmic exploration of each arm. It leaves the model and strategy arbitrary within the stated class. The milestones follow four statements from the proof on page 9: the Bernoulli entropy estimate in (11), the one-arm divergence chain in (10), the eventual bound on draws of the alternative's other arms, and the bound for one alternative law before taking the infimum. Their source text is recorded beside the local drafts Garivier–Ménard–Stoltz, p. 9.

What the result gives

If $\mathcal K_{\inf}$ is finite and positive, the theorem gives a concrete coefficient of $\ln T$ that any uniformly fast convergent strategy must spend on arm $a$. A small information cost means that the arm is hard to distinguish from a better alternative and must be sampled more often. If the cost is infinite because the model contains no better replacement, the reciprocal is zero and the bound makes no positive demand. If the cost is zero, the reciprocal is infinite: the normalized expected draw count must diverge. The extended-value convention is part of the target, not a choice of a finite stand-in Garivier–Ménard–Stoltz, pp. 4, 9.

The theorem is proved in the paper, while the Lean statements in this proposal are proof targets. A completed development would supply a machine-checked bridge from the canonical stochastic-bandit policy model through Bernoulli relative entropy and change of measure to the per-arm asymptotic claim. Its model and divergence definitions can also support lower bounds for other bandit classes. The existing Prove2Me StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions provide the bandit law, policy, draw count, means, and $\mathcal K_{\inf}$ used here; Definition 1's exact strategy class is supplied locally.

Difficulty

The central issue is the quantification over every alternative law in an arbitrary model. A suboptimal arm may become uniquely optimal after changing only its law, while the strategy must remain uniformly fast on that new problem. The information cost is an infimum over such changes, including an empty set or costs arbitrarily close to zero. A statement that reasons about just one convenient alternative does not yield the coefficient in Theorem 1. The proof also passes from finite-horizon information inequalities to a liminf as $T$ grows, so endpoint values of Bernoulli divergence and the extended-value arithmetic must agree with the source Garivier–Ménard–Stoltz, pp. 6, 9.

Formalization scope

Lean indexes the paper's arms $1,\ldots,K$ by Fin K, starting at zero, and uses natural-number horizons. A strategy is a history-dependent Markov kernel, whose generated probability measure describes the sequence of chosen arms and rewards. The pull count is bounded by $T$, so its expectation is a genuine Bochner integral. The model explicitly requires probability laws with integrable identity; this ensures that each mean in $\mathcal K_{\inf}$ is genuine. Bernoulli relative entropy and arm-law KL take values in extended nonnegative reals. The goal's liminf is also in extended nonnegative reals, avoiding a default real liminf for an unbounded sequence. The first two horizons, where $\ln T\le0$, cannot affect an asymptotic liminf.

The theorem sentence on page 9 says “all bandit problems” without restricting the original problem to $\mathcal D$. Its proof applies Definition 1 to that problem, so the proposal states that its arms belong to $\mathcal D$. Without this condition a strategy can behave arbitrarily outside the model. The source's other standing conventions are kept: every reward law has an expectation, the improvement condition in $\mathcal K_{\inf}$ is strict, and uniform fast convergence ranges over all model problems, all suboptimal arms, and all $0<\alpha\le1$. These choices rule out an empty strategy class or a special hard-coded bandit as a trivial route to the target.

Useful contributions include the finite-horizon change-of-measure inequality, endpoint-correct Bernoulli KL estimates, identities for sums of expected pull counts, and asymptotic lemmas for reciprocal infima. The milestone drafts identify the paper statements those contributions must support.

Selected references

• Aurélien Garivier, Pierre Ménard, and Gilles Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research, 2019; cited here from arXiv:1602.07182v3, §§1–2.
• Apostolos N. Burnetas and Michael N. Katehakis, Optimal Adaptive Policies for Sequential Allocation Problems, Advances in Applied Mathematics, 1996. DOI:10.1006/aama.1996.0007.

Motivation

The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times $\mathsf{dec}_\gamma(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}) \cdot T$, so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.

The multi-armed bandit is the first test of this program. Its minimax regret $\Theta(\sqrt{AT})$ is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by $A/\gamma$ from above, and Proposition 5.3 bounds it by $2^{-6} A/\gamma$ from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.

Setting

A decision space $\Pi$ is a finite set; here $\Pi = [A] = \{1, \dots, A\}$, the arms. A model $M$ assigns to every arm $\pi$ a distribution $M(\pi)$ over rewards in $\mathcal{R} = [0,1]$ (observations are trivial). Its mean reward is $f^M(\pi) = \mathbb{E}_{r \sim M(\pi)}[r]$, and $\pi_M \in \arg\max_\pi f^M(\pi)$ is an optimal arm. The squared Hellinger distance between distributions $P, Q$ on a finite set is $D^2_{\mathrm{H}}(P, Q) = \sum_y (\sqrt{P(y)} - \sqrt{Q(y)})^2$ (no factor $\tfrac12$, the paper's (5)).

For a class $\mathcal{M}$ of models, a reference model $\overline{M}$ and $\gamma > 0$, the DEC (2) is

$$\mathsf{dec}_\gamma(\mathcal{M}, \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}} \mathbb{E}_{\pi \sim p}\Bigl[ f^M(\pi_M) - f^M(\pi) - \gamma \cdot D^2_{\mathrm{H}}\bigl(M(\pi), \overline{M}(\pi)\bigr) \Bigr].$$

With $g^M(\pi) = f^M(\pi_M) - f^M(\pi)$, the $L_\infty$-localized class (12) is $\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon\ \forall \pi \}$.

A reference model $\overline{M} \in \mathcal M$ and models $M_1, \dots, M_N \in \mathcal M$, $N \ge 2$, form an $(\alpha, \beta, \delta)$-family (Definition 5.1) if there are $u_i, v_i : \Pi \to [0,1]$ with $\sum_i u_i(\pi) \le N/2$, $\sum_i v_i(\pi) \le 1$, $f^{M_i}(\pi_{M_i}) - f^{M_i}(\pi) \ge \alpha(1 - u_i(\pi))$ and $D^2_{\mathrm{H}}(M_i(\pi), \overline{M}(\pi)) \le \beta v_i(\pi) + \delta$. $\mathrm{Ber}(q)$ is the Bernoulli distribution with mean $q$.

Formalization targets

Goal: Proposition 5.3

For $A \ge 2$ arms, $\overline{M}(\pi) = \mathrm{Ber}(\tfrac12)$ and every $\gamma \ge A/3$, with $\varepsilon_\gamma = \frac{A}{12\gamma}$,

$$\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge 2^{-6} \cdot \frac{A}{\gamma}.$$

Milestones

1. Lemma A.7: $D^2_{\mathrm{H}}(\mathrm{Ber}(p), \mathrm{Ber}(q)) \le (p-q)^2\bigl(\frac{1}{p+q} + \frac{1}{2-p-q}\bigr)$, and in particular $D^2_{\mathrm{H}}(\mathrm{Ber}(\tfrac12 + \Delta), \mathrm{Ber}(\tfrac12)) \le 3\Delta^2$ for $\Delta \in (0, \tfrac12)$.
2. Lemma 5.1: an $(\alpha, \beta, \delta)$-family $\mathcal{M}'$ with $\beta \ge 0$ satisfies $\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) \ge \frac{\alpha}{2} - \gamma(\frac{\beta}{N} + \delta)$ for all $\gamma > 0$.
3. The hard family of the proof: $M_i(\pi) = \mathrm{Ber}(\tfrac12 + \Delta\,\mathbb{I}\{\pi = i\})$ is a $(\Delta, 3\Delta^2, 0)$-family around $\mathrm{Ber}(\tfrac12)$.
4. Localization: this family lies in $\mathcal{M}^\infty_\Delta(\overline{M})$.

Companions

The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by $A/\gamma$), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly $\Delta \in (0, \tfrac18)$, some $\overline{M}$ in the class has $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}), \overline{M}) \ge \frac{\Delta}{4}\mathbb{I}\{\gamma \le \frac{A}{48\Delta}\}$. Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.

Significance

Proposition 5.3 is the DEC half of the $\Omega(\sqrt{AT})$ minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and $\gamma \asymp \sqrt{AT}$, it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the $A/\gamma$ upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).

The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.

Difficulty

The DEC is an inf-sup, so a lower bound must hold against every exploration distribution $p$. A natural first attempt picks a single alternative model and compares; this fails because $p$ can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single $p$ is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen $\Delta$. In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are $0$ on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.

Formalization scope

• Finite alphabets. The paper works over measurable spaces; this mission formalizes the finite-alphabet case, as the published FoundationsRL layer does. A model is m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.
• Bernoulli subclass. The bandit class is the Bernoulli bandits (Y = Bool, reward $1$ on true), a subclass of the paper's all-distributions-on-$[0,1]$ class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.
• Optimal-arm selector. $\pi_M$ is a parameter piStar with the hypothesis that it picks a maximizer of $f^M$; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference $\mathrm{Ber}(\tfrac12)$ has every arm optimal).
• Added or dropped hypotheses. Lemma 5.1 makes the page's nonempty decision space explicit; its optimal-arm selector also implies nonemptiness. It adds $\beta \ge 0$, necessary for the printed averaging argument: without it, even identical models can contradict (52). The family definition includes membership of the reference and family models in a probability-model class. The localization claim inherits $A \ge 2$ from Proposition 5.3. Proposition 6.7 states $A \ge 2$, implicit on the page since a gap needs two arms. Proposition 5.1 represents models by their mean vectors and priors as finitely supported (footnote 5).
• Constants. All constants are the page's: $2^{-6}$, $A/(12\gamma)$, $\gamma \ge A/3$, $3\Delta^2$, $5\Delta^2$, $\Delta/4$, $A/(48\Delta)$. The page's proof of Proposition 6.7 names a $(\Delta, 5\Delta^2, 0)$-family but computes with $12\Delta^2$; the stated proposition is the one its arithmetic supports.
• No trivialization. A formalization in which the localized class could be empty, or the payoffs unbounded, would make decGf evaluate to the junk value $0$; the goal is stated over a class containing $\overline{M}$ with bounded rewards, so the inequality is the genuine one, and its right side $2^{-6} A/\gamma$ is strictly positive.

Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, 2021 (v3, 2023). https://arxiv.org/abs/2112.13487
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. https://arxiv.org/abs/2312.16730
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• J.-Y. Audibert, S. Bubeck, Regret Bounds and Minimax Policies under Partial Monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
• D. J. Foster, A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML, 2020. https://arxiv.org/abs/2002.04926