The characteristic polynomial recurrence for upper Hessenberg matrices

This file contains a recurrence formula for the characteristic polynomial of an upper Hessenberg matrix, in a noncomputable and a computable form, and a proof that the recurrence computes Matrix.charpoly.

The recurrence comes from equation 5.1 of Rehman-Ipsen. For an n × n upper Hessenberg matrix H it successively computes the characteristic polynomials pᵢ(X) = det (X * I - Hᵢ) of the leading principal submatrices Hᵢ of order i:

p_0 := 1

p_{k+1} = (X - C H[k][k]) p_k - ∑_{t<k} C (H[t][k] ∏_{j=t}^{k-1} H[j+1][j]) p_t

Main definitions

• hessP n H k: the polynomial pₖ of the recurrence, in R[X].
• hessCharpoly n H: the characteristic polynomial computed by the recurrence in R[X].
• coeffHessCharpoly n H: the characteristic polynomial computed by the recurrence on polynomials represented as lists of coefficients.

We have both hessCharpoly and coeffHessCharpoly so that for a literal matrix H we can produce the coefficients of the characteristic polynomial by computing coeffHessCharpoly using the kernel. The theorem ofCoeffList_coeffHessCharpoly interprets the result as hessCharpoly, a polynomial in R[X].

Main results

• ofCoeffList_coeffHessCharpoly: the recurrence on coefficient lists computes hessCharpoly n H.
• charpoly_eq_hessCharpoly: hessCharpoly computes the characteristic polynomial of an upper Hessenberg matrix.

Implementation details

The derivation of the recurrence formula for an n x n upper Hessenberg matrix H follows by Laplace expansion of the determinant of the characteristic matrix, CH, for H along its last column.

The minor Hᵢ of CH that omits the last column and the ith row of H has the following structure:

  columns 0 ... i-1 of H       columns i ... n-2 of H
[             Mᵢ           |              *            ]   rows 0 ... i-1 of H
[             0            |              Tᵢ           ]   rows i+1 ... n-1 of H

where Mᵢ is the leading principal i × i minor of CH (and so is upper Hessenberg) and Tᵢ is a n-1-i × n-1-i upper triangular matrix. Therefore

det Hᵢ = det Mᵢ · CH[i+1][i] · CH[i+2][i+1] · ... · CH[n-1][n-2]

and expanding det CH along its last column gives:

det CH = ∑_{i=0}^{n-1} (-1)^(i+n-1) CH[i][n-1] det Hᵢ

Now let pₖ be the characteristic polynomial of Hₖ, it is equal to det CHₖ where CHₖ is the leading principal k × k minor of CH. In particular pₙ = det CH is the characteristic polynomial of H.

By definition, we know that CH[n-1][n-1] = X - H[n-1][n-1] and H_{n-1} = CH_{n-1} and so we can rewrite det CH as:

pₙ = (X - H[n-1][n-1]) p_{n-1} + ∑_{i=0}^{n-2} (-1)^(i+n-1) CH[i][n-1] det Hᵢ

Now consider each term in the tail sum. We can expand Hᵢ into its block form, note that CH[i][n-1] = -H[i][n-1], and collect negative factors to obtain:

(-1)^(i+n-1) CH[i][n-1] det Hᵢ = -H[i][n-1] · pᵢ · ∏_{j=i}^{n-2} H[j+1][j]

The leading principal submatrices Hᵢ are also upper Hessenberg, so the same expansion applies to p₀, ..., p_{n-1}, which gives the recurrence formula above.

In the formalization:

• Matrix.leadingBlock defines the leading principal submatrix.
• IsUpperHessenberg.charmatrix and charmatrix_leadingBlock show that CH is upper Hessenberg with Mₖ the characteristic matrix of Hₖ.
• det_lastColMinor is the formula for det Hᵢ.
• det_eq_sum_of_isUpperHessenberg is the expansion of det CH along its last column.
• charpoly_isUpperHessenberg specializes the determinant expansion to CH.
• hessP_eq_charpoly is the proof of the recurrence formula.

References

• Rizwana Rehman, Ilse C. F. Ipsen, La Budde's method for computing characteristic polynomials

@[irreducible]

noncomputable def Mathlib.Tactic.Hessenberg.hessP {R : Type u_1} [CommRing R] (n : ℕ) (H : Array R) : ℕ → Polynomial R

The characteristic polynomial of the leading k × k block of the n × n Hessenberg matrix represented by an array of entries in row-major ordering.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Hessenberg.hessP n H 0 = 1

@[reducible, inline]

noncomputable abbrev Mathlib.Tactic.Hessenberg.hessCharpoly {R : Type u_1} [CommRing R] (n : ℕ) (H : Array R) : Polynomial R

The characteristic polynomial of an n × n Hessenberg matrix represented by an array of entries in row-major ordering.

Equations

• Mathlib.Tactic.Hessenberg.hessCharpoly n H = Mathlib.Tactic.Hessenberg.hessP n H n

theorem Mathlib.Tactic.Hessenberg.hessP_zero {R : Type u_1} [CommRing R] {n : ℕ} {H : Array R} : hessP n H 0 = 1

theorem Mathlib.Tactic.Hessenberg.hessP_succ {R : Type u_1} [CommRing R] {n : ℕ} {H : Array R} (k : ℕ) : hessP n H (k + 1) = (Polynomial.X - Polynomial.C (H.getD (n * k + k) 0)) * hessP n H k - ∑ t : Fin k, Polynomial.C (H.getD (n * ↑t + k) 0 * ∏ j ∈ Finset.Ico (↑t) k, H.getD (n * (j + 1) + j) 0) * hessP n H ↑t

theorem Mathlib.Tactic.Hessenberg.hessCharpoly_eq {R : Type u_1} [CommRing R] {n : ℕ} {H : Array R} : hessCharpoly n H = hessP n H n

The recurrence on coefficient lists

This section defines the recurrence on a polynomial representation (lists of coefficients) that the kernel can compute.

def Mathlib.Tactic.Hessenberg.coeffHessSum {R : Type u_1} [CommRing R] (n : ℕ) (H : Array R) (k i : ℕ) (r : R) (ps : Array (List R)) : List R

Compute the coefficients of ∑_{t ≤ i} H[t][k] · r · (∏_{j=t}^{i-1} H[j+1][j]) · p_t by recursion on i, where p_t is the polynomial defined in the coefficient list ps[t]. r accumulates the product of H[i+1][i] entries at each step.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Hessenberg.coeffHessSum n H k 0 x✝¹ x✝ = List.map (fun (x : R) => H.getD (n * 0 + k) 0 * x✝¹ * x) (x✝.getD 0 [])

def Mathlib.Tactic.Hessenberg.coeffHessStep {R : Type u_1} [CommRing R] (n : ℕ) (H : Array R) (k : ℕ) (ps : Array (List R)) : List R

Compute the coefficients of pₖ from the coefficient lists of p₀, ..., p_{k-1}. The coefficients of each polynomial are stored as a List R in ps.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Hessenberg.coeffHessStep n H 0 ps = [1]

def Mathlib.Tactic.Hessenberg.coeffHessCharpoly {R : Type u_1} [CommRing R] (n : ℕ) (H : Array R) : List R

Compute the coefficients of hessCharpoly n H.

Equations

• Mathlib.Tactic.Hessenberg.coeffHessCharpoly n H = ((fun (ps : Array (List R)) => ps.push (Mathlib.Tactic.Hessenberg.coeffHessStep n H ps.size ps))^[n] #[[1]]).getD n []

theorem Mathlib.Tactic.Hessenberg.ofCoeffList_coeffHessSum {R : Type u_1} [CommRing R] {n : ℕ} {H : Array R} (k i : ℕ) (r : R) (ps : Array (List R)) : Polynomial.ofCoeffList (coeffHessSum n H k i r ps) = ∑ t : Fin (i + 1), Polynomial.C (H.getD (n * ↑t + k) 0 * (r * ∏ j ∈ Finset.Ico (↑t) i, H.getD (n * (j + 1) + j) 0)) * Polynomial.ofCoeffList (ps.getD ↑t [])

theorem Mathlib.Tactic.Hessenberg.ofCoeffList_coeffHessStep {R : Type u_1} [CommRing R] {n : ℕ} {H : Array R} (k : ℕ) (ps : Array (List R)) : Polynomial.ofCoeffList (coeffHessStep n H (k + 1) ps) = (Polynomial.X - Polynomial.C (H.getD (n * k + k) 0)) * Polynomial.ofCoeffList (ps.getD k []) - ∑ t : Fin k, Polynomial.C (H.getD (n * ↑t + k) 0 * ∏ j ∈ Finset.Ico (↑t) k, H.getD (n * (j + 1) + j) 0) * Polynomial.ofCoeffList (ps.getD ↑t [])

@[simp]

theorem Mathlib.Tactic.Hessenberg.ofCoeffList_coeffHessCharpoly {R : Type u_1} [CommRing R] {n : ℕ} {H : Array R} : Polynomial.ofCoeffList (coeffHessCharpoly n H) = hessCharpoly n H

Correctness of the recurrence

The last-column expansion of the determinant of an upper Hessenberg matrix

The recurrence computes the characteristic polynomial

theorem Mathlib.Tactic.Hessenberg.charpoly_eq_hessCharpoly {R : Type u_1} [CommRing R] {n : ℕ} (H : Matrix (Fin n) (Fin n) R) (hH : H.IsUpperHessenberg) : H.charpoly = hessCharpoly n H.toArray

The characteristic polynomial of an upper Hessenberg matrix is computed by the leading-principal-block recurrence on the row-major array of its entries.