Bandit Algorithms III: Asymptotic and Minimax Optimality of UCBTextbook
The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant 16/Δi is eight times the information-theoretic limit, and its worst-case rate carries a spurious logn. Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule f(t)=1+tlog2t yields the asymptotically optimal limsupn→∞Rn/logn≤∑i:Δi>02/Δi — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index μ^i+Ti4log+(kTin) achieves minimax regret Rn≤39kn+∑iΔi, matching the Ω(kn) lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.
Bandit Algorithms II: Stochastic Bandits and the UCB AlgorithmTextbook
A learner repeatedly chooses one of k slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition Rn=∑iΔiE[Ti(n)]) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound Rn≤3∑iΔi+∑i:Δi>016log(n)/Δi — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion Rn≤8nklogn+3∑iΔi.
Bandit Algorithms XIV: Bayesian Bandits, the Gittins Index and Thompson SamplingTextbook
The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves limn→∞Rn/logn=∑i:Δi>02/Δi, exactly asymptotically optimal, alongside the minimax-grade Rn≤Cknlogn. Together they explain why posterior sampling is both principled and practically dominant.
Bandit Algorithms XI: Lower Bounds for Stochastic Linear BanditsTextbook
Is the dn regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter θ with ∥θ∥22=d2/(48n) forcing Rn≥163dn — the goal theorem — and the hypercube gives the same Ω(dn) rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant c(A,θ) is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.
Bandit Algorithms V: Adversarial Bandits and Exp3Textbook
What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial k-armed bandit: rewards xti∈[0,1] are an arbitrary fixed matrix, the learner samples At∼Pt, and regret is measured against maxi∑txti. The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates X^ti=1−1{At=i}(1−Xt)/Pti, achieves Rn≤2nklogk — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.
Improved Algorithms for Linear Stochastic Bandits I: High-Probability Regret Bound for the OFUL AlgorithmResearch Paper
Motivation
In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first n rounds.
The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret O(dnlog3/2n) with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.
Setting
Fix a dimension d≥1 and an unknown parameter θ∗∈Rd. In round t=1,2,… the learner is given a nonempty decision setDt⊆Rd, chooses Xt∈Dt, and observes the reward
Yt=⟨Xt,θ∗⟩+ηt.
There is a filtration {Ft}t≥0 such that Xt is Ft−1-measurable and ηt is Ft-measurable and conditionally R-sub-Gaussian: E[eληt∣Ft−1]≤exp(λ2R2/2) for all λ∈R, with R≥0 fixed.
For a regularization parameter λ>0 let Vt=λI+∑s=1tXsXs⊤ and let θt=Vt−1∑s=1tYsXs be the regularized least-squares estimate. With ∥v∥A=v⊤Av and a known bound ∥θ∗∥2≤S, the confidence ellipsoid is
The OFUL algorithm chooses, in round t, a pair (Xt,θt) maximizing ⟨x,θ⟩ over Dt×Ct−1. The pseudo-regret is Rn=∑t=1n⟨xt∗−Xt,θ∗⟩, where ⟨xt∗,θ∗⟩=maxx∈Dt⟨x,θ∗⟩.
Formalization targets
Goal: Theorem 3, the regret of OFUL
If ∥Xt∥2≤L, ⟨x,θ∗⟩∈[−1,1] for all x∈Dt, and λ≥max(1,L2), then for every δ>0, with probability at least 1−δ,
For any positive definite V, Vt=V+∑s≤tXsXs⊤ and St=∑s≤tηsXs: with probability at least 1−δ, for all t≥0,
∥St∥Vt−12≤2R2log(det(Vt)1/2det(V)−1/2/δ).
Milestones: Theorem 2, the confidence ellipsoids
With probability at least 1−δ, θ∗∈Ct for all t≥0 (first claim). If ∥Xt∥2≤L, then with probability at least 1−δ, for all t, ∥θt−θ∗∥Vt≤Rdlog((1+tL2/λ)/δ)+λ1/2S (second claim, stated here for d≥2).
Significance
Theorem 3 bounds the regret of OFUL by O(dnlogn) with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.
All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases V=λI, R=1, δ<1 of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.
Difficulty
The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence Xt has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix Vt, which is itself built from the adaptively chosen actions; a bound for each fixed t does not give it.
Formalization scope
Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and ∥x∥A is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed t+1 for t:N, so sums over s≤t are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy R2) requires; this is an added hypothesis. Every "with probability at least 1−δ, for all t" is stated as an outer-measure bound ≤δ on the failure event, with the time quantifier inside the event. det(⋅)1/2 is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.
OFUL is a predicate on the whole process: in every round the chosen pair maximizes ⟨x,θ⟩ over Dt×Ct−1, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward ⟨xt∗,θ∗⟩ is the supremum over Dt, finite because of the reward bound.
Two corrections to the printed Theorem 3 are made and disclosed. The printed nL/d is replaced by nL2/d, which is what the determinant–trace bound detVn≤(λ+nL2/d)d gives; for L≤1 the corrected bound implies the printed one. The hypothesis λ≥max(1,L2) is added: for λ<1 the printed logarithm can be negative, and the printed bound would then assert Rn≤0. In the second claim of Theorem 2, d≥2 is added, because at d=1 the claim does not follow from the first claim and the paper's proof is not available.
The goal is a probability bound over the noise, not the pathwise statement "if θ∗∈Ct−1 for all t then Rn≤…". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same δ as the conclusion.
Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on Rd, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general V and R, and reusable determinant lemmas are all welcome.
Selected references
Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
Bandit Algorithms XVI: Markov Decision Processes and UCRL2Textbook
The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with S states, A actions and rewards in [0,1]. The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability 1−δ, R^n<CD(M)SAnlog(nSA/δ), where D(M) is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound E[R^n]≥C′DSAn brackets the true complexity of tabular reinforcement learning up to DS.
Bandit Algorithms VII: Lower Bounds for Finite-Armed BanditsTextbook
How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: D(Pνπ,Pν′π)=∑iE[Ti(n)]D(Pi,Pi′). Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound Rn≥271(k−1)n over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers liminfnRn/logn≥∑i:Δi>0Δi/dinf(Pi,μ∗,Mi), certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.
Optimal Best Arm Identification with Fixed Confidence IV: Asymptotic Optimality of the Track-and-Stop StrategyResearch Paper
Motivation
In best arm identification with fixed confidence, a learner samples K unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk δ. The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexityEμ[τδ], the expected number of samples a strategy takes before stopping.
Timeline of the question this mission formalizes:
Chernoff (1959) introduced sequential tests based on generalized likelihood ratios for adaptive design of experiments, with a finite set of hypotheses (doi:10.1214/aoms/1177706205).
Kaufmann, Cappé and Garivier (2016, JMLR) proved a change-of-measure lower bound on the sample complexity of every δ-PAC strategy (arXiv:1407.4443).
Garivier and Kaufmann (COLT 2016) identified the exact constant T∗(μ) in that lower bound and gave the first strategy, Track-and-Stop, whose sample complexity matches it asymptotically as δ→0 (arXiv:1602.04589). This mission covers the upper-bound half of that paper.
Setting
A canonical one-parameter exponential family is a family of laws νθ, θ∈Θ, on R with density exp(θx−b(θ)) with respect to a reference measure ξ; b is twice differentiable and strictly convex, and νθ has mean b˙(θ). Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence d(μ,μ′) is the Kullback–Leibler divergence between the members with means μ and μ′.
A bandit model μ=(μ1,…,μK) assigns a member of the family to each arm. The class S consists of models with a unique optimal arm a∗(μ). At each round t=1,2,… the learner picks an arm At as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time τδ recommends an arm. Na(t) is the number of draws of arm a in the first t rounds and μ^a(t) its empirical mean.
With Alt(μ)={λ∈S:a∗(λ)=a∗(μ)} and ΣK the probability simplex, the characteristic time is
T∗(μ)−1=w∈ΣKsupλ∈Alt(μ)infa=1∑Kwad(μa,λa),
and the maximizer w∗(μ) are the optimal proportions of arm draws.
Track-and-Stop combines two ingredients:
a sampling rule that tracks the plug-in proportions w∗(μ^(t)) while forcing each arm to be drawn about t times: C-Tracking tracks the cumulated sum of projections of w∗(μ^(s)) onto ΣKϵs={w∈ΣK:wa≥ϵs}, ϵs=(K2+s)−1/2/2; D-Tracking draws an under-sampled arm when some Na(t)<t−K/2, and otherwise the arm maximizing twa∗(μ^(t))−Na(t);
Chernoff's stopping rule, which stops at the first t at which some arm a beats every other arm b in a generalized likelihood ratio test, Za,b(t)>β(t,δ), here with β(t,δ)=log(r(t)/δ).
Formalization targets
Goal: Theorem 14 (p. 13)
For α∈[1,e/2] and r(t)=O(tα), Chernoff's stopping rule with β(t,δ)=log(r(t)/δ) combined with C-Tracking or D-Tracking satisfies
Lemma 7 (p. 7): C-Tracking ensures Na(t)≥t+K2−2K and maxa∣Na(t)−∑s<twa∗(μ^(s))∣≤K(1+t).
Lemma 8 (p. 7): D-Tracking ensures Na(t)≥(t−K/2)+−1, and proportions within 3(K−1)ϵ of w∗(μ) after a time tϵ that does not depend on the trajectory, once the plug-in targets are within ϵ.
Proposition 9 (p. 8): under either rule, Na(t)/t→wa∗(μ) almost surely.
Lemma 18 (p. 27): an explicit x with c1x≥log(c2xα) for α∈[1,e/2].
Proposition 13 (p. 11): with any sampling rule whose proportions converge almost surely to w∗, τδ<∞ almost surely and limsupδ→0τδ/log(1/δ)≤αT∗(μ) almost surely.
Significance
Theorem 1 of the same paper shows Eμ[τδ]≥T∗(μ)kl(δ,1−δ) for every δ-PAC strategy, and kl(δ,1−δ)∼log(1/δ). Theorem 14 with α=1 therefore shows that the lower bound is attained: T∗(μ) is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.
The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.
Difficulty
The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of τδ/log(1/δ) does not control E[τδ], because on the rare events where the empirical means are far from μ the stopping time may be very large. Theorem 14 needs a quantitative concentration of μ^(t) on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the t lower bounds on Na(t) (the concentration step of App. D, Lemmas 19–20).
A second obstacle is the regularity of w∗: the tracking lemmas only transfer convergence of μ^(t) to convergence of Na(t)/t through the continuity of μ↦w∗(μ) on S, proved from the characterization of w∗ in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near μ, which requires the empirical means to lie in the interior of the mean space.
Formalization scope
Model. The exponential family is a structure (ξ,Θ,b) with Θ a nonempty open interval, each νθ normalized, b twice continuously differentiable and b¨>0 on Θ. Openness and b¨>0 are added to the paper's "convex, twice differentiable"; strict convexity is what makes νμ unique. Bandit models are parameter vectors θ∈ΘK with K≥2; arms are indexed 0,…,K−1. S is the set of parameter vectors with a unique arm of largest mean b˙(θa).
Protocol. Policies, the trajectory law Pμ, pull counts, empirical means and T∗(μ) are the platform's published definitions (BanditPolicy, BanditTrajectory, TrackAndStop). T∗ uses Kullback–Leibler divergences of the arm laws over the class S and takes values in [0,∞]. Trajectory coordinate t is round t+1. An arm never drawn has empirical mean 0.
Target map.w∗(μ^(t)) is undefined in the paper when μ^(t)∈/S (an unsampled arm, ties, a mean outside b˙(Θ)). Every tracking statement quantifies over every target map with values in ΣK that returns optimal proportions on S, over every choice of L∞ projections, and over every tie-breaking, including randomized ones.
Stopping rule. The two maxima in Za,b(t) are suprema over Θ in the extended reals. Za,b(t)>β is written without subtracting infinities. The stopping time is the first t≥1 at which the test succeeds, +∞ if none. "r(t)=O(tα)" is r(t)≤Dtα for t≥1; r>0 is added so that log(r(t)/δ) is defined.
Values in [0,∞]. Expectations of τδ, the ratios and T∗ live in [0,∞]. No statement converts them to reals, so an infinite expected stopping time is never read as 0.
Corrections, disclosed. Proposition 9's printed Pw is Pμ. Lemma 18 adds c2/c1α>1 and x>0, without which its expressions are undefined.
Ruled out. Specializing to Gaussian arms, or asserting that some sampling policy achieves the bound, would restate existing platform results and is not this theorem: the goal is about every C-Tracking or D-Tracking run in every exponential family.
Welcome contributions. Exponential-family facts (b˙ is the mean, the KL formula, concentration of empirical means); the continuity of w∗ (Proposition 6, App. A.3); Lemma 17 (App. B.2), from which Lemma 8 follows; the closed form (7) of the GLR statistic.
Selected references
A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016, JMLR W&CP 49. arXiv:1602.04589v2
E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. arXiv:1407.4443
Optimal Best Arm Identification with Fixed Confidence I: Non-Asymptotic Lower Bound on the Sample ComplexityResearch Paper
Motivation
Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces K unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed δ. The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.
Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant T∗(μ) is exactly matched, as δ→0, by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).
Setting
A canonical one-parameter exponential family is given by a reference measure ξ on R, an open interval Θ⊂R and a function b, twice continuously differentiable on Θ with b¨>0, such that the laws νθ with density exp(θx−b(θ)) with respect to ξ are probability measures for θ∈Θ. The mean of νθ is b˙(θ). Bernoulli laws and Gaussian laws of known variance are examples.
A bandit model is a vector θ=(θ1,…,θK)∈ΘK; arm a returns i.i.d. rewards with law νθa and mean μa=b˙(θa). Arm a∗(μ) is the unique optimal arm if μa∗>μa for every a=a∗. Let S be any set of bandit models of the family each having a unique optimal arm, and put Alt(μ)={λ∈S:a∗(λ)=a∗(μ)}.
A strategy consists of a sampling ruleπ (the arm At drawn at round t depends, possibly with extra randomization, on the first t−1 observations), a stopping timeτ of the natural filtration Ft=σ(A1,X1,…,At,Xt), and an Fτ-measurable decisiona^τ. It is δ-PAC on S if for every μ∈S, Pμ(τ<∞)=1 and Pμ(a^τ=a∗(μ))≤δ. Na(t) is the number of draws of arm a among the first t rounds.
Write d(μa,λa)=KL(νθa,νλa) for the divergence between two arm laws, kl(x,y)=xlogyx+(1−x)log1−y1−x, and ΣK for the probability simplex on the K arms. The characteristic time is defined by eq. (1):
T∗(μ)−1=w∈ΣKsupλ∈Alt(μ)infa=1∑Kwad(μa,λa).
Formalization targets
Goal: Theorem 1 (p. 3)
For δ∈(0,1/2], every δ-PAC strategy on S and every μ∈S,
Eμ[τ]≥T∗(μ)kl(δ,1−δ).
The statement fixes no constant beyond those of the paper, and it holds for every δ, not only in the limit.
Milestone: eq. (2) (p. 4)
For every λ∈S with a∗(λ)=a∗(μ),
a=1∑Kd(μa,λa)Eμ[Na(τ)]≥kl(δ,1−δ).
This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.
Significance
Theorem 1 identifies T∗(μ) as the exact problem-dependent complexity of fixed-confidence best arm identification: since kl(δ,1−δ)∼log(1/δ), it gives liminfδ→0Eμ[τδ]/log(1/δ)≥T∗(μ), and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer w∗(μ) of eq. (1) (mission II).
Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant log(1/(4δ)); for δ≤1/2, kl(δ,1−δ)≥log(1/(2.4δ))>log(1/(4δ)), so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.
Difficulty
The obvious proof applies the finite-horizon divergence decomposition KL(Pμn,Pλn)=∑aEμ[Na(n)]d(μa,λa) at a deterministic horizon n. That fails here: τ is random and unbounded, the decision is Fτ-measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into kl(δ,1−δ), is the central difficulty. A second, smaller difficulty is to identify the paper's divergence d and its means b˙(θ) with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.
Formalization scope
Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); kl is the platform's bernoulliRelativeEntropy and Na(t) is trajPullCount. Conventions:
arms are Fin K, 0-based (the paper's arm a is index a−1); trajectory coordinate t is round t+1;
Θ is a nonempty open interval and b¨>0 on Θ (added: the paper says b is convex and twice differentiable; strict convexity is what makes "the unique distribution with mean μ" meaningful); the paper's d is written as the KL divergence of the arm laws (its first equality on p. 3), and the unique optimal arm is defined through the parameter means b˙(θa);
S is an arbitrary set of models with a unique optimal arm, not the specific set the paper fixes from p. 4 on;
δ-PAC keeps both halves of the paper's definition (almost-sure stopping and error at most δ);
T∗(μ), divergences and expectations of τ take values in [0,∞], never truncated to reals; T∗=0 when Alt(μ)=∅ and T∗=∞ when the supremum in eq. (1) is 0;
δ≤1/2 is added. The paper states δ∈(0,1), but the theorem and eq. (2) are false for δ∈(1/2,1): with two unit-variance Gaussian arms, drawing arm 1 once and naming arm 1 exactly when the fractional part of the reward is below 1/2 is 0.9-PAC, while T∗(μ)→∞ as the two means merge. At δ=1/2 the bound is 0.
A statement with log(1/(4δ)) in place of kl(δ,1−δ), or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates E[τ] or T∗ to real numbers.
Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an Fτ-measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of νθ=b˙(θ)" and "KL of two family members =b(θ′)−b(θ)−b˙(θ)(θ′−θ)", and E[τ]=∑aE[Na(τ)]. All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.
Selected references
A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, Journal of Machine Learning Research 17(1), 2016. https://arxiv.org/abs/1407.4443
T. L. Graves, T. L. Lai, Asymptotically Efficient Adaptive Choice of Control Laws in Controlled Markov Chains, SIAM Journal on Control and Optimization 35(3), 1997. https://doi.org/10.1137/S0363012994275440
S. Mannor, J. N. Tsitsiklis, The Sample Complexity of Exploration in the Multi-Armed Bandit Problem, Journal of Machine Learning Research 5, 2004. https://www.jmlr.org/papers/v5/mannor04b.html
Improved Algorithms for Linear Stochastic Bandits II: Constant High-Probability Regret of UCB(δ)Research Paper
Motivation
The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of d actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.
The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time t (or with a horizon n fixed in advance), and its guarantee is on the expected regret, which grows like logn. Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.
Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the d-armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB(δ), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least 1−δ. This mission formalizes that section.
Setting
There are d≥1 arms with unknown meansμ1,…,μd∈R. Write μ∗=max1≤i≤dμi for the best mean and Δi=μ∗−μi≥0 for the gap of arm i.
Randomness lives on a probability space (Ω,F,P) with a filtration (Ft)t≥0. In round t=1,2,… the learner plays an arm It that is Ft−1-measurable and receives the reward μIt+ηt. The noise ηt is Ft-measurable and conditionally 1-sub-Gaussian:
E[eληt∣Ft−1]≤eλ2/2for all λ∈R.
The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.
After t rounds, Ni,t is the number of plays of arm i and Xi,t is the average reward received from it. For a confidence level δ>0 the confidence width is
ci,t=Ni,t21+Ni,t(1+2logδd(1+Ni,t)1/2)(3)
with ci,t=+∞ when Ni,t=0. UCB(δ) plays, in round t, an arm that maximizes Xi,t−1+ci,t−1; in particular every arm is played once before any comparison is made. The pseudo-regret after n rounds is
Rn=t=1∑n(μ∗−μIt).
This is the linear bandit of the paper with the standard basis of Rd as decision set and θ∗=μ.
Formalization targets
Goal: Theorem 7 (constant regret of UCB(δ))
For every δ>0, with probability at least 1−δ, for all n≥0 simultaneously,
Rn≤i:Δi>0∑(3Δi+Δi16logΔiδ2d).
The right-hand side depends only on the gaps, d and δ.
Milestone: Lemma 6 (confidence intervals)
For any adapted choice of arms (not only UCB(δ)) and every δ>0, with probability at least 1−δ,
∣Xi,t−μi∣≤ci,tfor all arms i and all t≥0.
Significance
The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability 1−δ the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability δ the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.
Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for V=λI and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.
Difficulty
Two points separate this from textbook UCB analyses. First, the number of samples Ni,t of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of t: a union bound over all t costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale ∑sηs1{Is=i}. Second, the regret statement is uniform in n with constants depending on the gaps; converting a condition of the form "c(N)≥Δi/2" into an explicit bound on N requires solving an inequality in which N appears both polynomially and inside a logarithm, and the explicit constants 3 and 16 must come out of that step.
Formalization scope
The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.
Arms are Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, μ∗ is ⨆ i, μ i (the maximum over a nonempty finite type).
Rounds are indexed t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index 0 are unused.
The sample space is assumed to be a standard Borel space, which Mathlib's conditional sub-Gaussianity requires; this hypothesis is not in the paper.
"With probability at least 1−δ, for all …" is stated as: the outer probability of the failure event, with the quantifiers over arms and times inside it, is at most δ. For δ≥1 the statements are trivially true, as in the paper.
The rule (4) is read with the statistics of rounds 1,…,t−1, because the printed Xi,t, ci,t already count round t. An unplayed arm, whose width is +∞ in the paper, is played before the indices are compared. Every tie-breaking rule is allowed, and measurability of the chosen arm is assumed rather than derived.
The printed Theorem 7 has no quantifier on n; it is formalized in the uniform-in-n form, matching the section's claim of constant regret and the time-uniform event of Lemma 6.
Lean's division by zero makes Xi,t and ci,t equal to 0 when Ni,t=0. Lemma 6 therefore excludes Ni,t=0 explicitly (where the paper's inequality is vacuous), and the run predicate handles unplayed arms separately. The regret bound sums over arms with Δi>0, so its divisions are well defined.
A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.
Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case (d=1, λ=1, As=1{Is=i}, Vt=1+Ni,t), a union bound over arms, and elementary inequalities inverting N↦N21+N(1+2log(d1+N/δ)). Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.
P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
Multi-armed Bandit Allocation Indices III: Superprocesses, Condition D and the Index Theorem for a SFASTextbook
Motivation
The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within ε of the index policy loses at most εγ−1(1−e−γ)−1 (Theorem 4.18).
Setting
A decision processD on a countable state space S has in each state x a nonempty finite set Γ(x) of controls; applying u yields the reward r(x,u) and moves the state by P(⋅∣x,u). Adding the freeze control, which leaves the state unchanged and yields nothing, makes D a superprocessS. Operating D under a feasible deterministic stationary Markov policy g (that is, g(x)∈Γ(x)) gives an ordinary bandit processDg, and the superprocess index is
with ν(Dg,x) the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is n superprocesses on a common (S,U); at each decision time 0,1,2,… exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by at. A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal ν(Si,xi,u).
Condition D. Let Λ be a standard bandit process with parameter λ (one state, reward λ). S satisfies Condition D if there is a function g such that, for every x and λ for which it is optimal in the family {S,Λ} to select S in state x, it is optimal to apply the control g(x). A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter μ(x); its stopping option is improving if μ(x(t)) is almost surely nondecreasing in process time.
Formalization targets
Goal: Theorem 4.3
For a decision process with bounded rewards and a Condition-D control g, every index policy with respect to ν(D,⋅,⋅) that applies g(xi) to the superprocess i it continues is optimal for the family of n superprocesses:
index policy π⟹π feasible and Rπ(x)=π′ feasiblesupRπ′(x) for every x∈Sn.
Milestones
Note 4.2 (under Condition D, S is selected in {S,Λ(λ)} iff ν(S,x)≥λ, and at λ=ν(S,x) a control u is optimal iff ν(S,x,u)=ν(S,x); the printed equivalence fails for λ<ν(S,x)); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor a is strictly increasing in ν); Theorem 4.18 (the ε-index bound, ε/(1−a)2 for the discrete-time index).
Significance
Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as ν does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.
Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.
Difficulty
The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process Dg for its Condition-D policy g and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than g(xi) to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most k times is ε-exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process Dg under charge λ. Theorem 4.8 is elementary given the value of {B,Λ} under a freezing rule, Rf(B)+λγ−1−λWf(B), but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by ε.
Formalization scope
Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with g(x)=u, bounded by the reward bound and nonempty for u∈Γ(x); for an unavailable u it is a default value that no index policy consults. Condition D is stated on the family {S,Λ} on S⊕Unit, where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of μ-index policies for the families {B,Λ}. Theorem 4.18 is on the k-armed Bandit Algorithms model with ε≥0 and the bound ε/(1−a)2: the book's εγ−1(1−e−γ)−1 is in continuous-time index units, γ/(1−a) times the discrete-time index used here, and read with the discrete index it is false for a<1/e. Theorem 4.3's index policy applies the Condition-D control g to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.
Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.
Selected references
J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 4. doi:10.1002/9780470980033
K. D. Glazebrook, Stoppable families of alternative bandit processes, Journal of Applied Probability 16(4), 1979. doi:10.2307/3213152
K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19(3), 1982. doi:10.2307/3213524
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401
Multi-armed Bandit Allocation Indices II: Jobs, Parallel Machines, Search and Bandit-Dependent DiscountingTextbook
Motivation
Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit γ↓0; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.
Setting
Jobs on parallel machines. There are n jobs with service times si>0 and weights ci, and m identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion timeCi of a job is the total service time of the jobs on its machine up to and including it; the flow time is ∑iCi and the weighted flow time∑iciCi. The load of a machine is the total service time assigned to it, and δj is its excess over the average S/m. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.
The search problem (Problem 3). A stationary object is hidden in one of n boxes, in box i with probability pi. A search of box i costs ci and finds the object with probability qi if it is there. A search policy is a sequence of boxes; after Ni unsuccessful searches of box i the posterior probability that the object is there is proportional to pi(1−qi)Ni, and the search index of the box is pi′qi/ci, the current probability of finding the object per unit cost. The expected cost of a policy is ∑kcσkPr[not found by the first k searches].
Two discount factors. Bandit process A (state space SA, kernel PA, reward rA) discounts at rate a and B at rate b; a reward obtained at time t is worth at or bt times its face value according to which process produced it. The cross indices are νAB(x)=supτ>0E∑t<τatrA(x(t))/E[1−bτ] and νBA(y) with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as E∫0τbtdt and compares νAB(x) with νBA(y) at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union SA⊕SB.
Formalization targets
Goal: Theorem 3.6
For prior probabilities pi≥0 summing to one, detection probabilities 0<qi≤1 and costs ci>0, a search policy is optimal if and only if at every step it searches a box of maximal current index pi′qi/ci:
Theorem 3.3, as the identity ∑iciCi=2κ(∑isi2+S2/m+∑jδj2) when ci=κsi; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time t, A when atνAB(x)>btνBA(y) and B when atνAB(x)<btνBA(y) attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on m machines and that the optimal schedules are exactly those placing the r-th block of m longest jobs at level r from the end, for some order of the equal jobs.
Significance
Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time t weighs the indices by at and bt, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying 0.18 (a=0.9) and 1 (b=0.5) are best played B,B,B and then A forever, which no stationary rule does.
None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.
Difficulty
For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as ∑iℓisi with ℓi the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.
Formalization scope
Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in [0,∞] of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, pi(1−qi)Niqi/ci, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an A-state by PA and a B-state by PB; the payoff is the round-by-round series ∑t(atE[r1{At=A}]+btE[r1{At=B}]), absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: m≥1, service times positive; pi≥0, ∑pi=1, 0<qi≤1, ci>0; countable state spaces, bounded rewards, a,b∈(0,1).
Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by at, bt. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.
Selected references
J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
Bandit Algorithms XIII: Pure Exploration and Best-Arm IdentificationTextbook
Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time τ and a recommendation must be sound (wrong with probability at most δ) while minimizing E[τ]. The information-theoretic complexity is c∗(ν)−1=supα∈Pk−1infν′∈Ealt(ν)∑iαiD(νi,νi′): every sound strategy needs E[τ]≥c∗(ν)log4δ1, and the Track-and-Stop algorithm — the goal theorem — achieves limδ→0E[τ]/log(1/δ)=c∗(ν) exactly. The mission also covers the fixed-budget counterpart, sequential halving.
Bandit Algorithms IV: Bernoulli Bandits and KL-UCBTextbook
When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of [0,1], and the correct exponential rate is governed by the binary relative entropy d(p,q)=plogqp+(1−p)log1−q1−p rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of d. The goal theorem shows KL-UCB attains
n→∞limsupRn/logn=i:Δi>0∑Δi/d(μi,μ∗)
— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.
Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy D(P,Q), and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event A, P(A)+Q(Ac)≥21exp(−D(P,Q)) — no test can distinguish P from Q with total error probability below 21e−D(P,Q). This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality ∫p∧q≥21(∫pq)2), Pinsker's inequality δ(P,Q)≤D(P,Q)/2, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.
Provably Efficient Reinforcement Learning with Linear Function Approximation 1: LSVI-UCB Has Regret O(√(d³H³Tι²)) with Probability 1 − p on Linear MDPsResearch Paper
Motivation
Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order H2SAT have been known since the work on UCRL and UCBVI, but they scale with the number of states S and actions A and say nothing when S is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.
Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension d and the horizon H and independent of S and A. The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.
Timeline:
2017–2018: Azar, Osband, Munos (arXiv:1703.05449) and Jin, Allen-Zhu, Bubeck, Jordan (arXiv:1807.03765) give near-optimal T regret for tabular episodic MDPs.
2019: Yang and Wang (arXiv:1902.04779) study linear transition models with a simulator; Jin, Yang, Wang, Jordan prove Theorem 3.1 below without a simulator.
2020: Zanette, Lazaric, Kochenderfer, Brunskill (arXiv:2003.00153) improve the dependence on d under a low inherent Bellman error assumption.
Setting
An episodic MDPMDP(S,A,H,P,r) has a measurable state space S, a finite action set A, a horizon H, transition kernels Ph(⋅∣x,a) and deterministic rewards rh(x,a)∈[0,1] for steps h=1,…,H. A policyπ(x,h) chooses an action at each state and step. Its value functions satisfy the Bellman equation Qhπ=rh+PhVh+1π, Vhπ(x)=Qhπ(x,π(x,h)), VH+1π=0, where PhV(x,a)=∫VdPh(⋅∣x,a); the optimal values Vh⋆, Qh⋆ satisfy the same recursion with a maximum over actions.
The MDP is linear (Assumption A) with feature map ϕ:S×A→Rd if ∥ϕ∥≤1 and for each step there are signed measures μh=(μh(1),…,μh(d)) and a vector θh with
Ph(⋅∣x,a)=⟨ϕ(x,a),μh(⋅)⟩,rh(x,a)=⟨ϕ(x,a),θh⟩,
and ∥θh∥≤d, ∥(∣μh(1)∣(S),…,∣μh(d)∣(S))∥≤d.
In each episode k=1,…,K an adversary chooses the initial state x1k; the agent then plays H steps, the next state xh+1k being drawn from Ph(⋅∣xhk,ahk). LSVI-UCB (Algorithm 1) computes, backwards over h, the Gram matrix Λhk=∑τ<kϕhτ(ϕhτ)⊤+λI of the past features ϕhτ=ϕ(xhτ,ahτ), the ridge-regression weight whk for the targets rh+maxaQh+1k, and the optimistic estimate
and then plays greedily with respect to Qhk. Its policy in episode k is πk, and the regret is
Regret(K)=k=1∑K[V1⋆(x1k)−V1πk(x1k)],T=KH.
Formalization targets
Goal: Theorem 3.1
There are absolute constants c,C>0 such that for every linear MDP, every p∈(0,1) and every run of LSVI-UCB with λ=1 and β=c⋅dHι, ι=log(2dT/p),
P(Regret(K)≤Cd3H3Tι2)≥1−p.
Milestones
The milestones follow Appendix B of the paper: linearity of Qπ (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.
A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators Thπ of (8) map linear action-value functions to linear ones for every policy, then Ph is linear in ϕ.
Significance
The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension d of the features and polynomially on H, not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.
The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures μh (see Formalization scope) and the existential reading of the weights in Lemma B.1.
Difficulty
The regression targets rh+maxaQh+1k(xh+1τ,⋅) depend on all past data through Qh+1k. The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating Vh+1k as fixed, fails because Vh+1k is not measurable with respect to the past at the time xh+1τ is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.
A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the KH steps) needs every object to be measurable with respect to the right σ-algebra.
Formalization scope
Model.S is any measurable space; A is a finite nonempty type with its discrete σ-algebra and a linear order used only to break ties in the argmax. Steps and episodes are 1-based. Vπ, Qπ, V⋆, Q⋆ are defined by the Bellman recursions (1) and (2), with value 0 outside 1≤h≤H; theorems about general policies assume them measurable.
Assumption A is stated with the total-variation normalization ∥(∣μh(i)∣(S))i∥≤d instead of the printed ∥μh(S)∥≤d; under the printed condition Lemma B.1 is false. The feature map is assumed measurable.
Runs. A run is a process on a probability space with a filtration over the flattened time (k−1)(H+1)+(h−1): states are adapted, actions are those of Algorithm 1, and the conditional law of xh+1k given the past is Ph(⋅∣xhk,ahk). The initial states are otherwise unrestricted.
Constants.c and C are quantified before the spaces, d, H, K, p, the MDP and the run; d,H,K≥1 and p∈(0,1). "With probability 1−p" is an upper bound on the outer measure of the failure event.
Ruling out trivializations. The goal does not assume the good event, optimism, or any milestone conclusion; β is fixed by the existentially quantified c, not free; the regret uses the model value of the greedy policy, not a realized return. A sorry-free check exhibits a linear MDP and a run satisfying all hypotheses.
Known gap. Algorithm 1 clips Qhk only from above, so the bound ∣Vh+1k∣≤H that Lemma B.3's proof needs (and the target bound in Lemma B.2's proof, here an explicit hypothesis) is not automatic off the good event. Lemma B.3 is stated as printed, for every cβ>0; a solver who finds it unprovable should report this in the discussion.
Infrastructure needed: covering numbers of norm balls, the self-normalized martingale bound, Azuma–Hoeffding (in Mathlib), integration against signed measures, and measurability of the algorithm's outputs. The MDP and run definitions are reusable for other episodic RL results; contributions of general lemmas about them are welcome.
Selected references
C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019. https://arxiv.org/abs/1902.04779
A. Zanette, A. Lazaric, M. Kochenderfer, E. Brunskill, Learning Near Optimal Policies with Low Inherent Bellman Error, ICML 2020. https://arxiv.org/abs/2003.00153
Optimal Best Arm Identification with Fixed Confidence III: δ-PAC Guarantee of Chernoff's Stopping Rule for Bernoulli BanditsResearch Paper
Motivation
In best arm identification with fixed confidence, a learner samples K unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk δ, while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.
Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most δ, must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold β(t,δ)=log(2t(K−1)/δ).
Setting
The arms are A={1,…,K}. A Bernoulli bandit model is a mean vector μ=(μ1,…,μK)∈[0,1]K: pulling arm a returns reward 1 with probability μa and 0 otherwise, independently of the past. The class S contains the models with a unique optimal arma∗(μ), i.e. μa∗>μi for all i=a∗.
At round t the learner chooses an arm At as a (possibly randomized) function of the past observations and observes a reward Xt. Write Na(t) for the number of pulls of arm a among the first t rounds, sa(t) for the number of those pulls that returned 1, and μ^a(t)=Na(t)−1∑s≤tXs1{As=a} for the empirical mean. The likelihood of arm a's observations under mean u is pu(XNa(t)a)=usa(t)(1−u)Na(t)−sa(t).
The GLR statistic for "arm a is at least as good as arm b" is
Chernoff's stopping rule with exploration rateβ(t,δ) is
τδ=inf{t≥1:∃a∈A,∀b=a,Za,b(t)>β(t,δ)},
and the decision rule recommends a^τδ∈argmaxaμ^a(τδ).
The Krichevsky–Trofimov (KT) distribution on binary sequences x∈{0,1}n is kt(x)=∫01(πu(1−u))−1pu(x)du, the Bernoulli likelihood mixed over the Beta(1/2,1/2) prior.
Formalization targets
Goal: Theorem 10
For every δ∈(0,1), every sampling strategy, and the threshold β(t,δ)=log(2t(K−1)/δ),
∀μ∈S,Pμ(τδ<∞,a^τδ=a∗)≤δ.
Milestone: Lemma 11 (Willems, Shtarkov and Tjalkens, 1995)
kt is a probability law on {0,1}n, and for n≥1,
x∈{0,1}nsupu∈[0,1]supkt(x)pu(x)≤2n.
Milestone: the pairwise crossing bound of Appendix C.1
With Ta,b=inf{t:Za,b(t)>β(t,δ)}, for all arms with μa<μb,
Pμ(Ta,b<∞)≤K−1δ.
Significance
Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits δ-correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.
The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.
Difficulty
The obvious approach bounds, for each fixed t, the probability that Za,b(t) exceeds β(t,δ) by a concentration inequality and sums over t. This fails: the sampling strategy is arbitrary and adaptive, so Na(t) and Nb(t) are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of Za,b is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood 1) and the boundary means 0 and 1.
Formalization scope
The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate s is round s+1) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.
Conventions committed to:
Arms are Fin K. Bernoulli means range over [0,1], degenerate laws included; the paper's exponential-family mean space is (0,1), so the [0,1] statement implies the paper's.
Za,b(t) is defined as the ratio of the two maxima over [0,1]2, not by the closed form (7), which holds only when μ^a(t)≥μ^b(t). Both maxima are attained and positive.
The stopping rule ranges over t≥1; at t=0 there is no observation and the paper's β(0,δ)=log0 is undefined. τδ=∞ when the rule never fires.
The decision rule is quantified: the goal holds for every recommendation that maximizes the empirical mean at τδ, whatever the tie-breaking.
Probabilities of events are outer measures under the trajectory law; no measurability is assumed.
K≥1 only. For K=1 the statement is trivially true (no suboptimal arm).
Disclosed deviations from the page: Lemma 11's ratio bound is stated for n≥1, since at n=0 the printed bound reads 1≤0; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as 1/πu(1−u) (a slip for 1/(πu(1−u)) of Lemma 11, which is the normalized one); the formalization follows Lemma 11.
A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.
Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.
Selected references
A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2, 2016. https://arxiv.org/abs/1602.04589
F. M. J. Willems, Y. M. Shtarkov, T. J. Tjalkens, The context-tree weighting method: basic properties, IEEE Transactions on Information Theory 41(3), 1995. https://doi.org/10.1109/18.382012
R. Krichevsky, V. Trofimov, The performance of universal encoding, IEEE Transactions on Information Theory 27(2), 1981. https://doi.org/10.1109/TIT.1981.1056331
Stochastic Linear Optimization under Bandit Feedback 1: The Regret Bound of ConfidenceBallResearch Paper
Motivation
In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision xt from a fixed set D⊆Rn and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function μ⊤xt. The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where D is the set of standard basis vectors.
Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is O∗(nT) with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).
Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the O∗(nT) bound and a matching Ω(nT) lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.
Setting
Fix n≥1 and a compact decision set D⊆Rn whose standard basis e1,…,en is a barycentric spanner: each ei∈D and every x∈D lies in the cube [−1,1]n. The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector μ∈Rn satisfies ∣μ⊤x∣≤1 for x∈D, and x∗∈D minimises μ⊤x.
On round t=1,2,… the learner plays xt∈D, measurable with respect to the information Ft before round t, and observes a loss ℓt∈[−1,1] with E[ℓt∣Ft]=μ⊤xt. The regret after T rounds is
RT=t=1∑T(μ⊤xt−μ⊤x∗).
ConfidenceBall₂(D,δ) maintains the design matrix At=I+∑τ<txτxτ⊤, the least-squares estimate μ^t=At−1∑τ<tℓτxτ, the radius
βt=max(128nlntln(t2/δ),(38ln(t2/δ))2),
and the confidence ellipsoidBt2={ν:(ν−μ^t)⊤At(ν−μ^t)≤βt}. It plays the optimistic decision xt∈argminx∈Dminν∈Bt2ν⊤x. The analysis uses the widthwt=xt⊤At−1xt, the error Zt=(μ^t−μ)⊤At(μ^t−μ), and the noise ηt=ℓt−μ⊤xt.
The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension n rather than on ∣D∣, holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor Θ∗(n). The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on logdetAt, are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.
The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).
Difficulty
The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to ∑τMτ would need a deterministic step bound, and the natural one gives only a T3/4 regret. The step sizes of Mt are bounded in terms of the random widths wt, so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event {V≤v} is random. The escape indicator Et, which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all t simultaneously. Freedman's inequality itself is not in Mathlib.
Formalization scope
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed t=1,2,… in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration (Ft); xt is Ft-measurable and ℓt is Ft+1-measurable. The argmin is encoded as a joint minimiser over D×Bt2, which admits every tie-break and is required on every outcome; measurability of xt is a hypothesis, not derived from the selection. The optimum x∗ is a hypothesis (x∗∈D, minimising), not an sInf.
Corrections of the printed statements, each labelled in the item's Formalization Note:
ln(T+1) for lnT in Lemma 9, Theorem 6 and Theorem 2. The printed bounds are false at T=1 (with n=1, D=[−1,1], μ>0, the tie-break x1=1 gives R1=2μ>0 against a bound of 0); the proof of Lemma 9 gives 2lndetAt+1≤2nln(t+1).
n≤β1=(38ln(1/δ))2 is added to Theorems 5 and 2: the proof of Theorem 5 claims Z1≤n<β1, which fails for δ near 1. Theorem 6 takes the proof's "1<β1" as the hypothesis β1≥1.
∣ℓt−μ⊤xt∣≤1 is added to Lemma 14, Theorems 5 and 2: Section 5.2 uses ∣ηt∣≤1, while the model gives only ∣ηt∣≤2. It holds when costs lie in [0,1].
Theorem 5's "δ>0" is stated with 0<δ<1; Lemma 10's index typo (wt for wτ) and Theorem 4's ∑i=1n (for T) are corrected.
A regret bound for an arbitrary decision sequence under the assumption μ∈Bt2 for all t is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and δ as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite D with a fixed tie-break and i.i.d. costs in [0,1].
Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.
P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://arxiv.org/abs/1102.2670
Multi-armed Bandit Allocation Indices I: The Gittins Index, Optimal Stopping and MonotonicityTextbook
Motivation
A decision-maker has n projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the n state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number ν(B,x), computable for each bandit process B from its own data and its own current state x, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.
The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.
Setting
A bandit processB (§2.3–2.4) is a Markov reward process on a countable state space E: transition probabilities P(y∣x), a bounded reward r(x) received each time the continuation control is applied in state x, and a discount factor a∈(0,1); the freeze control leaves the state unchanged and yields nothing. The law of the process started at x is Px and x(t) is its state at process time t=0,1,2,…. A stopping timeτ is a past-measurable rule for switching from continuation to freezing, taking values in {1,2,…}∪{∞}. For such τ, Rτ(B,x)=Ex[∑t<τatr(x(t))] is the expected discounted reward and Wτ(B,x)=Ex[∑t<τat] the expected discounted time; their ratio ντ(B,x) (2.7) is the equivalent constant reward rate of that portion of B. The Gittins index is
ν(B,x)=τ>0supWτ(B,x)Rτ(B,x)(2.6)
and, equivalently, the fair charge (2.5): the greatest rent λ per period for which continuing B for one or more periods, paying λ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is n such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted N∪{∞}-valued maps on trajectories, and gittinsIndex P r a x is (2.6).
Formalization targets
Goal: Lemma 2.2, the optimal stopping set
The supremum in (2.6) is attained. For the initial state ξ, the attaining stopping rule may be taken to be "stop at the first time t≥1 at which the state lies in Σ0" for any set Σ0 with
{x:ν(B,x)<ν(B,ξ)}⊆Σ0⊆{x:ν(B,x)≤ν(B,ξ)},
and every such rule has ντ(B,ξ)=ν(B,ξ).
Milestones
Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at τ=∞.
Significance
Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.
Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.
Difficulty
The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge λ=ν(B,ξ), whose value function satisfies φ(x)=max{0,r(x)−λ+aE[φ(x(1))∣x(0)=x]}, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities λ>ν(B,x) and λ≥ν(B,x). That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is max(0,ν/(1−a)), not ν/(1−a), because restarting forever is free.
Formalization scope
The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; a∈(0,1). The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes τ≥1 everywhere, so Wτ≥1 and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time 1 of a set, with ∞ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over {λ:profit(λ)≥0}, a nonempty set bounded above. The restart iteration is stated as a limit, with the value max(0,ν(B,ξ)/(1−a)): for a nonnegative index this is the book's ν/(1−a), and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under Px, written as events of measure one.
Two trivializing readings are excluded: the index is never taken over all N∪{∞}-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.
Selected references
J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401
Bandit feedback is only one point on a spectrum: a learner might see more than its own loss (full information) or less (a spam filter never learns what happened to mail it deleted). Chapter 37 of Lattimore–Szepesvári studies finite adversarial games G=(L,Φ) where the loss matrix and the feedback matrix are decoupled. The goal theorem is the celebrated classification theorem: every finite partial-monitoring game has minimax regret exactly 0, Θ(n), Θ(n2/3) or Ω(n) — determined by two purely combinatorial conditions, global and local observability, on the game's neighbourhood structure. A single geometric dichotomy thus governs the price of information in every online decision problem with finite actions and feedback.
Bandit Algorithms X: Stochastic Linear Bandits and LinUCBTextbook
When actions are feature vectors and the mean reward is linear — Xt=⟨θ∗,At⟩+ηt — a bandit can generalize across arms: pulling one arm reveals information about all of them. Chapter 19 of Lattimore–Szepesvári carries the optimism principle into this setting: LinUCB (a.k.a. OFUL) plays the action maximizing maxθ∈Ct⟨θ,a⟩ over the confidence ellipsoid Ct of Mission IX. The goal theorem: with probability 1−δ, R^n≤8nβnlogdetV0detVn≤8dnβnlogdλdλ+nL2 — regret O~(dn) independent of the number of actions. The combinatorial engine is the elliptical potential lemma, bounding how many times adaptively chosen directions can be surprising. Chapter 22's phased elimination with G-optimal design (Mission IX) sharpens this to O~(dnlogk) for finite action sets.
Bandit Algorithms IX: Self-Normalized Concentration and Optimal DesignTextbook
Least-squares estimation from adaptively collected data is the statistical heart of linear bandits: the actions At depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process Mt(x)=exp(⟨x,St⟩−21∥x∥Vt(λ)2) is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — P(∃t:∥St∥Vt(λ)−12≥2logδ1+logλddetVt(λ))≤δ, valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly d — the classical equivalence theorem of optimal design theory.
A Short Proof of the Gittins Index Theorem: For Finite-State Semi-Markov Bandits, Every Priority Policy Ordering States by the Index Algorithm's Indices Is OptimalResearch Paper
Motivation
The multi-armed bandit problem with discounted rewards asks how to allocate effort among n independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an n-dimensional dynamic program into n one-dimensional computations.
Several proofs followed, each with its own model and its own definition of the index:
Gittins and Jones (1974) and Gittins (1979): the original interchange proofs, with the index as a supremum over stopping times of a reward-to-time ratio.
Whittle (1980): a proof through the retirement option and the dynamic-programming equation of the multi-armed problem.
Varaiya, Walrand and Buyukkoc (1985): the largest-remaining-index algorithm for finite-state Markov bandits, which computes the indices by removing states one at a time.
Weber (1992): the "prevailing charge" proof.
Tsitsiklis (1994): the short proof formalized here, for semi-Markov bandits with finite state spaces, by induction on the total number of states, with the indices produced by an index algorithm of the largest-remaining-index type.
Setting
There are n≥1 bandit processes. Bandit i has a finite nonempty state space Xi, and X=X1∪⋯∪Xn is their disjoint union. When bandit i at state x∈Xi is played, a random reward R(x) is received, the bandit is busy for a random time T(x)≥0, and it then moves to a random state Y(x)∈Xi; the other bandits do not move. The joint law of (T(x),R(x),Y(x)) depends only on x, and different plays are independent.
A policy is a map π:X1×⋯×Xn→{1,…,n}: at time zero and at every play completion time it chooses the bandit to play from the current states. With ti the start time and Ri the reward of the i-th play and a discount rate β>0, the expected discounted reward from the initial joint state z is
Jπ(z)=E[i=1∑∞Rie−βti].
A policy is optimal if it maximizes Jπ(z) for every initial state z. A priority rule is a policy for which some ordering of X makes it always play the bandit whose current state is ordered highest.
The reward rate of a state is
r(x)=E[∫0T(x)e−βtdt]E[R(x)].(2.1)
Reducing bandit i∗ by removing a state s∗ merges every play that ends in s∗ with the following run of plays at s∗ into one composite play, whose reward rate is r^(x) of (2.3). The index algorithm repeatedly picks a state s∗ of maximal current rate, sets its indexγ(s∗) to that rate, and reduces its bandit by removing s∗ (or removes the bandit if s∗ was its last state).
Formalization targets
Goal: Theorem 2.2
Let γ be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies
γ(y)<γ(x)⟹y is ordered below x
is optimal. Ties in γ may be ordered either way, and the run may break ties in its own choices arbitrarily.
Milestones, in the order the proof uses them
(2.2), the interchange inequality E[(1−e−βτ)∫0T(s∗)r(s∗)e−βtdt]≥E[(1−e−βT(s∗))∫0τrˉ(t)e−βtdt] when rˉ≤r(s∗).
Lemma 2.1: if r(s∗)=maxxr(x), some optimal policy always plays bandit i∗ when it is at s∗.
Reduction step: optimizing within the policies giving s∗ top priority is a bandit problem with one state fewer, the reduced bandit with rates (2.3).
Theorem 2.1: some priority rule is optimal.
Pick-order optimality: a priority rule that orders the states as a run of the index algorithm picks them is optimal.
Index monotonicity: along a run, γ(s∗)≥γ(q∗) for consecutive picks s∗,q∗.
Picked-before characterization: x can be picked before y (in a run with the same indices) if and only if γ(x)≥γ(y).
Significance
The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the cμ rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.
The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.
Difficulty
Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.
Formalization scope
Bandits are indexed by Fin n (0,…,n−1), with n≥1 and each state type finite and nonempty. X is the sigma type Σ i, X i, disjoint by construction.
The law of (T(x),R(x),Y(x)) is a probability measure on R×R×Xi with T≥0 almost surely and R integrable. The model also assumes P(T(x)>0)>0, which the page leaves implicit: it makes the denominator of (2.1) nonzero.
Jπ is computed from the moments E[R(x)] and D(x,y)=E[e−βT(x);Y(x)=y]: it is the limit of the expected discounted reward of the first k plays, given by the first-step recursion. No path space is constructed. The row sums of D are below 1, so the limit exists; it never mentions rates, indices or reductions.
Policies are the paper's stationary deterministic maps of the current joint state, and optimality is within that class, for every initial state. An ordering of X is an injective ranking into N.
The reduced bandit is given by explicit formulas for its expected discounted reward, discounted duration and discounted transition data. These make the page's "transition probabilities are suitably modified" concrete, and the reduced rate is (2.3). Removing a bandit is the reduction of its last state.
The index is that of any run of the index algorithm, with arbitrary tie choices.
A formalization in which the value of a policy is defined through rates or indices, or in which γ is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.
Needed infrastructure: the convergence of the k-play values and the first-step (Bellman) equation for Jπ; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.
Selected references
J. N. Tsitsiklis, A Short Proof of the Gittins Index Theorem, Annals of Applied Probability 4(1) (1994), 194–199.
J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 1974, 241–266.
P. P. Varaiya, J. C. Walrand and C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30 (1985), 426–439. https://doi.org/10.1109/TAC.1985.1103989
Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms I: The Nonparametric Learn-then-Price Policy Has Regret at Most C(log n)^{1/2}/n^{1/4}Research Paper
Why price without knowing demand
A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand functionλ(p), the rate of purchase requests at price p, is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.
Besbes and Zeevi (2009) asked how much revenue is lost for not knowing λ. They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:
the problem is constrained by an initial inventory;
the set of prices is a continuum;
the set of possible demand functions is a nonparametric class.
This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order (logn)1/2n−1/4 in a market of size n.
Setting
Prices. Fix 0<p<p<∞ and an off pricep∞>0 outside [p,p]. The seller may charge any price in [p,p]∪{p∞}; charging p∞ stops demand.
Demand. Requests arrive as a Poisson process whose intensity at time t is λ(p(t)). Let N be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time t under a price path p(⋅) are N(∫0tλ(p(s))ds). The seller starts with inventory x and sells until either the horizon T ends or the stock runs out. The expected revenue of a policy π is Jπ(x,T;λ).
Demand class.L=L(M,K,K,m) is the set of regular demand functions satisfying Assumption 1. Regular means:
λ≥0 and λ(p∞)=0;
λ is non-increasing on [p,p], with inverse γ;
the revenue rate r(l)=lγ(l) is concave.
Assumption 1 requires:
(i) λ≤M on [p,p];
(ii) λ is K-Lipschitz and γ is K−1-Lipschitz;
(iii) maxppλ(p)≥m.
Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:
JD(x,T∣λ)=sup{∫0Tp(s)λ(p(s))ds:∫0Tλ(p(s))ds≤x}.
The regret of a policy is Rπ=1−Jπ/JD.
Scaling. In a market of size n the inventory is nx and the demand function is nλ, as in (11). The corresponding quantities are Jnπ, JnD=nJD and Rnπ.
Algorithm 1, π(τ,κ). The policy has three phases.
Learning. On [0,τ] it tests κ equally spaced prices pi=p+(i−1)(p−p)/κ, each for Δ=τ/κ time units. It estimates λ(pi) by the normalized request counts λ^(pi).
Optimization. It chooses p^u=argmaxipiλ^(pi) and p^c=argmini∣λ^(pi)−x/T∣, and sets p^=max{p^u,p^c}.
Pricing. It charges p^ on (τ,T] until the stock runs out.
Formalization targets
Goal: Proposition 1
Let τn≍n−1/4 and κn≍n1/4, and let πn=π(τn,κn). Then there is a finite constant C, independent of λ and n, such that
λ∈LsupRnπ(x,T;λ)≤n1/4C(logn)1/2(n≥2).
The constant is left unspecified, as in the paper. Its dependence on the class parameters, x and T is "somewhat complex" (p. 12), and the order (logn)1/2n−1/4 is the content of the result.
Milestones
The milestones follow the proof in the appendix, in order:
the scaling JnD=nJD (p. 12);
Fact 1, JD≥mmin{T,x/M} on L;
Lemma 1, the solution of (5): charge pD=max{pu,pc} until the stock runs out;
Lemma 2, a Poisson deviation bound;
the revenue lower bound (A-2);
Lemma 3, the learned price is near pD with high probability;
Lemma 4 and the Case 1 bound (A-11), for λ(p)≤x/T;
Lemma 5 and the Case 2 bound (A-15), for λ(p)>x/T;
the Step 4 bound Rnπ≤C12(un+τn), where un=(logn)1/2max{1/κn,(nΔn)−1/2}.
Significance
Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order n−1/2 for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.
The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:
a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
uniform (over the class) Poisson concentration bounds.
The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).
Difficulty
The obvious argument controls the estimation error at the tested prices and concludes that p^ is close to the optimal price. It breaks in two places.
First, pD is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at p^ is not controlled by the error in p^ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on γ.
Second, when demand at the highest price exceeds the inventory rate (λ(p)>x/T), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.
Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.
Formalization scope
Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space (Ω,P), a published platform definition: ℕ-valued, N(0)=0, monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating N at cumulative intensities.
Inventory. The inventory of the market of size n is ⌊nx⌋ units, and sales are min{N(⋅),⌊nx⌋}. The cap is never dropped.
Revenue.Jnπ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
Demand functions. A demand function is a map R→R, nonnegative, with λ(p∞)=0. Regularity and Assumption 1 are imposed on [p,p], and the inverse γ is Function.invFunOn.
Benchmark.JD is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
Algorithm. The grid excludes p, as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare λ^(pi) with x/T.
Tuning.τn≍n−1/4 and κn≍n1/4 are encoded with explicit constants 0<c≤c′, with τn∈(0,T] and κn≥1. Constants may depend on c,c′, the class parameters, the prices, x and T, but never on λ or n.
Range of n. Bounds whose right side vanishes at n=1 because log1=0 are stated for n≥2: the goal and (A-15).
Typo correction. Lemma 5's event uses nx−C9nun, as in its proof, not the printed nx−C9un.
Ruled out. A specific demand curve, a fixed n, deterministic demand, a finite price set, a known λ, constants depending on λ, or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 (Jπ≤JD for all admissible policies) are not included.
Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.
Selected references
O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999