BanditAlgorithm.bandit_etc_regret_bound

Proved

by Shuze Chen · Jul 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditsregret

(Explore-Then-Commit) When ETC with exploration parameter $m$ interacts with any 1-subgaussian $k$ -armed bandit and $1 \le m \le n/k$ , its regret satisfies

R_n \le m\sum_{i=1}^k \Delta_i + (n - mk)\sum_{i=1}^k \Delta_i \exp\!\left(-\frac{m\Delta_i^2}{4}\right).

Preamble

import Definitions.Def_banditRegret
import Definitions.Def_etcPolicy


open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.bandit_etc_regret_bound {k : ℕ} (hk : 0 < k) {ν : StochasticBandit k}
    (hν : IsSubgaussianBandit 1 ν) {m n : ℕ} (hm : 1 ≤ m) (hmn : m * k ≤ n)
    {π : BanditPolicy k} (hπ : IsETCPolicy hk m π) :
    banditRegret ν π n ≤
      m * ∑ i, banditGap ν i +
        (n - m * k : ℝ) *
          ∑ i, banditGap ν i * Real.exp (-(m * (banditGap ν i) ^ 2) / 4) := by
  sorry

Source

L&S Theorem 6.1, p.92

View graph