Prove2Me

One-step KL increment for a stopped bandit experiment

Proved
BanditAlgorithm.bandit_stopped_klDiv_one_step

by Harry_Xu · Jul 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditsinformation-theorystopping-times

Run the same adaptive kk-armed bandit policy π\pi in two environments ν=(Pi)i=1k\nu=(P_i)_{i=1}^k and ν′=(Pi′)i=1k\nu^{\prime}=(P_i^{\prime})_{i=1}^k, and let τ\tau be a stopping time. Let Pν,τ∧nπP^{\pi}_{\nu,\tau\wedge n} and Pν′,τ∧nπP^{\pi}_{\nu^{\prime},\tau\wedge n} denote the two trajectory laws restricted to the sigma-algebra observed by time τ∧n\tau\wedge n. Then, for every n≥0n\ge 0,

D ⁣(Pν,τ∧(n+1)π ∥ Pν′,τ∧(n+1)π)≤D ⁣(Pν,τ∧nπ ∥ Pν′,τ∧nπ)+∑i=1kPν,π(n<τ, An+1=i) D(Pi∥Pi′).D\!\left(P^{\pi}_{\nu,\tau\wedge(n+1)}\,\middle\Vert\,P^{\pi}_{\nu^{\prime},\tau\wedge(n+1)}\right) \le D\!\left(P^{\pi}_{\nu,\tau\wedge n}\,\middle\Vert\,P^{\pi}_{\nu^{\prime},\tau\wedge n}\right) + \sum_{i=1}^{k} \mathbb P_{\nu,\pi}(n<\tau,\ A_{n+1}=i)\,D(P_i\Vert P_i^{\prime}).

This is the one-round chain-rule increment for a stopped adaptive experiment. Iterating it yields the expected-information bound at a bounded stopping time, and the extended-nonnegative-real formulation also covers singular arm laws.

Formalization Note Rounds are zero-indexed, so the coordinate ωn\omega_n represents (An+1,Xn+1)(A_{n+1},X_{n+1}). The stopped laws are represented by trimming the infinite trajectory measures to Mathlib’s stopped measurable spaces.

Preamble
import Definitions.Def_BanditTrajectory

open MeasureTheory ProbabilityTheory InformationTheory ENNReal
Formal statement
theorem BanditAlgorithm.bandit_stopped_klDiv_one_step
    {k : ℕ} (ν ν' : StochasticBandit k) (π : BanditPolicy k)
    (τ : (ℕ → Fin k × ℝ) → ℕ∞) (hτ : IsBanditStoppingTime τ) (n : ℕ) :
    @klDiv (ℕ → Fin k × ℝ) (hτ.min_const (n + 1)).measurableSpace
        ((banditTrajMeasure ν π).trim
          (hτ.min_const (n + 1)).measurableSpace_le)
        ((banditTrajMeasure ν' π).trim
          (hτ.min_const (n + 1)).measurableSpace_le) ≤
      @klDiv (ℕ → Fin k × ℝ) (hτ.min_const n).measurableSpace
          ((banditTrajMeasure ν π).trim (hτ.min_const n).measurableSpace_le)
          ((banditTrajMeasure ν' π).trim (hτ.min_const n).measurableSpace_le) +
        ∑ i, (banditTrajMeasure ν π)
            {ω | (n : ℕ∞) < τ ω ∧ (ω n).1 = i} *
          klDiv (ν.P i) (ν'.P i) := by
  sorry
Source
Lattimore and Szepesvári, Bandit Algorithms (CUP 2020), Exercise 15.7, printed p. 211: stopped likelihood-ratio chain rule and truncation argument extending Lemma 15.1; compare Lemma 15.1, Eqs. (15.1)–(15.2), printed pp. 198–199.

View graph