MDP minimax regret lower bound (strengthened diameter hypothesis)
ProvedBanditAlgorithm.mdp_regret_lower_bound_large_diameter(MDP minimax lower bound; L&S Theorem 38.7, with the diameter hypothesis strengthened) There is a universal constant such that for all , , and : for any policy there exists an MDP with states, actions, rewards in and diameter at most (stated via the -valued diameter, which forces to be strongly connected) and an initial state distribution such that
Why the hypothesis differs from the book. L&S state this with , which appears too weak. In the §38.7 construction the diameter is realised by the pair and equals , so forces ; a tree with leaves needs depth , so at the boundary and the sojourn collapses to . The in is the sojourn — each decision carries rounds of reward consequence but returns one bit of feedback — so with the construction yields only . The original paper (Jaksch, Ortner & Auer, JMLR 11 (2010) 1563-1600, Thm 5) assumes with . The form used here implies both and and keeps uniformly, so no case split for small is needed. The constant is not optimised: any leaving slack works.
import Definitions.Def_FiniteMDPLearning import Mathlib.Data.Real.Sqrt import Mathlib.Analysis.SpecialFunctions.Log.Basic open MeasureTheory ProbabilityTheory
theorem BanditAlgorithm.mdp_regret_lower_bound_large_diameter :
∃ C : ℝ, 0 < C ∧
∀ S A n : ℕ, ∀ D : ℝ, 3 ≤ S → 2 ≤ A →
20 * (1 + Real.log S / Real.log A) ≤ D → D * S * A ≤ n →
∀ π : MDPPolicy S A,
∃ M : FiniteMDP S A, ∃ μ0 : MDPStateDistribution S,
mdpDiameterENN M ≤ ENNReal.ofReal D ∧
C * Real.sqrt (D * S * A * n) ≤
∫ h, mdpRegret M n h ∂(mdpMeasure M μ0 π n) := by
sorry