Proof of Lemma B.2, p. 22 — |ω±(µ)| = λ/(1 + √(1 − λ²)) for µ ∈ [−1, 1] (printed √(1 − λ)²)

Proved

AccelVI.MVC.omega_modulus

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

complex-numbersmomentump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1spectrum

Let $\lambda \in (0,1)$ and $\mu \in [-1, 1]$ , and let

\omega^{\pm}(\mu) = \frac{\lambda}{1 + \sqrt{1-\lambda^2}}\Big(\mu \pm i\sqrt{1-\mu^2}\Big)

be the two roots (B.2)–(B.3) of (B.1). Then

|\omega^+(\mu)| = |\omega^-(\mu)| = \frac{\lambda}{1 + \sqrt{1-\lambda^2}} .

Since the eigenvalues of $L_\pi$ lie in $[-1,1]$ for a reversible chain, every eigenvalue of $B_\pi$ has this same modulus.

Formalization Note. The page prints the constant as $\lambda/(1 + \sqrt{1-\lambda})^2$ , a typesetting slip: (B.2)–(B.3) on p. 21 carry $\lambda/(1+\sqrt{1-\lambda^2})$ , and only that value equals the rate of Theorem 5.5. The modulus is the complex absolute value.

Preamble

import Mathlib
import Definitions.Def_mm_basic
import Definitions.Def_AccelVI_MVC_Setting

Formal statement

namespace AccelVI.MVC

/-- Proof of Lemma B.2, p. 22, first display (with λ/(1 + √(1 − λ²)) for the printed λ/(1 + √(1 − λ)²)):
for μ ∈ [−1, 1], the roots ω^±(μ) = λ/(1 + √(1 − λ²)) · (μ ± i√(1 − μ²)) of (B.1), given in (B.2)–(B.3),
both have modulus λ/(1 + √(1 − λ²)). -/
theorem omega_modulus (lam : ℝ) (h0 : 0 < lam) (h1 : lam < 1) (μ : ℝ) (hμ1 : -1 ≤ μ) (hμ2 : μ ≤ 1) :
    ‖((lam / (1 + Real.sqrt (1 - lam ^ 2)) : ℝ) : ℂ) * ((μ : ℂ) + Complex.I * (Real.sqrt (1 - μ ^ 2) : ℂ))‖
        = lam / (1 + Real.sqrt (1 - lam ^ 2)) ∧
      ‖((lam / (1 + Real.sqrt (1 - lam ^ 2)) : ℝ) : ℂ) * ((μ : ℂ) - Complex.I * (Real.sqrt (1 - μ ^ 2) : ℂ))‖
        = lam / (1 + Real.sqrt (1 - lam ^ 2)) := by sorry

end AccelVI.MVC

Source

Goyal & Grand-Clément, A First-Order Approach to Accelerated Value Iteration, arXiv:1905.09963v7, p. 22, proof of Lemma B.2, first line (with (B.2)–(B.3), p. 21)

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