Theory Check_Matrix_Growth

theory Check_Matrix_Growth
imports Spectral_Radius_Theory_2 Sturm_Method
(* Author: Thiemann *)
section ‹An efficient algorithm to compute the growth rate of $A^n$.›

theory Check_Matrix_Growth
imports 
  Spectral_Radius_Theory_2
  Sturm_Sequences.Sturm_Method
begin

hide_const (open) Coset.order

definition check_matrix_complexity :: "real mat ⇒ real poly ⇒ nat ⇒ bool" where
  "check_matrix_complexity A cp d = (count_roots_above cp 1 = 0
     ∧ (poly cp 1 = 0 ⟶ (let ord = order 1 cp in 
        d + 1 < ord ⟶ kernel_dim ((A - 1m (dim_row A)) ^m (d + 1)) = ord)))" 

lemma check_matrix_complexity: assumes A: "A ∈ carrier_mat n n" and nn: "nonneg_mat A" 
  and check: "check_matrix_complexity A (char_poly A) d" 
shows "∃c1 c2. ∀k a. a ∈ elements_mat (A ^m k) ⟶ abs a ≤ (c1 + c2 * of_nat k ^ d)" 
proof (rule jnf_complexity_1_real[OF A nn])
  have id: "dim_gen_eigenspace A 1 (d + 1) = kernel_dim ((A - 1m (dim_row A)) ^m (d + 1))" 
    unfolding dim_gen_eigenspace_def
    by (rule arg_cong[of _ _ "λ x. kernel_dim (x ^m (d + 1))"], unfold char_matrix_def, insert A, auto)
  note check = check[unfolded check_matrix_complexity_def 
      Let_def count_roots_above_correct, folded id]
  have fin: "finite {x. poly (char_poly A) x = 0}" 
    by (rule poly_roots_finite, insert degree_monic_char_poly[OF A], auto)
  from check have "card {x. 1 < x ∧ poly (char_poly A) x = 0} = 0" by auto
  from this[unfolded card_eq_0_iff] fin 
  have "{x. 1 < x ∧ poly (char_poly A) x = 0} = {}" by auto
  thus "poly (char_poly A) x = 0 ⟹ x ≤ 1" for x by force
  assume "poly (char_poly A) 1 = 0" "d + 1 < order 1 (char_poly A)" 
  with check show "dim_gen_eigenspace A 1 (d + 1) = order 1 (char_poly A)" by auto
qed
end