Prove2Me

Theorem 5.5, p. 10 — for a reversible policy chain, M-VC converges to v^π with v_s = v^π + o(((1 − √(1/κ))/(1 + √(1/κ)) + η)^s) for every η > 0

Proved
AccelVI.MVC.theorem_5_5

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

convergence-ratemarkov-decision-processmomentump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1reversible-markov-chainvalue-iteration

Let (S,A,P,r,λ)(S, A, P, r, \lambda) be a finite MDP with discount factor λ∈(0,1)\lambda \in (0,1), and let π\pi be a policy whose transition matrix LπL_\pi defines an irreducible, reversible Markov chain on SS. Let (vs)s≥0(v_s)_{s \ge 0} be the iterates of Momentum Value Computation

vs+1=vs−α (vs−Tπ(vs))+β (vs−vs−1),s≥1,v_{s+1} = v_s - \alpha\,(v_s - T_\pi(v_s)) + \beta\,(v_s - v_{s-1}), \qquad s \ge 1,

with the constant step sizes (4.2), α=2/(1+1−λ2)\alpha = 2/(1+\sqrt{1-\lambda^2}) and β=(1−1−λ2)/(1+1−λ2)\beta = (1-\sqrt{1-\lambda^2})/(1+\sqrt{1-\lambda^2}), started from arbitrary v0,v1∈Rnv_0, v_1 \in \mathbb{R}^n. Write κ=(1+λ)/(1−λ)\kappa = (1+\lambda)/(1-\lambda). Then:

  1. (vs)s≥0(v_s)_{s \ge 0} converges to the value function vπv^\pi;
  2. for every η>0\eta > 0,
vs=vπ+o ⁣((1−1/κ1+1/κ+η)s)(s→∞);v_s = v^\pi + o\!\left(\left(\frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} + \eta\right)^{s}\right) \quad (s \to \infty);
  1. 0<1−1/κ1+1/κ<λ0 < \dfrac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda.

Momentum Value Computation therefore converges geometrically at a rate strictly better than the rate λ\lambda of Value Computation, and slightly better than the rate 1−1/κ1 - \sqrt{1/\kappa} of Accelerated Value Computation.

Formalization Note. The norm on Rn\mathbb{R}^n is the sup norm ∥⋅∥∞\|\cdot\|_\infty (Mathlib's norm on S → ℝ); the little-o is with respect to it as s→∞s \to \infty. The value function is the Neumann series ∑tλtLπtrπ\sum_t \lambda^t L_\pi^t r_\pi. "Irreducible, reversible" means irreducible plus a stationary probability distribution in detailed balance (Definition 2.1).

Preamble
import Mathlib
import Definitions.Def_mm_basic
import Definitions.Def_AccelVI_MVC_Setting
Formal statement
namespace AccelVI.MVC

variable {S A : Type*} [Fintype S] [DecidableEq S] [Fintype A]

/-- Theorem 5.5, p. 10: if π defines an irreducible, reversible Markov chain, the M-VC iterates with step
sizes (4.2) converge to v^π, v_s = v^π + o(((1 − √(1/κ))/(1 + √(1/κ)) + η)^s) for every η > 0, and
0 < (1 − √(1/κ))/(1 + √(1/κ)) < λ. -/
theorem theorem_5_5 (M : MDP S A) (hM : M.Valid) (pol : S → A → ℝ) (hpol : IsPolicy pol)
    (hrev : AccelVI.AVC.IsReversible (LPol M pol)) (v0 v1 : S → ℝ) :
    Filter.Tendsto (mvc M pol (alphaMVC M.lam) (betaMVC M.lam) v0 v1) Filter.atTop (nhds (valuePol M pol)) ∧
    (∀ η : ℝ, 0 < η →
      (fun s => mvc M pol (alphaMVC M.lam) (betaMVC M.lam) v0 v1 s - valuePol M pol)
        =o[Filter.atTop] (fun s => (rateMVC M.lam + η) ^ s)) ∧
    0 < rateMVC M.lam ∧ rateMVC M.lam < M.lam := by sorry

end AccelVI.MVC
Source
Goyal & Grand-Clément, A First-Order Approach to Accelerated Value Iteration, arXiv:1905.09963v7, p. 10, Theorem 5.5; proof p. 22 (combining Lemma B.1 with Lemma B.2)
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 15, 2026

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

View graph