Z-matrices #
A matrix whose off-diagonal entries are all non-positive is known as a Z-matrix. Cartan matrices are examples of Z-matrices.
Main results: #
Matrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen: a spectral bound result for Z-matrices satisfying a positive-definiteness condition.
theorem
Matrix.diag_pos_of_mul_diagonal_posDef
{ι : Type u_1}
{R : Type u_2}
[Fintype ι]
[DecidableEq ι]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[StarRing R]
[TrivialStar R]
(A : Matrix ι ι R)
(d : ι → R)
(hA : (diagonal d * A).PosDef)
(hD : ∀ (i : ι), 0 < d i)
(i : ι)
:
theorem
Matrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen
{ι : Type u_1}
{R : Type u_2}
[Fintype ι]
[DecidableEq ι]
[CommRing R]
[LinearOrder R]
[IsStrictOrderedRing R]
[StarRing R]
[TrivialStar R]
(A : Matrix ι ι R)
(d : ι → R)
(hA : (diagonal d * A).PosDef)
(hD : ∀ (i : ι), 0 < d i)
(μ ρ : R)
(hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0)
(hρ : Module.End.HasEigenvalue (toLin' A) ρ)
:
A spectral bound result for Z-matrices satisfying a positive-definiteness condition.
It is important because it applies to Cartan matrices, and shows that all (real) eigenvalues must
be strictly less than 4 (a fact which is necessary in the proof of
RootPairing.GeckConstruction.instIsIrreducible).