If the greedy policy is no better, both policies are optimal

Proved

SuttonBartoRL.DP.greedy_no_improvement_optimal

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 \le \gamma < 1$ , and let $\pi'$ be a deterministic policy greedy with respect to $q_\pi$ (4.9). Suppose $\pi'$ is as good as, but not better than, $\pi$ , i.e. $v_{\pi'} = v_\pi$ . Then

$v_{\pi'}$ satisfies the Bellman optimality equation (4.1): for all $s$ ,

v_{\pi'}(s) \;=\; \max_a \sum_{s',r} p(s',r\mid s,a)\,\big[r+\gamma v_{\pi'}(s')\big];

$v_{\pi'} = v_*$ , the optimal value function;
both $\pi$ and $\pi'$ are optimal policies.

Consequently policy improvement yields a strictly better policy unless the original policy is already optimal.

Formalization Note Optimality is with respect to all stochastic policies, and $v_*(s)$ is the supremum of $v_\pi(s)$ over all stochastic policies.

Preamble

import Mathlib
import Definitions.Def_SuttonBartoRL_DP_MDP
import Definitions.Def_SuttonBartoRL_DP_ValueFunctions

Formal statement

namespace SuttonBartoRL.DP

/-- Sutton & Barto (2018), p. 79: if the deterministic policy `π'` is greedy with respect to
`q_π` and is as good as, but not better than, the deterministic policy `π` (`v_{π'} = v_π`),
then `v_{π'}` satisfies the Bellman optimality equation (4.1),
`v_{π'}(s) = max_a Σ_{s', r} p(s', r | s, a) [r + γ v_{π'}(s')]`, `v_{π'} = v_*`, and both `π` and
`π'` are optimal policies. -/
theorem greedy_no_improvement_optimal {S A : Type} [Fintype S] [DecidableEq S] [Fintype A]
    [DecidableEq A] [Nonempty A] (M : MDP S A) (γ : ℝ) (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
    (π π' : S → A) (hgreedy : IsGreedy M γ (Policy.ofDet π) π')
    (heq : ∀ s, stateValue M γ (Policy.ofDet π') s = stateValue M γ (Policy.ofDet π) s) :
    (∀ s, stateValue M γ (Policy.ofDet π') s =
      Finset.univ.sup' Finset.univ_nonempty (fun a : A =>
        ∑ s', ∑ r ∈ M.R, M.p s a s' r * (r + γ * stateValue M γ (Policy.ofDet π') s'))) ∧
    (∀ s, stateValue M γ (Policy.ofDet π') s = optimalValue M γ s) ∧
    IsOptimalPolicy M γ (Policy.ofDet π) ∧ IsOptimalPolicy M γ (Policy.ofDet π') := by sorry

end SuttonBartoRL.DP

Source

Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, §4.2, p. 79 (paragraph after (4.9))

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