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