BanditAlgorithm.bandit_regret_decomposition

Proved

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

bandits

(Regret decomposition) For any policy $\pi$ and $k$ -armed bandit $\nu$ with finite means,

R_n = \sum_{i=1}^k \Delta_i\, \mathbb{E}[T_i(n)],

where $T_i(n) = \sum_{t=1}^n \mathbb{1}\{A_t = i\}$ is the number of pulls of arm $i$ .

Preamble

import Definitions.Def_banditRegret


open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.bandit_regret_decomposition {k : ℕ} (ν : StochasticBandit k)
    (hInt : ∀ i, Integrable id (ν.P i)) (π : BanditPolicy k) (n : ℕ) :
    banditRegret ν π n =
      ∑ i, banditGap ν i *
        ∫ h, (armPullCount i h : ℝ) ∂(banditMeasure ν π n) := by
  sorry

Source

L&S Lemma 4.5, p.62

View graph