Prove2Me

Example 5.5: ordinary importance sampling with infinite variance

Proved
SuttonBartoRL.ImportanceSampling.infinite_variance_example

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

importance-samplingmonte-carlop2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1reinforcement-learning

In the one-state MDP of Example 5.5 (from ss, right terminates with reward 00; left returns to ss with probability 0.90.9 and reward 00 or terminates with probability 0.10.1 and reward +1+1), take γ=1\gamma = 1, the target policy π\pi that always selects left and the behaviour policy bb that selects left and right with probability 12\tfrac12 each. Then:

  1. the value of ss under the target policy is vπ(s)=1v_\pi(s) = 1;
  2. the importance-sampling-scaled return has mean one, Eb[ρ0:T−1G0∣S0=s]=1\mathbb E_b[\rho_{0:T-1} G_0 \mid S_0 = s] = 1;
  3. its expected square is infinite:
Eb[(∏t=0T−1π(At∣St)b(At∣St) G0)2]=0.1∑k=0∞0.9k⋅2k⋅2=∞.\mathbb E_b\Bigl[\Bigl(\prod_{t=0}^{T-1} \frac{\pi(A_t \mid S_t)}{b(A_t \mid S_t)}\, G_0\Bigr)^2\Bigr] = 0.1 \sum_{k=0}^{\infty} 0.9^k \cdot 2^k \cdot 2 = \infty .

Hence the ordinary importance-sampling estimator has infinite variance in this example, although its mean is finite and correct.

Formalization Note Episodes here have unbounded length. The expectations are series over episode lengths; the expected square is computed in [0,∞][0, \infty] (ℝ≥0∞), where a divergent series has the value +∞+\infty.

Preamble
import Mathlib
import Definitions.Def_SuttonBartoRL_ImportanceSampling_Episodes
import Definitions.Def_SuttonBartoRL_ImportanceSampling_InfiniteVarianceExample
Formal statement
namespace SuttonBartoRL.ImportanceSampling

/-- Sutton & Barto (2018), Example 5.5 "Infinite Variance", pp. 106–108 (Figure 5.4), with `γ = 1`:
the value of `s` under the target policy (always `left`) is `1`; the importance-sampling-scaled
return `ρ_{0:T-1} G_0` of an episode from `s` under the behaviour policy (`left`/`right` with
probability `1/2`) has mean `1`; and its expected square is `+∞`. -/
theorem infinite_variance_example :
    value exampleMDP exampleTerminal exampleTarget 1 ExState.s = 1 ∧
    expectation exampleMDP exampleTerminal exampleBehavior ExState.s
      (fun n e => e.isRatio exampleTarget exampleBehavior n * e.ret 1) = 1 ∧
    ∑' n : ℕ, ∑ e : Episode exampleMDP n,
      ENNReal.ofReal (episodeProb exampleMDP exampleTerminal exampleBehavior ExState.s e *
        (e.isRatio exampleTarget exampleBehavior n * e.ret 1) ^ 2) = ⊤ := by sorry

end SuttonBartoRL.ImportanceSampling
Source
Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, Example 5.5 'Infinite Variance', pp. 106–108, Figure 5.4
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