Track-and-Stop upper bound: \\limsup_{\\delta\\to0}\\mathbb{E}[\\tau_\\delta]/\\log(1/\\delta)\\le c^*(\\nu)
ProvedBanditAlgorithm.best_arm_identification_track_and_stop_upper_bound(Track-and-Stop, upper half of Theorem 33.6) Over the class of unit-variance Gaussian bandits there exist a policy (not depending on ) and, for each confidence level , a stopping time of the natural filtration together with an -measurable recommendation rule , such that:
- Soundness. Each triple is -sound for .
- Finiteness. For every with a unique optimal arm and every , the expected stopping time is finite.
- Asymptotic upper bound. For every such and every , eventually as ,
Clause 3 is the statement , written in its -form so that it is free of the junk values a real-valued limsup takes on a function that is not bounded above.
This is the upper half of L&S Theorem 33.6; the matching lower half is Theorem 33.5, on the platform as BanditAlgorithm.best_arm_identification_sample_complexity_lower_bound. Together the two halves give the limit asserted by Theorem 33.6, and the reduction performing that squeeze is already accepted against the root.
Where the three clauses come from, and a constant that must be watched.
L&S only sketch Theorem 33.6 (p. 410: "we sketch the proof ... a more complete outline is given in Exercise 33.6"), so the pieces have to be assembled from two places.
Clause 1 (soundness) is L&S Lemma 33.7, which is specific to Gaussian bandits: with on and the threshold
the Chernoff stopping rule satisfies — exactly, at every , with no inflation of the leading constant, because .
This is the reason clause 1 and clause 3 can hold simultaneously with the constant itself. It is worth being explicit that the analogous general-exponential-family result of Garivier & Kaufmann (COLT 2016), their Proposition 12, does not suffice here: it requires in the threshold , and combining it with their Theorem 14 yields only for — as they themselves summarise ("combining Proposition 12 and Theorem 14, one obtains for every ..."). Anyone attacking this node through the general exponential-family route will land on and miss the statement; the Gaussian threshold of Lemma 33.7 is what closes the gap.
Clauses 2 and 3 are the content of Garivier & Kaufmann's Proposition 13 (almost-sure finiteness and integrability of — a separate result, not a corollary of the expectation bound, which is why finiteness is carried here as its own clause: without it the ENNReal.toReal in the root would silently read as ) and Theorem 14 (the bound). Their dependencies: forced-exploration concentration (Lemma 19), the tracking lemmas (7 and 8), and a Lambert- estimate (Lemma 18). None of these exist in Mathlib.
A bookkeeping caveat for the : Theorem 14 is stated for with , , and gives , whereas L&S's threshold has , i.e. . The in Theorem 14 is an artefact of the explicit (deliberately lossy) solution of supplied by their Lemma 18: the least such is , not . Since and the polynomial factor contributes only , the true asymptotics are for any polynomial — which is exactly what L&S's proof sketch asserts. A formal proof should therefore redo the Lemma 18 step without the inflation rather than cite Theorem 14 verbatim.
import Definitions.Def_BanditTrajectory import Definitions.Def_GaussianBandit open MeasureTheory ProbabilityTheory Filter ENNReal
theorem BanditAlgorithm.best_arm_identification_track_and_stop_upper_bound {k : ℕ}
(hk : 0 < k) :
∃ (π : BanditPolicy k) (τ : ℝ → (ℕ → Fin k × ℝ) → ℕ∞)
(ψ : ℝ → (ℕ → Fin k × ℝ) → Fin k),
(∀ δ ∈ Set.Ioo (0 : ℝ) 1,
∃ hτ : IsBanditStoppingTime (τ δ),
Measurable[hτ.measurableSpace] (ψ δ) ∧
IsSoundBAI δ π (τ δ) (ψ δ) (Set.range (gaussianBandit (k := k)))) ∧
∀ ν ∈ Set.range (gaussianBandit (k := k)), (∃! i, i ∈ banditOptimalArms ν) →
(∀ δ ∈ Set.Ioo (0 : ℝ) 1,
∫⁻ ω, (τ δ ω : ℝ≥0∞) ∂banditTrajMeasure ν π ≠ ⊤) ∧
∀ ε : ℝ, 0 < ε →
∀ᶠ δ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
(∫⁻ ω, (τ δ ω : ℝ≥0∞) ∂banditTrajMeasure ν π).toReal / Real.log (1 / δ)
≤ (baiComplexity ν (Set.range (gaussianBandit (k := k)))).toReal + ε := by
sorry