Theorem 5:1, eq. (5:3d) — $(r_i,Ap_i)=(p_i,Ap_i)$ and $(r_i,Ap_j)=0$ for $i\ne j, j+1$

Proved

ConjGrad.Termination.cg_residual_Adirection

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

conjugate-gradientnumerical-linear-algebrap2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $A$ be a real symmetric positive definite $n \times n$ matrix, let $k, x_0 \in \mathbb{R}^n$ , and let $r_i$ , $p_i$ be the residuals and directions produced by the conjugate gradient method (3:1) started at $x_0$ . Then

(r_i, Ap_i) = (p_i, Ap_i), \qquad (r_i, Ap_j) = 0 \quad (i \ne j,\ i \ne j + 1).

These relations complete the induction by which the paper proves Theorem 5:1, and they give the alternative formula (3:2b) for $b_i$ .

Formalization Note The statement is for all indices; after the method reaches the solution the residuals and directions are $0$ .

Preamble

import Mathlib
import Definitions.Def_ConjGrad_Termination_cgIter

open Matrix

Formal statement

namespace ConjGrad.Termination

/-- Theorem 5:1, eq. (5:3d) (Hestenes–Stiefel 1952, p. 414). For a symmetric positive
definite `A`, the cg-method (3:1) satisfies `(rᵢ, Apᵢ) = (pᵢ, Apᵢ)`, and `(rᵢ, Apⱼ) = 0`
whenever `i ≠ j` and `i ≠ j + 1`. -/
theorem cg_residual_Adirection {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ : Fin n → ℝ) :
    (∀ i, (cgIter A k x₀ i).r ⬝ᵥ (A *ᵥ (cgIter A k x₀ i).p) =
      (cgIter A k x₀ i).p ⬝ᵥ (A *ᵥ (cgIter A k x₀ i).p)) ∧
    (∀ i j, i ≠ j → i ≠ j + 1 → (cgIter A k x₀ i).r ⬝ᵥ (A *ᵥ (cgIter A k x₀ j).p) = 0) := by sorry

end ConjGrad.Termination

Source

Hestenes & Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6) (1952), https://doi.org/10.6028/jres.049.044, p. 414, Theorem 5:1, eq. (5:3d)

Read-back

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

Setting. Let $n \in \mathbb{N}$ and let $A$ be a real $n\times n$ matrix that is positive definite in this sense:

$A$ is symmetric, $A^\top = A$ ;
$\langle v, A v\rangle > 0$ for every nonzero $v \in \mathbb{R}^n$ .

Here $\langle u,v\rangle = \sum_l u_l v_l$ . Let $k, x_0 \in \mathbb{R}^n$ be arbitrary.

The iteration. Let $(x_i, r_i, p_i)_{i \in \mathbb{N}}$ be the sequence defined recursively as follows. Start with

r_0 = p_0 = k - A x_0 .

Then, for every $i \ge 0$ ,

a_i = \frac{\langle r_i, r_i\rangle}{\langle p_i, A p_i\rangle}, \quad x_{i+1} = x_i + a_i p_i, \quad r_{i+1} = r_i - a_i A p_i,

b_i = \frac{\langle r_{i+1}, r_{i+1}\rangle}{\langle r_i, r_i\rangle}, \quad p_{i+1} = r_{i+1} + b_i p_i .

Every quotient with a zero denominator is $0$ , and the recursion never stops.

Conclusion. The theorem asserts both of the following:

For every $i \in \mathbb{N}$ ,

\langle r_i, A p_i\rangle = \langle p_i, A p_i\rangle .

For all $i, j \in \mathbb{N}$ with $i \ne j$ and $i \ne j+1$ ,

\langle r_i, A p_j\rangle = 0 .

Part 2 excludes only two cases: $j = i$ , and $j = i - 1$ (the direction immediately before the residual). In particular it includes $j = i + 1$ , so it asserts $\langle r_i, A p_{i+1}\rangle = 0$ . It also includes every $j \ge i+2$ and every $j \le i-2$ .

Degenerate cases.

Unbounded indices. All natural-number indices are covered, including those beyond $n$ .
$n = 0$ . All dot products are $0$ and both parts hold trivially.
$k = A x_0$ . All $r_i$ and $p_i$ are $0$ , and every equation reads $0 = 0$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 5:1, eq. (5:3d) — (ri,Api)=(pi,Api)(r_i,Ap_i)=(p_i,Ap_i)(ri​,Api​)=(pi​,Api​) and (ri,Apj)=0(r_i,Ap_j)=0(ri​,Apj​)=0 for i≠j,j+1i\ne j, j+1i=j,j+1

Theorem 5:1, eq. (5:3d) — $(r_i,Ap_i)=(p_i,Ap_i)$ and $(r_i,Ap_j)=0$ for $i\ne j, j+1$