Prove2Me

The gradient of vπv_\pi in terms of qπq_\pi and ∇vπ\nabla v_\pi (proof box, p. 325)

Proved
SuttonBartoRL.PolicyGradient.grad_stateValue_recursion

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

p2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1policy-gradientreinforcement-learning

Let a finite episodic MDP and a differentiable policy parameterization be given, and let episodes terminate under πθ0\pi_{\theta_0}. Then for every nonterminal state ss the map θ↦vπθ(s)\theta \mapsto v_{\pi_\theta}(s) is differentiable at θ0\theta_0, and, with π(a∣s)=π(a∣s,θ0)\pi(a\mid s) = \pi(a\mid s,\theta_0), qπ=qπθ0q_\pi = q_{\pi_{\theta_0}} and all gradients taken at θ0\theta_0,

∇vπ(s)=∑a[∇π(a∣s) qπ(s,a)+π(a∣s)∑s′∈Sp(s′∣s,a) ∇vπ(s′)].\nabla v_\pi(s) = \sum_a \Big[\nabla \pi(a \mid s)\, q_\pi(s,a) + \pi(a\mid s) \sum_{s' \in \mathcal S} p(s' \mid s, a)\, \nabla v_\pi(s')\Big].

This is the recursion that the proof of the policy gradient theorem unrolls.

Formalization Note The existence of ∇vπ\nabla v_\pi, used silently in the book, is part of the conclusion. Termination is assumed at θ0\theta_0 only; because the policy is continuous in θ\theta, it then holds in a neighbourhood of θ0\theta_0.

Preamble
import Mathlib
import Definitions.Def_SuttonBartoRL_PolicyGradient_Model
import Definitions.Def_SuttonBartoRL_PolicyGradient_EpisodicValues
Formal statement
namespace SuttonBartoRL.PolicyGradient

/-- Box "Proof of the Policy Gradient Theorem (episodic case)", p. 325, first four lines: if episodes
terminate under `π_{θ₀}`, then every state value `θ ↦ v_{π_θ}(s)` is differentiable at `θ₀` and
`∇v_π(s) = Σ_a [∇π(a|s) q_π(s, a) + π(a|s) Σ_{s'} p(s'|s, a) ∇v_π(s')]`. -/
theorem grad_stateValue_recursion {S A : Type} [Fintype S] [DecidableEq S] [Fintype A] {d : ℕ}
    (M : EpisodicMDP S A) (π : ParamPolicy S A d) (θ₀ : EuclideanSpace ℝ (Fin d))
    (hT : M.Terminates π θ₀) (s : S) :
    HasGradientAt (fun θ => M.stateValue π θ s)
      (∑ a, (M.actionValue π θ₀ s a • gradient (fun θ => π.prob θ s a) θ₀ +
        π.prob θ₀ s a • ∑ s', M.trans s a s' • gradient (fun θ => M.stateValue π θ s') θ₀))
      θ₀ := by sorry

end SuttonBartoRL.PolicyGradient
Source
Sutton & Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press (2018), ISBN 9780262039246, box "Proof of the Policy Gradient Theorem (episodic case)", first four lines, p. 325
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