src/HOL/Library/Liminf_Limsup.thy
 author haftmann Tue Mar 18 22:11:46 2014 +0100 (2014-03-18) changeset 56212 3253aaf73a01 parent 54261 89991ef58448 child 56218 1c3f1f2431f9 permissions -rw-r--r--
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
```     1 (*  Title:      HOL/Library/Liminf_Limsup.thy
```
```     2     Author:     Johannes Hölzl, TU München
```
```     3 *)
```
```     4
```
```     5 header {* Liminf and Limsup on complete lattices *}
```
```     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 {* @{text Liminf} and @{text Limsup} *}
```
```    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> INFI (Collect P) f \<le> x) \<Longrightarrow>
```
```    47     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (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> SUPR (Collect P) f) \<Longrightarrow>
```
```    52     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (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}. INFI (Collect P) f \<le> INFI (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}. SUPR (Collect Q) f \<le> SUPR (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 "INFI (Collect P) f \<le> INFI (Collect ?C) f"
```
```   133     by (rule INF_mono) auto
```
```   134   also have "\<dots> \<le> SUPR (Collect ?C) f"
```
```   135     using not_False by (intro INF_le_SUP) auto
```
```   136   also have "\<dots> \<le> SUPR (Collect Q) f"
```
```   137     by (rule SUP_mono) auto
```
```   138   finally show "INFI (Collect P) f \<le> SUPR (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_Liminf_iff:
```
```   154   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
```
```   155   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
```
```   156 proof -
```
```   157   { fix y P assume "eventually P F" "y < INFI (Collect P) X"
```
```   158     then have "eventually (\<lambda>x. y < X x) F"
```
```   159       by (auto elim!: eventually_elim1 dest: less_INF_D) }
```
```   160   moreover
```
```   161   { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
```
```   162     have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
```
```   163     proof (cases "\<exists>z. y < z \<and> z < C")
```
```   164       case True
```
```   165       then obtain z where z: "y < z \<and> z < C" ..
```
```   166       moreover from z have "z \<le> INFI {x. z < X x} X"
```
```   167         by (auto intro!: INF_greatest)
```
```   168       ultimately show ?thesis
```
```   169         using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
```
```   170     next
```
```   171       case False
```
```   172       then have "C \<le> INFI {x. y < X x} X"
```
```   173         by (intro INF_greatest) auto
```
```   174       with `y < C` show ?thesis
```
```   175         using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
```
```   176     qed }
```
```   177   ultimately show ?thesis
```
```   178     unfolding Liminf_def le_SUP_iff by auto
```
```   179 qed
```
```   180
```
```   181 lemma lim_imp_Liminf:
```
```   182   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
```
```   183   assumes ntriv: "\<not> trivial_limit F"
```
```   184   assumes lim: "(f ---> f0) F"
```
```   185   shows "Liminf F f = f0"
```
```   186 proof (intro Liminf_eqI)
```
```   187   fix P assume P: "eventually P F"
```
```   188   then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
```
```   189     by eventually_elim (auto intro!: INF_lower)
```
```   190   then show "INFI (Collect P) f \<le> f0"
```
```   191     by (rule tendsto_le[OF ntriv lim tendsto_const])
```
```   192 next
```
```   193   fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
```
```   194   show "f0 \<le> y"
```
```   195   proof cases
```
```   196     assume "\<exists>z. y < z \<and> z < f0"
```
```   197     then obtain z where "y < z \<and> z < f0" ..
```
```   198     moreover have "z \<le> INFI {x. z < f x} f"
```
```   199       by (rule INF_greatest) simp
```
```   200     ultimately show ?thesis
```
```   201       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
```
```   202   next
```
```   203     assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
```
```   204     show ?thesis
```
```   205     proof (rule classical)
```
```   206       assume "\<not> f0 \<le> y"
```
```   207       then have "eventually (\<lambda>x. y < f x) F"
```
```   208         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
```
```   209       then have "eventually (\<lambda>x. f0 \<le> f x) F"
```
```   210         using discrete by (auto elim!: eventually_elim1)
```
```   211       then have "INFI {x. f0 \<le> f x} f \<le> y"
```
```   212         by (rule upper)
```
```   213       moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
```
```   214         by (intro INF_greatest) simp
```
```   215       ultimately show "f0 \<le> y" by simp
```
```   216     qed
```
```   217   qed
```
```   218 qed
```
```   219
```
```   220 lemma lim_imp_Limsup:
```
```   221   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
```
```   222   assumes ntriv: "\<not> trivial_limit F"
```
```   223   assumes lim: "(f ---> f0) F"
```
```   224   shows "Limsup F f = f0"
```
```   225 proof (intro Limsup_eqI)
```
```   226   fix P assume P: "eventually P F"
```
```   227   then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
```
```   228     by eventually_elim (auto intro!: SUP_upper)
```
```   229   then show "f0 \<le> SUPR (Collect P) f"
```
```   230     by (rule tendsto_le[OF ntriv tendsto_const lim])
```
```   231 next
```
```   232   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
```
```   233   show "y \<le> f0"
```
```   234   proof (cases "\<exists>z. f0 < z \<and> z < y")
```
```   235     case True
```
```   236     then obtain z where "f0 < z \<and> z < y" ..
```
```   237     moreover have "SUPR {x. f x < z} f \<le> z"
```
```   238       by (rule SUP_least) simp
```
```   239     ultimately show ?thesis
```
```   240       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
```
```   241   next
```
```   242     case False
```
```   243     show ?thesis
```
```   244     proof (rule classical)
```
```   245       assume "\<not> y \<le> f0"
```
```   246       then have "eventually (\<lambda>x. f x < y) F"
```
```   247         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
```
```   248       then have "eventually (\<lambda>x. f x \<le> f0) F"
```
```   249         using False by (auto elim!: eventually_elim1 simp: not_less)
```
```   250       then have "y \<le> SUPR {x. f x \<le> f0} f"
```
```   251         by (rule lower)
```
```   252       moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
```
```   253         by (intro SUP_least) simp
```
```   254       ultimately show "y \<le> f0" by simp
```
```   255     qed
```
```   256   qed
```
```   257 qed
```
```   258
```
```   259 lemma Liminf_eq_Limsup:
```
```   260   fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
```
```   261   assumes ntriv: "\<not> trivial_limit F"
```
```   262     and lim: "Liminf F f = f0" "Limsup F f = f0"
```
```   263   shows "(f ---> f0) F"
```
```   264 proof (rule order_tendstoI)
```
```   265   fix a assume "f0 < a"
```
```   266   with assms have "Limsup F f < a" by simp
```
```   267   then obtain P where "eventually P F" "SUPR (Collect P) f < a"
```
```   268     unfolding Limsup_def INF_less_iff by auto
```
```   269   then show "eventually (\<lambda>x. f x < a) F"
```
```   270     by (auto elim!: eventually_elim1 dest: SUP_lessD)
```
```   271 next
```
```   272   fix a assume "a < f0"
```
```   273   with assms have "a < Liminf F f" by simp
```
```   274   then obtain P where "eventually P F" "a < INFI (Collect P) f"
```
```   275     unfolding Liminf_def less_SUP_iff by auto
```
```   276   then show "eventually (\<lambda>x. a < f x) F"
```
```   277     by (auto elim!: eventually_elim1 dest: less_INF_D)
```
```   278 qed
```
```   279
```
```   280 lemma tendsto_iff_Liminf_eq_Limsup:
```
```   281   fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
```
```   282   shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
```
```   283   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
```
```   284
```
```   285 lemma liminf_subseq_mono:
```
```   286   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
```
```   287   assumes "subseq r"
```
```   288   shows "liminf X \<le> liminf (X \<circ> r) "
```
```   289 proof-
```
```   290   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
```
```   291   proof (safe intro!: INF_mono)
```
```   292     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
```
```   293       using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
```
```   294   qed
```
```   295   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
```
```   296 qed
```
```   297
```
```   298 lemma limsup_subseq_mono:
```
```   299   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
```
```   300   assumes "subseq r"
```
```   301   shows "limsup (X \<circ> r) \<le> limsup X"
```
```   302 proof-
```
```   303   have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
```
```   304   proof (safe intro!: SUP_mono)
```
```   305     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
```
```   306       using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
```
```   307   qed
```
```   308   then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
```
```   309 qed
```
```   310
```
```   311 end
```