Session Perron_Frobenius

Theory Cancel_Card_Constraint

(* Author: R. Thiemann *)
section ‹Elimination of CARD('n)›

text ‹In the following theory we provide a method which modifies theorems
  of the form $P[CARD('n)]$ into $n != 0 \Longrightarrow P[n]$, so that they can more
  easily be applied.
  
  Known issues: there might be problems with nested meta-implications and meta-quantification.›

theory Cancel_Card_Constraint
imports 
  "HOL-Types_To_Sets.Types_To_Sets"
  "HOL-Library.Cardinality"
begin

lemma n_zero_nonempty: "n  0  {0 ..< n :: nat}  {}" by auto

lemma type_impl_card_n: assumes "(Rep :: 'a  nat) Abs. type_definition Rep Abs {0 ..< n :: nat}"
  shows "class.finite (TYPE('a))  CARD('a) = n"
proof -
  from assms obtain rep :: "'a  nat" and abs :: "nat  'a" where t: "type_definition rep abs {0 ..< n}" by auto
  have "card (UNIV :: 'a set) = card {0 ..< n}" using t by (rule type_definition.card)
  also have " = n" by auto
  finally have bn: "CARD ('a) = n" .
  have "finite (abs ` {0 ..< n})" by auto
  also have "abs ` {0 ..< n} = UNIV" using t by (rule type_definition.Abs_image)
  finally have "class.finite (TYPE('a))" unfolding class.finite_def .
  with bn show ?thesis by blast
qed  

ML_file ‹cancel_card_constraint.ML›


(* below you find an example what the attribute cancel_card_constraint can do and how
   it works internally *)

(*
(* input: some type based lemma with CARD inside, like t0 *)
consts P :: "nat ⇒ nat ⇒ bool" 
axiomatization where t0: "P (CARD ('a :: finite)) (CARD('a) * m)"

(* t0 is converted into a property without the cardinality constraint via the new attribute *)
lemma t_1_to_6: "n ≠ 0 ⟹ P n (n * m)"
  by (rule t0[cancel_card_constraint])

(* The internal steps are as follows. *)

(* 1st step: pull out CARD and introduce new variable n *)
lemma t1: "CARD('a :: finite) = n ⟹ P n (n * m)" 
  using t0[where 'a = 'a] by blast

(* 2nd step: get rid of sorts *)
lemma t2: "class.finite TYPE('a) ⟹ CARD('a) = n ⟹ P n (n * m)"
  by (rule t1[internalize_sort "?'a::finite"])

(* 3rd step: restructure thm so that first two assumptions are merged into one *)
lemma t3: "class.finite TYPE('a) ∧ CARD('a) = n ⟹ P n (n * m)" 
  using t2 by blast

(* 4th step: choose an appropriate carrier set *)
lemma t4: "∃Rep Abs. type_definition Rep Abs {0..<n} ⟹ P n (n * m)"
  by (rule t3[OF type_impl_card_n])

(* 5th step: cancel type definition *)
lemma t5: "{0..<n} ≠ {} ⟹ P n (n * m)"
  by (rule t4[cancel_type_definition])

(* 6th step: simplify non-empty assumption to obtain final theorem *)
lemma t6: "n ≠ 0 ⟹ P n (n * m)" 
  by (rule t5[OF n_zero_nonempty])
*)

end

File ‹cancel_card_constraint.ML›

signature CARD_ELIMINATION =
sig
  val cancel_card_constraint: thm -> thm
  val cancel_card_constraint_attr: attribute
end

structure Card_Elimination : CARD_ELIMINATION =
struct

  (* turns A ==> B[CARD('a)] ==> C[CARD('a), CARD('b)] ==> ... ==> Z 
    into CARD('a) = n1 ==> CARD('b) = n2 ==> A ==> B[n1] ==> C[n1,n2] ==> ... ==> Z *)
  fun extract_card_type ctxt thm = let
    val prop = Thm.prop_of thm 
    fun add_match_terms f t = (if f t then insert (op =) t else I) #>
      (case t of         
        t1 $ t2 => add_match_terms f t1 #> add_match_terms f t2
      | Abs (_,_,t1) => add_match_terms f t1
      | _ => I)
    fun replace_terms xys t = (case AList.lookup (op =) xys t of SOME y => y
      | NONE => case t of
        t1 $ t2 => replace_terms xys t1 $ replace_terms xys t2
      | Abs (a,b,t1) => Abs (a,b,replace_terms xys t1)
      | _ => t)
    fun find_card (Const (c,_) $ Const (t,_)) = (c = @{const_name Finite_Set.card} 
          andalso t = @{const_name Orderings.top_class.top}) 
      | find_card _ = false    
    val card_ts = add_match_terms find_card prop []
    val vars = Term.add_vars prop []
    val all_tvars = Term.add_tvars prop []
    val all_tfrees = map TFree (Variable.variant_frees ctxt [prop] (map (apfst fst) all_tvars))
    val ns = map_index (fn (i,_) => ("n" ^ string_of_int i, @{typ nat})) card_ts
    val substT_map = map fst all_tvars ~~ all_tfrees
    val substT = I subst_TVars substT_map
    val free_ns = Variable.variant_frees ctxt [prop] (map (apfst fst) vars @ ns)
    val all_frees = map (substT o Free) free_ns
    val ns = drop (length vars) all_frees
    val subst = subst_vars (substT_map, map fst vars ~~ (take (length vars) all_frees))
    val prop' = subst prop
    val match_card_ns = add_match_terms find_card prop' [] ~~ rev ns
    val prop'' = replace_terms match_card_ns prop'
    val eqs = map (HOLogic.mk_eq #> HOLogic.mk_Trueprop) match_card_ns |> rev
    val new_thm = Goal.prove ctxt (map fst free_ns) eqs prop'' (fn {prems = prems, context = ctxt} => 
      unfold_tac ctxt (map (fn thm => @{thm sym} OF [thm]) prems)
      THEN resolve_tac ctxt [thm] 1
      THEN (REPEAT (assume_tac ctxt 1))) 
  in 
    (length ns, new_thm)
  end

  (* turns A ==> B ==> C into A /\ B ==> C *)
  (* does not properly work in case of nested meta-implications and meta-quantification *)
  (* TODO: fix and simplify *)
  fun combine_first_prems ctxt thm = let
    val prop = Thm.prop_of thm
    val (p1 :: p2 :: prems) = Thm.prems_of thm
    val concl = Thm.concl_of thm
    val all_tvars = Term.add_tvars prop []
    val all_tfrees = map TFree (Variable.variant_frees ctxt [prop] (map (apfst fst) all_tvars))
    val substT_map = map fst all_tvars ~~ all_tfrees
    val prop' = subst_TVars substT_map prop
    val all_vars = Term.add_vars prop' []
    val free_ns = Variable.variant_frees ctxt [prop'] (map (apfst fst) all_vars)
    val all_frees = map Free free_ns
    val subst = subst_vars (substT_map, map fst all_vars ~~ all_frees)
    
    val p1 = subst p1
    val p2 = subst p2
    val prems = map subst prems
    val concl = subst concl
    val p = HOLogic.mk_conj (HOLogic.dest_Trueprop p1, HOLogic.dest_Trueprop p2)
      |> HOLogic.mk_Trueprop
  in
    Goal.prove ctxt (map fst free_ns) (p :: prems) concl (fn {prems = prems, context = ctxt} =>
      let 
        val p = hd prems
        val p1 = @{thm conjunct1} OF [p]
        val p2 = @{thm conjunct2} OF [p]
        val prems = tl prems
      in           
        resolve_tac ctxt [thm OF (p1 :: p2 :: prems)] 1       
      end)
  end

  (* turns CARD('a) = n1 ==> A ==> B ==> C into
        A ==> B ==> n1 != 0 ==> C *)
  fun eliminate_card_constraint ctxt thm = let
    val v = Thm.ctyp_of ctxt (Thm.prems_of thm |> hd |> (fn t => Term.add_tvars t [] |> hd) |> TVar)
    val thm = Internalize_Sort.internalize_sort v thm |> snd
    val thm = combine_first_prems ctxt thm
    val thm = (thm OF @{thms type_impl_card_n}) |> Local_Typedef.cancel_type_definition
    val thm = thm OF @{thms n_zero_nonempty}
    val thm = rotate_prems 1 thm
  in 
    thm
  end

  (* turns CARD('a) = n1 ==> ... ==> CARD('z) = n_z ==> A ==> B ==> C into
        A ==> B ==> n1 != 0 ==> ... ==> n_z != 0 ==> C *)
  fun eliminate_card_constraints ctxt thm n = 
    fold (K (eliminate_card_constraint ctxt)) (replicate n true) thm
    
  (* turns A ==> B[CARD('a)] ==> C[CARD('a), CARD('b)] ==> ... ==> Z 
    into A ==> B[n1] ==> C[n1,n2] ==> ... ==> n1 != 0 ==> n2 != 0 ==> Z *)
  fun cancel_card_constraint thm = let
    val ctxt = Proof_Context.init_global (Thm.theory_of_thm thm)
    val (n,thm) = extract_card_type ctxt thm
  in 
    eliminate_card_constraints ctxt thm n
  end

  val cancel_card_constraint_attr = Thm.rule_attribute [] (K cancel_card_constraint);

  val _ = Context.>> (Context.map_theory (Attrib.setup @{binding cancel_card_constraint} 
    (Scan.succeed cancel_card_constraint_attr) "cancels carrier constraints")) 
end

Theory Bij_Nat

(*
  Authors: J. Divasón, R. Thiemann, A. Yamada
*)
section ‹Connecting HMA-matrices with JNF-matrices›

text ‹The following theories provide a connection between the type-based representation of vectors
  and matrices in HOL multivariate-analysis (HMA) with the set-based representation of vectors and matrices
  with integer indices in the Jordan-normal-form (JNF) development.›

subsection ‹Bijections between index types of HMA and natural numbers›

text ‹At the core of HMA-connect, there has to be a translation between indices
  of vectors and matrices, which are via index-types on the one hand, and natural
  numbers on the other hand.

  We some unspecified bijection in our application, and not the conversions
  to-nat and from-nat in theory 
  Rank-Nullity-Theorem/Mod-Type, since our definitions
  below do not enforce any further type constraints.›

theory Bij_Nat
imports 
  "HOL-Library.Cardinality"
  "HOL-Library.Numeral_Type"
begin

lemma finite_set_to_list: " xs :: 'a :: finite list. distinct xs  set xs = Y"
proof -
  have "finite Y" by simp
  thus ?thesis 
  proof (induct Y rule: finite_induct)
    case (insert y Y)
    then obtain xs where xs: "distinct xs" "set xs = Y" by auto
    show ?case
      by (rule exI[of _ "y # xs"], insert xs insert(2), auto)
  qed simp
qed

definition univ_list :: "'a :: finite list" where
  "univ_list = (SOME xs. distinct xs  set xs = UNIV)"

lemma univ_list: "distinct (univ_list :: 'a list)" "set univ_list = (UNIV :: 'a :: finite set)"
proof -
  let ?xs = "univ_list :: 'a list"
  have "distinct ?xs  set ?xs = UNIV"
    unfolding univ_list_def
    by (rule someI_ex, rule finite_set_to_list)
  thus "distinct ?xs" "set ?xs = UNIV" by auto
qed

definition to_nat :: "'a :: finite  nat" where
  "to_nat a = (SOME i. univ_list ! i = a  i < length (univ_list :: 'a list))"

definition from_nat :: "nat  'a :: finite" where
  "from_nat i = univ_list ! i"

lemma length_univ_list_card: "length (univ_list :: 'a :: finite list) = CARD('a)"
  using distinct_card[of "univ_list :: 'a list", symmetric] 
  by (auto simp: univ_list)

lemma to_nat_ex: "∃! i. univ_list ! i = (a :: 'a :: finite)  i < length (univ_list :: 'a list)"
proof -
  let ?ul = "univ_list :: 'a list"
  have a_in_set: "a  set ?ul" unfolding univ_list by auto
  from this [unfolded set_conv_nth] 
  obtain i where i1: "?ul ! i = a  i < length ?ul" by auto
  show ?thesis
  proof (rule ex1I, rule i1)
    fix j
    assume "?ul ! j = a  j < length ?ul"
    moreover have "distinct ?ul" by (simp add: univ_list)
    ultimately show "j = i" using i1 nth_eq_iff_index_eq by blast
  qed
qed
  
lemma to_nat_less_card: "to_nat (a :: 'a :: finite) < CARD('a)"
proof -
  let ?ul = "univ_list :: 'a list"
  from to_nat_ex[of a] obtain i where 
  i1: "univ_list ! i = a  i<length (univ_list::'a list)" by auto
  show ?thesis unfolding to_nat_def
  proof (rule someI2, rule i1)
   fix x
   assume x: "?ul ! x = a  x < length ?ul"
   thus "x < CARD ('a)" using x by (simp add: univ_list length_univ_list_card)
  qed
qed

lemma to_nat_from_nat_id: 
  assumes i: "i < CARD('a :: finite)" 
  shows "to_nat (from_nat i :: 'a) = i"
  unfolding to_nat_def from_nat_def
proof (rule some_equality, simp)
  have l: "length (univ_list::'a list) = card (set (univ_list::'a list))" 
    by (rule distinct_card[symmetric], simp add: univ_list)
  thus i2: "i < length (univ_list::'a list)"
    using i unfolding univ_list by simp
   fix n 
   assume n: "(univ_list::'a list) ! n = (univ_list::'a list) ! i  n < length (univ_list::'a list)"
   have d: "distinct (univ_list::'a list)" using univ_list by simp      
   show "n = i" using nth_eq_iff_index_eq[OF d _ i2] n by auto
qed

lemma from_nat_inj: assumes i: "i < CARD('a :: finite)"
  and j: "j < CARD('a :: finite)"
  and id: "(from_nat i :: 'a) = from_nat j"
  shows "i = j"
proof -
  from arg_cong[OF id, of to_nat]
  show ?thesis using i j by (simp add: to_nat_from_nat_id)
qed

lemma from_nat_to_nat_id[simp]:
  "(from_nat (to_nat a)) = (a::'a :: finite)"
proof -
  have a_in_set: "a  set (univ_list)" unfolding univ_list by auto
  from this [unfolded set_conv_nth] 
  obtain i where i1: "univ_list ! i = a  i<length (univ_list::'a list)" by auto
  show ?thesis 
  unfolding to_nat_def from_nat_def
  by (rule someI2, rule i1, simp)
qed

lemma to_nat_inj[simp]: assumes "to_nat a = to_nat b"
  shows "a = b"
proof -
  from to_nat_ex[of a] to_nat_ex[of b]
  show "a = b" unfolding to_nat_def by (metis assms from_nat_to_nat_id)
qed

lemma range_to_nat: "range (to_nat :: 'a :: finite  nat) = {0 ..< CARD('a)}" (is "?l = ?r")
proof -
  {
    fix i
    assume "i  ?l"
    hence "i  ?r" using to_nat_less_card[where 'a = 'a] by auto
  }
  moreover
  {
    fix i
    assume "i  ?r"
    hence "i < CARD('a)" by auto
    from to_nat_from_nat_id[OF this] 
    have "i  ?l" by (metis range_eqI)
  }
  ultimately show ?thesis by auto
qed

lemma inj_to_nat: "inj to_nat" by (simp add: inj_on_def)

lemma bij_to_nat: "bij_betw to_nat (UNIV :: 'a :: finite set) {0 ..< CARD('a)}"
  unfolding bij_betw_def by (auto simp: range_to_nat inj_to_nat)


lemma numeral_nat: "(numeral m1 :: nat) * numeral n1  numeral (m1 * n1)" 
  "(numeral m1 :: nat) + numeral n1  numeral (m1 + n1)" by simp_all

lemmas card_num_simps = 
  card_num1 card_bit0 card_bit1 
  mult_num_simps
  add_num_simps 
  eq_num_simps
  mult_Suc_right mult_0_right One_nat_def add.right_neutral 
  numeral_nat Suc_numeral 

end

Theory HMA_Connect

(*
  Authors: J. Divasón, R. Thiemann, A. Yamada, O. Kunčar
*)

subsection ‹Transfer rules to convert theorems from JNF to HMA and vice-versa.›

theory HMA_Connect
imports 
  Jordan_Normal_Form.Spectral_Radius 
  "HOL-Analysis.Determinants"
  "HOL-Analysis.Cartesian_Euclidean_Space"
  Bij_Nat
  Cancel_Card_Constraint
  "HOL-Eisbach.Eisbach" 
begin

text ‹Prefer certain constants and lemmas without prefix.›

hide_const (open) Matrix.mat
hide_const (open) Matrix.row
hide_const (open) Determinant.det

lemmas mat_def = Finite_Cartesian_Product.mat_def
lemmas det_def = Determinants.det_def
lemmas row_def = Finite_Cartesian_Product.row_def

notation vec_index (infixl "$v" 90)
notation vec_nth (infixl "$h" 90)


text ‹Forget that @{typ "'a mat"}, @{typ "'a Matrix.vec"}, and @{typ "'a poly"} 
  have been defined via lifting›


(* TODO: add to end of matrix theory, stores lifting + transfer setup *)
lifting_forget vec.lifting
lifting_forget mat.lifting

lifting_forget poly.lifting

text ‹Some notions which we did not find in the HMA-world.›
definition eigen_vector :: "'a::comm_ring_1 ^ 'n ^ 'n  'a ^ 'n  'a  bool" where
  "eigen_vector A v ev = (v  0  A *v v = ev *s v)"

definition eigen_value :: "'a :: comm_ring_1 ^ 'n ^ 'n  'a  bool" where
  "eigen_value A k = ( v. eigen_vector A v k)"

definition similar_matrix_wit 
  :: "'a :: semiring_1 ^ 'n ^ 'n  'a ^ 'n ^ 'n  'a ^ 'n ^ 'n  'a ^ 'n ^ 'n  bool" where
  "similar_matrix_wit A B P Q = (P ** Q = mat 1  Q ** P = mat 1  A = P ** B ** Q)"

definition similar_matrix 
  :: "'a :: semiring_1 ^ 'n ^ 'n  'a ^ 'n ^ 'n  bool" where
  "similar_matrix A B = ( P Q. similar_matrix_wit A B P Q)"

definition spectral_radius :: "complex ^ 'n ^ 'n  real" where
  "spectral_radius A = Max { norm ev | v ev. eigen_vector A v ev}"

definition Spectrum :: "'a :: field ^ 'n ^ 'n  'a set" where
  "Spectrum A = Collect (eigen_value A)" 

definition vec_elements_h :: "'a ^ 'n  'a set" where
  "vec_elements_h v = range (vec_nth v)"

lemma vec_elements_h_def': "vec_elements_h v = {v $h i | i. True}"
  unfolding vec_elements_h_def by auto

definition elements_mat_h :: "'a ^ 'nc ^ 'nr  'a set" where
  "elements_mat_h A = range (λ (i,j). A $h i $h j)"

lemma elements_mat_h_def': "elements_mat_h A = {A $h i $h j | i j. True}"
  unfolding elements_mat_h_def by auto

definition map_vector :: "('a  'b)  'a ^'n  'b ^'n" where 
  "map_vector f v  χ i. f (v $h i)"

definition map_matrix :: "('a  'b)  'a ^ 'n ^ 'm  'b ^ 'n ^ 'm" where 
  "map_matrix f A  χ i. map_vector f (A $h i)"

definition normbound :: "'a :: real_normed_field ^ 'nc ^ 'nr  real  bool" where
  "normbound A b   x  elements_mat_h A. norm x  b"

lemma spectral_radius_ev_def: "spectral_radius A = Max (norm ` (Collect (eigen_value A)))"
  unfolding spectral_radius_def eigen_value_def[abs_def]
  by (rule arg_cong[where f = Max], auto) 

lemma elements_mat: "elements_mat A = {A $$ (i,j) | i j. i < dim_row A  j < dim_col A}"
  unfolding elements_mat_def by force

definition vec_elements :: "'a Matrix.vec  'a set"
  where "vec_elements v = set [v $ i. i <- [0 ..< dim_vec v]]"

lemma vec_elements: "vec_elements v = { v $ i | i. i < dim_vec v}"
  unfolding vec_elements_def by auto


(* TODO: restore a bundle, for e.g., for matrix_impl *)
context includes vec.lifting 
begin
end

definition from_hmav :: "'a ^ 'n   'a Matrix.vec" where
  "from_hmav v = Matrix.vec CARD('n) (λ i. v $h from_nat i)"

definition from_hmam :: "'a ^ 'nc ^ 'nr  'a Matrix.mat" where
  "from_hmam a = Matrix.mat CARD('nr) CARD('nc) (λ (i,j). a $h from_nat i $h from_nat j)"

definition to_hmav :: "'a Matrix.vec  'a ^ 'n" where
  "to_hmav v = (χ i. v $v to_nat i)"

definition to_hmam :: "'a Matrix.mat  'a ^ 'nc  ^ 'nr " where
  "to_hmam a = (χ i j. a $$ (to_nat i, to_nat j))"

declare vec_lambda_eta[simp]

lemma to_hma_from_hmav[simp]: "to_hmav (from_hmav v) = v"
  by (auto simp: to_hmav_def from_hmav_def to_nat_less_card)

lemma to_hma_from_hmam[simp]: "to_hmam (from_hmam v) = v"
  by (auto simp: to_hmam_def from_hmam_def to_nat_less_card)

lemma from_hma_to_hmav[simp]:
  "v  carrier_vec (CARD('n))  from_hmav (to_hmav v :: 'a ^ 'n) = v"
  by (auto simp: to_hmav_def from_hmav_def to_nat_from_nat_id)

lemma from_hma_to_hmam[simp]:
  "A  carrier_mat (CARD('nr)) (CARD('nc))  from_hmam (to_hmam A :: 'a ^ 'nc  ^ 'nr) = A"
  by (auto simp: to_hmam_def from_hmam_def to_nat_from_nat_id)

lemma from_hmav_inj[simp]: "from_hmav x = from_hmav y  x = y"
  by (intro iffI, insert to_hma_from_hmav[of x], auto)

lemma from_hmam_inj[simp]: "from_hmam x = from_hmam y  x = y"
  by(intro iffI, insert to_hma_from_hmam[of x], auto)

definition HMA_V :: "'a Matrix.vec  'a ^ 'n   bool" where 
  "HMA_V = (λ v w. v = from_hmav w)"

definition HMA_M :: "'a Matrix.mat  'a ^ 'nc  ^ 'nr   bool" where 
  "HMA_M = (λ a b. a = from_hmam b)"

definition HMA_I :: "nat  'n :: finite  bool" where
  "HMA_I = (λ i a. i = to_nat a)"

context includes lifting_syntax
begin

lemma Domainp_HMA_V [transfer_domain_rule]: 
  "Domainp (HMA_V :: 'a Matrix.vec  'a ^ 'n  bool) = (λ v. v  carrier_vec (CARD('n )))"
  by(intro ext iffI, insert from_hma_to_hmav[symmetric], auto simp: from_hmav_def HMA_V_def)

lemma Domainp_HMA_M [transfer_domain_rule]: 
  "Domainp (HMA_M :: 'a Matrix.mat  'a ^ 'nc  ^ 'nr   bool) 
  = (λ A. A  carrier_mat CARD('nr) CARD('nc))"
  by (intro ext iffI, insert from_hma_to_hmam[symmetric], auto simp: from_hmam_def HMA_M_def)

lemma Domainp_HMA_I [transfer_domain_rule]: 
  "Domainp (HMA_I :: nat  'n :: finite  bool) = (λ i. i < CARD('n))" (is "?l = ?r")
proof (intro ext)
  fix i :: nat
  show "?l i = ?r i"
    unfolding HMA_I_def Domainp_iff
    by (auto intro: exI[of _ "from_nat i"] simp: to_nat_from_nat_id to_nat_less_card)
qed

lemma bi_unique_HMA_V [transfer_rule]: "bi_unique HMA_V" "left_unique HMA_V" "right_unique HMA_V"
  unfolding HMA_V_def bi_unique_def left_unique_def right_unique_def by auto

lemma bi_unique_HMA_M [transfer_rule]: "bi_unique HMA_M" "left_unique HMA_M" "right_unique HMA_M"
  unfolding HMA_M_def bi_unique_def left_unique_def right_unique_def by auto

lemma bi_unique_HMA_I [transfer_rule]: "bi_unique HMA_I" "left_unique HMA_I" "right_unique HMA_I"
  unfolding HMA_I_def bi_unique_def left_unique_def right_unique_def by auto

lemma right_total_HMA_V [transfer_rule]: "right_total HMA_V"
  unfolding HMA_V_def right_total_def by simp

lemma right_total_HMA_M [transfer_rule]: "right_total HMA_M"
  unfolding HMA_M_def right_total_def by simp

lemma right_total_HMA_I [transfer_rule]: "right_total HMA_I"
  unfolding HMA_I_def right_total_def by simp

lemma HMA_V_index [transfer_rule]: "(HMA_V ===> HMA_I ===> (=)) ($v) ($h)"
  unfolding rel_fun_def HMA_V_def HMA_I_def from_hmav_def
  by (auto simp: to_nat_less_card)

text ‹We introduce the index function to have pointwise access to 
  HMA-matrices by a constant. Otherwise, the transfer rule 
  with @{term "λ A i j. A $h i $h j"} instead of index is not applicable.›

definition "index_hma A i j  A $h i $h j"

lemma HMA_M_index [transfer_rule]:
  "(HMA_M ===> HMA_I ===> HMA_I ===> (=)) (λ A i j. A $$ (i,j)) index_hma"
  by (intro rel_funI, simp add: index_hma_def to_nat_less_card HMA_M_def HMA_I_def from_hmam_def)  

lemma HMA_V_0 [transfer_rule]: "HMA_V (0v CARD('n)) (0 :: 'a :: zero ^ 'n)"
  unfolding HMA_V_def from_hmav_def by auto

lemma HMA_M_0 [transfer_rule]: 
  "HMA_M (0m CARD('nr) CARD('nc)) (0 :: 'a :: zero ^ 'nc  ^ 'nr )"
  unfolding HMA_M_def from_hmam_def by auto

lemma HMA_M_1[transfer_rule]:
  "HMA_M (1m (CARD('n))) (mat 1 :: 'a::{zero,one}^'n^'n)"
  unfolding HMA_M_def
  by (auto simp add: mat_def from_hmam_def from_nat_inj)

lemma from_hmav_add: "from_hmav v + from_hmav w = from_hmav (v + w)"
  unfolding from_hmav_def by auto

lemma HMA_V_add [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (+) (+) "
  unfolding rel_fun_def HMA_V_def
  by (auto simp: from_hmav_add)

lemma from_hmav_diff: "from_hmav v - from_hmav w = from_hmav (v - w)"
  unfolding from_hmav_def by auto

lemma HMA_V_diff [transfer_rule]: "(HMA_V ===> HMA_V ===> HMA_V) (-) (-)"
  unfolding rel_fun_def HMA_V_def
  by (auto simp: from_hmav_diff)

lemma from_hmam_add: "from_hmam a + from_hmam b = from_hmam (a + b)"
  unfolding from_hmam_def by auto

lemma HMA_M_add [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (+) (+) "
  unfolding rel_fun_def HMA_M_def
  by (auto simp: from_hmam_add)

lemma from_hmam_diff: "from_hmam a - from_hmam b = from_hmam (a - b)"
  unfolding from_hmam_def by auto

lemma HMA_M_diff [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) (-) (-) "
  unfolding rel_fun_def HMA_M_def
  by (auto simp: from_hmam_diff)

lemma scalar_product: fixes v :: "'a :: semiring_1 ^ 'n "
  shows "scalar_prod (from_hmav v) (from_hmav w) = scalar_product v w"
  unfolding scalar_product_def scalar_prod_def from_hmav_def dim_vec
  by (simp add: sum.reindex[OF inj_to_nat, unfolded range_to_nat])

lemma [simp]:
  "from_hmam (y :: 'a ^ 'nc  ^ 'nr)  carrier_mat (CARD('nr)) (CARD('nc))"
  "dim_row (from_hmam (y :: 'a ^ 'nc  ^ 'nr )) = CARD('nr)"
  "dim_col (from_hmam (y :: 'a ^ 'nc  ^ 'nr )) = CARD('nc)"
  unfolding from_hmam_def by simp_all

lemma [simp]:
  "from_hmav (y :: 'a ^ 'n)  carrier_vec (CARD('n))"
  "dim_vec (from_hmav (y :: 'a ^ 'n)) = CARD('n)"
  unfolding from_hmav_def by simp_all

declare rel_funI [intro!]

lemma HMA_scalar_prod [transfer_rule]:
  "(HMA_V ===> HMA_V ===> (=)) scalar_prod scalar_product"
  by (auto simp: HMA_V_def scalar_product)

lemma HMA_row [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. Matrix.row a i) row"
  unfolding HMA_M_def HMA_I_def HMA_V_def
  by (auto simp: from_hmam_def from_hmav_def to_nat_less_card row_def)

lemma HMA_col [transfer_rule]: "(HMA_I ===> HMA_M ===> HMA_V) (λ i a. col a i) column"
  unfolding HMA_M_def HMA_I_def HMA_V_def
  by (auto simp: from_hmam_def from_hmav_def to_nat_less_card column_def)

definition mk_mat :: "('i  'j  'c)  'c^'j^'i" where
  "mk_mat f = (χ i j. f i j)"

definition mk_vec :: "('i  'c)  'c^'i" where
  "mk_vec f = (χ i. f i)"

lemma HMA_M_mk_mat[transfer_rule]: "((HMA_I ===> HMA_I ===> (=)) ===> HMA_M) 
  (λ f. Matrix.mat (CARD('nr)) (CARD('nc)) (λ (i,j). f i j)) 
  (mk_mat :: (('nr  'nc  'a)  'a^'nc^'nr))"
proof-
  {
    fix x y i j
    assume id: " (ya :: 'nr) (yb :: 'nc). (x (to_nat ya) (to_nat yb) :: 'a) = y ya yb"
       and i: "i < CARD('nr)" and j: "j < CARD('nc)"
    from to_nat_from_nat_id[OF i] to_nat_from_nat_id[OF j] id[rule_format, of "from_nat i" "from_nat j"]
    have "x i j = y (from_nat i) (from_nat j)" by auto
  }
  thus ?thesis
    unfolding rel_fun_def mk_mat_def HMA_M_def HMA_I_def from_hmam_def by auto
qed

lemma HMA_M_mk_vec[transfer_rule]: "((HMA_I ===> (=)) ===> HMA_V) 
  (λ f. Matrix.vec (CARD('n)) (λ i. f i)) 
  (mk_vec :: (('n  'a)  'a^'n))"
proof-
  {
    fix x y i
    assume id: " (ya :: 'n). (x (to_nat ya) :: 'a) = y ya"
       and i: "i < CARD('n)" 
    from to_nat_from_nat_id[OF i] id[rule_format, of "from_nat i"]
    have "x i = y (from_nat i)" by auto
  }
  thus ?thesis
    unfolding rel_fun_def mk_vec_def HMA_V_def HMA_I_def from_hmav_def by auto
qed


lemma mat_mult_scalar: "A ** B = mk_mat (λ i j. scalar_product (row i A) (column j B))"
  unfolding vec_eq_iff matrix_matrix_mult_def scalar_product_def mk_mat_def
  by (auto simp: row_def column_def)

lemma mult_mat_vec_scalar: "A *v v = mk_vec (λ i. scalar_product (row i A) v)"
  unfolding vec_eq_iff matrix_vector_mult_def scalar_product_def mk_mat_def mk_vec_def
  by (auto simp: row_def column_def)

lemma dim_row_transfer_rule: 
  "HMA_M A (A' :: 'a ^ 'nc ^ 'nr)  (=) (dim_row A) (CARD('nr))"
  unfolding HMA_M_def by auto

lemma dim_col_transfer_rule: 
  "HMA_M A (A' :: 'a ^ 'nc ^ 'nr)  (=) (dim_col A) (CARD('nc))"
  unfolding HMA_M_def by auto

lemma HMA_M_mult [transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) ((*)) ((**))"
proof -
  {
    fix A B :: "'a :: semiring_1 mat" and A' :: "'a ^ 'n  ^ 'nr" and B' :: "'a ^ 'nc ^ 'n"
    assume 1[transfer_rule]: "HMA_M A A'" "HMA_M B B'"
    note [transfer_rule] = dim_row_transfer_rule[OF 1(1)] dim_col_transfer_rule[OF 1(2)]
    have "HMA_M (A * B) (A' ** B')"
      unfolding times_mat_def mat_mult_scalar
      by (transfer_prover_start, transfer_step+, transfer, auto)
  }
  thus ?thesis by blast
qed
      

lemma HMA_V_smult [transfer_rule]: "((=) ===> HMA_V ===> HMA_V) (⋅v) ((*s))"
  unfolding smult_vec_def 
  unfolding rel_fun_def HMA_V_def from_hmav_def
  by auto

lemma HMA_M_mult_vec [transfer_rule]: "(HMA_M ===> HMA_V ===> HMA_V) ((*v)) ((*v))"
proof -
  {
    fix A :: "'a :: semiring_1 mat" and v :: "'a Matrix.vec"
      and A' :: "'a ^ 'nc  ^ 'nr" and v' :: "'a ^ 'nc"
    assume 1[transfer_rule]: "HMA_M A A'" "HMA_V v v'"
    note [transfer_rule] = dim_row_transfer_rule
    have "HMA_V (A *v v) (A' *v v')"
      unfolding mult_mat_vec_def mult_mat_vec_scalar
      by (transfer_prover_start, transfer_step+, transfer, auto)
  }
  thus ?thesis by blast  
qed

lemma HMA_det [transfer_rule]: "(HMA_M ===> (=)) Determinant.det 
  (det :: 'a :: comm_ring_1 ^ 'n ^ 'n  'a)"
proof -
  {
    fix a :: "'a ^ 'n ^ 'n"
    let ?tn = "to_nat :: 'n :: finite  nat"
    let ?fn = "from_nat :: nat  'n"
    let ?zn = "{0..< CARD('n)}"
    let ?U = "UNIV :: 'n set"
    let ?p1 = "{p. p permutes ?zn}"
    let ?p2 = "{p. p permutes ?U}"  
    let ?f= "λ p i. if i  ?U then ?fn (p (?tn i)) else i"
    let ?g = "λ p i. ?fn (p (?tn i))"
    have fg: " a b c. (if a  ?U then b else c) = b" by auto
    have "?p2 = ?f ` ?p1" 
      by (rule permutes_bij', auto simp: to_nat_less_card to_nat_from_nat_id)
    hence id: "?p2 = ?g ` ?p1" by simp
    have inj_g: "inj_on ?g ?p1"
      unfolding inj_on_def
    proof (intro ballI impI ext, auto)
      fix p q i
      assume p: "p permutes ?zn" and q: "q permutes ?zn"
        and id: "(λ i. ?fn (p (?tn i))) = (λ i. ?fn (q (?tn i)))"
      {
        fix i
        from permutes_in_image[OF p] have pi: "p (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
        from permutes_in_image[OF q] have qi: "q (?tn i) < CARD('n)" by (simp add: to_nat_less_card)
        from fun_cong[OF id] have "?fn (p (?tn i))  = from_nat (q (?tn i))" .
        from arg_cong[OF this, of ?tn] have "p (?tn i) = q (?tn i)"
          by (simp add: to_nat_from_nat_id pi qi)
      } note id = this             
      show "p i = q i"
      proof (cases "i < CARD('n)")
        case True
        hence "?tn (?fn i) = i" by (simp add: to_nat_from_nat_id)
        from id[of "?fn i", unfolded this] show ?thesis .
      next
        case False
        thus ?thesis using p q unfolding permutes_def by simp
      qed
    qed
    have mult_cong: " a b c d. a = b  c = d  a * c = b * d" by simp
    have "sum (λ p. 
      signof p * (i?zn. a $h ?fn i $h ?fn (p i))) ?p1
      = sum (λ p. of_int (sign p) * (iUNIV. a $h i $h p i)) ?p2"
      unfolding id sum.reindex[OF inj_g]
    proof (rule sum.cong[OF refl], unfold mem_Collect_eq o_def, rule mult_cong)
      fix p
      assume p: "p permutes ?zn"
      let ?q = "λ i. ?fn (p (?tn i))"
      from id p have q: "?q permutes ?U" by auto
      from p have pp: "permutation p" unfolding permutation_permutes by auto
      let ?ft = "λ p i. ?fn (p (?tn i))"
      have fin: "finite ?zn" by simp
      have "sign p = sign ?q  p permutes ?zn"
      using p fin proof (induction rule: permutes_induct)
        case id
        show ?case by (auto simp: sign_id[unfolded id_def] permutes_id[unfolded id_def])
      next
        case (swap a b p)
        then have ‹permutation p
          by (auto intro: permutes_imp_permutation)
        let ?sab = "Fun.swap a b id"
        let ?sfab = "Fun.swap (?fn a) (?fn b) id"
        have p_sab: "permutation ?sab" by (rule permutation_swap_id)
        have p_sfab: "permutation ?sfab" by (rule permutation_swap_id)
        from swap(4) have IH1: "p permutes ?zn" and IH2: "sign p = sign (?ft p)" by auto
        have sab_perm: "?sab permutes ?zn" using swap(1-2) by (rule permutes_swap_id)
        from permutes_compose[OF IH1 this] have perm1: "?sab o p permutes ?zn" .
        from IH1 have p_p1: "p  ?p1" by simp
        hence "?ft p  ?ft ` ?p1" by (rule imageI)
        from this[folded id] have "?ft p permutes ?U" by simp
        hence p_ftp: "permutation (?ft p)" unfolding permutation_permutes by auto
        {
          fix a b
          assume a: "a  ?zn" and b: "b  ?zn"
          hence "(?fn a = ?fn b) = (a = b)" using swap(1-2)
            by (auto simp: from_nat_inj)
        } note inj = this
        from inj[OF swap(1-2)] have id2: "sign ?sfab = sign ?sab" unfolding sign_swap_id by simp
        have id: "?ft (Fun.swap a b id  p) = Fun.swap (?fn a) (?fn b) id  ?ft p"
        proof
          fix c 
          show "?ft (Fun.swap a b id  p) c = (Fun.swap (?fn a) (?fn b) id  ?ft p) c"
          proof (cases "p (?tn c) = a  p (?tn c) = b")
            case True
            thus ?thesis by (cases, auto simp add: swap_id_eq)
          next
            case False
            hence neq: "p (?tn c)  a" "p (?tn c)  b" by auto
            have pc: "p (?tn c)  ?zn" unfolding permutes_in_image[OF IH1] 
              by (simp add: to_nat_less_card)
            from neq[folded inj[OF pc swap(1)] inj[OF pc swap(2)]]
            have "?fn (p (?tn c))  ?fn a" "?fn (p (?tn c))  ?fn b" .
            with neq show ?thesis by (auto simp: swap_id_eq)
          qed
        qed
        show ?case unfolding IH2 id sign_compose[OF p_sab ‹permutation p] sign_compose[OF p_sfab p_ftp] id2
          by (rule conjI[OF refl perm1])
      qed
      thus "signof p = of_int (sign ?q)" unfolding signof_def sign_def by auto
      show "(i = 0..<CARD('n). a $h ?fn i $h ?fn (p i)) =
           (iUNIV. a $h i $h ?q i)" unfolding 
           range_to_nat[symmetric] prod.reindex[OF inj_to_nat]
        by (rule prod.cong[OF refl], unfold o_def, simp)
    qed   
  }
  thus ?thesis unfolding HMA_M_def 
    by (auto simp: from_hmam_def Determinant.det_def det_def)
qed

lemma HMA_mat[transfer_rule]: "((=) ===> HMA_M) (λ k. k m 1m CARD('n)) 
  (Finite_Cartesian_Product.mat :: 'a::semiring_1  'a^'n^'n)"
  unfolding Finite_Cartesian_Product.mat_def[abs_def] rel_fun_def HMA_M_def
  by (auto simp: from_hmam_def from_nat_inj)


lemma HMA_mat_minus[transfer_rule]: "(HMA_M ===> HMA_M ===> HMA_M) 
  (λ A B. A + map_mat uminus B) ((-) :: 'a :: group_add ^'nc^'nr  'a^'nc^'nr  'a^'nc^'nr)"
  unfolding rel_fun_def HMA_M_def from_hmam_def by auto

definition mat2matofpoly where "mat2matofpoly A = (χ i j. [: A $ i $ j :])"

definition charpoly where charpoly_def: "charpoly A = det (mat (monom 1 (Suc 0)) - mat2matofpoly A)"

definition erase_mat :: "'a :: zero ^ 'nc ^ 'nr  'nr  'nc  'a ^ 'nc ^ 'nr" 
  where "erase_mat A i j = (χ i'. χ  j'. if i' = i  j' = j then 0 else A $ i' $ j')" 

definition sum_UNIV_type :: "('n :: finite  'a :: comm_monoid_add)  'n itself  'a" where
  "sum_UNIV_type f _ = sum f UNIV" 

definition sum_UNIV_set :: "(nat  'a :: comm_monoid_add)  nat  'a" where
  "sum_UNIV_set f n = sum f {..<n}" 

definition HMA_T :: "nat  'n :: finite itself  bool" where
  "HMA_T n _ = (n = CARD('n))" 

lemma HMA_mat2matofpoly[transfer_rule]: "(HMA_M ===> HMA_M) (λx. map_mat (λa. [:a:]) x) mat2matofpoly"
  unfolding rel_fun_def HMA_M_def from_hmam_def mat2matofpoly_def by auto

lemma HMA_char_poly [transfer_rule]: 
  "((HMA_M :: ('a:: comm_ring_1 mat  'a^'n^'n  bool)) ===> (=)) char_poly charpoly"
proof -
  {
    fix A :: "'a mat" and A' :: "'a^'n^'n"
    assume [transfer_rule]: "HMA_M A A'"
    hence [simp]: "dim_row A = CARD('n)" by (simp add: HMA_M_def)
    have [simp]: "monom 1 (Suc 0) = [:0, 1 :: 'a :]"
      by (simp add: monom_Suc)
    have [simp]: "map_mat uminus (map_mat (λa. [:a:]) A) = map_mat (λa. [:-a:]) A"
      by (rule eq_matI, auto)
    have "char_poly A = charpoly A'"
      unfolding char_poly_def[abs_def] char_poly_matrix_def charpoly_def[abs_def]
      by (transfer, simp)
  }
  thus ?thesis by blast
qed
 

lemma HMA_eigen_vector [transfer_rule]: "(HMA_M ===> HMA_V ===> (=)) eigenvector eigen_vector"
proof -
  { 
    fix A :: "'a mat" and v :: "'a Matrix.vec" 
    and A' :: "'a ^ 'n ^ 'n" and v' :: "'a ^ 'n" and k :: 'a
    assume 1[transfer_rule]: "HMA_M A A'" and 2[transfer_rule]: "HMA_V v v'"
    hence [simp]: "dim_row A = CARD('n)" "dim_vec v = CARD('n)" by (auto simp add: HMA_V_def HMA_M_def)
    have [simp]: "v  carrier_vec CARD('n)" using 2 unfolding HMA_V_def by simp
    have "eigenvector A v = eigen_vector A' v'" 
      unfolding eigenvector_def[abs_def] eigen_vector_def[abs_def] 
      by (transfer, simp)
  }
  thus ?thesis by blast
qed


lemma HMA_eigen_value [transfer_rule]: "(HMA_M ===> (=) ===> (=)) eigenvalue eigen_value"
proof -
  {
    fix A :: "'a mat" and A' :: "'a ^ 'n  ^ 'n" and k
    assume 1[transfer_rule]: "HMA_M A A'"
    hence [simp]: "dim_row A = CARD('n)" by (simp add: HMA_M_def)
    note [transfer_rule] = dim_row_transfer_rule[OF 1(1)]    
    have "(eigenvalue A k) = (eigen_value A' k)"
      unfolding eigenvalue_def[abs_def] eigen_value_def[abs_def] 
      by (transfer, auto simp add: eigenvector_def)
  }
  thus ?thesis by blast
qed


lemma HMA_spectral_radius [transfer_rule]: 
  "(HMA_M ===> (=)) Spectral_Radius.spectral_radius spectral_radius"
  unfolding Spectral_Radius.spectral_radius_def[abs_def] spectrum_def 
    spectral_radius_ev_def[abs_def]
  by transfer_prover

lemma HMA_elements_mat[transfer_rule]: "((HMA_M :: ('a mat  'a ^ 'nc ^ 'nr  bool))  ===> (=)) 
  elements_mat elements_mat_h"
proof -
  {
    fix y :: "'a ^ 'nc ^ 'nr" and i j :: nat
    assume i: "i < CARD('nr)" and j: "j < CARD('nc)"
    hence "from_hmam y $$ (i, j)  range (λ(i, ya). y $h i $h ya)"      
      using to_nat_from_nat_id[OF i] to_nat_from_nat_id[OF j] by (auto simp: from_hmam_def)
  }
  moreover
  {
    fix y :: "'a ^ 'nc ^ 'nr" and a b
    have "i j. y $h a $h b = from_hmam y $$ (i, j)  i < CARD('nr)  j < CARD('nc)"
      unfolding from_hmam_def
      by (rule exI[of _ "Bij_Nat.to_nat a"], rule exI[of _ "Bij_Nat.to_nat b"], auto
        simp: to_nat_less_card)
  }
  ultimately show ?thesis
    unfolding elements_mat[abs_def] elements_mat_h_def[abs_def] HMA_M_def
    by auto
qed  

lemma HMA_vec_elements[transfer_rule]: "((HMA_V :: ('a Matrix.vec  'a ^ 'n  bool))  ===> (=)) 
  vec_elements vec_elements_h"
proof -
  {
    fix y :: "'a ^ 'n" and i :: nat
    assume i: "i < CARD('n)" 
    hence "from_hmav y $ i  range (vec_nth y)"      
      using to_nat_from_nat_id[OF i] by (auto simp: from_hmav_def)
  }
  moreover
  {
    fix y :: "'a ^ 'n" and a
    have "i. y $h a = from_hmav y $ i  i < CARD('n)"
      unfolding from_hmav_def
      by (rule exI[of _ "Bij_Nat.to_nat a"], auto simp: to_nat_less_card)
  }
  ultimately show ?thesis
    unfolding vec_elements[abs_def] vec_elements_h_def[abs_def] rel_fun_def HMA_V_def
    by auto
qed  
  
lemma norm_bound_elements_mat: "norm_bound A b = ( x  elements_mat A. norm x  b)"
  unfolding norm_bound_def elements_mat by auto

lemma HMA_normbound [transfer_rule]: 
  "((HMA_M :: 'a :: real_normed_field mat  'a ^ 'nc ^ 'nr  bool) ===> (=) ===> (=))
  norm_bound normbound"
  unfolding normbound_def[abs_def] norm_bound_elements_mat[abs_def]
  by (transfer_prover)

lemma HMA_map_matrix [transfer_rule]: 
  "((=) ===> HMA_M ===> HMA_M) map_mat map_matrix"
  unfolding map_vector_def map_matrix_def[abs_def] map_mat_def[abs_def] HMA_M_def from_hmam_def
  by auto

lemma HMA_transpose_matrix [transfer_rule]: 
  "(HMA_M ===> HMA_M) transpose_mat transpose"
  unfolding transpose_mat_def transpose_def HMA_M_def from_hmam_def by auto

lemma HMA_map_vector [transfer_rule]: 
  "((=) ===> HMA_V ===> HMA_V) map_vec map_vector"
  unfolding map_vector_def[abs_def] map_vec_def[abs_def] HMA_V_def from_hmav_def
  by auto

lemma HMA_similar_mat_wit [transfer_rule]: 
  "((HMA_M :: _  'a :: comm_ring_1 ^ 'n ^ 'n  _) ===> HMA_M ===> HMA_M ===> HMA_M ===> (=)) 
  similar_mat_wit similar_matrix_wit"
proof (intro rel_funI, goal_cases)
  case (1 a A b B c C d D)  
  note [transfer_rule] = this
  hence id: "dim_row a = CARD('n)" by (auto simp: HMA_M_def)
  have *: "(c * d = 1m (dim_row a)  d * c = 1m (dim_row a)  a = c * b * d) =
    (C ** D = mat 1  D ** C = mat 1  A = C ** B ** D)" unfolding id
    by (transfer, simp)
  show ?case unfolding similar_mat_wit_def Let_def similar_matrix_wit_def *
    using 1 by (auto simp: HMA_M_def)
qed

lemma HMA_similar_mat [transfer_rule]: 
  "((HMA_M :: _  'a :: comm_ring_1 ^ 'n ^ 'n  _) ===> HMA_M ===> (=)) 
  similar_mat similar_matrix"
proof (intro rel_funI, goal_cases)
  case (1 a A b B)
  note [transfer_rule] = this
  hence id: "dim_row a = CARD('n)" by (auto simp: HMA_M_def)
  {
    fix c d
    assume "similar_mat_wit a b c d" 
    hence "{c,d}  carrier_mat CARD('n) CARD('n)" unfolding similar_mat_wit_def id Let_def by auto
  } note * = this
  show ?case unfolding similar_mat_def similar_matrix_def
    by (transfer, insert *, blast)
qed

lemma HMA_spectrum[transfer_rule]: "(HMA_M ===> (=)) spectrum Spectrum"
  unfolding spectrum_def[abs_def] Spectrum_def[abs_def]
  by transfer_prover

lemma HMA_M_erase_mat[transfer_rule]: "(HMA_M ===> HMA_I ===> HMA_I ===> HMA_M) mat_erase erase_mat" 
  unfolding mat_erase_def[abs_def] erase_mat_def[abs_def]
  by (auto simp: HMA_M_def HMA_I_def from_hmam_def to_nat_from_nat_id intro!: eq_matI)

lemma HMA_M_sum_UNIV[transfer_rule]: 
  "((HMA_I ===> (=)) ===> HMA_T ===> (=)) sum_UNIV_set sum_UNIV_type"
  unfolding rel_fun_def 
proof (clarify, rename_tac f fT n nT)
  fix f and fT :: "'b  'a" and n and nT :: "'b itself" 
  assume f: "x y. HMA_I x y  f x = fT y"
    and n: "HMA_T n nT" 
  let ?f = "from_nat :: nat  'b" 
  let ?t = "to_nat :: 'b  nat" 
  from n[unfolded HMA_T_def] have n: "n = CARD('b)" .
  from to_nat_from_nat_id[where 'a = 'b, folded n]
  have tf: "i < n  ?t (?f i) = i" for i by auto
  have "sum_UNIV_set f n = sum f (?t ` ?f ` {..<n})" 
    unfolding sum_UNIV_set_def
    by (rule arg_cong[of _ _ "sum f"], insert tf, force)
  also have " = sum (f  ?t) (?f ` {..<n})" 
    by (rule sum.reindex, insert tf n, auto simp: inj_on_def)
  also have "?f ` {..<n} = UNIV" 
    using range_to_nat[where 'a = 'b, folded n] by force
  also have "sum (f  ?t) UNIV = sum fT UNIV" 
  proof (rule sum.cong[OF refl])
    fix i :: 'b
    show "(f  ?t) i = fT i" unfolding o_def 
      by (rule f[rule_format], auto simp: HMA_I_def)
  qed
  also have " = sum_UNIV_type fT nT" 
    unfolding sum_UNIV_type_def ..
  finally show "sum_UNIV_set f n = sum_UNIV_type fT nT" .
qed
end

text ‹Setup a method to easily convert theorems from JNF into HMA.›

method transfer_hma uses rule = (
  (fold index_hma_def)?, (* prepare matrix access for transfer *)
  transfer,
  rule rule, 
  (unfold carrier_vec_def carrier_mat_def)?, 
  auto)

text ‹Now it becomes easy to transfer results which are not yet proven in HMA, such as:›

lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
  by (transfer_hma rule: add_mult_distrib_mat_vec)

lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
  by (transfer_hma rule: mult_add_distrib_mat_vec)

lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v (v - w) = M *v v - M *v w"
  by (transfer_hma rule: mult_minus_distrib_mat_vec)

lemma eigen_value_root_charpoly: 
  "eigen_value A k  poly (charpoly (A :: 'a :: field ^ 'n ^ 'n)) k = 0"
  by (transfer_hma rule: eigenvalue_root_char_poly)

lemma finite_spectrum: fixes A :: "'a :: field ^ 'n ^ 'n"
  shows "finite (Collect (eigen_value A))" 
  by (transfer_hma rule: card_finite_spectrum(1)[unfolded spectrum_def])

lemma non_empty_spectrum: fixes A :: "complex ^ 'n ^ 'n"
  shows "Collect (eigen_value A)  {}"
  by (transfer_hma rule: spectrum_non_empty[unfolded spectrum_def])

lemma charpoly_transpose: "charpoly (transpose A :: 'a :: field ^ 'n ^ 'n) = charpoly A"
  by (transfer_hma rule: char_poly_transpose_mat)

lemma eigen_value_transpose: "eigen_value (transpose A :: 'a :: field ^ 'n ^ 'n) v = eigen_value A v" 
  unfolding eigen_value_root_charpoly charpoly_transpose by simp

lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: ring_1 ^ 'n)"
  by (transfer_hma rule: minus_mult_distrib_mat_vec)

lemma similar_matrix_charpoly: "similar_matrix A B  charpoly A = charpoly B" 
  by (transfer_hma rule: char_poly_similar)

lemma pderiv_char_poly_erase_mat: fixes A :: "'a :: idom ^ 'n ^ 'n" 
  shows "monom 1 1 * pderiv (charpoly A) = sum (λ i. charpoly (erase_mat A i i)) UNIV" 
proof -
  let ?A = "from_hmam A" 
  let ?n = "CARD('n)" 
  have tA[transfer_rule]: "HMA_M ?A A" unfolding HMA_M_def by simp
  have tN[transfer_rule]: "HMA_T ?n TYPE('n)" unfolding HMA_T_def by simp
  have A: "?A  carrier_mat ?n ?n" unfolding from_hmam_def by auto
  have id: "sum (λ i. charpoly (erase_mat A i i)) UNIV = 
    sum_UNIV_type (λ i. charpoly (erase_mat A i i)) TYPE('n)"
    unfolding sum_UNIV_type_def ..
  show ?thesis unfolding id
    by (transfer, insert pderiv_char_poly_mat_erase[OF A], simp add: sum_UNIV_set_def)
qed

lemma degree_monic_charpoly: fixes A :: "'a :: comm_ring_1 ^ 'n ^ 'n" 
  shows "degree (charpoly A) = CARD('n)  monic (charpoly A)" 
proof (transfer, goal_cases)
  case 1
  from degree_monic_char_poly[OF 1] show ?case by auto
qed

end

Theory Perron_Frobenius_Aux

(* Author: Thiemann *)
section ‹Perron-Frobenius Theorem›

subsection ‹Auxiliary Notions›

text ‹We define notions like non-negative real-valued matrix, both
  in JNF and in HMA. These notions will be linked via HMA-connect.›

theory Perron_Frobenius_Aux
imports HMA_Connect
begin

definition real_nonneg_mat :: "complex mat  bool" where
  "real_nonneg_mat A   a  elements_mat A. a    Re a  0"

definition real_nonneg_vec :: "complex Matrix.vec  bool" where
  "real_nonneg_vec v   a  vec_elements v. a    Re a  0"

definition real_non_neg_vec :: "complex ^ 'n  bool" where
  "real_non_neg_vec v  ( a  vec_elements_h v. a    Re a  0)" 

definition real_non_neg_mat :: "complex ^ 'nr ^ 'nc  bool" where
  "real_non_neg_mat A  ( a  elements_mat_h A. a    Re a  0)" 

lemma real_non_neg_matD: assumes "real_non_neg_mat A"
  shows "A $h i $h j  " "Re (A $h i $h j)  0" 
  using assms unfolding real_non_neg_mat_def elements_mat_h_def by auto

definition nonneg_mat :: "'a :: linordered_idom mat  bool" where
  "nonneg_mat A   a  elements_mat A. a  0"

definition non_neg_mat :: "'a :: linordered_idom ^ 'nr ^ 'nc  bool" where
  "non_neg_mat A  ( a  elements_mat_h A. a  0)" 


context includes lifting_syntax
begin

lemma HMA_real_non_neg_mat [transfer_rule]:
  "((HMA_M :: complex mat  complex ^ 'nc ^ 'nr  bool) ===> (=)) 
  real_nonneg_mat real_non_neg_mat"
  unfolding real_nonneg_mat_def[abs_def] real_non_neg_mat_def[abs_def]
  by transfer_prover

lemma HMA_real_non_neg_vec [transfer_rule]:
  "((HMA_V :: complex Matrix.vec  complex ^ 'n  bool) ===> (=)) 
  real_nonneg_vec real_non_neg_vec"
  unfolding real_nonneg_vec_def[abs_def] real_non_neg_vec_def[abs_def]
  by transfer_prover

lemma HMA_non_neg_mat [transfer_rule]:
  "((HMA_M :: 'a :: linordered_idom mat  'a ^ 'nc ^ 'nr  bool) ===> (=)) 
  nonneg_mat non_neg_mat"
  unfolding nonneg_mat_def[abs_def] non_neg_mat_def[abs_def]
  by transfer_prover

end

primrec matpow :: "'a::semiring_1^'n^'n  nat  'a^'n^'n" where
  matpow_0:   "matpow A 0 = mat 1" |
  matpow_Suc: "matpow A (Suc n) = (matpow A n) ** A"

context includes lifting_syntax
begin  
lemma HMA_pow_mat[transfer_rule]:
  "((HMA_M ::'a::{semiring_1} mat  'a^'n^'n  bool) ===> (=) ===> HMA_M) pow_mat matpow"
proof -
  {
    fix A :: "'a mat" and A' :: "'a^'n^'n" and n :: nat
    assume [transfer_rule]: "HMA_M A A'"
    hence [simp]: "dim_row A = CARD('n)" unfolding HMA_M_def by simp
    have "HMA_M (pow_mat A n) (matpow A' n)"
    proof (induct n)
      case (Suc n)
      note [transfer_rule] = this
      show ?case by (simp, transfer_prover)
    qed (simp, transfer_prover)
  }
  thus ?thesis by blast
qed
end

lemma trancl_image: 
  "(i,j)  R+  (f i, f j)  (map_prod f f ` R)+" 
proof (induct rule: trancl_induct)
  case (step j k)
  from step(2) have "(f j, f k)  map_prod f f ` R" by auto
  from step(3) this show ?case by auto
qed auto

lemma inj_trancl_image: assumes inj: "inj f" 
  shows "(f i, f j)  (map_prod f f ` R)+ = ((i,j)  R+)" (is "?l = ?r")
proof
  assume ?r from trancl_image[OF this] show ?l .
next
  assume ?l from trancl_image[OF this, of "the_inv f"]
  show ?r unfolding image_image prod.map_comp o_def the_inv_f_f[OF inj] by auto
qed  

lemma matrix_add_rdistrib: "((B + C) ** A) = (B ** A) + (C ** A)"
  by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)

lemma norm_smult: "norm ((a :: real) *s x) = abs a * norm x" 
  unfolding norm_vec_def 
  by (metis norm_scaleR norm_vec_def scalar_mult_eq_scaleR)

lemma nonneg_mat_mult: 
  "nonneg_mat A  nonneg_mat B  A  carrier_mat nr n
   B  carrier_mat n nc  nonneg_mat (A * B)" 
  unfolding nonneg_mat_def
  by (auto simp: elements_mat_def scalar_prod_def intro!: sum_nonneg)

lemma nonneg_mat_power: assumes "A  carrier_mat n n" "nonneg_mat A" 
  shows "nonneg_mat (A ^m k)"
proof (induct k)
  case 0
  thus ?case by (auto simp: nonneg_mat_def)
next
  case (Suc k)
  from nonneg_mat_mult[OF this assms(2) _ assms(1), of n] assms(1)
  show ?case by auto
qed

lemma nonneg_matD: assumes "nonneg_mat A"
  and "i < dim_row A" and "j < dim_col A"
shows "A $$ (i,j)  0"
  using assms unfolding nonneg_mat_def elements_mat by auto

lemma (in comm_ring_hom) similar_mat_wit_hom: assumes
  "similar_mat_wit A B C D"
shows "similar_mat_wit (math A) (math B) (math C) (math D)"
proof -
  obtain n where n: "n = dim_row A" by auto
  note * = similar_mat_witD[OF n assms]
  from * have [simp]: "dim_row C = n" by auto
  note C = *(6) note D = *(7)
  note id = mat_hom_mult[OF C D] mat_hom_mult[OF D C]
  note ** = *(1-3)[THEN arg_cong[of _ _ "math"], unfolded id]
  note mult = mult_carrier_mat[of _ n n]
  note hom_mult = mat_hom_mult[of _ n n _ n]
  show ?thesis unfolding similar_mat_wit_def Let_def unfolding **(3) using **(1,2)
    by (auto simp: n[symmetric] hom_mult simp: *(4-) mult)
qed

lemma (in comm_ring_hom) similar_mat_hom:
  "similar_mat A B  similar_mat (math A) (math B)"
  using similar_mat_wit_hom[of A B C D for C D]
  by (smt similar_mat_def)

lemma det_dim_1: assumes A: "A  carrier_mat n n"
  and n: "n = 1"
shows "Determinant.det A = A $$ (0,0)"
  by (subst laplace_expansion_column[OF A[unfolded n], of 0], insert A n,
    auto simp: cofactor_def mat_delete_def)

lemma det_dim_2: assumes A: "A  carrier_mat n n"
  and n: "n = 2"
shows "Determinant.det A = A $$ (0,0) * A $$ (1,1) - A $$ (0,1) * A $$ (1,0)"
proof -
  have set: "(i<(2 :: nat). f i) = f 0 + f 1" for f
    by (subst sum.cong[of _ "{0,1}" f f], auto)
  show ?thesis
    apply (subst laplace_expansion_column[OF A[unfolded n], of 0], insert A n,
      auto simp: cofactor_def mat_delete_def set)
    apply (subst (1 2) det_dim_1, auto)
    done
qed


lemma jordan_nf_root_char_poly: fixes A :: "'a :: {semiring_no_zero_divisors, idom} mat"
  assumes "jordan_nf A n_as" 
  and "(m, lam)  set n_as" 
shows "poly (char_poly A) lam = 0" 
proof -
  from assms have m0: "m  0" unfolding jordan_nf_def by force
  from split_list[OF assms(2)] obtain as bs where nas: "n_as = as @ (m, lam) # bs" by auto
  show ?thesis using m0
    unfolding jordan_nf_char_poly[OF assms(1)] nas poly_prod_list prod_list_zero_iff by (auto simp: o_def)
qed

lemma inverse_power_tendsto_zero:
  "(λx. inverse ((of_nat x :: 'a :: real_normed_div_algebra) ^ Suc d))  0"
proof (rule filterlim_compose[OF tendsto_inverse_0], 
  intro filterlim_at_infinity[THEN iffD2, of 0] allI impI, goal_cases) 
  case (2 r)
  let ?r = "nat (ceiling r) + 1" 
  show ?case
  proof (intro eventually_sequentiallyI[of ?r], unfold norm_power norm_of_nat)
    fix x
    assume r: "?r  x" 
    hence x1: "real x  1" by auto 
    have "r  real ?r" by linarith
    also have "  x" using r by auto
    also have "  real x ^ Suc d" using x1 by simp
    finally show "r  real x ^ Suc d" .
  qed 
qed simp

lemma inverse_of_nat_tendsto_zero:
  "(λx. inverse (of_nat x :: 'a :: real_normed_div_algebra))  0"
  using inverse_power_tendsto_zero[of 0] by auto

lemma poly_times_exp_tendsto_zero: assumes b: "norm (b :: 'a :: real_normed_field) < 1" 
  shows "(λ x. of_nat x ^ k * b ^ x)  0" 
proof (cases "b = 0")
  case False
  define nla where "nla = norm b" 
  define s where "s = sqrt nla" 
  from b False have nla: "0 < nla" "nla < 1" unfolding nla_def by auto
  hence s: "0 < s" "s < 1" unfolding s_def by auto
  { 
    fix x
    have "s^x * s^x = sqrt (nla ^ (2 * x))"
      unfolding s_def power_add[symmetric] 
      unfolding real_sqrt_power[symmetric] 
      by (rule arg_cong[of _ _ "λ x. sqrt (nla ^ x)"], simp)
    also have " = nla^x" unfolding power_mult real_sqrt_power
      using nla by simp
    finally have "nla^x = s^x * s^x" by simp
  } note nla_s = this
  show "(λx. of_nat x ^ k * b ^ x)  0"        
  proof (rule tendsto_norm_zero_cancel, unfold norm_mult norm_power norm_of_nat nla_def[symmetric] nla_s
       mult.assoc[symmetric])  
    from poly_exp_constant_bound[OF s, of 1 k] obtain p where 
      p: "real x ^ k * s^x  p" for x by (auto simp: ac_simps)              
    have "norm (real x ^ k * s ^ x) = real x ^ k * s^x" for x using s by auto
    with p have p: "norm (real x ^ k * s ^ x)  p" for x by auto
    from s have s: "norm s < 1" by auto
    show "(λx. real x ^ k * s ^ x * s ^ x)  0" 
      by (rule lim_null_mult_left_bounded[OF _ LIMSEQ_power_zero[OF s], of _ p], insert p, auto)
  qed 
next
  case True
  show ?thesis unfolding True
    by (subst tendsto_cong[of _ "λ x. 0"], rule eventually_sequentiallyI[of 1], auto)
qed


lemma (in linorder_topology) tendsto_Min: assumes I: "I  {}" and fin: "finite I"
  shows "(i. i  I  (f i  a i) F)  ((λx. Min ((λ i. f i x) ` I))  
    (Min (a ` I) :: 'a)) F" 
  using fin I
proof (induct rule: finite_induct)
  case (insert i I)
  hence i: "(f i  a i) F" by auto
  show ?case
  proof (cases "I = {}")
    case True
    show ?thesis unfolding True using i by auto
  next
    case False
    have *: "Min (a ` insert i I) = min (a i) (Min (a ` I))" using False insert(1) by auto
    have **: "(λx. Min ((λi. f i x) ` insert i I)) = (λx. min (f i x) (Min ((λi. f i x) ` I)))" 
      using False insert(1) by auto
    have IH: "((λx. Min ((λi. f i x) ` I))  Min (a ` I)) F" 
      using insert(3)[OF insert(4) False] by auto
    show ?thesis unfolding * **
      by (auto intro!: tendsto_min i IH)
  qed
qed simp

lemma tendsto_mat_mult [tendsto_intros]: 
  "(f  a) F  (g  b) F  ((λx. f x ** g x)  a ** b) F" 
  for f :: "'a  'b :: {semiring_1, real_normed_algebra} ^ 'n1 ^ 'n2" 
  unfolding matrix_matrix_mult_def[abs_def] by (auto intro!: tendsto_intros)

lemma tendsto_matpower [tendsto_intros]: "(f  a) F  ((λx. matpow (f x) n)  matpow a n) F"
  for f :: "'a  'b :: {semiring_1, real_normed_algebra} ^ 'n ^ 'n"
  by (induct n, simp_all add: tendsto_mat_mult)

lemma continuous_matpow: "continuous_on R (λ A :: 'a :: {semiring_1, real_normed_algebra_1} ^ 'n ^ 'n. matpow A n)"
  unfolding continuous_on_def by (auto intro!: tendsto_intros)

lemma vector_smult_distrib: "(A *v ((a :: 'a :: comm_ring_1) *s x)) = a *s ((A *v x))" 
  unfolding matrix_vector_mult_def vector_scalar_mult_def
  by (simp add: ac_simps sum_distrib_left)  

instance real :: ordered_semiring_strict
  by (intro_classes, auto)

lemma poly_tendsto_pinfty:  fixes p :: "real poly"
  assumes "lead_coeff p > 0" "degree p  0" 
  shows "poly p  " 
  unfolding Lim_PInfty
proof 
  fix b
  show "N. nN. ereal b  ereal (poly p (real n))" 
    unfolding ereal_less_eq using poly_pinfty_ge[OF assms, of b]
    by (meson of_nat_le_iff order_trans real_arch_simple)
qed

lemma div_lt_nat: "(j :: nat) < x * y  j div x < y" 
  by (simp add: less_mult_imp_div_less mult.commute)


definition diagvector :: "('n  'a :: semiring_0)  'a ^ 'n ^ 'n" where
  "diagvector x = (χ i. χ j. if i = j then x i else 0)" 

lemma diagvector_mult_vector[simp]: "diagvector x *v y = (χ i. x i * y $ i)" 
  unfolding diagvector_def matrix_vector_mult_def vec_eq_iff vec_lambda_beta
proof (rule, goal_cases)
  case (1 i)
  show ?case by (subst sum.remove[of _ i], auto)
qed

lemma diagvector_mult_left: "diagvector x ** A = (χ i j. x i * A $ i $ j)" (is "?A = ?B") 
  unfolding vec_eq_iff
proof (intro allI)
  fix i j
  show "?A $h i $h j = ?B $h i $h j" 
    unfolding map_vector_def diagvector_def matrix_matrix_mult_def vec_lambda_beta
    by (subst sum.remove[of _ i], auto)
qed

lemma diagvector_mult_right: "A ** diagvector x = (χ i j. A $ i $ j * x j)" (is "?A = ?B") 
  unfolding vec_eq_iff
proof (intro allI)
  fix i j
  show "?A $h i $h j = ?B $h i $h j" 
    unfolding map_vector_def diagvector_def matrix_matrix_mult_def vec_lambda_beta
    by (subst sum.remove[of _ j], auto)
qed

lemma diagvector_mult[simp]: "diagvector x ** diagvector y = diagvector (λ i. x i * y i)" 
  unfolding diagvector_mult_left unfolding diagvector_def by (auto simp: vec_eq_iff)

lemma diagvector_const[simp]: "diagvector (λ x. k) = mat k" 
  unfolding diagvector_def mat_def by auto

lemma diagvector_eq_mat: "diagvector x = mat a  x = (λ x. a)" 
  unfolding diagvector_def mat_def by (auto simp: vec_eq_iff)

lemma cmod_eq_Re: assumes "cmod x = Re x"
  shows "of_real (Re x) = x" 
proof (cases "Im x = 0")
  case False
  hence "(cmod x)^2  (Re x)^2" unfolding norm_complex_def by simp
  from this[unfolded assms] show ?thesis by auto
qed (cases x, auto simp: norm_complex_def complex_of_real_def)

hide_fact (open) Matrix.vec_eq_iff

no_notation
  vec_index (infixl "$" 100)

lemma spectral_radius_ev:
  " ev v. eigen_vector A v ev  norm ev = spectral_radius A"
proof -
  from non_empty_spectrum[of A] finite_spectrum[of A] have
    "spectral_radius A  norm ` (Collect (eigen_value A))"
    unfolding spectral_radius_ev_def by auto
  thus ?thesis unfolding eigen_value_def[abs_def] by auto
qed

lemma spectral_radius_max: assumes "eigen_value A v"
  shows "norm v  spectral_radius A"
proof -
  from assms have "norm v  norm ` (Collect (eigen_value A))" by auto
  from Max_ge[OF _ this, folded spectral_radius_ev_def]
    finite_spectrum[of A] show ?thesis by auto
qed

text ‹For Perron-Frobenius it is useful to use the linear norm, and
  not the Euclidean norm.›

definition norm1 :: "'a :: real_normed_field ^ 'n  real" where
  "norm1 v = (iUNIV. norm (v $ i))"

lemma norm1_ge_0: "norm1 v  0" unfolding norm1_def
  by (rule sum_nonneg, auto)

lemma norm1_0[simp]: "norm1 0 = 0" unfolding norm1_def by auto

lemma norm1_nonzero: assumes "v  0"
  shows "norm1 v > 0"
proof -
  from v  0 obtain i where vi: "v $ i  0" unfolding vec_eq_iff
    using Finite_Cartesian_Product.vec_eq_iff zero_index by force
  have "sum (λ i. norm (v $ i)) (UNIV - {i})  0"
    by (rule sum_nonneg, auto)
  moreover have "norm (v $ i) > 0" using vi by auto
  ultimately
  have "0 < norm (v $ i) + sum (λ i. norm (v $ i)) (UNIV - {i})" by arith
  also have " = norm1 v" unfolding norm1_def
    by (simp add: sum.remove)
  finally show "norm1 v > 0" .
qed

lemma norm1_0_iff[simp]: "(norm1 v = 0) = (v = 0)"
  using norm1_0 norm1_nonzero by (cases "v = 0", force+)

lemma norm1_scaleR[simp]: "norm1 (r *R v) = abs r * norm1 v" unfolding norm1_def sum_distrib_left
  by (rule sum.cong, auto)

lemma abs_norm1[simp]: "abs (norm1 v) = norm1 v" using norm1_ge_0[of v] by arith

lemma normalize_eigen_vector: assumes "eigen_vector (A :: 'a :: real_normed_field ^ 'n ^ 'n) v ev"
  shows "eigen_vector A ((1 / norm1 v) *R v) ev" "norm1 ((1 / norm1 v) *R v) = 1"
proof -
  let ?v = "(1 / norm1 v) *R v"
  from assms[unfolded eigen_vector_def]
  have nz: "v  0" and id: "A *v v = ev *s v" by auto
  from nz have norm1: "norm1 v  0" by auto
  thus "norm1 ?v = 1" by simp
  from norm1 nz have nz: "?v  0" by auto
  have "A *v ?v = (1 / norm1 v) *R (A *v v)"
    by (auto simp: vec_eq_iff matrix_vector_mult_def real_vector.scale_sum_right)
  also have "A *v v = ev *s v" unfolding id ..
  also have "(1 / norm1 v) *R (ev *s v) = ev *s ?v"
    by (auto simp: vec_eq_iff)
  finally show "eigen_vector A ?v ev" using nz unfolding eigen_vector_def by auto
qed


lemma norm1_cont[simp]: "isCont norm1 v" unfolding norm1_def[abs_def] by auto

lemma norm1_ge_norm: "norm1 v  norm v" unfolding norm1_def norm_vec_def
  by (rule L2_set_le_sum, auto)

text ‹The following continuity lemmas have been proven with hints from Fabian Immler.›

lemma tendsto_matrix_vector_mult[tendsto_intros]:
  "((*v) (A :: 'a :: real_normed_algebra_1 ^ 'n ^ 'k)  A *v v) (at v within S)"
  unfolding matrix_vector_mult_def[abs_def]
  by (auto intro!: tendsto_intros)

lemma tendsto_matrix_matrix_mult[tendsto_intros]:
  "((**) (A :: 'a :: real_normed_algebra_1 ^ 'n ^ 'k)  A ** B) (at B within S)"
  unfolding matrix_matrix_mult_def[abs_def]
  by (auto intro!: tendsto_intros)

lemma matrix_vect_scaleR: "(A :: 'a :: real_normed_algebra_1 ^ 'n ^ 'k) *v (a *R v) = a *R (A *v v)"
  unfolding vec_eq_iff
  by (auto simp: matrix_vector_mult_def scaleR_vec_def scaleR_sum_right
  intro!: sum.cong)

lemma (in inj_semiring_hom) map_vector_0: "(map_vector hom v = 0) = (v = 0)"
  unfolding vec_eq_iff map_vector_def by auto

lemma (in inj_semiring_hom) map_vector_inj: "(map_vector hom v = map_vector hom w) = (v = w)"
  unfolding vec_eq_iff map_vector_def by auto

lemma (in semiring_hom) matrix_vector_mult_hom:
  "(map_matrix hom A) *v (map_vector hom v) = map_vector hom (A *v v)"
  by (transfer fixing: hom, auto simp: mult_mat_vec_hom)

lemma (in semiring_hom) vector_smult_hom:
  "hom x *s (map_vector hom v) = map_vector hom (x *s v)"
  by (transfer fixing: hom, auto simp: vec_hom_smult)

lemma (in inj_comm_ring_hom) eigen_vector_hom: 
  "eigen_vector (map_matrix hom A) (map_vector hom v) (hom x) = eigen_vector A v x"
  unfolding eigen_vector_def matrix_vector_mult_hom vector_smult_hom map_vector_0 map_vector_inj 
  by auto

end

Theory Perron_Frobenius

(* Author: R. Thiemann *)

subsection ‹Perron-Frobenius theorem via Brouwer's fixpoint theorem.›

theory Perron_Frobenius
imports
  "HOL-Analysis.Brouwer_Fixpoint"
  Perron_Frobenius_Aux
begin

text ‹We follow the textbook proof of Serre \cite[Theorem 5.2.1]{SerreMatrices}.›

context
  fixes A :: "complex ^ 'n ^ 'n :: finite"
  assumes rnnA: "real_non_neg_mat A"
begin

private abbreviation(input) sr where "sr  spectral_radius A"

private definition max_v_ev :: "(complex^'n) × complex" where
  "max_v_ev = (SOME v_ev. eigen_vector A (fst v_ev) (snd v_ev)
   norm (snd v_ev) = sr)"

private definition "max_v = (1 / norm1 (fst max_v_ev)) *R fst max_v_ev"
private definition "max_ev = snd max_v_ev"

private lemma max_v_ev:
  "eigen_vector A max_v max_ev"
  "norm max_ev = sr"
  "norm1 max_v = 1"
proof -
  obtain v ev where id: "max_v_ev = (v,ev)" by force
  from spectral_radius_ev[of A] someI_ex[of "λ v_ev. eigen_vector A (fst v_ev) (snd v_ev)
   norm (snd v_ev) = sr", folded max_v_ev_def, unfolded id]
  have v: "eigen_vector A v ev" and ev: "norm ev = sr" by auto
  from normalize_eigen_vector[OF v] ev
  show "eigen_vector A max_v max_ev" "norm max_ev = sr" "norm1 max_v = 1"
    unfolding max_v_def max_ev_def id by auto
qed

text ‹In the definition of S, we use the linear norm instead of the
  default euclidean norm which is defined via the type-class.
  The reason is that S is not convex if one uses the euclidean norm.›

private definition B :: "real ^ 'n ^ 'n" where "B  χ i j. Re (A $ i $ j)"
private definition S where "S = {v :: real ^ 'n . norm1 v = 1  ( i. v $ i  0) 
  ( i. (B *v v) $ i  sr * (v $ i))}"
private definition f :: "real ^ 'n  real ^ 'n" where
  "f v = (1 / norm1 (B *v v)) *R (B *v v)"

private lemma closedS: "closed S"
  unfolding S_def matrix_vector_mult_def[abs_def]
proof (intro closed_Collect_conj closed_Collect_all closed_Collect_le closed_Collect_eq)
  show "continuous_on UNIV norm1"
    by (simp add: continuous_at_imp_continuous_on)
qed (auto intro!: continuous_intros continuous_on_component)

private lemma boundedS: "bounded S"
proof -
  {
    fix v :: "real ^ 'n"
    from norm1_ge_norm[of v] have "norm1 v = 1  norm v  1" by auto
  }
  thus ?thesis
  unfolding S_def bounded_iff
  by (auto intro!: exI[of _ 1])
qed

private lemma compactS: "compact S"
  using boundedS closedS
  by (simp add: compact_eq_bounded_closed)

private lemmas rnn = real_non_neg_matD[OF rnnA]

lemma B_norm: "B $ i $ j = norm (A $ i $ j)"
  using rnn[of i j]
  by (cases "A $ i $ j", auto simp: B_def)

lemma mult_B_mono: assumes " i. v $ i  w $ i"
  shows "(B *v v) $ i  (B *v w) $ i" unfolding matrix_vector_mult_def vec_lambda_beta
  by (rule sum_mono, rule mult_left_mono[OF assms], unfold B_norm, auto)


private lemma non_emptyS: "S  {}"
proof -
  let ?v = "(χ i. norm (max_v $ i)) :: real ^ 'n"
  have "norm1 max_v = 1" by (rule max_v_ev(3))
  hence nv: "norm1 ?v = 1" unfolding norm1_def by auto
  {
    fix i
    have "sr * (?v $ i) = sr * norm (max_v $ i)" by auto
    also have " = (norm max_ev) * norm (max_v $ i)" using max_v_ev by auto
    also have " = norm ((max_ev *s max_v) $ i)" by (auto simp: norm_mult)
    also have "max_ev *s max_v = A *v max_v" using max_v_ev(1)[unfolded eigen_vector_def] by auto
    also have "norm ((A *v max_v) $ i)  (B *v ?v) $ i"
      unfolding matrix_vector_mult_def vec_lambda_beta
      by (rule sum_norm_le, auto simp: norm_mult B_norm)
    finally have "sr * (?v $ i)  (B *v ?v) $ i" .
  } note le = this
  have "?v  S" unfolding S_def using nv le by auto
  thus ?thesis by blast
qed

private lemma convexS: "convex S"
proof (rule convexI)
  fix v w a b
  assume *: "v  S" "w  S" "0  a" "0  b" "a + b = (1 :: real)"
  let ?lin = "a *R v + b *R w"
  from * have 1: "norm1 v = 1" "norm1 w = 1" unfolding S_def by auto
  have "norm1 ?lin = a * norm1 v + b * norm1 w"
    unfolding norm1_def sum_distrib_left sum.distrib[symmetric]
  proof (rule sum.cong)
    fix i :: 'n
    from * have "v $ i  0" "w $ i  0" unfolding S_def by auto
    thus "norm (?lin $ i) = a * norm (v $ i) + b * norm (w $ i)"
      using *(3-4) by auto
  qed simp
  also have " = 1" using *(5) 1 by auto
  finally have norm1: "norm1 ?lin = 1" .
  {
    fix i
    from * have "0  v $ i" "sr * v $ i  (B *v v) $ i" unfolding S_def by auto
    with a  0 have a: "a * (sr * v $ i)  a * (B *v v) $ i" by (intro mult_left_mono)
    from * have "0  w $ i" "sr * w $ i  (B *v w) $ i" unfolding S_def by auto
    with b  0 have b: "b * (sr * w $ i)  b * (B *v w) $ i" by (intro mult_left_mono)
    from a b have "a * (sr * v $ i) + b * (sr * w $ i)  a * (B *v v) $ i + b * (B *v w) $ i" by auto
  } note le = this
  have switch[simp]: " x y. x * a * y = a * x * y"  " x y. x * b * y = b * x * y" by auto
  have [simp]: "x  {v,w}  a * (r * x $h i) = r * (a * x $h i)" for a r i x by auto
  show "a *R v + b *R w  S" using * norm1 le unfolding S_def
    by (auto simp: matrix_vect_scaleR matrix_vector_right_distrib ring_distribs)
qed

private abbreviation (input) r :: "real  complex" where
  "r  of_real"

private abbreviation rv :: "real ^'n  complex ^'n" where
  "rv v  χ i. r (v $ i)"

private lemma rv_0: "(rv v = 0) = (v = 0)"
  by (simp add: of_real_hom.map_vector_0 map_vector_def vec_eq_iff)

private lemma rv_mult: "A *v rv v = rv (B *v v)"
proof -
  have "map_matrix r B = A"
    using rnnA unfolding map_matrix_def B_def real_non_neg_mat_def map_vector_def elements_mat_h_def
    by vector
  thus ?thesis
    using of_real_hom.matrix_vector_mult_hom[of B, where 'a = complex]
    unfolding map_vector_def by auto
qed

context
  assumes zero_no_ev: " v. v  S  A *v rv v  0"
begin
private lemma normB_S: assumes v: "v  S"
  shows "norm1 (B *v v)  0"
proof -
  from zero_no_ev[OF v, unfolded rv_mult rv_0]
  show ?thesis by auto
qed

private lemma image_f: "f ` S  S"
proof -
  {
    fix v
    assume v: "v  S"
    hence norm: "norm1 v = 1" and ge: " i. v $ i  0" " i. sr * v $ i  (B *v v) $ i" unfolding S_def by auto
    from normB_S[OF v] have normB: "norm1 (B *v v) > 0" using norm1_nonzero by auto
    have fv: "f v = (1 / norm1 (B *v v)) *R (B *v v)" unfolding f_def by auto
    from normB have Bv0: "B *v v  0" unfolding norm1_0_iff[symmetric] by linarith
    have norm: "norm1 (f v) = 1" unfolding fv using normB Bv0 by simp
    define c where "c = (1 / norm1 (B *v v))"
    have c: "c > 0" unfolding c_def using normB by auto
    {
      fix i
      have 1: "f v $ i  0" unfolding fv c_def[symmetric] using c ge
        by (auto simp: matrix_vector_mult_def sum_distrib_left B_norm intro!: sum_nonneg)
      have id1: " i. (B *v f v) $ i = c * ((B *v (B *v v)) $ i)"
        unfolding f_def c_def matrix_vect_scaleR by simp
      have id3: " i. sr * f v $ i = c * ((B *v (sr *R v)) $ i)"
        unfolding f_def c_def[symmetric] matrix_vect_scaleR by auto
      have 2: "sr * f v $ i  (B *v f v) $ i" unfolding id1 id3
        unfolding mult_le_cancel_iff2[OF c > 0]
        by (rule mult_B_mono, insert ge(2), auto)
      note 1 2
    }
    with norm have "f v  S" unfolding S_def by auto
  }
  thus ?thesis by blast
qed

private lemma cont_f: "continuous_on S f"
  unfolding f_def[abs_def] continuous_on using normB_S
  unfolding norm1_def
  by (auto intro!: tendsto_eq_intros)

qualified lemma perron_frobenius_positive_ev:
  " v. eigen_vector A v (r sr)  real_non_neg_vec v"
proof -
  from brouwer[OF compactS convexS non_emptyS cont_f image_f]
    obtain v where v: "v  S" and fv: "f v = v" by auto
  define ev where "ev = norm1 (B *v v)"
  from normB_S[OF v] have "ev  0" unfolding ev_def by auto
  with norm1_ge_0[of "B *v v", folded ev_def] have norm: "ev > 0" by auto
  from arg_cong[OF fv[unfolded f_def], of "λ (w :: real ^ 'n). ev *R w"] norm
  have ev: "B *v v = ev *s v" unfolding ev_def[symmetric] scalar_mult_eq_scaleR by simp
  with v[unfolded S_def] have ge: " i. sr * v $ i  ev * v $ i" by auto
  have "A *v rv v = rv (B *v v)" unfolding rv_mult ..
  also have " = ev *s rv v" unfolding ev vec_eq_iff
    by (simp add: scaleR_conv_of_real scaleR_vec_def)
  finally have ev: "A *v rv v = ev *s rv v" .
  from v have v0: "v  0" unfolding S_def by auto
  hence "rv v  0" unfolding rv_0 .
  with ev have ev: "eigen_vector A (rv v) ev" unfolding eigen_vector_def by auto
  hence "eigen_value A ev" unfolding eigen_value_def by auto
  from spectral_radius_max[OF this] have le: "norm (r ev)  sr" .
  from v0 obtain i where "v $ i  0" unfolding vec_eq_iff by auto
  from v have "v $ i  0" unfolding S_def by auto
  with v $ i  0 have "v $ i > 0" by auto
  with ge[of i] have ge: "sr  ev" by auto
  with le have sr: "r sr = ev" by auto
  from v have *: "real_non_neg_vec (rv v)" unfolding S_def real_non_neg_vec_def vec_elements_h_def by auto
  show ?thesis unfolding sr
    by (rule exI[of _ "rv v"], insert * ev norm, auto)
qed
end

qualified lemma perron_frobenius_both:
  " v. eigen_vector A v (r sr)  real_non_neg_vec v"
proof (cases " v  S. A *v rv v  0")
  case True
  show ?thesis
    by (rule Perron_Frobenius.perron_frobenius_positive_ev[OF rnnA], insert True, auto)
next
  case False
  then obtain v where v: "v  S" and A0: "A *v rv v = 0" by auto
  hence id: "A *v rv v = 0 *s rv v" and v0: "v  0" unfolding S_def by auto
  from v0 have "rv v  0" unfolding rv_0 .
  with id have ev: "eigen_vector A (rv v) 0" unfolding eigen_vector_def by auto
  hence "eigen_value A 0" unfolding eigen_value_def ..
  from spectral_radius_max[OF this] have 0: "0  sr" by auto
  from v[unfolded S_def] have ge: " i. sr * v $ i  (B *v v) $ i" by auto
  from v[unfolded S_def] have rnn: "real_non_neg_vec (rv v)"
    unfolding real_non_neg_vec_def vec_elements_h_def by auto
  from v0 obtain i where "v $ i  0" unfolding vec_eq_iff by auto
  from v have "v $ i  0" unfolding S_def by auto
  with v $ i  0 have vi: "v $ i > 0" by auto
  from rv_mult[of v, unfolded A0] have "rv (B *v v) = 0" by simp
  hence "B *v v = 0" unfolding rv_0 .
  from ge[of i, unfolded this] vi have ge: "sr  0" by (simp add: mult_le_0_iff)
  with 0  sr› have "sr = 0" by auto
  show ?thesis unfolding ‹sr = 0 using rnn ev by auto
qed
end

text ‹Perron Frobenius: The largest complex eigenvalue of a real-valued non-negative matrix
  is a real one, and it has a real-valued non-negative eigenvector.›

lemma perron_frobenius:
  assumes "real_non_neg_mat A"
  shows "v. eigen_vector A v (of_real (spectral_radius A))  real_non_neg_vec v"
  by (rule Perron_Frobenius.perron_frobenius_both[OF assms])

text ‹And a version which ignores the eigenvector.›

lemma perron_frobenius_eigen_value:
  assumes "real_non_neg_mat A"
  shows "eigen_value A (of_real (spectral_radius A))"
  using perron_frobenius[OF assms] unfolding eigen_value_def by blast

end

Theory Roots_Unity

(* author: Thiemann *)

section ‹Roots of Unity›

theory Roots_Unity
imports
  Polynomial_Factorization.Order_Polynomial
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
  Polynomial_Interpolation.Ring_Hom_Poly
begin

lemma cis_mult_cmod_id: "cis (arg x) * of_real (cmod x) = x"
  using rcis_cmod_arg[unfolded rcis_def] by (simp add: ac_simps)

lemma rcis_mult_cis[simp]: "rcis n a * cis b = rcis n (a + b)" unfolding cis_rcis_eq rcis_mult by simp
lemma rcis_div_cis[simp]: "rcis n a / cis b = rcis n (a - b)" unfolding cis_rcis_eq rcis_divide by simp

lemma cis_plus_2pi[simp]: "cis (x + 2 * pi) = cis x" by (auto simp: complex_eq_iff)
lemma cis_plus_2pi_neq_1: assumes x: "0 < x" "x < 2 * pi"
  shows "cis x  1"
proof -
  from x have "cos x  1" by (smt cos_2pi_minus cos_monotone_0_pi cos_zero)
  thus ?thesis by (auto simp: complex_eq_iff)
qed

lemma cis_times_2pi[simp]: "cis (of_nat n * 2 * pi) = 1"
proof (induct n)
  case (Suc n)
  have "of_nat (Suc n) * 2 * pi = of_nat n * 2 * pi + 2 * pi" by (simp add: distrib_right)
  also have "cis  = 1" unfolding cis_plus_2pi Suc ..
  finally show ?case .
qed simp

declare cis_pi[simp]

lemma cis_pi_2[simp]: "cis (pi / 2) = 𝗂"
  by (auto simp: complex_eq_iff)

lemma cis_add_pi[simp]: "cis (pi + x) = - cis x"
  by (auto simp: complex_eq_iff)

lemma cis_3_pi_2[simp]: "cis (pi * 3 / 2) = - 𝗂"
proof -
  have "cis (pi * 3 / 2) = cis (pi + pi / 2)"
    by (rule arg_cong[of _ _ cis], simp)
  also have " = - 𝗂" unfolding cis_add_pi by simp
  finally show ?thesis .
qed

lemma rcis_plus_2pi[simp]: "rcis y (x + 2 * pi) = rcis y x" unfolding rcis_def by simp
lemma rcis_times_2pi[simp]: "rcis r (of_nat n * 2 * pi) = of_real r"
  unfolding rcis_def cis_times_2pi by simp

lemma arg_rcis_cis: assumes n: "n > 0" shows "arg (rcis n x) = arg (cis x)"
  using arg_bounded arg_unique cis_arg complex_mod_rcis n rcis_def sgn_eq by auto

lemma arg_eqD: assumes "arg (cis x) = arg (cis y)" "-pi < x" "x  pi" "-pi < y" "y  pi"
  shows "x = y"
  using assms(1) unfolding arg_unique[OF sgn_cis assms(2-3)] arg_unique[OF sgn_cis assms(4-5)] .

lemma rcis_inj_on: assumes r: "r  0" shows "inj_on (rcis r) {0 ..< 2 * pi}"
proof (rule inj_onI, goal_cases)
  case (1 x y)
  from arg_cong[OF 1(3), of "λ x. x / r"] have "cis x = cis y" using r by (simp add: rcis_def)
  from arg_cong[OF this, of "λ x. inverse x"] have "cis (-x) = cis (-y)" by simp
  from arg_cong[OF this, of uminus] have *: "cis (-x + pi) = cis (-y + pi)"
    by (auto simp: complex_eq_iff)
  have "- x + pi = - y + pi"
    by (rule arg_eqD[OF arg_cong[OF *, of arg]], insert 1(1-2), auto)
  thus ?case by simp
qed

lemma cis_inj_on: "inj_on cis {0 ..< 2 * pi}"
  using rcis_inj_on[of 1] unfolding rcis_def by auto

definition root_unity :: "nat  'a :: comm_ring_1 poly" where
  "root_unity n = monom 1 n - 1"

lemma poly_root_unity: "poly (root_unity n) x = 0  x^n = 1"
  unfolding root_unity_def by (simp add: poly_monom)

lemma degree_root_unity[simp]: "degree (root_unity n) = n" (is "degree ?p = _")
proof -
  have p: "?p = monom 1 n + (-1)" unfolding root_unity_def by auto
  show ?thesis
  proof (cases n)
    case 0
    thus ?thesis unfolding p by simp
  next
    case (Suc m)
    show ?thesis unfolding p unfolding Suc
      by (subst degree_add_eq_left, auto simp: degree_monom_eq)
  qed
qed

lemma zero_root_unit[simp]: "root_unity n = 0  n = 0" (is "?p = 0  _")
proof (cases "n = 0")
  case True
  thus ?thesis unfolding root_unity_def by simp
next
  case False
  from degree_root_unity[of n] False
  have "degree ?p  0" by auto
  hence "?p  0" by fastforce
  thus ?thesis using False by auto
qed

definition prod_root_unity :: "nat list  'a :: idom poly" where
  "prod_root_unity ns = prod_list (map root_unity ns)"

lemma poly_prod_root_unity: "poly (prod_root_unity ns) x = 0  (kset ns. x ^ k = 1)"
  unfolding prod_root_unity_def
  by (simp add: poly_prod_list prod_list_zero_iff o_def image_def poly_root_unity)

lemma degree_prod_root_unity[simp]: "0  set ns  degree (prod_root_unity ns) = sum_list ns"
  unfolding prod_root_unity_def
  by (subst degree_prod_list_eq, auto simp: o_def)

lemma zero_prod_root_unit[simp]: "prod_root_unity ns = 0  0  set ns"
  unfolding prod_root_unity_def prod_list_zero_iff by auto

lemma roots_of_unity: assumes n: "n  0"
  shows "(λ i. (cis (of_nat i * 2 * pi / n))) ` {0 ..< n} = { x :: complex. x ^ n = 1}" (is "?prod = ?Roots")
     "{x. poly (root_unity n) x = 0} = { x :: complex. x ^ n = 1}"
     "card { x :: complex. x ^ n = 1} = n"
proof (atomize(full), goal_cases)
  case 1
  let ?one = "1 :: complex"
  let ?p = "monom ?one n - 1"
  have degM: "degree (monom ?one n) = n" by (rule degree_monom_eq, simp)
  have "degree ?p = degree (monom ?one n + (-1))" by simp
  also have " = degree (monom ?one n)"
    by (rule degree_add_eq_left, insert n, simp add: degM)
  finally have degp: "degree ?p = n" unfolding degM .
  with n have p: "?p  0" by auto
  have roots: "?Roots = {x. poly ?p x = 0}"
    unfolding poly_diff poly_monom by simp
  also have "finite " by (rule poly_roots_finite[OF p])
  finally have fin: "finite ?Roots" .
  have sub: "?prod  ?Roots"
  proof
    fix x
    assume "x  ?prod"
    then obtain i where x: "x = cis (real i * 2 * pi / n)" by auto
    have "x ^ n = cis (real i * 2 * pi)" unfolding x DeMoivre using n by simp
    also have " = 1" by simp
    finally show "x  ?Roots" by auto
  qed
  have Rn: "card ?Roots  n" unfolding roots
    by (rule poly_roots_degree[of ?p, unfolded degp, OF p])
  have " = card {0 ..< n}" by simp
  also have " = card ?prod"
  proof (rule card_image[symmetric], rule inj_onI, goal_cases)
    case (1 x y)
    {
      fix m
      assume "m < n"
      hence "real m < real n" by simp
      from mult_strict_right_mono[OF this, of "2 * pi / real n"] n
      have "real m * 2 * pi / real n < real n * 2 * pi / real n" by simp
      hence "real m * 2 * pi / real n < 2 * pi" using n by simp
    } note [simp] = this
    have 0: "(1 :: real)  0" using n by auto
    have "real x * 2 * pi / real n = real y * 2 * pi / real n"
      by (rule inj_onD[OF rcis_inj_on 1(3)[unfolded cis_rcis_eq]], insert 1(1-2), auto)
    with n show "x = y" by auto
  qed
  finally have cn:  "card ?prod = n" ..
  with Rn have "card ?prod  card ?Roots" by auto
  with card_mono[OF fin sub] have card: "card ?prod = card ?Roots" by auto
  have "?prod = ?Roots"
    by (rule card_subset_eq[OF fin sub card])
  from this roots[symmetric] cn[unfolded this]
  show ?case unfolding root_unity_def by blast
qed

lemma poly_roots_dvd: fixes p :: "'a :: field poly"
  assumes "p  0" and "degree p = n"
  and "card {x. poly p x = 0}  n" and "{x. poly p x = 0}  {x. poly q x = 0}"
shows "p dvd q"
proof -
  from poly_roots_degree[OF assms(1)] assms(2-3) have "card {x. poly p x = 0} = n" by auto
  from assms(1-2) this assms(4)
  show ?thesis
  proof (induct n arbitrary: p q)
    case (0 p q)
    from is_unit_iff_degree[OF 0(1)] 0(2) show ?case by blast
  next
    case (Suc n p q)
    let ?P = "{x. poly p x = 0}"
    let ?Q = "{x. poly q x = 0}"
    from Suc(4-5) card_gt_0_iff[of ?P] obtain x where
      x: "poly p x = 0" "poly q x = 0" and fin: "finite ?P" by auto
    define r where "r = [:-x, 1:]"
    from x[unfolded poly_eq_0_iff_dvd r_def[symmetric]] obtain p' q' where
      p: "p = r * p'" and q: "q = r * q'" unfolding dvd_def by auto
    from Suc(2) have "degree p = degree r + degree p'" unfolding p
      by (subst degree_mult_eq, auto)
    with Suc(3) have deg: "degree p' = n" unfolding r_def by auto
    from Suc(2) p have p'0: "p'  0" by auto
    let ?P' = "{x. poly p' x = 0}"
    let ?Q' = "{x. poly q' x = 0}"
    have P: "?P = insert x ?P'" unfolding p poly_mult unfolding r_def by auto
    have Q: "?Q = insert x ?Q'" unfolding q poly_mult unfolding r_def by auto
    {
      assume "x  ?P'"
      hence "?P = ?P'" unfolding P by auto
      from arg_cong[OF this, of card, unfolded Suc(4)] deg have False
        using poly_roots_degree[OF p'0] by auto
    } note xp' = this
    hence xP': "x  ?P'" by auto
    have "card ?P = Suc (card ?P')" unfolding P
      by (rule card_insert_disjoint[OF _ xP'], insert fin[unfolded P], auto)
    with Suc(4) have card: "card ?P' = n" by auto
    from Suc(5)[unfolded P Q] xP' have "?P'  ?Q'" by auto
    from Suc(1)[OF p'0 deg card this]
    have IH: "p' dvd q'" .
    show ?case unfolding p q using IH by simp
  qed
qed

lemma root_unity_decomp: assumes n: "n  0"
  shows "root_unity n =
    prod_list (map (λ i. [:-cis (of_nat i * 2 * pi / n), 1:]) [0 ..< n])" (is "?u = ?p")
proof -
  have deg: "degree ?u = n" by simp
  note main = roots_of_unity[OF n]
  have dvd: "?u dvd ?p"
  proof (rule poly_roots_dvd[OF _ deg])
    show "n  card {x. poly ?u x = 0}" using main by auto
    show "?u  0" using n by auto
    show "{x. poly ?u x = 0}  {x. poly ?p x = 0}"
      unfolding main(2) main(1)[symmetric] poly_prod_list prod_list_zero_iff by auto
  qed
  have deg': "degree ?p = n"
    by (subst degree_prod_list_eq, auto simp: o_def sum_list_triv)
  have mon: "monic ?u" using deg unfolding root_unity_def using n by auto
  have mon': "monic ?p" by (rule monic_prod_list, auto)
  from dvd[unfolded dvd_def] obtain f where puf: "?p = ?u * f" by auto
  have "degree ?p = degree ?u + degree f" using mon' n unfolding puf
    by (subst degree_mult_eq, auto)
  with deg deg' have "degree f = 0" by auto
  from degree0_coeffs[OF this] obtain a where f: "f = [:a:]" by blast
  from arg_cong[OF puf, of lead_coeff] mon mon'
  have "a = 1" unfolding puf f by (cases "a = 0", auto)
  with f have f: "f = 1" by auto
  with puf show ?thesis by auto
qed

lemma order_monic_linear: "order x [:y,1:] = (if y + x = 0 then 1 else 0)"
proof (cases "y + x = 0")
  case True
  hence "poly [:y,1:] x = 0" by simp
  from this[unfolded order_root] have "order x [:y,1:]  0" by auto
  moreover from order_degree[of "[:y,1:]" x] have "order x [:y,1:]  1" by auto
  ultimately show ?thesis unfolding True by auto
next
  case False
  hence "poly [:y,1:] x  0" by auto
  from order_0I[OF this] False show ?thesis by auto
qed

lemma order_root_unity: fixes x :: complex assumes n: "n  0"
  shows "order x (root_unity n) = (if x^n = 1 then 1 else 0)"
  (is "order _ ?u = _")
proof (cases "x^n = 1")
  case False
  with roots_of_unity(2)[OF n] have "poly ?u x  0" by auto
  from False order_0I[OF this] show ?thesis by auto
next
  case True
  let ?phi = "λ i :: nat. i * 2 * pi / n"
  from True roots_of_unity(1)[OF n] obtain i where i: "i < n"
    and x: "x = cis (?phi i)" by force
  from i have n_split: "[0 ..< n] = [0 ..< i] @ i # [Suc i ..< n]"
    by (metis le_Suc_ex less_imp_le_nat not_le_imp_less not_less0 upt_add_eq_append upt_conv_Cons)
  {
    fix j
    assume j: "j < n  j < i" and eq: "cis (?phi i) = cis (?phi j)"
    from inj_onD[OF cis_inj_on eq] i j n have "i = j" by (auto simp: field_simps)
  } note inj = this
  have "order x ?u = 1" unfolding root_unity_decomp[OF n]
    unfolding x n_split using inj
    by (subst order_prod_list, force, fastforce simp: order_monic_linear)
  with True show ?thesis by auto
qed

lemma order_prod_root_unity: assumes 0: "0  set ks"
  shows "order (x :: complex) (prod_root_unity ks) = length (filter (λ k. x^k = 1) ks)"
proof -
  have "order x (prod_root_unity ks) = (kks. order x (root_unity k))"
    unfolding prod_root_unity_def
    by (subst order_prod_list, insert 0, auto simp: o_def)
  also have " = (kks. (if x^k = 1 then 1 else 0))"
    by (rule arg_cong, rule map_cong, insert 0, force, intro order_root_unity, metis)
  also have " = length (filter (λ k. x^k = 1) ks)"
    by (subst sum_list_map_filter'[symmetric], simp add: sum_list_triv)
  finally show ?thesis .
qed

lemma root_unity_witness: fixes xs :: "complex list"
  assumes "prod_list (map (λ x. [:-x,1:]) xs) = monom 1 n - 1"
  shows "x^n = 1  x  set xs"
proof -
  from assms have n0: "n  0" by (cases "n = 0", auto simp: prod_list_zero_iff)
  have "x  set xs  poly (prod_list (map (λ x. [:-x,1:]) xs)) x = 0"
    unfolding poly_prod_list prod_list_zero_iff by auto
  also have "  x^n = 1" using roots_of_unity(2)[OF n0] unfolding assms root_unity_def by auto
  finally show ?thesis by auto
qed

lemma root_unity_explicit: fixes x :: complex
  shows
    "(x ^ 1 = 1)  x = 1"
    "(x ^ 2 = 1)  (x  {1, -1})"
    "(x ^ 3 = 1)  (x  {1, Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)})"
    "(x ^ 4 = 1)  (x  {1, -1, 𝗂, - 𝗂})"
proof -
  show "(x ^ 1 = 1)  x = 1"
    by (subst root_unity_witness[of "[1]"], code_simp, auto)
  show "(x ^ 2 = 1)  (x  {1, -1})"
    by (subst root_unity_witness[of "[1,-1]"], code_simp, auto)
  show "(x ^ 4 = 1)  (x  {1, -1, 𝗂, - 𝗂})"
    by (subst root_unity_witness[of "[1,-1, 𝗂, - 𝗂]"], code_simp, auto)
  have 3: "3 = Suc (Suc (Suc 0))" "1 = [:1:]" by auto
  show "(x ^ 3 = 1)  (x  {1, Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)})"
    by (subst root_unity_witness[of
      "[1, Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)]"],
      auto simp: 3 monom_altdef complex_mult complex_eq_iff)
qed

definition primitive_root_unity :: "nat  'a :: power  bool" where
  "primitive_root_unity k x = (k  0  x^k = 1  ( k' < k. k'  0  x^k'  1))"

lemma primitive_root_unityD: assumes "primitive_root_unity k x"
  shows "k  0" "x^k = 1" "k'  0  x^k' = 1  k  k'"
proof -
  note * = assms[unfolded primitive_root_unity_def]
  from * have **: "k' < k  k'  0  x ^ k'  1" by auto
  show "k  0" "x^k = 1" using * by auto
  show "k'  0  x^k' = 1  k  k'" using ** by force
qed

lemma primitive_root_unity_exists: assumes "k  0" "x ^ k = 1"
  shows " k'. k'  k  primitive_root_unity k' x"
proof -
  let ?P = "λ k. x ^ k = 1  k  0"
  define k' where "k' = (LEAST k. ?P k)"
  from assms have Pk: " k. ?P k" by auto
  from LeastI_ex[OF Pk, folded k'_def]
  have "k'  0" "x ^ k' = 1" by auto
  with not_less_Least[of _ ?P, folded k'_def]
  have "primitive_root_unity k' x" unfolding primitive_root_unity_def by auto
  with primitive_root_unityD(3)[OF this assms]
  show ?thesis by auto
qed

lemma primitive_root_unity_dvd: fixes x :: "complex"
  assumes k: "primitive_root_unity k x"
  shows "x ^ n = 1  k dvd n"
proof
  assume "k dvd n" then obtain j where n: "n = k * j" unfolding dvd_def by auto
  have "x ^ n = (x ^ k) ^ j" unfolding n power_mult by simp
  also have " = 1" unfolding primitive_root_unityD[OF k] by simp
  finally show "x ^ n = 1" .
next
  assume n: "x ^ n = 1"
  note k = primitive_root_unityD[OF k]
  show "k dvd n"
  proof (cases "n = 0")
    case n0: False
    from k(3)[OF n0] n have nk: "n  k" by force
    from roots_of_unity[OF k(1)] k(2) obtain i :: nat where xk: "x = cis (i * 2 * pi / k)"
      and ik: "i < k" by force
    from roots_of_unity[OF n0] n obtain j :: nat where xn: "x = cis (j * 2 * pi / n)"
      and jn: "j < n" by force
    have cop: "coprime i k"
    proof (rule gcd_eq_1_imp_coprime)
      from k(1) have "gcd i k  0" by auto
      from gcd_coprime_exists[OF this] this obtain i' k' g where
        *: "i = i' * g" "k = k' * g" "g  0" and g: "g = gcd i k" by blast
      from *(2) k(1) have k': "k'  0" by auto
      have "x = cis (i * 2 * pi / k)" by fact
      also have "i * 2 * pi / k = i' * 2 * pi / k'" unfolding * using *(3) by auto
      finally have "x ^ k' = 1" by (simp add: DeMoivre k')
      with k(3)[OF k'] have "k'  k" by linarith
      moreover with * k(1) have "g = 1" by auto
      then show "gcd i k = 1" by (simp add: g)
    qed
    from inj_onD[OF cis_inj_on xk[unfolded xn]] n0 k(1) ik jn
    have "j * real k = i * real n" by (auto simp: field_simps)
    hence "real (j * k) = real (i * n)" by simp
    hence eq: "j * k = i * n" by linarith
    with cop show "k dvd n"
      by (metis coprime_commute coprime_dvd_mult_right_iff dvd_triv_right)
  qed auto
qed

lemma primitive_root_unity_simple_computation:
  "primitive_root_unity k x  = (if k = 0 then False else
     x ^ k = 1  ( i  {1 ..< k}. x ^ i  1))"
  unfolding primitive_root_unity_def by auto

lemma primitive_root_unity_explicit: fixes x :: complex
  shows "primitive_root_unity 1 x  x = 1"
    "primitive_root_unity 2 x  x = -1"
    "primitive_root_unity 3 x  (x  {Complex (-1/2) (sqrt 3 / 2), Complex (-1/2) (- sqrt 3 / 2)})"
    "primitive_root_unity 4 x  (x  {𝗂, - 𝗂})"
proof (atomize(full), goal_cases)
  case 1
  {
    fix P :: "nat  bool"
    have *: "{1 ..< 2 :: nat} = {1}" "{1 ..< 3 :: nat} = {1,2}" "{1 ..< 4 :: nat} = {1,2,3}"
      by code_simp+
    have "(i {1 ..< 2}. P i) = P 1" "(i {1 ..< 3}. P i)  P 1  P 2"
      "(i {1 ..< 4}. P i)  P 1  P 2  P 3"
      unfolding * by auto
  } note * = this
  show ?case unfolding primitive_root_unity_simple_computation root_unity_explicit *
    by (auto simp: complex_eq_iff)
qed

function decompose_prod_root_unity_main ::
  "'a :: field poly  nat  nat list × 'a poly" where
  "decompose_prod_root_unity_main p k = (
    if k = 0 then ([], p) else
   let q = root_unity k in if q dvd p then if p = 0 then ([],0) else
     map_prod (Cons k) id (decompose_prod_root_unity_main (p div q) k) else
     decompose_prod_root_unity_main p (k - 1))"
  by pat_completeness auto

termination by (relation "measure (λ (p,k). degree p + k)", auto simp: degree_div_less)

declare decompose_prod_root_unity_main.simps[simp del]

lemma decompose_prod_root_unity_main: fixes p :: "complex poly"
  assumes p: "p = prod_root_unity ks * f"
  and d: "decompose_prod_root_unity_main p k = (ks',g)"
  and f: " x. cmod x = 1  poly f x  0"
  and k: " k'. k' > k  ¬ root_unity k' dvd p"
shows "p = prod_root_unity ks' * f  f = g  set ks = set ks'"
  using d p k
proof (induct p k arbitrary: ks ks' rule: decompose_prod_root_unity_main.induct)
  case (1 p k ks ks')
  note p = 1(4)
  note k = 1(5)
  from k[of "Suc k"] have p0: "p  0" by auto
  hence "p = 0  False" by auto
  note d = 1(3)[unfolded decompose_prod_root_unity_main.simps[of p k] this if_False Let_def]
  from p0[unfolded p] have ks0: "0  set ks" by simp
  from f[of 1] have f0: "f  0" by auto
  note IH = 1(1)[OF _ refl _ p0] 1(2)[OF _ refl]
  show ?case
  proof (cases "k = 0")
    case True
    with p k[unfolded this, of "hd ks"] p0 have "ks = []"
      by (cases ks, auto simp: prod_root_unity_def)
    with d p True show ?thesis by (auto simp: prod_root_unity_def)
  next
    case k0: False
    note IH = IH[OF k0]
    from k0 have "k = 0  False" by auto
    note d = d[unfolded this if_False]
    let ?u = "root_unity k :: complex poly"
    show ?thesis
    proof (cases "?u dvd p")
      case True
      note IH = IH(1)[OF True]
      let ?call = "decompose_prod_root_unity_main (p div ?u) k"
      from True d obtain Ks where rec: "?call = (Ks,g)" and ks': "ks' = (k # Ks)"
        by (cases ?call, auto)
      from True have "?u dvd p  True" by simp
      note d = d[unfolded this if_True rec]
      let ?x = "cis (2 * pi / k)"
      have rt: "poly ?u ?x = 0" unfolding poly_root_unity using cis_times_2pi[of 1]
        by (simp add: DeMoivre)
      with True have "poly p ?x = 0" unfolding dvd_def by auto
      from this[unfolded p] f[of ?x] rt have "poly (prod_root_unity ks) ?x = 0"
        unfolding poly_root_unity by auto
      from this[unfolded poly_prod_root_unity] ks0 obtain k' where k': "k'  set ks"
        and rt: "?x ^ k' = 1" and k'0: "k'  0" by auto
      let ?u' = "root_unity k' :: complex poly"
      from k' rt k'0 have rtk': "poly ?u' ?x = 0" unfolding poly_root_unity by auto
      {
        let ?phi = " k' * (2 * pi / k)"
        assume "k' < k"
        hence "0 < ?phi" "?phi < 2 * pi" using k0 k'0 by (auto simp: field_simps)
        from cis_plus_2pi_neq_1[OF this] rtk'
        have False unfolding poly_root_unity DeMoivre ..
      }
      hence kk': "k  k'" by presburger
      {
        assume "k' > k"
        from k[OF this, unfolded p]
        have "¬ ?u' dvd prod_root_unity ks" using dvd_mult2 by auto
        with k' have False unfolding prod_root_unity_def
          using prod_list_dvd[of ?u' "map root_unity ks"] by auto
      }
      with kk' have kk': "k' = k" by presburger
      with k' have "k  set ks" by auto
      from split_list[OF this] obtain ks1 ks2 where ks: "ks = ks1 @ k # ks2" by auto
      hence "p div ?u = (?u * (prod_root_unity (ks1 @ ks2) * f)) div ?u"
        by (simp add: ac_simps p prod_root_unity_def)
      also have " = prod_root_unity (ks1 @ ks2) * f"
        by (rule nonzero_mult_div_cancel_left, insert k0, auto)
      finally have id: "p div ?u = prod_root_unity (ks1 @ ks2) * f" .
      from d have ks': "ks' = k # Ks" by auto
      have "k < k'  ¬ root_unity k' dvd p div ?u" for k'
        using k[of k'] True by (metis dvd_div_mult_self dvd_mult2)
      from IH[OF rec id this]
      have id: "p div root_unity k = prod_root_unity Ks * f" and
        *: "f = g  set (ks1 @ ks2) = set Ks" by auto
      from arg_cong[OF id, of "λ x. x * ?u"] True
      have "p = prod_root_unity Ks * f * root_unity k" by auto
      thus ?thesis using * unfolding ks ks' by (auto simp: prod_root_unity_def)
    next
      case False
      from d False have "decompose_prod_root_unity_main p (k - 1) = (ks',g)" by auto
      note IH = IH(2)[OF False this p]
      have k: "k - 1 < k'  ¬ root_unity k' dvd p" for k' using False k[of k'] k0
        by (cases "k' = k", auto)
      show ?thesis by (rule IH, insert False k, auto)
    qed
  qed
qed

definition "decompose_prod_root_unity p = decompose_prod_root_unity_main p (degree p)"

lemma decompose_prod_root_unity: fixes p :: "complex poly"
  assumes p: "p = prod_root_unity ks * f"
  and d: "decompose_prod_root_unity p = (ks',g)"
  and f: " x. cmod x = 1  poly f x  0"
  and p0: "p  0"
shows "p = prod_root_unity ks' * f  f = g  set ks = set ks'"
proof (rule decompose_prod_root_unity_main[OF p d[unfolded decompose_prod_root_unity_def] f])
  fix k
  assume deg: "degree p < k"
  hence "degree p < degree (root_unity k)" by simp
  with p0 show "¬ root_unity k dvd p"
    by (simp add: poly_divides_conv0)
qed

lemma (in comm_ring_hom) hom_root_unity: "map_poly hom (root_unity n) = root_unity n"
proof -
  interpret p: map_poly_comm_ring_hom hom ..
  show ?thesis unfolding root_unity_def
    by (simp add: hom_distribs)
qed

lemma (in idom_hom) hom_prod_root_unity: "map_poly hom (prod_root_unity n) = prod_root_unity n"
proof -
  interpret p: map_poly_comm_ring_hom hom ..
  show ?thesis unfolding prod_root_unity_def p.hom_prod_list map_map o_def hom_root_unity ..
qed

lemma (in field_hom) hom_decompose_prod_root_unity_main:
  "decompose_prod_root_unity_main (map_poly hom p) k = map_prod id (map_poly hom)
    (decompose_prod_root_unity_main p k)"
proof (induct p k rule: decompose_prod_root_unity_main.induct)
  case (1 p k)
  let ?h = "map_poly hom"
  let ?p = "?h p"
  let ?u = "root_unity k :: 'a poly"
  let ?u' = "root_unity k :: 'b poly"
  interpret p: map_poly_inj_idom_divide_hom hom ..
  have u': "?u' = ?h ?u" unfolding hom_root_unity ..
  note simp = decompose_prod_root_unity_main.simps
  let ?rec1 = "decompose_prod_root_unity_main (p div ?u) k"
  have 0: "?p = 0  p = 0" by simp
  show ?case
    unfolding simp[of ?p k] simp[of p k] if_distrib[of "map_prod id ?h"] Let_def u'
    unfolding 0 p.hom_div[symmetric] p.hom_dvd_iff
    by (rule if_cong[OF refl], force, rule if_cong[OF refl if_cong[OF refl]], force,
     (subst 1(1), auto, cases ?rec1, auto)[1],
     (subst 1(2), auto))
qed

lemma (in field_hom) hom_decompose_prod_root_unity:
  "decompose_prod_root_unity (map_poly hom p) = map_prod id (map_poly hom)
    (decompose_prod_root_unity p)"
  unfolding decompose_prod_root_unity_def
  by (subst hom_decompose_prod_root_unity_main, simp)


end

Theory Perron_Frobenius_Irreducible

(* Author: Thiemann *)
subsection ‹The Perron Frobenius Theorem for Irreducible Matrices›

theory Perron_Frobenius_Irreducible
imports
  Perron_Frobenius
  Roots_Unity
  Rank_Nullity_Theorem.Miscellaneous (* for scalar-matrix-multiplication, 
    this import is incompatible with field_simps, ac_simps *)
begin 

lifting_forget vec.lifting
lifting_forget mat.lifting
lifting_forget poly.lifting

lemma charpoly_of_real: "charpoly (map_matrix complex_of_real A) = map_poly of_real (charpoly A)" 
  by (transfer_hma rule: of_real_hom.char_poly_hom)

context includes lifting_syntax
begin
lemma HMA_M_smult[transfer_rule]: "((=) ===> HMA_M ===> HMA_M) (⋅m) ((*k))" 
  unfolding smult_mat_def 
  unfolding rel_fun_def HMA_M_def from_hmam_def
  by (auto simp: matrix_scalar_mult_def)
end

lemma order_charpoly_smult: fixes A :: "complex ^ 'n ^ 'n" 
  assumes k: "k  0" 
  shows "order x (charpoly (k *k A)) = order (x / k) (charpoly A)" 
  by (transfer fixing: k, rule order_char_poly_smult[OF _ k])

(* use field, since the *k-lemmas have been stated for fields *)
lemma smult_eigen_vector: fixes a :: "'a :: field"  
  assumes "eigen_vector A v x" 
  shows "eigen_vector (a *k A) v (a * x)" 
proof -
  from assms[unfolded eigen_vector_def] have v: "v  0" and id: "A *v v = x *s v" by auto
  from arg_cong[OF id, of "(*s) a"] have id: "(a *k A) *v v = (a * x) *s v" 
    unfolding scalar_matrix_vector_assoc by simp
  thus "eigen_vector (a *k A) v (a * x)" using v unfolding eigen_vector_def by auto
qed

lemma smult_eigen_value: fixes a :: "'a :: field"  
  assumes "eigen_value A x" 
  shows "eigen_value (a *k A) (a * x)" 
  using assms smult_eigen_vector[of A _ x a] unfolding eigen_value_def by blast

locale fixed_mat = fixes A :: "'a :: zero ^ 'n ^ 'n"
begin
definition G :: "'n rel" where
  "G = { (i,j). A $ i $ j  0}" 

definition irreducible :: bool where
  "irreducible = (UNIV  G^+)" 
end

lemma G_transpose: 
  "fixed_mat.G (transpose A) = ((fixed_mat.G A))^-1"
  unfolding fixed_mat.G_def by (force simp: transpose_def)

lemma G_transpose_trancl: 
  "(fixed_mat.G (transpose A))^+ = ((fixed_mat.G A)^+)^-1"
  unfolding G_transpose trancl_converse by auto 

locale pf_nonneg_mat = fixed_mat A for 
  A :: "'a :: linordered_idom ^ 'n ^ 'n" + 
  assumes non_neg_mat: "non_neg_mat A"  
begin 
lemma nonneg: "A $ i $ j  0" 
  using non_neg_mat unfolding non_neg_mat_def elements_mat_h_def by auto

lemma nonneg_matpow: "matpow A n $ i $ j  0" 
  by (induct n arbitrary: i j, insert nonneg, 
    auto intro!: sum_nonneg simp: matrix_matrix_mult_def mat_def)

lemma G_relpow_matpow_pos: "(i,j)  G ^^ n  matpow A n $ i $ j > 0" 
proof (induct n arbitrary: i j)
  case (0 i)
  thus ?case by (auto simp: mat_def)
next
  case (Suc n i j)
  from Suc(2) have "(i,j)  G ^^ n O G"
    by (simp add: relpow_commute) 
  then obtain k where
    ik: "A $ k $ j  0" and kj: "(i, k)  G ^^ n" by (auto simp: G_def)
  from ik nonneg[of k j] have ik: "A $ k $ j > 0" by auto
  from Suc(1)[OF kj] have IH: "matpow A n $h i $h k > 0" .
  thus ?case using ik by (auto simp: nonneg_matpow nonneg matrix_matrix_mult_def 
    intro!: sum_pos2[of _ k] mult_nonneg_nonneg)
qed

lemma matpow_mono: assumes B: " i j. B $ i $ j  A $ i $ j"
  shows "matpow B n $ i $ j  matpow A n $ i $ j" 
proof (induct n arbitrary: i j)
  case (Suc n i j)
  thus ?case using B nonneg_matpow[of n] nonneg 
    by (auto simp: matrix_matrix_mult_def intro!: sum_mono mult_mono')
qed simp

lemma matpow_sum_one_mono: "matpow (A + mat 1) (n + k) $ i $ j  matpow (A + mat 1) n $ i $ j" 
proof (induct k)
  case (Suc k)
  have "(matpow (A + mat 1) (n + k) ** A) $h i $h j  0" unfolding matrix_matrix_mult_def
    using order.trans[OF nonneg_matpow matpow_mono[of "A + mat 1" "n + k"]]
    by (auto intro!: sum_nonneg mult_nonneg_nonneg nonneg simp: mat_def)
  thus ?case using Suc by (simp add: matrix_add_ldistrib matrix_mul_rid)
qed simp

lemma G_relpow_matpow_pos_ge: 
  assumes "(i,j)  G ^^ m" "n  m"
  shows "matpow (A + mat 1) n $ i $ j > 0" 
proof -
  from assms(2) obtain k where n: "n = m + k" using le_Suc_ex by blast  
  have "0 < matpow A m $ i $ j" by (rule G_relpow_matpow_pos[OF assms(1)])
  also have "  matpow (A + mat 1) m $ i $ j" 
    by (rule matpow_mono, auto simp: mat_def)
  also have "  matpow (A + mat 1) n $ i $ j" unfolding n using matpow_sum_one_mono .
  finally show ?thesis .
qed
end

locale perron_frobenius = pf_nonneg_mat A 
  for A :: "real ^ 'n ^ 'n" +
  assumes irr: irreducible
begin

definition N where "N = (SOME N.  ij.  n  N. ij  G ^^ n)" 

lemma N: " n  N. ij  G ^^ n" 
proof -
  {
    fix ij
    have "ij  G^+" using irr[unfolded irreducible_def] by auto
    from this[unfolded trancl_power] have " n. ij  G ^^ n" by blast
  }
  hence " ij.  n. ij  G ^^ n" by auto
  from choice[OF this] obtain f where f: " ij. ij  G ^^ (f ij)" by auto
  define N where N: "N = Max (range f)" 
  {
    fix ij
    from f[of ij] have "ij  G ^^ f ij" .
    moreover have "f ij  N" unfolding N
      by (rule Max_ge, auto) 
    ultimately have " n  N. ij  G ^^ n" by blast
  } note main = this
  let ?P = "λ N.  ij.  n  N. ij  G ^^ n" 
  from main have "?P N" by blast
  from someI[of ?P, OF this, folded N_def]
  show ?thesis by blast
qed

lemma irreducible_matpow_pos: assumes irreducible 
  shows "matpow (A + mat 1) N $ i $ j > 0"
proof -
  from N obtain n where n: "n  N" and reach: "(i,j)  G ^^ n" by auto
  show ?thesis by (rule G_relpow_matpow_pos_ge[OF reach n])
qed

lemma pf_transpose: "perron_frobenius (transpose A)" 
proof
  show "fixed_mat.irreducible (transpose A)" 
    unfolding fixed_mat.irreducible_def G_transpose_trancl using irr[unfolded irreducible_def] 
    by auto
qed (insert nonneg, auto simp: transpose_def non_neg_mat_def elements_mat_h_def)

abbreviation le_vec :: "real ^ 'n  real ^ 'n  bool" where
  "le_vec x y  ( i. x $ i  y $ i)" 

abbreviation lt_vec :: "real ^ 'n  real ^ 'n  bool" where
  "lt_vec x y  ( i. x $ i < y $ i)" 

definition "A1n = matpow (A + mat 1) N" 

lemmas A1n_pos = irreducible_matpow_pos[OF irr, folded A1n_def]

definition r :: "real ^ 'n  real" where
  "r x = Min { (A *v x) $ j / x $ j | j. x $ j  0 }" 

definition X :: "(real ^ 'n )set" where
  "X = { x . le_vec 0 x  x  0 }" 

lemma nonneg_Ax: "x  X  le_vec 0 (A *v x)" 
  unfolding X_def using nonneg
  by (auto simp: matrix_vector_mult_def intro!: sum_nonneg)

lemma A_nonzero_fixed_i: " j. A $ i $ j  0" 
proof -
  from irr[unfolded irreducible_def] have "(i,i)  G^+" by auto
  then obtain j where "(i,j)  G" by (metis converse_tranclE)
  hence Aij: "A $ i $ j  0" unfolding G_def by auto
  thus ?thesis ..
qed

lemma A_nonzero_fixed_j: " i. A $ i $ j  0" 
proof -
  from irr[unfolded irreducible_def] have "(j,j)  G^+" by auto
  then obtain i where "(i,j)  G" by (cases, auto)
  hence Aij: "A $ i $ j  0" unfolding G_def by auto
  thus ?thesis ..
qed

lemma Ax_pos: assumes x: "lt_vec 0 x" 
  shows "lt_vec 0 (A *v x)" 
proof 
  fix i
  from A_nonzero_fixed_i[of i] obtain j where "A $ i $ j  0" by auto
  with nonneg[of i j] have A: "A $ i $ j > 0" by simp
  from x have "x $ j  0" for j by (auto simp: order.strict_iff_order)
  note nonneg = mult_nonneg_nonneg[OF nonneg[of i] this]
  have "(A *v x) $ i = (jUNIV. A $ i $ j * x $ j)" 
    unfolding matrix_vector_mult_def by simp
  also have " = A $ i $ j * x $ j + (jUNIV - {j}. A $ i $ j * x $ j)" 
    by (subst sum.remove, auto)
  also have " > 0 + 0" 
    by (rule add_less_le_mono, insert A x[rule_format] nonneg,
    auto intro!: sum_nonneg mult_pos_pos)
  finally show "0 $ i < (A *v x) $ i" by simp
qed
  

lemma nonzero_Ax: assumes x: "x  X"
  shows "A *v x  0" 
proof 
  assume 0: "A *v x = 0" 
  from x[unfolded X_def] have x: "le_vec 0 x" "x  0" by auto
  from x(2) obtain j where xj: "x $ j  0"
    by (metis vec_eq_iff zero_index)
  from A_nonzero_fixed_j[of j]  obtain i where Aij: "A $ i $ j  0" by auto
  from arg_cong[OF 0, of "λ v. v $ i", unfolded matrix_vector_mult_def]
  have "0 = ( k  UNIV. A $h i $h k * x $h k)" by auto
  also have " = A $h i $h j * x $h j + ( k  UNIV - {j}. A $h i $h k * x $h k)" 
    by (subst sum.remove[of _ j], auto)
  also have " > 0 + 0" 
    by (rule add_less_le_mono, insert nonneg[of i] Aij x(1) xj, 
    auto intro!: sum_nonneg mult_pos_pos simp: dual_order.not_eq_order_implies_strict) 
  finally show False by simp
qed

lemma r_witness: assumes x: "x  X" 
  shows " j. x $ j > 0  r x = (A *v x) $ j / x $ j"
proof -
  from x[unfolded X_def] have x: "le_vec 0 x" "x  0" by auto
  let ?A = "{ (A *v x) $ j / x $ j | j. x $ j  0 }" 
  from x(2) obtain j where "x $ j  0"
    by (metis vec_eq_iff zero_index)
  hence empty: "?A  {}" by auto
  from Min_in[OF _ this, folded r_def]
  obtain j where "x $ j  0" and rx: "r x = (A *v x) $ j / x $ j" by auto
  with x have "x $ j > 0" by (auto simp: dual_order.not_eq_order_implies_strict)
  with rx show ?thesis by auto
qed

lemma rx_nonneg: assumes x: "x  X"
  shows "r x  0"
proof -
  from x[unfolded X_def] have x: "le_vec 0 x" "x  0" by auto
  let ?A = "{ (A *v x) $ j / x $ j | j. x $ j  0 }" 
  from r_witness[OF x  X›]
  have empty: "?A  {}" by force
  show ?thesis unfolding r_def X_def
  proof (subst Min_ge_iff, force, use empty in force, intro ballI) 
    fix y
    assume "y  ?A" 
    then obtain j where "y = (A *v x) $ j / x $ j" and "x $ j  0" by auto
    from nonneg_Ax[OF x  X›] this x
    show "0  y" by simp
  qed
qed

lemma rx_pos: assumes x: "lt_vec 0 x"
  shows "r x > 0"
proof -
  from Ax_pos[OF x] have lt: "lt_vec 0 (A *v x)" .
  from x have x': "x  X" unfolding X_def order.strict_iff_order by auto
  let ?A = "{ (A *v x) $ j / x $ j | j. x $ j  0 }" 
  from r_witness[OF x  X›]
  have empty: "?A  {}" by force
  show ?thesis unfolding r_def X_def
  proof (subst Min_gr_iff, force, use empty in force, intro ballI) 
    fix y
    assume "y  ?A" 
    then obtain j where "y = (A *v x) $ j / x $ j" and "x $ j  0" by auto
    from lt this x show "0 < y" by simp
  qed
qed

lemma rx_le_Ax: assumes x: "x  X" 
  shows "le_vec (r x *s x) (A *v x)" 
proof (intro allI)
  fix i
  show "(r x *s x) $h i  (A *v x) $h i" 
  proof (cases "x $ i = 0")
    case True
    with nonneg_Ax[OF x] show ?thesis by auto
  next
    case False
    with x[unfolded X_def] have pos: "x $ i > 0" 
      by (auto simp: dual_order.not_eq_order_implies_strict)
    from False have "(A *v x) $h i / x $ i  { (A *v x) $ j / x $ j | j. x $ j  0 }" by auto
    hence "(A *v x) $h i / x $ i  r x" unfolding r_def by simp
    hence "x $ i * r x  x $ i * ((A *v x) $h i / x $ i)" unfolding mult_le_cancel_left_pos[OF pos] .
    also have " = (A *v x) $h i" using pos by simp
    finally show ?thesis by (simp add: ac_simps)
  qed
qed

lemma rho_le_x_Ax_imp_rho_le_rx: assumes x: "x  X"
  and ρ: "le_vec (ρ *s x) (A *v x)"
shows "ρ  r x" 
proof -
  from r_witness[OF x] obtain j where 
    rx: "r x = (A *v x) $ j / x $ j" and xj: "x $ j > 0" "x $ j  0" by auto
  from divide_right_mono[OF ρ[rule_format, of j] xj(2)]
  show ?thesis unfolding rx using xj by simp 
qed

lemma rx_Max: assumes x: "x  X"
  shows "r x = Sup { ρ . le_vec (ρ *s x) (A *v x) }" (is "_ = Sup ?S")
proof -
  have "r x  ?S" using rx_le_Ax[OF x] by auto
  moreover {
    fix y
    assume "y  ?S"
    hence y: "le_vec (y *s x) (A *v x)" by auto
    from rho_le_x_Ax_imp_rho_le_rx[OF x this]
    have "y  r x" . 
  }
  ultimately show ?thesis by (metis (mono_tags, lifting) cSup_eq_maximum)
qed

lemma r_smult: assumes x: "x  X" 
  and a: "a > 0" 
shows "r (a *s x) = r x" 
  unfolding r_def
  by (rule arg_cong[of _ _ Min], unfold vector_smult_distrib, insert a, simp)

definition "X1 = (X  {x. norm x = 1})" 

lemma bounded_X1: "bounded X1" unfolding bounded_iff X1_def by auto

lemma closed_X1: "closed X1"
proof -
  have X1: "X1 = {x. le_vec 0 x  norm x = 1}" 
    unfolding X1_def X_def by auto
  show ?thesis unfolding X1
    by (intro closed_Collect_conj closed_Collect_all  closed_Collect_le closed_Collect_eq,
      auto intro: continuous_intros)
qed

lemma compact_X1: "compact X1" using bounded_X1 closed_X1
  by (simp add: compact_eq_bounded_closed)

definition "pow_A_1 x = A1n *v x" 



lemma continuous_pow_A_1: "continuous_on R pow_A_1"
  unfolding pow_A_1_def continuous_on
  by (auto intro: tendsto_intros)

definition "Y = pow_A_1 ` X1" 

lemma compact_Y: "compact Y" 
  unfolding Y_def using compact_X1 continuous_pow_A_1[of X1] 
  by (metis compact_continuous_image)

lemma Y_pos_main: assumes y: "y  pow_A_1 ` X" 
  shows "y $ i > 0" 
proof -
  from y obtain x where x: "x  X" and y: "y = pow_A_1 x" unfolding Y_def X1_def by auto
  from r_witness[OF x] obtain j where xj: "x $ j > 0" by auto
  from x[unfolded X_def] have xi: "x $ i  0" for i by auto
  have nonneg: "0  A1n $ i $ k * x $ k" for k using A1n_pos[of i k] xi[of k] by auto 
  have "y $ i = (jUNIV. A1n $ i $ j * x $ j)" 
    unfolding y pow_A_1_def matrix_vector_mult_def by simp
  also have " = A1n $ i $ j * x $ j + (jUNIV - {j}. A1n $ i $ j * x $ j)" 
    by (subst sum.remove, auto)
  also have " > 0 + 0" 
    by (rule add_less_le_mono, insert xj A1n_pos nonneg, 
    auto intro!: sum_nonneg mult_pos_pos simp: dual_order.not_eq_order_implies_strict)
  finally show ?thesis by simp
qed

lemma Y_pos: assumes y: "y  Y" 
  shows "y $ i > 0" 
  using Y_pos_main[of y i] y unfolding Y_def X1_def by auto

lemma Y_nonzero: assumes y: "y  Y" 
  shows "y $ i  0" 
  using Y_pos[OF y, of i] by auto

definition r' :: "real ^ 'n  real" where
  "r' x = Min (range (λ j. (A *v x) $ j / x $ j))" 

lemma r'_r: assumes x: "x  Y" shows "r' x = r x" 
  unfolding r'_def r_def
proof (rule arg_cong[of _ _ Min])
  have "range (λj. (A *v x) $ j / x $ j)  {(A *v x) $ j / x $ j |j. x $ j  0}" (is "?L  ?R")
  proof 
    fix y
    assume "y  ?L" 
    then obtain j where "y = (A *v x) $ j / x $ j" by auto
    with Y_pos[OF x, of j] show "y  ?R" by auto
  qed
  moreover have "?L  ?R" by auto
  ultimately show "?L = ?R" by blast
qed  

lemma continuous_Y_r: "continuous_on Y r"
proof -
  have *: "( y  Y. P y (r y)) = ( y  Y. P y (r' y))" for P using r'_r by auto
  have "continuous_on Y r = continuous_on Y r'" 
    by (rule continuous_on_cong[OF refl r'_r[symmetric]])
  also have 
    unfolding continuous_on r'_def using Y_nonzero
    by (auto intro!: tendsto_Min tendsto_intros)
  finally show ?thesis .
qed
 
lemma X1_nonempty: "X1  {}" 
proof -
  define x where "x = ((χ i. if i = undefined then 1 else 0) :: real ^ 'n)" 
  {
    assume "x = 0" 
    from arg_cong[OF this, of "λ x. x $ undefined"] have False unfolding x_def by auto
  }
  hence x: "x  0" by auto
  moreover have "le_vec 0 x" unfolding x_def by auto
  moreover have "norm x = 1" unfolding norm_vec_def L2_set_def
    by (auto, subst sum.remove[of _ undefined], auto simp: x_def)
  ultimately show ?thesis unfolding X1_def X_def by auto
qed

lemma Y_nonempty: "Y  {}" 
  unfolding Y_def using X1_nonempty by auto

definition z where "z = (SOME z. z  Y  ( y  Y. r y  r z))" 

abbreviation "sr  r z"

lemma z: "z  Y" and sr_max_Y: " y. y  Y  r y  sr" 
proof -
  let ?P = "λ z. z  Y  ( y  Y. r y  r z)" 
  from continuous_attains_sup[OF compact_Y Y_nonempty continuous_Y_r]
  obtain y where "?P y" by blast
  from someI[of ?P, OF this, folded z_def]
  show "z  Y" " y. y  Y  r y  r z" by blast+
qed

lemma Y_subset_X: "Y  X" 
proof
  fix y
  assume "y  Y" 
  from Y_pos[OF this] show "y  X" unfolding X_def 
    by (auto simp: order.strict_iff_order) 
qed

lemma zX: "z  X" 
  using z(1) Y_subset_X by auto

lemma le_vec_mono_left: assumes B: " i j. B $ i $ j  0" 
  and "le_vec x y" 
shows "le_vec (B *v x) (B *v y)" 
proof (intro allI)
  fix i
  show "(B *v x) $ i  (B *v y) $ i" unfolding matrix_vector_mult_def using B[of i] assms(2)
    by (auto intro!: sum_mono mult_left_mono)
qed  


lemma matpow_1_commute: "matpow (A + mat 1) n ** A = A ** matpow (A + mat 1) n" 
  by (induct n, auto simp: matrix_add_rdistrib matrix_add_ldistrib matrix_mul_rid matrix_mul_lid
  matrix_mul_assoc[symmetric])

lemma A1n_commute: "A1n ** A = A ** A1n" 
  unfolding A1n_def by (rule matpow_1_commute)

lemma le_vec_pow_A_1: assumes le: "le_vec (rho *s x) (A *v x)" 
  shows "le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)" 
proof -
  have "A1n $ i $ j  0" for i j using A1n_pos[of i j] by auto
  from le_vec_mono_left[OF this le]
  have "le_vec (A1n *v (rho *s x)) (A1n *v (A *v x))" .
  also have "A1n *v (A *v x) = (A1n ** A) *v x" by (simp add: matrix_vector_mul_assoc)
  also have " = A *v (A1n *v x)" unfolding A1n_commute by (simp add: matrix_vector_mul_assoc)
  also have " = A *v (pow_A_1 x)" unfolding pow_A_1_def ..
  also have "A1n *v (rho *s x) = rho *s (A1n *v x)" unfolding vector_smult_distrib ..
  also have " = rho *s pow_A_1 x" unfolding pow_A_1_def ..
  finally show "le_vec (rho *s pow_A_1 x) (A *v pow_A_1 x)" .
qed

lemma r_pow_A_1: assumes x: "x  X"
  shows "r x  r (pow_A_1 x)" 
proof -
  let ?y = "pow_A_1 x" 
  have "?y  pow_A_1 ` X" using x by auto
  from Y_pos_main[OF this] 
  have y: "?y  X" unfolding X_def by (auto simp: order.strict_iff_order) 
  let ?A = "{ρ. le_vec (ρ *s x) (A *v x)}" 
  let ?B = "{ρ. le_vec (ρ *s pow_A_1 x) (A *v pow_A_1 x)}" 
  show ?thesis unfolding rx_Max[OF x] rx_Max[OF y]
  proof (rule cSup_mono)
    show "bdd_above ?B" using rho_le_x_Ax_imp_rho_le_rx[OF y] by fast
    show "?A  {}" using rx_le_Ax[OF x] by auto 
    fix rho
    assume "rho  ?A"
    hence "le_vec (rho *s x) (A *v x)" by auto
    from le_vec_pow_A_1[OF this] have "rho  ?B" by auto
    thus " rho'  ?B. rho  rho'" by auto
  qed
qed

lemma sr_max: assumes x: "x  X" 
  shows "r x  sr" 
proof -
  let ?n = "norm x" 
  define x' where "x' = inverse ?n *s x" 
  from x[unfolded X_def] have x0: "x  0" by auto
  hence n: "?n > 0" by auto
  have x': "x'  X1" "x'  X" using x n unfolding X1_def X_def x'_def by (auto simp: norm_smult)
  have id: "r x = r x'" unfolding x'_def 
    by (rule sym, rule r_smult[OF x], insert n, auto)
  define y where "y = pow_A_1 x'" 
  from x' have y: "y  Y" unfolding Y_def y_def by auto
  note id
  also have "r x'  r y" using r_pow_A_1[OF x'(2)] unfolding y_def .
  also have "  r z" using sr_max_Y[OF y] .
  finally show "r x  r z" .
qed

lemma z_pos: "z $ i > 0" 
  using Y_pos[OF z(1)] by auto

lemma sr_pos: "sr > 0"
  by (rule rx_pos, insert z_pos, auto)

context fixes u
  assumes u: "u  X" and ru: "r u = sr" 
begin

lemma sr_imp_eigen_vector_main: "sr *s u = A *v u" 
proof (rule ccontr)
  assume *: "sr *s u  A *v u" 
  let ?x = "A *v u - sr *s u" 
  from * have 0: "?x  0" by auto
  let ?y = "pow_A_1 u" 
  have "le_vec (sr *s u) (A *v u)" using rx_le_Ax[OF u] unfolding ru .
  hence le: "le_vec 0 ?x" by auto
  from 0 le have x: "?x  X" unfolding X_def by auto
  have y_pos: "lt_vec 0 ?y" using Y_pos_main[of ?y] u by auto
  hence y: "?y  X" unfolding X_def by (auto simp: order.strict_iff_order)  
  from Y_pos_main[of "pow_A_1 ?x"] x 
  have "lt_vec 0 (pow_A_1 ?x)" by auto
  hence lt: "lt_vec (sr *s ?y) (A *v ?y)" unfolding pow_A_1_def matrix_vector_right_distrib_diff
    matrix_vector_mul_assoc A1n_commute vector_smult_distrib by simp
  let ?f = "(λ i. (A *v ?y - sr *s ?y) $ i / ?y $ i)" 
  let ?U = "UNIV :: 'n set"
  define eps where "eps = Min (?f ` ?U)" 
  have U: "finite (?f ` ?U)" "?f ` ?U  {}" by auto
  have eps: "eps > 0" unfolding eps_def Min_gr_iff[OF U]
    using lt sr_pos y_pos by auto
  have le: "le_vec ((sr + eps) *s ?y) (A *v ?y)"
  proof 
    fix i
    have "((sr + eps) *s ?y) $ i = sr * ?y $ i + eps * ?y $ i"
      by (simp add: comm_semiring_class.distrib)
    also have "  sr * ?y $ i + ?f i * ?y $ i" 
    proof (rule add_left_mono[OF mult_right_mono])
      show "0  ?y $ i" using y_pos[rule_format, of i] by auto
      show "eps  ?f i" unfolding eps_def by (rule Min_le, auto) 
    qed
    also have " = (A *v ?y) $ i" using sr_pos y_pos[rule_format, of i] 
      by simp
    finally  
    show "((sr + eps) *s ?y) $ i  (A *v ?y) $ i" .
  qed
  from rho_le_x_Ax_imp_rho_le_rx[OF y le]
  have "r ?y  sr + eps" .
  with sr_max[OF y] eps show False by auto
qed

lemma sr_imp_eigen_vector: "eigen_vector A u sr" 
  unfolding eigen_vector_def sr_imp_eigen_vector_main using u unfolding X_def by auto

lemma sr_u_pos: "lt_vec 0 u" 
proof -
  let ?y = "pow_A_1 u" 
  define n where "n = N" 
  define c where "c = (sr + 1)^N" 
  have c: "c > 0" using sr_pos unfolding c_def by auto
  have "lt_vec 0 ?y" using Y_pos_main[of ?y] u by auto
  also have "?y = A1n *v u" unfolding pow_A_1_def ..
  also have " = c *s u" unfolding c_def A1n_def n_def[symmetric]
  proof (induct n)
    case (Suc n)
    then show ?case
      by (simp add: matrix_vector_mul_assoc[symmetric] algebra_simps vec.scale
          sr_imp_eigen_vector_main[symmetric])
  qed auto
  finally have lt: "lt_vec 0 (c *s u)" .
  have "0 < u $ i" for i using lt[rule_format, of i] c by simp (metis zero_less_mult_pos)
  thus "lt_vec 0 u" by simp
qed
end

lemma eigen_vector_z_sr: "eigen_vector A z sr" 
  using sr_imp_eigen_vector[OF zX refl] by auto

lemma eigen_value_sr: "eigen_value A sr" 
  using eigen_vector_z_sr unfolding eigen_value_def by auto

abbreviation "c  complex_of_real" 
abbreviation "cA  map_matrix c A" 
abbreviation "norm_v  map_vector (norm :: complex  real)" 

lemma norm_v_ge_0: "le_vec 0 (norm_v v)" by (auto simp: map_vector_def)
lemma norm_v_eq_0: "norm_v v = 0  v = 0" by (auto simp: map_vector_def vec_eq_iff)

lemma cA_index: "cA $ i $ j = c (A $ i $ j)" 
  unfolding map_matrix_def map_vector_def by simp

lemma norm_cA[simp]: "norm (cA $ i $ j) = A $ i $ j" 
  using nonneg[of i j] by (simp add: cA_index)

context fixes α v
  assumes ev: "eigen_vector cA v α" 
begin

lemma evD: "α *s v = cA *v v" "v  0" 
  using ev[unfolded eigen_vector_def] by auto

lemma ev_alpha_norm_v: "norm_v (α *s v) = (norm α *s norm_v v)" 
  by (auto simp: map_vector_def norm_mult vec_eq_iff)

lemma ev_A_norm_v: "norm_v (cA *v v) $ j  (A *v norm_v v) $ j" 
proof -
  have "norm_v (cA *v v) $ j = norm (iUNIV. cA $ j $ i * v $ i)" 
    unfolding map_vector_def by (simp add: matrix_vector_mult_def)
  also have "  (iUNIV. norm (cA $ j $ i * v $ i))" by (rule norm_sum)
  also have " = (iUNIV. A $ j $ i * norm_v v $ i)" 
    by (rule sum.cong[OF refl], auto simp: norm_mult map_vector_def)
  also have " = (A *v norm_v v) $ j" by (simp add: matrix_vector_mult_def)
  finally show ?thesis .
qed

lemma ev_le_vec: "le_vec (norm α *s norm_v v) (A *v norm_v v)" 
  using arg_cong[OF evD(1), of norm_v, unfolded ev_alpha_norm_v] ev_A_norm_v by auto

lemma norm_v_X: "norm_v v  X" 
  using norm_v_ge_0[of v] evD(2) norm_v_eq_0[of v] unfolding X_def by auto

lemma ev_inequalities: "norm α  r (norm_v v)" "r (norm_v v)  sr"
proof -
  have v: "norm_v v  X" by (rule norm_v_X)
  from rho_le_x_Ax_imp_rho_le_rx[OF v ev_le_vec] 
  show "norm α  r (norm_v v)" .
  from sr_max[OF v]
  show "r (norm_v v)  sr" .
qed

lemma eigen_vector_norm_sr: "norm α  sr" using ev_inequalities by auto
end

lemma eigen_value_norm_sr: assumes "eigen_value cA α" 
  shows "norm α  sr" 
  using eigen_vector_norm_sr[of _ α] assms unfolding eigen_value_def by auto


lemma le_vec_trans: "le_vec x y  le_vec y u  le_vec x u" 
  using order.trans[of "x $ i" "y $ i" "u $ i" for i] by auto

lemma eigen_vector_z_sr_c: "eigen_vector cA (map_vector c z) (c sr)" 
  unfolding of_real_hom.eigen_vector_hom by (rule eigen_vector_z_sr)

lemma eigen_value_sr_c: "eigen_value cA (c sr)" 
  using eigen_vector_z_sr_c unfolding eigen_value_def by auto

definition "w = perron_frobenius.z (transpose A)" 

lemma w: "transpose A *v w = sr *s w" "lt_vec 0 w" "perron_frobenius.sr (transpose A) = sr"
proof -
  interpret t: perron_frobenius "transpose A" 
    by (rule pf_transpose)
  from eigen_vector_z_sr_c t.eigen_vector_z_sr_c 
  have ev: "eigen_value cA (c sr)" "eigen_value t.cA (c t.sr)" 
    unfolding eigen_value_def by auto
  {
    fix x
    have "eigen_value (t.cA) x = eigen_value (transpose cA) x" 
      unfolding map_matrix_def map_vector_def transpose_def 
      by (auto simp: vec_eq_iff)
    also have " = eigen_value cA x" by (rule eigen_value_transpose)
    finally have "eigen_value (t.cA) x = eigen_value cA x" .
  } note ev_id = this
  with ev have ev: "eigen_value t.cA (c sr)" "eigen_value cA (c t.sr)" by auto
  from eigen_value_norm_sr[OF ev(2)] t.eigen_value_norm_sr[OF ev(1)] 
  show id: "t.sr = sr" by auto
  from t.eigen_vector_z_sr[unfolded id, folded w_def] show "transpose A *v w = sr *s w" 
    unfolding eigen_vector_def by auto
  from t.z_pos[folded w_def] show "lt_vec 0 w" by auto
qed

lemma c_cmod_id: "a    Re a  0  c (cmod a) = a" by (auto simp: Reals_def)

lemma pos_rowvector_mult_0: assumes lt: "lt_vec 0 x" 
  and 0: "(rowvector x :: real ^ 'n ^ 'n) *v y = 0" (is "?x *v _ = 0") and le: "le_vec 0 y" 
shows "y = 0" 
proof -
  {
    fix i
    assume "y $ i  0" 
    with le have yi: "y $ i > 0" by (auto simp: order.strict_iff_order)
    have "0 = (?x *v y) $ i" unfolding 0 by simp
    also have " = (jUNIV. x $ j * y $ j)" 
      unfolding rowvector_def matrix_vector_mult_def by simp
    also have " > 0" 
      by (rule sum_pos2[of _ i], insert yi lt le, auto intro!: mult_nonneg_nonneg 
        simp: order.strict_iff_order)
    finally have False by simp
  }
  thus ?thesis by (auto simp: vec_eq_iff)
qed

lemma pos_matrix_mult_0: assumes le: " i j. B $ i $ j  0" 
  and lt: "lt_vec 0 x" 
  and 0: "B *v x = 0" 
shows "B = 0" 
proof -
  {
    fix i j
    assume "B $ i $ j  0" 
    with le have gt: "B $ i $ j > 0" by (auto simp: order.strict_iff_order)
    have "0 = (B *v x) $ i" unfolding 0 by simp
    also have " = (jUNIV. B $ i $ j * x $ j)" 
      unfolding matrix_vector_mult_def by simp
    also have " > 0" 
      by (rule sum_pos2[of _ j], insert gt lt le, auto intro!: mult_nonneg_nonneg 
        simp: order.strict_iff_order)
    finally have False by simp
  }
  thus "B = 0" unfolding vec_eq_iff by auto
qed

lemma eigen_value_smaller_matrix: assumes B: " i j. 0  B $ i $ j  B $ i $ j  A $ i $ j"
  and AB: "A  B" 
  and ev: "eigen_value (map_matrix c B) sigma"
shows "cmod sigma < sr" 
proof -  
  let ?B = "map_matrix c B" 
  let ?sr = "spectral_radius ?B" 
  define σ where "σ = ?sr" 
  have "real_non_neg_mat ?B" unfolding real_non_neg_mat_def elements_mat_h_def
    by (auto simp: map_matrix_def map_vector_def B)
  from perron_frobenius[OF this, folded σ_def] obtain x where ev_sr: "eigen_vector ?B x (c σ)" 
    and rnn: "real_non_neg_vec x" by auto  
  define y where "y = norm_v x" 
  from rnn have xy: "x = map_vector c y" 
    unfolding real_non_neg_vec_def vec_elements_h_def y_def
    by (auto simp: map_vector_def vec_eq_iff c_cmod_id)
  from spectral_radius_max[OF ev, folded σ_def] have sigma_sigma: "cmod sigma  σ" .
  from ev_sr[unfolded xy of_real_hom.eigen_vector_hom] 
  have ev_B: "eigen_vector B y σ" .
  from ev_B[unfolded eigen_vector_def] have ev_B': "B *v y = σ *s y" by auto
  have ypos: "y $ i  0" for i unfolding y_def by (auto simp: map_vector_def)
  from ev_B this have y: "y  X" unfolding eigen_vector_def X_def by auto
  
  have BA: "(B *v y) $ i  (A *v y) $ i" for i
    unfolding matrix_vector_mult_def vec_lambda_beta
    by (rule sum_mono, rule mult_right_mono, insert B ypos, auto)  
  hence le_vec: "le_vec (σ *s y) (A *v y)" unfolding ev_B' by auto
  from rho_le_x_Ax_imp_rho_le_rx[OF y le_vec] 
  have "σ  r y" by auto
  also have "  sr" using y by (rule sr_max)
  finally have sig_le_sr: "σ  sr" .
  {
    assume "σ = sr" 
    hence r_sr: "r y = sr" and sr_sig: "sr = σ" using σ  r y ‹r y  sr› by auto
    from sr_u_pos[OF y r_sr] have pos: "lt_vec 0 y" .
    from sr_imp_eigen_vector[OF y r_sr] have ev': "eigen_vector A y sr" .
    have "(A - B) *v y = A *v y - B *v y" unfolding matrix_vector_mult_def
      by (auto simp: vec_eq_iff field_simps sum_subtractf) 
    also have "A *v y = sr *s y" using ev'[unfolded eigen_vector_def] by auto
    also have "B *v y = sr *s y" unfolding ev_B' sr_sig ..
    finally have id: "(A - B) *v y = 0" by simp
    from pos_matrix_mult_0[OF _ pos id] assms(1-2) have False by auto
  }
  with sig_le_sr sigma_sigma show ?thesis by argo
qed

lemma charpoly_erase_mat_sr: "0 < poly (charpoly (erase_mat A i i)) sr" 
proof -
  let ?A = "erase_mat A i i" 
  let ?pos = "poly (charpoly ?A) sr" 
  {
    from A_nonzero_fixed_j[of i] obtain k where "A $ k $ i  0" by auto
    assume "A = ?A" 
    hence "A $ k $ i = ?A $ k $ i" by simp
    also have "?A $ k $ i = 0" by (auto simp: erase_mat_def)
    also have "A $ k $ i  0" by fact
    finally have False by simp
  }
  hence AA: "A  ?A" by auto
  have le: "0  ?A $ i $ j  ?A $ i $ j  A $ i $ j" for i j
    by (auto simp: erase_mat_def nonneg)
  note ev_small = eigen_value_smaller_matrix[OF le AA]  
  {
    fix rho :: real
    assume "eigen_value ?A rho" 
    hence ev: "eigen_value (map_matrix c ?A) (c rho)" 
      unfolding eigen_value_def using of_real_hom.eigen_vector_hom[of ?A _ rho] by auto
    from ev_small[OF this] have "abs rho < sr" by auto
  } note ev_small_real = this
  have pos0: "?pos  0" 
    using ev_small_real[of sr] by (auto simp: eigen_value_root_charpoly)
  {
    define p where "p = charpoly ?A"
    assume pos: "?pos < 0" 
    hence neg: "poly p sr < 0" unfolding p_def by auto
    from degree_monic_charpoly[of ?A] have mon: "monic p" and deg: "degree p  0" unfolding p_def by auto
    let ?f = "poly p" 
    have cont: "continuous_on {a..b} ?f" for a b by (auto intro: continuous_intros)
    from pos have le: "?f sr  0" by (auto simp: p_def)
    from mon have lc: "lead_coeff p > 0" by auto
    from poly_pinfty_ge[OF this deg, of 0] obtain z where lez: " x. z  x  0  ?f x" by auto
    define y where "y = max z sr" 
    have yr: "y  sr" and "y  z" unfolding y_def by auto
    from lez[OF this(2)] have y0: "?f y  0" .
    from IVT'[of ?f, OF le y0 yr cont] obtain x where ge: "x  sr" and rt: "?f x = 0" 
      unfolding p_def by auto
    hence "eigen_value ?A x" unfolding p_def by (simp add: eigen_value_root_charpoly)
    from ev_small_real[OF this] ge have False by auto
  }
  with pos0 show ?thesis by argo
qed

lemma multiplicity_sr_1: "order sr (charpoly A) = 1" 
proof -
  {
    assume "poly (pderiv (charpoly A)) sr = 0" 
    hence "0 = poly (monom 1 1 * pderiv (charpoly A)) sr" by simp
    also have " = sum (λ i. poly (charpoly (erase_mat A i i)) sr) UNIV" 
      unfolding pderiv_char_poly_erase_mat poly_sum ..
    also have " > 0" 
      by (rule sum_pos, (force simp: charpoly_erase_mat_sr)+)
    finally have False by simp
  } 
  hence nZ: "poly (pderiv (charpoly A)) sr  0" and nZ': "pderiv (charpoly A)  0" by auto
  from eigen_vector_z_sr have "eigen_value A sr" unfolding eigen_value_def ..
  from this[unfolded eigen_value_root_charpoly]
  have "poly (charpoly A) sr = 0" .
  hence "order sr (charpoly A)  0" unfolding order_root using nZ' by auto
  from order_pderiv[OF nZ' this] order_0I[OF nZ]
  show ?thesis by simp
qed

lemma sr_spectral_radius: "sr = spectral_radius cA" 
proof -
  from eigen_vector_z_sr_c have "eigen_value cA (c sr)" 
    unfolding eigen_value_def by auto
  from spectral_radius_max[OF this] 
  have sr: "sr  spectral_radius cA" by auto
  with spectral_radius_ev[of cA] eigen_vector_norm_sr
  show ?thesis by force
qed

lemma le_vec_A_mu: assumes y: "y  X" and le: "le_vec (A *v y) (mu *s y)" 
  shows "sr  mu" "lt_vec 0 y" 
  "mu = sr  A *v y = mu *s y  mu = sr  A *v y = mu *s y" 
proof -
  let ?w = "rowvector w" 
  let ?w' = "columnvector w" 
  have "?w ** A = transpose (transpose (?w ** A))" 
    unfolding transpose_transpose by simp
  also have "transpose (?w ** A) = transpose A ** transpose ?w" 
    by (rule matrix_transpose_mul)
  also have "transpose ?w = columnvector w" by (rule transpose_rowvector)
  also have "transpose A **  = columnvector (transpose A *v w)" 
    unfolding dot_rowvector_columnvector[symmetric] ..
  also have "transpose A *v w = sr *s w" unfolding w by simp
  also have "transpose (columnvector ) = rowvector (sr *s w)"
    unfolding transpose_def columnvector_def rowvector_def vector_scalar_mult_def by auto
  finally have 1: "?w ** A = rowvector (sr *s w)" .
  have "sr *s (?w *v y) = ?w ** A *v y" unfolding 1
    by (auto simp: rowvector_def vector_scalar_mult_def matrix_vector_mult_def vec_eq_iff
       sum_distrib_left mult.assoc)
  also have " = ?w *v (A *v y)" by (simp add: matrix_vector_mul_assoc)
  finally have eq1: "sr *s (rowvector w *v y) = rowvector w *v (A *v y)" .
  have "le_vec (rowvector w *v (A *v y)) (?w *v (mu *s y))" 
    by (rule le_vec_mono_left[OF _ le], insert w(2), auto simp: rowvector_def order.strict_iff_order)
  also have "?w *v (mu *s y) = mu *s (?w *v y)" by (simp add: algebra_simps vec.scale)
  finally have le1: "le_vec (rowvector w *v (A *v y)) (mu *s (?w *v y))" .
  from le1[unfolded eq1[symmetric]] 
  have 2: "le_vec (sr *s (?w *v y)) (mu *s (?w *v y))" .
  {
    from y obtain i where yi: "y $ i > 0" and y: " j. y $ j  0" unfolding X_def
      by (auto simp: order.strict_iff_order vec_eq_iff)
    from w(2) have wi: "w $ i > 0" and w: " j. w $ j  0"
      by (auto simp: order.strict_iff_order)
    have "(?w *v y) $ i > 0" using yi y wi w
      by (auto simp: matrix_vector_mult_def rowvector_def 
        intro!: sum_pos2[of _ i] mult_nonneg_nonneg)
    moreover from 2[rule_format, of i] have "sr * (?w *v y) $ i  mu * (?w *v y) $ i" by simp
    ultimately have "sr  mu" by simp
  } 
  thus *: "sr  mu" .
  define cc where "cc = (mu + 1)^ N" 
  define n where "n = N" 
  from * sr_pos have mu: "mu  0" "mu > 0" by auto
  hence cc: "cc > 0" unfolding cc_def by simp  
  from y have "pow_A_1 y  pow_A_1 ` X" by auto
  from Y_pos_main[OF this] have lt: "0 < (A1n *v y) $ i" for i by (simp add: pow_A_1_def)
  have le: "le_vec (A1n *v y) (cc *s y)" unfolding cc_def A1n_def n_def[symmetric]
  proof (induct n)
    case (Suc n)
    let ?An = "matpow (A + mat 1) n" 
    let ?mu = "(mu + 1)" 
    have id': "matpow (A + mat 1) (Suc n) *v y = A *v (?An *v y) + ?An *v y" (is "?a = ?b + ?c")
      by (simp add: matrix_add_ldistrib matrix_mul_rid matrix_add_vect_distrib matpow_1_commute
       matrix_vector_mul_assoc[symmetric])
    have "le_vec ?b (?mu^n *s (A *v y))" 
      using le_vec_mono_left[OF nonneg Suc] by (simp add: algebra_simps vec.scale)
    moreover have "le_vec (?mu^n *s (A *v y)) (?mu^n *s (mu *s y))" 
      using le mu by auto
    moreover have id: "?mu^n *s (mu *s y) = (?mu^n * mu) *s y" by simp
    from le_vec_trans[OF calculation[unfolded id]] 
    have le1: "le_vec ?b ((?mu^n * mu) *s y)" . 
    from Suc have le2: "le_vec ?c ((mu + 1) ^ n *s y)" .
    have le: "le_vec ?a ((?mu^n * mu) *s y + ?mu^n *s y)" 
      unfolding id' using add_mono[OF le1[rule_format] le2[rule_format]] by auto
    have id'': "(?mu^n * mu) *s y + ?mu^n *s y = ?mu^Suc n *s y" by (simp add: algebra_simps)
    show ?case using le unfolding id'' .
  qed (simp add: matrix_vector_mul_lid)
  have lt: "0 < cc * y $ i" for i using lt[of i] le[rule_format, of i] by auto
  have "y $ i > 0" for i using lt[of i] cc by (rule zero_less_mult_pos)
  thus "lt_vec 0 y" by auto
  assume **: "mu = sr  A *v y = mu *s y" 
  {
    assume "A *v y = mu *s y" 
    with y have "eigen_vector A y mu" unfolding X_def eigen_vector_def by auto
    hence "eigen_vector cA (map_vector c y) (c mu)" unfolding of_real_hom.eigen_vector_hom .
    from eigen_vector_norm_sr[OF this] * have "mu = sr" by auto
  }
  with ** have mu_sr: "mu = sr" by auto
  from eq1[folded vector_smult_distrib]
  have 0: "?w *v (sr *s y - A *v y) = 0"
    unfolding matrix_vector_right_distrib_diff by simp
  have le0: "le_vec 0 (sr *s y - A *v y)" using assms(2)[unfolded mu_sr] by auto
  have "sr *s y - A *v y = 0" using pos_rowvector_mult_0[OF w(2) 0 le0] .
  hence ev_y: "A *v y = sr *s y" by auto
  show "mu = sr  A *v y = mu *s y" using ev_y mu_sr by auto
qed

lemma nonnegative_eigenvector_has_ev_sr: assumes "eigen_vector A v mu" and le: "le_vec 0 v" 
  shows "mu = sr" 
proof -
  from assms(1)[unfolded eigen_vector_def] have v: "v  0" and ev: "A *v v = mu *s v" by auto
  from le v have v: "v  X" unfolding X_def by auto
  from ev have "le_vec (A *v v) (mu *s v)" by auto
  from le_vec_A_mu[OF v this] ev show ?thesis by auto
qed

lemma similar_matrix_rotation: assumes ev: "eigen_value cA α" and α: "cmod α = sr"
  shows "similar_matrix (cis (arg α) *k cA) cA" 
proof -
  from ev obtain y where ev: "eigen_vector cA y α" unfolding eigen_value_def by auto
  let ?y = "norm_v y"
  note maps = map_vector_def map_matrix_def
  define yp where "yp = norm_v y" 
  let ?yp = "map_vector c yp" 
  have yp: "yp  X" unfolding yp_def by (rule norm_v_X[OF ev])
  from ev[unfolded eigen_vector_def] have ev_y: "cA *v y = α *s y" by auto
  from ev_le_vec[OF ev, unfolded α, folded yp_def]
  have 1: "le_vec (sr *s yp) (A *v yp)" by simp
  from rho_le_x_Ax_imp_rho_le_rx[OF yp 1] have "sr  r yp" by auto
  with ev_inequalities[OF ev, folded yp_def]
  have 2: "r yp = sr" by auto
  have ev_yp: "A *v yp = sr *s yp" 
    and pos_yp: "lt_vec 0 yp" 
    using sr_imp_eigen_vector_main[OF yp 2] sr_u_pos[OF yp 2] by auto
  define D where "D = diagvector (λ j. cis (arg (y $ j)))" 
  define inv_D where "inv_D = diagvector (λ j. cis (- arg (y $ j)))" 
  have DD: "inv_D ** D = mat 1" "D ** inv_D = mat 1" unfolding D_def inv_D_def 
    by (auto simp add: diagvector_eq_mat cis_mult)
  {
    fix i
    have "(D *v ?yp) $ i = cis (arg (y $ i)) * c (cmod (y $ i))" 
      unfolding D_def yp_def by (simp add: maps) 
    also have " = y $ i" by (simp add: cis_mult_cmod_id)
    also note calculation
  }
  hence y_D_yp: "y = D *v ?yp" by (auto simp: vec_eq_iff)
  define φ where "φ = arg α" 
  let  = "cis (- φ)" 
  have [simp]: "cis (- φ) * rcis sr φ = sr" unfolding cis_rcis_eq rcis_mult by simp
  have α: "α = rcis sr φ" unfolding φ_def α[symmetric] rcis_cmod_arg ..
  define F where "F =  *k (inv_D ** cA ** D)" 
  have "cA *v (D *v ?yp) = α *s y" unfolding y_D_yp[symmetric] ev_y by simp
  also have "inv_D *v  = α *s ?yp" 
    unfolding vector_smult_distrib y_D_yp matrix_vector_mul_assoc DD matrix_vector_mul_lid ..
  also have " *s  = sr *s ?yp" unfolding α by simp
  also have " = map_vector c (sr *s yp)" unfolding vec_eq_iff by (auto simp: maps)
  also have " = cA *v ?yp" unfolding ev_yp[symmetric] by (auto simp: maps matrix_vector_mult_def)
  finally have F: "F *v ?yp = cA *v ?yp" unfolding F_def matrix_scalar_vector_ac[symmetric]
    unfolding matrix_vector_mul_assoc[symmetric] vector_smult_distrib .
  have prod: "inv_D ** cA ** D = (χ i j. cis (- arg (y $ i)) * cA $ i $ j * cis (arg (y $ j)))" 
    unfolding inv_D_def D_def diagvector_mult_right diagvector_mult_left by simp
  {
    fix i j
    have "cmod (F $ i $ j) = cmod ( * cA $h i $h j * (cis (- arg (y $h i)) * cis (arg (y $h j))))" 
      unfolding F_def prod vec_lambda_beta matrix_scalar_mult_def
      by (simp only: ac_simps)
    also have " = A $ i $ j" unfolding cis_mult unfolding norm_mult by simp
    also note calculation
  }
  hence FA: "map_matrix norm F = A" unfolding maps by auto
  let ?F = "map_matrix c (map_matrix norm F)" 
  let ?G = "?F - F" 
  let ?Re = "map_matrix Re" 
  from F[folded FA] have 0: "?G *v ?yp = 0" unfolding matrix_diff_vect_distrib by simp
  have "?Re ?G *v yp = map_vector Re (?G *v ?yp)" 
    unfolding maps matrix_vector_mult_def vec_lambda_beta Re_sum by auto
  also have " = 0" unfolding 0 by (simp add: vec_eq_iff maps)
  finally have 0: "?Re ?G *v yp = 0" .
  have "?Re ?G = 0" 
    by (rule pos_matrix_mult_0[OF _ pos_yp 0], auto simp: maps complex_Re_le_cmod)
  hence "?F = F" by (auto simp: maps vec_eq_iff cmod_eq_Re)
  with FA have AF: "cA = F" by simp
  from arg_cong[OF this, of "λ A. cis φ *k A"]
  have sim: "cis φ *k cA = inv_D ** cA ** D" unfolding F_def matrix.scale_scale cis_mult
    by simp
  have "similar_matrix (cis φ *k cA) cA" unfolding similar_matrix_def similar_matrix_wit_def
     sim
    by (rule exI[of _ inv_D