Theory Fekete

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section ‹Subadditive and submultiplicative sequences›

theory Fekete
  imports "HOL-Analysis.Multivariate_Analysis"
begin

text ‹A real sequence is subadditive if $u_{n+m} \leq u_n+u_m$. This implies the
convergence of $u_n/n$ to $Inf\{u_n/n\} \in [-\infty, +\infty)$, a useful result known
as Fekete lemma. We prove it below.

Taking logarithms, the same result applies to submultiplicative sequences. We illustrate
it with the definition of the spectral radius as the limit of $\|x^n\|^{1/n}$, the
convergence following from Fekete lemma.›


subsection ‹Subadditive sequences›

text ‹We define subadditive sequences, either from the start or eventually.›

definition subadditive::"(nat⇒real) ⇒ bool"
  where "subadditive u = (∀m n. u (m+n) ≤ u m + u n)"

lemma subadditiveI:
  assumes "⋀m n. u (m+n) ≤ u m + u n"
  shows "subadditive u"
unfolding subadditive_def using assms by auto

lemma subadditiveD:
  assumes "subadditive u"
  shows "u (m+n) ≤ u m + u n"
using assms unfolding subadditive_def by auto

lemma subadditive_un_le_nu1:
  assumes "subadditive u"
          "n > 0"
  shows "u n ≤ n * u 1"
proof -
  have *: "n = 0 ∨ (u n ≤ n * u 1)" for n
  proof (induction n)
    case 0
    then show ?case by auto
  next
    case (Suc n)
    consider "n = 0" | "n > 0" by auto
    then show ?case
    proof (cases)
      case 1
      then show ?thesis by auto
    next
      case 2
      then have "u (Suc n) ≤ u n + u 1" using subadditiveD[OF assms(1), of n 1] by auto
      then show ?thesis using Suc.IH 2 by (auto simp add: algebra_simps)
    qed
  qed
  show ?thesis using *[of n] ‹n > 0› by auto
qed

definition eventually_subadditive::"(nat⇒real) ⇒ nat ⇒ bool"
  where "eventually_subadditive u N0 = (∀m>N0. ∀n>N0. u (m+n) ≤ u m + u n)"

lemma eventually_subadditiveI:
  assumes "⋀m n. m > N0 ⟹ n > N0 ⟹ u (m+n) ≤ u m + u n"
  shows "eventually_subadditive u N0"
unfolding eventually_subadditive_def using assms by auto

lemma subadditive_imp_eventually_subadditive:
  assumes "subadditive u"
  shows "eventually_subadditive u 0"
using assms unfolding subadditive_def eventually_subadditive_def by auto

text ‹The main inequality that will lead to convergence is given in the next lemma:
given $n$, then eventually $u_m/m$ is bounded by $u_n/n$, up to an arbitrarily small error.
This is proved by doing the euclidean division of $m$ by $n$ and using the subadditivity.
(the remainder in the euclidean division will give the error term.)›

lemma eventually_subadditive_ineq:
  assumes "eventually_subadditive u N0" "e>0" "n>N0"
  shows "∃N>N0. ∀m≥N. u m/m < u n/n + e"
proof -
  have ineq_rec: "u(a*n+r) ≤ a * u n + u r" if "n>N0" "r>N0" for a n r
  proof (induct a)
    case (Suc a)
    have "a*n+r>N0" using ‹r>N0› by simp
    have "u((Suc a)*n+r) = u(a*n+r+n)" by (simp add: algebra_simps)
    also have "... ≤ u(a*n+r)+u n" using assms ‹n>N0› ‹a*n+r>N0› eventually_subadditive_def by blast
    also have "... ≤ a*u n + u r + u n" by (simp add: Suc.hyps)
    also have "... = (Suc a) * u n + u r" by (simp add: algebra_simps)
    finally show ?case by simp
  qed (simp)

  have "n>0" "real n > 0" using ‹n>N0› by auto
  define C where "C = Max {abs(u i) |i. i≤2*n}"
  have ineq_C: "abs(u i) ≤ C" if "i ≤ 2 * n" for i
    unfolding C_def by (intro Max_ge, auto simp add: that)

  have ineq_all_m: "u m/m ≤ u n/n + 3*C/m" if "m≥n" for m
  proof -
    have "real m>0" using ‹m≥n› ‹0 < real n› by linarith

    obtain a0 r0 where "r0<n" "m = a0*n+r0"
      using ‹0 < n› mod_div_decomp mod_less_divisor by blast
    define a where "a = a0-1"
    define r where "r = r0+n"
    have "r<2*n" "r≥n" unfolding r_def by (auto simp add: ‹r0<n›)
    have "a0>0" using ‹m = a0*n + r0› ‹n ≤ m› ‹r0 < n› not_le by fastforce
    then have "m = a * n + r" using a_def r_def ‹m = a0*n+r0› mult_eq_if by auto
    then have real_eq: "-r = real n * a - m" by simp

    have "r>N0" using ‹r≥n› ‹n>N0› by simp
    then have "u m ≤ a * u n + u r" using ineq_rec ‹m = a*n+r› ‹n>N0› by simp
    then have "n * u m ≤ n * (a * u n + u r)" using ‹real n>0› by simp
    then have "n * u m - m * u n ≤ -r * u n + n * u r"
      unfolding real_eq by (simp add: algebra_simps)
    also have "... ≤ r * abs(u n) + n * abs(u r)"
      apply (intro add_mono mult_left_mono) using real_0_le_add_iff by fastforce+
    also have "... ≤ (2 * n) * C + n * C"
      apply (intro add_mono mult_mono ineq_C) using less_imp_le[OF ‹r < 2 * n›] by auto
    finally have "n * u m - m * u n ≤ 3*C*n" by auto
    then show "u m/m ≤ u n/n + 3*C/m"
      using ‹0 < real n› ‹0 < real m› by (simp add: divide_simps mult.commute)
  qed

  obtain M::nat where M: "M ≥ 3 * C / e" using real_nat_ceiling_ge by auto
  define N where "N = M + n + N0 + 1"
  have "N > 3 * C / e" "N ≥ n" "N > N0" unfolding N_def using M by auto
  have "u m/m < u n/n + e" if "m ≥ N" for m
  proof -
    have "3 * C / m < e"
      using that ‹N > 3 * C / e› ‹e > 0› apply (auto simp add: algebra_simps divide_simps)
      by (meson le_less_trans linorder_not_le mult_less_cancel_left_pos of_nat_less_iff)
    then show ?thesis using ineq_all_m[of m] ‹n ≤ N› ‹N ≤ m› by auto
  qed
  then show ?thesis using ‹N0 < N› by blast
qed

text ‹From the inequality above, we deduce the convergence of $u_n/n$ to its infimum. As this
infimum might be $-\infty$, we formulate this convergence in the extended reals. Then, we
specialize it to the real situation, separating the cases where $u_n/n$ is bounded below or not.›

lemma subadditive_converges_ereal':
  assumes "eventually_subadditive u N0"
  shows "(λm. ereal(u m/m)) ⇢ Inf {ereal(u n/n) | n. n>N0}"
proof -
  define v where "v = (λm. ereal(u m/m))"
  define V where "V = {v n | n. n>N0}"
  define l where "l = Inf V"

  have "⋀t. t∈V ⟹ t≥l" by (simp add: Inf_lower l_def)
  then have "v n ≥ l" if "n > N0" for n using V_def that by blast
  then have lower: "eventually (λn. a < v n) sequentially" if "a < l" for a
    by (meson that dual_order.strict_trans1 eventually_at_top_dense)

  have upper: "eventually (λn. a > v n) sequentially" if "a > l" for a
  proof -
    obtain t where "t∈V" "t<a" by (metis ‹a>l› Inf_greatest l_def not_le)
    then obtain e::real where "e>0" "t+e < a" by (meson ereal_le_epsilon2 leD le_less_linear)
    obtain n where "n>N0" "t = u n/n" using V_def v_def ‹t ∈ V› by blast
    then have "u n/n + e < a" using ‹t+e < a› by simp
    obtain N where "∀m≥N. u m/m < u n/n + e"
      using eventually_subadditive_ineq[OF assms] ‹0 < e› ‹N0 < n› by blast
    then have "u m/m < a" if "m ≥ N" for m
      using that ‹u n/n + e < a› less_ereal.simps(1) less_trans by blast
    then have "v m< a" if "m ≥ N" for m using v_def that by blast
    then show ?thesis using eventually_at_top_linorder by auto
  qed
  show ?thesis
    using lower upper unfolding V_def l_def v_def by (simp add: order_tendsto_iff)
qed

lemma subadditive_converges_ereal:
  assumes "subadditive u"
  shows "(λm. ereal(u m/m)) ⇢ Inf {ereal(u n/n) | n. n>0}"
by (rule subadditive_converges_ereal'[OF subadditive_imp_eventually_subadditive[OF assms]])

lemma subadditive_converges_bounded':
  assumes "eventually_subadditive u N0"
          "bdd_below {u n/n | n. n>N0}"
  shows "(λn. u n/n) ⇢ Inf {u n/n | n. n>N0}"
proof-
  have *: "(λn. ereal(u n /n)) ⇢ Inf {ereal(u n/n)|n. n > N0}"
    by (simp add: assms(1) subadditive_converges_ereal')
  define V where "V = {u n/n | n. n>N0}"
  have a: "bdd_below V" "V≠{}" by (auto simp add: V_def assms(2))
  have "Inf {ereal(t)| t. t∈V} = ereal(Inf V)" by (subst ereal_Inf'[OF a], simp add: Setcompr_eq_image)
  moreover have "{ereal(t)| t. t∈V} = {ereal(u n/n)|n. n > N0}" using V_def by blast
  ultimately have "Inf {ereal(u n/n)|n. n > N0} = ereal(Inf {u n/n |n. n > N0})" using V_def by auto
  then have "(λn. ereal(u n /n)) ⇢ ereal(Inf {u n/n | n. n>N0})" using * by auto
  then show ?thesis by simp
qed

lemma subadditive_converges_bounded:
  assumes "subadditive u"
          "bdd_below {u n/n | n. n>0}"
  shows "(λn. u n/n) ⇢ Inf {u n/n | n. n>0}"
by (rule subadditive_converges_bounded'[OF subadditive_imp_eventually_subadditive[OF assms(1)] assms(2)])

text ‹We reformulate the previous lemma in a more directly usable form, avoiding the infimum.›

lemma subadditive_converges_bounded'':
  assumes "subadditive u"
          "⋀n. n > 0 ⟹ u n ≥ n * (a::real)"
  shows "∃l. (λn. u n / n) ⇢ l ∧ (∀n>0. u n ≥ n * l)"
proof -
  have B: "bdd_below {u n/n | n. n>0}"
    apply (rule bdd_belowI[of _ a]) using assms(2)
    apply (auto simp add: divide_simps)
    apply (metis mult.commute mult_left_le_imp_le of_nat_0_less_iff)
    done
  define l where "l = Inf {u n/n | n. n>0}"
  have *: "u n / n ≥ l" if "n > 0" for n
    unfolding l_def using that by (auto intro!: cInf_lower[OF _ B])
  show ?thesis
    apply (rule exI[of _ l], auto)
    using subadditive_converges_bounded[OF assms(1) B] apply (simp add: l_def)
    using * by (simp add: divide_simps algebra_simps)
qed

lemma subadditive_converges_unbounded':
  assumes "eventually_subadditive u N0"
          "¬ (bdd_below {u n/n | n. n>N0})"
  shows "(λn. ereal(u n/n)) ⇢ -∞"
proof -
  have *: "(λn. ereal(u n /n)) ⇢ Inf {ereal(u n/n)|n. n > N0}"
    by (simp add: assms(1) subadditive_converges_ereal')
  define V where "V = {u n/n | n. n>N0}"
  then have "¬ bdd_below V" using assms by simp
  have "Inf {ereal(t) | t. t∈V} = -∞"
    by (rule ereal_bot, metis (mono_tags, lifting) ‹¬ bdd_below V› bdd_below_def
        leI Inf_lower2 ereal_less_eq(3) le_less mem_Collect_eq)
  moreover have "{ereal(t)| t. t∈V} = {ereal(u n/n)|n. n > N0}" using V_def by blast
  ultimately have "Inf {ereal(u n/n)|n. n > N0} = -∞" by auto
  then show ?thesis using * by simp
qed

lemma subadditive_converges_unbounded:
  assumes "subadditive u"
          "¬ (bdd_below {u n/n | n. n>0})"
  shows "(λn. ereal(u n/n)) ⇢ -∞"
by (rule subadditive_converges_unbounded'[OF subadditive_imp_eventually_subadditive[OF assms(1)] assms(2)])

subsection ‹Superadditive sequences›

text ‹While most applications involve subadditive sequences, one sometimes encounters superadditive
sequences. We reformulate quickly some of the above results in this setting.›

definition superadditive::"(nat⇒real) ⇒ bool"
  where "superadditive u = (∀m n. u (m+n) ≥ u m + u n)"

lemma subadditive_of_superadditive:
  assumes "superadditive u"
  shows "subadditive (λn. -u n)"
using assms unfolding superadditive_def subadditive_def by (auto simp add: algebra_simps)

lemma superadditive_un_ge_nu1:
  assumes "superadditive u"
          "n > 0"
  shows "u n ≥ n * u 1"
using subadditive_un_le_nu1[OF subadditive_of_superadditive[OF assms(1)] assms(2)] by auto

lemma superadditive_converges_bounded'':
  assumes "superadditive u"
          "⋀n. n > 0 ⟹ u n ≤ n * (a::real)"
  shows "∃l. (λn. u n / n) ⇢ l ∧ (∀n>0. u n ≤ n * l)"
proof -
  have "∃l. (λn. -u n / n) ⇢ l ∧ (∀n>0. -u n ≥ n * l)"
    apply (rule subadditive_converges_bounded''[OF subadditive_of_superadditive[OF assms(1)], of "-a"])
    using assms(2) by auto
  then obtain l where l: "(λn. -u n / n) ⇢ l" "(∀n>0. -u n ≥ n * l)" by blast
  have "(λn. -((-u n)/n)) ⇢ -l"
    by (intro tendsto_intros l)
  moreover have "∀n>0. u n ≤ n * (-l)"
    using l(2) by (auto simp add: algebra_simps) (metis minus_equation_iff neg_le_iff_le)
  ultimately show ?thesis
    by auto
qed


subsection ‹Almost additive sequences›

text ‹One often encounters sequences which are both subadditive and superadditive, but only up
to an additive constant. Adding or subtracting this constant, one can make the sequence
genuinely subadditive or superadditive, and thus deduce results about its convergence, as follows.
Such sequences appear notably when dealing with quasimorphisms.›

lemma almost_additive_converges:
  fixes u::"nat ⇒ real"
  assumes "⋀m n. abs(u(m+n) - u m - u n) ≤ C"
  shows "convergent (λn. u n/n)"
        "abs(u k - k * lim (λn. u n / n)) ≤ C"
proof -
  have "(abs (u 0)) ≤ C" using assms[of 0 0] by auto
  then have "C ≥ 0" by auto

  define v where "v = (λn. u n + C)"
  have "subadditive v"
    unfolding subadditive_def v_def using assms by (auto simp add: algebra_simps abs_diff_le_iff)
  then have vle: "v n ≤ n * v 1" if "n > 0" for n
    using subadditive_un_le_nu1 that by auto
  define w where "w = (λn. u n - C)"
  have "superadditive w"
    unfolding superadditive_def w_def using assms by (auto simp add: algebra_simps abs_diff_le_iff)
  then have wge: "w n ≥ n * w 1" if "n > 0" for n
    using superadditive_un_ge_nu1 that by auto

  have I: "v n ≥ w n" for n
    unfolding v_def w_def using ‹C ≥ 0› by auto
  then have *: "v n ≥ n * w 1" if "n > 0" for n using order_trans[OF wge[OF that]] by auto
  then obtain lv where lv: "(λn. v n/n) ⇢ lv" "⋀n. n > 0 ⟹ v n ≥ n * lv"
    using subadditive_converges_bounded''[OF ‹subadditive v› *] by auto
  have *: "w n ≤ n * v 1" if "n > 0" for n using order_trans[OF _ vle[OF that]] I by auto
  then obtain lw where lw: "(λn. w n/n) ⇢ lw" "⋀n. n > 0 ⟹ w n ≤ n * lw"
    using superadditive_converges_bounded''[OF ‹superadditive w› *] by auto

  have *: "v n/n = w n /n + 2*C*(1/n)" for n
    unfolding v_def w_def by (auto simp add: algebra_simps divide_simps)
  have "(λn. w n /n + 2*C*(1/n)) ⇢ lw + 2*C*0"
    by (intro tendsto_add tendsto_mult lim_1_over_n lw, auto)
  then have "lw = lv"
    unfolding *[symmetric] using lv(1) LIMSEQ_unique by auto

  have *: "u n/n = w n /n + C*(1/n)" for n
    unfolding w_def by (auto simp add: algebra_simps divide_simps)
  have "(λn. u n /n) ⇢ lw + C*0"
    unfolding * by (intro tendsto_add tendsto_mult lim_1_over_n lw, auto)
  then have lu: "convergent (λn. u n/n)" "lim (λn. u n/n) = lw"
    by (auto simp add: convergentI limI)
  then show "convergent (λn. u n/n)" by simp

  show "abs(u k - k * lim (λn. u n / n)) ≤ C"
  proof (cases "k>0")
    case False
    then show ?thesis using assms[of 0 0] by auto
  next
    case True
    have "u k - k * lim (λn. u n/n) = v k - C - k * lv" unfolding lu(2) ‹lw = lv› v_def by auto
    also have "... ≥ -C" using lv(2)[OF True] by auto
    finally have A: "u k - k * lim (λn. u n/n) ≥ - C" by simp
    have "u k - k * lim (λn. u n/n) = w k + C - k * lw" unfolding lu(2) w_def by auto
    also have "... ≤ C" using lw(2)[OF True] by auto
    finally show ?thesis using A by auto
  qed
qed


subsection ‹Submultiplicative sequences, application to the spectral radius›

text ‹In the same way as subadditive sequences, one may define submultiplicative sequences.
Essentially, a sequence is submultiplicative if its logarithm is subadditive. A difference is
that we allow a submultiplicative sequence to take the value $0$, as this shows up in applications.
This implies that we have to distinguish in the proofs the situations where the value $0$
is taken or not. In the latter situation, we can use directly the results from the
subadditive case to deduce convergence. In the former situation, convergence to $0$ is obvious
as the sequence vanishes eventually.›

lemma submultiplicative_converges:
  fixes u::"nat⇒real"
  assumes "⋀n. u n ≥ 0"
          "⋀m n. u (m+n) ≤ u m * u n"
  shows "(λn. root n (u n))⇢ Inf {root n (u n) | n. n>0}"
proof -
  define v where "v = (λ n. root n (u n))"
  define V where "V = {v n | n. n>0}"
  then have "V ≠ {}" by blast
  have "t ≥ 0" if "t ∈ V" for t using that V_def v_def assms(1) by auto
  then have "Inf V ≥ 0" by (simp add: ‹V ≠ {}› cInf_greatest)
  have "bdd_below V" by (meson ‹⋀t. t ∈ V ⟹ 0 ≤ t› bdd_below_def)

  show ?thesis
  proof cases
    assume "∃n. u n = 0"
    then obtain n where "u n = 0" by auto
    then have "u m = 0" if "m ≥ n" for m by (metis that antisym_conv assms(1) assms(2) le_Suc_ex mult_zero_left)
    then have *: "v m = 0" if "m ≥ n" for m using v_def that by simp
    then have "v ⇢ 0" using lim_explicit by force

    have "v (Suc n) ∈ V" using V_def by blast
    moreover have "v (Suc n) = 0" using * by auto
    ultimately have "Inf V ≤ 0" by (simp add: ‹bdd_below V› cInf_lower)
    then have "Inf V = 0" using ‹0 ≤ Inf V› by auto
    then show ?thesis using V_def v_def ‹v ⇢ 0› by auto
  next
    assume "¬ (∃n. u n = 0)"
    then have "u n > 0" for n by (metis assms(1) less_eq_real_def)
    define w where "w n = ln (u n)" for n
    have express_vn: "v n = exp(w n/n)" if "n>0" for n
    proof -
      have "(exp(w n/n))^n = exp(n*(w n/n))" by (metis exp_of_nat_mult)
      also have "... = exp(w n)" by (simp add: ‹0 < n›)
      also have "... = u n" by (simp add: ‹⋀n. 0 < u n› w_def)
      finally have "exp(w n/n) = root n (u n)" by (metis ‹0 < n› exp_ge_zero real_root_power_cancel)
      then show ?thesis unfolding v_def by simp
    qed

    have "eventually_subadditive w 0"
    proof (rule eventually_subadditiveI)
      fix m n
      have "w (m+n) = ln (u (m+n))" by (simp add: w_def)
      also have "... ≤ ln(u m * u n)"
        by (meson ‹⋀n. 0 < u n› assms(2) zero_less_mult_iff ln_le_cancel_iff)
      also have "... = ln(u m) + ln(u n)" by (simp add: ‹⋀n. 0 < u n› ln_mult)
      also have "... = w m + w n" by (simp add: w_def)
      finally show "w (m+n) ≤ w m + w n".
    qed

    define l where "l = Inf V"
    then have "v n≥l" if "n > 0" for n
      using V_def that by (metis (mono_tags, lifting) ‹bdd_below V› cInf_lower mem_Collect_eq)
    then have lower: "eventually (λn. a < v n) sequentially" if "a < l" for a
      by (meson that dual_order.strict_trans1 eventually_at_top_dense)

    have upper: "eventually (λn. a > v n) sequentially" if "a > l" for a
    proof -
      obtain t where "t∈V" "t < a" using ‹V ≠ {}› cInf_lessD l_def ‹a>l› by blast
      then have "t > 0" using V_def ‹⋀n. 0 < u n› v_def by auto
      then have "a/t > 1" using ‹t<a› by simp
      define e where "e = ln(a/t)/2"
      have "e > 0" "e < ln(a/t)" unfolding e_def by (simp_all add: ‹1 < a / t› ln_gt_zero)
      then have "exp(e) < a/t" by (metis ‹1 < a / t› exp_less_cancel_iff exp_ln less_trans zero_less_one)

      obtain n where "n>0" "t = v n" using V_def v_def ‹t ∈ V› by blast
      with ‹0 < t› have "v n * exp(e) < a" using ‹exp(e) < a/t›
        by (auto simp add: field_simps)

      obtain N where *: "N>0" "⋀m. m≥N ⟹ w m/m < w n/n + e"
        using eventually_subadditive_ineq[OF ‹eventually_subadditive w 0›] ‹0 < n› ‹e>0› by blast
      have "v m < a" if "m ≥ N" for m
      proof -
        have "m>0" using that ‹N>0› by simp
        have "w m/m < w n/n + e" by (simp add: ‹N ≤ m› *)
        then have "exp(w m/m) < exp(w n/n + e)" by simp
        also have "... = exp(w n/n) * exp(e)" by (simp add: mult_exp_exp)
        finally have "v m < v n * exp(e)" using express_vn ‹m>0› ‹n>0› by simp
        then show "v m < a" using ‹v n * exp(e) < a› by simp
      qed
      then show ?thesis using eventually_at_top_linorder by auto
    qed

    show ?thesis
      using lower upper unfolding v_def l_def V_def by (simp add: order_tendsto_iff)
  qed
qed

text ‹An important application of submultiplicativity is to prove the existence of the
spectral radius of a matrix, as the limit of $\|A^n\|^{1/n}$.›

definition spectral_radius::"'a::real_normed_algebra_1 ⇒ real"
  where "spectral_radius x = Inf {root n (norm(x^n))| n. n>0}"

lemma spectral_radius_aux:
  fixes x::"'a::real_normed_algebra_1"
  defines "V ≡ {root n (norm(x^n))| n. n>0}"
  shows "⋀t. t∈V ⟹ t ≥ spectral_radius x"
        "⋀t. t∈V ⟹ t ≥ 0"
        "bdd_below V"
        "V ≠ {}"
        "Inf V ≥ 0"
proof -
  show "V≠{}" using V_def by blast
  show *: "t ≥ 0" if "t ∈ V" for t using that unfolding V_def using real_root_pos_pos_le by auto
  then show "bdd_below V" by (meson bdd_below_def)
  then show "Inf V ≥ 0" by (simp add: ‹V ≠ {}› * cInf_greatest)
  show "⋀t. t∈V ⟹ t ≥ spectral_radius x" by (metis (mono_tags, lifting) ‹bdd_below V› assms cInf_lower spectral_radius_def)
qed

lemma spectral_radius_nonneg [simp]:
  "spectral_radius x ≥ 0"
by (simp add: spectral_radius_aux(5) spectral_radius_def)

lemma spectral_radius_upper_bound [simp]:
  "(spectral_radius x)^n ≤ norm(x^n)"
proof (cases)
  assume "¬(n = 0)"
  have "root n (norm(x^n)) ≥ spectral_radius x"
    using spectral_radius_aux ‹n ≠ 0› by auto
  then show ?thesis
    by (metis ‹n ≠ 0› spectral_radius_nonneg norm_ge_zero not_gr0 power_mono real_root_pow_pos2)
qed (simp)

lemma spectral_radius_limit:
  "(λn. root n (norm(x^n))) ⇢ spectral_radius x"
proof -
  have "norm(x^(m+n)) ≤ norm(x^m) * norm(x^n)" for m n by (simp add: power_add norm_mult_ineq)
  then show ?thesis unfolding spectral_radius_def using submultiplicative_converges by auto
qed

end (*of Fekete.thy*)