KL-UCB optimal-index underestimation count bound

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

This is the optimal-arm index-underestimation estimate used in the KL-UCB analysis.

Consider a finite Bernoulli bandit and fix an optimal arm $a$, a comparison arm $i$, a horizon $n$, and a tolerance $0<\varepsilon<\Delta_i$. Let $L_{a,i,\varepsilon}(n)$ count selections of $i$ made during initialization or while the KL-UCB index of $a$ is at most $\mu^\star-\varepsilon$. Then

The bound is the canonical-bandit count form of the stopping-time estimate in Lemma 10.7 and controls how long the optimal arm can have an index substantially below its true mean.

Formalization Note The hypothesis $\varepsilon<\Delta_i$ is the regime used in Theorem 10.6; for Bernoulli means it ensures that the index threshold lies strictly inside the relevant parameter interval. The first count also absorbs the selected initialization round.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.klucb_optimal_underestimation_count_bound
    {k : ℕ} (μvec : Fin k → ℝ)
    (hμ : ∀ i, μvec i ∈ Set.Icc (0 : ℝ) 1)
    (ν : BanditAlgorithm.StochasticBandit k)
    (hν : ν = BanditAlgorithm.bernoulliBandit μvec hμ)
    {π : BanditAlgorithm.BanditPolicy k}
    (n : ℕ) (a i : Fin k) (ε : ℝ)
    (ha : BanditAlgorithm.banditArmMean ν a =
      BanditAlgorithm.banditOptimalMean ν)
    (hε : 0 < ε)
    (hεlt : ε < BanditAlgorithm.banditGap ν i) :
    MeasureTheory.integral (BanditAlgorithm.banditMeasure ν π n)
        (fun h ↦
          (BanditAlgorithm.klucbFailureCount ν a i ε h).1) ≤
      2 / ε ^ 2 := by
  sorry

The underestimation count is bounded for an arbitrary policy, allowing one that never initializes the optimal arm.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Require IsKLUCBPolicy k n π with the source initialization rule, in addition to the stated distribution and gap hypotheses.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.