One step of the A-conjugacy of PCG search directions: $d_{k+1}^T A d_k = 0$

Disproved

LimitedBFGS.SQN.pcg_direction_A_conjugacy_step

by WillR · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

conjugate-gradientnumerical-linear-algebrapreconditioningquasi-newton

Let $f(x) = \tfrac12 x^TAx + b^Tx$ on $\mathbb{R}^n$ with $A$ symmetric positive definite, and run the preconditioned conjugate gradient method with fixed preconditioner $H_0$ and exact line searches from $x_0$ , so that with $g_k = Ax_k + b$ and $y_k = g_{k+1} - g_k$ the directions obey

d_{k+1} = -H_0 g_{k+1} + \beta_k\, d_k, \qquad \beta_k = \frac{y_k^T H_0 g_{k+1}}{y_k^T d_k}.

Then two successive search directions are $A$ -conjugate:

d_{k+1}^T A\, d_k = 0 \qquad \text{for every } k \ge 0.

Why it is true. The gradient of a quadratic is affine, so along the line $x + a\,d$ the gradient changes by $a\,Ad$ . Since $y_k = g_{k+1} - g_k$ is exactly the change produced by the step $a_k = \mathrm{exactStep}$ , one has $y_k = a_k\,A d_k$ , and therefore

\beta_k = \frac{(A d_k)^T (H_0 g_{k+1})}{(A d_k)^T d_k},

the factor $a_k$ cancelling. Substituting the direction recurrence and using that $u^TAv = v^TAu$ for symmetric $A$ ,

d_{k+1}^T A d_k = -(H_0 g_{k+1})^T (A d_k) + \beta_k \, (d_k^T A d_k) = -\,\frac{(A d_k)^T (H_0 g_{k+1})}{(A d_k)^T d_k}\,(A d_k)^T d_k + (A d_k)^T (H_0 g_{k+1}) = 0,

because the two parenthesised scalars are the same two numbers written in the two orders allowed by self-adjointness.

Formalization note. No case split is needed. When $y_k^T d_k = 0$ Lean's convention $x/0 = 0$ makes $\beta_k = 0$ , and then $y_k = a_k A d_k$ with the same vanishing denominator gives $(A d_k)^T(H_0 g_{k+1}) = 0$ as well, so both summands are $0$ and the identity still holds. The hypothesis is exactly that $A$ is symmetric (positive definiteness is not needed for this step, and is carried only because it is the standing hypothesis of the iteration). This is a statement about one index only, so unlike the full conjugacy it is a direct algebraic consequence of the definition of $\beta$ and requires no induction.

Preamble

import Mathlib
import Definitions.Def_LimitedBFGS_SQN_pcgIter

open Matrix

Formal statement

namespace LimitedBFGS.SQN

/-- One step of the `A`-conjugacy of the search directions generated by the
preconditioned conjugate gradient iteration (13) of Nocedal 1980, p. 777.

Write `st_k = pcgIter A b H0 x0 k` and `st_{k+1} = pcgIter A b H0 x0 (k + 1)`.
The direction recurrence is `d_{k+1} = -H0 g_{k+1} + beta_k d_k` with
`beta_k = y_kᵀ H0 g_{k+1} / y_kᵀ d_k` and `y_k = g_{k+1} - g_k`. Then

    d_{k+1}ᵀ A d_k = 0.

This is exactly the property `beta` exists to enforce: since the gradient is
affine, `y_k = a_k (A d_k)` for the line-search step `a_k = exactStep A b
st_k.x st_k.d`, so

    beta_k = [(A d_k)ᵀ (H0 g_{k+1})] / [(A d_k)ᵀ d_k],

and in `d_{k+1}ᵀ (A d_k) = -(H0 g_{k+1})ᵀ (A d_k) + beta_k (d_kᵀ A d_k)` the two
summands are the same two scalars exchanged, because the bilinear form
`uᵀ A v` is self-adjoint when `A` is symmetric. The identity is therefore
structural rather than inductive: it needs no hypothesis about any earlier
index, and it holds in the degenerate case `y_kᵀ d_k = 0`, where Lean's `x/0 = 0`
makes both summands vanish.

This is the base case of the `A`-conjugacy of the directions, and it is the
step from which the orthogonality relations `g_iᵀ H0 g_j = 0` and
`g_iᵀ d_j = 0` of eq. (15)-(16), p. 777, are obtained. -/
theorem pcg_direction_A_conjugacy_step {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef)
    (b : Fin n → ℝ) (H₀ : Matrix (Fin n) (Fin n) ℝ) (x₀ : Fin n → ℝ) (k : ℕ) :
    (pcgIter A b H₀ x₀ (k + 1)).d ⬝ᵥ (A *ᵥ (pcgIter A b H₀ x₀ k).d) = 0 := by sorry

end LimitedBFGS.SQN

Source

Nocedal, Updating Quasi-Newton Matrices with Limited Storage, Math. Comp. 35 (1980), p. 777, iteration (13) and the A-conjugacy of the search directions underlying eqs. (15)-(16)

View graph

One step of the A-conjugacy of PCG search directions: dk+1TAdk=0d_{k+1}^T A d_k = 0dk+1T​Adk​=0

One step of the A-conjugacy of PCG search directions: $d_{k+1}^T A d_k = 0$