ETC wrong-commit probability at the exploration cutoff

Open

BanditAlgorithm.etc_commit_probability_at_exploration_end

by Zehao Jin · Aug 20, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bandit-algorithmsconcentrationprobability

Let k > 0 and m ≥ 1. Consider a 1-subgaussian k-armed bandit and a policy whose first mk rounds pull the arms in deterministic round-robin order. Let C be a measurable commitment rule at the end of exploration that maximizes the empirical mean. Then for every arm i, the commitment indicator is integrable and

\mathbb P(C=i) \le \exp\!\left(-\frac{m\Delta_i^2}{4}\right),

where Δ_i is the gap between the optimal mean and the mean of arm i. The statement includes optimal arms, for which Δ_i = 0 and the bound is one.

This isolates the concentration estimate in Eq. (6.3), independently of the later occupation-count and regret algebra.

Formalization Note Measurability of C is encoded by identifying the policy kernel at the commitment time with the Dirac kernel at C.

Preamble

import Definitions.Def_etcPolicy

open MeasureTheory ProbabilityTheory

Formal statement

namespace BanditAlgorithm

theorem etc_commit_probability_at_exploration_end
    {k : ℕ} (hk : 0 < k)
    {ν : StochasticBandit k}
    (hν : IsSubgaussianBandit 1 ν)
    {m : ℕ} (hm : 1 ≤ m) {π : BanditPolicy k}
    (commit : BanditHistory k (m * k) → Fin k)
    (hmax : ∀ h₀ : BanditHistory k (m * k), ∀ j : Fin k,
      armEmpiricalMean j h₀ ≤ armEmpiricalMean (commit h₀) h₀)
    (hexplore : ∀ (n : ℕ) (h : BanditHistory k n) (hlt : n < m * k),
      (π.select n) h = Measure.dirac ⟨n % k, Nat.mod_lt n hk⟩)
    (hcommit : ∀ h : BanditHistory k (m * k),
      (π.select (m * k)) h = Measure.dirac (commit h))
    (i : Fin k) :
    Integrable (fun h : BanditHistory k (m * k) ↦
      if commit h = i then (1 : ℝ) else 0) (banditMeasure ν π (m * k)) ∧
    ∫ h, (if commit h = i then (1 : ℝ) else 0) ∂banditMeasure ν π (m * k) ≤
      Real.exp (-(m * (banditGap ν i) ^ 2) / 4) := by
  sorry

end BanditAlgorithm

Source

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (CUP 2020), Section 6.1, Theorem 6.1, Eq. (6.3), printed pp. 92–93 / PDF pp. 101–102, https://tor-lattimore.com/downloads/book/book.pdf

View graph