Library perron_frobenius

Require Import Rdefinitions.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop ssralg.
Require Import poly matrix mxpoly mxalgebra ssrnum complex zmodp polydiv.
Require Import Rstruct C_complements set_theory big_minmax.
Require Import mxorder struct_top.
Require Import ssrcomplements mxstructure similar closed_poly.
Require Import frobenius_form jordan.

Set Implicit Arguments.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Section C_archi.

Local Notation C := (complex Rdefinitions.R).
Open Scope ring_scope.

Lemma archiC_Mixin :
 Num.archimedean_axiom [numDomainType of C].

Definition C_archiDomain := ArchiDomainType C archiC_Mixin.
Canonical C_archiDomain.

End C_archi.

Section R_Top.

Let Rn := [numDomainType of R].

Canonical Structure ArchiD_R := Eval hnf in
  [archiDomainType of R for (archi_archi [archiFieldType of R])].
Canonical Structure EspMet_R :=
  Eval hnf in [espMetType R of R for (numEspMetType Rn)].
Canonical Structure EspTop_R :=
  Eval hnf in [topologyType of R for (numTopologyType Rn)].

End R_Top.

Section definition.

Variable R : rcfType.
Local Notation C := (complex R).

Open Scope ring_scope.

Local Notation "A ^%:C" := (map_mx (real_complex_def (Phant R)) A) (at level 2).

Definition eigen_seq n (M : 'M[C]_n) := root_seq (char_poly M).

Definition spectral_radius n (M : 'M[C]_n) :=
  (\big[(@maxr _)/0]_(lam <- eigen_seq M) Re `|lam|).

Notation "\rho A" := (spectral_radius A) (at level 0).

Lemma eigenE n (M : 'M[C]_n) lam :
 (lam \in eigenvalue M) = (lam \in eigen_seq M).

Lemma rho_ge_eigen n (M : 'M[C]_n) lam : lam \in eigenvalue M ->
  `|lam| <= (\rho M)%:C.

Lemma eigen_seq_nnil n (M : 'M[C]_n.+1) : eigen_seq M != [::].

Lemma rho0 n : \rho (0 : 'M_n) = 0.

Lemma rho_ge0 n (M : 'M_n) : 0 <= \rho (M).

Lemma char_poly_trmx (T : comRingType) n (A : 'M[T]_n) :
  char_poly A = char_poly A^T.

Lemma eigen_trmx (F : fieldType) n (A : 'M[F]_n) lam :
  lam \in eigenvalue A = (lam \in eigenvalue (A^T)).

Lemma eigenvalue2P (F : fieldType) n (A : 'M[F]_n) lam :
  reflect (exists2 v : 'cV_n, A *m v = lam *: v & v != 0) (lam \in eigenvalue A ).

Lemma ex_eigen_rho n (A : 'M[C]_n.+1) :
  {lam | eigenvalue A lam & `|lam| = \rho(A)%:C}.

Lemma rho_scalemx n a (A :'M_n) : \rho (a *: A) = Re `|a| * \rho A.

End definition.

Notation "\rho A" := (spectral_radius A) (at level 0).

Section perron_thm.

Local Notation C := (complex R).
Local Notation "A ^%:C" := (map_mx (real_complex_def (Phant R)) A) (at level 2).
Local Notation "A ^%:R" := (map_mx (@Re _) A) (at level 2).

Open Scope ring_scope.

Lemma root_invf_eigen (F: fieldType) m (A : 'M[F]_m) (p : {poly F}) x :
p \in (invariant_factors A) -> root p x -> eigenvalue A x.

Lemma mx_cvg0P n (A :'M[R]_n.+1) :
  reflect ((fun k => A^+k) >->> 0) (\rho (A^%:C) < 1).

Lemma PF_gt0 n (A : 'M[R]_n) (x : 'cV_n) (lam : C) :
  let x' := (Mabs x)^%:R in
  0 <m: A ->
  x != 0 -> A^%:C *m x = lam *: x -> `|lam| = (\rho (A^%:C))%:C ->
  [/\ (A *m x' = \rho (A^%:C) *: x'), 0 <m: x' & 0 < \rho (A^%:C)].

Lemma Perron_gt0 n (A : 'M[R]_n.+1) : 0 <m: A ->
  exists x : 'cV_n.+1, 0 <m: x /\ A *m x = (\rho (A^%:C)) *: x.

End perron_thm.