Prove2Me

pt′gk+1=0p_t'g_{k+1} = 0 under exact searches and conjugacy

Proved
ShannoCG.SCONB.restart_step_orth_grad

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

conjugate-gradientp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1quadratic-programming

Let AA be a real n×nn\times n matrix, c∈Rnc \in \mathbb R^n, and gradients gi=Axi+cg_i = Ax_i + c along iterates with xi+1=xi+pix_{i+1} = x_i + p_i for t≤i≤kt \le i \le k, where t<kt < k. Assume

  1. the restart search is exact: pt′gt+1=0p_t' g_{t+1} = 0;
  2. the restart step is conjugate to the later steps: pt′Api=0p_t' A p_i = 0 for i=t+1,…,ki = t+1, \dots, k.

Then

pt′gk+1=0.p_t' g_{k+1} = 0.

This is the fact, stated in Shanno's proof, that with exact searches on a quadratic the restart step is orthogonal to every later gradient of the cycle; it is what makes the restart matrix act on gk+1g_{k+1} in the simple form (42).

Formalization Note The conjugacy of the restart step with the later steps is a hypothesis, as in the paper, which takes it as known for exact searches on a quadratic; it is not derived from a run of the algorithm. No positive definiteness is needed.

Preamble
import Mathlib

open Matrix
Formal statement
namespace ShannoCG.SCONB

/-- Shanno, *Conjugate Gradient Methods with Inexact Searches*, Math. Oper. Res. 3(3) (1978), §IV, p. 251 (PDF 8), the sentence before (41), the display after (41) and the sentence
after it: with exact searches on a quadratic, `p_t' g_{k+1} = 0`. The paper's argument uses
`p_t' g_{t+1} = 0` (exact search at the restart step) and the conjugacy
`p_t' A p_i = 0`, `i = t+1, …, k`.

**Formalization Note.** Gradient `g i = A *ᵥ x i + c` (arbitrary `c`), steps `x_{i+1} = x_i + p_i`
for `t ≤ i ≤ k`. The exact search at `t` and the conjugacy are the hypotheses `hexact_t` and
`hconj` (the paper states them as known facts for exact searches on a quadratic; they are not
derived here). No positive definiteness is needed. -/
theorem restart_step_orth_grad {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (c : Fin n → ℝ)
    (x p g : ℕ → Fin n → ℝ) (t k : ℕ) (htk : t < k)
    (hg : ∀ i, g i = A *ᵥ x i + c)
    (hstep : ∀ i, t ≤ i → i ≤ k → x (i + 1) = x i + p i)
    (hexact_t : p t ⬝ᵥ g (t + 1) = 0)
    (hconj : ∀ i, t < i → i ≤ k → p t ⬝ᵥ (A *ᵥ p i) = 0) :
    p t ⬝ᵥ g (k + 1) = 0 := by sorry

end ShannoCG.SCONB
Source
Shanno, Conjugate Gradient Methods with Inexact Searches, Math. Oper. Res. 3(3) (1978) 244–256, DOI 10.1287/moor.3.3.244, p. 251 (PDF p. 8), §IV, the sentence before eq. (41), the display after it and the sentence after that
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph