Theorem 5:5, eq. (5:10) — $a_i=|r_i|^2/(p_i,Ap_i)=(p_i,r_i)/(p_i,Ap_i)=(p_i,r_0)/(p_i,Ap_i)$

Proved

ConjGrad.Termination.cg_stepLength_formulas

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 $x_i$ , $r_i$ , $p_i$ be produced by the conjugate gradient method (3:1) started at $x_0$ , with step lengths $a_i = |r_i|^2/(p_i, Ap_i)$ as in (3:1b). Then for every $i$

a_i = \frac{|r_i|^2}{(p_i, Ap_i)} = \frac{(p_i, r_i)}{(p_i, Ap_i)} = \frac{(p_i, r_0)}{(p_i, Ap_i)}.

The middle expression is the step length (4:1a) of the method of conjugate directions, so this identity is one half of the statement that the cg-method is a cd-method; the last expression is (4:4).

Formalization Note The first equality is the definition of $a_i$ (cgA); the statement asserts the other two. It covers only formula (5:10) of Theorem 5:5; the formulas (5:11) for $b_i$ and the Rayleigh quotient bounds (5:12) are not part of it. After the method reaches the solution both sides are $0$ .

Preamble

import Mathlib
import Definitions.Def_ConjGrad_Termination_cgIter

open Matrix

Formal statement

namespace ConjGrad.Termination

/-- Theorem 5:5, eq. (5:10) (Hestenes–Stiefel 1952, p. 416). For a symmetric positive
definite `A`, the step length `aᵢ = |rᵢ|²/(pᵢ, Apᵢ)` of the cg-method (3:1b) also equals
`(pᵢ, rᵢ)/(pᵢ, Apᵢ)` and `(pᵢ, r₀)/(pᵢ, Apᵢ)`. -/
theorem cg_stepLength_formulas {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ : Fin n → ℝ) (i : ℕ) :
    cgA A (cgIter A k x₀ i) =
        ((cgIter A k x₀ i).p ⬝ᵥ (cgIter A k x₀ i).r) /
          ((cgIter A k x₀ i).p ⬝ᵥ (A *ᵥ (cgIter A k x₀ i).p)) ∧
      cgA A (cgIter A k x₀ i) =
        ((cgIter A k x₀ i).p ⬝ᵥ (cgIter A k x₀ 0).r) /
          ((cgIter A k x₀ i).p ⬝ᵥ (A *ᵥ (cgIter A k x₀ i).p)) := 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. 416, Theorem 5:5, eq. (5:10)

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 and fix an index $i \in \mathbb{N}$ .

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. For the fixed $i$ , the step length $a_i$ satisfies both

a_i = \frac{\langle p_i, r_i\rangle}{\langle p_i, A p_i\rangle} \qquad\text{and}\qquad a_i = \frac{\langle p_i, r_0\rangle}{\langle p_i, A p_i\rangle},

with all quotients read as $0$ when their denominator is $0$ .

Degenerate cases.

$\langle p_i, A p_i\rangle = 0$ . By positive definiteness this happens exactly when $p_i = 0$ . Then all three expressions are $0$ by the division convention, so the statement holds trivially at that index.
Arbitrary $i$ . The index is any natural number, including values beyond $n$ .
$n = 0$ . Everything is $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:5, eq. (5:10) — ai=∣ri∣2/(pi,Api)=(pi,ri)/(pi,Api)=(pi,r0)/(pi,Api)a_i=|r_i|^2/(p_i,Ap_i)=(p_i,r_i)/(p_i,Ap_i)=(p_i,r_0)/(p_i,Ap_i)ai​=∣ri​∣2/(pi​,Api​)=(pi​,ri​)/(pi​,Api​)=(pi​,r0​)/(pi​,Api​)

Theorem 5:5, eq. (5:10) — $a_i=|r_i|^2/(p_i,Ap_i)=(p_i,r_i)/(p_i,Ap_i)=(p_i,r_0)/(p_i,Ap_i)$