LeanMachineLearning

2.6. Online.Bandit.Algorithms.Regret.BayesRegretTS🔗

Bayesian regret of Thompson sampling

This file provides a Bayesian regret upper bound (integral_regret_le) for Thompson sampling under the assumption (among others) that it has the correct prior over environments.

The Bayesian regret upper bound relies on a clipped upper confidence bound whose definition and properties are also given in this file.

Main definitions

  • ucb A R l u σ2 δ a n : clipped upper confidence bound used in the regret analysis of Thompson sampling for a sequence of actions A : ℕ → Ω → Fin K, rewards R : ℕ → Ω → ℝ, reward lower bound l : ℝ, reward upper bound u : ℝ, sub-Gaussian variance proxy σ2 : ℝ, confidence parameter δ : ℝ, action a : Fin K, and time n : ℕ.

  • ucb' n h l u σ2 δ a: clipped upper confidence bound for action a : Fin K at time n : ℕ given the history h : Iic n → Fin K × ℝ (rather than the entire sequences of actions and rewards).

Main results

  • integral_regret_le: if Thompson sampling has the correct prior over environments and every environment has K actions, each of which has a corresponding reward between l and u that is sub-Gaussian with variance proxy σ2 after its mean is subtracted, then the Bayesian regret at time n is at most (2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n).

Module LeanMachineLearning.Online.Bandit.Algorithms.Regret.BayesRegretTS contains 15 exposed declarations.