src/HOL/Library/Liminf_Limsup.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62343 24106dc44def
child 62624 59ceeb6f3079
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     1 (*  Title:      HOL/Library/Liminf_Limsup.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Manuel Eberl, TU München
     4 *)
     5 
     6 section \<open>Liminf and Limsup on complete lattices\<close>
     7 
     8 theory Liminf_Limsup
     9 imports Complex_Main
    10 begin
    11 
    12 lemma le_Sup_iff_less:
    13   fixes x :: "'a :: {complete_linorder, dense_linorder}"
    14   shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
    15   unfolding le_SUP_iff
    16   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    17 
    18 lemma Inf_le_iff_less:
    19   fixes x :: "'a :: {complete_linorder, dense_linorder}"
    20   shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    21   unfolding INF_le_iff
    22   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    23 
    24 lemma SUP_pair:
    25   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    26   shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    27   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    28 
    29 lemma INF_pair:
    30   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    31   shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    32   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    33 
    34 subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
    35 
    36 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    37   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
    38 
    39 definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    40   "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
    41 
    42 abbreviation "liminf \<equiv> Liminf sequentially"
    43 
    44 abbreviation "limsup \<equiv> Limsup sequentially"
    45 
    46 lemma Liminf_eqI:
    47   "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
    48     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    49   unfolding Liminf_def by (auto intro!: SUP_eqI)
    50 
    51 lemma Limsup_eqI:
    52   "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
    53     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    54   unfolding Limsup_def by (auto intro!: INF_eqI)
    55 
    56 lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
    57   unfolding Liminf_def eventually_sequentially
    58   by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
    59 
    60 lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
    61   unfolding Limsup_def eventually_sequentially
    62   by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
    63 
    64 lemma Limsup_const:
    65   assumes ntriv: "\<not> trivial_limit F"
    66   shows "Limsup F (\<lambda>x. c) = c"
    67 proof -
    68   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    69   have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
    70     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
    71   then show ?thesis
    72     unfolding Limsup_def using eventually_True
    73     by (subst INF_cong[where D="\<lambda>x. c"])
    74        (auto intro!: INF_const simp del: eventually_True)
    75 qed
    76 
    77 lemma Liminf_const:
    78   assumes ntriv: "\<not> trivial_limit F"
    79   shows "Liminf F (\<lambda>x. c) = c"
    80 proof -
    81   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    82   have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
    83     using ntriv by (intro INF_const) (auto simp: eventually_False *)
    84   then show ?thesis
    85     unfolding Liminf_def using eventually_True
    86     by (subst SUP_cong[where D="\<lambda>x. c"])
    87        (auto intro!: SUP_const simp del: eventually_True)
    88 qed
    89 
    90 lemma Liminf_mono:
    91   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
    92   shows "Liminf F f \<le> Liminf F g"
    93   unfolding Liminf_def
    94 proof (safe intro!: SUP_mono)
    95   fix P assume "eventually P F"
    96   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
    97   then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
    98     by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
    99 qed
   100 
   101 lemma Liminf_eq:
   102   assumes "eventually (\<lambda>x. f x = g x) F"
   103   shows "Liminf F f = Liminf F g"
   104   by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
   105 
   106 lemma Limsup_mono:
   107   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   108   shows "Limsup F f \<le> Limsup F g"
   109   unfolding Limsup_def
   110 proof (safe intro!: INF_mono)
   111   fix P assume "eventually P F"
   112   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   113   then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
   114     by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
   115 qed
   116 
   117 lemma Limsup_eq:
   118   assumes "eventually (\<lambda>x. f x = g x) net"
   119   shows "Limsup net f = Limsup net g"
   120   by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
   121 
   122 lemma Liminf_le_Limsup:
   123   assumes ntriv: "\<not> trivial_limit F"
   124   shows "Liminf F f \<le> Limsup F f"
   125   unfolding Limsup_def Liminf_def
   126   apply (rule SUP_least)
   127   apply (rule INF_greatest)
   128 proof safe
   129   fix P Q assume "eventually P F" "eventually Q F"
   130   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   131   then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
   132     using ntriv by (auto simp add: eventually_False)
   133   have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
   134     by (rule INF_mono) auto
   135   also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
   136     using not_False by (intro INF_le_SUP) auto
   137   also have "\<dots> \<le> SUPREMUM (Collect Q) f"
   138     by (rule SUP_mono) auto
   139   finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
   140 qed
   141 
   142 lemma Liminf_bounded:
   143   assumes ntriv: "\<not> trivial_limit F"
   144   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   145   shows "C \<le> Liminf F X"
   146   using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
   147 
   148 lemma Limsup_bounded:
   149   assumes ntriv: "\<not> trivial_limit F"
   150   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   151   shows "Limsup F X \<le> C"
   152   using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
   153 
   154 lemma le_Limsup:
   155   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
   156   shows "l \<le> Limsup F f"
   157 proof -
   158   have "l = Limsup F (\<lambda>x. l)"
   159     using F by (simp add: Limsup_const)
   160   also have "\<dots> \<le> Limsup F f"
   161     by (intro Limsup_mono x)
   162   finally show ?thesis .
   163 qed
   164 
   165 lemma le_Liminf_iff:
   166   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   167   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   168 proof -
   169   have "eventually (\<lambda>x. y < X x) F"
   170     if "eventually P F" "y < INFIMUM (Collect P) X" for y P
   171     using that by (auto elim!: eventually_mono dest: less_INF_D)
   172   moreover
   173   have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
   174     if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
   175   proof (cases "\<exists>z. y < z \<and> z < C")
   176     case True
   177     then obtain z where z: "y < z \<and> z < C" ..
   178     moreover from z have "z \<le> INFIMUM {x. z < X x} X"
   179       by (auto intro!: INF_greatest)
   180     ultimately show ?thesis
   181       using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   182   next
   183     case False
   184     then have "C \<le> INFIMUM {x. y < X x} X"
   185       by (intro INF_greatest) auto
   186     with \<open>y < C\<close> show ?thesis
   187       using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   188   qed
   189   ultimately show ?thesis
   190     unfolding Liminf_def le_SUP_iff by auto
   191 qed
   192 
   193 lemma Limsup_le_iff:
   194   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   195   shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
   196 proof -
   197   { fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
   198     then have "eventually (\<lambda>x. y > X x) F"
   199       by (auto elim!: eventually_mono dest: SUP_lessD) }
   200   moreover
   201   { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
   202     have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X"
   203     proof (cases "\<exists>z. C < z \<and> z < y")
   204       case True
   205       then obtain z where z: "C < z \<and> z < y" ..
   206       moreover from z have "z \<ge> SUPREMUM {x. z > X x} X"
   207         by (auto intro!: SUP_least)
   208       ultimately show ?thesis
   209         using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
   210     next
   211       case False
   212       then have "C \<ge> SUPREMUM {x. y > X x} X"
   213         by (intro SUP_least) (auto simp: not_less)
   214       with \<open>y > C\<close> show ?thesis
   215         using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
   216     qed }
   217   ultimately show ?thesis
   218     unfolding Limsup_def INF_le_iff by auto
   219 qed
   220 
   221 lemma less_LiminfD:
   222   "y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F"
   223   using le_Liminf_iff[of "Liminf F f" F f] by simp
   224 
   225 lemma Limsup_lessD:
   226   "y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F"
   227   using Limsup_le_iff[of F f "Limsup F f"] by simp
   228 
   229 lemma lim_imp_Liminf:
   230   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   231   assumes ntriv: "\<not> trivial_limit F"
   232   assumes lim: "(f \<longlongrightarrow> f0) F"
   233   shows "Liminf F f = f0"
   234 proof (intro Liminf_eqI)
   235   fix P assume P: "eventually P F"
   236   then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
   237     by eventually_elim (auto intro!: INF_lower)
   238   then show "INFIMUM (Collect P) f \<le> f0"
   239     by (rule tendsto_le[OF ntriv lim tendsto_const])
   240 next
   241   fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
   242   show "f0 \<le> y"
   243   proof cases
   244     assume "\<exists>z. y < z \<and> z < f0"
   245     then obtain z where "y < z \<and> z < f0" ..
   246     moreover have "z \<le> INFIMUM {x. z < f x} f"
   247       by (rule INF_greatest) simp
   248     ultimately show ?thesis
   249       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   250   next
   251     assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
   252     show ?thesis
   253     proof (rule classical)
   254       assume "\<not> f0 \<le> y"
   255       then have "eventually (\<lambda>x. y < f x) F"
   256         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   257       then have "eventually (\<lambda>x. f0 \<le> f x) F"
   258         using discrete by (auto elim!: eventually_mono)
   259       then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
   260         by (rule upper)
   261       moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
   262         by (intro INF_greatest) simp
   263       ultimately show "f0 \<le> y" by simp
   264     qed
   265   qed
   266 qed
   267 
   268 lemma lim_imp_Limsup:
   269   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   270   assumes ntriv: "\<not> trivial_limit F"
   271   assumes lim: "(f \<longlongrightarrow> f0) F"
   272   shows "Limsup F f = f0"
   273 proof (intro Limsup_eqI)
   274   fix P assume P: "eventually P F"
   275   then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
   276     by eventually_elim (auto intro!: SUP_upper)
   277   then show "f0 \<le> SUPREMUM (Collect P) f"
   278     by (rule tendsto_le[OF ntriv tendsto_const lim])
   279 next
   280   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
   281   show "y \<le> f0"
   282   proof (cases "\<exists>z. f0 < z \<and> z < y")
   283     case True
   284     then obtain z where "f0 < z \<and> z < y" ..
   285     moreover have "SUPREMUM {x. f x < z} f \<le> z"
   286       by (rule SUP_least) simp
   287     ultimately show ?thesis
   288       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   289   next
   290     case False
   291     show ?thesis
   292     proof (rule classical)
   293       assume "\<not> y \<le> f0"
   294       then have "eventually (\<lambda>x. f x < y) F"
   295         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   296       then have "eventually (\<lambda>x. f x \<le> f0) F"
   297         using False by (auto elim!: eventually_mono simp: not_less)
   298       then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
   299         by (rule lower)
   300       moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
   301         by (intro SUP_least) simp
   302       ultimately show "y \<le> f0" by simp
   303     qed
   304   qed
   305 qed
   306 
   307 lemma Liminf_eq_Limsup:
   308   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   309   assumes ntriv: "\<not> trivial_limit F"
   310     and lim: "Liminf F f = f0" "Limsup F f = f0"
   311   shows "(f \<longlongrightarrow> f0) F"
   312 proof (rule order_tendstoI)
   313   fix a assume "f0 < a"
   314   with assms have "Limsup F f < a" by simp
   315   then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
   316     unfolding Limsup_def INF_less_iff by auto
   317   then show "eventually (\<lambda>x. f x < a) F"
   318     by (auto elim!: eventually_mono dest: SUP_lessD)
   319 next
   320   fix a assume "a < f0"
   321   with assms have "a < Liminf F f" by simp
   322   then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
   323     unfolding Liminf_def less_SUP_iff by auto
   324   then show "eventually (\<lambda>x. a < f x) F"
   325     by (auto elim!: eventually_mono dest: less_INF_D)
   326 qed
   327 
   328 lemma tendsto_iff_Liminf_eq_Limsup:
   329   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   330   shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   331   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
   332 
   333 lemma liminf_subseq_mono:
   334   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   335   assumes "subseq r"
   336   shows "liminf X \<le> liminf (X \<circ> r) "
   337 proof-
   338   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   339   proof (safe intro!: INF_mono)
   340     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   341       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   342   qed
   343   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
   344 qed
   345 
   346 lemma limsup_subseq_mono:
   347   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   348   assumes "subseq r"
   349   shows "limsup (X \<circ> r) \<le> limsup X"
   350 proof-
   351   have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
   352   proof (safe intro!: SUP_mono)
   353     fix m :: nat
   354     assume "n \<le> m"
   355     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
   356       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   357   qed
   358   then show ?thesis
   359     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
   360 qed
   361 
   362 lemma continuous_on_imp_continuous_within:
   363   "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
   364   unfolding continuous_on_eq_continuous_within
   365   by (auto simp: continuous_within intro: tendsto_within_subset)
   366 
   367 lemma Liminf_compose_continuous_mono:
   368   fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   369   assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
   370   shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)"
   371 proof -
   372   { fix P assume "eventually P F"
   373     have "\<exists>x. P x"
   374     proof (rule ccontr)
   375       assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   376         by auto
   377       with \<open>eventually P F\<close> F show False
   378         by auto
   379     qed }
   380   note * = this
   381 
   382   have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
   383     unfolding Liminf_def
   384     by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
   385        (auto intro: eventually_True)
   386   also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   387     by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
   388        (auto dest!: eventually_happens simp: F)
   389   finally show ?thesis by (auto simp: Liminf_def)
   390 qed
   391 
   392 lemma Limsup_compose_continuous_mono:
   393   fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   394   assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
   395   shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)"
   396 proof -
   397   { fix P assume "eventually P F"
   398     have "\<exists>x. P x"
   399     proof (rule ccontr)
   400       assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   401         by auto
   402       with \<open>eventually P F\<close> F show False
   403         by auto
   404     qed }
   405   note * = this
   406 
   407   have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
   408     unfolding Limsup_def
   409     by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
   410        (auto intro: eventually_True)
   411   also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
   412     by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
   413        (auto dest!: eventually_happens simp: F)
   414   finally show ?thesis by (auto simp: Limsup_def)
   415 qed
   416 
   417 lemma Liminf_compose_continuous_antimono:
   418   fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
   419   assumes c: "continuous_on UNIV f"
   420     and am: "antimono f"
   421     and F: "F \<noteq> bot"
   422   shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
   423 proof -
   424   have *: "\<exists>x. P x" if "eventually P F" for P
   425   proof (rule ccontr)
   426     assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   427       by auto
   428     with \<open>eventually P F\<close> F show False
   429       by auto
   430   qed
   431   have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
   432     unfolding Limsup_def
   433     by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   434        (auto intro: eventually_True)
   435   also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   436     by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   437        (auto dest!: eventually_happens simp: F)
   438   finally show ?thesis
   439     by (auto simp: Liminf_def)
   440 qed
   441 
   442 lemma Limsup_compose_continuous_antimono:
   443   fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   444   assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
   445   shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)"
   446 proof -
   447   { fix P assume "eventually P F"
   448     have "\<exists>x. P x"
   449     proof (rule ccontr)
   450       assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   451         by auto
   452       with \<open>eventually P F\<close> F show False
   453         by auto
   454     qed }
   455   note * = this
   456 
   457   have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
   458     unfolding Liminf_def
   459     by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   460        (auto intro: eventually_True)
   461   also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
   462     by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   463        (auto dest!: eventually_happens simp: F)
   464   finally show ?thesis
   465     by (auto simp: Limsup_def)
   466 qed
   467 
   468 
   469 subsection \<open>More Limits\<close>
   470 
   471 lemma convergent_limsup_cl:
   472   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   473   shows "convergent X \<Longrightarrow> limsup X = lim X"
   474   by (auto simp: convergent_def limI lim_imp_Limsup)
   475 
   476 lemma convergent_liminf_cl:
   477   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   478   shows "convergent X \<Longrightarrow> liminf X = lim X"
   479   by (auto simp: convergent_def limI lim_imp_Liminf)
   480 
   481 lemma lim_increasing_cl:
   482   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   483   obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
   484 proof
   485   show "f \<longlonglongrightarrow> (SUP n. f n)"
   486     using assms
   487     by (intro increasing_tendsto)
   488        (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   489 qed
   490 
   491 lemma lim_decreasing_cl:
   492   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   493   obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
   494 proof
   495   show "f \<longlonglongrightarrow> (INF n. f n)"
   496     using assms
   497     by (intro decreasing_tendsto)
   498        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   499 qed
   500 
   501 lemma compact_complete_linorder:
   502   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   503   shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
   504 proof -
   505   obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   506     using seq_monosub[of X]
   507     unfolding comp_def
   508     by auto
   509   then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
   510     by (auto simp add: monoseq_def)
   511   then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
   512      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   513      by auto
   514   then show ?thesis
   515     using \<open>subseq r\<close> by auto
   516 qed
   517 
   518 end