BanditAlgorithm.bandit_regret_decomposition

Proved

by Shuze Chen · Jul 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Notation (all unfolded from the imported definitions). Fix $k \ge 0$ and a $k$ -armed stochastic bandit $\nu$ : probability measures $P_0, \dots, P_{k-1}$ on $\mathbb{R}$ , with arm means $\mu_i = \int x \, dP_i$ , optimal mean $\mu^* = \sup_i \mu_i$ ( $= 0$ by convention when $k = 0$ ), and gaps $\Delta_i = \mu^* - \mu_i$ . A policy $\pi$ is a family of Markov kernels $\pi_n$ from length- $n$ histories $h : t \mapsto (A_t(h), X_t(h))$ to arms; $\mathbb{P}^n_{\nu,\pi}$ is the history measure defined by $\mathbb{P}^0 = \delta_{()}$ and $\mathbb{P}^{m+1} = (\mathbb{P}^m \otimes K_m) \circ \mathrm{append}^{-1}$ , where $K_m$ draws $a \sim \pi_m(\cdot \mid h)$ then $x \sim P_a$ . Write $T_i(h)$ for the number of rounds of $h$ playing arm $i$ , and

R_n(\nu,\pi) = n\,\mu^* - \int \Big(\sum_{t<n} X_t(h)\Big) d\mathbb{P}^n_{\nu,\pi}(h)

for the regret (with the convention that a non-integrable integrand makes the integral $0$ ).

Claim. For every $k \ge 0$ , every bandit $\nu$ such that $x \mapsto x$ is $P_i$ -integrable for every arm $i$ , every policy $\pi$ , and every horizon $n \in \mathbb{N}$ :

R_n(\nu, \pi) \;=\; \sum_{i=0}^{k-1} \Delta_i \int_{\mathcal{H}_n} T_i(h) \, d\mathbb{P}^n_{\nu,\pi}(h).

Hypotheses:

integrability of the identity under each $P_i$ — nothing more (no subgaussianity, no boundedness, no moment conditions beyond the first);
no positivity constraint on $k$ or on $n$ .

Edge cases:

The statement is an exact equality, not an inequality in either direction.
Each pull count satisfies $0 \le T_i(h) \le n$ , so the right-hand integrands are bounded; the total-reward integrand inside $R_n$ carries no integrability hypothesis, and if it is not $\mathbb{P}^n$ -integrable its integral is the junk value $0$ — the claimed equality is asserted for that case too.
For $k = 0$ no policy exists (a Markov kernel into an empty arm set is impossible), so the statement is vacuous there; for $n = 0$ both sides are $0$ .

Human review

Endorsed by Community (Bot) · Jul 17, 2026
Endorsed by Shuze Chen · Jul 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph