move Liminf / Limsup lemmas on complete_lattices to its own file
authorhoelzl
Tue Mar 05 15:43:08 2013 +0100 (2013-03-05)
changeset 513405e6296afe08d
parent 51339 04ebef4ee844
child 51341 8c10293e7ea7
move Liminf / Limsup lemmas on complete_lattices to its own file
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Lebesgue_Integration.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 05 15:27:08 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 05 15:43:08 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Extended real number line *}
     1.5  
     1.6  theory Extended_Real
     1.7 -imports Complex_Main Extended_Nat
     1.8 +imports Complex_Main Extended_Nat Liminf_Limsup
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -18,26 +18,6 @@
    1.13  
    1.14  *}
    1.15  
    1.16 -lemma SUPR_pair:
    1.17 -  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    1.18 -  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    1.19 -
    1.20 -lemma INFI_pair:
    1.21 -  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    1.22 -  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    1.23 -
    1.24 -lemma le_Sup_iff_less:
    1.25 -  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
    1.26 -  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
    1.27 -  unfolding le_SUP_iff
    1.28 -  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    1.29 -
    1.30 -lemma Inf_le_iff_less:
    1.31 -  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
    1.32 -  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    1.33 -  unfolding INF_le_iff
    1.34 -  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    1.35 -
    1.36  subsection {* Definition and basic properties *}
    1.37  
    1.38  datatype ereal = ereal real | PInfty | MInfty
    1.39 @@ -1718,6 +1698,31 @@
    1.40    show thesis by auto
    1.41  qed
    1.42  
    1.43 +instance ereal :: perfect_space
    1.44 +proof (default, rule)
    1.45 +  fix a :: ereal assume a: "open {a}"
    1.46 +  show False
    1.47 +  proof (cases a)
    1.48 +    case MInf
    1.49 +    then obtain y where "{..<ereal y} \<le> {a}" using a open_MInfty2[of "{a}"] by auto
    1.50 +    then have "ereal (y - 1) \<in> {a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
    1.51 +    then show False using `a = -\<infinity>` by auto
    1.52 +  next
    1.53 +    case PInf
    1.54 +    then obtain y where "{ereal y<..} \<le> {a}" using a open_PInfty2[of "{a}"] by auto
    1.55 +    then have "ereal (y + 1) \<in> {a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
    1.56 +    then show False using `a = \<infinity>` by auto
    1.57 +  next
    1.58 +    case (real r)
    1.59 +    then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
    1.60 +    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
    1.61 +    then obtain b where b_def: "a<b \<and> b<a+e"
    1.62 +      using fin ereal_between dense[of a "a+e"] by auto
    1.63 +    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
    1.64 +    then show False using b_def e by auto
    1.65 +  qed
    1.66 +qed
    1.67 +
    1.68  subsubsection {* Convergent sequences *}
    1.69  
    1.70  lemma lim_ereal[simp]:
    1.71 @@ -1981,123 +1986,15 @@
    1.72      using ereal_LimI_finite[of x] assms by auto
    1.73  qed
    1.74  
    1.75 -
    1.76 -subsubsection {* @{text Liminf} and @{text Limsup} *}
    1.77 -
    1.78 -definition
    1.79 -  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
    1.80 -
    1.81 -definition
    1.82 -  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
    1.83 -
    1.84 -abbreviation "liminf \<equiv> Liminf sequentially"
    1.85 -
    1.86 -abbreviation "limsup \<equiv> Limsup sequentially"
    1.87 -
    1.88 -lemma Liminf_eqI:
    1.89 -  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    1.90 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    1.91 -  unfolding Liminf_def by (auto intro!: SUP_eqI)
    1.92 -
    1.93 -lemma Limsup_eqI:
    1.94 -  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    1.95 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    1.96 -  unfolding Limsup_def by (auto intro!: INF_eqI)
    1.97 -
    1.98 -lemma liminf_SUPR_INFI:
    1.99 -  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
   1.100 -  shows "liminf f = (SUP n. INF m:{n..}. f m)"
   1.101 -  unfolding Liminf_def eventually_sequentially
   1.102 -  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
   1.103 -
   1.104 -lemma limsup_INFI_SUPR:
   1.105 -  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
   1.106 -  shows "limsup f = (INF n. SUP m:{n..}. f m)"
   1.107 -  unfolding Limsup_def eventually_sequentially
   1.108 -  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
   1.109 -
   1.110 -lemma Limsup_const: 
   1.111 -  assumes ntriv: "\<not> trivial_limit F"
   1.112 -  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
   1.113 -proof -
   1.114 -  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
   1.115 -  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
   1.116 -    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
   1.117 -  then show ?thesis
   1.118 -    unfolding Limsup_def using eventually_True
   1.119 -    by (subst INF_cong[where D="\<lambda>x. c"])
   1.120 -       (auto intro!: INF_const simp del: eventually_True)
   1.121 -qed
   1.122 +lemma ereal_Limsup_uminus:
   1.123 +  fixes f :: "'a => ereal"
   1.124 +  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
   1.125 +  unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
   1.126  
   1.127 -lemma Liminf_const:
   1.128 -  assumes ntriv: "\<not> trivial_limit F"
   1.129 -  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
   1.130 -proof -
   1.131 -  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
   1.132 -  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
   1.133 -    using ntriv by (intro INF_const) (auto simp: eventually_False *)
   1.134 -  then show ?thesis
   1.135 -    unfolding Liminf_def using eventually_True
   1.136 -    by (subst SUP_cong[where D="\<lambda>x. c"])
   1.137 -       (auto intro!: SUP_const simp del: eventually_True)
   1.138 -qed
   1.139 -
   1.140 -lemma Liminf_mono:
   1.141 -  fixes f g :: "'a => 'b :: complete_lattice"
   1.142 -  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   1.143 -  shows "Liminf F f \<le> Liminf F g"
   1.144 -  unfolding Liminf_def
   1.145 -proof (safe intro!: SUP_mono)
   1.146 -  fix P assume "eventually P F"
   1.147 -  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   1.148 -  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
   1.149 -    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
   1.150 -qed
   1.151 -
   1.152 -lemma Liminf_eq:
   1.153 -  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   1.154 -  assumes "eventually (\<lambda>x. f x = g x) F"
   1.155 -  shows "Liminf F f = Liminf F g"
   1.156 -  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
   1.157 -
   1.158 -lemma Limsup_mono:
   1.159 -  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   1.160 -  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   1.161 -  shows "Limsup F f \<le> Limsup F g"
   1.162 -  unfolding Limsup_def
   1.163 -proof (safe intro!: INF_mono)
   1.164 -  fix P assume "eventually P F"
   1.165 -  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   1.166 -  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
   1.167 -    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
   1.168 -qed
   1.169 -
   1.170 -lemma Limsup_eq:
   1.171 -  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   1.172 -  assumes "eventually (\<lambda>x. f x = g x) net"
   1.173 -  shows "Limsup net f = Limsup net g"
   1.174 -  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
   1.175 -
   1.176 -lemma Liminf_le_Limsup:
   1.177 -  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   1.178 -  assumes ntriv: "\<not> trivial_limit F"
   1.179 -  shows "Liminf F f \<le> Limsup F f"
   1.180 -  unfolding Limsup_def Liminf_def
   1.181 -  apply (rule complete_lattice_class.SUP_least)
   1.182 -  apply (rule complete_lattice_class.INF_greatest)
   1.183 -proof safe
   1.184 -  fix P Q assume "eventually P F" "eventually Q F"
   1.185 -  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   1.186 -  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
   1.187 -    using ntriv by (auto simp add: eventually_False)
   1.188 -  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
   1.189 -    by (rule INF_mono) auto
   1.190 -  also have "\<dots> \<le> SUPR (Collect ?C) f"
   1.191 -    using not_False by (intro INF_le_SUP) auto
   1.192 -  also have "\<dots> \<le> SUPR (Collect Q) f"
   1.193 -    by (rule SUP_mono) auto
   1.194 -  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
   1.195 -qed
   1.196 +lemma liminf_bounded_iff:
   1.197 +  fixes x :: "nat \<Rightarrow> ereal"
   1.198 +  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
   1.199 +  unfolding le_Liminf_iff eventually_sequentially ..
   1.200  
   1.201  lemma
   1.202    fixes X :: "nat \<Rightarrow> ereal"
   1.203 @@ -2105,220 +2002,6 @@
   1.204      and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
   1.205    unfolding incseq_def decseq_def by auto
   1.206  
   1.207 -lemma Liminf_bounded:
   1.208 -  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   1.209 -  assumes ntriv: "\<not> trivial_limit F"
   1.210 -  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   1.211 -  shows "C \<le> Liminf F X"
   1.212 -  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
   1.213 -
   1.214 -lemma Limsup_bounded:
   1.215 -  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   1.216 -  assumes ntriv: "\<not> trivial_limit F"
   1.217 -  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   1.218 -  shows "Limsup F X \<le> C"
   1.219 -  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
   1.220 -
   1.221 -lemma le_Liminf_iff:
   1.222 -  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   1.223 -  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   1.224 -proof -
   1.225 -  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
   1.226 -    then have "eventually (\<lambda>x. y < X x) F"
   1.227 -      by (auto elim!: eventually_elim1 dest: less_INF_D) }
   1.228 -  moreover
   1.229 -  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
   1.230 -    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
   1.231 -    proof cases
   1.232 -      assume "\<exists>z. y < z \<and> z < C"
   1.233 -      then guess z ..
   1.234 -      moreover then have "z \<le> INFI {x. z < X x} X"
   1.235 -        by (auto intro!: INF_greatest)
   1.236 -      ultimately show ?thesis
   1.237 -        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   1.238 -    next
   1.239 -      assume "\<not> (\<exists>z. y < z \<and> z < C)"
   1.240 -      then have "C \<le> INFI {x. y < X x} X"
   1.241 -        by (intro INF_greatest) auto
   1.242 -      with `y < C` show ?thesis
   1.243 -        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   1.244 -    qed }
   1.245 -  ultimately show ?thesis
   1.246 -    unfolding Liminf_def le_SUP_iff by auto
   1.247 -qed
   1.248 -
   1.249 -lemma lim_imp_Liminf:
   1.250 -  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
   1.251 -  assumes ntriv: "\<not> trivial_limit F"
   1.252 -  assumes lim: "(f ---> f0) F"
   1.253 -  shows "Liminf F f = f0"
   1.254 -proof (intro Liminf_eqI)
   1.255 -  fix P assume P: "eventually P F"
   1.256 -  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
   1.257 -    by eventually_elim (auto intro!: INF_lower)
   1.258 -  then show "INFI (Collect P) f \<le> f0"
   1.259 -    by (rule tendsto_le[OF ntriv lim tendsto_const])
   1.260 -next
   1.261 -  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
   1.262 -  show "f0 \<le> y"
   1.263 -  proof cases
   1.264 -    assume "\<exists>z. y < z \<and> z < f0"
   1.265 -    then guess z ..
   1.266 -    moreover have "z \<le> INFI {x. z < f x} f"
   1.267 -      by (rule INF_greatest) simp
   1.268 -    ultimately show ?thesis
   1.269 -      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   1.270 -  next
   1.271 -    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
   1.272 -    show ?thesis
   1.273 -    proof (rule classical)
   1.274 -      assume "\<not> f0 \<le> y"
   1.275 -      then have "eventually (\<lambda>x. y < f x) F"
   1.276 -        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   1.277 -      then have "eventually (\<lambda>x. f0 \<le> f x) F"
   1.278 -        using discrete by (auto elim!: eventually_elim1)
   1.279 -      then have "INFI {x. f0 \<le> f x} f \<le> y"
   1.280 -        by (rule upper)
   1.281 -      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
   1.282 -        by (intro INF_greatest) simp
   1.283 -      ultimately show "f0 \<le> y" by simp
   1.284 -    qed
   1.285 -  qed
   1.286 -qed
   1.287 -
   1.288 -lemma lim_imp_Limsup:
   1.289 -  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
   1.290 -  assumes ntriv: "\<not> trivial_limit F"
   1.291 -  assumes lim: "(f ---> f0) F"
   1.292 -  shows "Limsup F f = f0"
   1.293 -proof (intro Limsup_eqI)
   1.294 -  fix P assume P: "eventually P F"
   1.295 -  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
   1.296 -    by eventually_elim (auto intro!: SUP_upper)
   1.297 -  then show "f0 \<le> SUPR (Collect P) f"
   1.298 -    by (rule tendsto_le[OF ntriv tendsto_const lim])
   1.299 -next
   1.300 -  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
   1.301 -  show "y \<le> f0"
   1.302 -  proof cases
   1.303 -    assume "\<exists>z. f0 < z \<and> z < y"
   1.304 -    then guess z ..
   1.305 -    moreover have "SUPR {x. f x < z} f \<le> z"
   1.306 -      by (rule SUP_least) simp
   1.307 -    ultimately show ?thesis
   1.308 -      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   1.309 -  next
   1.310 -    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
   1.311 -    show ?thesis
   1.312 -    proof (rule classical)
   1.313 -      assume "\<not> y \<le> f0"
   1.314 -      then have "eventually (\<lambda>x. f x < y) F"
   1.315 -        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   1.316 -      then have "eventually (\<lambda>x. f x \<le> f0) F"
   1.317 -        using discrete by (auto elim!: eventually_elim1 simp: not_less)
   1.318 -      then have "y \<le> SUPR {x. f x \<le> f0} f"
   1.319 -        by (rule lower)
   1.320 -      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
   1.321 -        by (intro SUP_least) simp
   1.322 -      ultimately show "y \<le> f0" by simp
   1.323 -    qed
   1.324 -  qed
   1.325 -qed
   1.326 -
   1.327 -lemma Liminf_eq_Limsup:
   1.328 -  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
   1.329 -  assumes ntriv: "\<not> trivial_limit F"
   1.330 -    and lim: "Liminf F f = f0" "Limsup F f = f0"
   1.331 -  shows "(f ---> f0) F"
   1.332 -proof (rule order_tendstoI)
   1.333 -  fix a assume "f0 < a"
   1.334 -  with assms have "Limsup F f < a" by simp
   1.335 -  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
   1.336 -    unfolding Limsup_def INF_less_iff by auto
   1.337 -  then show "eventually (\<lambda>x. f x < a) F"
   1.338 -    by (auto elim!: eventually_elim1 dest: SUP_lessD)
   1.339 -next
   1.340 -  fix a assume "a < f0"
   1.341 -  with assms have "a < Liminf F f" by simp
   1.342 -  then obtain P where "eventually P F" "a < INFI (Collect P) f"
   1.343 -    unfolding Liminf_def less_SUP_iff by auto
   1.344 -  then show "eventually (\<lambda>x. a < f x) F"
   1.345 -    by (auto elim!: eventually_elim1 dest: less_INF_D)
   1.346 -qed
   1.347 -
   1.348 -lemma tendsto_iff_Liminf_eq_Limsup:
   1.349 -  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
   1.350 -  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   1.351 -  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
   1.352 -
   1.353 -lemma liminf_bounded_iff:
   1.354 -  fixes x :: "nat \<Rightarrow> ereal"
   1.355 -  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
   1.356 -  unfolding le_Liminf_iff eventually_sequentially ..
   1.357 -
   1.358 -lemma liminf_subseq_mono:
   1.359 -  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   1.360 -  assumes "subseq r"
   1.361 -  shows "liminf X \<le> liminf (X \<circ> r) "
   1.362 -proof-
   1.363 -  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   1.364 -  proof (safe intro!: INF_mono)
   1.365 -    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   1.366 -      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
   1.367 -  qed
   1.368 -  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
   1.369 -qed
   1.370 -
   1.371 -lemma limsup_subseq_mono:
   1.372 -  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   1.373 -  assumes "subseq r"
   1.374 -  shows "limsup (X \<circ> r) \<le> limsup X"
   1.375 -proof-
   1.376 -  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
   1.377 -  proof (safe intro!: SUP_mono)
   1.378 -    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
   1.379 -      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
   1.380 -  qed
   1.381 -  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
   1.382 -qed
   1.383 -
   1.384 -definition (in order) mono_set:
   1.385 -  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
   1.386 -
   1.387 -lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
   1.388 -lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
   1.389 -lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
   1.390 -lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
   1.391 -
   1.392 -lemma (in complete_linorder) mono_set_iff:
   1.393 -  fixes S :: "'a set"
   1.394 -  defines "a \<equiv> Inf S"
   1.395 -  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
   1.396 -proof
   1.397 -  assume "mono_set S"
   1.398 -  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
   1.399 -  show ?c
   1.400 -  proof cases
   1.401 -    assume "a \<in> S"
   1.402 -    show ?c
   1.403 -      using mono[OF _ `a \<in> S`]
   1.404 -      by (auto intro: Inf_lower simp: a_def)
   1.405 -  next
   1.406 -    assume "a \<notin> S"
   1.407 -    have "S = {a <..}"
   1.408 -    proof safe
   1.409 -      fix x assume "x \<in> S"
   1.410 -      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
   1.411 -      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
   1.412 -    next
   1.413 -      fix x assume "a < x"
   1.414 -      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
   1.415 -      with mono[of y x] show "x \<in> S" by auto
   1.416 -    qed
   1.417 -    then show ?c ..
   1.418 -  qed
   1.419 -qed auto
   1.420 -
   1.421  subsubsection {* Tests for code generator *}
   1.422  
   1.423  (* A small list of simple arithmetic expressions *)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 05 15:43:08 2013 +0100
     2.3 @@ -0,0 +1,320 @@
     2.4 +(*  Title:      HOL/Library/Liminf_Limsup.thy
     2.5 +    Author:     Johannes Hölzl, TU München
     2.6 +*)
     2.7 +
     2.8 +header {* Liminf and Limsup on complete lattices *}
     2.9 +
    2.10 +theory Liminf_Limsup
    2.11 +imports "~~/src/HOL/Complex_Main"
    2.12 +begin
    2.13 +
    2.14 +lemma le_Sup_iff_less:
    2.15 +  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
    2.16 +  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
    2.17 +  unfolding le_SUP_iff
    2.18 +  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
    2.19 +
    2.20 +lemma Inf_le_iff_less:
    2.21 +  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
    2.22 +  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
    2.23 +  unfolding INF_le_iff
    2.24 +  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
    2.25 +
    2.26 +lemma SUPR_pair:
    2.27 +  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    2.28 +  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    2.29 +
    2.30 +lemma INFI_pair:
    2.31 +  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    2.32 +  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    2.33 +
    2.34 +subsubsection {* @{text Liminf} and @{text Limsup} *}
    2.35 +
    2.36 +definition
    2.37 +  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
    2.38 +
    2.39 +definition
    2.40 +  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
    2.41 +
    2.42 +abbreviation "liminf \<equiv> Liminf sequentially"
    2.43 +
    2.44 +abbreviation "limsup \<equiv> Limsup sequentially"
    2.45 +
    2.46 +lemma Liminf_eqI:
    2.47 +  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
    2.48 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    2.49 +  unfolding Liminf_def by (auto intro!: SUP_eqI)
    2.50 +
    2.51 +lemma Limsup_eqI:
    2.52 +  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
    2.53 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    2.54 +  unfolding Limsup_def by (auto intro!: INF_eqI)
    2.55 +
    2.56 +lemma liminf_SUPR_INFI:
    2.57 +  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
    2.58 +  shows "liminf f = (SUP n. INF m:{n..}. f m)"
    2.59 +  unfolding Liminf_def eventually_sequentially
    2.60 +  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
    2.61 +
    2.62 +lemma limsup_INFI_SUPR:
    2.63 +  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
    2.64 +  shows "limsup f = (INF n. SUP m:{n..}. f m)"
    2.65 +  unfolding Limsup_def eventually_sequentially
    2.66 +  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
    2.67 +
    2.68 +lemma Limsup_const: 
    2.69 +  assumes ntriv: "\<not> trivial_limit F"
    2.70 +  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
    2.71 +proof -
    2.72 +  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    2.73 +  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
    2.74 +    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
    2.75 +  then show ?thesis
    2.76 +    unfolding Limsup_def using eventually_True
    2.77 +    by (subst INF_cong[where D="\<lambda>x. c"])
    2.78 +       (auto intro!: INF_const simp del: eventually_True)
    2.79 +qed
    2.80 +
    2.81 +lemma Liminf_const:
    2.82 +  assumes ntriv: "\<not> trivial_limit F"
    2.83 +  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
    2.84 +proof -
    2.85 +  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
    2.86 +  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
    2.87 +    using ntriv by (intro INF_const) (auto simp: eventually_False *)
    2.88 +  then show ?thesis
    2.89 +    unfolding Liminf_def using eventually_True
    2.90 +    by (subst SUP_cong[where D="\<lambda>x. c"])
    2.91 +       (auto intro!: SUP_const simp del: eventually_True)
    2.92 +qed
    2.93 +
    2.94 +lemma Liminf_mono:
    2.95 +  fixes f g :: "'a => 'b :: complete_lattice"
    2.96 +  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
    2.97 +  shows "Liminf F f \<le> Liminf F g"
    2.98 +  unfolding Liminf_def
    2.99 +proof (safe intro!: SUP_mono)
   2.100 +  fix P assume "eventually P F"
   2.101 +  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   2.102 +  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
   2.103 +    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
   2.104 +qed
   2.105 +
   2.106 +lemma Liminf_eq:
   2.107 +  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   2.108 +  assumes "eventually (\<lambda>x. f x = g x) F"
   2.109 +  shows "Liminf F f = Liminf F g"
   2.110 +  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
   2.111 +
   2.112 +lemma Limsup_mono:
   2.113 +  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   2.114 +  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
   2.115 +  shows "Limsup F f \<le> Limsup F g"
   2.116 +  unfolding Limsup_def
   2.117 +proof (safe intro!: INF_mono)
   2.118 +  fix P assume "eventually P F"
   2.119 +  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   2.120 +  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
   2.121 +    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
   2.122 +qed
   2.123 +
   2.124 +lemma Limsup_eq:
   2.125 +  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
   2.126 +  assumes "eventually (\<lambda>x. f x = g x) net"
   2.127 +  shows "Limsup net f = Limsup net g"
   2.128 +  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
   2.129 +
   2.130 +lemma Liminf_le_Limsup:
   2.131 +  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
   2.132 +  assumes ntriv: "\<not> trivial_limit F"
   2.133 +  shows "Liminf F f \<le> Limsup F f"
   2.134 +  unfolding Limsup_def Liminf_def
   2.135 +  apply (rule complete_lattice_class.SUP_least)
   2.136 +  apply (rule complete_lattice_class.INF_greatest)
   2.137 +proof safe
   2.138 +  fix P Q assume "eventually P F" "eventually Q F"
   2.139 +  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   2.140 +  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
   2.141 +    using ntriv by (auto simp add: eventually_False)
   2.142 +  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
   2.143 +    by (rule INF_mono) auto
   2.144 +  also have "\<dots> \<le> SUPR (Collect ?C) f"
   2.145 +    using not_False by (intro INF_le_SUP) auto
   2.146 +  also have "\<dots> \<le> SUPR (Collect Q) f"
   2.147 +    by (rule SUP_mono) auto
   2.148 +  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
   2.149 +qed
   2.150 +
   2.151 +lemma Liminf_bounded:
   2.152 +  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   2.153 +  assumes ntriv: "\<not> trivial_limit F"
   2.154 +  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
   2.155 +  shows "C \<le> Liminf F X"
   2.156 +  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
   2.157 +
   2.158 +lemma Limsup_bounded:
   2.159 +  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
   2.160 +  assumes ntriv: "\<not> trivial_limit F"
   2.161 +  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
   2.162 +  shows "Limsup F X \<le> C"
   2.163 +  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
   2.164 +
   2.165 +lemma le_Liminf_iff:
   2.166 +  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   2.167 +  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   2.168 +proof -
   2.169 +  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
   2.170 +    then have "eventually (\<lambda>x. y < X x) F"
   2.171 +      by (auto elim!: eventually_elim1 dest: less_INF_D) }
   2.172 +  moreover
   2.173 +  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
   2.174 +    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
   2.175 +    proof cases
   2.176 +      assume "\<exists>z. y < z \<and> z < C"
   2.177 +      then guess z ..
   2.178 +      moreover then have "z \<le> INFI {x. z < X x} X"
   2.179 +        by (auto intro!: INF_greatest)
   2.180 +      ultimately show ?thesis
   2.181 +        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   2.182 +    next
   2.183 +      assume "\<not> (\<exists>z. y < z \<and> z < C)"
   2.184 +      then have "C \<le> INFI {x. y < X x} X"
   2.185 +        by (intro INF_greatest) auto
   2.186 +      with `y < C` show ?thesis
   2.187 +        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   2.188 +    qed }
   2.189 +  ultimately show ?thesis
   2.190 +    unfolding Liminf_def le_SUP_iff by auto
   2.191 +qed
   2.192 +
   2.193 +lemma lim_imp_Liminf:
   2.194 +  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
   2.195 +  assumes ntriv: "\<not> trivial_limit F"
   2.196 +  assumes lim: "(f ---> f0) F"
   2.197 +  shows "Liminf F f = f0"
   2.198 +proof (intro Liminf_eqI)
   2.199 +  fix P assume P: "eventually P F"
   2.200 +  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
   2.201 +    by eventually_elim (auto intro!: INF_lower)
   2.202 +  then show "INFI (Collect P) f \<le> f0"
   2.203 +    by (rule tendsto_le[OF ntriv lim tendsto_const])
   2.204 +next
   2.205 +  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
   2.206 +  show "f0 \<le> y"
   2.207 +  proof cases
   2.208 +    assume "\<exists>z. y < z \<and> z < f0"
   2.209 +    then guess z ..
   2.210 +    moreover have "z \<le> INFI {x. z < f x} f"
   2.211 +      by (rule INF_greatest) simp
   2.212 +    ultimately show ?thesis
   2.213 +      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   2.214 +  next
   2.215 +    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
   2.216 +    show ?thesis
   2.217 +    proof (rule classical)
   2.218 +      assume "\<not> f0 \<le> y"
   2.219 +      then have "eventually (\<lambda>x. y < f x) F"
   2.220 +        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   2.221 +      then have "eventually (\<lambda>x. f0 \<le> f x) F"
   2.222 +        using discrete by (auto elim!: eventually_elim1)
   2.223 +      then have "INFI {x. f0 \<le> f x} f \<le> y"
   2.224 +        by (rule upper)
   2.225 +      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
   2.226 +        by (intro INF_greatest) simp
   2.227 +      ultimately show "f0 \<le> y" by simp
   2.228 +    qed
   2.229 +  qed
   2.230 +qed
   2.231 +
   2.232 +lemma lim_imp_Limsup:
   2.233 +  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
   2.234 +  assumes ntriv: "\<not> trivial_limit F"
   2.235 +  assumes lim: "(f ---> f0) F"
   2.236 +  shows "Limsup F f = f0"
   2.237 +proof (intro Limsup_eqI)
   2.238 +  fix P assume P: "eventually P F"
   2.239 +  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
   2.240 +    by eventually_elim (auto intro!: SUP_upper)
   2.241 +  then show "f0 \<le> SUPR (Collect P) f"
   2.242 +    by (rule tendsto_le[OF ntriv tendsto_const lim])
   2.243 +next
   2.244 +  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
   2.245 +  show "y \<le> f0"
   2.246 +  proof cases
   2.247 +    assume "\<exists>z. f0 < z \<and> z < y"
   2.248 +    then guess z ..
   2.249 +    moreover have "SUPR {x. f x < z} f \<le> z"
   2.250 +      by (rule SUP_least) simp
   2.251 +    ultimately show ?thesis
   2.252 +      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   2.253 +  next
   2.254 +    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
   2.255 +    show ?thesis
   2.256 +    proof (rule classical)
   2.257 +      assume "\<not> y \<le> f0"
   2.258 +      then have "eventually (\<lambda>x. f x < y) F"
   2.259 +        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   2.260 +      then have "eventually (\<lambda>x. f x \<le> f0) F"
   2.261 +        using discrete by (auto elim!: eventually_elim1 simp: not_less)
   2.262 +      then have "y \<le> SUPR {x. f x \<le> f0} f"
   2.263 +        by (rule lower)
   2.264 +      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
   2.265 +        by (intro SUP_least) simp
   2.266 +      ultimately show "y \<le> f0" by simp
   2.267 +    qed
   2.268 +  qed
   2.269 +qed
   2.270 +
   2.271 +lemma Liminf_eq_Limsup:
   2.272 +  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
   2.273 +  assumes ntriv: "\<not> trivial_limit F"
   2.274 +    and lim: "Liminf F f = f0" "Limsup F f = f0"
   2.275 +  shows "(f ---> f0) F"
   2.276 +proof (rule order_tendstoI)
   2.277 +  fix a assume "f0 < a"
   2.278 +  with assms have "Limsup F f < a" by simp
   2.279 +  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
   2.280 +    unfolding Limsup_def INF_less_iff by auto
   2.281 +  then show "eventually (\<lambda>x. f x < a) F"
   2.282 +    by (auto elim!: eventually_elim1 dest: SUP_lessD)
   2.283 +next
   2.284 +  fix a assume "a < f0"
   2.285 +  with assms have "a < Liminf F f" by simp
   2.286 +  then obtain P where "eventually P F" "a < INFI (Collect P) f"
   2.287 +    unfolding Liminf_def less_SUP_iff by auto
   2.288 +  then show "eventually (\<lambda>x. a < f x) F"
   2.289 +    by (auto elim!: eventually_elim1 dest: less_INF_D)
   2.290 +qed
   2.291 +
   2.292 +lemma tendsto_iff_Liminf_eq_Limsup:
   2.293 +  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
   2.294 +  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   2.295 +  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
   2.296 +
   2.297 +lemma liminf_subseq_mono:
   2.298 +  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   2.299 +  assumes "subseq r"
   2.300 +  shows "liminf X \<le> liminf (X \<circ> r) "
   2.301 +proof-
   2.302 +  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   2.303 +  proof (safe intro!: INF_mono)
   2.304 +    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   2.305 +      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
   2.306 +  qed
   2.307 +  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
   2.308 +qed
   2.309 +
   2.310 +lemma limsup_subseq_mono:
   2.311 +  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   2.312 +  assumes "subseq r"
   2.313 +  shows "limsup (X \<circ> r) \<le> limsup X"
   2.314 +proof-
   2.315 +  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
   2.316 +  proof (safe intro!: SUP_mono)
   2.317 +    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
   2.318 +      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
   2.319 +  qed
   2.320 +  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
   2.321 +qed
   2.322 +
   2.323 +end
     3.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 15:27:08 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 15:43:08 2013 +0100
     3.3 @@ -22,35 +22,13 @@
     3.4  
     3.5  lemma ereal_open_uminus:
     3.6    fixes S :: "ereal set"
     3.7 -  assumes "open S"
     3.8 -  shows "open (uminus ` S)"
     3.9 -  unfolding open_ereal_def
    3.10 -proof (intro conjI impI)
    3.11 -  obtain x y where
    3.12 -    S: "open (ereal -` S)" "\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S"
    3.13 -    using `open S` unfolding open_ereal_def by auto
    3.14 -  have "ereal -` uminus ` S = uminus ` (ereal -` S)"
    3.15 -  proof safe
    3.16 -    fix x y
    3.17 -    assume "ereal x = - y" "y \<in> S"
    3.18 -    then show "x \<in> uminus ` ereal -` S" by (cases y) auto
    3.19 -  next
    3.20 -    fix x
    3.21 -    assume "ereal x \<in> S"
    3.22 -    then show "- x \<in> ereal -` uminus ` S"
    3.23 -      by (auto intro: image_eqI[of _ _ "ereal x"])
    3.24 -  qed
    3.25 -  then show "open (ereal -` uminus ` S)"
    3.26 -    using S by (auto intro: open_negations)
    3.27 -  { assume "\<infinity> \<in> uminus ` S"
    3.28 -    then have "-\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus)
    3.29 -    then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
    3.30 -    then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto }
    3.31 -  { assume "-\<infinity> \<in> uminus ` S"
    3.32 -    then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus)
    3.33 -    then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto
    3.34 -    then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }
    3.35 -qed
    3.36 +  assumes "open S" shows "open (uminus ` S)"
    3.37 +  using `open S`[unfolded open_generated_order]
    3.38 +proof induct
    3.39 +  have "range uminus = (UNIV :: ereal set)"
    3.40 +    by (auto simp: image_iff ereal_uminus_eq_reorder)
    3.41 +  then show "open (range uminus :: ereal set)" by simp
    3.42 +qed (auto simp add: image_Union image_Int)
    3.43  
    3.44  lemma ereal_uminus_complement:
    3.45    fixes S :: "ereal set"
    3.46 @@ -61,32 +39,7 @@
    3.47    fixes S :: "ereal set"
    3.48    assumes "closed S"
    3.49    shows "closed (uminus ` S)"
    3.50 -  using assms unfolding closed_def
    3.51 -  using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
    3.52 -
    3.53 -instance ereal :: perfect_space
    3.54 -proof (default, rule)
    3.55 -  fix a :: ereal assume a: "open {a}"
    3.56 -  show False
    3.57 -  proof (cases a)
    3.58 -    case MInf
    3.59 -    then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
    3.60 -    then have "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
    3.61 -    then show False using `a=(-\<infinity>)` by auto
    3.62 -  next
    3.63 -    case PInf
    3.64 -    then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
    3.65 -    then have "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
    3.66 -    then show False using `a=\<infinity>` by auto
    3.67 -  next
    3.68 -    case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
    3.69 -    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
    3.70 -    then obtain b where b_def: "a<b & b<a+e"
    3.71 -      using fin ereal_between dense[of a "a+e"] by auto
    3.72 -    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
    3.73 -    then show False using b_def e by auto
    3.74 -  qed
    3.75 -qed
    3.76 +  using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus)
    3.77  
    3.78  lemma ereal_closed_contains_Inf:
    3.79    fixes S :: "ereal set"
    3.80 @@ -303,113 +256,9 @@
    3.81    then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
    3.82  qed
    3.83  
    3.84 -lemma ereal_open_mono_set:
    3.85 -  fixes S :: "ereal set"
    3.86 -  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
    3.87 -  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
    3.88 -    ereal_open_closed mono_set_iff open_ereal_greaterThan)
    3.89 -
    3.90 -lemma ereal_closed_mono_set:
    3.91 -  fixes S :: "ereal set"
    3.92 -  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
    3.93 -  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
    3.94 -    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
    3.95 -
    3.96 -lemma ereal_Liminf_Sup_monoset:
    3.97 -  fixes f :: "'a => ereal"
    3.98 -  shows "Liminf net f =
    3.99 -    Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   3.100 -    (is "_ = Sup ?A")
   3.101 -proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
   3.102 -  fix P assume P: "eventually P net"
   3.103 -  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
   3.104 -  { fix x assume "P x"
   3.105 -    then have "INFI (Collect P) f \<le> f x"
   3.106 -      by (intro complete_lattice_class.INF_lower) simp
   3.107 -    with S have "f x \<in> S"
   3.108 -      by (simp add: mono_set) }
   3.109 -  with P show "eventually (\<lambda>x. f x \<in> S) net"
   3.110 -    by (auto elim: eventually_elim1)
   3.111 -next
   3.112 -  fix y l
   3.113 -  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   3.114 -  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
   3.115 -  show "l \<le> y"
   3.116 -  proof (rule dense_le)
   3.117 -    fix B assume "B < l"
   3.118 -    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
   3.119 -      by (intro S[rule_format]) auto
   3.120 -    then have "INFI {x. B < f x} f \<le> y"
   3.121 -      using P by auto
   3.122 -    moreover have "B \<le> INFI {x. B < f x} f"
   3.123 -      by (intro INF_greatest) auto
   3.124 -    ultimately show "B \<le> y"
   3.125 -      by simp
   3.126 -  qed
   3.127 -qed
   3.128 -
   3.129 -lemma ereal_Limsup_Inf_monoset:
   3.130 -  fixes f :: "'a => ereal"
   3.131 -  shows "Limsup net f =
   3.132 -    Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   3.133 -    (is "_ = Inf ?A")
   3.134 -proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
   3.135 -  fix P assume P: "eventually P net"
   3.136 -  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
   3.137 -  { fix x assume "P x"
   3.138 -    then have "f x \<le> SUPR (Collect P) f"
   3.139 -      by (intro complete_lattice_class.SUP_upper) simp
   3.140 -    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
   3.141 -    have "f x \<in> S"
   3.142 -      by (simp add: inj_image_mem_iff) }
   3.143 -  with P show "eventually (\<lambda>x. f x \<in> S) net"
   3.144 -    by (auto elim: eventually_elim1)
   3.145 -next
   3.146 -  fix y l
   3.147 -  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   3.148 -  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   3.149 -  show "y \<le> l"
   3.150 -  proof (rule dense_ge)
   3.151 -    fix B assume "l < B"
   3.152 -    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   3.153 -      by (intro S[rule_format]) auto
   3.154 -    then have "y \<le> SUPR {x. f x < B} f"
   3.155 -      using P by auto
   3.156 -    moreover have "SUPR {x. f x < B} f \<le> B"
   3.157 -      by (intro SUP_least) auto
   3.158 -    ultimately show "y \<le> B"
   3.159 -      by simp
   3.160 -  qed
   3.161 -qed
   3.162 -
   3.163  lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
   3.164    using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
   3.165  
   3.166 -lemma ereal_Limsup_uminus:
   3.167 -  fixes f :: "'a => ereal"
   3.168 -  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
   3.169 -proof -
   3.170 -  { fix P l
   3.171 -    have "(\<exists>x. (l::ereal) = -x \<and> P x) \<longleftrightarrow> P (-l)"
   3.172 -      by (auto intro!: exI[of _ "-l"]) }
   3.173 -  note Ex_cancel = this
   3.174 -  { fix P :: "ereal set \<Rightarrow> bool"
   3.175 -    have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
   3.176 -      apply auto
   3.177 -      apply (erule_tac x="uminus`S" in allE)
   3.178 -      apply (auto simp: image_image)
   3.179 -      done }
   3.180 -  note add_uminus_image = this
   3.181 -  { fix x S
   3.182 -    have "(x::ereal) \<in> uminus`S \<longleftrightarrow> -x\<in>S"
   3.183 -      by (auto intro!: image_eqI[of _ _ "-x"]) }
   3.184 -  note remove_uminus_image = this
   3.185 -  show ?thesis
   3.186 -    unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset
   3.187 -    unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
   3.188 -    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
   3.189 -qed
   3.190 -
   3.191  lemma ereal_Liminf_uminus:
   3.192    fixes f :: "'a => ereal"
   3.193    shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
   3.194 @@ -423,14 +272,6 @@
   3.195      ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
   3.196    by (auto simp: ereal_uminus_reorder)
   3.197  
   3.198 -lemma lim_imp_Limsup:
   3.199 -  fixes f :: "'a => ereal"
   3.200 -  assumes "\<not> trivial_limit net"
   3.201 -    and lim: "(f ---> f0) net"
   3.202 -  shows "Limsup net f = f0"
   3.203 -  using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
   3.204 -     ereal_Liminf_uminus[of net f] assms by simp
   3.205 -
   3.206  lemma convergent_ereal_limsup:
   3.207    fixes X :: "nat \<Rightarrow> ereal"
   3.208    shows "convergent X \<Longrightarrow> limsup X = lim X"
   3.209 @@ -461,43 +302,10 @@
   3.210    using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
   3.211          ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
   3.212  
   3.213 -lemma ereal_Liminf_eq_Limsup:
   3.214 -  fixes f :: "'a \<Rightarrow> ereal"
   3.215 -  assumes ntriv: "\<not> trivial_limit net"
   3.216 -    and lim: "Liminf net f = f0" "Limsup net f = f0"
   3.217 -  shows "(f ---> f0) net"
   3.218 -proof (cases f0)
   3.219 -  case PInf
   3.220 -  then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
   3.221 -next
   3.222 -  case MInf
   3.223 -  then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
   3.224 -next
   3.225 -  case (real r)
   3.226 -  show "(f ---> f0) net"
   3.227 -  proof (rule topological_tendstoI)
   3.228 -    fix S
   3.229 -    assume "open S" "f0 \<in> S"
   3.230 -    then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
   3.231 -      using ereal_open_cont_interval2[of S f0] real lim by auto
   3.232 -    then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
   3.233 -      unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
   3.234 -      by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
   3.235 -    with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
   3.236 -      by (rule_tac eventually_mono) auto
   3.237 -  qed
   3.238 -qed
   3.239 -
   3.240 -lemma ereal_Liminf_eq_Limsup_iff:
   3.241 -  fixes f :: "'a \<Rightarrow> ereal"
   3.242 -  assumes "\<not> trivial_limit net"
   3.243 -  shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
   3.244 -  by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
   3.245 -
   3.246  lemma convergent_ereal:
   3.247    fixes X :: "nat \<Rightarrow> ereal"
   3.248    shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   3.249 -  using ereal_Liminf_eq_Limsup_iff[of sequentially]
   3.250 +  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   3.251    by (auto simp: convergent_def)
   3.252  
   3.253  lemma limsup_INFI_SUPR:
   3.254 @@ -535,45 +343,6 @@
   3.255    shows "X N >= L"
   3.256    using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   3.257  
   3.258 -lemma liminf_bounded_open:
   3.259 -  fixes x :: "nat \<Rightarrow> ereal"
   3.260 -  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
   3.261 -  (is "_ \<longleftrightarrow> ?P x0")
   3.262 -proof
   3.263 -  assume "?P x0"
   3.264 -  then show "x0 \<le> liminf x"
   3.265 -    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
   3.266 -    by (intro complete_lattice_class.Sup_upper) auto
   3.267 -next
   3.268 -  assume "x0 \<le> liminf x"
   3.269 -  { fix S :: "ereal set"
   3.270 -    assume om: "open S & mono_set S & x0:S"
   3.271 -    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
   3.272 -    moreover
   3.273 -    { assume "~(S=UNIV)"
   3.274 -      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
   3.275 -      then have "B<x0" using om by auto
   3.276 -      then have "EX N. ALL n>=N. x n : S"
   3.277 -        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
   3.278 -    }
   3.279 -    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
   3.280 -  }
   3.281 -  then show "?P x0" by auto
   3.282 -qed
   3.283 -
   3.284 -lemma limsup_subseq_mono:
   3.285 -  fixes X :: "nat \<Rightarrow> ereal"
   3.286 -  assumes "subseq r"
   3.287 -  shows "limsup (X \<circ> r) \<le> limsup X"
   3.288 -proof -
   3.289 -  have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
   3.290 -  then have "- limsup X \<le> - limsup (X \<circ> r)"
   3.291 -     using liminf_subseq_mono[of r "(%n. - X n)"]
   3.292 -       ereal_Liminf_uminus[of sequentially X]
   3.293 -       ereal_Liminf_uminus[of sequentially "X o r"] assms by auto
   3.294 -  then show ?thesis by auto
   3.295 -qed
   3.296 -
   3.297  lemma bounded_abs:
   3.298    assumes "(a::real)<=x" "x<=b"
   3.299    shows "abs x <= max (abs a) (abs b)"
   3.300 @@ -652,85 +421,6 @@
   3.301      show "f ----> x" by auto }
   3.302  qed
   3.303  
   3.304 -lemma Liminf_within:
   3.305 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   3.306 -  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   3.307 -  unfolding Liminf_def eventually_within
   3.308 -proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
   3.309 -  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   3.310 -  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   3.311 -    by (auto simp: zero_less_dist_iff dist_commute)
   3.312 -  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
   3.313 -    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
   3.314 -next
   3.315 -  fix d :: real assume "0 < d"
   3.316 -  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   3.317 -    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
   3.318 -    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   3.319 -       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   3.320 -qed
   3.321 -
   3.322 -lemma Limsup_within:
   3.323 -  fixes f :: "'a::metric_space => 'b::complete_lattice"
   3.324 -  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   3.325 -  unfolding Limsup_def eventually_within
   3.326 -proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
   3.327 -  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   3.328 -  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   3.329 -    by (auto simp: zero_less_dist_iff dist_commute)
   3.330 -  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
   3.331 -    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
   3.332 -next
   3.333 -  fix d :: real assume "0 < d"
   3.334 -  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   3.335 -    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
   3.336 -    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   3.337 -       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   3.338 -qed
   3.339 -
   3.340 -lemma Liminf_within_UNIV:
   3.341 -  fixes f :: "'a::metric_space => _"
   3.342 -  shows "Liminf (at x) f = Liminf (at x within UNIV) f"
   3.343 -  by simp (* TODO: delete *)
   3.344 -
   3.345 -
   3.346 -lemma Liminf_at:
   3.347 -  fixes f :: "'a::metric_space => _"
   3.348 -  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
   3.349 -  using Liminf_within[of x UNIV f] by simp
   3.350 -
   3.351 -
   3.352 -lemma Limsup_within_UNIV:
   3.353 -  fixes f :: "'a::metric_space => _"
   3.354 -  shows "Limsup (at x) f = Limsup (at x within UNIV) f"
   3.355 -  by simp (* TODO: delete *)
   3.356 -
   3.357 -
   3.358 -lemma Limsup_at:
   3.359 -  fixes f :: "'a::metric_space => _"
   3.360 -  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
   3.361 -  using Limsup_within[of x UNIV f] by simp
   3.362 -
   3.363 -lemma Lim_within_constant:
   3.364 -  assumes "ALL y:S. f y = C"
   3.365 -  shows "(f ---> C) (at x within S)"
   3.366 -  unfolding tendsto_def Limits.eventually_within eventually_at_topological
   3.367 -  using assms by simp (metis open_UNIV UNIV_I)
   3.368 -
   3.369 -lemma Liminf_within_constant:
   3.370 -  fixes f :: "'a::topological_space \<Rightarrow> ereal"
   3.371 -  assumes "ALL y:S. f y = C"
   3.372 -    and "~trivial_limit (at x within S)"
   3.373 -  shows "Liminf (at x within S) f = C"
   3.374 -  by (metis Lim_within_constant assms lim_imp_Liminf)
   3.375 -
   3.376 -lemma Limsup_within_constant:
   3.377 -  fixes f :: "'a::topological_space \<Rightarrow> ereal"
   3.378 -  assumes "ALL y:S. f y = C"
   3.379 -    and "~trivial_limit (at x within S)"
   3.380 -  shows "Limsup (at x within S) f = C"
   3.381 -  by (metis Lim_within_constant assms lim_imp_Limsup)
   3.382 -
   3.383  lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
   3.384    unfolding islimpt_def by blast
   3.385  
   3.386 @@ -1317,4 +1007,205 @@
   3.387    then show "\<forall>i. f i = 0" by auto
   3.388  qed simp
   3.389  
   3.390 +lemma Liminf_within:
   3.391 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   3.392 +  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   3.393 +  unfolding Liminf_def eventually_within
   3.394 +proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
   3.395 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   3.396 +  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   3.397 +    by (auto simp: zero_less_dist_iff dist_commute)
   3.398 +  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
   3.399 +    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
   3.400 +next
   3.401 +  fix d :: real assume "0 < d"
   3.402 +  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   3.403 +    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
   3.404 +    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   3.405 +       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   3.406 +qed
   3.407 +
   3.408 +lemma Limsup_within:
   3.409 +  fixes f :: "'a::metric_space => 'b::complete_lattice"
   3.410 +  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   3.411 +  unfolding Limsup_def eventually_within
   3.412 +proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
   3.413 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   3.414 +  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   3.415 +    by (auto simp: zero_less_dist_iff dist_commute)
   3.416 +  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
   3.417 +    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
   3.418 +next
   3.419 +  fix d :: real assume "0 < d"
   3.420 +  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   3.421 +    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
   3.422 +    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   3.423 +       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   3.424 +qed
   3.425 +
   3.426 +lemma Liminf_at:
   3.427 +  fixes f :: "'a::metric_space => _"
   3.428 +  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
   3.429 +  using Liminf_within[of x UNIV f] by simp
   3.430 +
   3.431 +lemma Limsup_at:
   3.432 +  fixes f :: "'a::metric_space => _"
   3.433 +  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
   3.434 +  using Limsup_within[of x UNIV f] by simp
   3.435 +
   3.436 +lemma min_Liminf_at:
   3.437 +  fixes f :: "'a::metric_space => 'b::complete_linorder"
   3.438 +  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
   3.439 +  unfolding inf_min[symmetric] Liminf_at
   3.440 +  apply (subst inf_commute)
   3.441 +  apply (subst SUP_inf)
   3.442 +  apply (intro SUP_cong[OF refl])
   3.443 +  apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
   3.444 +  apply (simp add: INF_def del: inf_ereal_def)
   3.445 +  done
   3.446 +
   3.447 +subsection {* monoset *}
   3.448 +
   3.449 +definition (in order) mono_set:
   3.450 +  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
   3.451 +
   3.452 +lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
   3.453 +lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
   3.454 +lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
   3.455 +lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
   3.456 +
   3.457 +lemma (in complete_linorder) mono_set_iff:
   3.458 +  fixes S :: "'a set"
   3.459 +  defines "a \<equiv> Inf S"
   3.460 +  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
   3.461 +proof
   3.462 +  assume "mono_set S"
   3.463 +  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
   3.464 +  show ?c
   3.465 +  proof cases
   3.466 +    assume "a \<in> S"
   3.467 +    show ?c
   3.468 +      using mono[OF _ `a \<in> S`]
   3.469 +      by (auto intro: Inf_lower simp: a_def)
   3.470 +  next
   3.471 +    assume "a \<notin> S"
   3.472 +    have "S = {a <..}"
   3.473 +    proof safe
   3.474 +      fix x assume "x \<in> S"
   3.475 +      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
   3.476 +      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
   3.477 +    next
   3.478 +      fix x assume "a < x"
   3.479 +      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
   3.480 +      with mono[of y x] show "x \<in> S" by auto
   3.481 +    qed
   3.482 +    then show ?c ..
   3.483 +  qed
   3.484 +qed auto
   3.485 +
   3.486 +lemma ereal_open_mono_set:
   3.487 +  fixes S :: "ereal set"
   3.488 +  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
   3.489 +  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
   3.490 +    ereal_open_closed mono_set_iff open_ereal_greaterThan)
   3.491 +
   3.492 +lemma ereal_closed_mono_set:
   3.493 +  fixes S :: "ereal set"
   3.494 +  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
   3.495 +  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
   3.496 +    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
   3.497 +
   3.498 +lemma ereal_Liminf_Sup_monoset:
   3.499 +  fixes f :: "'a => ereal"
   3.500 +  shows "Liminf net f =
   3.501 +    Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   3.502 +    (is "_ = Sup ?A")
   3.503 +proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
   3.504 +  fix P assume P: "eventually P net"
   3.505 +  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
   3.506 +  { fix x assume "P x"
   3.507 +    then have "INFI (Collect P) f \<le> f x"
   3.508 +      by (intro complete_lattice_class.INF_lower) simp
   3.509 +    with S have "f x \<in> S"
   3.510 +      by (simp add: mono_set) }
   3.511 +  with P show "eventually (\<lambda>x. f x \<in> S) net"
   3.512 +    by (auto elim: eventually_elim1)
   3.513 +next
   3.514 +  fix y l
   3.515 +  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   3.516 +  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
   3.517 +  show "l \<le> y"
   3.518 +  proof (rule dense_le)
   3.519 +    fix B assume "B < l"
   3.520 +    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
   3.521 +      by (intro S[rule_format]) auto
   3.522 +    then have "INFI {x. B < f x} f \<le> y"
   3.523 +      using P by auto
   3.524 +    moreover have "B \<le> INFI {x. B < f x} f"
   3.525 +      by (intro INF_greatest) auto
   3.526 +    ultimately show "B \<le> y"
   3.527 +      by simp
   3.528 +  qed
   3.529 +qed
   3.530 +
   3.531 +lemma ereal_Limsup_Inf_monoset:
   3.532 +  fixes f :: "'a => ereal"
   3.533 +  shows "Limsup net f =
   3.534 +    Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
   3.535 +    (is "_ = Inf ?A")
   3.536 +proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
   3.537 +  fix P assume P: "eventually P net"
   3.538 +  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
   3.539 +  { fix x assume "P x"
   3.540 +    then have "f x \<le> SUPR (Collect P) f"
   3.541 +      by (intro complete_lattice_class.SUP_upper) simp
   3.542 +    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
   3.543 +    have "f x \<in> S"
   3.544 +      by (simp add: inj_image_mem_iff) }
   3.545 +  with P show "eventually (\<lambda>x. f x \<in> S) net"
   3.546 +    by (auto elim: eventually_elim1)
   3.547 +next
   3.548 +  fix y l
   3.549 +  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   3.550 +  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   3.551 +  show "y \<le> l"
   3.552 +  proof (rule dense_ge)
   3.553 +    fix B assume "l < B"
   3.554 +    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   3.555 +      by (intro S[rule_format]) auto
   3.556 +    then have "y \<le> SUPR {x. f x < B} f"
   3.557 +      using P by auto
   3.558 +    moreover have "SUPR {x. f x < B} f \<le> B"
   3.559 +      by (intro SUP_least) auto
   3.560 +    ultimately show "y \<le> B"
   3.561 +      by simp
   3.562 +  qed
   3.563 +qed
   3.564 +
   3.565 +lemma liminf_bounded_open:
   3.566 +  fixes x :: "nat \<Rightarrow> ereal"
   3.567 +  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
   3.568 +  (is "_ \<longleftrightarrow> ?P x0")
   3.569 +proof
   3.570 +  assume "?P x0"
   3.571 +  then show "x0 \<le> liminf x"
   3.572 +    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
   3.573 +    by (intro complete_lattice_class.Sup_upper) auto
   3.574 +next
   3.575 +  assume "x0 \<le> liminf x"
   3.576 +  { fix S :: "ereal set"
   3.577 +    assume om: "open S & mono_set S & x0:S"
   3.578 +    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
   3.579 +    moreover
   3.580 +    { assume "~(S=UNIV)"
   3.581 +      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
   3.582 +      then have "B<x0" using om by auto
   3.583 +      then have "EX N. ALL n>=N. x n : S"
   3.584 +        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
   3.585 +    }
   3.586 +    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
   3.587 +  }
   3.588 +  then show "?P x0" by auto
   3.589 +qed
   3.590 +
   3.591  end
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 05 15:27:08 2013 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 05 15:43:08 2013 +0100
     4.3 @@ -2190,7 +2190,7 @@
     4.4      using diff positive_integral_positive[of M]
     4.5      by (subst integral_eq_positive_integral[of _ M]) (auto simp: ereal_real integrable_def)
     4.6    then show ?lim_diff
     4.7 -    using ereal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
     4.8 +    using Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
     4.9      by simp
    4.10  
    4.11    show ?lim