Prove2Me

Corollary 4.2 — the step size α=(1−γ)A4R\alpha=\frac{(1-\gamma)\mathbb A}{4R} improves ημ\eta_\mu by at least A28R\frac{\mathbb A^2}{8R}

Proved
ApproxOptRL.CPI.conservative_update_step_size

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. If A≥0\mathbb A\ge 0, then the conservative update πnew=(1−α)π+απ′\pi_{new} = (1-\alpha)\pi+\alpha\pi' with

α=(1−γ)A4R\alpha = \frac{(1-\gamma)\mathbb A}{4R}

guarantees the policy improvement

ημ(πnew)−ημ(π)≥A28R.\eta_\mu(\pi_{new}) - \eta_\mu(\pi) \ge \frac{\mathbb A^2}{8R}.

The larger the policy advantage, the larger the guaranteed increase in performance; this is the quantitative improvement that bounds the number of iterations of conservative policy iteration.

Formalization Note The paper's "RR the maximal possible reward" is formalized as any upper bound R>0R>0 on the rewards (rewards in [0,R][0,R]), not necessarily attained; the statement is the paper's for the attained maximum and holds for every such bound. The condition α≤1\alpha\le1 is not assumed: it follows from A≤R\mathbb A\le R.

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

/-- **Corollary 4.2** (Kakade–Langford, ICML 2002, p. 5). Let `R` be the maximal possible
reward and `𝔸 = 𝔸_{π,μ}(π')` the policy advantage of `π'` with respect to `π` and `μ`. If
`𝔸 ≥ 0`, then the update (4.1) with `α = (1 - γ)𝔸/(4R)` guarantees
`η_μ(π_new) - η_μ(π) ≥ 𝔸²/(8R)`.
`R` is any upper bound on the rewards (rewards in `[0, R]`, `R > 0`), not necessarily the
attained maximum. Standing assumptions of §2: finite nonempty `S`, `A`; transition kernel `P`;
`0 ≤ γ < 1`; `μ` a state distribution. -/
theorem conservative_update_step_size {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 π')
    (hA : 0 ≤ policyAdvantage P r γ π μ π') :
    let α : ℝ := (1 - γ) * policyAdvantage P r γ π μ π' / (4 * R)
    (policyAdvantage P r γ π μ π') ^ 2 / (8 * R) ≤
      eta P r γ (mixPolicy α π π') μ - eta P r γ π μ := by sorry

end ApproxOptRL.CPI
Source
Kakade, Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002, p. 5, Corollary 4.2
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