# Theory Fekete

theory Fekete
imports Multivariate_Analysis
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

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.›

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

where "subadditive u = (∀m n. u (m+n) ≤ u m + u n)"

assumes "⋀m n. u (m+n) ≤ u m + u n"
unfolding subadditive_def using assms by auto

shows "u (m+n) ≤ u m + u n"
using assms unfolding subadditive_def by auto

"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)"

assumes "⋀m n. m > N0 ⟹ n > N0 ⟹ u (m+n) ≤ u m + u n"
unfolding eventually_subadditive_def using assms 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.)›

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)"
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.›

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

shows "(λm. ereal(u m/m)) ⇢ Inf {ereal(u n/n) | n. n>0}"

"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}"
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

"bdd_below {u n/n | n. n>0}"
shows "(λn. u n/n) ⇢ Inf {u n/n | n. n>0}"

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

"⋀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 (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 * by (simp add: divide_simps algebra_simps)
qed

"¬ (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}"
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

"¬ (bdd_below {u n/n | n. n>0})"
shows "(λn. ereal(u n/n)) ⇢ -∞"

sequences. We reformulate quickly some of the above results in this setting.›

where "superadditive u = (∀m n. u (m+n) ≥ u m + u n)"

"n > 0"
shows "u n ≥ n * u 1"

"⋀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)"
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

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
Such sequences appear notably when dealing with quasimorphisms.›

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)"
then have vle: "v n ≤ n * v 1" if "n > 0" for n
define w where "w = (λn. u n - C)"
then have wge: "w n ≥ n * w 1" if "n > 0" for n

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"
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"

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

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›

obtain N where *: "N>0" "⋀m. m≥N ⟹ w m/m < w n/n + e"
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}$.›

where "spectral_radius x = Inf {root n (norm(x^n))| n. n>0}"

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

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)