Prove2Me

Conjugacy of active CG directions

Proved
VectorSpaceOpt.cg_directions_conjugate_until_stop

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

conjugate-gradientinvariantpre-terminationq-orthogonality

Run the total conjugate-gradient iteration for a self-adjoint operator with a positive coercivity bound. Fix an index n and assume every stored direction through step n is nonzero, so the run has not yet entered its stuttering state. Then any two distinct active directions with indices i < j ≤ n are orthogonal in the Q inner product:

⟨pi,Qpj⟩=0.⟨p_i,Qp_j⟩=0.

This is the central invariant established in the first half of §10.8, Theorem 1. Its premise makes the algorithm's termination boundary explicit. The result can feed the general conjugate-directions theorem or be reused directly to establish residual orthogonality and finite-dimensional exact termination.

Preamble
import Definitions.Def_VectorSpaceOpt_conjugate_gradient

open scoped RealInnerProductSpace
Formal statement
namespace VectorSpaceOpt

/-- The conjugacy invariant proved in §10.8 before the convergence estimate. -/
theorem cg_directions_conjugate_until_stop
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    (Q : H →L[ℝ] H) (b x₀ : H) (m M : ℝ) (hm : 0 < m)
    (hself : IsRealSelfAdjoint Q) (hbounds : IsCoerciveBetween Q m M) :
    ∀ n : ℕ,
      (∀ k ≤ n, (conjugateGradientIterate Q b x₀ k).p ≠ 0) →
      ∀ i j, i < j → j ≤ n →
        ⟪(conjugateGradientIterate Q b x₀ i).p,
          Q ((conjugateGradientIterate Q b x₀ j).p)⟫ = 0 := by
  sorry

end VectorSpaceOpt
Source
David G. Luenberger, Optimization by Vector Space Methods (Wiley, 1969), Chapter 10, §10.8, proof of Theorem 1, printed p. 295 (physical PDF p. 313), restricted explicitly to pre-termination iterates. 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 HH be any real inner-product space, not assumed complete; let Q:H→HQ:H→H be continuous and real-linear; let b,x0∈Hb,x₀∈H and m,M∈Rm,M∈ℝ. Assume m>0m>0, assume ⟨Qx,y⟩=⟨x,Qy⟩⟨Qx,y⟩=⟨x,Qy⟩ for all x,yx,y, and assume m‖x‖2≤⟨x,Qx⟩≤M‖x‖2m‖x‖²≤⟨x,Qx⟩≤M‖x‖² for every xx. Write (xn,rn,pn)(x_n,r_n,p_n) for the total conjugate-gradient iterate initialized by (x0,b−Qx0,b−Qx0)(x₀,b-Qx₀,b-Qx₀) and using the stated stop/stutter step. Then, for every n∈Nn∈ℕ, if pk≠0p_k≠0 for every natural k≤nk≤n, every pair of natural indices i<j≤ni<j≤n satisfies ⟨pi,Qpj⟩=0⟨p_i,Qp_j⟩=0. If some pkp_k with k≤nk≤n is zero, the implication for that nn asserts nothing; for n=0n=0 its indexed conclusion is vacuous because no i<j≤0i<j≤0 exist. No conjugacy claim is made here after the stopping condition has occurred.

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