UCRL2 admits an optimistic phase run on the confidence event
ProvedBanditAlgorithm.mdp_ucrl2_optimistic_phase_run_on_confidence_eventFix states, actions, a horizon , a confidence level and a known reward function with values in . There is a policy, depending on these known quantities but not on the transition matrix, such that for every communicating MDP with reward function and diameter and every initial state distribution there is an event with such that every trajectory lying in and in the confidence good event admits an optimistic phase run.
Recall that an optimistic phase run of a trajectory consists of a partition of the rounds into consecutive phases , , together with a gain , a bias and a transition matrix per phase, subject to , optimism , span , the Bellman equation along the realised trajectory, and explicit bounds on the accumulated estimation error and martingale fluctuation.
This is everything in the analysis of UCRL2 (Lattimore--Szepesvari, Sections 38.5 and 38.6) except the concentration of the confidence balls themselves, which is assumed here as membership in mdpConfidenceGoodEvent. The policy is UCRL2: it proceeds in phases ended by the doubling criterion, which gives the bound on ; at the start of each phase it plays the memoryless deterministic action map of a solution of the Bellman optimality equation of the extended MDP built from the confidence balls, which gives optimism, the span bound and the Bellman equation as soon as the true rows lie in those balls. The estimation error is then bounded by Hoelder's inequality against the radii together with the doubling bound on , and the remaining event is the one on which the martingale of the run does not deviate, controlled by Azuma--Hoeffding.
Formalization Note The states and actions of the trajectory are named by functions on agreeing with below , so that the terminal state, which the trajectory does not record but the telescoping and the martingale term refer to, may be supplied as extra data.
import Definitions.Def_UCRL2ConfidenceSets open MeasureTheory ProbabilityTheory ENNReal
theorem BanditAlgorithm.mdp_ucrl2_optimistic_phase_run_on_confidence_event
(S A n : ℕ) (hS : 2 ≤ S) (hA : 0 < A) (hn : 0 < n)
(δ : ℝ) (hδ : δ ∈ Set.Ioo (0 : ℝ) 1)
(r : Fin S → Fin A → ℝ) (hr : ∀ s a, r s a ∈ Set.Icc (0 : ℝ) 1) :
∃ π : MDPPolicy S A,
∀ M : FiniteMDP S A, M.r = r → M.IsCommunicating → 1 ≤ mdpDiameter M →
∀ μ0 : MDPStateDistribution S,
∃ E : Set (MDPTrajectory S A n),
mdpMeasure M μ0 π n Eᶜ ≤ ENNReal.ofReal (δ / 2) ∧
∀ h ∈ mdpConfidenceGoodEvent M n δ ∩ E,
∃ (st : ℕ → Fin S) (act : ℕ → Fin A) (K : ℕ) (τ : ℕ → ℕ)
(ρ : ℕ → ℝ) (v : ℕ → Fin S → ℝ) (q : ℕ → Fin S → Fin S → ℝ),
(∀ t : Fin n, h t = (st t, act t)) ∧
τ 0 = 0 ∧ τ K = n ∧ (∀ k, τ k ≤ τ (k + 1)) ∧
(K : ℝ) ≤ 3 * Real.sqrt (S * A * n) ∧
(∀ k < K, mdpOptimalGain M ≤ ρ k) ∧
(∀ k < K, ∀ x y : Fin S, v k x - v k y ≤ mdpDiameter M) ∧
(∀ k < K, ∀ t ∈ Finset.Ico (τ k) (τ (k + 1)),
ρ k + v k (st t)
= M.r (st t) (act t) + ∑ s', q k (st t) s' * v k s') ∧
(∑ k ∈ Finset.range K, ∑ t ∈ Finset.Ico (τ k) (τ (k + 1)),
∑ s', (q k (st t) s' - (M.P (st t) (act t) s' : ℝ)) * v k s'
≤ mdpDiameter M * (Real.sqrt 2 + 1) *
Real.sqrt (14 * S * Real.log (2 * S * A * n / δ)) *
Real.sqrt (S * A * n)) ∧
(∑ k ∈ Finset.range K, ∑ t ∈ Finset.Ico (τ k) (τ (k + 1)),
((∑ s', (M.P (st t) (act t) s' : ℝ) * v k s') - v k (st (t + 1)))
≤ mdpDiameter M * Real.sqrt (2 * n * Real.log (2 / δ))) := by
sorry