Total conjugate-gradient iteration

Definition

VectorSpaceOpt_conjugate_gradient

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

conjugate-gradientdefinitionguarded-recursionhilbert-space

For a real inner-product space, IsRealSelfAdjoint Q expresses symmetry of a continuous linear operator, and IsCoerciveBetween Q m M records its lower and upper quadratic bounds. A conjugate-gradient state stores an iterate x, residual r, and direction p. Starting from r₀ = p₀ = b - Q x₀, an active step uses

α=⟨r,p⟩/⟨p,Qp⟩, \quad x^+=x+αp, \quad β=⟨r^+,Qp⟩/⟨p,Qp⟩, \quad p^+=r^+-βp.

If p = 0, the state is returned unchanged. Thus conjugateGradientIterate is a total natural-number sequence with explicit exact-termination semantics, and conjugateGradientEnergy records the quadratic error energy used in convergence. The stop/stutter convention is essential for auditing every later denominator.

Definition code

import Mathlib

open Filter Set
open scoped RealInnerProductSpace

namespace VectorSpaceOpt

/-- A real continuous linear operator is self-adjoint when it can be moved across the inner product. -/
def IsRealSelfAdjoint
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) : Prop :=
  ∀ x y : H, ⟪Q x, y⟫ = ⟪x, Q y⟫

/-- The lower and upper quadratic bounds used throughout §§10.5–10.8. -/
def IsCoerciveBetween
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) (m M : ℝ) : Prop :=
  ∀ x : H, m * ‖x‖ ^ 2 ≤ ⟪x, Q x⟫ ∧ ⟪x, Q x⟫ ≤ M * ‖x‖ ^ 2

/-- The three vectors carried by one conjugate-gradient iteration. -/
structure ConjugateGradientState (H : Type*) where
  x : H
  r : H
  p : H

/-- One conjugate-gradient step, explicitly stuttering after `p = 0`. -/
noncomputable def conjugateGradientStep
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) (b : H) (s : ConjugateGradientState H) :
    ConjugateGradientState H :=
  letI := Classical.decEq H
  if s.p = 0 then s
  else
    let alpha : ℝ := ⟪s.r, s.p⟫ / ⟪s.p, Q s.p⟫
    let xNext : H := s.x + alpha • s.p
    let rNext : H := b - Q xNext
    let beta : ℝ := ⟪rNext, Q s.p⟫ / ⟪s.p, Q s.p⟫
    { x := xNext, r := rNext, p := rNext - beta • s.p }

/-- The total conjugate-gradient sequence, with initial direction equal to the initial residual. -/
noncomputable def conjugateGradientIterate
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) (b x₀ : H) (n : ℕ) : ConjugateGradientState H :=
  (conjugateGradientStep Q b)^[n]
    { x := x₀, r := b - Q x₀, p := b - Q x₀ }

/-- The quadratic error energy used in the convergence proof. -/
def conjugateGradientEnergy
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) (xStar x : H) : ℝ :=
  ⟪x - xStar, Q (x - xStar)⟫

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.6 and §10.8, definitions and recurrences, printed pp. 290–295 (physical PDF pp. 308–313), with explicit stop/stutter added at the omitted zero-direction boundary. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

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

IsRealSelfAdjoint. For any type $H$ carrying a normed additive commutative-group structure and a real inner-product-space structure, and any continuous real-linear map $Q:H→H$ , this predicate means that for every $x,y∈H$ , $⟨Qx,y⟩=⟨x,Qy⟩$ . It imposes neither completeness nor positivity.

IsCoerciveBetween. For such an $H$ , a continuous real-linear $Q$ , and arbitrary real numbers $m,M$ , this predicate means that every $x∈H$ simultaneously satisfies $m‖x‖²≤⟨x,Qx⟩$ and $⟨x,Qx⟩≤M‖x‖²$ . The definition itself does not require $m>0$ , $m≤M$ , or completeness; it also includes $x=0$ .

ConjugateGradientState. For an arbitrary type $H$ , a state is exactly a record of three elements of $H$ , named $x$ , $r$ , and $p$ ; the structure itself assumes no algebraic operations on $H$ .

conjugateGradientStep. Given a real inner-product space $H$ , a continuous real-linear $Q:H→H$ , a vector $b$ , and a state $s=(x,r,p)$ , one step first tests equality $p=0$ . If $p=0$ , it returns the identical state, so every later application also stutters. If $p≠0$ , it sets $α=⟨r,p⟩/⟨p,Qp⟩$ , $x_{next}=x+αp$ , $r_{next}=b-Qx_{next}$ , $β=⟨r_{next},Qp⟩/⟨p,Qp⟩$ , and returns $(x_{next},r_{next},r_{next}-βp)$ . This total definition has no hypothesis that $⟨p,Qp⟩$ is nonzero: real division by zero is defined, yielding $α=0$ and $β=0$ when that denominator is zero.

conjugateGradientIterate. Given $Q,b,x₀$ and $n∈ℕ$ , this is the result of applying the preceding step exactly $n$ times to the initial state $(x₀,b-Qx₀,b-Qx₀)$ . At $n=0$ it is exactly that initial state; if any step reaches $p=0$ , all subsequent states are the same by the step definition.

conjugateGradientEnergy. Given $Q$ and vectors $x^*,x$ , the energy is the real number $⟨x-x^*,Q(x-x^*)⟩$ . Without additional assumptions on $Q$ , this definition does not assert that the value is nonnegative.

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