Theorem 5:3, eq. (5:6a) — $(p_i,p_j)=|r_j|^2|p_i|^2/|r_i|^2$ for $i\le j$

Proved

ConjGrad.ErrorDecrease.direction_inner_5_6a

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_0,r_1,\dots$ and $p_0,p_1,\dots$ be the residuals and direction vectors of the cg-method (5:1) started at $x_0$ . Then for all indices $i\le j$ ,

(p_i,p_j) = \frac{|r_j|^2\,|p_i|^2}{|r_i|^2}.

In particular $(p_i,p_j)\ge 0$ for all $i\le j$ : the direction vectors never make an obtuse angle with each other. In the proof of Theorem 6:3 this relation expresses the inner products $(p_l,p_{i-1})$ through the squared residuals.

Formalization Note The identity is stated for all $i\le j$ , without the restriction to steps before termination. After termination the recursion gives $r_j=p_j=0$ , and both sides are $0$ (the right side through Lean's convention $t/0=0$ when $r_i=0$ ).

Preamble

import Mathlib
import Definitions.Def_ConjGrad_ErrorDecrease_cgIter

open Matrix

Formal statement

namespace ConjGrad.ErrorDecrease

theorem direction_inner_5_6a {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (k x₀ : Fin n → ℝ) (i j : ℕ) (hij : i ≤ j) :
    (cgIter A k x₀ i).p ⬝ᵥ (cgIter A k x₀ j).p =
      ((cgIter A k x₀ j).r ⬝ᵥ (cgIter A k x₀ j).r) *
        ((cgIter A k x₀ i).p ⬝ᵥ (cgIter A k x₀ i).p) /
        ((cgIter A k x₀ i).r ⬝ᵥ (cgIter A k x₀ i).r) := 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. 415, Theorem 5:3, eq. (5:6a)

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 all $z\ne0$ .
$k, x_0\in\mathbb{R}^n$ are arbitrary. No solution vector $h$ is involved.
$i \le j$ are natural numbers.

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$ .

Conclusion. The statement asserts

p_i\cdot p_j \;=\; \frac{|r_j|^2\,|p_i|^2}{|r_i|^2},

where $|v|^2 = v\cdot v$ is the squared Euclidean norm.

Degenerate cases.

$r_i = 0$ : the right-hand side is $0$ by the division convention, so the claim becomes $p_i\cdot p_j = 0$ .
$i = j$ : the claim is $|p_i|^2 = |p_i|^2$ when $r_i\ne0$ . When $r_i = 0$ it asserts $|p_i|^2 = 0$ , i.e. $p_i = 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

Theorem 5:3, eq. (5:6a) — (pi,pj)=∣rj∣2∣pi∣2/∣ri∣2(p_i,p_j)=|r_j|^2|p_i|^2/|r_i|^2(pi​,pj​)=∣rj​∣2∣pi​∣2/∣ri​∣2 for i≤ji\le ji≤j

Theorem 5:3, eq. (5:6a) — $(p_i,p_j)=|r_j|^2|p_i|^2/|r_i|^2$ for $i\le j$