The control variate does not change the expected value of the off-policy return (Exercise 7.6, for (7.13))

Proved

SuttonBartoRL.NStep.controlVariate_expectation

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

importance-samplingp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1reinforcement-learning

Let a finite MDP be given, a target policy $\pi$ and a behavior policy $b$ with coverage: $\pi(a \mid s) > 0$ implies $b(a \mid s) > 0$ . Fix a value estimate $V$ , a discount $\gamma$ , a number of steps $n$ and a state $s$ , and let actions be drawn from $b$ . Write $\rho_t = \pi(A_t \mid S_t)/b(A_t \mid S_t)$ and consider, with horizon $h = t + n$ ,

the off-policy return with control variate (7.13): $G^{\mathrm{cv}}_{t:h} = \rho_t (R_{t+1} + \gamma G^{\mathrm{cv}}_{t+1:h}) + (1-\rho_t) V(S_t)$ , $G^{\mathrm{cv}}_{h:h} = V(S_h)$ ;
the same return without the control variate: $G^{\mathrm{pd}}_{t:h} = \rho_t (R_{t+1} + \gamma G^{\mathrm{pd}}_{t+1:h})$ , $G^{\mathrm{pd}}_{h:h} = V(S_h)$ .

Then

\mathbb E_b\big[G^{\mathrm{cv}}_{t:h} \mid S_t = s\big] = \mathbb E_b\big[G^{\mathrm{pd}}_{t:h} \mid S_t = s\big] = \mathbb E_\pi\big[G_{t:h} \mid S_t = s\big],

where $G_{t:h}$ is the on-policy $n$ -step return (7.1) and the last expectation is over trajectories generated by $\pi$ .

The first equality is the statement of the exercise: the control variate term $(1-\rho_t)V(S_t)$ leaves the expected return unchanged. The second is the property the book states on p. 150, that the control variate "does not change the expected update".

Formalization Note The book poses this as Exercise 7.6 (no solution given) right after the action-value return (7.14), referring to "the above equations"; this item states it for the state-value return (7.13) of p. 150. The second equality (unbiasedness for the on-policy return) is a stronger conclusion than the literal exercise and is stated deliberately. Expectations are finite sums over $n$ -step segments, and $V$ is fixed (the book's $V_{h-1}$ ).

Preamble

import Mathlib
import Definitions.Def_SuttonBartoRL_NStep_MDP
import Definitions.Def_SuttonBartoRL_NStep_Trajectories

Formal statement

namespace SuttonBartoRL.NStep

/-- Sutton & Barto (2018), Exercise 7.6, p. 151, for the state-value return (7.13), p. 150: the
control variate `(1 − ρ_t) V(S_t)` does not change the expected value of the return. For a finite
MDP, a target policy `π`, a behavior policy `b` with coverage (`π(a|s) > 0 ⇒ b(a|s) > 0`), a fixed
value estimate `V`, any `γ` and any number of steps `n`, the expectation under `b` given `S_t = s` of
the control-variate return (7.13) equals that of the per-decision importance-sampled return without
the control variate, and both equal the on-policy expectation `E_π[G_{t:t+n} | S_t = s]` of the
`n`-step return (7.1). -/
theorem controlVariate_expectation {S A : Type} [Fintype S] [DecidableEq S]
    [Fintype A] [DecidableEq A]
    (M : MDP S A) (π b : Policy S A) (hcov : ∀ s a, 0 < π.prob s a → 0 < b.prob s a)
    (γ : ℝ) (V : S → ℝ) (n : ℕ) (s : S) :
    segmentExpectation M b n s (controlVariateReturnOn M π b γ V n s) =
        segmentExpectation M b n s (perDecisionReturnOn M π b γ V n s) ∧
      segmentExpectation M b n s (controlVariateReturnOn M π b γ V n s) =
        expectedNStepReturn M π γ V n s := by sorry

end SuttonBartoRL.NStep

Source

Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, Exercise 7.6, p. 151, for Eq. (7.13) and the discussion of the control variate, p. 150

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph