Prove2Me

Theorem 4.1 — improvement bound for the conservative update πnew=(1−α)π+απ′\pi_{new}=(1-\alpha)\pi+\alpha\pi'

Proved
ApproxOptRL.CPI.conservative_update_improvement

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

mdpp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1policy-improvementreinforcement-learning

Consider a finite MDP with nonempty state set SS, nonempty action set AA, transition probabilities P(s′;s,a)P(s';s,a), rewards R(s,a)∈[0,R]\mathcal R(s,a)\in[0,R] with R>0R>0, and discount factor 0≤γ<10\le\gamma<1; let μ\mu be a state distribution and let π\pi, π′\pi' be policies.

Let A=Aπ,μ(π′)\mathbb A = \mathbb A_{\pi,\mu}(\pi') be the policy advantage of π′\pi' with respect to π\pi and μ\mu, and let

ε=max⁡s∣Ea∼π′(a;s)[Aπ(s,a)]∣.\varepsilon = \max_s\big|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]\big|.

For the update rule (4.1), πnew(a;s)=(1−α)π(a;s)+απ′(a;s)\pi_{new}(a;s) = (1-\alpha)\pi(a;s)+\alpha\pi'(a;s), and for all α∈[0,1]\alpha\in[0,1]:

ημ(πnew)−ημ(π)≥α1−γ(A−2αγε1−γ(1−α)).\eta_\mu(\pi_{new}) - \eta_\mu(\pi) \ge \frac{\alpha}{1-\gamma}\left(\mathbb A - \frac{2\alpha\gamma\varepsilon}{1-\gamma(1-\alpha)}\right).

The first term is the first-order gain α1−γA\frac{\alpha}{1-\gamma}\mathbb A and the second a penalty for the state distribution of πnew\pi_{new} differing from dπ,μd_{\pi,\mu}. For small α\alpha the bound guarantees improvement whenever the policy advantage is positive; it is the step on which conservative policy iteration rests.

Formalization Note ε\varepsilon is a quantity local to this theorem (the maximum over all states, written as Finset.sup'), unrelated to the accuracy of a greedy chooser. The denominator 1−γ(1−α)1-\gamma(1-\alpha) is positive under 0≤γ<10\le\gamma<1, α∈[0,1]\alpha\in[0,1].

Preamble
import Mathlib
import Definitions.Def_FoundationsML_ReinforcementLearning_IsTransitionKernel
import Definitions.Def_FoundationsML_ReinforcementLearning_IsPolicy
import Definitions.Def_ApproxOptRL_Shared_Model
import Definitions.Def_ApproxOptRL_CPI_PolicyAdvantage
open ApproxOptRL.Shared
open FoundationsML.ReinforcementLearning
Formal statement
namespace ApproxOptRL.CPI

/-- **Theorem 4.1** (Kakade–Langford, ICML 2002, p. 4; proof p. 8). Let `𝔸 = 𝔸_{π,μ}(π')` be
the policy advantage of `π'` with respect to `π` and `μ`, and let
`ε = max_s |E_{a ∼ π'(a;s)}[A_π(s, a)]|`. For the update rule (4.1),
`π_new = (1 - α) π + α π'`, and for all `α ∈ [0, 1]`:
`η_μ(π_new) - η_μ(π) ≥ (α/(1-γ)) (𝔸 - 2αγε/(1 - γ(1 - α)))`.
Here `ε` is a quantity local to this theorem (not the accuracy of a greedy chooser).
Standing assumptions of the paper's §2: finite nonempty `S`, `A`; transition kernel `P`;
rewards in `[0, R]`; `0 ≤ γ < 1`; `μ` a state distribution. -/
theorem conservative_update_improvement {S A : Type} [Fintype S] [Fintype A] [DecidableEq S]
    [Nonempty S] [Nonempty A]
    (P : S → A → S → ℝ) (hP : IsTransitionKernel P)
    (r : S → A → ℝ) (R : ℝ) (hR : 0 < R) (hr : ∀ s a, 0 ≤ r s a ∧ r s a ≤ R)
    (γ : ℝ) (hγ0 : 0 ≤ γ) (hγ1 : γ < 1)
    (μ : S → ℝ) (hμ : IsStateDist μ)
    (π π' : S → A → ℝ) (hπ : IsPolicy π) (hπ' : IsPolicy π')
    (α : ℝ) (hα : α ∈ Set.Icc (0 : ℝ) 1) :
    let ε : ℝ := Finset.univ.sup' Finset.univ_nonempty
      (fun s => |∑ a, π' s a * advantage P r γ π s a|)
    α / (1 - γ) * (policyAdvantage P r γ π μ π' - 2 * α * γ * ε / (1 - γ * (1 - α))) ≤
      eta P r γ (mixPolicy α π π') μ - eta P r γ π μ := by sorry

end ApproxOptRL.CPI
Source
Kakade, Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002, p. 4, Theorem 4.1 (proof p. 8, appendix §8)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph