Upper Hessenberg matrices

A square matrix is upper Hessenberg when all entries below the subdiagonal are zero.

This file defines the predicate Matrix.IsUpperHessenberg with a corresponding Decidable instance.

Main definitions

• Matrix.IsUpperHessenberg with Matrix.isUpperHessenberg_iff to unfold it

Main results

• Matrix.isUpperHessenberg_fin_iff: the IsUpperHessenberg predicate on Fin n
• Matrix.IsUpperTriangular.isUpperHessenberg: upper triangular matrices are upper Hessenberg.

def Matrix.IsUpperHessenberg {R : Type u_1} {m : Type u_2} [Zero R] [Preorder m] [SuccOrder m] (M : Matrix m m R) : Prop

M is upper Hessenberg: entries strictly below the subdiagonal vanish.

Equations

• M.IsUpperHessenberg = ∀ ⦃i j : m⦄, Order.succ j < i → M i j = 0

theorem Matrix.isUpperHessenberg_iff {R : Type u_1} {m : Type u_2} [Zero R] [Preorder m] [SuccOrder m] {M : Matrix m m R} : M.IsUpperHessenberg ↔ ∀ ⦃i j : m⦄, Order.succ j < i → M i j = 0

@[instance_reducible]

instance Matrix.instDecidableIsUpperHessenbergOfDecidableEqOfFintypeOfDecidableLT {R : Type u_1} {m : Type u_2} [Zero R] [Preorder m] [SuccOrder m] [DecidableEq R] [Fintype m] [DecidableLT m] (M : Matrix m m R) : Decidable M.IsUpperHessenberg

Equations

• M.instDecidableIsUpperHessenbergOfDecidableEqOfFintypeOfDecidableLT = decidable_of_iff (∀ (ij : m × m), Order.succ ij.2 < ij.1 → M ij.1 ij.2 = 0) ⋯

theorem Matrix.IsUpperTriangular.isUpperHessenberg {R : Type u_1} {m : Type u_2} [Zero R] [Preorder m] [SuccOrder m] {M : Matrix m m R} (h : M.IsUpperTriangular) : M.IsUpperHessenberg

theorem Matrix.isUpperHessenberg_fin_iff {R : Type u_1} [Zero R] {n : ℕ} {M : Matrix (Fin n) (Fin n) R} : M.IsUpperHessenberg ↔ ∀ (i j : Fin n), ↑j + 1 < ↑i → M i j = 0