Reduction of a matrix over ℚ to Hessenberg form

reduce computes, for a square matrix A over ℚ, a sequence of row and column swaps, a unit lower triangular matrix L and an upper Hessenberg matrix H such that Aσ * L = L * H, where Aσ := A.submatrix σ σ is A with its rows and columns permuted by the swaps.

Implementation notes

reduce follows steps 1 to 4 of Cohen, Algorithm 2.2.9.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, Algorithm 2.2.9

structure Mathlib.Tactic.Hessenberg.Reduction : Type

A similarity Aσ * L = L * H of a rational matrix A to upper Hessenberg form, where Aσ := A.submatrix σ σ for the arrangement σ of the interchanges.

• swaps : Array (ℕ × ℕ)

  The row and column interchanges, in order. The permutation σ is their product.

• L : Array (Array ℚ)

  The unit lower triangular transform.

• H : Array (Array ℚ)

  The upper Hessenberg form.

def Mathlib.Tactic.Hessenberg.Reduction.perm (d : Reduction) : Array ℕ

The row and column swaps of a Reduction represented as an indexed array. An entry e at index i means that row and column e of the original matrix move to position i.

Equations

• d.perm = Array.foldl (fun (ord : Array ℕ) (x : ℕ × ℕ) => match x with | (a, b) => ord.swapIfInBounds a b) (Array.range d.L.size) d.swaps

def Mathlib.Tactic.Hessenberg.reduce (n : ℕ) (A : Array (Array ℚ)) : Reduction

Reduce the n × n matrix A over ℚ, given as an array of rows, to upper Hessenberg form by Gaussian elimination with row and column swaps.

Equations

• One or more equations did not get rendered due to their size.