D-Tracking: a -free policy whose allocation converges to
ProvedBanditAlgorithm.exists_optimal_tracking_policy(D-Tracking, existence of an optimal tracking sampling rule; L&S Algorithm 21 lines 4–7, Garivier–Kaufmann Lemma 8) There is a single policy — not depending on the confidence level — such that for every unit-variance Gaussian bandit with a unique optimal arm there is an allocation attaining the supremum in
for which, almost surely, the empirical allocation converges to it: for every arm .
The witness is the sampling rule of Algorithm 21: at each round, if play (forced exploration), and otherwise play , where is the optimal allocation of the empirical bandit. The forced-exploration step guarantees every arm is played order times, hence ; continuity of at (which is where the uniqueness of the optimal arm is used) then gives , and the tracking step converts that into convergence of the realised allocation.
That the policy does not depend on is essential: L&S Theorem 33.6 asserts a single policy together with a family of stopping rules indexed by , and this node supplies the policy.
L&S remark (§33.3 discussion) that the forced-exploration step is rarely useful in practice but genuinely necessary here: without it, when the strategy can fail to terminate with positive probability.
import Definitions.Def_TrackAndStop import Definitions.Def_GaussianBandit open MeasureTheory ProbabilityTheory InformationTheory NNReal ENNReal Filter
theorem BanditAlgorithm.exists_optimal_tracking_policy {k : ℕ} [NeZero k] :
∃ π : BanditPolicy k, ∀ ν ∈ Set.range (gaussianBandit (k := k)),
(∃! i, i ∈ banditOptimalArms ν) →
∃ α : Fin k → ℝ≥0,
IsOptimalAllocation ν (Set.range (gaussianBandit (k := k))) α ∧
∀ᵐ ω ∂banditTrajMeasure ν π, ∀ i : Fin k,
Tendsto (fun t : ℕ ↦ trajAllocation i t ω) atTop (nhds ((α i : ℝ))) := by
sorry