Theory Kohlberg_Neyman_Karlsson
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