ETC exploration occupation at commitment

Proved

BanditAlgorithm.etc_arm_expected_pull_count_at_commit_time

by Hartmann_Psi · Jul 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

banditsprobability

Let $k>0$ , let $m\ge0$ , and run the round-robin exploration phase of Explore-Then-Commit for $mk$ rounds. Every arm $i$ is pulled exactly $m$ times, hence

\mathbb E[T_i(mk)]=m.

This is the exploration occupation identity used in Eq. (6.2). It is deterministic and remains valid for $m=0$ ; the reward laws need no tail assumption.

Formalization Note The expectation is the integral of the arm-pull count under the canonical bandit history measure.

Preamble

import Definitions.Def_etcPolicy

open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.etc_arm_expected_pull_count_at_commit_time
    {k : ℕ} (hk : 0 < k)
    {ν : BanditAlgorithm.StochasticBandit k}
    {m : ℕ} {π : BanditAlgorithm.BanditPolicy k}
    (hπ : BanditAlgorithm.IsETCPolicy hk m π) (i : Fin k) :
    MeasureTheory.integral (BanditAlgorithm.banditMeasure ν π (m * k))
        (fun h : BanditAlgorithm.BanditHistory k (m * k) ↦
          (BanditAlgorithm.armPullCount i h : ℝ)) = m := by
  sorry

Source

Lattimore and Szepesvari, Bandit Algorithms (CUP 2020), Section 6.1, Theorem 6.1, printed p. 92 / PDF p. 101, Eq. (6.2).

View graph