Perron–Frobenius theorem

DefinitionComplexification of a real matrix#✓fully proved

For a real square matrix \(A\) with rows and columns indexed by a nonempty finite set \(S\), its complexification \(A_{\mathbb{C}}\) is the complex matrix with entries \((A_{\mathbb{C}})_{ij} = A_{ij}\) for \(i, j \in S\), each real entry viewed as a complex number.

noncomputable def toComplexMatrix (A : Matrix n n ℝ) : Matrix n n ℂ :=
  A.map Complex.ofReal

Used by 2

Used byPerron–Frobenius theorem for irreducible nonnegative matrices · Perron–Frobenius theorem for nonzero irreducible nonnegative matrices

TheoremPerron–Frobenius theorem for irreducible nonnegative matrices#✓fully proved

Let \(A\) be a real square matrix with rows and columns indexed by a nonempty finite set \(S\), and suppose \(A\) is irreducible: its entries are nonnegative, and for all \(i, j \in S\) there is a path \(i = i_0, i_1, \dots, i_k = j\) of length \(k \ge 1\) with \(A_{i_{t-1} i_t} > 0\) for every \(t\). Then there are a real number \(r > 0\) and a vector \(v \in \mathbb{R}^S\) with \(v_i > 0\) for every \(i \in S\) such that \(Av = rv\), and every complex number \(\mu\) with \(\det(\mu E - A_{\mathbb{C}}) = 0\) satisfies \(|\mu| \le r\), where \(E\) is the identity matrix and \(A_{\mathbb{C}}\) is the complex matrix with the same entries as \(A\).

theorem _root_.Matrix.IsIrreducible.perron_frobenius
    {A : Matrix n n ℝ} (hA : A.IsIrreducible) :
    ∃ (r : ℝ) (v : n → ℝ),
      0 < r ∧ (∀ i, 0 < v i) ∧ A.mulVec v = r • v ∧
        ∀ μ : ℂ, Matrix.det (μ • (1 : Matrix n n ℂ) - A.map Complex.ofReal) = 0 → ‖μ‖ ≤ r

Uses 1 · Used by 1

Proof usesComplexification of a real matrix

Used byPerron–Frobenius theorem for nonzero irreducible nonnegative matrices

TheoremPerron–Frobenius theorem for nonzero irreducible nonnegative matrices#✓fully proved

Let \(A\) be a nonzero real square matrix with rows and columns indexed by a nonempty finite set \(S\), and suppose \(A\) is irreducible: its entries are nonnegative, and for all \(i, j \in S\) there is a path \(i = i_0, i_1, \dots, i_k = j\) of length \(k \ge 1\) with \(A_{i_{t-1} i_t} > 0\) for every \(t\). Then there are a real number \(r > 0\) and a vector \(v \in \mathbb{R}^S\) with \(v_i > 0\) for every \(i \in S\) such that \(Av = rv\), and every complex number \(\mu\) with \(\det(\mu E - A_{\mathbb{C}}) = 0\) satisfies \(|\mu| \le r\), where \(E\) is the identity matrix and \(A_{\mathbb{C}}\) is the complexification of \(A\).

The hypothesis \(A \ne 0\) is not needed: irreducibility already forces some entry to be positive.

theorem perron_frobenius
    (A : Matrix n n ℝ) (hA : A.IsIrreducible) (hA0 : A ≠ 0) :
    ∃ (r : ℝ) (v : n → ℝ),
      0 < r ∧ (∀ i, 0 < v i) ∧ A.mulVec v = r • v ∧
        ∀ μ : ℂ, Matrix.det (μ • (1 : Matrix n n ℂ) - toComplexMatrix A) = 0 → ‖μ‖ ≤ r

Sources

O. Perron, Math. Ann. 64 (1907), 248-263, DOI 10.1007/BF01449896; G. Frobenius, S.-Ber. Preuss. Akad. Wiss. Berlin (1912), 456-477.

Uses 2

Statement usesComplexification of a real matrix

Proof usesPerron–Frobenius theorem for irreducible nonnegative matrices

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.