(* Author: Sébastien Gouëzel sebastien.gouezel@univ-nantes.fr License: BSD *) section ‹A theorem by Kohlberg and Neyman› theory Kohlberg_Neyman_Karlsson imports Fekete begin text ‹In this section, we prove a theorem due to Kohlberg and Neyman: given a semicontraction $T$ of a euclidean space, then $T^n(0)/n$ converges when $n \to \infty$. The proof we give is due to Karlsson. It mainly builds on subadditivity ideas. The geometry of the space is essentially not relevant except at the very end of the argument, where strict convexity comes into play.› text ‹We recall Fekete's lemma: if a sequence is subadditive (i.e., $u_{n+m}\leq u_n + u_m$), then $u_n/n$ converges to its infimum. It is proved in a different file, but we recall the statement for self-containedness.› lemma fekete: fixes u::"nat ⇒ real" assumes "⋀n m. u (m+n) ≤ u m + u n" "bdd_below {u n/n | n. n>0}" shows "(λn. u n/n) ⇢ Inf {u n/n | n. n>0}" apply (rule subadditive_converges_bounded) unfolding subadditive_def using assms by auto text ‹A real sequence tending to infinity has infinitely many high-scores, i.e., there are infinitely many times where it is larger than all its previous values.› lemma high_scores: fixes u::"nat ⇒ real" and i::nat assumes "u ⇢ ∞" shows "∃n ≥ i. ∀l ≤ n. u l ≤ u n" proof - define M where "M = Max {u l|l. l < i}" define n where "n = Inf {m. u m > M}" have "eventually (λm. u m > M) sequentially" using assms by (simp add: filterlim_at_top_dense tendsto_PInfty_eq_at_top) then have "{m. u m > M} ≠ {}" by fastforce then have "n ∈ {m. u m > M}" unfolding n_def using Inf_nat_def1 by metis then have "u n > M" by simp have "n ≥ i" proof (rule ccontr) assume " ¬ i ≤ n" then have *: "n < i" by simp have "u n ≤ M" unfolding M_def apply (rule Max_ge) using * by auto then show False using ‹u n > M› by auto qed moreover have "u l ≤ u n" if "l ≤ n" for l proof (cases "l = n") case True then show ?thesis by simp next case False then have "l < n" using ‹l ≤ n› by auto then have "l ∉ {m. u m > M}" unfolding n_def by (meson bdd_below_def cInf_lower not_le zero_le) then show ?thesis using ‹u n > M› by auto qed ultimately show ?thesis by auto qed text ‹Hahn-Banach in euclidean spaces: given a vector $u$, there exists a unit norm vector $v$ such that $\langle u, v \rangle = \|u\|$ (and we put a minus sign as we will use it in this form). This uses the fact that, in Isabelle/HOL, euclidean spaces have positive dimension by definition.› lemma select_unit_norm: fixes u::"'a::euclidean_space" shows "∃v. norm v = 1 ∧ v ∙ u = - norm u" proof (cases "u = 0") case True then show ?thesis using norm_Basis nonempty_Basis by fastforce next case False show ?thesis apply (rule exI[of _ "-u/⇩_{R}norm u"]) using False by (auto simp add: dot_square_norm power2_eq_square) qed text ‹We set up the assumption that we will use until the end of this file, in the following locale: we fix a semicontraction $T$ of a euclidean space. Our goal will be to show that such a semicontraction has an asymptotic translation vector.› locale Kohlberg_Neyman_Karlsson = fixes T::"'a::euclidean_space ⇒ 'a" assumes semicontract: "dist (T x) (T y) ≤ dist x y" begin text ‹The iterates of $T$ are still semicontractions, by induction.› lemma semicontract_Tn: "dist ((T^^n) x) ((T^^n) y) ≤ dist x y" apply (induction n, auto) using semicontract order_trans by blast text ‹The main quantity we will use is the distance from the origin to its image under $T^n$. We denote it by $u_n$. The main point is that it is subadditive by semicontraction, hence it converges to a limit $A$ given by $Inf \{u_n/n\}$, thanks to Fekete Lemma.› definition u::"nat ⇒ real" where "u n = dist 0 ((T^^n) 0)" definition A::real where "A = Inf {u n/n | n. n>0}" lemma Apos: "A ≥ 0" unfolding A_def u_def by (rule cInf_greatest, auto) lemma Alim:"(λn. u n/n) ⇢ A" unfolding A_def proof (rule fekete) show "bdd_below {u n / real n |n. 0 < n}" unfolding u_def bdd_below_def by (rule exI[of _ 0], auto) fix m n have "u (m+n) = dist 0 ((T^^(m+n)) 0)" unfolding u_def by simp also have "... ≤ dist 0 ((T^^m) 0) + dist ((T^^m) 0) ((T^^(m+n)) 0)" by (rule dist_triangle) also have "... = dist 0 ((T^^m) 0) + dist ((T^^m) 0) ((T^^m) ((T^^n) 0))" by (auto simp add: funpow_add) also have "... ≤ dist 0 ((T^^m) 0) + dist 0 ((T^^n) 0)" using semicontract_Tn[of m] add_mono_thms_linordered_semiring(2) by blast also have "... = u m + u n" unfolding u_def by auto finally show "u (m+n) ≤ u m + u n" by auto qed text ‹The main fact to prove the existence of an asymptotic translation vector for $T$ is the following proposition: there exists a unit norm vector $v$ such that $T^\ell(0)$ is in the half-space at distance $A \ell$ of the origin directed by $v$. The idea of the proof is to find such a vector $v_i$ that works (with a small error $\epsilon_i > 0$) for times up to a time $n_i$, and then take a limit by compactness (or weak compactness, but since we are in finite dimension, compactness works fine). Times $n_i$ are chosen to be large high scores of the sequence $u_n - (A-\epsilon_i) n$, which tends to infinity since $u_n/n$ tends to $A$.› proposition half_space: "∃v. norm v = 1 ∧ (∀l. v ∙ (T ^^ l) 0 ≤ - A * l)" proof - define eps::"nat ⇒ real" where "eps = (λi. 1/of_nat (i+1))" have "eps i > 0" for i unfolding eps_def by auto have "eps ⇢ 0" unfolding eps_def using LIMSEQ_ignore_initial_segment[OF lim_1_over_n, of 1] by simp have vi: "∃vi. norm vi = 1 ∧ (∀l ≤ i. vi ∙ (T ^^ l) 0 ≤ (- A + eps i) * l)" for i proof - have L: "(λn. ereal(u n - (A - eps i) * n)) ⇢ ∞" proof (rule Lim_transform_eventually) have "ereal ((u n/n - A) + eps i) * ereal n = ereal(u n - (A - eps i) * n)" if "n ≥ 1" for n using that by (auto simp add: divide_simps algebra_simps) then show "eventually (λn. ereal ((u n/n - A) + eps i) * ereal n = ereal(u n - (A - eps i) * n)) sequentially" unfolding eventually_sequentially by auto have "(λn. (ereal ((u n/n - A) + eps i)) * ereal n) ⇢ (0 + eps i) * ∞" apply (intro tendsto_intros) using ‹eps i > 0› Alim by (auto simp add: LIM_zero) then show "(λn. ereal (u n / real n - A + eps i) * ereal (real n)) ⇢ ∞" using ‹eps i > 0› by simp qed obtain n where n: "n ≥ i" "⋀l. l ≤ n ⟹ u l - (A - eps i) * l ≤ u n - (A - eps i) * n" using high_scores[OF L, of i] by auto obtain vi where vi: "norm vi = 1" "vi ∙ ((T^^n) 0) = - norm ((T^^n) 0)" using select_unit_norm by auto have "vi ∙ (T ^^ l) 0 ≤ (- A + eps i) * l" if "l ≤ i" for l proof - have *: "n = l + (n-l)" using that ‹n ≥ i› by auto have **: "real (n-l) = real n - real l" using that ‹n ≥ i› by auto have "vi ∙ (T ^^ l) 0 = vi ∙ ((T ^^ l) 0 - (T^^n) 0) + vi ∙ ((T^^n) 0)" by (simp add: inner_diff_right) also have "... ≤ norm vi * norm (((T ^^ l) 0 - (T^^n) 0)) + vi ∙ ((T^^n) 0)" by (simp add: norm_cauchy_schwarz) also have "... = dist ((T^^l)(0)) ((T^^n) 0) - norm ((T^^n) 0)" using vi by (auto simp add: dist_norm) also have "... = dist ((T^^l)(0)) ((T^^l) ((T^^(n-l)) 0)) - norm ((T^^n) 0)" by (metis * funpow_add o_apply) also have "... ≤ dist 0 ((T^^(n-l)) 0) - norm ((T^^n) 0)" using semicontract_Tn[of l 0 "(T^^(n-l)) 0"] by auto also have "... = u (n-l) - u n" unfolding u_def by auto also have "... ≤ - (A - eps i) * l" using n(2)[of "n-l"] unfolding ** by (auto simp add: algebra_simps) finally show ?thesis by auto qed then show ?thesis using vi(1) by auto qed have "∃V::(nat ⇒ 'a). ∀i. norm (V i) = 1 ∧ (∀l≤i. V i ∙ (T ^^ l) 0 ≤ (- A + eps i) * l)" apply (rule choice) using vi by auto then obtain V::"nat ⇒ 'a" where V: "⋀i. norm (V i) = 1" "⋀l i. l ≤ i ⟹ V i ∙ (T ^^ l) 0 ≤ (- A + eps i) * l" by auto have "compact (sphere (0::'a) 1)" by simp moreover have "V i ∈ sphere 0 1" for i using V(1) by auto ultimately have "∃v ∈ sphere 0 1. ∃r. strict_mono r ∧ (V o r) ⇢ v" using compact_eq_seq_compact_metric seq_compact_def by metis then obtain v r where v: "v ∈ sphere 0 1" "strict_mono r" "(V o r) ⇢ v" by auto have "v ∙ (T ^^ l) 0 ≤ - A * l" for l proof - have *: "(λi. (-A + eps (r i)) * l - V (r i) ∙ (T ^^ l) 0) ⇢ (-A + 0) * l - v ∙ (T ^^ l) 0" apply (intro tendsto_intros) using ‹(V o r) ⇢ v› ‹eps ⇢ 0› ‹strict_mono r› LIMSEQ_subseq_LIMSEQ unfolding comp_def by auto have "eventually (λi. (-A + eps (r i)) * l - V (r i) ∙ (T ^^ l) 0 ≥ 0) sequentially" unfolding eventually_sequentially apply (rule exI[of _ l]) using V(2)[of l] seq_suble[OF ‹strict_mono r›] apply auto using le_trans by blast then have " (-A + 0) * l - v ∙ (T ^^ l) 0 ≥ 0" using LIMSEQ_le_const[OF *, of 0] unfolding eventually_sequentially by auto then show ?thesis by auto qed then show ?thesis using ‹v ∈ sphere 0 1› by auto qed text ‹We can now show the existence of an asymptotic translation vector for $T$. It is the vector $-v$ of the previous proposition: the point $T^\ell(0)$ is in the half-space at distance $A \ell$ of the origin directed by $v$, and has norm $\sim A \ell$, hence it has to be essentially $-A v$ by strict convexity of the euclidean norm.› theorem KNK_thm: "convergent (λn. ((T^^n) 0) /⇩_{R}n)" proof - obtain v where v: "norm v = 1" "⋀l. v ∙ (T ^^ l) 0 ≤ - A * l" using half_space by auto have "(λn. norm(((T^^n) 0) /⇩_{R}n + A *⇩_{R}v)^2) ⇢ 0" proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. (norm((T^^n) 0) /⇩_{R}n)^2 - A^2"]) have "norm(((T^^n) 0) /⇩_{R}n + A *⇩_{R}v)^2 ≤ (norm((T^^n) 0) /⇩_{R}n)^2 - A^2" if "n ≥ 1" for n proof - have "norm(((T^^n) 0) /⇩_{R}n + A *⇩_{R}v)^2 = norm(((T^^n) 0) /⇩_{R}n)^2 + A * A * (norm v)^2 + 2 * A * inverse n * (v ∙ (T^^n) 0)" unfolding power2_norm_eq_inner by (auto simp add: inner_commute algebra_simps) also have "... ≤ norm(((T^^n) 0) /⇩_{R}n)^2 + A * A * (norm v)^2 + 2 * A * inverse n * (-A * n)" using mult_left_mono[OF v(2)[of n] Apos] ‹n ≥ 1› by (auto, auto simp add: divide_simps) also have "... = norm(((T^^n) 0) /⇩_{R}n)^2 - A * A" using ‹n ≥ 1› v(1) by auto finally show ?thesis by (simp add: power2_eq_square) qed then show "eventually (λn. norm ((T ^^ n) 0 /⇩_{R}real n + A *⇩_{R}v)^2 ≤ (norm ((T ^^ n) 0) /⇩_{R}real n)⇧^{2}- A^2) sequentially" unfolding eventually_sequentially by auto have "(λn. (norm ((T ^^ n) 0) /⇩_{R}real n)^2) ⇢ A⇧^{2}" apply (intro tendsto_intros) using Alim unfolding u_def by (auto simp add: divide_simps) then show "(λn. (norm ((T ^^ n) 0) /⇩_{R}real n)⇧^{2}- A⇧^{2}) ⇢ 0" by (simp add: LIM_zero) qed (auto) then have "(λn. sqrt((norm(((T^^n) 0) /⇩_{R}n + A *⇩_{R}v))^2)) ⇢ sqrt 0" by (intro tendsto_intros) then have "(λn. norm((((T^^n) 0) /⇩_{R}n) - (- A *⇩_{R}v))) ⇢ 0" by auto then have "(λn. ((T^^n) 0) /⇩_{R}n) ⇢ - A *⇩_{R}v" using Lim_null tendsto_norm_zero_iff by blast then show "convergent (λn. ((T^^n) 0) /⇩_{R}n)" unfolding convergent_def by auto qed end end (*of Kolberg_Neyman_Karlsson.thy*)