One-sided Azuma–Hoeffding along an MDP trajectory

Proved

BanditAlgorithm.mdp_trajectory_azuma_of_centered_bounded_increments

by Grace · Aug 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

concentrationprobabilityreinforcement-learning

Fix a finite MDP $M$ , an initial state distribution, a policy and a horizon $n$ . Let $G$ assign to a trajectory $h$ , a time $t$ and a state $s'$ a real number $G_h(t,s')$ , and suppose that

$G_h(t,\cdot)$ depends on $h$ only through the rounds $0,\dots,t$ ;
$\sum_{s'}P_{A_t}(S_t,s')\,G_h(t,s')=0$ for every $t<n$ and every $h$ , where $(S_t,A_t)$ is the round played at time $t$ ;
$|G_h(t,s')|\le c$ for all $t,h,s'$ .

Then for every $\varepsilon\ge0$ ,

\mathbb{P}\Big(\sum_{t<n-1}G_h\big(t,S_{t+1}\big)\ \ge\ \varepsilon\Big)\ \le\ \exp\Big(\frac{-\varepsilon^{2}}{2(n-1)c^{2}}\Big).

This is the Azuma--Hoeffding inequality along the trajectory of a finite MDP. The first hypothesis says that the summand is predictable: it is determined by the history up to time $t$ together with the single new state $S_{t+1}$ . The second says that, given that history, the summand has conditional mean zero, because conditionally on the history the state $S_{t+1}$ is drawn from the true row $P_{A_t}(S_t,\cdot)$ ; the partial sums are therefore a martingale for the filtration generated by the rounds. The third bounds its increments uniformly, so Hoeffding's lemma applies at each step. The statement is one-sided, which is what the regret analysis of an optimistic algorithm needs, and no assumption is made on the policy: it may depend on the whole past in an arbitrary way.

Formalization note. The rounds are indexed by Fin n, so the state at time $t+1$ is exposed by quantifying over sequences st, act that agree with the trajectory; the deviation event is the set of trajectories admitting such a pair with a large sum. The sum runs over $t<n-1$ because the state following the last recorded round is not part of a trajectory of $n$ rounds. When $n\le1$ the right-hand side is $1$ and the statement is vacuous.

Source: Azuma--Hoeffding; the use made of it here is Jaksch, Ortner and Auer, Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11 (2010), Section 4.3, and Lattimore and Szepesvari, Bandit Algorithms (CUP 2020), Section 38.5.

Preamble

import Definitions.Def_FiniteMDPLearning

open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.mdp_trajectory_azuma_of_centered_bounded_increments
    {S A : ℕ} (n : ℕ) (M : FiniteMDP S A) (μ0 : MDPStateDistribution S)
    (π : MDPPolicy S A) (G : MDPTrajectory S A n → ℕ → Fin S → ℝ)
    (c : ℝ) (hc : 0 ≤ c)
    (hdep : ∀ (t : ℕ) (h h' : MDPTrajectory S A n),
        (∀ i : Fin n, i.val ≤ t → h i = h' i) → G h t = G h' t)
    (hcent : ∀ (t : ℕ) (ht : t < n) (h : MDPTrajectory S A n),
        ∑ s', ((M.P (h ⟨t, ht⟩).1 (h ⟨t, ht⟩).2 s' : ℝ)) * G h t s' = 0)
    (hbdd : ∀ (t : ℕ) (h : MDPTrajectory S A n) (s' : Fin S), |G h t s'| ≤ c)
    {ε : ℝ} (hε : 0 ≤ ε) :
    (mdpMeasure M μ0 π n).real
        {h | ∃ (st : ℕ → Fin S) (act : ℕ → Fin A),
              (∀ t : Fin n, h t = (st t, act t)) ∧
              ε ≤ ∑ t ∈ Finset.range (n - 1), G h t (st (t + 1))}
      ≤ Real.exp (-ε ^ 2 / (2 * ((n : ℝ) - 1) * c ^ 2)) := by
  sorry

Source

Jaksch, Ortner, Auer, JMLR 11 (2010), Sec. 4.3; Lattimore-Szepesvari, Bandit Algorithms, Sec. 38.5

View graph