Conjugate gradient method

DefinitionEnergy norm induced by a matrix#✓fully proved

The energy norm ‖v‖_A = √(vᵀ A v); a norm when A is positive definite.

noncomputable def energyNorm {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (v : Fin n → ℝ) : ℝ :=
  √(v ⬝ᵥ (A *ᵥ v))

Used by 4

Used byCG minimizes the energy norm of the error over the Krylov space · The conjugate gradient error bound · The conjugate gradient error bound in terms of the condition number · The Chebyshev bound for Krylov energy minimizers

DefinitionKrylov subspace#✓fully proved

The Krylov space 𝒦_k(A, r) = span {r, A r, …, A^{k-1} r}.

noncomputable def krylov {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (r : Fin n → ℝ) (k : ℕ) :
    Submodule ℝ (Fin n → ℝ) :=
  Submodule.span ℝ (Set.range fun i : Fin k => (A ^ (i : ℕ)) *ᵥ r)

Used by 4

Used byCG minimizes the energy norm of the error over the Krylov space · The conjugate gradient error bound · The Chebyshev bound for Krylov energy minimizers · CG stays in the Krylov space

StructureState of the conjugate gradient method#✓fully proved

The state of the conjugate gradient method: iterate x, residual r = b - A x and search direction d.

structure State (n : ℕ) where
  /-- The current iterate. -/
  x : Fin n → ℝ
  /-- The current residual `b - A x`. -/
  r : Fin n → ℝ
  /-- The current search direction. -/
  d : Fin n → ℝ

Used by 7

Used byCG minimizes the energy norm of the error over the Krylov space · The conjugate gradient error bound · The conjugate gradient error bound in terms of the condition number · Initial conjugate gradient state · Conjugate gradient state after \(k\) steps · CG stays in the Krylov space · One Hestenes–Stiefel conjugate gradient step

DefinitionOne Hestenes–Stiefel conjugate gradient step#✓fully proved

One Hestenes–Stiefel conjugate gradient step.

noncomputable def step {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (s : State n) : State n :=
  let α := (s.r ⬝ᵥ s.r) / (s.d ⬝ᵥ (A *ᵥ s.d))
  let r' := s.r - α • (A *ᵥ s.d)
  { x := s.x + α • s.d
    r := r'
    d := r' + ((r' ⬝ᵥ r') / (s.r ⬝ᵥ s.r)) • s.d }

Uses 1 · Used by 3

Statement usesState of the conjugate gradient method

Used byCG minimizes the energy norm of the error over the Krylov space · Conjugate gradient state after \(k\) steps · CG stays in the Krylov space

DefinitionInitial conjugate gradient state#✓fully proved

The initial state x₀, r₀ = d₀ = b - A x₀.

def init {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (b x₀ : Fin n → ℝ) : State n :=
  ⟨x₀, b - A *ᵥ x₀, b - A *ᵥ x₀⟩

Uses 1 · Used by 3

Statement usesState of the conjugate gradient method

Used byCG minimizes the energy norm of the error over the Krylov space · Conjugate gradient state after \(k\) steps · CG stays in the Krylov space

DefinitionConjugate gradient state after \(k\) steps#✓fully proved

The k-th conjugate gradient state from x₀ for the system A x = b.

noncomputable def iterate {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (b x₀ : Fin n → ℝ) (k : ℕ) :
    State n :=
  (step A)^[k] (init A b x₀)

Uses 3 · Used by 4

Statement usesState of the conjugate gradient method · Initial conjugate gradient state · One Hestenes–Stiefel conjugate gradient step

Used byCG minimizes the energy norm of the error over the Krylov space · The conjugate gradient error bound · The conjugate gradient error bound in terms of the condition number · CG stays in the Krylov space

12 fully proved

Krylov spaces

TheoremCG stays in the Krylov space#✓fully proved

x_k - x₀ ∈ 𝒦_k(A, r₀).

theorem iterate_x_sub_mem_krylov {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)
    (b x₀ : Fin n → ℝ) (k : ℕ) :
    (iterate A b x₀ k).x - x₀ ∈ krylov A (b - A *ᵥ x₀) k

Uses 5

Statement usesState of the conjugate gradient method · Conjugate gradient state after \(k\) steps · Krylov subspace

Proof usesInitial conjugate gradient state · One Hestenes–Stiefel conjugate gradient step

TheoremCG minimizes the energy norm of the error over the Krylov space#✓fully proved

For the solution x⋆ of A x⋆ = b, ‖x_k - x⋆‖_A ≤ ‖x₀ + z - x⋆‖_A for every z ∈ 𝒦_k(A, r₀).

theorem energyNorm_iterate_le {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosDef) {b xs : Fin n → ℝ} (hxs : A *ᵥ xs = b)
    (x₀ : Fin n → ℝ) (k : ℕ) {z : Fin n → ℝ} (hz : z ∈ krylov A (b - A *ᵥ x₀) k) :
    energyNorm A ((iterate A b x₀ k).x - xs) ≤ energyNorm A (x₀ + z - xs)

Uses 6 · Used by 1

Statement usesState of the conjugate gradient method · Energy norm induced by a matrix · Conjugate gradient state after \(k\) steps · Krylov subspace

Proof usesInitial conjugate gradient state · One Hestenes–Stiefel conjugate gradient step

Used byThe conjugate gradient error bound

The Chebyshev bound

TheoremThe Chebyshev bound for Krylov energy minimizers#✓fully proved

If the eigenvalues of A lie in [a, c] with 0 < a, and x minimizes ‖· - x⋆‖_A over x₀ + 𝒦_k(A, A (x⋆ - x₀)), then ‖x - x⋆‖_A ≤ 2 ((√κ - 1) / (√κ + 1))^k ‖x₀ - x⋆‖_A with κ = c / a.

theorem energyNorm_le_of_isMin_krylov {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosDef) {a c : ℝ} (ha : 0 < a)
    (hlow : ∀ i, a ≤ hA.isHermitian.eigenvalues i) (hup : ∀ i, hA.isHermitian.eigenvalues i ≤ c)
    {xs x₀ x : Fin n → ℝ} (k : ℕ)
    (hmin : ∀ z ∈ krylov A (A *ᵥ (xs - x₀)) k, energyNorm A (x - xs) ≤ energyNorm A (x₀ + z - xs)) :
    energyNorm A (x - xs) ≤
      2 * ((√(c / a) - 1) / (√(c / a) + 1)) ^ k * energyNorm A (x₀ - xs)

Uses 2 · Used by 1

Statement usesEnergy norm induced by a matrix · Krylov subspace

Used byThe conjugate gradient error bound

TheoremThe conjugate gradient error bound#✓fully proved

If the eigenvalues of A lie in [a, c] with 0 < a and A x⋆ = b, the CG iterates satisfy ‖x_k - x⋆‖_A ≤ 2 ((√κ - 1) / (√κ + 1))^k ‖x₀ - x⋆‖_A with κ = c / a.

theorem energyNorm_iterate_sub_le {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosDef) {a c : ℝ} (ha : 0 < a)
    (hlow : ∀ i, a ≤ hA.isHermitian.eigenvalues i) (hup : ∀ i, hA.isHermitian.eigenvalues i ≤ c)
    {b xs : Fin n → ℝ} (hxs : A *ᵥ xs = b) (x₀ : Fin n → ℝ) (k : ℕ) :
    energyNorm A ((iterate A b x₀ k).x - xs) ≤
      2 * ((√(c / a) - 1) / (√(c / a) + 1)) ^ k * energyNorm A (x₀ - xs)

Uses 6 · Used by 1

Statement usesState of the conjugate gradient method · Energy norm induced by a matrix · Conjugate gradient state after \(k\) steps

Proof usesCG minimizes the energy norm of the error over the Krylov space · The Chebyshev bound for Krylov energy minimizers · Krylov subspace

Used byThe conjugate gradient error bound in terms of the condition number

DefinitionSpectral condition number of a positive definite matrix#✓fully proved

The spectral condition number λ_max / λ_min of a positive definite matrix. For n = 0 it is 0 / 0 = 0 (no eigenvalues), a junk value; the bound below is stated for 0 < n.

noncomputable def condNum {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosDef) : ℝ :=
  (⨆ i, hA.isHermitian.eigenvalues i) / ⨅ i, hA.isHermitian.eigenvalues i

Used by 1

Used byThe conjugate gradient error bound in terms of the condition number

TheoremThe conjugate gradient error bound in terms of the condition number#✓fully proved

The conjugate gradient error bound in terms of the condition number κ of A: ‖x_k - x⋆‖_A ≤ 2 ((√κ - 1) / (√κ + 1))^k ‖x₀ - x⋆‖_A.

theorem energyNorm_iterate_sub_le_condNum {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hn : 0 < n)
    (hA : A.PosDef) {b xs : Fin n → ℝ}
    (hxs : A *ᵥ xs = b) (x₀ : Fin n → ℝ) (k : ℕ) :
    energyNorm A ((iterate A b x₀ k).x - xs) ≤
      2 * ((√(condNum hA) - 1) / (√(condNum hA) + 1)) ^ k * energyNorm A (x₀ - xs)

Uses 5

Statement usesState of the conjugate gradient method · Spectral condition number of a positive definite matrix · Energy norm induced by a matrix · Conjugate gradient state after \(k\) steps

Proof usesThe conjugate gradient error bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.