p. 22 — 0 < (1 − √(1/κ))/(1 + √(1/κ)) < λ for λ ∈ (0, 1)

Proved

AccelVI.MVC.rate_bounds

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

convergence-ratemomentump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\lambda \in (0,1)$ and $\kappa = (1+\lambda)/(1-\lambda)$ . Then

0 < \frac{1 - \sqrt{1/\kappa}}{1 + \sqrt{1/\kappa}} < \lambda .

So the rate of Momentum Value Computation is strictly better than the rate $\lambda$ of plain Value Computation.

Preamble

import Mathlib
import Definitions.Def_mm_basic
import Definitions.Def_AccelVI_MVC_Setting

Formal statement

namespace AccelVI.MVC

/-- p. 22: 0 < (1 − √(1/κ))/(1 + √(1/κ)) < λ for λ ∈ (0, 1). -/
theorem rate_bounds (lam : ℝ) (h0 : 0 < lam) (h1 : lam < 1) :
    0 < rateMVC lam ∧ rateMVC lam < lam := by sorry

end AccelVI.MVC

Source

Goyal & Grand-Clément, A First-Order Approach to Accelerated Value Iteration, arXiv:1905.09963v7, p. 22, sentence after the proof of Lemma B.2 (and Theorem 5.5, p. 10, last sentence)

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