One-step conjugate-gradient energy contraction

Proved

VectorSpaceOpt.cg_energy_contraction

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

coercivityconjugate-gradientenergy-estimatelinear-contraction

Let xStar solve Q xStar = b, with Q self-adjoint and satisfying 0 < m ≤ M and the standard quadratic bounds. At any iteration whose search direction is nonzero, the guarded conjugate-gradient step contracts the quadratic error energy by the uniform factor 1 - m/M:

E(x_{n+1}) ≤ (1-m/M)E(x_n), \qquad E(x)=⟨x-x^*,Q(x-x^*)⟩.

This is the estimate at the top of printed p. 296. The active-step premise ensures both recurrence denominators are justified; after exact termination the total sequence stutters at a solution and needs no contraction division. The lemma is the quantitative bridge from the recurrence invariants to norm convergence.

Preamble

import Definitions.Def_VectorSpaceOpt_conjugate_gradient

Formal statement

namespace VectorSpaceOpt

/-- Equation at the top of p. 296: the one-step energy contraction. -/
theorem cg_energy_contraction
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) (b x₀ xStar : H) (m M : ℝ)
    (hm : 0 < m) (hmM : m ≤ M) (hxStar : Q xStar = b)
    (hself : IsRealSelfAdjoint Q) (hbounds : IsCoerciveBetween Q m M) :
    ∀ n : ℕ, (conjugateGradientIterate Q b x₀ n).p ≠ 0 →
      conjugateGradientEnergy Q xStar (conjugateGradientIterate Q b x₀ (n + 1)).x ≤
        (1 - m / M) *
          conjugateGradientEnergy Q xStar (conjugateGradientIterate Q b x₀ n).x := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.8, energy estimate in the proof of Theorem 1, printed pp. 295–296 (physical PDF pp. 313–314). Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5

Let $H$ be any real inner-product space, let $Q:H→H$ be continuous and real-linear, let $b,x₀,x^*∈H$ , and let $m,M∈ℝ$ . Assume $m>0$ , $m≤M$ , $Qx^*=b$ , $Q$ is self-adjoint in the sense $⟨Qx,y⟩=⟨x,Qy⟩$ , and $m‖x‖²≤⟨x,Qx⟩≤M‖x‖²$ for all $x$ . For every $n∈ℕ$ such that the direction $p_n$ in the total conjugate-gradient iterate is nonzero, the energies $E_n=⟨x_n-x^*,Q(x_n-x^*)⟩$ obey $E_{n+1}≤(1-m/M)E_n$ . The quotient $m/M$ is real division; the stated bounds and $m>0$ force $M>0$ , although division and the underlying iteration are total even at zero denominators. If $p_n=0$ , this theorem's implication makes no assertion for that $n$ , even though the iteration itself stutters from then on. Completeness of $H$ is not assumed.

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by wenxinzhang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph