Prove2Me

Proof of Lemma B.1, p. 21 — for the step sizes (4.2), α = 1 + β

Proved
AccelVI.MVC.alpha_eq_one_add_beta

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

momentump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1step-size

Let λ∈(0,1)\lambda \in (0,1) and let α,β\alpha, \beta be the constant step sizes (4.2) of Momentum Value Computation,

α=21+1−λ2,β=1−1−λ21+1−λ2.\alpha = \frac{2}{1 + \sqrt{1-\lambda^2}}, \qquad \beta = \frac{1 - \sqrt{1-\lambda^2}}{1 + \sqrt{1-\lambda^2}}.

Then

α=1+β.\alpha = 1 + \beta .

This identity makes the coefficient 1−α+β1 - \alpha + \beta of vsv_s vanish in the expanded M-VC recursion, which is what turns the iteration into the linear recursion xs=Bπxs−1+bπx_s = B_\pi x_{s-1} + b_\pi of Lemma B.1.

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

/-- Proof of Lemma B.1, p. 21: for α, β tuned as in (4.2), α = 1 + β. -/
theorem alpha_eq_one_add_beta (lam : ℝ) (h0 : 0 < lam) (h1 : lam < 1) :
    alphaMVC lam = 1 + betaMVC lam := by sorry

end AccelVI.MVC
Source
Goyal & Grand-Clément, A First-Order Approach to Accelerated Value Iteration, arXiv:1905.09963v7, p. 21, proof of Lemma B.1, first paragraph
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