Section 6, eq. (6:6) — $(y_{i+1},x_{i+1}-x_i)=f(x_{i+1})/\mu(p_i)$

Proved

ConjGrad.ErrorDecrease.error_vector_inner_6_6

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 $h$ solve $Ah=k$ . Let $x_i$ and $p_i$ be the estimates and direction vectors of the cg-method (5:1) started at $x_0$ , write $y_i=h-x_i$ for the error vector of $x_i$ , let $f(x)=(h-x,A(h-x))$ be the error function (4:5), and let $\mu(z)=(z,Az)/|z|^2$ be the Rayleigh quotient (4:12). Then for every $i\ge 0$ ,

(y_{i+1},\,x_{i+1}-x_i) = \frac{f(x_{i+1})}{\mu(p_i)} .

This is the identity (6:6), displayed in the paper's proof of Theorem 6:3 (with the index shifted by one): the step $x_{i+1}-x_i$ and the new error vector $y_{i+1}$ make a nonnegative inner product, whose value is determined by the error function. It is the ingredient that turns the decrease of $f$ into a decrease of the Euclidean length of the error vector.

Formalization Note The statement is for all $i$ , including steps after termination; there $x_{i+1}=x_i=h$ and both sides are $0$ . The index is shifted (step $i+1$ goes from $x_i$ to $x_{i+1}$ ) to avoid natural-number subtraction.

Preamble

import Mathlib
import Definitions.Def_ConjGrad_ErrorDecrease_cgIter
import Definitions.Def_ConjGrad_ErrorDecrease_errorFun
import Definitions.Def_ConjGrad_ErrorDecrease_rayleigh

open Matrix

Formal statement

namespace ConjGrad.ErrorDecrease

theorem error_vector_inner_6_6 {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ h : Fin n → ℝ) (hh : A *ᵥ h = k) (i : ℕ) :
    (h - (cgIter A k x₀ (i + 1)).x) ⬝ᵥ ((cgIter A k x₀ (i + 1)).x - (cgIter A k x₀ i).x) =
      errorFun A h (cgIter A k x₀ (i + 1)).x / rayleigh A (cgIter A k x₀ i).p := by sorry

end ConjGrad.ErrorDecrease

Source

Hestenes & Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6) (1952), p. 417, Section 6, eq. (6:6) (in the proof of Theorem 6:3)

Read-back

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

Setting and hypotheses.

$n$ is a natural number.
$A$ is a positive definite real $n\times n$ matrix: symmetric, with $z\cdot Az>0$ for $z\ne0$ .
$k, x_0\in\mathbb{R}^n$ are arbitrary.
$h$ satisfies $Ah=k$ .
$i\in\mathbb{N}$ is arbitrary.

The sequence. $(x_i, r_i, p_i)$ is generated from $A$ , $k$ and $x_0$ as follows:

Start with $r_0=p_0=k-Ax_0$ .
Set $a_i=(r_i\cdot r_i)/(p_i\cdot Ap_i)$ , then $x_{i+1}=x_i+a_ip_i$ and $r_{i+1}=r_i-a_iAp_i$ .
Set $b_i=(r_{i+1}\cdot r_{i+1})/(r_i\cdot r_i)$ and $p_{i+1}=r_{i+1}+b_ip_i$ .
Division by zero yields $0$ .

Functions used.

The error function is $f(x)=(h-x)\cdot A(h-x)$ .
The Rayleigh quotient is $\mu(z)=(z\cdot Az)/(z\cdot z)$ , with $\mu(0)=0$ .

Conclusion. The statement asserts

(h - x_{i+1})\cdot(x_{i+1} - x_i) \;=\; \frac{f(x_{i+1})}{\mu(p_i)} .

The left side uses the plain Euclidean dot product, not the one weighted by $A$ .

Degenerate cases.

$\mu(p_i) = 0$ : under positive definiteness this happens exactly when $p_i=0$ . The right-hand side is then $0$ by the division convention, and $a_i = 0$ gives $x_{i+1}=x_i$ , so the left-hand side is also $0$ .
$n=0$ : both sides are $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

Section 6, eq. (6:6) — (yi+1,xi+1−xi)=f(xi+1)/μ(pi)(y_{i+1},x_{i+1}-x_i)=f(x_{i+1})/\mu(p_i)(yi+1​,xi+1​−xi​)=f(xi+1​)/μ(pi​)

Section 6, eq. (6:6) — $(y_{i+1},x_{i+1}-x_i)=f(x_{i+1})/\mu(p_i)$