Prove2Me

Batch TD(0) fixed points are exactly the certainty-equivalence estimate

Proved
SuttonBartoRL.BatchTD.batch_td_fixed_point_iff_certainty_equivalence

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

markov-chainp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1reinforcement-learningtemporal-difference-learning

Fix a finite batch of episodes over a finite set S\mathcal S of nonterminal states, each ending in the terminal state, and γ∈[0,1]\gamma \in [0, 1]. Let P^\hat P, r^\hat r be the maximum-likelihood Markov reward process of the batch and

v^(s)=∑k≥0γk(P^kr^)(s)\hat v(s) = \sum_{k \ge 0} \gamma^k (\hat P^k \hat r)(s)

its value function, the certainty-equivalence estimate. Then:

  1. the series defining v^(s)\hat v(s) converges at every s∈Ss \in \mathcal S;
  2. for every array VV, the batch TD(0) increment ∑visits t of s[Rt+1+γV(St+1)−V(St)]\sum_{\text{visits } t \text{ of } s}[R_{t+1} + \gamma V(S_{t+1}) - V(S_t)] vanishes at every state if and only if V(s)=v^(s)V(s) = \hat v(s) for every state ss visited in the batch.

This is the statement that batch TD(0) finds the estimates that would be exactly correct for the maximum-likelihood model: the answer of batch TD(0) is characterized without reference to α\alpha.

Formalization Note The case γ=1\gamma = 1 (used in Example 6.4) is included; no hypothesis on the batch beyond finiteness is made, because every episode ends in the terminal state by construction. Values at unvisited states are unconstrained, as they receive no increment.

Preamble
import Mathlib
import Definitions.Def_SuttonBartoRL_BatchTD_Episodes
import Definitions.Def_SuttonBartoRL_BatchTD_BatchUpdating
Formal statement
namespace SuttonBartoRL.BatchTD

/-- §6.3, p. 128: batch TD(0) "always finds the estimates that would be exactly correct for the
maximum-likelihood model of the Markov process". For `γ ∈ [0, 1]`, the series defining the
certainty-equivalence estimate converges at every state, and an array `V` is a fixed point of
batch TD(0) (the sum of all increments vanishes at every state) iff `V` agrees with the
certainty-equivalence estimate on every state visited in the batch. -/
theorem batch_td_fixed_point_iff_certainty_equivalence {S : Type} [Fintype S] [DecidableEq S]
    (b : Batch S) (γ : ℝ) (hγ0 : 0 ≤ γ) (hγ1 : γ ≤ 1) :
    (∀ s : S, Summable fun k : ℕ => γ ^ k * (Matrix.mulVec (mlMatrix b ^ k) (mlExpectedReward b)) s) ∧
    ∀ V : S → ℝ,
      (∀ s : S, tdIncrement γ b V s = 0) ↔
        ∀ s : S, visitCount b s ≠ 0 → V s = ceEstimate γ b s := by sorry

end SuttonBartoRL.BatchTD
Source
Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, §6.3, p. 128
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