Prove2Me

The greedy policy (4.9) satisfies (4.7) and improves on π\pi

Proved
SuttonBartoRL.DP.greedy_policy_improves

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

dynamic-programmingp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1reinforcement-learning

Let π\pi be a deterministic policy of a finite MDP with discount 0≤γ<10 \le \gamma < 1, and let π′\pi' be a deterministic policy that is greedy with respect to qπq_\pi:

π′(s)∈argmax⁡aqπ(s,a)=argmax⁡a∑s′,rp(s′,r∣s,a) [r+γvπ(s′)]for all s,\pi'(s) \in \operatorname*{argmax}_a q_\pi(s,a) = \operatorname*{argmax}_a \sum_{s',r} p(s',r\mid s,a)\,\big[r+\gamma v_\pi(s')\big] \qquad \text{for all } s,

with ties broken arbitrarily. Then

  1. π′\pi' meets the condition (4.7) of the policy improvement theorem: qπ(s,π′(s))≥vπ(s)q_\pi(s, \pi'(s)) \ge v_\pi(s) for all ss;
  2. π′\pi' is as good as, or better than, π\pi: vπ′(s)≥vπ(s)v_{\pi'}(s) \ge v_\pi(s) for all ss.

This is the policy improvement step of policy iteration.

Formalization Note Values are expected discounted returns with 0≤γ<10\le\gamma<1; qπq_\pi is defined by (4.6). A deterministic policy is identified with the stochastic policy selecting π(s)\pi(s) with probability one.

Preamble
import Mathlib
import Definitions.Def_SuttonBartoRL_DP_MDP
import Definitions.Def_SuttonBartoRL_DP_ValueFunctions
Formal statement
namespace SuttonBartoRL.DP

/-- Greedy policy improvement, Sutton & Barto (2018), (4.9), p. 79: if the deterministic policy
`π'` is greedy with respect to `q_π` for a deterministic policy `π`, then `π'` meets the
condition (4.7), `q_π(s, π'(s)) ≥ v_π(s)` for all `s`, and it is as good as or better than `π`:
`v_{π'}(s) ≥ v_π(s)` for all `s`. -/
theorem greedy_policy_improves {S A : Type} [Fintype S] [DecidableEq S] [Fintype A]
    [DecidableEq A] (M : MDP S A) (γ : ℝ) (hγ0 : 0 ≤ γ) (hγ1 : γ < 1) (π π' : S → A)
    (hgreedy : IsGreedy M γ (Policy.ofDet π) π') :
    (∀ s, stateValue M γ (Policy.ofDet π) s ≤ actionValue M γ (Policy.ofDet π) s (π' s)) ∧
    (∀ s, stateValue M γ (Policy.ofDet π) s ≤ stateValue M γ (Policy.ofDet π') s) := by sorry

end SuttonBartoRL.DP
Source
Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, Eq. (4.9) and the paragraph after it, p. 79
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