Canonical bandit histories preserve prefix expectations

Proved

BanditAlgorithm.banditExplorationPrefix_integral

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

bandit-algorithmsmeasure-theoryprobability

Let B_{ν,π}^r be the canonical law of a k-armed bandit history after r rounds under environment ν and policy π. Fix m and a horizon r ≥ mk. For every integrable real functional g of the first mk rounds,

\mathbb E_{B_{\nu,\pi}^r}\!\left[g(H_{1:mk})\right] = \mathbb E_{B_{\nu,\pi}^{mk}}\!\left[g(H)\right].

Moreover, the pullback h ↦ g(h_{1:mk}) is integrable under B_{ν,π}^r.

This is the reusable prefix-marginal consistency property of the canonical bandit history law. It lets finite-horizon events proved at an exploration cutoff be used unchanged at every later horizon.

Formalization Note The prefix map is banditExplorationPrefix.

Preamble

import Definitions.Def_etcPolicy

open MeasureTheory ProbabilityTheory

Formal statement

namespace BanditAlgorithm

theorem banditExplorationPrefix_integral
    {k m r : ℕ} {ν : StochasticBandit k} {π : BanditPolicy k}
    (hr : m * k ≤ r) (g : BanditHistory k (m * k) → ℝ)
    (hg : Integrable g (banditMeasure ν π (m * k))) :
    Integrable
        (fun h : BanditHistory k r ↦ g (banditExplorationPrefix hr h))
        (banditMeasure ν π r) ∧
      ∫ h, g (banditExplorationPrefix hr h) ∂banditMeasure ν π r =
        ∫ h₀, g h₀ ∂banditMeasure ν π (m * k) := by
  sorry

end BanditAlgorithm

Source

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (CUP 2020), Section 4.6 (canonical bandit model), printed p. 65 / PDF p. 74, together with Chapter 6, Algorithm 1, https://tor-lattimore.com/downloads/book/book.pdf

View graph