src/HOL/Library/Liminf_Limsup.thy
author wenzelm
Wed Dec 30 11:21:54 2015 +0100 (2015-12-30)
changeset 61973 0c7e865fa7cb
parent 61969 e01015e49041
child 62049 b0f941e207cf
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Library/Liminf_Limsup.thy
     2     Author:     Johannes Hölzl, TU München
     3 *)
     4 
     5 section \<open>Liminf and Limsup on complete lattices\<close>
     6 
     7 theory Liminf_Limsup
     8 imports Complex_Main
     9 begin
    10 
    11 lemma le_Sup_iff_less:
    12   fixes x :: "'a :: {complete_linorder, dense_linorder}"
    13   shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
    14   unfolding le_SUP_iff
    15   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    16 
    17 lemma Inf_le_iff_less:
    18   fixes x :: "'a :: {complete_linorder, dense_linorder}"
    19   shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    20   unfolding INF_le_iff
    21   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    22 
    23 lemma SUP_pair:
    24   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    25   shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    26   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    27 
    28 lemma INF_pair:
    29   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    30   shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    31   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    32 
    33 subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
    34 
    35 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    36   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
    37 
    38 definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
    39   "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
    40 
    41 abbreviation "liminf \<equiv> Liminf sequentially"
    42 
    43 abbreviation "limsup \<equiv> Limsup sequentially"
    44 
    45 lemma Liminf_eqI:
    46   "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
    47     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    48   unfolding Liminf_def by (auto intro!: SUP_eqI)
    49 
    50 lemma Limsup_eqI:
    51   "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
    52     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    53   unfolding Limsup_def by (auto intro!: INF_eqI)
    54 
    55 lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
    56   unfolding Liminf_def eventually_sequentially
    57   by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
    58 
    59 lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
    60   unfolding Limsup_def eventually_sequentially
    61   by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
    62 
    63 lemma Limsup_const:
    64   assumes ntriv: "\<not> trivial_limit F"
    65   shows "Limsup F (\<lambda>x. c) = c"
    66 proof -
    67   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    68   have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
    69     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
    70   then show ?thesis
    71     unfolding Limsup_def using eventually_True
    72     by (subst INF_cong[where D="\<lambda>x. c"])
    73        (auto intro!: INF_const simp del: eventually_True)
    74 qed
    75 
    76 lemma Liminf_const:
    77   assumes ntriv: "\<not> trivial_limit F"
    78   shows "Liminf F (\<lambda>x. c) = c"
    79 proof -
    80   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    81   have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
    82     using ntriv by (intro INF_const) (auto simp: eventually_False *)
    83   then show ?thesis
    84     unfolding Liminf_def using eventually_True
    85     by (subst SUP_cong[where D="\<lambda>x. c"])
    86        (auto intro!: SUP_const simp del: eventually_True)
    87 qed
    88 
    89 lemma Liminf_mono:
    90   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
    91   shows "Liminf F f \<le> Liminf F g"
    92   unfolding Liminf_def
    93 proof (safe intro!: SUP_mono)
    94   fix P assume "eventually P F"
    95   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
    96   then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
    97     by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
    98 qed
    99 
   100 lemma Liminf_eq:
   101   assumes "eventually (\<lambda>x. f x = g x) F"
   102   shows "Liminf F f = Liminf F g"
   103   by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
   104 
   105 lemma Limsup_mono:
   106   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   107   shows "Limsup F f \<le> Limsup F g"
   108   unfolding Limsup_def
   109 proof (safe intro!: INF_mono)
   110   fix P assume "eventually P F"
   111   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   112   then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
   113     by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
   114 qed
   115 
   116 lemma Limsup_eq:
   117   assumes "eventually (\<lambda>x. f x = g x) net"
   118   shows "Limsup net f = Limsup net g"
   119   by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
   120 
   121 lemma Liminf_le_Limsup:
   122   assumes ntriv: "\<not> trivial_limit F"
   123   shows "Liminf F f \<le> Limsup F f"
   124   unfolding Limsup_def Liminf_def
   125   apply (rule SUP_least)
   126   apply (rule INF_greatest)
   127 proof safe
   128   fix P Q assume "eventually P F" "eventually Q F"
   129   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   130   then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
   131     using ntriv by (auto simp add: eventually_False)
   132   have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
   133     by (rule INF_mono) auto
   134   also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
   135     using not_False by (intro INF_le_SUP) auto
   136   also have "\<dots> \<le> SUPREMUM (Collect Q) f"
   137     by (rule SUP_mono) auto
   138   finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
   139 qed
   140 
   141 lemma Liminf_bounded:
   142   assumes ntriv: "\<not> trivial_limit F"
   143   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   144   shows "C \<le> Liminf F X"
   145   using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
   146 
   147 lemma Limsup_bounded:
   148   assumes ntriv: "\<not> trivial_limit F"
   149   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   150   shows "Limsup F X \<le> C"
   151   using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
   152 
   153 lemma le_Limsup:
   154   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
   155   shows "l \<le> Limsup F f"
   156 proof -
   157   have "l = Limsup F (\<lambda>x. l)"
   158     using F by (simp add: Limsup_const)
   159   also have "\<dots> \<le> Limsup F f"
   160     by (intro Limsup_mono x)
   161   finally show ?thesis .
   162 qed
   163 
   164 lemma le_Liminf_iff:
   165   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   166   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   167 proof -
   168   have "eventually (\<lambda>x. y < X x) F"
   169     if "eventually P F" "y < INFIMUM (Collect P) X" for y P
   170     using that by (auto elim!: eventually_mono dest: less_INF_D)
   171   moreover
   172   have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
   173     if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
   174   proof (cases "\<exists>z. y < z \<and> z < C")
   175     case True
   176     then obtain z where z: "y < z \<and> z < C" ..
   177     moreover from z have "z \<le> INFIMUM {x. z < X x} X"
   178       by (auto intro!: INF_greatest)
   179     ultimately show ?thesis
   180       using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   181   next
   182     case False
   183     then have "C \<le> INFIMUM {x. y < X x} X"
   184       by (intro INF_greatest) auto
   185     with \<open>y < C\<close> show ?thesis
   186       using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   187   qed
   188   ultimately show ?thesis
   189     unfolding Liminf_def le_SUP_iff by auto
   190 qed
   191 
   192 lemma lim_imp_Liminf:
   193   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   194   assumes ntriv: "\<not> trivial_limit F"
   195   assumes lim: "(f \<longlongrightarrow> f0) F"
   196   shows "Liminf F f = f0"
   197 proof (intro Liminf_eqI)
   198   fix P assume P: "eventually P F"
   199   then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
   200     by eventually_elim (auto intro!: INF_lower)
   201   then show "INFIMUM (Collect P) f \<le> f0"
   202     by (rule tendsto_le[OF ntriv lim tendsto_const])
   203 next
   204   fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
   205   show "f0 \<le> y"
   206   proof cases
   207     assume "\<exists>z. y < z \<and> z < f0"
   208     then obtain z where "y < z \<and> z < f0" ..
   209     moreover have "z \<le> INFIMUM {x. z < f x} f"
   210       by (rule INF_greatest) simp
   211     ultimately show ?thesis
   212       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   213   next
   214     assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
   215     show ?thesis
   216     proof (rule classical)
   217       assume "\<not> f0 \<le> y"
   218       then have "eventually (\<lambda>x. y < f x) F"
   219         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   220       then have "eventually (\<lambda>x. f0 \<le> f x) F"
   221         using discrete by (auto elim!: eventually_mono)
   222       then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
   223         by (rule upper)
   224       moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
   225         by (intro INF_greatest) simp
   226       ultimately show "f0 \<le> y" by simp
   227     qed
   228   qed
   229 qed
   230 
   231 lemma lim_imp_Limsup:
   232   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
   233   assumes ntriv: "\<not> trivial_limit F"
   234   assumes lim: "(f \<longlongrightarrow> f0) F"
   235   shows "Limsup F f = f0"
   236 proof (intro Limsup_eqI)
   237   fix P assume P: "eventually P F"
   238   then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
   239     by eventually_elim (auto intro!: SUP_upper)
   240   then show "f0 \<le> SUPREMUM (Collect P) f"
   241     by (rule tendsto_le[OF ntriv tendsto_const lim])
   242 next
   243   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
   244   show "y \<le> f0"
   245   proof (cases "\<exists>z. f0 < z \<and> z < y")
   246     case True
   247     then obtain z where "f0 < z \<and> z < y" ..
   248     moreover have "SUPREMUM {x. f x < z} f \<le> z"
   249       by (rule SUP_least) simp
   250     ultimately show ?thesis
   251       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   252   next
   253     case False
   254     show ?thesis
   255     proof (rule classical)
   256       assume "\<not> y \<le> f0"
   257       then have "eventually (\<lambda>x. f x < y) F"
   258         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   259       then have "eventually (\<lambda>x. f x \<le> f0) F"
   260         using False by (auto elim!: eventually_mono simp: not_less)
   261       then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
   262         by (rule lower)
   263       moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
   264         by (intro SUP_least) simp
   265       ultimately show "y \<le> f0" by simp
   266     qed
   267   qed
   268 qed
   269 
   270 lemma Liminf_eq_Limsup:
   271   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   272   assumes ntriv: "\<not> trivial_limit F"
   273     and lim: "Liminf F f = f0" "Limsup F f = f0"
   274   shows "(f \<longlongrightarrow> f0) F"
   275 proof (rule order_tendstoI)
   276   fix a assume "f0 < a"
   277   with assms have "Limsup F f < a" by simp
   278   then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
   279     unfolding Limsup_def INF_less_iff by auto
   280   then show "eventually (\<lambda>x. f x < a) F"
   281     by (auto elim!: eventually_mono dest: SUP_lessD)
   282 next
   283   fix a assume "a < f0"
   284   with assms have "a < Liminf F f" by simp
   285   then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
   286     unfolding Liminf_def less_SUP_iff by auto
   287   then show "eventually (\<lambda>x. a < f x) F"
   288     by (auto elim!: eventually_mono dest: less_INF_D)
   289 qed
   290 
   291 lemma tendsto_iff_Liminf_eq_Limsup:
   292   fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
   293   shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   294   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
   295 
   296 lemma liminf_subseq_mono:
   297   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   298   assumes "subseq r"
   299   shows "liminf X \<le> liminf (X \<circ> r) "
   300 proof-
   301   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   302   proof (safe intro!: INF_mono)
   303     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   304       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   305   qed
   306   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
   307 qed
   308 
   309 lemma limsup_subseq_mono:
   310   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   311   assumes "subseq r"
   312   shows "limsup (X \<circ> r) \<le> limsup X"
   313 proof-
   314   have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
   315   proof (safe intro!: SUP_mono)
   316     fix m :: nat
   317     assume "n \<le> m"
   318     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
   319       using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   320   qed
   321   then show ?thesis
   322     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
   323 qed
   324 
   325 lemma continuous_on_imp_continuous_within:
   326   "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
   327   unfolding continuous_on_eq_continuous_within
   328   by (auto simp: continuous_within intro: tendsto_within_subset)
   329 
   330 lemma Liminf_compose_continuous_antimono:
   331   fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
   332   assumes c: "continuous_on UNIV f"
   333     and am: "antimono f"
   334     and F: "F \<noteq> bot"
   335   shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
   336 proof -
   337   have *: "\<exists>x. P x" if "eventually P F" for P
   338   proof (rule ccontr)
   339     assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
   340       by auto
   341     with \<open>eventually P F\<close> F show False
   342       by auto
   343   qed
   344   have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
   345     unfolding Limsup_def INF_def
   346     by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   347        (auto intro: eventually_True)
   348   also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   349     by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   350        (auto dest!: eventually_happens simp: F)
   351   finally show ?thesis
   352     by (auto simp: Liminf_def)
   353 qed
   354 subsection \<open>More Limits\<close>
   355 
   356 lemma convergent_limsup_cl:
   357   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   358   shows "convergent X \<Longrightarrow> limsup X = lim X"
   359   by (auto simp: convergent_def limI lim_imp_Limsup)
   360 
   361 lemma convergent_liminf_cl:
   362   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   363   shows "convergent X \<Longrightarrow> liminf X = lim X"
   364   by (auto simp: convergent_def limI lim_imp_Liminf)
   365 
   366 lemma lim_increasing_cl:
   367   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   368   obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
   369 proof
   370   show "f \<longlonglongrightarrow> (SUP n. f n)"
   371     using assms
   372     by (intro increasing_tendsto)
   373        (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   374 qed
   375 
   376 lemma lim_decreasing_cl:
   377   assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   378   obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
   379 proof
   380   show "f \<longlonglongrightarrow> (INF n. f n)"
   381     using assms
   382     by (intro decreasing_tendsto)
   383        (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   384 qed
   385 
   386 lemma compact_complete_linorder:
   387   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   388   shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
   389 proof -
   390   obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   391     using seq_monosub[of X]
   392     unfolding comp_def
   393     by auto
   394   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)"
   395     by (auto simp add: monoseq_def)
   396   then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
   397      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   398      by auto
   399   then show ?thesis
   400     using \<open>subseq r\<close> by auto
   401 qed
   402 
   403 end