M-matrices and Hurwitz stability

DefinitionHurwitz matrix#✓fully proved

A real square matrix is Hurwitz if every complex eigenvalue has negative real part.

def IsHurwitz (A : Matrix ι ι ℝ) : Prop :=
  ∀ μ ∈ spectrum ℂ (A.map (algebraMap ℝ ℂ)), μ.re < 0

Used by 9

Used byExponential decay of a Hurwitz semigroup · Lyapunov's indirect method (linearized stability), conditional decay form · R₀ > 1 gives an unstable mode · Threshold theorem, stability half, conditional decay form · Hurwitz criterion for block lower-triangular matrices · R₀ as a threshold for the linearized infected subsystem · Inverse positivity of M-matrices · Nonsingular M-matrix · Nonsingular M-matrices are invertible

DefinitionZ-matrix#✓fully proved

A Z-matrix has nonpositive off-diagonal entries.

def IsZMatrix (A : Matrix ι ι ℝ) : Prop :=
  ∀ i j, i ≠ j → A i j ≤ 0

Used by 5

Used byR₀ > 1 gives an unstable mode · R₀ as a threshold for the linearized infected subsystem · Inverse positivity of M-matrices · Nonsingular M-matrix · Nonsingular M-matrices are invertible

DefinitionNonsingular M-matrix#✓fully proved

A nonsingular M-matrix is a Z-matrix all of whose complex eigenvalues have positive real part (Berman–Plemmons, Ch. 6, Theorem 2.3, condition (G20)).

def IsNonsingularMMatrix (A : Matrix ι ι ℝ) : Prop :=
  A.IsZMatrix ∧ (-A).IsHurwitz

Uses 2 · Used by 6

Statement usesHurwitz matrix · Z-matrix

Used byR₀ > 1 gives an unstable mode · Threshold theorem, instability half, spectral form · Threshold theorem, stability half, conditional decay form · R₀ as a threshold for the linearized infected subsystem · Inverse positivity of M-matrices · Nonsingular M-matrices are invertible

TheoremInvertibility of 1 − K when the spectral radius is below one#✓fully proved

If the spectral radius of K is < 1, then 1 is not an eigenvalue of K, so 1 - K is invertible.

theorem isUnit_one_sub_of_spectralRadius_lt_one {K : Matrix ι ι ℝ}
    (hK : spectralRadius ℂ (K.map (algebraMap ℝ ℂ)) < 1) : IsUnit (1 - K)

Used by 3

Used byInverse positivity of M-matrices · Neumann series · Nonsingular M-matrices are invertible

TheoremNeumann series#✓fully proved

If K is entrywise nonnegative with spectral radius < 1, then (1 - K)⁻¹ is entrywise nonnegative (the proof identifies it with the limit of the partial sums ∑_{n<N} Kⁿ).

theorem inv_one_sub_nonneg {K : Matrix ι ι ℝ} (hK0 : ∀ i j, 0 ≤ K i j)
    (hK : spectralRadius ℂ (K.map (algebraMap ℝ ℂ)) < 1) (i j : ι) :
    0 ≤ (1 - K)⁻¹ i j

Uses 1 · Used by 1

Proof usesInvertibility of 1 − K when the spectral radius is below one

Used byInverse positivity of M-matrices

TheoremCollatz–Wielandt lower bound#✓fully proved

If K ≥ 0 entrywise, z ≥ 0, z ≠ 0 and r • z ≤ K *ᵥ z with r ≥ 0, then r is at most the spectral radius of K.

theorem le_spectralRadius_of_smul_le_mulVec {K : Matrix ι ι ℝ} (hK0 : ∀ i j, 0 ≤ K i j)
    {z : ι → ℝ} (hz : 0 ≤ z) (hz0 : z ≠ 0) {r : ℝ} (hr : 0 ≤ r) (h : r • z ≤ K *ᵥ z) :
    ENNReal.ofReal r ≤ spectralRadius ℂ (K.map (algebraMap ℝ ℂ))

Used by 2

Used byR₀ > 1 gives an unstable mode · R₀ as a threshold for the linearized infected subsystem

TheoremNonsingular M-matrices are invertible#✓fully proved

A nonsingular M-matrix is invertible.

theorem IsNonsingularMMatrix.isUnit {A : Matrix ι ι ℝ} (hA : A.IsNonsingularMMatrix) :
    IsUnit A

Uses 4 · Used by 2

Statement usesNonsingular M-matrix

Proof usesHurwitz matrix · Z-matrix · Invertibility of 1 − K when the spectral radius is below one

Used byR₀ > 1 gives an unstable mode · R₀ as a threshold for the linearized infected subsystem

TheoremInverse positivity of M-matrices#✓fully proved

The inverse of a nonsingular M-matrix is entrywise nonnegative (Berman–Plemmons, Ch. 6, Theorem 2.3, (G20) ⇒ (N38)).

theorem IsNonsingularMMatrix.inv_nonneg {A : Matrix ι ι ℝ} (hA : A.IsNonsingularMMatrix)
    (i j : ι) : 0 ≤ A⁻¹ i j

Uses 5 · Used by 2

Statement usesNonsingular M-matrix

Proof usesHurwitz matrix · Z-matrix · Neumann series · Invertibility of 1 − K when the spectral radius is below one

Used byR₀ > 1 gives an unstable mode · R₀ as a threshold for the linearized infected subsystem

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.