Exp3 generic expected-regret bound

Proved

BanditAlgorithm.exp3_expected_regret_generic_bound

by LukeBernese · Jul 18, 2026 · Mathlib c5ea003 (Lean v4.30.0)

For an adversarial $k$ -armed bandit with rewards in $[0,1]$ , horizon $n\ge 1$ , and an Exp3 policy with any positive learning rate $\eta$ , the expected regret satisfies

R_n(\pi,x)\le \frac{\log k}{\eta}+\frac{\eta n k}{2}.

This is the pre-optimization estimate obtained by taking expectations in Eq. (11.15).

Preamble

import Definitions.Def_AdversarialBandit
import Definitions.Def_exp3Policy

open MeasureTheory ProbabilityTheory

Formal statement

namespace BanditAlgorithm

theorem exp3_expected_regret_generic_bound
    {k : ℕ} (hk : 1 < k) (n : ℕ) (hn : 0 < n)
    (x : ℕ → Fin k → ℝ) (hx : ∀ t : ℕ, ∀ i : Fin k, x t i ∈ Set.Icc (0 : ℝ) 1)
    (π : BanditPolicy k) (η : ℝ) (hη : 0 < η) (hπ : IsExp3Policy η π) :
    adversarialRegret n x π ≤ Real.log k / η + η * n * k / 2 := by
  sorry

end BanditAlgorithm

Source

Lattimore and Szepesvári, Bandit Algorithms (CUP 2020), Theorem 11.2 proof, printed pp. 156–157, especially Eq. (11.15) and the expectation calculation immediately following it. https://tor-lattimore.com/downloads/book/book.pdf

View graph