src/HOL/Library/Liminf_Limsup.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69861 62e47f06d22c
child 70378 ebd108578ab1
permissions -rw-r--r--
improved code equations taken over from AFP
     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 conditionally complete lattices\<close>
     7 
     8 theory Liminf_Limsup
     9 imports Complex_Main
    10 begin
    11 
    12 lemma (in conditionally_complete_linorder) le_cSup_iff:
    13   assumes "A \<noteq> {}" "bdd_above A"
    14   shows "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
    15 proof safe
    16   fix y assume "x \<le> Sup A" "y < x"
    17   then have "y < Sup A" by auto
    18   then show "\<exists>a\<in>A. y < a"
    19     unfolding less_cSup_iff[OF assms] .
    20 qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
    21 
    22 lemma (in conditionally_complete_linorder) le_cSUP_iff:
    23   "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> Sup (f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
    24   using le_cSup_iff [of "f ` A"] by simp
    25 
    26 lemma le_cSup_iff_less:
    27   fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
    28   shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
    29   by (simp add: le_cSUP_iff)
    30      (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    31 
    32 lemma le_Sup_iff_less:
    33   fixes x :: "'a :: {complete_linorder, dense_linorder}"
    34   shows "x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
    35   unfolding le_SUP_iff
    36   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    37 
    38 lemma (in conditionally_complete_linorder) cInf_le_iff:
    39   assumes "A \<noteq> {}" "bdd_below A"
    40   shows "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
    41 proof safe
    42   fix y assume "x \<ge> Inf A" "y > x"
    43   then have "y > Inf A" by auto
    44   then show "\<exists>a\<in>A. y > a"
    45     unfolding cInf_less_iff[OF assms] .
    46 qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
    47 
    48 lemma (in conditionally_complete_linorder) cINF_le_iff:
    49   "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> Inf (f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
    50   using cInf_le_iff [of "f ` A"] by simp
    51 
    52 lemma cInf_le_iff_less:
    53   fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
    54   shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    55   by (simp add: cINF_le_iff)
    56      (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    57 
    58 lemma Inf_le_iff_less:
    59   fixes x :: "'a :: {complete_linorder, dense_linorder}"
    60   shows "(INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    61   unfolding INF_le_iff
    62   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    63 
    64 lemma SUP_pair:
    65   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    66   shows "(SUP i \<in> A. SUP j \<in> B. f i j) = (SUP p \<in> A \<times> B. f (fst p) (snd p))"
    67   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    68 
    69 lemma INF_pair:
    70   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    71   shows "(INF i \<in> A. INF j \<in> B. f i j) = (INF p \<in> A \<times> B. f (fst p) (snd p))"
    72   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    73 
    74 lemma INF_Sigma:
    75   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    76   shows "(INF i \<in> A. INF j \<in> B i. f i j) = (INF p \<in> Sigma A B. f (fst p) (snd p))"
    77   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    78 
    79 subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
    80 
    81 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    82   "Liminf F f = (SUP P\<in>{P. eventually P F}. INF x\<in>{x. P x}. f x)"
    83 
    84 definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    85   "Limsup F f = (INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. f x)"
    86 
    87 abbreviation "liminf \<equiv> Liminf sequentially"
    88 
    89 abbreviation "limsup \<equiv> Limsup sequentially"
    90 
    91 lemma Liminf_eqI:
    92   "(\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> x) \<Longrightarrow>
    93     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    94   unfolding Liminf_def by (auto intro!: SUP_eqI)
    95 
    96 lemma Limsup_eqI:
    97   "(\<And>P. eventually P F \<Longrightarrow> x \<le> Sup (f ` (Collect P))) \<Longrightarrow>
    98     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    99   unfolding Limsup_def by (auto intro!: INF_eqI)
   100 
   101 lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
   102   unfolding Liminf_def eventually_sequentially
   103   by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
   104 
   105 lemma limsup_INF_SUP: "limsup f = (INF n. SUP m\<in>{n..}. f m)"
   106   unfolding Limsup_def eventually_sequentially
   107   by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
   108 
   109 lemma Limsup_const:
   110   assumes ntriv: "\<not> trivial_limit F"
   111   shows "Limsup F (\<lambda>x. c) = c"
   112 proof -
   113   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
   114   have "\<And>P. eventually P F \<Longrightarrow> (SUP x \<in> {x. P x}. c) = c"
   115     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
   116   then show ?thesis
   117     apply (auto simp add: Limsup_def)
   118     apply (rule INF_const)
   119     apply auto
   120     using eventually_True apply blast
   121     done
   122 qed
   123 
   124 lemma Liminf_const:
   125   assumes ntriv: "\<not> trivial_limit F"
   126   shows "Liminf F (\<lambda>x. c) = c"
   127 proof -
   128   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
   129   have "\<And>P. eventually P F \<Longrightarrow> (INF x \<in> {x. P x}. c) = c"
   130     using ntriv by (intro INF_const) (auto simp: eventually_False *)
   131   then show ?thesis
   132     apply (auto simp add: Liminf_def)
   133     apply (rule SUP_const)
   134     apply auto
   135     using eventually_True apply blast
   136     done
   137 qed
   138 
   139 lemma Liminf_mono:
   140   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   141   shows "Liminf F f \<le> Liminf F g"
   142   unfolding Liminf_def
   143 proof (safe intro!: SUP_mono)
   144   fix P assume "eventually P F"
   145   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   146   then show "\<exists>Q\<in>{P. eventually P F}. Inf (f ` (Collect P)) \<le> Inf (g ` (Collect Q))"
   147     by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
   148 qed
   149 
   150 lemma Liminf_eq:
   151   assumes "eventually (\<lambda>x. f x = g x) F"
   152   shows "Liminf F f = Liminf F g"
   153   by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
   154 
   155 lemma Limsup_mono:
   156   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   157   shows "Limsup F f \<le> Limsup F g"
   158   unfolding Limsup_def
   159 proof (safe intro!: INF_mono)
   160   fix P assume "eventually P F"
   161   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   162   then show "\<exists>Q\<in>{P. eventually P F}. Sup (f ` (Collect Q)) \<le> Sup (g ` (Collect P))"
   163     by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
   164 qed
   165 
   166 lemma Limsup_eq:
   167   assumes "eventually (\<lambda>x. f x = g x) net"
   168   shows "Limsup net f = Limsup net g"
   169   by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
   170 
   171 lemma Liminf_bot[simp]: "Liminf bot f = top"
   172   unfolding Liminf_def top_unique[symmetric]
   173   by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all
   174 
   175 lemma Limsup_bot[simp]: "Limsup bot f = bot"
   176   unfolding Limsup_def bot_unique[symmetric]
   177   by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all
   178 
   179 lemma Liminf_le_Limsup:
   180   assumes ntriv: "\<not> trivial_limit F"
   181   shows "Liminf F f \<le> Limsup F f"
   182   unfolding Limsup_def Liminf_def
   183   apply (rule SUP_least)
   184   apply (rule INF_greatest)
   185 proof safe
   186   fix P Q assume "eventually P F" "eventually Q F"
   187   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   188   then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
   189     using ntriv by (auto simp add: eventually_False)
   190   have "Inf (f ` (Collect P)) \<le> Inf (f ` (Collect ?C))"
   191     by (rule INF_mono) auto
   192   also have "\<dots> \<le> Sup (f ` (Collect ?C))"
   193     using not_False by (intro INF_le_SUP) auto
   194   also have "\<dots> \<le> Sup (f ` (Collect Q))"
   195     by (rule SUP_mono) auto
   196   finally show "Inf (f ` (Collect P)) \<le> Sup (f ` (Collect Q))" .
   197 qed
   198 
   199 lemma Liminf_bounded:
   200   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   201   shows "C \<le> Liminf F X"
   202   using Liminf_mono[OF le] Liminf_const[of F C]
   203   by (cases "F = bot") simp_all
   204 
   205 lemma Limsup_bounded:
   206   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   207   shows "Limsup F X \<le> C"
   208   using Limsup_mono[OF le] Limsup_const[of F C]
   209   by (cases "F = bot") simp_all
   210 
   211 lemma le_Limsup:
   212   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
   213   shows "l \<le> Limsup F f"
   214   using F Liminf_bounded[of l f F] Liminf_le_Limsup[of F f] order.trans x by blast
   215 
   216 lemma Liminf_le:
   217   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
   218   shows "Liminf F f \<le> l"
   219   using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
   220 
   221 lemma le_Liminf_iff:
   222   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   223   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   224 proof -
   225   have "eventually (\<lambda>x. y < X x) F"
   226     if "eventually P F" "y < Inf (X ` (Collect P))" for y P
   227     using that by (auto elim!: eventually_mono dest: less_INF_D)
   228   moreover
   229   have "\<exists>P. eventually P F \<and> y < Inf (X ` (Collect P))"
   230     if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
   231   proof (cases "\<exists>z. y < z \<and> z < C")
   232     case True
   233     then obtain z where z: "y < z \<and> z < C" ..
   234     moreover from z have "z \<le> Inf (X ` {x. z < X x})"
   235       by (auto intro!: INF_greatest)
   236     ultimately show ?thesis
   237       using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   238   next
   239     case False
   240     then have "C \<le> Inf (X ` {x. y < X x})"
   241       by (intro INF_greatest) auto
   242     with \<open>y < C\<close> show ?thesis
   243       using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   244   qed
   245   ultimately show ?thesis
   246     unfolding Liminf_def le_SUP_iff by auto
   247 qed
   248 
   249 lemma Limsup_le_iff:
   250   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   251   shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
   252 proof -
   253   { fix y P assume "eventually P F" "y > Sup (X ` (Collect P))"
   254     then have "eventually (\<lambda>x. y > X x) F"
   255       by (auto elim!: eventually_mono dest: SUP_lessD) }
   256   moreover
   257   { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
   258     have "\<exists>P. eventually P F \<and> y > Sup (X ` (Collect P))"
   259     proof (cases "\<exists>z. C < z \<and> z < y")
   260       case True
   261       then obtain z where z: "C < z \<and> z < y" ..
   262       moreover from z have "z \<ge> Sup (X ` {x. X x < z})"
   263         by (auto intro!: SUP_least)
   264       ultimately show ?thesis
   265         using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
   266     next
   267       case False
   268       then have "C \<ge> Sup (X ` {x. X x < y})"
   269         by (intro SUP_least) (auto simp: not_less)
   270       with \<open>y > C\<close> show ?thesis
   271         using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
   272     qed }
   273   ultimately show ?thesis
   274     unfolding Limsup_def INF_le_iff by auto
   275 qed
   276 
   277 lemma less_LiminfD:
   278   "y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F"
   279   using le_Liminf_iff[of "Liminf F f" F f] by simp
   280 
   281 lemma Limsup_lessD:
   282   "y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F"
   283   using Limsup_le_iff[of F f "Limsup F f"] by simp
   284 
   285 lemma lim_imp_Liminf:
   286   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   287   assumes ntriv: "\<not> trivial_limit F"
   288   assumes lim: "(f \<longlongrightarrow> f0) F"
   289   shows "Liminf F f = f0"
   290 proof (intro Liminf_eqI)
   291   fix P assume P: "eventually P F"
   292   then have "eventually (\<lambda>x. Inf (f ` (Collect P)) \<le> f x) F"
   293     by eventually_elim (auto intro!: INF_lower)
   294   then show "Inf (f ` (Collect P)) \<le> f0"
   295     by (rule tendsto_le[OF ntriv lim tendsto_const])
   296 next
   297   fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y"
   298   show "f0 \<le> y"
   299   proof cases
   300     assume "\<exists>z. y < z \<and> z < f0"
   301     then obtain z where "y < z \<and> z < f0" ..
   302     moreover have "z \<le> Inf (f ` {x. z < f x})"
   303       by (rule INF_greatest) simp
   304     ultimately show ?thesis
   305       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   306   next
   307     assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
   308     show ?thesis
   309     proof (rule classical)
   310       assume "\<not> f0 \<le> y"
   311       then have "eventually (\<lambda>x. y < f x) F"
   312         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   313       then have "eventually (\<lambda>x. f0 \<le> f x) F"
   314         using discrete by (auto elim!: eventually_mono)
   315       then have "Inf (f ` {x. f0 \<le> f x}) \<le> y"
   316         by (rule upper)
   317       moreover have "f0 \<le> Inf (f ` {x. f0 \<le> f x})"
   318         by (intro INF_greatest) simp
   319       ultimately show "f0 \<le> y" by simp
   320     qed
   321   qed
   322 qed
   323 
   324 lemma lim_imp_Limsup:
   325   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   326   assumes ntriv: "\<not> trivial_limit F"
   327   assumes lim: "(f \<longlongrightarrow> f0) F"
   328   shows "Limsup F f = f0"
   329 proof (intro Limsup_eqI)
   330   fix P assume P: "eventually P F"
   331   then have "eventually (\<lambda>x. f x \<le> Sup (f ` (Collect P))) F"
   332     by eventually_elim (auto intro!: SUP_upper)
   333   then show "f0 \<le> Sup (f ` (Collect P))"
   334     by (rule tendsto_le[OF ntriv tendsto_const lim])
   335 next
   336   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))"
   337   show "y \<le> f0"
   338   proof (cases "\<exists>z. f0 < z \<and> z < y")
   339     case True
   340     then obtain z where "f0 < z \<and> z < y" ..
   341     moreover have "Sup (f ` {x. f x < z}) \<le> z"
   342       by (rule SUP_least) simp
   343     ultimately show ?thesis
   344       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   345   next
   346     case False
   347     show ?thesis
   348     proof (rule classical)
   349       assume "\<not> y \<le> f0"
   350       then have "eventually (\<lambda>x. f x < y) F"
   351         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   352       then have "eventually (\<lambda>x. f x \<le> f0) F"
   353         using False by (auto elim!: eventually_mono simp: not_less)
   354       then have "y \<le> Sup (f ` {x. f x \<le> f0})"
   355         by (rule lower)
   356       moreover have "Sup (f ` {x. f x \<le> f0}) \<le> f0"
   357         by (intro SUP_least) simp
   358       ultimately show "y \<le> f0" by simp
   359     qed
   360   qed
   361 qed
   362 
   363 lemma Liminf_eq_Limsup:
   364   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   365   assumes ntriv: "\<not> trivial_limit F"
   366     and lim: "Liminf F f = f0" "Limsup F f = f0"
   367   shows "(f \<longlongrightarrow> f0) F"
   368 proof (rule order_tendstoI)
   369   fix a assume "f0 < a"
   370   with assms have "Limsup F f < a" by simp
   371   then obtain P where "eventually P F" "Sup (f ` (Collect P)) < a"
   372     unfolding Limsup_def INF_less_iff by auto
   373   then show "eventually (\<lambda>x. f x < a) F"
   374     by (auto elim!: eventually_mono dest: SUP_lessD)
   375 next
   376   fix a assume "a < f0"
   377   with assms have "a < Liminf F f" by simp
   378   then obtain P where "eventually P F" "a < Inf (f ` (Collect P))"
   379     unfolding Liminf_def less_SUP_iff by auto
   380   then show "eventually (\<lambda>x. a < f x) F"
   381     by (auto elim!: eventually_mono dest: less_INF_D)
   382 qed
   383 
   384 lemma tendsto_iff_Liminf_eq_Limsup:
   385   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   386   shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   387   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
   388 
   389 lemma liminf_subseq_mono:
   390   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   391   assumes "strict_mono r"
   392   shows "liminf X \<le> liminf (X \<circ> r) "
   393 proof-
   394   have "\<And>n. (INF m\<in>{n..}. X m) \<le> (INF m\<in>{n..}. (X \<circ> r) m)"
   395   proof (safe intro!: INF_mono)
   396     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   397       using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   398   qed
   399   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
   400 qed
   401 
   402 lemma limsup_subseq_mono:
   403   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   404   assumes "strict_mono r"
   405   shows "limsup (X \<circ> r) \<le> limsup X"
   406 proof-
   407   have "(SUP m\<in>{n..}. (X \<circ> r) m) \<le> (SUP m\<in>{n..}. X m)" for n
   408   proof (safe intro!: SUP_mono)
   409     fix m :: nat
   410     assume "n \<le> m"
   411     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
   412       using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   413   qed
   414   then show ?thesis
   415     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
   416 qed
   417 
   418 lemma continuous_on_imp_continuous_within:
   419   "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
   420   unfolding continuous_on_eq_continuous_within
   421   by (auto simp: continuous_within intro: tendsto_within_subset)
   422 
   423 lemma Liminf_compose_continuous_mono:
   424   fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   425   assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
   426   shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)"
   427 proof -
   428   { fix P assume "eventually P F"
   429     have "\<exists>x. P x"
   430     proof (rule ccontr)
   431       assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   432         by auto
   433       with \<open>eventually P F\<close> F show False
   434         by auto
   435     qed }
   436   note * = this
   437 
   438   have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
   439     Sup (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
   440     using am continuous_on_imp_continuous_within [OF c]
   441     by (rule continuous_at_Sup_mono) (auto intro: eventually_True)
   442   then have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
   443     by (simp add: Liminf_def image_comp)
   444   also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
   445     using * continuous_at_Inf_mono [OF am continuous_on_imp_continuous_within [OF c]]
   446     by auto 
   447   finally show ?thesis by (auto simp: Liminf_def image_comp)
   448 qed
   449 
   450 lemma Limsup_compose_continuous_mono:
   451   fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   452   assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
   453   shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)"
   454 proof -
   455   { fix P assume "eventually P F"
   456     have "\<exists>x. P x"
   457     proof (rule ccontr)
   458       assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   459         by auto
   460       with \<open>eventually P F\<close> F show False
   461         by auto
   462     qed }
   463   note * = this
   464 
   465   have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
   466     Inf (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
   467     using am continuous_on_imp_continuous_within [OF c]
   468     by (rule continuous_at_Inf_mono) (auto intro: eventually_True)
   469   then have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
   470     by (simp add: Limsup_def image_comp)
   471   also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
   472     using * continuous_at_Sup_mono [OF am continuous_on_imp_continuous_within [OF c]]
   473     by auto
   474   finally show ?thesis by (auto simp: Limsup_def image_comp)
   475 qed
   476 
   477 lemma Liminf_compose_continuous_antimono:
   478   fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
   479   assumes c: "continuous_on UNIV f"
   480     and am: "antimono f"
   481     and F: "F \<noteq> bot"
   482   shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
   483 proof -
   484   have *: "\<exists>x. P x" if "eventually P F" for P
   485   proof (rule ccontr)
   486     assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   487       by auto
   488     with \<open>eventually P F\<close> F show False
   489       by auto
   490   qed
   491 
   492   have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
   493     Sup (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
   494     using am continuous_on_imp_continuous_within [OF c]
   495     by (rule continuous_at_Inf_antimono) (auto intro: eventually_True)
   496   then have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
   497     by (simp add: Limsup_def image_comp)
   498   also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
   499     using * continuous_at_Sup_antimono [OF am continuous_on_imp_continuous_within [OF c]]
   500     by auto
   501   finally show ?thesis
   502     by (auto simp: Liminf_def image_comp)
   503 qed
   504 
   505 lemma Limsup_compose_continuous_antimono:
   506   fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
   507   assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
   508   shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)"
   509 proof -
   510   { fix P assume "eventually P F"
   511     have "\<exists>x. P x"
   512     proof (rule ccontr)
   513       assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   514         by auto
   515       with \<open>eventually P F\<close> F show False
   516         by auto
   517     qed }
   518   note * = this
   519 
   520   have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
   521     Inf (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
   522     using am continuous_on_imp_continuous_within [OF c]
   523     by (rule continuous_at_Sup_antimono) (auto intro: eventually_True)
   524   then have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
   525     by (simp add: Liminf_def image_comp)
   526   also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
   527     using * continuous_at_Inf_antimono [OF am continuous_on_imp_continuous_within [OF c]]
   528     by auto
   529   finally show ?thesis
   530     by (auto simp: Limsup_def image_comp)
   531 qed
   532 
   533 lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
   534   apply (cases "F = bot", simp)
   535   by (subst Liminf_def)
   536     (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least)
   537 
   538 lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))"
   539   apply (cases "F = bot", simp)
   540   by (subst Limsup_def)
   541     (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
   542 
   543 lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x\<in>Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
   544   by (auto intro!: SUP_least simp: Liminf_def)
   545 
   546 lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x\<in>Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
   547   by (auto intro!: INF_greatest simp: Limsup_def)
   548 
   549 lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
   550   apply (cases "F = bot", simp)
   551   apply (rule Liminf_least)
   552   subgoal for P
   553     by (auto simp: eventually_filtermap the_inv_f_f
   554         intro!: Liminf_bounded INF_lower2 eventually_mono[of P])
   555   done
   556 
   557 lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))"
   558   apply (cases "F = bot", simp)
   559   apply (rule Limsup_greatest)
   560   subgoal for P
   561     by (auto simp: eventually_filtermap the_inv_f_f
   562         intro!: Limsup_bounded SUP_upper2 eventually_mono[of P])
   563   done
   564 
   565 lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))"
   566   using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g]
   567   by simp
   568 
   569 lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))"
   570   using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f]
   571   by simp
   572 
   573 
   574 subsection \<open>More Limits\<close>
   575 
   576 lemma convergent_limsup_cl:
   577   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   578   shows "convergent X \<Longrightarrow> limsup X = lim X"
   579   by (auto simp: convergent_def limI lim_imp_Limsup)
   580 
   581 lemma convergent_liminf_cl:
   582   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   583   shows "convergent X \<Longrightarrow> liminf X = lim X"
   584   by (auto simp: convergent_def limI lim_imp_Liminf)
   585 
   586 lemma lim_increasing_cl:
   587   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   588   obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
   589 proof
   590   show "f \<longlonglongrightarrow> (SUP n. f n)"
   591     using assms
   592     by (intro increasing_tendsto)
   593        (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   594 qed
   595 
   596 lemma lim_decreasing_cl:
   597   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   598   obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
   599 proof
   600   show "f \<longlonglongrightarrow> (INF n. f n)"
   601     using assms
   602     by (intro decreasing_tendsto)
   603        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   604 qed
   605 
   606 lemma compact_complete_linorder:
   607   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   608   shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
   609 proof -
   610   obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
   611     using seq_monosub[of X]
   612     unfolding comp_def
   613     by auto
   614   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)"
   615     by (auto simp add: monoseq_def)
   616   then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
   617      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   618      by auto
   619   then show ?thesis
   620     using \<open>strict_mono r\<close> by auto
   621 qed
   622 
   623 lemma tendsto_Limsup:
   624   fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   625   shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"
   626   by (subst tendsto_iff_Liminf_eq_Limsup) auto
   627 
   628 lemma tendsto_Liminf:
   629   fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   630   shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Liminf F f) F"
   631   by (subst tendsto_iff_Liminf_eq_Limsup) auto
   632 
   633 end