Successors at visits to a pair are NOT i.i.d. (false as stated)

Disproved

BanditAlgorithm.mdp_visit_successors_iid_empirical_representation

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

markov-decision-processesreinforcement-learning

Fix a finite MDP $M$ , an initial distribution, a policy, a horizon $n$ , a state-action pair $(s,a)$ and an integer $m\ge1$ . There are random variables $X_1,\dots,X_m$ on the space of trajectories which are measurable, independent, each distributed as the true transition row $P_a(s,\cdot)$ , and which represent the empirical row: whenever a trajectory has had exactly $m$ transitions out of $(s,a)$ observed before some time $k\le n$ , its empirical row mdpEmpiricalRow at that time is the empirical distribution

\hat P_a(s,s')=\frac1m\sum_{i=1}^{m}\mathbf 1\{X_i=s'\}

of that sample.

This is the step of the analysis of UCRL2 at which the interaction protocol is converted into an i.i.d. sample, and it is the only place where the sequential nature of the data is used. It is not a triviality: the rounds at which the pair $(s,a)$ is played are stopping times, chosen by a policy that may react to everything observed so far, so the successor states are not a fixed block of the trajectory. What makes the statement true is the strong Markov property of the protocol -- conditionally on the history up to the $i$ -th visit to $(s,a)$ , the next state is drawn from $P_a(s,\cdot)$ regardless of how that visit came about -- so the successors of the successive visits to a fixed pair are independent draws from the true row.

Formalization Note The conclusion is an existential over the sample rather than a statement about a conditional law, which is what makes it directly usable: the sample is defined on the trajectory space itself, so a concentration inequality for i.i.d. samples applies to it verbatim under the trajectory measure, and the last clause transfers the conclusion back to the empirical row on the event that the count equals $m$ .

Preamble

import Definitions.Def_UCRL2ConfidenceSets
import Mathlib.Probability.Moments.SubGaussian

open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal

Formal statement

theorem BanditAlgorithm.mdp_visit_successors_iid_empirical_representation
    (S A n : ℕ) (hS : 0 < S) (hA : 0 < A)
    (M : FiniteMDP S A) (μ0 : MDPStateDistribution S) (π : MDPPolicy S A)
    (s : Fin S) (a : Fin A) (m : ℕ) (hm : 0 < m) :
    ∃ X : Fin m → MDPTrajectory S A n → Fin S,
      (∀ i, Measurable (X i)) ∧
      iIndepFun X (mdpMeasure M μ0 π n) ∧
      (∀ (i : Fin m) (s' : Fin S),
        (mdpMeasure M μ0 π n).real {h | X i h = s'} = (M.P s a s' : ℝ)) ∧
      (∀ (h : MDPTrajectory S A n) (k : ℕ), k ≤ n →
        mdpObservedCount h k s a = m →
        ∀ s' : Fin S,
          mdpEmpiricalRow h k s a s'
            = (∑ i : Fin m, if X i h = s' then (1 : ℝ) else 0) / (m : ℝ)) := by
  sorry

Source

Lattimore and Szepesvari, Bandit Algorithms (CUP 2020), Section 38.6 Step 1 and Lemma 38.8 (Exercise 38.21), printed pp. 525-527 / PDF pp. 534-536; after Jaksch, Ortner and Auer, Near-optimal regret bounds for reinforcement learning, JMLR 11 (2010), Appendix C.1.

View graph