Convergence along complete conjugate directions

Proved

VectorSpaceOpt.conjugate_directions_converge

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

conjugate-directionsconvergencedense-spanorthogonality

Let Q be self-adjoint and coercively bounded on a real Hilbert space, and let xStar solve Q xStar = b. Suppose p n is a sequence of nonzero, pairwise Q-orthogonal directions whose closed linear span is the whole space. Define residuals r n = b - Q (x n) and take each next iterate by exact minimization along p n, using the displayed scalar ratio in §10.6. Then

⟨r_n,p_k⟩=0 \quad (k<n), \qquad x_n → x^*.

This is Luenberger's method-of-conjugate-directions theorem. Explicit nonzeroness prevents hidden zero denominators, while density is the completeness hypothesis that converts all finite orthogonality relations into norm convergence.

Preamble

import Definitions.Def_VectorSpaceOpt_conjugate_gradient

open Filter Set
open scoped RealInnerProductSpace

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 10, §10.6, Theorem 1. -/
theorem conjugate_directions_converge
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (Q : H →L[ℝ] H) (b xStar : H) (m M : ℝ) (hm : 0 < m)
    (hself : IsRealSelfAdjoint Q) (hbounds : IsCoerciveBetween Q m M)
    (hxStar : Q xStar = b) (p x r : ℕ → H)
    (hpne : ∀ n, p n ≠ 0)
    (hconj : ∀ i j, i ≠ j → ⟪p i, Q (p j)⟫ = 0)
    (hdense : closure ((Submodule.span ℝ (Set.range p) : Submodule ℝ H) : Set H) = Set.univ)
    (hres : ∀ n, r n = b - Q (x n))
    (hstep : ∀ n,
      x (n + 1) = x n + (⟪p n, r n⟫ / ⟪p n, Q (p n)⟫) • p n) :
    (∀ n k, k < n → ⟪r n, p k⟫ = 0) ∧ Tendsto x atTop (nhds xStar) := by
  sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.6, Theorem 1, printed pp. 291–292 (physical PDF pp. 309–310). 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, and let $b,x^*∈H$ and $m,M∈ℝ$ . Assume $m>0$ , $Q$ is self-adjoint, $m‖z‖²≤⟨z,Qz⟩≤M‖z‖²$ for every $z$ , and $Qx^*=b$ . Let $p,x,r:ℕ→H$ be arbitrary sequences satisfying: $p_n≠0$ for every $n$ ; $⟨p_i,Qp_j⟩=0$ for every distinct pair $i,j$ ; the closure of the real linear span of the range of $p$ is all of $H$ ; $r_n=b-Qx_n$ for every $n$ ; and $x_{n+1}=x_n+(⟨p_n,r_n⟩/⟨p_n,Qp_n⟩)p_n$ for every $n$ . Then both of the following hold: for all naturals $n,k$ with $k<n$ , $⟨r_n,p_k⟩=0$ ; and $x_n$ tends to $x^*$ as $n→∞$ in the norm topology. The update's division is total, but $m>0$ and $p_n≠0$ imply its denominator $⟨p_n,Qp_n⟩$ is positive. No recurrence for the directions $p_n$ or residuals beyond the displayed assumptions is imposed.

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