Prove2Me

Exercise 10.7: differential values −1/3,0,1/3-1/3, 0, 1/3 in the three-state ring

Proved
SuttonBartoRL.AverageReward.exercise_10_7

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

average-rewardexercisep2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1reinforcement-learning

In the ring Markov reward process A→B→C→A\mathsf A \to \mathsf B \to \mathsf C \to \mathsf A with reward +1+1 upon arrival in A\mathsf A and 00 otherwise:

  1. the average reward (10.6) is 13\tfrac13 from every starting state;
  2. with r(π)=13r(\pi) = \tfrac13, the differential values (10.13) are
v(A)=−13,v(B)=0,v(C)=13.v(\mathsf A) = -\tfrac13,\qquad v(\mathsf B) = 0, \qquad v(\mathsf C) = \tfrac13 .

The book leaves the answer to the reader; it is computed here. The chain is periodic, so the limit (10.7) does not exist, but (10.13) gives well-defined differential values. The same ring is used in Exercise 10.8, which gives 13\tfrac13 as the true average reward.

Formalization Note A,B,C\mathsf A, \mathsf B, \mathsf C are the states 0, 1, 2 of Fin 3 in ringMRP.

Preamble
import Mathlib
import Definitions.Def_SuttonBartoRL_AverageReward_MDP
import Definitions.Def_SuttonBartoRL_AverageReward_AverageReward
import Definitions.Def_SuttonBartoRL_AverageReward_RingMRP

open Filter Topology
Formal statement
namespace SuttonBartoRL.AverageReward

/-- Sutton & Barto (2018), Exercise 10.7, p. 251 (answers not printed; computed here). In the ring
Markov reward process `A → B → C → A` with reward `+1` upon arrival in `A` (`A = 0`, `B = 1`,
`C = 2`), the average reward (10.6) is `1/3` from every state, and the differential values (10.13)
with `r(π) = 1/3` are `v(A) = −1/3`, `v(B) = 0`, `v(C) = 1/3`. -/
theorem exercise_10_7 :
    (∀ s : Fin 3, Tendsto (fun h : ℕ => (1 / (h : ℝ)) *
        ∑ t ∈ Finset.range h, ringMRP.expectedRewardAt ringPolicy t s) atTop (𝓝 (1 / 3))) ∧
    HasDifferentialValue ringMRP ringPolicy (1 / 3) 0 (-1 / 3) ∧
    HasDifferentialValue ringMRP ringPolicy (1 / 3) 1 0 ∧
    HasDifferentialValue ringMRP ringPolicy (1 / 3) 2 (1 / 3) := by sorry

end SuttonBartoRL.AverageReward
Source
Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, Exercise 10.7 with Eq. (10.13), p. 251 (no solution printed); average reward 1/3 stated in Exercise 10.8, p. 251
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