(* 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*)