Reinforcement Learning

Motivation

An intervention inside a continuing system can change what happens after the moment at which it is assigned. In a search service, for example, an action shown now can alter the system state that later users encounter. A simple randomized experiment therefore mixes two effects: the immediate reward of treatment and the change in the distribution of future states. Farias, Li, Peng and Zheng model this setting as a finite Markov decision process and study how to estimate the long-run effect of always using the intervention from data collected while treatment is randomized Farias et al., 2022.

The paper calls the difference between treatment and control averages the Naive estimator. It can be biased at first order in the intervention's effect on transitions, because both averages use the state distribution generated by the randomized experiment. The differences-in-Q estimator uses state-action values instead of immediate rewards. Theorem 1 asserts that its population bias is at most second order in that transition effect under a geometric mixing assumption Farias et al., 2022, Theorem 1.

Setting

Let $S$ be a finite state space. At each time, the system takes one of two actions: $0$ is control and $1$ is intervention. An action $a$ at state $s$ earns a real reward $r(s,a)$ and moves to the next state according to the row $P_a(s,\cdot)$ of a stochastic matrix $P_a$. The control policy always selects $0$; the intervention policy always selects $1$. The experiment policy selects each action with probability one half independently at each decision, so its transition matrix and expected reward vector are

$$P_{1/2}=\tfrac12(P_0+P_1),\qquad r_{1/2}=\tfrac12(r_0+r_1).$$

Write $\rho_0$, $\rho_1$ and $\rho_{1/2}$ for stationary probability distributions of these three matrices. The average treatment effect is the difference between the long-run average rewards under always intervening and always controlling:

$$\mathrm{ATE}=\rho_1^{\top}r_1-\rho_0^{\top}r_0.$$

For the experiment policy, $Q_{1/2}(s,a)$ is the expected excess reward when action $a$ is taken first at state $s$ and the experiment policy is followed thereafter. Excess means reward relative to the experiment's stationary average reward $\rho_{1/2}^{\top}r_{1/2}$. The idealized differences-in-Q value is

$$D=\sum_{s\in S}\rho_{1/2}(s)\bigl(Q_{1/2}(s,1)-Q_{1/2}(s,0)\bigr).$$

This is the population quantity whose bias Theorem 1 bounds. It is distinct from the finite-sample estimator calculated from a trajectory Farias et al., 2022, §3.1–3.2.

The mixing condition, Assumption 1, says that for every state $s$ and time $k\ge0$, the total-variation distance between the $k$-step experiment law and its stationary law is at most $C\lambda^k$. The intervention impact is measured by a second total-variation bound, $d_{\mathrm{TV}}(P_1(s,\cdot),P_0(s,\cdot))\le\delta$ for every $s$ Farias et al., 2022, Assumption 1 and Theorem 1.

Formalization targets

Second-order population bias

The goal is Theorem 1. With $r_{\max}=\max_{s,a}|r(s,a)|$, it asks for one polynomial $q$, valid uniformly over all finite models and all admissible $C$, $\lambda$ and $\delta$, such that

$$|\mathrm{ATE}-D|\le q(\log C)\left(\frac1{1-\lambda}\right)^2r_{\max}\delta^2.$$

This formalizes the paper's statement that the unspecified constant depends polynomially on $\log C$. The polynomial is quantified before the state space and the model, so its coefficients cannot be chosen from a particular example.

Source milestones

Five subtargets record the paper's route to this statement: Lemma 1's stationary-distribution perturbation identity; the corrected norm bound of Appendix F, Lemma 2; the corrected average-treatment-effect expansion in Eq. (6); the identification of the experiment's relative value with a group-inverse expression; and the identity that makes $D$ the first-order truncation Farias et al., 2022, pp. 13–15, 41. The goal and these milestones concern the idealized population estimator. Asymptotic normality and finite-sample estimation from Theorem 2 are outside this mission.

Significance

The result quantifies what the DQ adjustment buys in a dynamic experiment. When action-dependent transitions differ by at most $\delta$ in total variation, the population bias scales as $\delta^2$, with an explicit dependence on the experiment chain's mixing rate and the reward bound. This provides a statement against which variants of the estimator and sharper constants can be compared Farias et al., 2022, Theorem 1.

The theorem is proved in the cited paper; the task here is to give its claim and the supporting identities machine-checkable proofs. The finite-chain definitions, perturbation identity and group-inverse bound can be reused in other average-reward Markov-chain arguments. No machine-checked proof of this theorem or these milestones was found in the local Prove2Me catalog search for this mission.

Difficulty

The immediate-reward difference averages under $\rho_{1/2}$, whereas the treatment effect compares rewards under $\rho_1$ and $\rho_0$. Replacing both stationary laws by $\rho_{1/2}$ therefore loses a term of order $\delta$ in general. The relative-value and Q-function expressions account for that term, but their definitions involve infinite excess-reward series. A formal proof must establish their convergence from mixing and reconcile them with the matrix group inverse. It must also control the norm of that inverse with the paper's precise row norm; using a generic matrix norm would change the claim.

Formalization scope

The state type is finite, actions are Fin 2, and reward vectors take real values. The matrices $P_0$ and $P_1$ are row stochastic. Primitivity represents the §2 standing ergodicity convention for the control and intervention policies. A stationary distribution is a nonnegative vector summing to one, so an empty state space cannot satisfy the theorem's hypotheses. Total variation is half the rowwise $\ell_1$ distance. The paper's $\|M\|_{1,\infty}$ is the maximum absolute row sum, and $\mathbf1\rho^{\top}$ is a rank-one matrix. The group inverse is represented by $(I-P+\mathbf1\rho^{\top})^{-1}-\mathbf1\rho^{\top}$, used under hypotheses making the inverse valid Farias et al., 2022, Appendix A.

The relative value $V_{1/2}$ and action value $Q_{1/2}$ are sums of expected excess rewards, matching the reading of the paper's expectation formulas used in §3.3. They are not defined by the group inverse: the equivalence is a milestone. The idealized DQ value averages their action difference under $\rho_{1/2}$; the ATE uses the stationary-distribution form stated on p. 13. The goal assumes $0<\lambda<1$, as required by the mixing expression and the denominator. Its polynomial constant is uniform over all instances. These choices exclude an instance-dependent constant or a definition that builds the desired equality into $V$.

The Appendix F version of Lemma 2 is corrected with $C\ge1$: without it, the one-state case permits a negative stated upper bound. Its premise bounds the maximum row norm. The p. 14 total-variation version omits the factor of two needed to convert to that norm. Accordingly, the remainder inequality and Eq. (6) milestones use the corrected Appendix F premise; their verbatim fields preserve what the paper prints Farias et al., 2022, pp. 14, 41. Contributions that establish these identities and bounds under the stated hypotheses, including reusable finite-chain matrix results and summability facts, are within scope.

Selected references

• V. F. Farias, A. A. Li, T. Peng and A. Zheng, Markovian Interference in Experiments, arXiv preprint arXiv:2206.02371v2, 2022. Preprint.

Motivation

Temporal-difference (TD) learning is the basic algorithm of reinforcement learning for estimating the value function of a fixed policy from a single stream of experience. With a linear function approximation $V_\theta(s)=\phi(s)^\top\theta$, TD(0) is the evaluation step inside many policy-iteration and actor–critic methods, and its behaviour governs how much data such methods need.

The asymptotic theory is classical. Tsitsiklis and Van Roy (1997) proved that TD(λ) with linear features converges almost surely along a single trajectory of an ergodic Markov chain, to the unique solution $\theta^*$ of the projected Bellman equation, under Robbins–Monro step sizes. Their proof uses the ODE method, which says nothing about how fast the iterates approach $\theta^*$, nor how the rate depends on the step size, on the conditioning of the features, or on how quickly the chain mixes.

Finite-time results came later and mostly for independent samples. Dalal, Szörényi, Thoppe and Mannor (2018) and Lakshminarayanan and Szepesvári (2018) analysed TD(0) when the observed transitions are drawn i.i.d. from the stationary distribution. Bhandari, Russo and Singal (2018) gave a short analysis in the i.i.d. model and, for a projected variant of TD, the first finite-time bounds when the transitions come from one trajectory of the Markov chain, so that consecutive observations are strongly correlated. This mission formalizes that Markovian result, Theorem 3 of the paper.

Setting

A finite Markov reward process consists of a finite state space $S$, a stochastic matrix $P$ with $P(s,s')$ the probability of moving from $s$ to $s'$, transition rewards $R(s,s')$ with $|R(s,s')|\le r_{\max}$, and a discount factor $0\le\gamma<1$. The chain has a stationary distribution $\pi$ ($\pi P=\pi$), and the observed trajectory $s_0,s_1,\dots$ starts from $\pi$, so it is a stationary sequence.

Each state carries a feature vector $\phi(s)\in\mathbb{R}^d$ with $\|\phi(s)\|_2\le1$. The steady-state feature covariance $\Sigma=\sum_s\pi(s)\phi(s)\phi(s)^\top$ has full rank, and $\omega>0$ is its minimum eigenvalue. Value functions are compared in the steady-state seminorm $\|V_\theta\|_D^2=\sum_s\pi(s)(\phi(s)^\top\theta)^2$.

At a transition $(s,s')$ the TD direction is $g(\theta;s,s')=\big(R(s,s')+\gamma\phi(s')^\top\theta-\phi(s)^\top\theta\big)\phi(s)$. Its steady-state mean is $\bar g(\theta)=\sum_{s,s'}\pi(s)P(s,s')\,g(\theta;s,s')$, and the TD fixed point $\theta^*$ is the vector with $\bar g(\theta^*)=0$. Projected TD(0) with radius $R\ge\|\theta^*\|_2$ starts from $\|\theta_0\|_2\le R$ and iterates

$$\theta_{t+1}=\Pi_{2,R}\big(\theta_t+\alpha_t\,g(\theta_t;s_t,s_{t+1})\big),$$

where $\Pi_{2,R}$ is the Euclidean projection onto the ball of radius $R$. The averaged iterate is $\bar\theta_T=T^{-1}\sum_{t=0}^{T-1}\theta_t$.

The chain mixes uniformly (Assumption 1): there are $m>0$ and $\rho\in(0,1)$ with $\sup_s d_{TV}(P^t(s,\cdot),\pi)\le m\rho^t$ for all $t\ge0$. The mixing time is $\tau_{\mathrm{mix}}(\epsilon)=\min\{t\ge0: m\rho^t\le\epsilon\}$. Write $G=r_{\max}+2R$.

Formalization targets

Goal: Theorem 3 (pp. 17–18)

All three bounds are stated together, with $\mathbb{E}$ the expectation over the stationary trajectory:

(a) for $T\ge1$ and $\alpha_t\equiv1/\sqrt T$,

$$\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{\|\theta^*-\theta_0\|_2^2+G^2\big(9+12\tau_{\mathrm{mix}}(1/\sqrt T)\big)}{2\sqrt T(1-\gamma)};$$

(b) for a constant $\alpha_t\equiv\alpha_0\in\big(0,\,1/(2\omega(1-\gamma))\big)$,

$$\mathbb{E}\|\theta^*-\theta_T\|_2^2\le e^{-2\alpha_0(1-\gamma)\omega T}\|\theta^*-\theta_0\|_2^2+\alpha_0\frac{G^2\big(9+12\tau_{\mathrm{mix}}(\alpha_0)\big)}{2(1-\gamma)\omega};$$

(c) for $\alpha_t=1/(\omega(t+1)(1-\gamma))$ and $T\ge1$,

$$\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{G^2\big(9+24\tau_{\mathrm{mix}}(\alpha_T)\big)}{T(1-\gamma)^2\omega}(1+\log T).$$

Milestones

The milestones are the paper's own lemmas, in the order the proof in Appendix A uses them: norm equivalence $\sqrt\omega\|\theta\|_2\le\|V_\theta\|_D\le\|\theta\|_2$ (Lemma 1); the descent inequality $(\theta^*-\theta)^\top\bar g(\theta)\ge(1-\gamma)\|V_{\theta^*}-V_\theta\|_D^2$ (Lemma 3); the gradient bound $\|g_t(\theta)\|_2\le r_{\max}+2\|\theta\|_2$ (Lemma 6); the pathwise error recursion (Lemma 8); the coupling bound $|\mathbb{E}v(X,Y)-\mathbb{E}v(X',Y')|\le2\|v\|_\infty m\rho^\tau$ (Lemma 9); boundedness and Lipschitz continuity of the gradient error $\zeta_t$ (Lemma 10); and the bias bound $\mathbb{E}[\zeta_t(\theta_t)]\le G^2(4+6\tau_{\mathrm{mix}}(\alpha_T))\alpha_{t^*}$ (Lemma 11).

Significance

Theorem 3 gives explicit, non-asymptotic mean-squared-error bounds for TD(0) with linear features under Markovian sampling. Part (a) does not depend on the conditioning $\omega$, part (b) shows exponential convergence to a neighbourhood whose radius scales with $\alpha_0G^2\tau_{\mathrm{mix}}(\alpha_0)$, and part (c) gives an $\tilde O(1/T)$ rate. Compared with the i.i.d. bounds, the only change is a factor of order $\tau_{\mathrm{mix}}$: roughly, one mixing time of correlated observations is worth one independent sample. The same argument carries over, in the paper itself, to projected TD(λ) (Theorem 4) and to Q-learning for optimal stopping (§10), so the lemmas formalized here are the core of all of its Markovian results.

The result is proved on paper but has not been machine-checked. The mission provides a Lean statement of the theorem and of each lemma of its proof, all built on one model. The trajectory-level definitions (path law, total-variation mixing, mixing time, projected iterates) can be reused by later formalizations of Markovian stochastic approximation.

Difficulty

The obvious approach, from the i.i.d. analysis, takes expectations in the error recursion of Lemma 8 and uses $\mathbb{E}[\zeta_t(\theta_t)]=0$. Under Markov sampling this fails: $\theta_t$ is a function of $s_0,\dots,s_t$ and is correlated with the observation $(s_t,s_{t+1})$ at which it is evaluated, so the gradient is biased and the noise is not a martingale difference. Bounding that bias needs a quantitative decorrelation between the iterate $\tau$ steps back and the current observation, which is a total-variation estimate on the joint law of a path (Lemma 9). It also needs control of how far the iterates drift in $\tau$ steps, which is where the projection and the uniform gradient bound $G$ enter. The rest of the proof then combines telescoping, a geometric recursion and harmonic sums, with every constant ($9+12\tau$, $9+24\tau$) tracked exactly.

Formalization scope

• State space and expectation. $S$ is a Fintype. The expectation over the stationary trajectory is the finite sum $\sum_{w\in S^{T+1}}\pi(w_0)\prod_iP(w_i,w_{i+1})\,F(w)$, the exact law of $(s_0,\dots,s_T)$ for a finite chain started from $\pi$, so no measure theory is used. The paper itself works with a finite $S$ (p. 5).
• Coupling lemma. Lemma 9 uses probability measures for the conditional laws of $X,Y$ given $s_t,s_{t+\tau}$; their factorization expresses $X\to s_t\to s_{t+\tau}\to Y$. The variables may take values in arbitrary measurable spaces, including the iterates and observations used in the proof.
• Norms. Parameters and features live in EuclideanSpace ℝ (Fin d) with $d\ge1$, so every $\|\cdot\|$ is Euclidean.
• Standing hypotheses, added or made explicit: $0\le\gamma$ (the paper writes $\gamma<1$; the proof of Lemma 3 needs $\gamma\ge0$). $\omega$ is the least value of $\theta^\top\Sigma\theta$ on the unit sphere, that is $\lambda_{\min}(\Sigma)$, together with $\omega>0$ (full rank). $\pi$ is a stationary probability vector, and no separate irreducibility hypothesis is added, since Assumption 1 implies ergodicity. $\theta^*$ is given as a vector with $\bar g(\theta^*)=0$. The implicit conditions are explicit: $T\ge1$ in (a) and (c), $\alpha_0>0$ in (b), $\alpha_T>0$ in Lemma 11, and $\alpha_t\ge0$ in Lemma 8.
• Conventions. $\Pi_{2,R}$ is defined by the rescaling formula of p. 16. $\bar\theta_T$ averages $\theta_0,\dots,\theta_{T-1}$, as in the text and the proof (Algorithm 1's averaging recursion is a slip). $\tau_{\mathrm{mix}}$ is sInf over $\mathbb{N}$ and is only evaluated at positive thresholds, where it is a true minimum. "With probability 1" is stated for every path or transition.
• No trivialization. The expectation must start from $\pi$, never from an arbitrary state. $\theta_t$ and the observation must come from the same trajectory. $\omega$ must be $\lambda_{\min}(\Sigma)$, not an arbitrary positive constant, since it fixes the step size in (c). A formalization with independent samples, with the sup norm on $\mathbb{R}^d$, or with a junk-valued $\tau_{\mathrm{mix}}(0)=0$ would prove a different statement.
• Not in scope. Theorem 1 (mean-path TD), Theorem 2 (i.i.d. model), Theorem 4 (projected TD(λ)) and §10 (Q-learning for optimal stopping) are separate results. Theorem 3's proof does not use them.
• Welcome contributions. Proofs of the milestones, and general lemmas on finite path sums (marginalisation of the trajectory law, the variational form of total variation, nonexpansiveness of the ball projection).

Selected references

• J. Bhandari, D. Russo, R. Singal, A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximation, arXiv:1806.02450v2, 2018; Operations Research 69(3), 2021. https://arxiv.org/abs/1806.02450
• J. N. Tsitsiklis, B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
• G. Dalal, B. Szörényi, G. Thoppe, S. Mannor, Finite Sample Analyses for TD(0) with Function Approximation, AAAI 2018. https://arxiv.org/abs/1704.01161
• C. Lakshminarayanan, C. Szepesvári, Linear Stochastic Approximation: How Far Does Constant Step-Size and Iterate Averaging Go?, AISTATS 2018. http://proceedings.mlr.press/v84/lakshminarayanan18a.html
• R. S. Sutton, Learning to Predict by the Methods of Temporal Differences, Machine Learning 3, 1988. https://doi.org/10.1007/BF00115009
• D. A. Levin, Y. Peres, Markov Chains and Mixing Times, 2nd ed., AMS, 2017. https://doi.org/10.1090/mbk/107

Motivation

Off-policy evaluation (OPE) asks for the long-run value of a target decision policy, using only data collected under a different policy. It arises wherever running the target policy is expensive or unsafe: a new treatment rule in medicine, a new recommendation or pricing rule, a candidate controller in reinforcement learning. Importance-sampling estimators reweight whole trajectories. Their variance grows exponentially with the horizon, the curse of horizon (Liu et al. 2018, arXiv:1810.12429).

Kallus and Uehara (arXiv:1909.05850, Operations Research 2022) treat infinite-horizon discounted OPE as a semiparametric estimation problem. They derive the efficiency bound under three models: non-Markov, time-varying Markov and time-invariant Markov (MDP). They then propose double reinforcement learning (DRL), an estimator that combines a q-function estimate with an estimate of the ratio between the discounted state visitation of the target policy and the state distribution of the data. In the MDP model it attains the efficiency bound. This mission formalizes the transition-sampling version of that result, Theorem 6.

Timeline:

• 2016: Jiang and Li (arXiv:1511.03722) and Thomas and Brunskill (arXiv:1604.00923) give doubly robust OPE estimators for finite horizons, built on trajectory-wise importance weights.
• 2018: Liu, Li, Tang and Zhou (arXiv:1810.12429) replace trajectory weights by stationary state-distribution ratios, removing the exponential dependence on the horizon, but without efficiency guarantees.
• 2018: Chernozhukov et al. (arXiv:1608.00060) formalize cross-fitting and Neyman orthogonality for estimation with machine-learned nuisances (double machine learning).
• 2019–2022: Kallus and Uehara derive the MDP efficiency bound (Theorem 3) and prove that cross-fitted DRL attains it (Theorem 6), also under trajectory sampling with mixing (Theorems 10–13).

Setting

States lie in a measurable space $S$ and actions in a measurable space $A$. A time-invariant MDP is a transition kernel $p(s'\mid s,a)$ and a reward kernel $p(r\mid s,a)$ with rewards in $[0,R_{\max}]$. A policy $\pi(a\mid s)$ is a kernel from $S$ to $A$. Fix a discount $\gamma\in[0,1)$, a known target policy $\pi_e$ with known initial law $p^{(0)}_{\pi_e}$, and a behavior policy $\pi_b$.

The estimand is the normalized discounted value

$$\rho^{\pi_e}=\lim_{T\to\infty}\Big(\sum_{t=0}^T\gamma^t\Big)^{-1}\mathbb E_{p_{\pi_e}}\Big[\sum_{t=0}^T\gamma^tr_t\Big].$$

The q-function is $q(s,a)=\mathbb E_{p_{\pi_e}}[\sum_k\gamma^kr_k\mid s_0=s,a_0=a]$, and $v(s)=\int q(s,a)\,\pi_e(da\mid s)$. The discounted visitation is $p^{(\infty)}_{\pi_e,\gamma}=(1-\gamma)\sum_t\gamma^t p^{(t)}_{\pi_e}$, where $p^{(t)}_{\pi_e}$ is the law of $s_t$.

Transition sampling. The data are i.i.d. observations $O_i=(s,a,r,s')$ with law $p_{\pi_b}$: $s\sim p^{(0)}_{\pi_b}$, $a\sim\pi_b(\cdot\mid s)$, and, given $(s,a)$, independently $r\sim p(\cdot\mid s,a)$ and $s'\sim p(\cdot\mid s,a)$. The law of $s'$ may differ from that of $s$.

The density ratios are $\eta(s,a)=\pi_e(a\mid s)/\pi_b(a\mid s)$ and $w(s)=p^{(\infty)}_{\pi_e,\gamma}(s)/p^{(0)}_{\pi_b}(s)$. For candidate nuisances $w',q'$, with $v'(s)=\int q'(s,a)\pi_e(da\mid s)$, the estimating function is

$$\psi(s,a,r,s';w',q')=(1-\gamma)\,\mathbb E_{p^{(0)}_{\pi_e}}[v'(s_0)]+w'(s)\eta(s,a)\big(r+\gamma v'(s')-q'(s,a)\big).$$

The cross-fitted estimator $\hat\rho_{\rm DRL}(\mathcal M_3)$ splits the sample into two folds. It fits $\hat w^{[j]},\hat q^{[j]}$ on fold $j$ and averages $\psi$ over all observations, each evaluated at the nuisances of the other fold. The efficient influence function is $\phi_{\rm eff}=w(s)\eta(s,a)(r+\gamma v(s')-q(s,a))$, and the efficiency bound is $\mathrm{EB}(\mathcal M_3)=\mathbb E[\phi_{\rm eff}^2]$.

Formalization targets

Goal: Theorem 6

Assume the following:

• $w\le C_w$ and $p_{b,S'}\le C_{S'}p_{b,S}$ (6a);
• $\eta\le C_\eta$ (added);
• $\hat w^{[j]},\hat q^{[j]}$ lie in $[0,C_w]$ and $[0,R_{\max}/(1-\gamma)]$ (6b);
• $\|\hat w^{[j]}-w\|_2,\|\hat q^{[j]}-q\|_2=o_p(1)$ (6c);
• $\sqrt n\,\|\hat w^{[j]}-w\|_2\|\hat q^{[k]}-q\|_2=o_p(1)$ for all $j,k\in\{0,1\}$ (6d, equivalent to common envelopes for both folds).

Then

$$\sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)-\frac1{\sqrt n}\sum_{i<n}\phi_{\rm eff}(O_i)\xrightarrow{p}0,\qquad \sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)\xrightarrow{d}N\big(0,\mathrm{EB}(\mathcal M_3)\big).$$

No rate exponent or learner class is fixed. Only the product rate enters.

Milestones, in proof order

1. Lemma 1 (forward): $\mathbb E[\gamma w(s)\eta(s,a)f(s')-w(s)f(s)]+(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[f]=0$ for bounded measurable $f$.
2. $\rho^{\pi_e}=\mathbb E[w(s)\eta(s,a)r]$ (p. 16).
3. Eq. (5): $\mathbb E[\psi(w',q)]=(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[v]=\rho^{\pi_e}$ for every bounded $w'$.
4. $\psi(w,q)=\rho^{\pi_e}+\phi_{\rm eff}$ pointwise (p. 22).
5. Eqs. (6)–(8): $\mathbb E[\psi(w,q')]=\rho^{\pi_e}$ for every bounded $q'$.
6. Jensen step, corrected: $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}C_\eta}\,\|\hat q-q\|_2$.
7. Term (30): $|\mathbb E\psi(\hat w,\hat q)-\rho^{\pi_e}|\le C_\eta(1+\gamma\sqrt{C_{S'}C_\eta})\|\hat w-w\|_2\|\hat q-q\|_2$.
8. Term (28), variance: $\operatorname{var}[\psi(\hat w,\hat q)-\psi(w,q)]\le2a^2\|\hat w-w\|_2^2+2b^2\|\hat q-q\|_2^2$.
9. Term (28) is $o_p(1)$: the centred fold empirical process at the opposite fold's nuisances vanishes.

Significance

Theorem 6 shows that, in a Markov model, a $\sqrt n$-consistent and efficient OPE estimator exists whose variance scales with the number of observed transitions, not trajectories. It requires no complexity (Donsker or entropy) restriction on the nuisance estimators, only a product rate. Any black-box learners with $\|\hat w-w\|_2\|\hat q-q\|_2=o_p(n^{-1/2})$, which allows two subparametric rates, give asymptotically valid confidence intervals at the efficiency bound. The mixed-bias identities (Eqs. (5)–(8)) and Lemma 1 are the same ingredients used by later minimax and adversarial estimators of $w$ and $q$.

The result is proved in the paper; nothing here is presented as open. As far as is known, none of it has a machine-checked proof: no off-policy evaluation, density-ratio characterization or cross-fitting asymptotics exists in Mathlib or on the platform. Formalizing it checks the appendix argument, which is short and contains errors (below). It also produces a reusable layer: kernel-based discounted MDPs on general measurable spaces, discounted visitation measures, and the cross-fitting plus Slutsky template that other double-machine-learning results share.

Difficulty

The obvious route is "the estimator equals the oracle average $\mathbb P_n\psi(w,q)$ plus negligible terms, then apply the CLT". Two of its steps are not routine.

First, the negligible terms are random functions evaluated at random data. The empirical-process term (28) is controlled only conditionally on the other fold, through a conditional Chebyshev argument that needs the independence structure of the split. Treating $\hat w,\hat q$ as fixed functions loses exactly this.

Second, the bias term (30) is second order only because of the mixed-bias structure. That structure rests on Lemma 1, a change-of-measure identity between the discounted visitation of $\pi_e$ and the data distribution. The printed constants are wrong. The Jensen step $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}}\|\hat q-q\|_2$ fails when $\eta$ is large: with one state, $\pi_b$ uniform on two actions and $\pi_e$ a point mass, the left side is $1$ and the right side is $1/\sqrt2$. The bound by $\|\hat w-w\|_2\|\eta\|_2\|\hat q-q\|_2$ is not a valid inequality for a triple product. Both need a bound $\eta\le C_\eta$, which the mission adds.

Formalization scope

• Spaces and kernels. $S$, $A$ are measurable spaces, the action σ-algebra countably generated (for Mathlib's jointly measurable Kernel.rnDeriv). The MDP, the policies and the observation law are Mathlib kernels and measures. The paper's base measures are not used.
• Ratios. $w$ and $\eta$ are toReal of Radon–Nikodym derivatives, not free functions satisfying an identity. Overlap ($\pi_e(\cdot\mid s)\ll\pi_b(\cdot\mid s)$, $p^{(\infty)}_{\pi_e,\gamma}\ll p^{(0)}_{\pi_b}$) is a standing assumption.
• Objects. $q$ is the discounted series, not "a solution of the Bellman equation". $\rho^{\pi_e}$ is the limit of normalized discounted sums, not $(1-\gamma)\mathbb E[v]$ or $\mathbb E[w\eta r]$; those identities are milestones. The discounted visitation is the measure $(1-\gamma)\sum_t\gamma^tp^{(t)}_{\pi_e}$, the limit of the paper's normalized averages.
• Cross-fitting. The folds are $\{i<\lfloor n/2\rfloor\}$ and the rest. Each learner is a jointly measurable function of its own fold's observations only. Rates are convergence in probability of the actual random $L^2$ errors.
• Conclusion. "RAL and efficient" is posed as asymptotic linearity with influence function $\phi_{\rm eff}$ plus the normal limit. Regularity needs the tangent-space framework of Theorem 3 and is not posed.
• Ruled out. The oracle statement with $\hat w=w$, $\hat q=q$ is an i.i.d. CLT for a fixed function and drops the theorem's content. It is not an acceptable substitute for the goal.
• Infrastructure needed. Linearity and Fubini for kernel compositions; summation of discounted occupancies; conditional Chebyshev for cross-fitted empirical processes; Slutsky (TendstoInDistribution with TendstoInMeasure) and Mathlib's i.i.d. CLT tendstoInDistribution_inv_sqrt_mul_sum_sub. The occupancy and Lemma 1 layer and the cross-fitting template are reusable beyond this mission. Proofs of any milestone, and helper lemmas on kernel powers and discounted sums, are welcome.

Selected references

• N. Kallus and M. Uehara, Efficiently Breaking the Curse of Horizon in Off-Policy Evaluation with Double Reinforcement Learning, Operations Research 70(6), 2022; arXiv:1909.05850v6 (2023). https://arxiv.org/abs/1909.05850
• Q. Liu, L. Li, Z. Tang and D. Zhou, Breaking the Curse of Horizon: Infinite-Horizon Off-Policy Estimation, NeurIPS 2018. https://arxiv.org/abs/1810.12429
• V. Chernozhukov, D. Chetverikov, M. Demirer, E. Duflo, C. Hansen, W. Newey and J. Robins, Double/Debiased Machine Learning for Treatment and Structural Parameters, The Econometrics Journal 21(1), 2018. https://arxiv.org/abs/1608.00060
• N. Jiang and L. Li, Doubly Robust Off-Policy Value Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1511.03722
• P. Thomas and E. Brunskill, Data-Efficient Off-Policy Policy Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1604.00923

Motivation

Policy evaluation asks for the value of a fixed decision rule in a Markov decision process whose transition probabilities are unknown. It is the inner loop of policy iteration, the subroutine behind actor-critic methods, and the question an operator faces before deploying a policy in an inventory, queueing or routing system that can only be simulated. The simplest estimator is the plug-in (model-based) one: sample transitions from a simulator, build the empirical transition kernel, and compute the value of the policy in the resulting empirical MDP.

How many samples this estimator needs has a short history. Azar, Munos and Kappen (Machine Learning, 2013) introduced the total-variance argument that yields the $(1-\gamma)^{-3}$ dependence for planning with a generative model. Agarwal, Kakade and Yang (COLT 2020) proved minimax-optimal guarantees for model-based planning, but only when the sample size per state-action pair exceeds roughly $(1-\gamma)^{-2}$. Pananjady and Wainwright (IEEE Trans. Inf. Theory, 2021) gave instance-dependent policy-evaluation bounds and a minimax lower bound, again under a sample-size requirement of order $(1-\gamma)^{-2}$. Li, Wei, Chi and Chen (arXiv:2005.12900v8; Operations Research, 2024) removed this barrier: their Theorem 3 shows that the plug-in estimate is accurate across the whole accuracy range once the sample size exceeds $(1-\gamma)^{-1}$ up to logarithmic factors. This mission formalizes that theorem and the lemmas its proof rests on.

Setting

A discounted Markov decision process consists of a finite state set $\mathcal S$, a finite action set $\mathcal A$, a transition kernel $P$ (for each pair $(s,a)$, $P(\cdot\mid s,a)$ is a probability vector over $\mathcal S$), a reward $r:\mathcal S\times\mathcal A\to[0,1]$ and a discount factor $0<\gamma<1$. A deterministic policy is a map $\pi:\mathcal S\to\mathcal A$. Its value function is

$$V^\pi(s)=\mathbb E\Big[\sum_{t=0}^\infty\gamma^t r(s^t,a^t)\,\Big|\,s^0=s\Big],\qquad a^t=\pi(s^t),\quad s^{t+1}\sim P(\cdot\mid s^t,a^t).$$

Write $P_\pi(s,s')=P(s'\mid s,\pi(s))$ for the state transition matrix of $\pi$ and $r_\pi(s)=r(s,\pi(s))$ for its reward vector, so that $V^\pi=(I-\gamma P_\pi)^{-1}r_\pi$. For a vector $V\in\mathbb R^{\mathcal S}$, $\mathrm{Var}_{P_\pi}(V)(s)=\sum_{s'}P_\pi(s,s')V(s')^2-\big(\sum_{s'}P_\pi(s,s')V(s')\big)^2$ is the one-step variance of $V$ under the chain.

The generative model returns, for every pair $(s,a)$, $N$ independent next states $s^1_{s,a},\dots,s^N_{s,a}\sim P(\cdot\mid s,a)$. The empirical kernel is $\widehat P(s'\mid s,a)=\frac1N\sum_{i=1}^N\mathbb 1\{s^i_{s,a}=s'\}$, and for a policy $\pi$ chosen independently of the data the plug-in estimate $\widehat V^\pi$ is the value function of $\pi$ in the empirical MDP $(\mathcal S,\mathcal A,\widehat P,r,\gamma)$, that is, $\widehat V^\pi=(I-\gamma\widehat P_\pi)^{-1}r_\pi$. Norms $\|\cdot\|_\infty$ are maxima of absolute entries; $e=\exp(1)$ and $\log$ is natural.

Formalization targets

Goal: Theorem 3 (p. 9)

There is a universal constant $c_0>0$ such that for every MDP as above, every fixed policy $\pi$, every $0<\delta<1$ and every $0<\varepsilon\le\frac1{1-\gamma}$,

$$N\ge c_0\,\frac{\log\big(|\mathcal S|\log\frac{e}{1-\gamma}/\delta\big)}{(1-\gamma)^3\varepsilon^2} \quad\Longrightarrow\quad \mathbb P\Big(\max_{s}\big|\widehat V^\pi(s)-V^\pi(s)\big|\le\varepsilon\Big)\ge1-\delta .$$

The constant $c_0$ is not specified, so the goal survives any later improvement of the constants.

Milestones

In attack order: Lemma 10 (elementary facts on $(I-\gamma P_\pi)^{-1}$, p. 23); the matrix form (27) of $V^\pi$ (p. 12); Lemma 11, $\|(I-\gamma P_\pi)^{-1}\sqrt{\mathrm{Var}_{P_\pi}(V)}\|_\infty\le\frac{4}{\gamma\sqrt{1-\gamma}}\|V\|_\infty$ for $V=(I-\gamma P_\pi)^{-1}r_\pi$ with $r_\pi\ge0$ (p. 24); the total-variance bound (70) of Azar et al. (p. 24); the deterministic instance-dependent bound (80) under a Bernstein-type condition (pp. 25–26); Lemma 2, the worst-case bound $\|\widehat V^\pi-V^\pi\|_\infty\le\frac{6}{1-\gamma}\sqrt{\frac{\beta_1}{N(1-\gamma)}}$ under the same condition (p. 15); the high-probability Bernstein bound (82) for a fixed policy (p. 27); and Lemma 1, the explicit-constant version of the goal with an instance-dependent refinement (p. 13):

$$\big\|\widehat V^\pi-V^\pi\big\|_\infty\le 4\gamma\sqrt{\tfrac{2L}{N}}\Big\|(I-\gamma P_\pi)^{-1}\sqrt{\mathrm{Var}_{P_\pi}[V^\pi]}\Big\|_\infty+\tfrac{2\gamma L}{(1-\gamma)N}\|V^\pi\|_\infty\le 6\sqrt{\tfrac{2L}{N(1-\gamma)^3}},$$

with $L=\log\big(4|\mathcal S|\log\frac{e}{1-\gamma}/\delta\big)$ and $N\ge\frac{32e^2}{1-\gamma}L$.

Significance

The theorem says that the plug-in estimate of a fixed policy's value beats a random guess as soon as $N$ exceeds $\frac1{1-\gamma}$ up to logarithmic factors, and that its sample size matches the minimax lower bound of Pananjady and Wainwright (2019, Theorem 2(b)) up to a $\log\log\frac1{1-\gamma}$ factor over the full range $\varepsilon\in(0,\frac1{1-\gamma}]$. Lemma 2, which does not require the policy to be independent of the data, is the step the paper reuses to analyze the data-dependent optimal policy of the empirical MDP (Theorems 1 and 2, posed in sibling missions of this series).

The result is proved in the paper; none of it is formalized. The mission produces a machine-checked account of the variance-aware analysis of tabular MDPs: the resolvent calculus of Lemma 10, the total-variance bounds (70) and Lemma 11, which recur across the reinforcement-learning sample-complexity literature, and a high-order expansion argument that turns a Bernstein-type condition into an error bound. A formal proof of (70), which the paper quotes without proof, would itself be a reusable result.

Difficulty

The obvious argument writes $\widehat V^\pi-V^\pi=\gamma(I-\gamma\widehat P_\pi)^{-1}(\widehat P_\pi-P_\pi)V^\pi$ and bounds the two factors separately. The resolvent of the empirical chain is correlated with the deviation $(\widehat P_\pi-P_\pi)V^\pi$, and bounding $(I-\gamma\widehat P_\pi)^{-1}$ crudely by its row sums $\frac1{1-\gamma}$ loses a factor that forces $N\gtrsim(1-\gamma)^{-2}$; this is exactly the barrier in earlier work. Removing it requires controlling a whole sequence of auxiliary vectors $V^{(l)}$, each defined through the variance of the previous one, up to a logarithmic depth, and showing that their norms do not blow up (Lemma 11). The Bernstein step must also use the variance, not the range, of $V^{(l)}$; a Hoeffding bound gives the wrong power of $1-\gamma$.

Formalization scope

States and actions are finite types; the kernel is P : S → A → S → ℝ with P s a s' $=P(s'\mid s,a)$, a probability vector for each (s, a) (the published IsTransitionKernel). The standing setting is the predicate IsDiscountedMDP P r γ: a kernel, $r(s,a)\in[0,1]$, $0<\gamma<1$, and nonempty state and action sets ($\mathcal S=\{1,\dots,|\mathcal S|\}$, $\mathcal A=\{1,\dots,|\mathcal A|\}$, p. 5). Policies are deterministic maps S → A; the value function is the published series PolicyValue of the induced point-mass policy. Vector norms are Mathlib's sup norm on finite function types, matching $\|\cdot\|_\infty$; vector inequalities and square roots are entrywise.

The data set is the finite type of arrays of $N$ next states per pair, its law is the product of the kernel probabilities, and $\mathbb P$ of an event is a finite sum. "With probability at least $1-\delta$, $E$" is stated as $\mathbb P(\text{not }E)\le\delta$. The goal assumes $N>0$, the standing assumption of the empirical kernel (3), which is implied by the sample-size condition since $\mathcal S$ is nonempty. Index ranges "$0\le l\le\log\frac{e}{1-\gamma}$" range over the integers in that interval. The deterministic milestones (80) and Lemma 2 are stated for an arbitrary transition kernel $\widehat P$, which is what their proofs use.

Three formalizations would trivialize the goal and are ruled out: computing $\widehat V^\pi$ from the true kernel $P$ instead of the empirical one; letting $\pi$ be chosen after the data are seen; and letting $c_0$ depend on $\mathcal S$, $\mathcal A$, $\gamma$, $P$, $r$ or $\pi$ (the existential over $c_0$ precedes all of them).

A complete development needs: the matrix form of the value function, Neumann series and nonnegativity of $(I-\gamma P_\pi)^{-1}$; variance identities for finite distributions; a Bernstein inequality for i.i.d. bounded categorical samples with a union bound over states and indices; and the algebra of the recursive expansion. The resolvent and total-variance lemmas are reusable for any tabular discounted MDP. Proofs of individual milestones are welcome independently; (70) is a standalone classical result.

Selected references

• G. Li, Y. Wei, Y. Chi, Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8, 2023. https://arxiv.org/abs/2005.12900
• M. G. Azar, R. Munos, H. J. Kappen, Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model, Machine Learning 91(3), 2013. https://doi.org/10.1007/s10994-013-5368-1
• A. Agarwal, S. Kakade, L. F. Yang, Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal, COLT 2020. https://arxiv.org/abs/1906.03804
• A. Pananjady, M. J. Wainwright, Instance-Dependent ℓ∞-Bounds for Policy Evaluation in Tabular Reinforcement Learning, IEEE Transactions on Information Theory 67(1), 2021. https://arxiv.org/abs/1909.08749