(* Author: RenĂ© Thiemann Akihisa Yamada License: BSD *) 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