Theory Jordan_Normal_Form.Spectral_Radius
section ‹Spectral Radius Theory›
text ‹The following results show that the spectral radius characterize polynomial growth
of matrix powers.›
theory Spectral_Radius
imports
Jordan_Normal_Form_Existence
begin
definition "spectrum A = Collect (eigenvalue A)"
lemma spectrum_root_char_poly: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "spectrum A = {k. poly (char_poly A) k = 0}"
unfolding spectrum_def eigenvalue_root_char_poly[OF A, symmetric] by auto
lemma card_finite_spectrum: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "finite (spectrum A)" "card (spectrum A) ≤ n"
proof -
define CP where "CP = char_poly A"
from spectrum_root_char_poly[OF A] have id: "spectrum A = { k. poly CP k = 0}"
unfolding CP_def by auto
from degree_monic_char_poly[OF A] have d: "degree CP = n" and c: "coeff CP n = 1"
unfolding CP_def by auto
from c have "CP ≠ 0" by auto
from poly_roots_finite[OF this]
show "finite (spectrum A)" unfolding id .
from poly_roots_degree[OF ‹CP ≠ 0›]
show "card (spectrum A) ≤ n" unfolding id using d by simp
qed
lemma spectrum_non_empty: assumes A: "(A :: complex mat) ∈ carrier_mat n n"
and n: "n > 0"
shows "spectrum A ≠ {}"
proof -
define CP where "CP = char_poly A"
from spectrum_root_char_poly[OF A] have id: "spectrum A = { k. poly CP k = 0}"
unfolding CP_def by auto
from degree_monic_char_poly[OF A] have d: "degree CP > 0" using n
unfolding CP_def by auto
hence "¬ constant (poly CP)" by (simp add: constant_degree)
from fundamental_theorem_of_algebra[OF this] show ?thesis unfolding id by auto
qed
definition spectral_radius :: "complex mat ⇒ real" where
"spectral_radius A = Max (norm ` spectrum A)"
lemma spectral_radius_mem_max: assumes A: "A ∈ carrier_mat n n"
and n: "n > 0"
shows "spectral_radius A ∈ norm ` spectrum A" (is ?one)
"a ∈ norm ` spectrum A ⟹ a ≤ spectral_radius A"
proof -
define SA where "SA = norm ` spectrum A"
from card_finite_spectrum[OF A]
have fin: "finite SA" unfolding SA_def by auto
from spectrum_non_empty[OF A n] have ne: "SA ≠ {}" unfolding SA_def by auto
note d = spectral_radius_def SA_def[symmetric] Sup_fin_Max[symmetric]
show ?one unfolding d
by (rule Sup_fin.closed[OF fin ne], auto simp: sup_real_def)
assume "a ∈ norm ` spectrum A"
thus "a ≤ spectral_radius A" unfolding d
by (intro Sup_fin.coboundedI[OF fin])
qed
text ‹If spectral radius is at most 1, and JNF exists, then we have polynomial growth.›
lemma spectral_radius_jnf_norm_bound_le_1: assumes A: "A ∈ carrier_mat n n"
and sr_1: "spectral_radius A ≤ 1"
and jnf_exists: "∃ n_as. jordan_nf A n_as"
shows "∃ c1 c2. ∀ k. norm_bound (A ^⇩m k) (c1 + c2 * of_nat k ^ (n - 1))"
proof -
let ?p = "char_poly A"
from char_poly_factorized[OF A] obtain as where cA: "char_poly A = (∏a←as. [:- a, 1:])"
and len: "length as = n" by auto
show ?thesis
proof (rule factored_char_poly_norm_bound[OF A cA jnf_exists])
fix a
show "length (filter ((=) a) as) ≤ n" using len by auto
assume "a ∈ set as"
from linear_poly_root[OF this]
have "poly ?p a = 0" unfolding cA by simp
with spectrum_root_char_poly[OF A]
have mem: "norm a ∈ norm ` spectrum A" by auto
with card_finite_spectrum[OF A] have "n > 0" by (cases n, auto)
from spectral_radius_mem_max(2)[OF A this mem] sr_1
show "norm a ≤ 1" by auto
qed
qed
text ‹If spectral radius is smaller than 1, and JNF exists, then we have a constant bound.›
lemma spectral_radius_jnf_norm_bound_less_1: assumes A: "A ∈ carrier_mat n n"
and sr_1: "spectral_radius A < 1"
and jnf_exists: "∃ n_as. jordan_nf A n_as"
shows "∃ c. ∀ k. norm_bound (A ^⇩m k) c"
proof -
let ?p = "char_poly A"
from char_poly_factorized[OF A] obtain as where cA: "char_poly A = (∏a←as. [:- a, 1:])" by auto
have "∃ c1 c2. ∀ k. norm_bound (A ^⇩m k) (c1 + c2 * of_nat k ^ (0 - 1))"
proof (rule factored_char_poly_norm_bound[OF A cA jnf_exists])
fix a
assume "a ∈ set as"
from linear_poly_root[OF this]
have "poly ?p a = 0" unfolding cA by simp
with spectrum_root_char_poly[OF A]
have mem: "norm a ∈ norm ` spectrum A" by auto
with card_finite_spectrum[OF A] have "n > 0" by (cases n, auto)
from spectral_radius_mem_max(2)[OF A this mem] sr_1
have lt: "norm a < 1" by auto
thus "norm a ≤ 1" by auto
from lt show "norm a = 1 ⟹ length (filter ((=) a) as) ≤ 0" by auto
qed
thus ?thesis by auto
qed
text ‹If spectral radius is larger than 1, than we have exponential growth.›
lemma spectral_radius_gt_1: assumes A: "A ∈ carrier_mat n n"
and n: "n > 0"
and sr_1: "spectral_radius A > 1"
shows "∃ v c. v ∈ carrier_vec n ∧ norm c > 1 ∧ v ≠ 0⇩v n ∧ A ^⇩m k *⇩v v = c^k ⋅⇩v v"
proof -
from sr_1 spectral_radius_mem_max[OF A n] obtain ev
where ev: "ev ∈ spectrum A" and gt: "norm ev > 1" by auto
from ev[unfolded spectrum_def eigenvalue_def[abs_def]]
obtain v where ev: "eigenvector A v ev" by auto
from eigenvector_pow[OF A this] this[unfolded eigenvector_def] A gt
show ?thesis
by (intro exI[of _ v], intro exI[of _ ev], auto)
qed
text ‹If spectral radius is at most 1 for a complex matrix, then we have polynomial growth.›
lemma spectral_radius_jnf_norm_bound_le_1_upper_triangular: assumes A: "(A :: complex mat) ∈ carrier_mat n n"
and sr_1: "spectral_radius A ≤ 1"
shows "∃ c1 c2. ∀ k. norm_bound (A ^⇩m k) (c1 + c2 * of_nat k ^ (n - 1))"
by (rule spectral_radius_jnf_norm_bound_le_1[OF A sr_1],
insert char_poly_factorized[OF A] jordan_nf_exists[OF A], blast)
text ‹If spectral radius is less than 1 for a complex matrix, then we have a constant bound.›
lemma spectral_radius_jnf_norm_bound_less_1_upper_triangular: assumes A: "(A :: complex mat) ∈ carrier_mat n n"
and sr_1: "spectral_radius A < 1"
shows "∃ c. ∀ k. norm_bound (A ^⇩m k) c"
by (rule spectral_radius_jnf_norm_bound_less_1[OF A sr_1],
insert char_poly_factorized[OF A] jordan_nf_exists[OF A], blast)
text ‹And we can also get a quantative approximation via the multiplicity of the eigenvalues.›
lemma spectral_radius_poly_bound: fixes A :: "complex mat"
assumes A: "A ∈ carrier_mat n n"
and sr_1: "spectral_radius A ≤ 1"
and eq_1: "⋀ ev k. poly (char_poly A) ev = 0 ⟹ norm ev = 1 ⟹ Polynomial.order ev (char_poly A) ≤ d"
shows "∃ c1 c2. ∀ k. norm_bound (A ^⇩m k) (c1 + c2 * of_nat k ^ (d - 1))"
proof -
{
fix ev
assume "poly (char_poly A) ev = 0"
with eigenvalue_root_char_poly[OF A] have ev: "eigenvalue A ev" by simp
hence "norm ev ∈ norm ` spectrum A" unfolding spectrum_def by auto
from spectral_radius_mem_max(2)[OF A eigenvalue_imp_nonzero_dim[OF A ev] this] sr_1
have "norm ev ≤ 1" by auto
} note le_1 = this
let ?p = "char_poly A"
from char_poly_factorized[OF A] obtain as where cA: "char_poly A = (∏a←as. [:- a, 1:])"
and lenn: "length as = n" by auto
from degree_monic_char_poly[OF A] have deg: "degree (char_poly A) = n" by auto
show ?thesis
proof (rule factored_char_poly_norm_bound[OF A cA jordan_nf_exists[OF A]], rule cA)
fix ev
assume "ev ∈ set as"
hence root: "poly (char_poly A) ev = 0" unfolding cA by (rule linear_poly_root)
from le_1[OF root] show "norm ev ≤ 1" .
let ?k = "length (filter ((=) ev) as)"
have len: "length (filter ((=) (- ev)) (map uminus as)) = length (filter ((=) ev) as)"
by (induct as, auto)
have prod: "(∏a←map uminus as. [:a, 1:]) = (∏a←as. [:- a, 1:])"
by (induct as, auto)
have dvd: "[:- ev, 1:] ^ ?k dvd char_poly A" unfolding cA using
poly_linear_exp_linear_factors_rev[of "- ev" "map uminus as"]
unfolding len prod .
from ‹ev ∈ set as› deg lenn
have "degree (char_poly A) ≠ 0" by (cases as, auto)
hence "char_poly A ≠ 0" by auto
from order_max[OF dvd this] have k: "?k ≤ Polynomial.order ev (char_poly A)" .
assume "norm ev = 1"
from eq_1[OF root this] k
show "?k ≤ d" by simp
qed
qed
end