Conjugate-gradient convergence

Proved

VectorSpaceOpt.conjugate_gradient_converges

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

conjugate-gradienthilbert-spacenorm-convergencestop-stutter

Let $H$ be a real Hilbert space and let $Q : H →L[ℝ] H$ be self-adjoint with constants $0 < m ≤ M$ satisfying

m\|x\|^2 ≤ ⟨x,Qx⟩ ≤ M\|x\|^2

for every $x$ . For any right-hand side $b$ and initial point $x₀$ , there is a unique solution $x^\ast$ of $Q(x^\ast) = b$ , and the iterate component of the guarded conjugate-gradient sequence satisfies

x_n → x^*.

The convergence is in the norm topology of $H$ . The sequence performs Luenberger's recurrence while its direction is nonzero and stutters once a zero direction certifies exact solution. This capstone is §10.8, Theorem 1 with all inherited coercivity hypotheses repeated and its undefined post-termination boundary repaired.

Preamble

import Definitions.Def_VectorSpaceOpt_conjugate_gradient

open Filter

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 10, §10.8, Theorem 1, with total stop/stutter semantics. -/
theorem conjugate_gradient_converges
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (Q : H →L[ℝ] H) (b x₀ : H) (m M : ℝ)
    (hm : 0 < m) (hmM : m ≤ M)
    (hself : IsRealSelfAdjoint Q) (hbounds : IsCoerciveBetween Q m M) :
    ∃ xStar : H, Q xStar = b ∧
      (∀ y : H, Q y = b → y = xStar) ∧
      Tendsto (fun n => (conjugateGradientIterate Q b x₀ n).x) atTop (nhds xStar) := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.8, Theorem 1, printed pp. 294–296 (physical PDF pp. 312–314), with explicit stop/stutter semantics at zero direction. 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 a complete real inner-product space, let $Q:H→H$ be continuous and real-linear, let $b,x₀∈H$ , and let $m,M∈ℝ$ . Assume $m>0$ , $m≤M$ , $Q$ is self-adjoint, and $m‖x‖²≤⟨x,Qx⟩≤M‖x‖²$ for every $x$ . Then there exists $x^*∈H$ such that $Qx^*=b$ , every $y∈H$ satisfying $Qy=b$ equals $x^*$ , and the $x$ -component of the total conjugate-gradient iterate from $x₀$ tends to $x^*$ along the natural-number at-top filter. The iterate uses real divisions as total operations and, whenever its direction is zero, returns the same entire state forever; thus an initially solved system is included. The conclusion gives existence, uniqueness, and convergence, but no explicit rate.

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