add Extended_Reals from AFP/Lower_Semicontinuous
authorhoelzl
Mon Mar 14 14:37:39 2011 +0100 (2011-03-14)
changeset 4197315927c040731
parent 41972 8885ba629692
child 41974 6e691abef08f
add Extended_Reals from AFP/Lower_Semicontinuous
src/HOL/IsaMakefile
src/HOL/Library/Extended_Reals.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 14 14:37:37 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 14 14:37:39 2011 +0100
     1.3 @@ -437,10 +437,10 @@
     1.4    Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
     1.5    Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
     1.6    Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
     1.7 -  Library/Executable_Set.thy Library/Float.thy				\
     1.8 -  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
     1.9 -  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
    1.10 -  Library/Function_Algebras.thy						\
    1.11 +  Library/Executable_Set.thy Library/Extended_Reals.thy			\
    1.12 +  Library/Float.thy Library/Formal_Power_Series.thy			\
    1.13 +  Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Cset.thy	\
    1.14 +  Library/FuncSet.thy Library/Function_Algebras.thy			\
    1.15    Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
    1.16    Library/Indicator_Function.thy Library/Infinite_Set.thy		\
    1.17    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:39 2011 +0100
     2.3 @@ -0,0 +1,3191 @@
     2.4 + (* Title: Extended_Reals.thy
     2.5 +   Author: Johannes Hölzl, Robert Himmelmann, Armin Heller; TU München
     2.6 +   Author: Bogdan Grechuk; University of Edinburgh *)
     2.7 +
     2.8 +header {* Extended real number line *}
     2.9 +
    2.10 +theory Extended_Reals
    2.11 +  imports Topology_Euclidean_Space
    2.12 +begin
    2.13 +
    2.14 +subsection {* Definition and basic properties *}
    2.15 +
    2.16 +datatype extreal = extreal real | PInfty | MInfty
    2.17 +
    2.18 +notation (xsymbols)
    2.19 +  PInfty  ("\<infinity>")
    2.20 +
    2.21 +notation (HTML output)
    2.22 +  PInfty  ("\<infinity>")
    2.23 +
    2.24 +instantiation extreal :: uminus
    2.25 +begin
    2.26 +  fun uminus_extreal where
    2.27 +    "- (extreal r) = extreal (- r)"
    2.28 +  | "- \<infinity> = MInfty"
    2.29 +  | "- MInfty = \<infinity>"
    2.30 +  instance ..
    2.31 +end
    2.32 +
    2.33 +lemma MInfty_neq_PInfty[simp]:
    2.34 +  "\<infinity> \<noteq> - \<infinity>" "- \<infinity> \<noteq> \<infinity>" by simp_all
    2.35 +
    2.36 +lemma MInfty_neq_extreal[simp]:
    2.37 +  "extreal r \<noteq> - \<infinity>" "- \<infinity> \<noteq> extreal r" by simp_all
    2.38 +
    2.39 +lemma MInfinity_cases[simp]:
    2.40 +  "(case - \<infinity> of extreal r \<Rightarrow> f r | \<infinity> \<Rightarrow> y | MInfinity \<Rightarrow> z) = z"
    2.41 +  by simp
    2.42 +
    2.43 +lemma extreal_uminus_uminus[simp]:
    2.44 +  fixes a :: extreal shows "- (- a) = a"
    2.45 +  by (cases a) simp_all
    2.46 +
    2.47 +lemma MInfty_eq[simp]:
    2.48 +  "MInfty = - \<infinity>" by simp
    2.49 +
    2.50 +declare uminus_extreal.simps(2)[simp del]
    2.51 +
    2.52 +lemma extreal_cases[case_names real PInf MInf, cases type: extreal]:
    2.53 +  assumes "\<And>r. x = extreal r \<Longrightarrow> P"
    2.54 +  assumes "x = \<infinity> \<Longrightarrow> P"
    2.55 +  assumes "x = -\<infinity> \<Longrightarrow> P"
    2.56 +  shows P
    2.57 +  using assms by (cases x) auto
    2.58 +
    2.59 +lemma extreal2_cases[case_names
    2.60 +  real_real real_PInf real_MInf
    2.61 +  PInf_real PInf_PInf PInf_MInf
    2.62 +  MInf_real MInf_PInf MInf_MInf]:
    2.63 +  assumes "\<And>r p. y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.64 +  assumes "\<And>p. y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
    2.65 +  assumes "\<And>p. y = extreal p \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
    2.66 +  assumes "\<And>r. y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.67 +  assumes "y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
    2.68 +  assumes "y = \<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
    2.69 +  assumes "\<And>r. y = -\<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.70 +  assumes "y = -\<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
    2.71 +  assumes "y = -\<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
    2.72 +  shows P
    2.73 +  apply (cases x)
    2.74 +  apply (cases y) using assms apply simp_all
    2.75 +  apply (cases y) using assms apply simp_all
    2.76 +  apply (cases y) using assms apply simp_all
    2.77 +  done
    2.78 +
    2.79 +lemma extreal3_cases[case_names
    2.80 +  real_real_real real_real_PInf real_real_MInf
    2.81 +  real_PInf_real real_PInf_PInf real_PInf_MInf
    2.82 +  real_MInf_real real_MInf_PInf real_MInf_MInf
    2.83 +  PInf_real_real PInf_real_PInf PInf_real_MInf
    2.84 +  PInf_PInf_real PInf_PInf_PInf PInf_PInf_MInf
    2.85 +  PInf_MInf_real PInf_MInf_PInf PInf_MInf_MInf
    2.86 +  MInf_real_real MInf_real_PInf MInf_real_MInf
    2.87 +  MInf_PInf_real MInf_PInf_PInf MInf_PInf_MInf
    2.88 +  MInf_MInf_real MInf_MInf_PInf MInf_MInf_MInf]:
    2.89 +  assumes "\<And>r p q. z = extreal q \<Longrightarrow> y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.90 +  assumes "\<And>p q. z = extreal q \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
    2.91 +  assumes "\<And>p q. z = extreal q \<Longrightarrow> y = extreal p \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
    2.92 +  assumes "\<And>r q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.93 +  assumes "\<And>q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
    2.94 +  assumes "\<And>q. z = extreal q \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
    2.95 +  assumes "\<And>q r. z = extreal q \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.96 +  assumes "\<And>q. z = extreal q \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
    2.97 +  assumes "\<And>q. z = extreal q \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
    2.98 +  assumes "\<And>r p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"
    2.99 +  assumes "\<And>p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
   2.100 +  assumes "\<And>p. z = \<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
   2.101 +  assumes "\<And>r. z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
   2.102 +  assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
   2.103 +  assumes "z = \<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
   2.104 +  assumes "\<And>r. z = \<infinity> \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
   2.105 +  assumes "z = \<infinity> \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
   2.106 +  assumes "z = \<infinity> \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
   2.107 +  assumes "\<And>r p. z = -\<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = extreal r \<Longrightarrow> P"
   2.108 +  assumes "\<And>p. z = -\<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
   2.109 +  assumes "\<And>p. z = -\<infinity> \<Longrightarrow> y = extreal p \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
   2.110 +  assumes "\<And>r. z = -\<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
   2.111 +  assumes "z = -\<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
   2.112 +  assumes "z = -\<infinity> \<Longrightarrow> y = \<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
   2.113 +  assumes "\<And>r. z = -\<infinity> \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = extreal r \<Longrightarrow> P"
   2.114 +  assumes "z = -\<infinity> \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = \<infinity> \<Longrightarrow> P"
   2.115 +  assumes "z = -\<infinity> \<Longrightarrow> y = -\<infinity> \<Longrightarrow> x = -\<infinity> \<Longrightarrow> P"
   2.116 +  shows P
   2.117 +  apply (cases x)
   2.118 +  apply (cases rule: extreal2_cases[of y z]) using assms apply simp_all
   2.119 +  apply (cases  rule: extreal2_cases[of y z]) using assms apply simp_all
   2.120 +  apply (cases  rule: extreal2_cases[of y z]) using assms apply simp_all
   2.121 +  done
   2.122 +
   2.123 +lemma extreal_uminus_eq_iff[simp]:
   2.124 +  fixes a b :: extreal shows "-a = -b \<longleftrightarrow> a = b"
   2.125 +  by (cases rule: extreal2_cases[of a b]) simp_all
   2.126 +
   2.127 +function of_extreal :: "extreal \<Rightarrow> real" where
   2.128 +"of_extreal (extreal r) = r" |
   2.129 +"of_extreal \<infinity> = 0" |
   2.130 +"of_extreal (-\<infinity>) = 0"
   2.131 +  by (auto intro: extreal_cases)
   2.132 +termination proof qed (rule wf_empty)
   2.133 +
   2.134 +defs (overloaded)
   2.135 +  real_of_extreal_def [code_unfold]: "real \<equiv> of_extreal"
   2.136 +
   2.137 +lemma real_of_extreal[simp]:
   2.138 +    "real (- x :: extreal) = - (real x)"
   2.139 +    "real (extreal r) = r"
   2.140 +    "real \<infinity> = 0"
   2.141 +  by (cases x) (simp_all add: real_of_extreal_def)
   2.142 +
   2.143 +lemma range_extreal[simp]: "range extreal = UNIV - {\<infinity>, -\<infinity>}"
   2.144 +proof safe
   2.145 +  fix x assume "x \<notin> range extreal" "x \<noteq> \<infinity>"
   2.146 +  then show "x = -\<infinity>" by (cases x) auto
   2.147 +qed auto
   2.148 +
   2.149 +instantiation extreal :: number
   2.150 +begin
   2.151 +definition [simp]: "number_of x = extreal (number_of x)"
   2.152 +instance proof qed
   2.153 +end
   2.154 +
   2.155 +subsubsection "Addition"
   2.156 +
   2.157 +instantiation extreal :: comm_monoid_add
   2.158 +begin
   2.159 +
   2.160 +definition "0 = extreal 0"
   2.161 +
   2.162 +function plus_extreal where
   2.163 +"extreal r + extreal p = extreal (r + p)" |
   2.164 +"\<infinity> + a = \<infinity>" |
   2.165 +"a + \<infinity> = \<infinity>" |
   2.166 +"extreal r + -\<infinity> = - \<infinity>" |
   2.167 +"-\<infinity> + extreal p = -\<infinity>" |
   2.168 +"-\<infinity> + -\<infinity> = -\<infinity>"
   2.169 +proof -
   2.170 +  case (goal1 P x)
   2.171 +  moreover then obtain a b where "x = (a, b)" by (cases x) auto
   2.172 +  ultimately show P
   2.173 +   by (cases rule: extreal2_cases[of a b]) auto
   2.174 +qed auto
   2.175 +termination proof qed (rule wf_empty)
   2.176 +
   2.177 +lemma Infty_neq_0[simp]:
   2.178 +  "\<infinity> \<noteq> 0" "0 \<noteq> \<infinity>"
   2.179 +  "-\<infinity> \<noteq> 0" "0 \<noteq> -\<infinity>"
   2.180 +  by (simp_all add: zero_extreal_def)
   2.181 +
   2.182 +lemma extreal_eq_0[simp]:
   2.183 +  "extreal r = 0 \<longleftrightarrow> r = 0"
   2.184 +  "0 = extreal r \<longleftrightarrow> r = 0"
   2.185 +  unfolding zero_extreal_def by simp_all
   2.186 +
   2.187 +instance
   2.188 +proof
   2.189 +  fix a :: extreal show "0 + a = a"
   2.190 +    by (cases a) (simp_all add: zero_extreal_def)
   2.191 +  fix b :: extreal show "a + b = b + a"
   2.192 +    by (cases rule: extreal2_cases[of a b]) simp_all
   2.193 +  fix c :: extreal show "a + b + c = a + (b + c)"
   2.194 +    by (cases rule: extreal3_cases[of a b c]) simp_all
   2.195 +qed
   2.196 +end
   2.197 +
   2.198 +lemma extreal_uminus_zero[simp]:
   2.199 +  "- 0 = (0::extreal)"
   2.200 +  by (simp add: zero_extreal_def)
   2.201 +
   2.202 +lemma extreal_uminus_zero_iff[simp]:
   2.203 +  fixes a :: extreal shows "-a = 0 \<longleftrightarrow> a = 0"
   2.204 +  by (cases a) simp_all
   2.205 +
   2.206 +lemma extreal_plus_eq_PInfty[simp]:
   2.207 +  shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
   2.208 +  by (cases rule: extreal2_cases[of a b]) auto
   2.209 +
   2.210 +lemma extreal_plus_eq_MInfty[simp]:
   2.211 +  shows "a + b = -\<infinity> \<longleftrightarrow>
   2.212 +    (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
   2.213 +  by (cases rule: extreal2_cases[of a b]) auto
   2.214 +
   2.215 +lemma extreal_add_cancel_left:
   2.216 +  assumes "a \<noteq> -\<infinity>"
   2.217 +  shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
   2.218 +  using assms by (cases rule: extreal3_cases[of a b c]) auto
   2.219 +
   2.220 +lemma extreal_add_cancel_right:
   2.221 +  assumes "a \<noteq> -\<infinity>"
   2.222 +  shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
   2.223 +  using assms by (cases rule: extreal3_cases[of a b c]) auto
   2.224 +
   2.225 +lemma extreal_real:
   2.226 +  "extreal (real x) = (if x = \<infinity> \<or> x = -\<infinity> then 0 else x)"
   2.227 +  by (cases x) simp_all
   2.228 +
   2.229 +subsubsection "Linear order on @{typ extreal}"
   2.230 +
   2.231 +instantiation extreal :: linorder
   2.232 +begin
   2.233 +
   2.234 +function less_extreal where
   2.235 +"extreal x < extreal y \<longleftrightarrow> x < y" |
   2.236 +"        \<infinity> < a         \<longleftrightarrow> False" |
   2.237 +"        a < -\<infinity>        \<longleftrightarrow> False" |
   2.238 +"extreal x < \<infinity>         \<longleftrightarrow> True" |
   2.239 +"       -\<infinity> < extreal r \<longleftrightarrow> True" |
   2.240 +"       -\<infinity> < \<infinity>         \<longleftrightarrow> True"
   2.241 +proof -
   2.242 +  case (goal1 P x)
   2.243 +  moreover then obtain a b where "x = (a,b)" by (cases x) auto
   2.244 +  ultimately show P by (cases rule: extreal2_cases[of a b]) auto
   2.245 +qed simp_all
   2.246 +termination by (relation "{}") simp
   2.247 +
   2.248 +definition "x \<le> (y::extreal) \<longleftrightarrow> x < y \<or> x = y"
   2.249 +
   2.250 +lemma extreal_infty_less[simp]:
   2.251 +  "x < \<infinity> \<longleftrightarrow> (x \<noteq> \<infinity>)"
   2.252 +  "-\<infinity> < x \<longleftrightarrow> (x \<noteq> -\<infinity>)"
   2.253 +  by (cases x, simp_all) (cases x, simp_all)
   2.254 +
   2.255 +lemma extreal_infty_less_eq[simp]:
   2.256 +  "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
   2.257 +  "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
   2.258 +  by (auto simp add: less_eq_extreal_def)
   2.259 +
   2.260 +lemma extreal_less[simp]:
   2.261 +  "extreal r < 0 \<longleftrightarrow> (r < 0)"
   2.262 +  "0 < extreal r \<longleftrightarrow> (0 < r)"
   2.263 +  "0 < \<infinity>"
   2.264 +  "-\<infinity> < 0"
   2.265 +  by (simp_all add: zero_extreal_def)
   2.266 +
   2.267 +lemma extreal_less_eq[simp]:
   2.268 +  "x \<le> \<infinity>"
   2.269 +  "-\<infinity> \<le> x"
   2.270 +  "extreal r \<le> extreal p \<longleftrightarrow> r \<le> p"
   2.271 +  "extreal r \<le> 0 \<longleftrightarrow> r \<le> 0"
   2.272 +  "0 \<le> extreal r \<longleftrightarrow> 0 \<le> r"
   2.273 +  by (auto simp add: less_eq_extreal_def zero_extreal_def)
   2.274 +
   2.275 +lemma extreal_infty_less_eq2:
   2.276 +  "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = \<infinity>"
   2.277 +  "a \<le> b \<Longrightarrow> b = -\<infinity> \<Longrightarrow> a = -\<infinity>"
   2.278 +  by simp_all
   2.279 +
   2.280 +instance
   2.281 +proof
   2.282 +  fix x :: extreal show "x \<le> x"
   2.283 +    by (cases x) simp_all
   2.284 +  fix y :: extreal show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   2.285 +    by (cases rule: extreal2_cases[of x y]) auto
   2.286 +  show "x \<le> y \<or> y \<le> x "
   2.287 +    by (cases rule: extreal2_cases[of x y]) auto
   2.288 +  { assume "x \<le> y" "y \<le> x" then show "x = y"
   2.289 +    by (cases rule: extreal2_cases[of x y]) auto }
   2.290 +  { fix z assume "x \<le> y" "y \<le> z" then show "x \<le> z"
   2.291 +    by (cases rule: extreal3_cases[of x y z]) auto }
   2.292 +qed
   2.293 +end
   2.294 +
   2.295 +lemma extreal_MInfty_lessI[intro, simp]:
   2.296 +  "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
   2.297 +  by (cases a) auto
   2.298 +
   2.299 +lemma extreal_less_PInfty[intro, simp]:
   2.300 +  "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
   2.301 +  by (cases a) auto
   2.302 +
   2.303 +lemma extreal_less_extreal_Ex:
   2.304 +  fixes a b :: extreal
   2.305 +  shows "x < extreal r \<longleftrightarrow> x = -\<infinity> \<or> (\<exists>p. p < r \<and> x = extreal p)"
   2.306 +  by (cases x) auto
   2.307 +
   2.308 +lemma extreal_add_mono:
   2.309 +  fixes a b c d :: extreal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d"
   2.310 +  using assms
   2.311 +  apply (cases a)
   2.312 +  apply (cases rule: extreal3_cases[of b c d], auto)
   2.313 +  apply (cases rule: extreal3_cases[of b c d], auto)
   2.314 +  done
   2.315 +
   2.316 +lemma extreal_minus_le_minus[simp]:
   2.317 +  fixes a b :: extreal shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
   2.318 +  by (cases rule: extreal2_cases[of a b]) auto
   2.319 +
   2.320 +lemma extreal_minus_less_minus[simp]:
   2.321 +  fixes a b :: extreal shows "- a < - b \<longleftrightarrow> b < a"
   2.322 +  by (cases rule: extreal2_cases[of a b]) auto
   2.323 +
   2.324 +lemma extreal_le_real_iff:
   2.325 +  "x \<le> real y \<longleftrightarrow> ((y \<noteq> -\<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> extreal x \<le> y) \<and> (y = -\<infinity> \<or> y = \<infinity> \<longrightarrow> x \<le> 0))"
   2.326 +  by (cases y) auto
   2.327 +
   2.328 +lemma real_le_extreal_iff:
   2.329 +  "real y \<le> x \<longleftrightarrow> ((y \<noteq> -\<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> y \<le> extreal x) \<and> (y = -\<infinity> \<or> y = \<infinity> \<longrightarrow> 0 \<le> x))"
   2.330 +  by (cases y) auto
   2.331 +
   2.332 +lemma extreal_less_real_iff:
   2.333 +  "x < real y \<longleftrightarrow> ((y \<noteq> -\<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> extreal x < y) \<and> (y = -\<infinity> \<or> y = \<infinity> \<longrightarrow> x < 0))"
   2.334 +  by (cases y) auto
   2.335 +
   2.336 +lemma real_less_extreal_iff:
   2.337 +  "real y < x \<longleftrightarrow> ((y \<noteq> -\<infinity> \<and> y \<noteq> \<infinity> \<longrightarrow> y < extreal x) \<and> (y = -\<infinity> \<or> y = \<infinity> \<longrightarrow> 0 < x))"
   2.338 +  by (cases y) auto
   2.339 +
   2.340 +lemmas real_of_extreal_ord_simps =
   2.341 +  extreal_le_real_iff real_le_extreal_iff extreal_less_real_iff real_less_extreal_iff
   2.342 +
   2.343 +lemma extreal_dense:
   2.344 +  fixes x y :: extreal assumes "x < y"
   2.345 +  shows "EX z. x < z & z < y"
   2.346 +proof -
   2.347 +{ assume a: "x = (-\<infinity>)"
   2.348 +  { assume "y = \<infinity>" hence ?thesis using a by (auto intro!: exI[of _ "0"]) }
   2.349 +  moreover
   2.350 +  { assume "y ~= \<infinity>"
   2.351 +    with `x < y` obtain r where r: "y = extreal r" by (cases y) auto
   2.352 +    hence ?thesis using `x < y` a by (auto intro!: exI[of _ "extreal (r - 1)"])
   2.353 +  } ultimately have ?thesis by auto
   2.354 +}
   2.355 +moreover
   2.356 +{ assume "x ~= (-\<infinity>)"
   2.357 +  with `x < y` obtain p where p: "x = extreal p" by (cases x) auto
   2.358 +  { assume "y = \<infinity>" hence ?thesis using `x < y` p
   2.359 +       by (auto intro!: exI[of _ "extreal (p + 1)"]) }
   2.360 +  moreover
   2.361 +  { assume "y ~= \<infinity>"
   2.362 +    with `x < y` obtain r where r: "y = extreal r" by (cases y) auto
   2.363 +    with p `x < y` have "p < r" by auto
   2.364 +    with dense obtain z where "p < z" "z < r" by auto
   2.365 +    hence ?thesis using r p by (auto intro!: exI[of _ "extreal z"])
   2.366 +  } ultimately have ?thesis by auto
   2.367 +} ultimately show ?thesis by auto
   2.368 +qed
   2.369 +
   2.370 +lemma extreal_dense2:
   2.371 +  fixes x y :: extreal assumes "x < y"
   2.372 +  shows "EX z. x < extreal z & extreal z < y"
   2.373 +  by (metis extreal_dense[OF `x < y`] extreal_cases less_extreal.simps(2,3))
   2.374 +
   2.375 +subsubsection "Multiplication"
   2.376 +
   2.377 +instantiation extreal :: comm_monoid_mult
   2.378 +begin
   2.379 +
   2.380 +definition "1 = extreal 1"
   2.381 +
   2.382 +function times_extreal where
   2.383 +"extreal r * extreal p = extreal (r * p)" |
   2.384 +"extreal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
   2.385 +"\<infinity> * extreal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
   2.386 +"extreal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
   2.387 +"-\<infinity> * extreal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
   2.388 +"\<infinity> * \<infinity> = \<infinity>" |
   2.389 +"-\<infinity> * \<infinity> = -\<infinity>" |
   2.390 +"\<infinity> * -\<infinity> = -\<infinity>" |
   2.391 +"-\<infinity> * -\<infinity> = \<infinity>"
   2.392 +proof -
   2.393 +  case (goal1 P x)
   2.394 +  moreover then obtain a b where "x = (a, b)" by (cases x) auto
   2.395 +  ultimately show P by (cases rule: extreal2_cases[of a b]) auto
   2.396 +qed simp_all
   2.397 +termination by (relation "{}") simp
   2.398 +
   2.399 +instance
   2.400 +proof
   2.401 +  fix a :: extreal show "1 * a = a"
   2.402 +    by (cases a) (simp_all add: one_extreal_def)
   2.403 +  fix b :: extreal show "a * b = b * a"
   2.404 +    by (cases rule: extreal2_cases[of a b]) simp_all
   2.405 +  fix c :: extreal show "a * b * c = a * (b * c)"
   2.406 +    by (cases rule: extreal3_cases[of a b c])
   2.407 +       (simp_all add: zero_extreal_def zero_less_mult_iff)
   2.408 +qed
   2.409 +end
   2.410 +
   2.411 +lemma extreal_mult_zero[simp]:
   2.412 +  fixes a :: extreal shows "a * 0 = 0"
   2.413 +  by (cases a) (simp_all add: zero_extreal_def)
   2.414 +
   2.415 +lemma extreal_zero_mult[simp]:
   2.416 +  fixes a :: extreal shows "0 * a = 0"
   2.417 +  by (cases a) (simp_all add: zero_extreal_def)
   2.418 +
   2.419 +lemma extreal_m1_less_0[simp]:
   2.420 +  "-(1::extreal) < 0"
   2.421 +  by (simp add: zero_extreal_def one_extreal_def)
   2.422 +
   2.423 +lemma extreal_zero_m1[simp]:
   2.424 +  "1 \<noteq> (0::extreal)"
   2.425 +  by (simp add: zero_extreal_def one_extreal_def)
   2.426 +
   2.427 +lemma extreal_times_0[simp]:
   2.428 +  fixes x :: extreal shows "0 * x = 0"
   2.429 +  by (cases x) (auto simp: zero_extreal_def)
   2.430 +
   2.431 +lemma extreal_times[simp]:
   2.432 +  "1 \<noteq> \<infinity>" "\<infinity> \<noteq> 1"
   2.433 +  "1 \<noteq> -\<infinity>" "-\<infinity> \<noteq> 1"
   2.434 +  by (auto simp add: times_extreal_def one_extreal_def)
   2.435 +
   2.436 +lemma extreal_plus_1[simp]:
   2.437 +  "1 + extreal r = extreal (r + 1)" "extreal r + 1 = extreal (r + 1)"
   2.438 +  "1 + -\<infinity> = -\<infinity>" "-\<infinity> + 1 = -\<infinity>"
   2.439 +  unfolding one_extreal_def by auto
   2.440 +
   2.441 +lemma extreal_zero_times[simp]:
   2.442 +  fixes a b :: extreal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   2.443 +  by (cases rule: extreal2_cases[of a b]) auto
   2.444 +
   2.445 +lemma extreal_mult_eq_PInfty[simp]:
   2.446 +  shows "a * b = \<infinity> \<longleftrightarrow>
   2.447 +    (a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
   2.448 +  by (cases rule: extreal2_cases[of a b]) auto
   2.449 +
   2.450 +lemma extreal_mult_eq_MInfty[simp]:
   2.451 +  shows "a * b = -\<infinity> \<longleftrightarrow>
   2.452 +    (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
   2.453 +  by (cases rule: extreal2_cases[of a b]) auto
   2.454 +
   2.455 +lemma extreal_0_less_1[simp]: "0 < (1::extreal)"
   2.456 +  by (simp_all add: zero_extreal_def one_extreal_def)
   2.457 +
   2.458 +lemma extreal_zero_one[simp]: "0 \<noteq> (1::extreal)"
   2.459 +  by (simp_all add: zero_extreal_def one_extreal_def)
   2.460 +
   2.461 +lemma extreal_mult_minus_left[simp]:
   2.462 +  fixes a b :: extreal shows "-a * b = - (a * b)"
   2.463 +  by (cases rule: extreal2_cases[of a b]) auto
   2.464 +
   2.465 +lemma extreal_mult_minus_right[simp]:
   2.466 +  fixes a b :: extreal shows "a * -b = - (a * b)"
   2.467 +  by (cases rule: extreal2_cases[of a b]) auto
   2.468 +
   2.469 +lemma extreal_mult_infty[simp]:
   2.470 +  "a * \<infinity> = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   2.471 +  by (cases a) auto
   2.472 +
   2.473 +lemma extreal_infty_mult[simp]:
   2.474 +  "\<infinity> * a = (if a = 0 then 0 else if 0 < a then \<infinity> else - \<infinity>)"
   2.475 +  by (cases a) auto
   2.476 +
   2.477 +lemma extreal_mult_strict_right_mono:
   2.478 +  assumes "a < b" and "0 < c" "c < \<infinity>"
   2.479 +  shows "a * c < b * c"
   2.480 +  using assms
   2.481 +  by (cases rule: extreal3_cases[of a b c])
   2.482 +     (auto simp: zero_le_mult_iff extreal_less_PInfty)
   2.483 +
   2.484 +lemma extreal_mult_strict_left_mono:
   2.485 +  "\<lbrakk> a < b ; 0 < c ; c < \<infinity>\<rbrakk> \<Longrightarrow> c * a < c * b"
   2.486 +  using extreal_mult_strict_right_mono by (simp add: mult_commute[of c])
   2.487 +
   2.488 +lemma extreal_mult_right_mono:
   2.489 +  fixes a b c :: extreal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c"
   2.490 +  using assms
   2.491 +  apply (cases "c = 0") apply simp
   2.492 +  by (cases rule: extreal3_cases[of a b c])
   2.493 +     (auto simp: zero_le_mult_iff extreal_less_PInfty)
   2.494 +
   2.495 +lemma extreal_mult_left_mono:
   2.496 +  fixes a b c :: extreal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
   2.497 +  using extreal_mult_right_mono by (simp add: mult_commute[of c])
   2.498 +
   2.499 +subsubsection {* Subtraction *}
   2.500 +
   2.501 +lemma extreal_minus_minus_image[simp]:
   2.502 +  fixes S :: "extreal set"
   2.503 +  shows "uminus ` uminus ` S = S"
   2.504 +  by (auto simp: image_iff)
   2.505 +
   2.506 +lemma extreal_uminus_lessThan[simp]:
   2.507 +  fixes a :: extreal shows "uminus ` {..<a} = {-a<..}"
   2.508 +proof (safe intro!: image_eqI)
   2.509 +  fix x assume "-a < x"
   2.510 +  then have "- x < - (- a)" by (simp del: extreal_uminus_uminus)
   2.511 +  then show "- x < a" by simp
   2.512 +qed auto
   2.513 +
   2.514 +lemma extreal_uminus_greaterThan[simp]:
   2.515 +  "uminus ` {(a::extreal)<..} = {..<-a}"
   2.516 +  by (metis extreal_uminus_lessThan extreal_uminus_uminus
   2.517 +            extreal_minus_minus_image)
   2.518 +
   2.519 +instantiation extreal :: minus
   2.520 +begin
   2.521 +definition "x - y = x + -(y::extreal)"
   2.522 +instance ..
   2.523 +end
   2.524 +
   2.525 +lemma extreal_minus[simp]:
   2.526 +  "extreal r - extreal p = extreal (r - p)"
   2.527 +  "-\<infinity> - extreal r = -\<infinity>"
   2.528 +  "extreal r - \<infinity> = -\<infinity>"
   2.529 +  "\<infinity> - x = \<infinity>"
   2.530 +  "-\<infinity> - \<infinity> = -\<infinity>"
   2.531 +  "x - -y = x + y"
   2.532 +  "x - 0 = x"
   2.533 +  "0 - x = -x"
   2.534 +  by (simp_all add: minus_extreal_def)
   2.535 +
   2.536 +lemma extreal_x_minus_x[simp]:
   2.537 +  "x - x = (if x = -\<infinity> \<or> x = \<infinity> then \<infinity> else 0)"
   2.538 +  by (cases x) simp_all
   2.539 +
   2.540 +lemma extreal_eq_minus_iff:
   2.541 +  fixes x y z :: extreal
   2.542 +  shows "x = z - y \<longleftrightarrow>
   2.543 +    (y \<noteq> \<infinity> \<longrightarrow> y \<noteq> -\<infinity> \<longrightarrow> x + y = z) \<and>
   2.544 +    (y = -\<infinity> \<longrightarrow> x = \<infinity>) \<and>
   2.545 +    (y = \<infinity> \<longrightarrow> z = \<infinity> \<longrightarrow> x = \<infinity>) \<and>
   2.546 +    (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>)"
   2.547 +  by (cases rule: extreal3_cases[of x y z]) auto
   2.548 +
   2.549 +lemma extreal_eq_minus:
   2.550 +  fixes x y z :: extreal
   2.551 +  shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> -\<infinity> \<Longrightarrow> x = z - y \<longleftrightarrow> x + y = z"
   2.552 +  by (simp add: extreal_eq_minus_iff)
   2.553 +
   2.554 +lemma extreal_less_minus_iff:
   2.555 +  fixes x y z :: extreal
   2.556 +  shows "x < z - y \<longleftrightarrow>
   2.557 +    (y = \<infinity> \<longrightarrow> z = \<infinity> \<and> x \<noteq> \<infinity>) \<and>
   2.558 +    (y = -\<infinity> \<longrightarrow> x \<noteq> \<infinity>) \<and>
   2.559 +    (y \<noteq> \<infinity> \<longrightarrow> y \<noteq> -\<infinity> \<longrightarrow> x + y < z)"
   2.560 +  by (cases rule: extreal3_cases[of x y z]) auto
   2.561 +
   2.562 +lemma extreal_less_minus:
   2.563 +  fixes x y z :: extreal
   2.564 +  shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> -\<infinity> \<Longrightarrow> x < z - y \<longleftrightarrow> x + y < z"
   2.565 +  by (simp add: extreal_less_minus_iff)
   2.566 +
   2.567 +lemma extreal_le_minus_iff:
   2.568 +  fixes x y z :: extreal
   2.569 +  shows "x \<le> z - y \<longleftrightarrow>
   2.570 +    (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and>
   2.571 +    (y \<noteq> \<infinity> \<longrightarrow> y \<noteq> -\<infinity> \<longrightarrow> x + y \<le> z)"
   2.572 +  by (cases rule: extreal3_cases[of x y z]) auto
   2.573 +
   2.574 +lemma extreal_le_minus:
   2.575 +  fixes x y z :: extreal
   2.576 +  shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> -\<infinity> \<Longrightarrow> x \<le> z - y \<longleftrightarrow> x + y \<le> z"
   2.577 +  by (simp add: extreal_le_minus_iff)
   2.578 +
   2.579 +lemma extreal_minus_less_iff:
   2.580 +  fixes x y z :: extreal
   2.581 +  shows "x - y < z \<longleftrightarrow>
   2.582 +    y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and>
   2.583 +    (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"
   2.584 +  by (cases rule: extreal3_cases[of x y z]) auto
   2.585 +
   2.586 +lemma extreal_minus_less:
   2.587 +  fixes x y z :: extreal
   2.588 +  shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> -\<infinity> \<Longrightarrow> x - y < z \<longleftrightarrow> x < z + y"
   2.589 +  by (simp add: extreal_minus_less_iff)
   2.590 +
   2.591 +lemma extreal_minus_le_iff:
   2.592 +  fixes x y z :: extreal
   2.593 +  shows "x - y \<le> z \<longleftrightarrow>
   2.594 +    (y = -\<infinity> \<longrightarrow> z = \<infinity>) \<and>
   2.595 +    (y = \<infinity> \<longrightarrow> x = \<infinity> \<longrightarrow> z = \<infinity>) \<and>
   2.596 +    (y \<noteq> \<infinity> \<longrightarrow> y \<noteq> -\<infinity> \<longrightarrow> x \<le> z + y)"
   2.597 +  by (cases rule: extreal3_cases[of x y z]) auto
   2.598 +
   2.599 +lemma extreal_minus_le:
   2.600 +  fixes x y z :: extreal
   2.601 +  shows "y \<noteq> \<infinity> \<Longrightarrow> y \<noteq> -\<infinity> \<Longrightarrow> x - y \<le> z \<longleftrightarrow> x \<le> z + y"
   2.602 +  by (simp add: extreal_minus_le_iff)
   2.603 +
   2.604 +lemma extreal_minus_eq_minus_iff:
   2.605 +  fixes a b c :: extreal
   2.606 +  shows "a - b = a - c \<longleftrightarrow>
   2.607 +    b = c \<or> a = \<infinity> \<or> (a = -\<infinity> \<and> b \<noteq> -\<infinity> \<and> c \<noteq> -\<infinity>)"
   2.608 +  by (cases rule: extreal3_cases[of a b c]) auto
   2.609 +
   2.610 +lemma extreal_add_le_add_iff:
   2.611 +  "c + a \<le> c + b \<longleftrightarrow>
   2.612 +    a \<le> b \<or> c = \<infinity> \<or> (c = -\<infinity> \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>)"
   2.613 +  by (cases rule: extreal3_cases[of a b c]) (simp_all add: field_simps)
   2.614 +
   2.615 +lemma extreal_mult_le_mult_iff:
   2.616 +  "c \<noteq> \<infinity> \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow>
   2.617 +    (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
   2.618 +  by (cases rule: extreal3_cases[of a b c]) (simp_all add: mult_le_cancel_left)
   2.619 +
   2.620 +lemma extreal_between:
   2.621 +  fixes x e :: extreal
   2.622 +  assumes "x \<noteq> \<infinity>" "x \<noteq> -\<infinity>" "0 < e"
   2.623 +  shows "x - e < x" "x < x + e"
   2.624 +using assms apply (cases x, cases e) apply auto
   2.625 +using assms by (cases x, cases e) auto
   2.626 +
   2.627 +lemma extreal_distrib:
   2.628 +  fixes a b c :: extreal
   2.629 +  assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "c \<noteq> \<infinity>" "c \<noteq> -\<infinity>"
   2.630 +  shows "(a + b) * c = a * c + b * c"
   2.631 +  using assms
   2.632 +  by (cases rule: extreal3_cases[of a b c]) (simp_all add: field_simps)
   2.633 +
   2.634 +subsubsection {* Division *}
   2.635 +
   2.636 +instantiation extreal :: inverse
   2.637 +begin
   2.638 +
   2.639 +function inverse_extreal where
   2.640 +"inverse (extreal r) = (if r = 0 then \<infinity> else extreal (inverse r))" |
   2.641 +"inverse \<infinity> = 0" |
   2.642 +"inverse (-\<infinity>) = 0"
   2.643 +  by (auto intro: extreal_cases)
   2.644 +termination by (relation "{}") simp
   2.645 +
   2.646 +definition "x / y = x * inverse (y :: extreal)"
   2.647 +
   2.648 +instance proof qed
   2.649 +end
   2.650 +
   2.651 +lemma extreal_inverse[simp]:
   2.652 +  "inverse 0 = \<infinity>"
   2.653 +  "inverse (1::extreal) = 1"
   2.654 +  by (simp_all add: one_extreal_def zero_extreal_def)
   2.655 +
   2.656 +lemma extreal_divide[simp]:
   2.657 +  "extreal r / extreal p = (if p = 0 then extreal r * \<infinity> else extreal (r / p))"
   2.658 +  unfolding divide_extreal_def by (auto simp: divide_real_def)
   2.659 +
   2.660 +lemma extreal_divide_same[simp]:
   2.661 +  "x / x = (if x = \<infinity> \<or> x = -\<infinity> \<or> x = 0 then 0 else 1)"
   2.662 +  by (cases x)
   2.663 +     (simp_all add: divide_real_def divide_extreal_def one_extreal_def)
   2.664 +
   2.665 +lemma extreal_inv_inv[simp]:
   2.666 +  "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
   2.667 +  by (cases x) auto
   2.668 +
   2.669 +lemma extreal_inverse_minus[simp]:
   2.670 +  "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
   2.671 +  by (cases x) simp_all
   2.672 +
   2.673 +lemma extreal_uminus_divide[simp]:
   2.674 +  fixes x y :: extreal shows "- x / y = - (x / y)"
   2.675 +  unfolding divide_extreal_def by simp
   2.676 +
   2.677 +lemma extreal_divide_Infty[simp]:
   2.678 +  "x / \<infinity> = 0" "x / -\<infinity> = 0"
   2.679 +  unfolding divide_extreal_def by simp_all
   2.680 +
   2.681 +lemma extreal_divide_one[simp]:
   2.682 +  "x / 1 = (x::extreal)"
   2.683 +  unfolding divide_extreal_def by simp
   2.684 +
   2.685 +lemma extreal_divide_extreal[simp]:
   2.686 +  "\<infinity> / extreal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
   2.687 +  unfolding divide_extreal_def by simp
   2.688 +
   2.689 +lemma extreal_mult_le_0_iff:
   2.690 +  fixes a b :: extreal
   2.691 +  shows "a * b \<le> 0 \<longleftrightarrow> (0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b)"
   2.692 +  by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_le_0_iff)
   2.693 +
   2.694 +lemma extreal_zero_le_0_iff:
   2.695 +  fixes a b :: extreal
   2.696 +  shows "0 \<le> a * b \<longleftrightarrow> (0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0)"
   2.697 +  by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_le_mult_iff)
   2.698 +
   2.699 +lemma extreal_mult_less_0_iff:
   2.700 +  fixes a b :: extreal
   2.701 +  shows "a * b < 0 \<longleftrightarrow> (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b)"
   2.702 +  by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_less_0_iff)
   2.703 +
   2.704 +lemma extreal_zero_less_0_iff:
   2.705 +  fixes a b :: extreal
   2.706 +  shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"
   2.707 +  by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_less_mult_iff)
   2.708 +
   2.709 +lemma extreal_le_divide_pos:
   2.710 +  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
   2.711 +  by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps)
   2.712 +
   2.713 +lemma extreal_divide_le_pos:
   2.714 +  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
   2.715 +  by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps)
   2.716 +
   2.717 +lemma extreal_le_divide_neg:
   2.718 +  "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
   2.719 +  by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps)
   2.720 +
   2.721 +lemma extreal_divide_le_neg:
   2.722 +  "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
   2.723 +  by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps)
   2.724 +
   2.725 +lemma extreal_inverse_antimono_strict:
   2.726 +  fixes x y :: extreal
   2.727 +  shows "0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> inverse y < inverse x"
   2.728 +  by (cases rule: extreal2_cases[of x y]) auto
   2.729 +
   2.730 +lemma extreal_inverse_antimono:
   2.731 +  fixes x y :: extreal
   2.732 +  shows "0 \<le> x \<Longrightarrow> x <= y \<Longrightarrow> inverse y <= inverse x"
   2.733 +  by (cases rule: extreal2_cases[of x y]) auto
   2.734 +
   2.735 +lemma inverse_inverse_Pinfty_iff[simp]:
   2.736 +  "inverse x = \<infinity> \<longleftrightarrow> x = 0"
   2.737 +  by (cases x) auto
   2.738 +
   2.739 +lemma extreal_inverse_eq_0:
   2.740 +  "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
   2.741 +  by (cases x) auto
   2.742 +
   2.743 +lemma extreal_mult_less_right:
   2.744 +  assumes "b * a < c * a" "0 < a" "a < \<infinity>"
   2.745 +  shows "b < c"
   2.746 +  using assms
   2.747 +  by (cases rule: extreal3_cases[of a b c])
   2.748 +     (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
   2.749 +
   2.750 +subsection "Complete lattice"
   2.751 +
   2.752 +lemma extreal_bot:
   2.753 +  fixes x :: extreal assumes "\<And>B. x \<le> extreal B" shows "x = - \<infinity>"
   2.754 +proof (cases x)
   2.755 +  case (real r) with assms[of "r - 1"] show ?thesis by auto
   2.756 +next case PInf with assms[of 0] show ?thesis by auto
   2.757 +next case MInf then show ?thesis by simp
   2.758 +qed
   2.759 +
   2.760 +lemma extreal_top:
   2.761 +  fixes x :: extreal assumes "\<And>B. x \<ge> extreal B" shows "x = \<infinity>"
   2.762 +proof (cases x)
   2.763 +  case (real r) with assms[of "r + 1"] show ?thesis by auto
   2.764 +next case MInf with assms[of 0] show ?thesis by auto
   2.765 +next case PInf then show ?thesis by simp
   2.766 +qed
   2.767 +
   2.768 +instantiation extreal :: lattice
   2.769 +begin
   2.770 +definition [simp]: "sup x y = (max x y :: extreal)"
   2.771 +definition [simp]: "inf x y = (min x y :: extreal)"
   2.772 +instance proof qed simp_all
   2.773 +end
   2.774 +
   2.775 +instantiation extreal :: complete_lattice
   2.776 +begin
   2.777 +
   2.778 +definition "bot = (-\<infinity>)"
   2.779 +definition "top = \<infinity>"
   2.780 +
   2.781 +definition "Sup S = (LEAST z. ALL x:S. x <= z :: extreal)"
   2.782 +definition "Inf S = (GREATEST z. ALL x:S. z <= x :: extreal)"
   2.783 +
   2.784 +lemma extreal_complete_Sup:
   2.785 +  fixes S :: "extreal set" assumes "S \<noteq> {}"
   2.786 +  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
   2.787 +proof cases
   2.788 +  assume "\<exists>x. \<forall>a\<in>S. a \<le> extreal x"
   2.789 +  then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> extreal y" by auto
   2.790 +  then have "\<infinity> \<notin> S" by force
   2.791 +  show ?thesis
   2.792 +  proof cases
   2.793 +    assume "S = {-\<infinity>}"
   2.794 +    then show ?thesis by (auto intro!: exI[of _ "-\<infinity>"])
   2.795 +  next
   2.796 +    assume "S \<noteq> {-\<infinity>}"
   2.797 +    with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
   2.798 +    with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
   2.799 +      by (auto simp: real_of_extreal_ord_simps)
   2.800 +    with reals_complete2[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
   2.801 +    obtain s where s:
   2.802 +       "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
   2.803 +       by auto
   2.804 +    show ?thesis
   2.805 +    proof (safe intro!: exI[of _ "extreal s"])
   2.806 +      fix z assume "z \<in> S" with `\<infinity> \<notin> S` show "z \<le> extreal s"
   2.807 +      proof (cases z)
   2.808 +        case (real r)
   2.809 +        then show ?thesis
   2.810 +          using s(1)[rule_format, of z] `z \<in> S` `z = extreal r` by auto
   2.811 +      qed auto
   2.812 +    next
   2.813 +      fix z assume *: "\<forall>y\<in>S. y \<le> z"
   2.814 +      with `S \<noteq> {-\<infinity>}` `S \<noteq> {}` show "extreal s \<le> z"
   2.815 +      proof (cases z)
   2.816 +        case (real u)
   2.817 +        with * have "s \<le> u"
   2.818 +          by (intro s(2)[of u]) (auto simp: real_of_extreal_ord_simps)
   2.819 +        then show ?thesis using real by simp
   2.820 +      qed auto
   2.821 +    qed
   2.822 +  qed
   2.823 +next
   2.824 +  assume *: "\<not> (\<exists>x. \<forall>a\<in>S. a \<le> extreal x)"
   2.825 +  show ?thesis
   2.826 +  proof (safe intro!: exI[of _ \<infinity>])
   2.827 +    fix y assume **: "\<forall>z\<in>S. z \<le> y"
   2.828 +    with * show "\<infinity> \<le> y"
   2.829 +    proof (cases y)
   2.830 +      case MInf with * ** show ?thesis by (force simp: not_le)
   2.831 +    qed auto
   2.832 +  qed simp
   2.833 +qed
   2.834 +
   2.835 +lemma extreal_complete_Inf:
   2.836 +  fixes S :: "extreal set" assumes "S ~= {}"
   2.837 +  shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) --> z <= x)"
   2.838 +proof-
   2.839 +def S1 == "uminus ` S"
   2.840 +hence "S1 ~= {}" using assms by auto
   2.841 +from this obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
   2.842 +   using extreal_complete_Sup[of S1] by auto
   2.843 +{ fix z assume "ALL y:S. z <= y"
   2.844 +  hence "ALL y:S1. y <= -z" unfolding S1_def by auto
   2.845 +  hence "x <= -z" using x_def by auto
   2.846 +  hence "z <= -x"
   2.847 +    apply (subst extreal_uminus_uminus[symmetric])
   2.848 +    unfolding extreal_minus_le_minus . }
   2.849 +moreover have "(ALL y:S. -x <= y)"
   2.850 +   using x_def unfolding S1_def
   2.851 +   apply simp
   2.852 +   apply (subst (3) extreal_uminus_uminus[symmetric])
   2.853 +   unfolding extreal_minus_le_minus by simp
   2.854 +ultimately show ?thesis by auto
   2.855 +qed
   2.856 +
   2.857 +lemma extreal_complete_uminus_eq:
   2.858 +  fixes S :: "extreal set"
   2.859 +  shows "(\<forall>y\<in>uminus`S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>uminus`S. y \<le> z) \<longrightarrow> x \<le> z)
   2.860 +     \<longleftrightarrow> (\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
   2.861 +  by simp (metis extreal_minus_le_minus extreal_uminus_uminus)
   2.862 +
   2.863 +lemma extreal_Sup_uminus_image_eq:
   2.864 +  fixes S :: "extreal set"
   2.865 +  shows "Sup (uminus ` S) = - Inf S"
   2.866 +proof cases
   2.867 +  assume "S = {}"
   2.868 +  moreover have "(THE x. All (op \<le> x)) = (-\<infinity>::extreal)"
   2.869 +    by (rule the_equality) (auto intro!: extreal_bot)
   2.870 +  moreover have "(SOME x. \<forall>y. y \<le> x) = (\<infinity>::extreal)"
   2.871 +    by (rule some_equality) (auto intro!: extreal_top)
   2.872 +  ultimately show ?thesis unfolding Inf_extreal_def Sup_extreal_def
   2.873 +    Least_def Greatest_def GreatestM_def by simp
   2.874 +next
   2.875 +  assume "S \<noteq> {}"
   2.876 +  with extreal_complete_Sup[of "uminus`S"]
   2.877 +  obtain x where x: "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> -x)"
   2.878 +    unfolding extreal_complete_uminus_eq by auto
   2.879 +  show "Sup (uminus ` S) = - Inf S"
   2.880 +    unfolding Inf_extreal_def Greatest_def GreatestM_def
   2.881 +  proof (intro someI2[of _ _ "\<lambda>x. Sup (uminus`S) = - x"])
   2.882 +    show "(\<forall>y\<in>S. -x \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> -x)"
   2.883 +      using x .
   2.884 +    fix x' assume "(\<forall>y\<in>S. x' \<le> y) \<and> (\<forall>y. (\<forall>z\<in>S. y \<le> z) \<longrightarrow> y \<le> x')"
   2.885 +    then have "(\<forall>y\<in>uminus`S. y \<le> - x') \<and> (\<forall>y. (\<forall>z\<in>uminus`S. z \<le> y) \<longrightarrow> - x' \<le> y)"
   2.886 +      unfolding extreal_complete_uminus_eq by simp
   2.887 +    then show "Sup (uminus ` S) = -x'"
   2.888 +      unfolding Sup_extreal_def extreal_uminus_eq_iff
   2.889 +      by (intro Least_equality) auto
   2.890 +  qed
   2.891 +qed
   2.892 +
   2.893 +instance
   2.894 +proof
   2.895 +  { fix x :: extreal and A
   2.896 +    show "bot <= x" by (cases x) (simp_all add: bot_extreal_def)
   2.897 +    show "x <= top" by (simp add: top_extreal_def) }
   2.898 +
   2.899 +  { fix x :: extreal and A assume "x : A"
   2.900 +    with extreal_complete_Sup[of A]
   2.901 +    obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
   2.902 +    hence "x <= s" using `x : A` by auto
   2.903 +    also have "... = Sup A" using s unfolding Sup_extreal_def
   2.904 +      by (auto intro!: Least_equality[symmetric])
   2.905 +    finally show "x <= Sup A" . }
   2.906 +  note le_Sup = this
   2.907 +
   2.908 +  { fix x :: extreal and A assume *: "!!z. (z : A ==> z <= x)"
   2.909 +    show "Sup A <= x"
   2.910 +    proof (cases "A = {}")
   2.911 +      case True
   2.912 +      hence "Sup A = -\<infinity>" unfolding Sup_extreal_def
   2.913 +        by (auto intro!: Least_equality)
   2.914 +      thus "Sup A <= x" by simp
   2.915 +    next
   2.916 +      case False
   2.917 +      with extreal_complete_Sup[of A]
   2.918 +      obtain s where s: "\<forall>y\<in>A. y <= s" "\<forall>z. (\<forall>y\<in>A. y <= z) \<longrightarrow> s <= z" by auto
   2.919 +      hence "Sup A = s"
   2.920 +        unfolding Sup_extreal_def by (auto intro!: Least_equality)
   2.921 +      also have "s <= x" using * s by auto
   2.922 +      finally show "Sup A <= x" .
   2.923 +    qed }
   2.924 +  note Sup_le = this
   2.925 +
   2.926 +  { fix x :: extreal and A assume "x \<in> A"
   2.927 +    with le_Sup[of "-x" "uminus`A"] show "Inf A \<le> x"
   2.928 +      unfolding extreal_Sup_uminus_image_eq by simp }
   2.929 +
   2.930 +  { fix x :: extreal and A assume *: "!!z. (z : A ==> x <= z)"
   2.931 +    with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
   2.932 +      unfolding extreal_Sup_uminus_image_eq by force }
   2.933 +qed
   2.934 +end
   2.935 +
   2.936 +lemma extreal_SUPR_uminus:
   2.937 +  fixes f :: "'a => extreal"
   2.938 +  shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
   2.939 +  unfolding SUPR_def INFI_def
   2.940 +  using extreal_Sup_uminus_image_eq[of "f`R"]
   2.941 +  by (simp add: image_image)
   2.942 +
   2.943 +lemma extreal_INFI_uminus:
   2.944 +  fixes f :: "'a => extreal"
   2.945 +  shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
   2.946 +  using extreal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
   2.947 +
   2.948 +lemma extreal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: extreal set)"
   2.949 +  by (auto intro!: inj_onI)
   2.950 +
   2.951 +lemma extreal_image_uminus_shift:
   2.952 +  fixes X Y :: "extreal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
   2.953 +proof
   2.954 +  assume "uminus ` X = Y"
   2.955 +  then have "uminus ` uminus ` X = uminus ` Y"
   2.956 +    by (simp add: inj_image_eq_iff)
   2.957 +  then show "X = uminus ` Y" by (simp add: image_image)
   2.958 +qed (simp add: image_image)
   2.959 +
   2.960 +lemma Inf_extreal_iff:
   2.961 +  fixes z :: extreal
   2.962 +  shows "(!!x. x:X ==> z <= x) ==> (EX x:X. x<y) <-> Inf X < y"
   2.963 +  by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear
   2.964 +            order_less_le_trans)
   2.965 +
   2.966 +lemma Sup_eq_MInfty:
   2.967 +  fixes S :: "extreal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
   2.968 +proof
   2.969 +  assume a: "Sup S = -\<infinity>"
   2.970 +  with complete_lattice_class.Sup_upper[of _ S]
   2.971 +  show "S={} \<or> S={-\<infinity>}" by auto
   2.972 +next
   2.973 +  assume "S={} \<or> S={-\<infinity>}" then show "Sup S = -\<infinity>"
   2.974 +    unfolding Sup_extreal_def by (auto intro!: Least_equality)
   2.975 +qed
   2.976 +
   2.977 +lemma Inf_eq_PInfty:
   2.978 +  fixes S :: "extreal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
   2.979 +  using Sup_eq_MInfty[of "uminus`S"]
   2.980 +  unfolding extreal_Sup_uminus_image_eq extreal_image_uminus_shift by simp
   2.981 +
   2.982 +lemma Inf_eq_MInfty: "-\<infinity> : S ==> Inf S = -\<infinity>"
   2.983 +  unfolding Inf_extreal_def
   2.984 +  by (auto intro!: Greatest_equality)
   2.985 +
   2.986 +lemma Sup_eq_PInfty: "\<infinity> : S ==> Sup S = \<infinity>"
   2.987 +  unfolding Sup_extreal_def
   2.988 +  by (auto intro!: Least_equality)
   2.989 +
   2.990 +lemma extreal_SUPI:
   2.991 +  fixes x :: extreal
   2.992 +  assumes "!!i. i : A ==> f i <= x"
   2.993 +  assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
   2.994 +  shows "(SUP i:A. f i) = x"
   2.995 +  unfolding SUPR_def Sup_extreal_def
   2.996 +  using assms by (auto intro!: Least_equality)
   2.997 +
   2.998 +lemma extreal_INFI:
   2.999 +  fixes x :: extreal
  2.1000 +  assumes "!!i. i : A ==> f i >= x"
  2.1001 +  assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
  2.1002 +  shows "(INF i:A. f i) = x"
  2.1003 +  unfolding INFI_def Inf_extreal_def
  2.1004 +  using assms by (auto intro!: Greatest_equality)
  2.1005 +
  2.1006 +lemma Sup_extreal_close:
  2.1007 +  fixes e :: extreal
  2.1008 +  assumes "0 < e" and S: "Sup S \<noteq> \<infinity>" "Sup S \<noteq> -\<infinity>" "S \<noteq> {}"
  2.1009 +  shows "\<exists>x\<in>S. Sup S - e < x"
  2.1010 +proof (rule less_Sup_iff[THEN iffD1])
  2.1011 +  show "Sup S - e < Sup S " using assms
  2.1012 +    by (cases "Sup S", cases e) auto
  2.1013 +qed
  2.1014 +
  2.1015 +lemma Inf_extreal_close:
  2.1016 +  fixes e :: extreal assumes "Inf X \<noteq> \<infinity>" "Inf X \<noteq> -\<infinity>" "0 < e"
  2.1017 +  shows "\<exists>x\<in>X. x < Inf X + e"
  2.1018 +proof (rule Inf_less_iff[THEN iffD1])
  2.1019 +  show "Inf X < Inf X + e" using assms
  2.1020 +    by (cases "Inf X", cases e) auto
  2.1021 +qed
  2.1022 +
  2.1023 +lemma (in complete_lattice) top_le:
  2.1024 +  "top \<le> x \<Longrightarrow> x = top"
  2.1025 +  by (rule antisym) auto
  2.1026 +
  2.1027 +lemma Sup_eq_top_iff:
  2.1028 +  fixes A :: "'a::{complete_lattice, linorder} set"
  2.1029 +  shows "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
  2.1030 +proof
  2.1031 +  assume *: "Sup A = top"
  2.1032 +  show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding *[symmetric]
  2.1033 +  proof (intro allI impI)
  2.1034 +    fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
  2.1035 +      unfolding less_Sup_iff by auto
  2.1036 +  qed
  2.1037 +next
  2.1038 +  assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
  2.1039 +  show "Sup A = top"
  2.1040 +  proof (rule ccontr)
  2.1041 +    assume "Sup A \<noteq> top"
  2.1042 +    with top_greatest[of "Sup A"]
  2.1043 +    have "Sup A < top" unfolding le_less by auto
  2.1044 +    then have "Sup A < Sup A"
  2.1045 +      using * unfolding less_Sup_iff by auto
  2.1046 +    then show False by auto
  2.1047 +  qed
  2.1048 +qed
  2.1049 +
  2.1050 +lemma SUP_eq_top_iff:
  2.1051 +  fixes f :: "'a \<Rightarrow> 'b::{complete_lattice, linorder}"
  2.1052 +  shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
  2.1053 +  unfolding SUPR_def Sup_eq_top_iff by auto
  2.1054 +
  2.1055 +lemma SUP_nat_Infty: "(SUP i::nat. extreal (real i)) = \<infinity>"
  2.1056 +proof -
  2.1057 +  { fix x assume "x \<noteq> \<infinity>"
  2.1058 +    then have "\<exists>k::nat. x < extreal (real k)"
  2.1059 +    proof (cases x)
  2.1060 +      case MInf then show ?thesis by (intro exI[of _ 0]) auto
  2.1061 +    next
  2.1062 +      case (real r)
  2.1063 +      moreover obtain k :: nat where "r < real k"
  2.1064 +        using ex_less_of_nat by (auto simp: real_eq_of_nat)
  2.1065 +      ultimately show ?thesis by auto
  2.1066 +    qed simp }
  2.1067 +  then show ?thesis
  2.1068 +    using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. extreal (real n)"]
  2.1069 +    by (auto simp: top_extreal_def)
  2.1070 +qed
  2.1071 +
  2.1072 +lemma infeal_le_Sup:
  2.1073 +  fixes x :: extreal
  2.1074 +  shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))"
  2.1075 +(is "?lhs <-> ?rhs")
  2.1076 +proof-
  2.1077 +{ assume "?rhs"
  2.1078 +  { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
  2.1079 +    from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using extreal_dense by auto
  2.1080 +    from this obtain i where "i : A & y <= f i" using `?rhs` by auto
  2.1081 +    hence "y <= (SUP i:A. f i)" using le_SUPI[of i A f] by auto
  2.1082 +    hence False using y_def by auto
  2.1083 +  } hence "?lhs" by auto
  2.1084 +}
  2.1085 +moreover
  2.1086 +{ assume "?lhs" hence "?rhs"
  2.1087 +  by (metis Collect_def Collect_mem_eq SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
  2.1088 +      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
  2.1089 +} ultimately show ?thesis by auto
  2.1090 +qed
  2.1091 +
  2.1092 +lemma infeal_Inf_le:
  2.1093 +  fixes x :: extreal
  2.1094 +  shows "((INF i:A. f i) <= x) <-> (ALL y. x < y --> (EX i. i : A & f i <= y))"
  2.1095 +(is "?lhs <-> ?rhs")
  2.1096 +proof-
  2.1097 +{ assume "?rhs"
  2.1098 +  { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
  2.1099 +    from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using extreal_dense by auto
  2.1100 +    from this obtain i where "i : A & f i <= y" using `?rhs` by auto
  2.1101 +    hence "(INF i:A. f i) <= y" using INF_leI[of i A f] by auto
  2.1102 +    hence False using y_def by auto
  2.1103 +  } hence "?lhs" by auto
  2.1104 +}
  2.1105 +moreover
  2.1106 +{ assume "?lhs" hence "?rhs"
  2.1107 +  by (metis Collect_def Collect_mem_eq le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
  2.1108 +      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
  2.1109 +} ultimately show ?thesis by auto
  2.1110 +qed
  2.1111 +
  2.1112 +lemma Inf_less:
  2.1113 +  fixes x :: extreal
  2.1114 +  assumes "(INF i:A. f i) < x"
  2.1115 +  shows "EX i. i : A & f i <= x"
  2.1116 +proof(rule ccontr)
  2.1117 +  assume "~ (EX i. i : A & f i <= x)"
  2.1118 +  hence "ALL i:A. f i > x" by auto
  2.1119 +  hence "(INF i:A. f i) >= x" apply (subst le_INFI) by auto
  2.1120 +  thus False using assms by auto
  2.1121 +qed
  2.1122 +
  2.1123 +lemma same_INF:
  2.1124 +  assumes "ALL e:A. f e = g e"
  2.1125 +  shows "(INF e:A. f e) = (INF e:A. g e)"
  2.1126 +proof-
  2.1127 +have "f ` A = g ` A" unfolding image_def using assms by auto
  2.1128 +thus ?thesis unfolding INFI_def by auto
  2.1129 +qed
  2.1130 +
  2.1131 +lemma same_SUP:
  2.1132 +  assumes "ALL e:A. f e = g e"
  2.1133 +  shows "(SUP e:A. f e) = (SUP e:A. g e)"
  2.1134 +proof-
  2.1135 +have "f ` A = g ` A" unfolding image_def using assms by auto
  2.1136 +thus ?thesis unfolding SUPR_def by auto
  2.1137 +qed
  2.1138 +
  2.1139 +subsection "Limits on @{typ extreal}"
  2.1140 +
  2.1141 +subsubsection "Topological space"
  2.1142 +
  2.1143 +instantiation extreal :: topological_space
  2.1144 +begin
  2.1145 +
  2.1146 +definition "open A \<longleftrightarrow>
  2.1147 +  (\<exists>T. open T \<and> extreal ` T = A - {\<infinity>, -\<infinity>})
  2.1148 +       \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {extreal x <..} \<subseteq> A))
  2.1149 +       \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<extreal x} \<subseteq> A))"
  2.1150 +
  2.1151 +lemma open_PInfty: "open A ==> \<infinity> : A ==> (EX x. {extreal x<..} <= A)"
  2.1152 +  unfolding open_extreal_def by auto
  2.1153 +
  2.1154 +lemma open_MInfty: "open A ==> (-\<infinity>) : A ==> (EX x. {..<extreal x} <= A)"
  2.1155 +  unfolding open_extreal_def by auto
  2.1156 +
  2.1157 +lemma open_PInfty2: assumes "open A" "\<infinity> : A" obtains x where "{extreal x<..} <= A"
  2.1158 +  using open_PInfty[OF assms] by auto
  2.1159 +
  2.1160 +lemma open_MInfty2: assumes "open A" "(-\<infinity>) : A" obtains x where "{..<extreal x} <= A"
  2.1161 +  using open_MInfty[OF assms] by auto
  2.1162 +
  2.1163 +lemma extreal_openE: assumes "open A" obtains A' x y where
  2.1164 +  "open A'" "extreal ` A' = A - {\<infinity>, (-\<infinity>)}"
  2.1165 +  "\<infinity> : A ==> {extreal x<..} <= A"
  2.1166 +  "(-\<infinity>) : A ==> {..<extreal y} <= A"
  2.1167 +  using assms open_extreal_def by auto
  2.1168 +
  2.1169 +instance
  2.1170 +proof
  2.1171 +  let ?U = "UNIV::extreal set"
  2.1172 +  show "open ?U" unfolding open_extreal_def
  2.1173 +    by (auto intro!: exI[of _ "UNIV"] exI[of _ 0])
  2.1174 +next
  2.1175 +  fix S T::"extreal set" assume "open S" and "open T"
  2.1176 +  from `open S`[THEN extreal_openE] guess S' xS yS . note S' = this
  2.1177 +  from `open T`[THEN extreal_openE] guess T' xT yT . note T' = this
  2.1178 +
  2.1179 +  have "extreal ` (S' Int T') = (extreal ` S') Int (extreal ` T')" by auto
  2.1180 +  also have "... = S Int T - {\<infinity>, (-\<infinity>)}" using S' T' by auto
  2.1181 +  finally have "extreal ` (S' Int T') =  S Int T - {\<infinity>, (-\<infinity>)}" by auto
  2.1182 +  moreover have "open (S' Int T')" using S' T' by auto
  2.1183 +  moreover
  2.1184 +  { assume a: "\<infinity> : S Int T"
  2.1185 +    hence "EX x. {extreal x<..} <= S Int T"
  2.1186 +    apply(rule_tac x="max xS xT" in exI)
  2.1187 +    proof-
  2.1188 +    { fix x assume *: "extreal (max xS xT) < x"
  2.1189 +      hence "x : S Int T" apply (cases x, auto simp: max_def split: split_if_asm)
  2.1190 +      using a S' T' by auto
  2.1191 +    } thus "{extreal (max xS xT)<..} <= S Int T" by auto
  2.1192 +    qed }
  2.1193 +  moreover
  2.1194 +  { assume a: "(-\<infinity>) : S Int T"
  2.1195 +    hence "EX x. {..<extreal x} <= S Int T"
  2.1196 +    apply(rule_tac x="min yS yT" in exI)
  2.1197 +    proof-
  2.1198 +    { fix x assume *: "extreal (min yS yT) > x"
  2.1199 +      hence "x<extreal yS & x<extreal yT" by (cases x) auto
  2.1200 +      hence "x : S Int T" using a S' T' by auto
  2.1201 +    } thus "{..<extreal (min yS yT)} <= S Int T" by auto
  2.1202 +    qed }
  2.1203 +  ultimately show "open (S Int T)" unfolding open_extreal_def by auto
  2.1204 +next
  2.1205 +  fix K assume openK: "ALL S : K. open (S:: extreal set)"
  2.1206 +  hence "ALL S:K. EX T. open T & extreal ` T = S - {\<infinity>, (-\<infinity>)}" by (auto simp: open_extreal_def)
  2.1207 +  from bchoice[OF this] guess T .. note T = this[rule_format]
  2.1208 +
  2.1209 +  show "open (Union K)" unfolding open_extreal_def
  2.1210 +  proof (safe intro!: exI[of _ "Union (T ` K)"])
  2.1211 +    fix x S assume "x : T S" "S : K"
  2.1212 +    with T[OF `S : K`] show "extreal x : Union K" by auto
  2.1213 +  next
  2.1214 +    fix x S assume x: "x ~: extreal ` (Union (T ` K))" "S : K" "x : S" "x ~= \<infinity>"
  2.1215 +    hence "x ~: extreal ` (T S)"
  2.1216 +      by (auto simp: image_UN UN_simps[symmetric] simp del: UN_simps)
  2.1217 +    thus "x=(-\<infinity>)" using T[OF `S : K`] `x : S` `x ~= \<infinity>` by auto
  2.1218 +  next
  2.1219 +    fix S assume "\<infinity> : S" "S : K"
  2.1220 +    from openK[rule_format, OF `S : K`, THEN extreal_openE] guess S' x .
  2.1221 +    from this(3) `\<infinity> : S`
  2.1222 +    show "EX x. {extreal x<..} <= Union K"
  2.1223 +      by (auto intro!: exI[of _ x] bexI[OF _ `S : K`])
  2.1224 +  next
  2.1225 +    fix S assume "(-\<infinity>) : S" "S : K"
  2.1226 +    from openK[rule_format, OF `S : K`, THEN extreal_openE] guess S' x y .
  2.1227 +    from this(4) `(-\<infinity>) : S`
  2.1228 +    show "EX y. {..<extreal y} <= Union K"
  2.1229 +      by (auto intro!: exI[of _ y] bexI[OF _ `S : K`])
  2.1230 +  next
  2.1231 +    from T[THEN conjunct1] show "open (Union (T`K))" by auto
  2.1232 +  qed auto
  2.1233 +qed
  2.1234 +end
  2.1235 +
  2.1236 +lemma open_extreal_lessThan[simp]:
  2.1237 +  "open {..< a :: extreal}"
  2.1238 +proof (cases a)
  2.1239 +  case (real x)
  2.1240 +  then show ?thesis unfolding open_extreal_def
  2.1241 +  proof (safe intro!: exI[of _ "{..< x}"])
  2.1242 +    fix y assume "y < extreal x"
  2.1243 +    moreover assume "y ~: (extreal ` {..<x})"
  2.1244 +    ultimately have "y ~= extreal (real y)" using real by (cases y) auto
  2.1245 +    thus "y = (-\<infinity>)" apply (cases y) using `y < extreal x` by auto
  2.1246 +  qed auto
  2.1247 +qed (auto simp: open_extreal_def)
  2.1248 +
  2.1249 +lemma open_extreal_greaterThan[simp]:
  2.1250 +  "open {a :: extreal <..}"
  2.1251 +proof (cases a)
  2.1252 +  case (real x)
  2.1253 +  then show ?thesis unfolding open_extreal_def
  2.1254 +  proof (safe intro!: exI[of _ "{x<..}"])
  2.1255 +    fix y assume "extreal x < y"
  2.1256 +    moreover assume "y ~: (extreal ` {x<..})"
  2.1257 +    moreover assume "y ~= \<infinity>"
  2.1258 +    ultimately have "y ~= extreal (real y)" using real by (cases y) auto
  2.1259 +    hence False apply (cases y) using `extreal x < y` `y ~= \<infinity>` by auto
  2.1260 +    thus "y = (-\<infinity>)" by auto
  2.1261 +  qed auto
  2.1262 +qed (auto simp: open_extreal_def)
  2.1263 +
  2.1264 +lemma extreal_open_greaterThanLessThan[simp]: "open {a::extreal <..< b}"
  2.1265 +  unfolding greaterThanLessThan_def by auto
  2.1266 +
  2.1267 +lemma closed_extreal_atLeast[simp, intro]: "closed {a :: extreal ..}"
  2.1268 +proof -
  2.1269 +  have "- {a ..} = {..< a}" by auto
  2.1270 +  then show "closed {a ..}"
  2.1271 +    unfolding closed_def using open_extreal_lessThan by auto
  2.1272 +qed
  2.1273 +
  2.1274 +lemma closed_extreal_atMost[simp, intro]: "closed {.. b :: extreal}"
  2.1275 +proof -
  2.1276 +  have "- {.. b} = {b <..}" by auto
  2.1277 +  then show "closed {.. b}"
  2.1278 +    unfolding closed_def using open_extreal_greaterThan by auto
  2.1279 +qed
  2.1280 +
  2.1281 +lemma closed_extreal_atLeastAtMost[simp, intro]:
  2.1282 +  shows "closed {a :: extreal .. b}"
  2.1283 +  unfolding atLeastAtMost_def by auto
  2.1284 +
  2.1285 +lemma closed_extreal_singleton:
  2.1286 +  "closed {a :: extreal}"
  2.1287 +by (metis atLeastAtMost_singleton closed_extreal_atLeastAtMost)
  2.1288 +
  2.1289 +lemma extreal_open_cont_interval:
  2.1290 +  assumes "open S" "x \<in> S" and "x \<noteq> \<infinity>" "x \<noteq> - \<infinity>"
  2.1291 +  obtains e where "e>0" "{x-e <..< x+e} \<subseteq> S"
  2.1292 +proof-
  2.1293 +  obtain m where m_def: "x = extreal m" using assms by (cases x) auto
  2.1294 +  obtain A where "open A" and A_def: "extreal ` A = S - {\<infinity>,(-\<infinity>)}"
  2.1295 +    using assms by (auto elim!: extreal_openE)
  2.1296 +  hence "m : A" using m_def assms by auto
  2.1297 +  from this obtain e where e_def: "e>0 & ball m e <= A"
  2.1298 +    using open_contains_ball[of A] `open A` by auto
  2.1299 +  moreover have "ball m e = {m-e <..< m+e}" unfolding ball_def dist_norm by auto
  2.1300 +  ultimately have *: "{m-e <..< m+e} <= A" using e_def by auto
  2.1301 +  { fix y assume y_def: "y:{x-extreal e <..< x+extreal e}"
  2.1302 +    from this obtain z where z_def: "y = extreal z" by (cases y) auto
  2.1303 +    hence "z:A" using y_def m_def * by auto
  2.1304 +    hence "y:S" using z_def A_def by auto
  2.1305 +  } hence "{x-extreal e <..< x+extreal e} <= S" by auto
  2.1306 +  thus thesis apply- apply(rule that[of "extreal e"]) using e_def by auto
  2.1307 +qed
  2.1308 +
  2.1309 +lemma extreal_open_cont_interval2:
  2.1310 +  assumes "open S" "x \<in> S" and x: "x \<noteq> \<infinity>" "x \<noteq> -\<infinity>"
  2.1311 +  obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
  2.1312 +proof-
  2.1313 +  guess e using extreal_open_cont_interval[OF assms] .
  2.1314 +  with that[of "x-e" "x+e"] extreal_between[OF x, of e]
  2.1315 +  show thesis by auto
  2.1316 +qed
  2.1317 +
  2.1318 +lemma extreal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::extreal)" by auto
  2.1319 +
  2.1320 +lemma extreal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::extreal)"
  2.1321 +  by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_less_minus)
  2.1322 +
  2.1323 +lemma extreal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::extreal)"
  2.1324 +  by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_le_minus)
  2.1325 +
  2.1326 +lemmas extreal_uminus_reorder =
  2.1327 +  extreal_uminus_eq_reorder extreal_uminus_less_reorder extreal_uminus_le_reorder
  2.1328 +
  2.1329 +lemma extreal_open_uminus:
  2.1330 +  fixes S :: "extreal set"
  2.1331 +  assumes "open S"
  2.1332 +  shows "open (uminus ` S)"
  2.1333 +proof-
  2.1334 +  obtain T x y where T_def: "open T & extreal ` T = S - {\<infinity>, (-\<infinity>)} &
  2.1335 +     (\<infinity> : S --> {extreal x<..} <= S) & ((-\<infinity>) : S --> {..<extreal y} <= S)"
  2.1336 +     using assms extreal_openE[of S] by metis
  2.1337 +  have "extreal ` uminus ` T = uminus ` extreal ` T" apply auto
  2.1338 +     by (metis imageI extreal_uminus_uminus uminus_extreal.simps)
  2.1339 +  also have "...=uminus ` (S - {\<infinity>, (-\<infinity>)})" using T_def by auto
  2.1340 +  finally have "extreal ` uminus ` T = uminus ` S - {\<infinity>, (-\<infinity>)}" by (auto simp: extreal_uminus_reorder)
  2.1341 +  moreover have "open (uminus ` T)" using T_def open_negations[of T] by auto
  2.1342 +  ultimately have "EX T. open T & extreal ` T = uminus ` S - {\<infinity>, (-\<infinity>)}" by auto
  2.1343 +  moreover
  2.1344 +  { assume "\<infinity>: uminus ` S"
  2.1345 +    hence "(-\<infinity>) : S" by (metis image_iff extreal_uminus_uminus)
  2.1346 +    hence "uminus ` {..<extreal y} <= uminus ` S" using T_def by (intro image_mono) auto
  2.1347 +    hence "EX x. {extreal x<..} <= uminus ` S" using extreal_uminus_lessThan by auto
  2.1348 +  } moreover
  2.1349 +  { assume "(-\<infinity>): uminus ` S"
  2.1350 +    hence "\<infinity> : S" by (metis image_iff extreal_uminus_uminus)
  2.1351 +    hence "uminus ` {extreal x<..} <= uminus ` S" using T_def by (intro image_mono) auto
  2.1352 +    hence "EX y. {..<extreal y} <= uminus ` S" using extreal_uminus_greaterThan by auto
  2.1353 +  }
  2.1354 +  ultimately show ?thesis unfolding open_extreal_def by auto
  2.1355 +qed
  2.1356 +
  2.1357 +lemma extreal_uminus_complement:
  2.1358 +  fixes S :: "extreal set"
  2.1359 +  shows "(uminus ` (- S)) = (- uminus ` S)"
  2.1360 +proof-
  2.1361 +{ fix x
  2.1362 +  have "x:uminus ` (- S) <-> -x:(- S)" by (metis image_iff extreal_uminus_uminus)
  2.1363 +  also have "... <-> x:(- uminus ` S)"
  2.1364 +     by (metis ComplI Compl_iff image_eqI extreal_uminus_uminus extreal_minus_minus_image)
  2.1365 +  finally have "x:uminus ` (- S) <-> x:(- uminus ` S)" by auto
  2.1366 +} thus ?thesis by auto
  2.1367 +qed
  2.1368 +
  2.1369 +lemma extreal_closed_uminus:
  2.1370 +  fixes S :: "extreal set"
  2.1371 +  assumes "closed S"
  2.1372 +  shows "closed (uminus ` S)"
  2.1373 +using assms unfolding closed_def
  2.1374 +using extreal_open_uminus[of "- S"] extreal_uminus_complement by auto
  2.1375 +
  2.1376 +
  2.1377 +lemma not_open_extreal_singleton:
  2.1378 +  "~(open {a :: extreal})"
  2.1379 +proof(rule ccontr)
  2.1380 +  assume "~ ~ open {a}" hence a: "open {a}" by auto
  2.1381 +  { assume "a=(-\<infinity>)"
  2.1382 +    then obtain y where "{..<extreal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
  2.1383 +    hence "extreal(y - 1):{a}" apply (subst subsetD[of "{..<extreal y}"]) by auto
  2.1384 +    hence False using `a=(-\<infinity>)` by auto
  2.1385 +  } moreover
  2.1386 +  { assume "a=\<infinity>"
  2.1387 +    then obtain y where "{extreal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
  2.1388 +    hence "extreal(y+1):{a}" apply (subst subsetD[of "{extreal y<..}"]) by auto
  2.1389 +    hence False using `a=\<infinity>` by auto
  2.1390 +  } moreover
  2.1391 +  { assume fin: "a~=(-\<infinity>)" "a~=\<infinity>"
  2.1392 +    from extreal_open_cont_interval[OF a singletonI this(2,1)] guess e . note e = this
  2.1393 +    then obtain b where b_def: "a<b & b<a+e"
  2.1394 +      using fin extreal_between extreal_dense[of a "a+e"] by auto
  2.1395 +    then have "b: {a-e <..< a+e}" using fin extreal_between[of a e] e by auto
  2.1396 +    then have False using b_def e by auto
  2.1397 +  } ultimately show False by auto
  2.1398 +qed
  2.1399 +
  2.1400 +lemma extreal_closed_contains_Inf:
  2.1401 +  fixes S :: "extreal set"
  2.1402 +  assumes "closed S" "S ~= {}"
  2.1403 +  shows "Inf S : S"
  2.1404 +proof(rule ccontr)
  2.1405 +assume "~(Inf S:S)" hence a: "open (-S)" "Inf S:(- S)" using assms by auto
  2.1406 +{ assume minf: "Inf S=(-\<infinity>)" hence "(-\<infinity>) : - S" using a by auto
  2.1407 +  then obtain y where "{..<extreal y} <= (-S)" using a open_MInfty2[of "- S"] by auto
  2.1408 +  hence "extreal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff
  2.1409 +     complete_lattice_class.Inf_greatest double_complement set_rev_mp)
  2.1410 +  hence False using minf by auto
  2.1411 +} moreover
  2.1412 +{ assume pinf: "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
  2.1413 +  hence False by (metis `Inf S ~: S` insert_code mem_def pinf)
  2.1414 +} moreover
  2.1415 +{ assume fin: "Inf S ~= \<infinity>" "Inf S ~= (-\<infinity>)"
  2.1416 +  from extreal_open_cont_interval[OF a this] guess e . note e = this
  2.1417 +  { fix x assume "x:S" hence "x>=Inf S" by (rule complete_lattice_class.Inf_lower)
  2.1418 +    hence *: "x>Inf S-e" using e by (metis fin extreal_between(1) order_less_le_trans)
  2.1419 +    { assume "x<Inf S+e" hence "x:{Inf S-e <..< Inf S+e}" using * by auto
  2.1420 +      hence False using e `x:S` by auto
  2.1421 +    } hence "x>=Inf S+e" by (metis linorder_le_less_linear)
  2.1422 +  } hence "Inf S + e <= Inf S" by (metis le_Inf_iff)
  2.1423 +  hence False by (metis calculation(1) calculation(2) e extreal_between(2) leD)
  2.1424 +} ultimately show False by auto
  2.1425 +qed
  2.1426 +
  2.1427 +lemma extreal_closed_contains_Sup:
  2.1428 +  fixes S :: "extreal set"
  2.1429 +  assumes "closed S" "S ~= {}"
  2.1430 +  shows "Sup S : S"
  2.1431 +proof-
  2.1432 +  have "closed (uminus ` S)" by (metis assms(1) extreal_closed_uminus)
  2.1433 +  hence "Inf (uminus ` S) : uminus ` S" using assms extreal_closed_contains_Inf[of "uminus ` S"] by auto
  2.1434 +  hence "- Sup S : uminus ` S" using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)
  2.1435 +  thus ?thesis by (metis imageI extreal_uminus_uminus extreal_minus_minus_image)
  2.1436 +qed
  2.1437 +
  2.1438 +lemma extreal_open_closed_aux:
  2.1439 +  fixes S :: "extreal set"
  2.1440 +  assumes "open S" "closed S"
  2.1441 +  assumes S: "(-\<infinity>) ~: S"
  2.1442 +  shows "S = {}"
  2.1443 +proof(rule ccontr)
  2.1444 +  assume "S ~= {}"
  2.1445 +  hence *: "(Inf S):S" by (metis assms(2) extreal_closed_contains_Inf)
  2.1446 +  { assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto }
  2.1447 +  moreover
  2.1448 +  { assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
  2.1449 +    hence False by (metis assms(1) not_open_extreal_singleton) }
  2.1450 +  moreover
  2.1451 +  { assume fin: "~(Inf S=\<infinity>)" "~(Inf S=(-\<infinity>))"
  2.1452 +    from extreal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
  2.1453 +    then obtain b where b_def: "Inf S-e<b & b<Inf S"
  2.1454 +      using fin extreal_between[of "Inf S" e] extreal_dense[of "Inf S-e"] by auto
  2.1455 +    hence "b: {Inf S-e <..< Inf S+e}" using e fin extreal_between[of "Inf S" e] by auto
  2.1456 +    hence "b:S" using e by auto
  2.1457 +    hence False using b_def by (metis complete_lattice_class.Inf_lower leD)
  2.1458 +  } ultimately show False by auto
  2.1459 +qed
  2.1460 +
  2.1461 +
  2.1462 +lemma extreal_open_closed:
  2.1463 +  fixes S :: "extreal set"
  2.1464 +  shows "(open S & closed S) <-> (S = {} | S = UNIV)"
  2.1465 +proof-
  2.1466 +{ assume lhs: "open S & closed S"
  2.1467 +  { assume "(-\<infinity>) ~: S" hence "S={}" using lhs extreal_open_closed_aux by auto }
  2.1468 +  moreover
  2.1469 +  { assume "(-\<infinity>) : S" hence "(- S)={}" using lhs extreal_open_closed_aux[of "-S"] by auto }
  2.1470 +  ultimately have "S = {} | S = UNIV" by auto
  2.1471 +} thus ?thesis by auto
  2.1472 +qed
  2.1473 +
  2.1474 +
  2.1475 +lemma extreal_le_epsilon:
  2.1476 +  fixes x y :: extreal
  2.1477 +  assumes "ALL e. 0 < e --> x <= y + e"
  2.1478 +  shows "x <= y"
  2.1479 +proof-
  2.1480 +{ assume a: "EX r. y = extreal r"
  2.1481 +  from this obtain r where r_def: "y = extreal r" by auto
  2.1482 +  { assume "x=(-\<infinity>)" hence ?thesis by auto }
  2.1483 +  moreover
  2.1484 +  { assume "~(x=(-\<infinity>))"
  2.1485 +    from this obtain p where p_def: "x = extreal p"
  2.1486 +    using a assms[rule_format, of 1] by (cases x) auto
  2.1487 +    { fix e have "0 < e --> p <= r + e"
  2.1488 +      using assms[rule_format, of "extreal e"] p_def r_def by auto }
  2.1489 +    hence "p <= r" apply (subst field_le_epsilon) by auto
  2.1490 +    hence ?thesis using r_def p_def by auto
  2.1491 +  } ultimately have ?thesis by blast
  2.1492 +}
  2.1493 +moreover
  2.1494 +{ assume "y=(-\<infinity>) | y=\<infinity>" hence ?thesis
  2.1495 +    using assms[rule_format, of 1] by (cases x) auto
  2.1496 +} ultimately show ?thesis by (cases y) auto
  2.1497 +qed
  2.1498 +
  2.1499 +
  2.1500 +lemma extreal_le_epsilon2:
  2.1501 +  fixes x y :: extreal
  2.1502 +  assumes "ALL e. 0 < e --> x <= y + extreal e"
  2.1503 +  shows "x <= y"
  2.1504 +proof-
  2.1505 +{ fix e :: extreal assume "e>0"
  2.1506 +  { assume "e=\<infinity>" hence "x<=y+e" by auto }
  2.1507 +  moreover
  2.1508 +  { assume "e~=\<infinity>"
  2.1509 +    from this obtain r where "e = extreal r" using `e>0` apply (cases e) by auto
  2.1510 +    hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto
  2.1511 +  } ultimately have "x<=y+e" by blast
  2.1512 +} from this show ?thesis using extreal_le_epsilon by auto
  2.1513 +qed
  2.1514 +
  2.1515 +lemma extreal_le_real:
  2.1516 +  fixes x y :: extreal
  2.1517 +  assumes "ALL z. x <= extreal z --> y <= extreal z"
  2.1518 +  shows "y <= x"
  2.1519 +by (metis assms extreal.exhaust extreal_bot extreal_less_eq(1)
  2.1520 +          extreal_less_eq(2) order_refl uminus_extreal.simps(2))
  2.1521 +
  2.1522 +lemma extreal_le_extreal:
  2.1523 +  fixes x y :: extreal
  2.1524 +  assumes "\<And>B. B < x \<Longrightarrow> B <= y"
  2.1525 +  shows "x <= y"
  2.1526 +by (metis assms extreal_dense leD linorder_le_less_linear)
  2.1527 +
  2.1528 +
  2.1529 +lemma extreal_ge_extreal:
  2.1530 +  fixes x y :: extreal
  2.1531 +  assumes "ALL B. B>x --> B >= y"
  2.1532 +  shows "x >= y"
  2.1533 +by (metis assms extreal_dense leD linorder_le_less_linear)
  2.1534 +
  2.1535 +
  2.1536 +instance extreal :: t2_space
  2.1537 +proof
  2.1538 +  fix x y :: extreal assume "x ~= y"
  2.1539 +  let "?P x (y::extreal)" = "EX U V. open U & open V & x : U & y : V & U Int V = {}"
  2.1540 +
  2.1541 +  { fix x y :: extreal assume "x < y"
  2.1542 +    from extreal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
  2.1543 +    have "?P x y"
  2.1544 +      apply (rule exI[of _ "{..<z}"])
  2.1545 +      apply (rule exI[of _ "{z<..}"])
  2.1546 +      using z by auto }
  2.1547 +  note * = this
  2.1548 +
  2.1549 +  from `x ~= y`
  2.1550 +  show "EX U V. open U & open V & x : U & y : V & U Int V = {}"
  2.1551 +  proof (cases rule: linorder_cases)
  2.1552 +    assume "x = y" with `x ~= y` show ?thesis by simp
  2.1553 +  next assume "x < y" from *[OF this] show ?thesis by auto
  2.1554 +  next assume "y < x" from *[OF this] show ?thesis by auto
  2.1555 +  qed
  2.1556 +qed
  2.1557 +
  2.1558 +lemma open_extreal: assumes "open S" shows "open (extreal ` S)"
  2.1559 +  unfolding open_extreal_def apply(rule,rule,rule,rule assms) by auto
  2.1560 +
  2.1561 +lemma open_real_of_extreal:
  2.1562 +  fixes S :: "extreal set" assumes "open S"
  2.1563 +  shows "open (real ` (S - {\<infinity>, -\<infinity>}))"
  2.1564 +proof -
  2.1565 +  from `open S` obtain T where T: "open T" "S - {\<infinity>, -\<infinity>} = extreal ` T"
  2.1566 +    unfolding open_extreal_def by auto
  2.1567 +  show ?thesis using T by (simp add: image_image)
  2.1568 +qed
  2.1569 +
  2.1570 +subsubsection {* Convergent sequences *}
  2.1571 +
  2.1572 +lemma inj_extreal[simp, intro]: "inj_on extreal A" by (auto intro: inj_onI)
  2.1573 +
  2.1574 +lemma lim_extreal[simp]:
  2.1575 +  "((\<lambda>n. extreal (f n)) ---> extreal x) net \<longleftrightarrow> (f ---> x) net" (is "?l = ?r")
  2.1576 +proof (intro iffI topological_tendstoI)
  2.1577 +  fix S assume "?l" "open S" "x \<in> S"
  2.1578 +  then show "eventually (\<lambda>x. f x \<in> S) net"
  2.1579 +    using `?l`[THEN topological_tendstoD, OF open_extreal, OF `open S`]
  2.1580 +    by (simp add: inj_image_mem_iff)
  2.1581 +next
  2.1582 +  fix S assume "?r" "open S" "extreal x \<in> S"
  2.1583 +  have *: "\<And>x. x \<in> real ` (S - {\<infinity>, - \<infinity>}) \<longleftrightarrow> extreal x \<in> S"
  2.1584 +    apply (safe intro!: rev_image_eqI)
  2.1585 +    by (case_tac xa) auto
  2.1586 +  show "eventually (\<lambda>x. extreal (f x) \<in> S) net"
  2.1587 +    using `?r`[THEN topological_tendstoD, OF open_real_of_extreal, OF `open S`]
  2.1588 +    using `extreal x \<in> S` by (simp add: *)
  2.1589 +qed
  2.1590 +
  2.1591 +lemma lim_real_of_extreal[simp]:
  2.1592 +  assumes lim: "(f ---> extreal x) net"
  2.1593 +  shows "((\<lambda>x. real (f x)) ---> x) net"
  2.1594 +proof (intro topological_tendstoI)
  2.1595 +  fix S assume "open S" "x \<in> S"
  2.1596 +  then have S: "open S" "extreal x \<in> extreal ` S"
  2.1597 +    by (simp_all add: inj_image_mem_iff)
  2.1598 +  have "\<forall>x. f x \<in> extreal ` S \<longrightarrow> real (f x) \<in> S" by auto
  2.1599 +  from this lim[THEN topological_tendstoD, OF open_extreal, OF S]
  2.1600 +  show "eventually (\<lambda>x. real (f x) \<in> S) net"
  2.1601 +    by (rule eventually_mono)
  2.1602 +qed
  2.1603 +
  2.1604 +lemma Lim_PInfty: "f ----> \<infinity> <-> (ALL B. EX N. ALL n>=N. f n >= extreal B)" (is "?l = ?r")
  2.1605 +proof assume ?r show ?l apply(rule topological_tendstoI)
  2.1606 +    unfolding eventually_sequentially
  2.1607 +  proof- fix S assume "open S" "\<infinity> : S"
  2.1608 +    from open_PInfty[OF this] guess B .. note B=this
  2.1609 +    from `?r`[rule_format,of "B+1"] guess N .. note N=this
  2.1610 +    show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
  2.1611 +    proof safe case goal1
  2.1612 +      have "extreal B < extreal (B + 1)" by auto
  2.1613 +      also have "... <= f n" using goal1 N by auto
  2.1614 +      finally show ?case using B by fastsimp
  2.1615 +    qed
  2.1616 +  qed
  2.1617 +next assume ?l show ?r
  2.1618 +  proof fix B::real have "open {extreal B<..}" "\<infinity> : {extreal B<..}" by auto
  2.1619 +    from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
  2.1620 +    guess N .. note N=this
  2.1621 +    show "EX N. ALL n>=N. extreal B <= f n" apply(rule_tac x=N in exI) using N by auto
  2.1622 +  qed
  2.1623 +qed
  2.1624 +
  2.1625 +
  2.1626 +lemma Lim_MInfty: "f ----> (-\<infinity>) <-> (ALL B. EX N. ALL n>=N. f n <= extreal B)" (is "?l = ?r")
  2.1627 +proof assume ?r show ?l apply(rule topological_tendstoI)
  2.1628 +    unfolding eventually_sequentially
  2.1629 +  proof- fix S assume "open S" "(-\<infinity>) : S"
  2.1630 +    from open_MInfty[OF this] guess B .. note B=this
  2.1631 +    from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this
  2.1632 +    show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
  2.1633 +    proof safe case goal1
  2.1634 +      have "extreal (B - 1) >= f n" using goal1 N by auto
  2.1635 +      also have "... < extreal B" by auto
  2.1636 +      finally show ?case using B by fastsimp
  2.1637 +    qed
  2.1638 +  qed
  2.1639 +next assume ?l show ?r
  2.1640 +  proof fix B::real have "open {..<extreal B}" "(-\<infinity>) : {..<extreal B}" by auto
  2.1641 +    from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
  2.1642 +    guess N .. note N=this
  2.1643 +    show "EX N. ALL n>=N. extreal B >= f n" apply(rule_tac x=N in exI) using N by auto
  2.1644 +  qed
  2.1645 +qed
  2.1646 +
  2.1647 +
  2.1648 +lemma Lim_bounded_PInfty: assumes lim:"f ----> l" and "!!n. f n <= extreal B" shows "l ~= \<infinity>"
  2.1649 +proof(rule ccontr,unfold not_not) let ?B = "B + 1" assume as:"l=\<infinity>"
  2.1650 +  from lim[unfolded this Lim_PInfty,rule_format,of "?B"]
  2.1651 +  guess N .. note N=this[rule_format,OF le_refl]
  2.1652 +  hence "extreal ?B <= extreal B" using assms(2)[of N] by(rule order_trans)
  2.1653 +  hence "extreal ?B < extreal ?B" apply (rule le_less_trans) by auto
  2.1654 +  thus False by auto
  2.1655 +qed
  2.1656 +
  2.1657 +
  2.1658 +lemma Lim_bounded_MInfty: assumes lim:"f ----> l" and "!!n. f n >= extreal B" shows "l ~= (-\<infinity>)"
  2.1659 +proof(rule ccontr,unfold not_not) let ?B = "B - 1" assume as:"l=(-\<infinity>)"
  2.1660 +  from lim[unfolded this Lim_MInfty,rule_format,of "?B"]
  2.1661 +  guess N .. note N=this[rule_format,OF le_refl]
  2.1662 +  hence "extreal B <= extreal ?B" using assms(2)[of N] order_trans[of "extreal B" "f N" "extreal(B - 1)"] by blast
  2.1663 +  thus False by auto
  2.1664 +qed
  2.1665 +
  2.1666 +
  2.1667 +lemma tendsto_explicit:
  2.1668 +  "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
  2.1669 +  unfolding tendsto_def eventually_sequentially by auto
  2.1670 +
  2.1671 +
  2.1672 +lemma tendsto_obtains_N:
  2.1673 +  assumes "f ----> f0"
  2.1674 +  assumes "open S" "f0 : S"
  2.1675 +  obtains N where "ALL n>=N. f n : S"
  2.1676 +  using tendsto_explicit[of f f0] assms by auto
  2.1677 +
  2.1678 +
  2.1679 +lemma tail_same_limit:
  2.1680 +  fixes X Y N
  2.1681 +  assumes "X ----> L" "ALL n>=N. X n = Y n"
  2.1682 +  shows "Y ----> L"
  2.1683 +proof-
  2.1684 +{ fix S assume "open S" and "L:S"
  2.1685 +  from this obtain N1 where "ALL n>=N1. X n : S"
  2.1686 +     using assms unfolding tendsto_def eventually_sequentially by auto
  2.1687 +  hence "ALL n>=max N N1. Y n : S" using assms by auto
  2.1688 +  hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
  2.1689 +}
  2.1690 +thus ?thesis using tendsto_explicit by auto
  2.1691 +qed
  2.1692 +
  2.1693 +
  2.1694 +lemma Lim_bounded_PInfty2:
  2.1695 +assumes lim:"f ----> l" and "ALL n>=N. f n <= extreal B"
  2.1696 +shows "l ~= \<infinity>"
  2.1697 +proof-
  2.1698 +  def g == "(%n. if n>=N then f n else extreal B)"
  2.1699 +  hence "g ----> l" using tail_same_limit[of f l N g] lim by auto
  2.1700 +  moreover have "!!n. g n <= extreal B" using g_def assms by auto
  2.1701 +  ultimately show ?thesis using  Lim_bounded_PInfty by auto
  2.1702 +qed
  2.1703 +
  2.1704 +lemma Lim_bounded_extreal:
  2.1705 +  assumes lim:"f ----> (l :: extreal)"
  2.1706 +  and "ALL n>=M. f n <= C"
  2.1707 +  shows "l<=C"
  2.1708 +proof-
  2.1709 +{ assume "l=(-\<infinity>)" hence ?thesis by auto }
  2.1710 +moreover
  2.1711 +{ assume "~(l=(-\<infinity>))"
  2.1712 +  { assume "C=\<infinity>" hence ?thesis by auto }
  2.1713 +  moreover
  2.1714 +  { assume "C=(-\<infinity>)" hence "ALL n>=M. f n = (-\<infinity>)" using assms by auto
  2.1715 +    hence "l=(-\<infinity>)" using assms
  2.1716 +       Lim_unique[OF trivial_limit_sequentially] tail_same_limit[of "\<lambda>n. -\<infinity>" "-\<infinity>" M f, OF tendsto_const] by auto
  2.1717 +    hence ?thesis by auto }
  2.1718 +  moreover
  2.1719 +  { assume "EX B. C = extreal B"
  2.1720 +    from this obtain B where B_def: "C=extreal B" by auto
  2.1721 +    hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
  2.1722 +    from this obtain m where m_def: "extreal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
  2.1723 +    from this obtain N where N_def: "ALL n>=N. f n : {extreal(m - 1) <..< extreal(m+1)}"
  2.1724 +       apply (subst tendsto_obtains_N[of f l "{extreal(m - 1) <..< extreal(m+1)}"]) using assms by auto
  2.1725 +    { fix n assume "n>=N"
  2.1726 +      hence "EX r. extreal r = f n" using N_def by (cases "f n") auto
  2.1727 +    } from this obtain g where g_def: "ALL n>=N. extreal (g n) = f n" by metis
  2.1728 +    hence "(%n. extreal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
  2.1729 +    hence *: "(%n. g n) ----> m" using m_def by auto
  2.1730 +    { fix n assume "n>=max N M"
  2.1731 +      hence "extreal (g n) <= extreal B" using assms g_def B_def by auto
  2.1732 +      hence "g n <= B" by auto
  2.1733 +    } hence "EX N. ALL n>=N. g n <= B" by blast
  2.1734 +    hence "m<=B" using * LIMSEQ_le_const2[of g m B] by auto
  2.1735 +    hence ?thesis using m_def B_def by auto
  2.1736 +  } ultimately have ?thesis by (cases C) auto
  2.1737 +} ultimately show ?thesis by blast
  2.1738 +qed
  2.1739 +
  2.1740 +lemma real_of_extreal_0[simp]: "real (0::extreal) = 0"
  2.1741 +  unfolding real_of_extreal_def zero_extreal_def by simp
  2.1742 +
  2.1743 +lemma real_of_extreal_mult[simp]:
  2.1744 +  fixes a b :: extreal shows "real (a * b) = real a * real b"
  2.1745 +  by (cases rule: extreal2_cases[of a b]) auto
  2.1746 +
  2.1747 +lemma real_of_extreal_eq_0:
  2.1748 +  "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
  2.1749 +  by (cases x) auto
  2.1750 +
  2.1751 +lemma tendsto_extreal_realD:
  2.1752 +  fixes f :: "'a \<Rightarrow> extreal"
  2.1753 +  assumes "x \<noteq> 0" and tendsto: "((\<lambda>x. extreal (real (f x))) ---> x) net"
  2.1754 +  shows "(f ---> x) net"
  2.1755 +proof (intro topological_tendstoI)
  2.1756 +  fix S assume S: "open S" "x \<in> S"
  2.1757 +  with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}" by auto
  2.1758 +  from tendsto[THEN topological_tendstoD, OF this]
  2.1759 +  show "eventually (\<lambda>x. f x \<in> S) net"
  2.1760 +    by (rule eventually_rev_mp) (auto simp: extreal_real real_of_extreal_0)
  2.1761 +qed
  2.1762 +
  2.1763 +lemma tendsto_extreal_realI:
  2.1764 +  fixes f :: "'a \<Rightarrow> extreal"
  2.1765 +  assumes x: "x \<noteq> \<infinity>" "x \<noteq> -\<infinity>" and tendsto: "(f ---> x) net"
  2.1766 +  shows "((\<lambda>x. extreal (real (f x))) ---> x) net"
  2.1767 +proof (intro topological_tendstoI)
  2.1768 +  fix S assume "open S" "x \<in> S"
  2.1769 +  with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}" by auto
  2.1770 +  from tendsto[THEN topological_tendstoD, OF this]
  2.1771 +  show "eventually (\<lambda>x. extreal (real (f x)) \<in> S) net"
  2.1772 +    by (elim eventually_elim1) (auto simp: extreal_real)
  2.1773 +qed
  2.1774 +
  2.1775 +lemma extreal_mult_cancel_left:
  2.1776 +  fixes a b c :: extreal shows "a * b = a * c \<longleftrightarrow>
  2.1777 +    (((a = \<infinity> \<or> a = -\<infinity>) \<and> 0 < b * c) \<or> a = 0 \<or> b = c)"
  2.1778 +  by (cases rule: extreal3_cases[of a b c])
  2.1779 +     (simp_all add: zero_less_mult_iff)
  2.1780 +
  2.1781 +lemma extreal_inj_affinity:
  2.1782 +  assumes "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" "t \<noteq> \<infinity>" "t \<noteq> -\<infinity>"
  2.1783 +  shows "inj_on (\<lambda>x. m * x + t) A"
  2.1784 +  using assms
  2.1785 +  by (cases rule: extreal2_cases[of m t])
  2.1786 +     (auto intro!: inj_onI simp: extreal_add_cancel_right extreal_mult_cancel_left)
  2.1787 +
  2.1788 +lemma extreal_PInfty_eq_plus[simp]:
  2.1789 +  shows "\<infinity> = a + b \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
  2.1790 +  by (cases rule: extreal2_cases[of a b]) auto
  2.1791 +
  2.1792 +lemma extreal_MInfty_eq_plus[simp]:
  2.1793 +  shows "-\<infinity> = a + b \<longleftrightarrow> (a = -\<infinity> \<and> b \<noteq> \<infinity>) \<or> (b = -\<infinity> \<and> a \<noteq> \<infinity>)"
  2.1794 +  by (cases rule: extreal2_cases[of a b]) auto
  2.1795 +
  2.1796 +lemma extreal_less_divide_pos:
  2.1797 +  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y < z / x \<longleftrightarrow> x * y < z"
  2.1798 +  by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps)
  2.1799 +
  2.1800 +lemma extreal_divide_less_pos:
  2.1801 +  "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y / x < z \<longleftrightarrow> y < x * z"
  2.1802 +  by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps)
  2.1803 +
  2.1804 +lemma extreal_open_affinity_pos:
  2.1805 +  assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "t \<noteq> \<infinity>" "t \<noteq> -\<infinity>"
  2.1806 +  shows "open ((\<lambda>x. m * x + t) ` S)"
  2.1807 +proof -
  2.1808 +  obtain r where r[simp]: "m = extreal r" using m by (cases m) auto
  2.1809 +  obtain p where p[simp]: "t = extreal p" using t by (cases t) auto
  2.1810 +  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto
  2.1811 +  from `open S`[THEN extreal_openE] guess T l u . note T = this
  2.1812 +  let ?f = "(\<lambda>x. m * x + t)"
  2.1813 +  show ?thesis unfolding open_extreal_def
  2.1814 +  proof (intro conjI impI exI subsetI)
  2.1815 +    show "open ((\<lambda>x. r*x + p)`T)"
  2.1816 +      using open_affinity[OF `open T` `r \<noteq> 0`] by (auto simp: ac_simps)
  2.1817 +    have affine_infy: "?f ` {\<infinity>, - \<infinity>} = {\<infinity>, -\<infinity>}"
  2.1818 +      using `r \<noteq> 0` by auto
  2.1819 +    have "extreal ` (\<lambda>x. r * x + p) ` T = ?f ` (extreal ` T)"
  2.1820 +      by (simp add: image_image)
  2.1821 +    also have "\<dots> = ?f ` (S - {\<infinity>, -\<infinity>})"
  2.1822 +      using T(2) by simp
  2.1823 +    also have "\<dots> = ?f ` S - {\<infinity>, -\<infinity>}"
  2.1824 +      using extreal_inj_affinity[OF m' t] by (simp only: image_set_diff affine_infy)
  2.1825 +    finally show "extreal ` (\<lambda>x. r * x + p) ` T = ?f ` S - {\<infinity>, -\<infinity>}" .
  2.1826 +  next
  2.1827 +    assume "\<infinity> \<in> ?f`S" with `0 < r` have "\<infinity> \<in> S" by auto
  2.1828 +    fix x assume "x \<in> {extreal (r * l + p)<..}"
  2.1829 +    then have [simp]: "extreal (r * l + p) < x" by auto
  2.1830 +    show "x \<in> ?f`S"
  2.1831 +    proof (rule image_eqI)
  2.1832 +      show "x = m * ((x - t) / m) + t"
  2.1833 +        using m t by (cases rule: extreal3_cases[of m x t]) auto
  2.1834 +      have "extreal l < (x - t)/m"
  2.1835 +        using m t by (simp add: extreal_less_divide_pos extreal_less_minus)
  2.1836 +      then show "(x - t)/m \<in> S" using T(3)[OF `\<infinity> \<in> S`] by auto
  2.1837 +    qed
  2.1838 +  next
  2.1839 +    assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto
  2.1840 +    fix x assume "x \<in> {..<extreal (r * u + p)}"
  2.1841 +    then have [simp]: "x < extreal (r * u + p)" by auto
  2.1842 +    show "x \<in> ?f`S"
  2.1843 +    proof (rule image_eqI)
  2.1844 +      show "x = m * ((x - t) / m) + t"
  2.1845 +        using m t by (cases rule: extreal3_cases[of m x t]) auto
  2.1846 +      have "(x - t)/m < extreal u"
  2.1847 +        using m t by (simp add: extreal_divide_less_pos extreal_minus_less)
  2.1848 +      then show "(x - t)/m \<in> S" using T(4)[OF `-\<infinity> \<in> S`] by auto
  2.1849 +    qed
  2.1850 +  qed
  2.1851 +qed
  2.1852 +
  2.1853 +lemma extreal_open_affinity:
  2.1854 +  assumes "open S" and m: "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" and t: "t \<noteq> \<infinity>" "t \<noteq> -\<infinity>"
  2.1855 +  shows "open ((\<lambda>x. m * x + t) ` S)"
  2.1856 +proof cases
  2.1857 +  assume "0 < m" then show ?thesis
  2.1858 +    using extreal_open_affinity_pos[OF `open S` `m \<noteq> \<infinity>` _ t] by auto
  2.1859 +next
  2.1860 +  assume "\<not> 0 < m" then
  2.1861 +  have "0 < -m" using `m \<noteq> 0` by (cases m) auto
  2.1862 +  then have m: "-m \<noteq> \<infinity>" "0 < -m" using `m \<noteq> -\<infinity>`
  2.1863 +    by (simp_all add: extreal_uminus_eq_reorder)
  2.1864 +  from extreal_open_affinity_pos[OF extreal_open_uminus[OF `open S`] m t]
  2.1865 +  show ?thesis unfolding image_image by simp
  2.1866 +qed
  2.1867 +
  2.1868 +lemma extreal_divide_eq:
  2.1869 +  "b \<noteq> 0 \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b \<noteq> -\<infinity> \<Longrightarrow> a / b = c \<longleftrightarrow> a = b * c"
  2.1870 +  by (cases rule: extreal3_cases[of a b c])
  2.1871 +     (simp_all add: field_simps)
  2.1872 +
  2.1873 +lemma extreal_inverse_not_MInfty[simp]: "inverse a \<noteq> -\<infinity>"
  2.1874 +  by (cases a) auto
  2.1875 +
  2.1876 +lemma extreal_lim_mult:
  2.1877 +  fixes X :: "'a \<Rightarrow> extreal"
  2.1878 +  assumes lim: "(X ---> L) net" and a: "a \<noteq> \<infinity>" "a \<noteq> -\<infinity>"
  2.1879 +  shows "((\<lambda>i. a * X i) ---> a * L) net"
  2.1880 +proof cases
  2.1881 +  assume "a \<noteq> 0"
  2.1882 +  show ?thesis
  2.1883 +  proof (rule topological_tendstoI)
  2.1884 +    fix S assume "open S" "a * L \<in> S"
  2.1885 +    have "a * L / a = L"
  2.1886 +      using `a \<noteq> 0` a by (cases rule: extreal2_cases[of a L]) auto
  2.1887 +    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
  2.1888 +      using `a * L \<in> S` by (force simp: image_iff)
  2.1889 +    moreover have "open ((\<lambda>x. x / a) ` S)"
  2.1890 +      using extreal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
  2.1891 +      by (simp add: extreal_divide_eq extreal_inverse_eq_0 divide_extreal_def ac_simps)
  2.1892 +    note * = lim[THEN topological_tendstoD, OF this L]
  2.1893 +    { fix x from a `a \<noteq> 0` have "a * (x / a) = x"
  2.1894 +        by (cases rule: extreal2_cases[of a x]) auto }
  2.1895 +    note this[simp]
  2.1896 +    show "eventually (\<lambda>x. a * X x \<in> S) net"
  2.1897 +      by (rule eventually_mono[OF _ *]) auto
  2.1898 +  qed
  2.1899 +qed auto
  2.1900 +
  2.1901 +lemma extreal_mult_m1[simp]: "x * extreal (-1) = -x"
  2.1902 +  by (cases x) auto
  2.1903 +
  2.1904 +lemma extreal_lim_uminus:
  2.1905 +  fixes X :: "'a \<Rightarrow> extreal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
  2.1906 +  using extreal_lim_mult[of X L net "extreal (-1)"]
  2.1907 +        extreal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "extreal (-1)"]
  2.1908 +  by (auto simp add: algebra_simps)
  2.1909 +
  2.1910 +lemma Lim_bounded2_extreal:
  2.1911 +  assumes lim:"f ----> (l :: extreal)"
  2.1912 +  and ge: "ALL n>=N. f n >= C"
  2.1913 +  shows "l>=C"
  2.1914 +proof-
  2.1915 +def g == "(%i. -(f i))"
  2.1916 +{ fix n assume "n>=N" hence "g n <= -C" using assms extreal_minus_le_minus g_def by auto }
  2.1917 +hence "ALL n>=N. g n <= -C" by auto
  2.1918 +moreover have limg: "g ----> (-l)" using g_def extreal_lim_uminus lim by auto
  2.1919 +ultimately have "-l <= -C" using Lim_bounded_extreal[of g "-l" _ "-C"] by auto
  2.1920 +from this show ?thesis using extreal_minus_le_minus by auto
  2.1921 +qed
  2.1922 +
  2.1923 +
  2.1924 +lemma extreal_LimI_finite:
  2.1925 +  assumes "x ~= \<infinity>" "x ~= (-\<infinity>)"
  2.1926 +  assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
  2.1927 +  shows "u ----> x"
  2.1928 +proof (rule topological_tendstoI, unfold eventually_sequentially)
  2.1929 +  obtain rx where rx_def: "x=extreal rx" using assms by (cases x) auto
  2.1930 +  fix S assume "open S" "x : S"
  2.1931 +  then obtain A where "open A" and A_eq: "extreal ` A = S - {\<infinity>,(-\<infinity>)}"
  2.1932 +     by (auto elim!: extreal_openE)
  2.1933 +  then have "x : extreal ` A" using `x : S` assms by auto
  2.1934 +  then have "rx : A" using rx_def by auto
  2.1935 +  then obtain r where "0 < r" and dist: "!!y. dist y (real x) < r ==> y : A"
  2.1936 +    using `open A` unfolding open_real_def rx_def by auto
  2.1937 +  then obtain n where
  2.1938 +    upper: "!!N. n <= N ==> u N < x + extreal r" and
  2.1939 +    lower: "!!N. n <= N ==> x < u N + extreal r" using assms(3)[of "extreal r"] by auto
  2.1940 +  show "EX N. ALL n>=N. u n : S"
  2.1941 +  proof (safe intro!: exI[of _ n])
  2.1942 +    fix N assume "n <= N"
  2.1943 +    from upper[OF this] lower[OF this] assms `0 < r`
  2.1944 +    have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
  2.1945 +    from this obtain ra where ra_def: "(u N) = extreal ra" by (cases "u N") auto
  2.1946 +    hence "rx < ra + r" and "ra < rx + r"
  2.1947 +       using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
  2.1948 +    hence "dist (real (u N)) (real x) < r"
  2.1949 +      using rx_def ra_def
  2.1950 +      by (auto simp: dist_real_def abs_diff_less_iff field_simps)
  2.1951 +    from dist[OF this]
  2.1952 +    have "u N : extreal ` A" using `u N  ~: {\<infinity>,(-\<infinity>)}`
  2.1953 +      by (auto intro!: image_eqI[of _ _ "real (u N)"] simp: extreal_real)
  2.1954 +    thus "u N : S" using A_eq by simp
  2.1955 +  qed
  2.1956 +qed
  2.1957 +
  2.1958 +lemma extreal_LimI_finite_iff:
  2.1959 +  assumes "x ~= \<infinity>" "x ~= (-\<infinity>)"
  2.1960 +  shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
  2.1961 +  (is "?lhs <-> ?rhs")
  2.1962 +proof-
  2.1963 +{ assume lim: "u ----> x"
  2.1964 +  { fix r assume "(r::extreal)>0"
  2.1965 +    from this obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
  2.1966 +       apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
  2.1967 +       using lim extreal_between[of x r] assms `r>0` by auto
  2.1968 +    hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
  2.1969 +      using extreal_minus_less[of r x] by (cases r) auto
  2.1970 +  } hence "?rhs" by auto
  2.1971 +} from this show ?thesis using extreal_LimI_finite assms by blast
  2.1972 +qed
  2.1973 +
  2.1974 +
  2.1975 +subsubsection {* @{text Liminf} and @{text Limsup} *}
  2.1976 +
  2.1977 +definition
  2.1978 +  "Liminf net f = (GREATEST l. \<forall>y<l. eventually (\<lambda>x. y < f x) net)"
  2.1979 +
  2.1980 +definition
  2.1981 +  "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
  2.1982 +
  2.1983 +lemma Liminf_Sup:
  2.1984 +  fixes f :: "'a => 'b::{complete_lattice, linorder}"
  2.1985 +  shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
  2.1986 +  by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
  2.1987 +
  2.1988 +lemma Limsup_Inf:
  2.1989 +  fixes f :: "'a => 'b::{complete_lattice, linorder}"
  2.1990 +  shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
  2.1991 +  by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
  2.1992 +
  2.1993 +lemma extreal_SupI:
  2.1994 +  fixes x :: extreal
  2.1995 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  2.1996 +  assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
  2.1997 +  shows "Sup A = x"
  2.1998 +  unfolding Sup_extreal_def
  2.1999 +  using assms by (auto intro!: Least_equality)
  2.2000 +
  2.2001 +lemma extreal_InfI:
  2.2002 +  fixes x :: extreal
  2.2003 +  assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
  2.2004 +  assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
  2.2005 +  shows "Inf A = x"
  2.2006 +  unfolding Inf_extreal_def
  2.2007 +  using assms by (auto intro!: Greatest_equality)
  2.2008 +
  2.2009 +lemma Limsup_const:
  2.2010 +  fixes c :: "'a::{complete_lattice, linorder}"
  2.2011 +  assumes ntriv: "\<not> trivial_limit net"
  2.2012 +  shows "Limsup net (\<lambda>x. c) = c"
  2.2013 +  unfolding Limsup_Inf
  2.2014 +proof (safe intro!: antisym complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower)
  2.2015 +  fix x assume *: "\<forall>y>x. eventually (\<lambda>_. c < y) net"
  2.2016 +  show "c \<le> x"
  2.2017 +  proof (rule ccontr)
  2.2018 +    assume "\<not> c \<le> x" then have "x < c" by auto
  2.2019 +    then show False using ntriv * by (auto simp: trivial_limit_def)
  2.2020 +  qed
  2.2021 +qed auto
  2.2022 +
  2.2023 +lemma Liminf_const:
  2.2024 +  fixes c :: "'a::{complete_lattice, linorder}"
  2.2025 +  assumes ntriv: "\<not> trivial_limit net"
  2.2026 +  shows "Liminf net (\<lambda>x. c) = c"
  2.2027 +  unfolding Liminf_Sup
  2.2028 +proof (safe intro!: antisym complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
  2.2029 +  fix x assume *: "\<forall>y<x. eventually (\<lambda>_. y < c) net"
  2.2030 +  show "x \<le> c"
  2.2031 +  proof (rule ccontr)
  2.2032 +    assume "\<not> x \<le> c" then have "c < x" by auto
  2.2033 +    then show False using ntriv * by (auto simp: trivial_limit_def)
  2.2034 +  qed
  2.2035 +qed auto
  2.2036 +
  2.2037 +lemma mono_set:
  2.2038 +  fixes S :: "('a::order) set"
  2.2039 +  shows "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
  2.2040 +  by (auto simp: mono_def mem_def)
  2.2041 +
  2.2042 +lemma mono_greaterThan[intro, simp]: "mono {B<..}" unfolding mono_set by auto
  2.2043 +lemma mono_atLeast[intro, simp]: "mono {B..}" unfolding mono_set by auto
  2.2044 +lemma mono_UNIV[intro, simp]: "mono UNIV" unfolding mono_set by auto
  2.2045 +lemma mono_empty[intro, simp]: "mono {}" unfolding mono_set by auto
  2.2046 +
  2.2047 +lemma mono_set_iff:
  2.2048 +  fixes S :: "'a::{linorder,complete_lattice} set"
  2.2049 +  defines "a \<equiv> Inf S"
  2.2050 +  shows "mono S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
  2.2051 +proof
  2.2052 +  assume "mono S"
  2.2053 +  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
  2.2054 +  show ?c
  2.2055 +  proof cases
  2.2056 +    assume "a \<in> S"
  2.2057 +    show ?c
  2.2058 +      using mono[OF _ `a \<in> S`]
  2.2059 +      by (auto intro: complete_lattice_class.Inf_lower simp: a_def)
  2.2060 +  next
  2.2061 +    assume "a \<notin> S"
  2.2062 +    have "S = {a <..}"
  2.2063 +    proof safe
  2.2064 +      fix x assume "x \<in> S"
  2.2065 +      then have "a \<le> x" unfolding a_def by (rule complete_lattice_class.Inf_lower)
  2.2066 +      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
  2.2067 +    next
  2.2068 +      fix x assume "a < x"
  2.2069 +      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
  2.2070 +      with mono[of y x] show "x \<in> S" by auto
  2.2071 +    qed
  2.2072 +    then show ?c ..
  2.2073 +  qed
  2.2074 +qed auto
  2.2075 +
  2.2076 +lemma (in complete_lattice) not_less_bot[simp]: "\<not> (x < bot)"
  2.2077 +proof
  2.2078 +  assume "x < bot"
  2.2079 +  with bot_least[of x] show False by (auto simp: le_less)
  2.2080 +qed
  2.2081 +
  2.2082 +lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
  2.2083 +proof
  2.2084 +  assume "{x..} = UNIV"
  2.2085 +  show "x = bot"
  2.2086 +  proof (rule ccontr)
  2.2087 +    assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less)
  2.2088 +    then show False using `{x..} = UNIV` by simp
  2.2089 +  qed
  2.2090 +qed auto
  2.2091 +
  2.2092 +
  2.2093 +lemma extreal_open_atLeast: "open {x..} \<longleftrightarrow> x = -\<infinity>"
  2.2094 +proof
  2.2095 +  assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
  2.2096 +  then show "open {x..}" by auto
  2.2097 +next
  2.2098 +  assume "open {x..}"
  2.2099 +  then have "open {x..} \<and> closed {x..}" by auto
  2.2100 +  then have "{x..} = UNIV" unfolding extreal_open_closed by auto
  2.2101 +  then show "x = -\<infinity>" by (simp add: bot_extreal_def atLeast_eq_UNIV_iff)
  2.2102 +qed
  2.2103 +
  2.2104 +lemma extreal_open_mono_set:
  2.2105 +  fixes S :: "extreal set"
  2.2106 +  defines "a \<equiv> Inf S"
  2.2107 +  shows "(open S \<and> mono S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
  2.2108 +  by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff extreal_open_atLeast
  2.2109 +            extreal_open_closed mono_set_iff open_extreal_greaterThan)
  2.2110 +
  2.2111 +lemma extreal_closed_mono_set:
  2.2112 +  fixes S :: "extreal set"
  2.2113 +  shows "(closed S \<and> mono S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
  2.2114 +  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_extreal_atLeast
  2.2115 +            extreal_open_closed mono_empty mono_set_iff open_extreal_greaterThan)
  2.2116 +
  2.2117 +lemma extreal_Liminf_Sup_monoset:
  2.2118 +  fixes f :: "'a => extreal"
  2.2119 +  shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
  2.2120 +  unfolding Liminf_Sup
  2.2121 +proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
  2.2122 +  fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono S" "l \<in> S"
  2.2123 +  then have "S = UNIV \<or> S = {Inf S <..}"
  2.2124 +    using extreal_open_mono_set[of S] by auto
  2.2125 +  then show "eventually (\<lambda>x. f x \<in> S) net"
  2.2126 +  proof
  2.2127 +    assume S: "S = {Inf S<..}"
  2.2128 +    then have "Inf S < l" using `l \<in> S` by auto
  2.2129 +    then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
  2.2130 +    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
  2.2131 +  qed auto
  2.2132 +next
  2.2133 +  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
  2.2134 +  have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
  2.2135 +    using `y < l` by (intro S[rule_format]) auto
  2.2136 +  then show "eventually (\<lambda>x. y < f x) net" by auto
  2.2137 +qed
  2.2138 +
  2.2139 +lemma extreal_Inf_uminus_image_eq: "Inf (uminus ` S) = - Sup (S::extreal set)"
  2.2140 +  using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image)
  2.2141 +
  2.2142 +lemma extreal_range_uminus[simp]: "range uminus = (UNIV::extreal set)"
  2.2143 +proof safe
  2.2144 +  fix x :: extreal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
  2.2145 +qed auto
  2.2146 +
  2.2147 +lemma extreal_Limsup_Inf_monoset:
  2.2148 +  fixes f :: "'a => extreal"
  2.2149 +  shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
  2.2150 +  unfolding Limsup_Inf
  2.2151 +proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
  2.2152 +  fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono (uminus`S)" "l \<in> S"
  2.2153 +  then have "open (uminus`S) \<and> mono (uminus`S)" by (simp add: extreal_open_uminus)
  2.2154 +  then have "S = UNIV \<or> S = {..< Sup S}"
  2.2155 +    unfolding extreal_open_mono_set extreal_Inf_uminus_image_eq extreal_image_uminus_shift by simp
  2.2156 +  then show "eventually (\<lambda>x. f x \<in> S) net"
  2.2157 +  proof
  2.2158 +    assume S: "S = {..< Sup S}"
  2.2159 +    then have "l < Sup S" using `l \<in> S` by auto
  2.2160 +    then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
  2.2161 +    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
  2.2162 +  qed auto
  2.2163 +next
  2.2164 +  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
  2.2165 +  have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
  2.2166 +    using `l < y` by (intro S[rule_format]) auto
  2.2167 +  then show "eventually (\<lambda>x. f x < y) net" by auto
  2.2168 +qed
  2.2169 +
  2.2170 +lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::extreal set)"
  2.2171 +  using extreal_open_uminus[of S] extreal_open_uminus[of "uminus`S"] by auto
  2.2172 +
  2.2173 +lemma extreal_Limsup_uminus:
  2.2174 +  fixes f :: "'a => extreal"
  2.2175 +  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
  2.2176 +proof -
  2.2177 +  { fix P l have "(\<exists>x. (l::extreal) = -x \<and> P x) \<longleftrightarrow> P (-l)" by (auto intro!: exI[of _ "-l"]) }
  2.2178 +  note Ex_cancel = this
  2.2179 +  { fix P :: "extreal set \<Rightarrow> bool" have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
  2.2180 +      apply auto by (erule_tac x="uminus`S" in allE) (auto simp: image_image) }
  2.2181 +  note add_uminus_image = this
  2.2182 +  { fix x S have "(x::extreal) \<in> uminus`S \<longleftrightarrow> -x\<in>S" by (auto intro!: image_eqI[of _ _ "-x"]) }
  2.2183 +  note remove_uminus_image = this
  2.2184 +  show ?thesis
  2.2185 +    unfolding extreal_Limsup_Inf_monoset extreal_Liminf_Sup_monoset
  2.2186 +    unfolding extreal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
  2.2187 +    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
  2.2188 +qed
  2.2189 +
  2.2190 +lemma extreal_Liminf_uminus:
  2.2191 +  fixes f :: "'a => extreal"
  2.2192 +  shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
  2.2193 +  using extreal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
  2.2194 +
  2.2195 +lemma extreal_Lim_uminus:
  2.2196 +  fixes f :: "'a \<Rightarrow> extreal" shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
  2.2197 +  using
  2.2198 +    extreal_lim_mult[of f f0 net "- 1"]
  2.2199 +    extreal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
  2.2200 +  by (auto simp: extreal_uminus_reorder)
  2.2201 +
  2.2202 +lemma lim_imp_Liminf:
  2.2203 +  fixes f :: "'a \<Rightarrow> extreal"
  2.2204 +  assumes ntriv: "\<not> trivial_limit net"
  2.2205 +  assumes lim: "(f ---> f0) net"
  2.2206 +  shows "Liminf net f = f0"
  2.2207 +  unfolding Liminf_Sup
  2.2208 +proof (safe intro!: extreal_SupI)
  2.2209 +  fix y assume *: "\<forall>y'<y. eventually (\<lambda>x. y' < f x) net"
  2.2210 +  show "y \<le> f0"
  2.2211 +  proof (rule extreal_le_extreal)
  2.2212 +    fix B assume "B < y"
  2.2213 +    { assume "f0 < B"
  2.2214 +      then have "eventually (\<lambda>x. f x < B \<and> B < f x) net"
  2.2215 +         using topological_tendstoD[OF lim, of "{..<B}"] *[rule_format, OF `B < y`]
  2.2216 +         by (auto intro: eventually_conj)
  2.2217 +      also have "(\<lambda>x. f x < B \<and> B < f x) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
  2.2218 +      finally have False using ntriv[unfolded trivial_limit_def] by auto
  2.2219 +    } then show "B \<le> f0" by (metis linorder_le_less_linear)
  2.2220 +  qed
  2.2221 +next
  2.2222 +  fix y assume *: "\<forall>z. z \<in> {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net} \<longrightarrow> z \<le> y"
  2.2223 +  show "f0 \<le> y"
  2.2224 +  proof (safe intro!: *[rule_format])
  2.2225 +    fix y assume "y < f0" then show "eventually (\<lambda>x. y < f x) net"
  2.2226 +      using lim[THEN topological_tendstoD, of "{y <..}"] by auto
  2.2227 +  qed
  2.2228 +qed
  2.2229 +
  2.2230 +lemma lim_imp_Limsup:
  2.2231 +  fixes f :: "'a => extreal"
  2.2232 +  assumes "\<not> trivial_limit net"
  2.2233 +  assumes lim: "(f ---> f0) net"
  2.2234 +  shows "Limsup net f = f0"
  2.2235 +  using extreal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
  2.2236 +     extreal_Liminf_uminus[of net f] assms by simp
  2.2237 +
  2.2238 +lemma extreal_Liminf_le_Limsup:
  2.2239 +  fixes f :: "'a \<Rightarrow> extreal"
  2.2240 +  assumes ntriv: "\<not> trivial_limit net"
  2.2241 +  shows "Liminf net f \<le> Limsup net f"
  2.2242 +  unfolding Limsup_Inf Liminf_Sup
  2.2243 +proof (safe intro!: complete_lattice_class.Inf_greatest  complete_lattice_class.Sup_least)
  2.2244 +  fix u v assume *: "\<forall>y<u. eventually (\<lambda>x. y < f x) net" "\<forall>y>v. eventually (\<lambda>x. f x < y) net"
  2.2245 +  show "u \<le> v"
  2.2246 +  proof (rule ccontr)
  2.2247 +    assume "\<not> u \<le> v"
  2.2248 +    then obtain t where "t < u" "v < t"
  2.2249 +      using extreal_dense[of v u] by (auto simp: not_le)
  2.2250 +    then have "eventually (\<lambda>x. t < f x \<and> f x < t) net"
  2.2251 +      using * by (auto intro: eventually_conj)
  2.2252 +    also have "(\<lambda>x. t < f x \<and> f x < t) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
  2.2253 +    finally show False using ntriv by (auto simp: trivial_limit_def)
  2.2254 +  qed
  2.2255 +qed
  2.2256 +
  2.2257 +lemma Liminf_PInfty:
  2.2258 +  fixes f :: "'a \<Rightarrow> extreal"
  2.2259 +  assumes "\<not> trivial_limit net"
  2.2260 +  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
  2.2261 +proof (intro lim_imp_Liminf iffI assms)
  2.2262 +  assume rhs: "Liminf net f = \<infinity>"
  2.2263 +  { fix S assume "open S & \<infinity> : S"
  2.2264 +    then obtain m where "{extreal m<..} <= S" using open_PInfty2 by auto
  2.2265 +    moreover have "eventually (\<lambda>x. f x \<in> {extreal m<..}) net"
  2.2266 +      using rhs unfolding Liminf_Sup top_extreal_def[symmetric] Sup_eq_top_iff
  2.2267 +      by (auto elim!: allE[where x="extreal m"] simp: top_extreal_def)
  2.2268 +    ultimately have "eventually (%x. f x : S) net" apply (subst eventually_mono) by auto
  2.2269 +  } then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
  2.2270 +qed
  2.2271 +
  2.2272 +lemma Limsup_MInfty:
  2.2273 +  fixes f :: "'a \<Rightarrow> extreal"
  2.2274 +  assumes "\<not> trivial_limit net"
  2.2275 +  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
  2.2276 +  using assms extreal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
  2.2277 +        extreal_Liminf_uminus[of _ f] by (auto simp: extreal_uminus_eq_reorder)
  2.2278 +
  2.2279 +lemma extreal_Liminf_eq_Limsup:
  2.2280 +  fixes f :: "'a \<Rightarrow> extreal"
  2.2281 +  assumes ntriv: "\<not> trivial_limit net"
  2.2282 +  assumes lim: "Liminf net f = f0" "Limsup net f = f0"
  2.2283 +  shows "(f ---> f0) net"
  2.2284 +proof (cases f0)
  2.2285 +  case PInf then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
  2.2286 +next
  2.2287 +  case MInf then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
  2.2288 +next
  2.2289 +  case (real r)
  2.2290 +  show "(f ---> f0) net"
  2.2291 +  proof (rule topological_tendstoI)
  2.2292 +    fix S assume "open S""f0 \<in> S"
  2.2293 +    then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
  2.2294 +      using extreal_open_cont_interval2[of S f0] real lim by auto
  2.2295 +    then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
  2.2296 +      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
  2.2297 +      by (auto intro!: eventually_conj simp add: greaterThanLessThan_iff)
  2.2298 +    with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
  2.2299 +      by (rule_tac eventually_mono) auto
  2.2300 +  qed
  2.2301 +qed
  2.2302 +
  2.2303 +lemma extreal_Liminf_eq_Limsup_iff:
  2.2304 +  fixes f :: "'a \<Rightarrow> extreal"
  2.2305 +  assumes "\<not> trivial_limit net"
  2.2306 +  shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
  2.2307 +  by (metis assms extreal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
  2.2308 +
  2.2309 +
  2.2310 +lemma Liminf_mono:
  2.2311 +  fixes f g :: "'a => extreal"
  2.2312 +  assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
  2.2313 +  shows "Liminf net f \<le> Liminf net g"
  2.2314 +  unfolding Liminf_Sup
  2.2315 +proof (safe intro!: Sup_mono bexI)
  2.2316 +  fix a y assume "\<forall>y<a. eventually (\<lambda>x. y < f x) net" and "y < a"
  2.2317 +  then have "eventually (\<lambda>x. y < f x) net" by auto
  2.2318 +  then show "eventually (\<lambda>x. y < g x) net"
  2.2319 +    by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
  2.2320 +qed simp
  2.2321 +
  2.2322 +lemma Liminf_eq:
  2.2323 +  fixes f g :: "'a \<Rightarrow> extreal"
  2.2324 +  assumes "eventually (\<lambda>x. f x = g x) net"
  2.2325 +  shows "Liminf net f = Liminf net g"
  2.2326 +  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
  2.2327 +
  2.2328 +lemma Liminf_mono_all:
  2.2329 +  fixes f g :: "'a \<Rightarrow> extreal"
  2.2330 +  assumes "\<And>x. f x \<le> g x"
  2.2331 +  shows "Liminf net f \<le> Liminf net g"
  2.2332 +  using assms by (intro Liminf_mono always_eventually) auto
  2.2333 +
  2.2334 +lemma Limsup_mono:
  2.2335 +  fixes f g :: "'a \<Rightarrow> extreal"
  2.2336 +  assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
  2.2337 +  shows "Limsup net f \<le> Limsup net g"
  2.2338 +  unfolding Limsup_Inf
  2.2339 +proof (safe intro!: Inf_mono bexI)
  2.2340 +  fix a y assume "\<forall>y>a. eventually (\<lambda>x. g x < y) net" and "a < y"
  2.2341 +  then have "eventually (\<lambda>x. g x < y) net" by auto
  2.2342 +  then show "eventually (\<lambda>x. f x < y) net"
  2.2343 +    by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
  2.2344 +qed simp
  2.2345 +
  2.2346 +lemma Limsup_mono_all:
  2.2347 +  fixes f g :: "'a \<Rightarrow> extreal"
  2.2348 +  assumes "\<And>x. f x \<le> g x"
  2.2349 +  shows "Limsup net f \<le> Limsup net g"
  2.2350 +  using assms by (intro Limsup_mono always_eventually) auto
  2.2351 +
  2.2352 +lemma Limsup_eq:
  2.2353 +  fixes f g :: "'a \<Rightarrow> extreal"
  2.2354 +  assumes "eventually (\<lambda>x. f x = g x) net"
  2.2355 +  shows "Limsup net f = Limsup net g"
  2.2356 +  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
  2.2357 +
  2.2358 +abbreviation "liminf \<equiv> Liminf sequentially"
  2.2359 +
  2.2360 +abbreviation "limsup \<equiv> Limsup sequentially"
  2.2361 +
  2.2362 +lemma (in complete_lattice) less_INFD:
  2.2363 +  assumes "y < INFI A f"" i \<in> A" shows "y < f i"
  2.2364 +proof -
  2.2365 +  note `y < INFI A f`
  2.2366 +  also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
  2.2367 +  finally show "y < f i" .
  2.2368 +qed
  2.2369 +
  2.2370 +lemma liminf_SUPR_INFI:
  2.2371 +  fixes f :: "nat \<Rightarrow> extreal"
  2.2372 +  shows "liminf f = (SUP n. INF m:{n..}. f m)"
  2.2373 +  unfolding Liminf_Sup eventually_sequentially
  2.2374 +proof (safe intro!: antisym complete_lattice_class.Sup_least)
  2.2375 +  fix x assume *: "\<forall>y<x. \<exists>N. \<forall>n\<ge>N. y < f n" show "x \<le> (SUP n. INF m:{n..}. f m)"
  2.2376 +  proof (rule extreal_le_extreal)
  2.2377 +    fix y assume "y < x"
  2.2378 +    with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
  2.2379 +    then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
  2.2380 +    also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro le_SUPI) auto
  2.2381 +    finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
  2.2382 +  qed
  2.2383 +next
  2.2384 +  show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
  2.2385 +  proof (unfold SUPR_def, safe intro!: Sup_mono bexI)
  2.2386 +    fix y n assume "y < INFI {n..} f"
  2.2387 +    from less_INFD[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
  2.2388 +  qed (rule order_refl)
  2.2389 +qed
  2.2390 +
  2.2391 +lemma limsup_INFI_SUPR:
  2.2392 +  fixes f :: "nat \<Rightarrow> extreal"
  2.2393 +  shows "limsup f = (INF n. SUP m:{n..}. f m)"
  2.2394 +  using extreal_Limsup_uminus[of sequentially "\<lambda>x. - f x"]
  2.2395 +  by (simp add: liminf_SUPR_INFI extreal_INFI_uminus extreal_SUPR_uminus)
  2.2396 +
  2.2397 +lemma liminf_PInfty:
  2.2398 +  fixes X :: "nat => extreal"
  2.2399 +  shows "X ----> \<infinity> <-> liminf X = \<infinity>"
  2.2400 +by (metis Liminf_PInfty trivial_limit_sequentially)
  2.2401 +
  2.2402 +lemma limsup_MInfty:
  2.2403 +  fixes X :: "nat => extreal"
  2.2404 +  shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)"
  2.2405 +by (metis Limsup_MInfty trivial_limit_sequentially)
  2.2406 +
  2.2407 +lemma tail_same_limsup:
  2.2408 +  fixes X Y :: "nat => extreal"
  2.2409 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
  2.2410 +  shows "limsup X = limsup Y"
  2.2411 +  using Limsup_eq[of X Y sequentially] eventually_sequentially assms by auto
  2.2412 +
  2.2413 +lemma tail_same_liminf:
  2.2414 +  fixes X Y :: "nat => extreal"
  2.2415 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
  2.2416 +  shows "liminf X = liminf Y"
  2.2417 +  using Liminf_eq[of X Y sequentially] eventually_sequentially assms by auto
  2.2418 +
  2.2419 +lemma liminf_mono:
  2.2420 +  fixes X Y :: "nat \<Rightarrow> extreal"
  2.2421 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
  2.2422 +  shows "liminf X \<le> liminf Y"
  2.2423 +  using Liminf_mono[of X Y sequentially] eventually_sequentially assms by auto
  2.2424 +
  2.2425 +lemma limsup_mono:
  2.2426 +  fixes X Y :: "nat => extreal"
  2.2427 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
  2.2428 +  shows "limsup X \<le> limsup Y"
  2.2429 +  using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
  2.2430 +
  2.2431 +declare trivial_limit_sequentially[simp]
  2.2432 +
  2.2433 +lemma liminf_bounded:
  2.2434 +  fixes X Y :: "nat \<Rightarrow> extreal"
  2.2435 +  assumes "\<And>n. N \<le> n \<Longrightarrow> C \<le> X n"
  2.2436 +  shows "C \<le> liminf X"
  2.2437 +  using liminf_mono[of N "\<lambda>n. C" X] assms Liminf_const[of sequentially C] by simp
  2.2438 +
  2.2439 +lemma limsup_bounded:
  2.2440 +  fixes X Y :: "nat => extreal"
  2.2441 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= C"
  2.2442 +  shows "limsup X \<le> C"
  2.2443 +  using limsup_mono[of N X "\<lambda>n. C"] assms Limsup_const[of sequentially C] by simp
  2.2444 +
  2.2445 +lemma liminf_bounded_iff:
  2.2446 +  fixes x :: "nat \<Rightarrow> extreal"
  2.2447 +  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
  2.2448 +proof safe
  2.2449 +  fix B assume "B < C" "C \<le> liminf x"
  2.2450 +  then have "B < liminf x" by auto
  2.2451 +  then obtain N where "B < (INF m:{N..}. x m)"
  2.2452 +    unfolding liminf_SUPR_INFI SUPR_def less_Sup_iff by auto
  2.2453 +  from less_INFD[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
  2.2454 +next
  2.2455 +  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
  2.2456 +  { fix B assume "B<C"
  2.2457 +    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
  2.2458 +    hence "B \<le> (INF m:{N..}. x m)" by (intro le_INFI) auto
  2.2459 +    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro le_SUPI) simp
  2.2460 +    finally have "B \<le> liminf x" .
  2.2461 +  } then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
  2.2462 +qed
  2.2463 +
  2.2464 +lemma liminf_bounded_open:
  2.2465 +  fixes x :: "nat \<Rightarrow> extreal"
  2.2466 +  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" 
  2.2467 +  (is "_ \<longleftrightarrow> ?P x0")
  2.2468 +proof
  2.2469 +  assume "?P x0" then show "x0 \<le> liminf x"
  2.2470 +    unfolding extreal_Liminf_Sup_monoset eventually_sequentially
  2.2471 +    by (intro complete_lattice_class.Sup_upper) auto
  2.2472 +next
  2.2473 +  assume "x0 \<le> liminf x"
  2.2474 +  { fix S :: "extreal set" assume om: "open S & mono S & x0:S"
  2.2475 +    { assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto }
  2.2476 +    moreover
  2.2477 +    { assume "~(S=UNIV)"
  2.2478 +      then obtain B where B_def: "S = {B<..}" using om extreal_open_mono_set by auto
  2.2479 +      hence "B<x0" using om by auto
  2.2480 +      hence "EX N. ALL n>=N. x n : S" unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
  2.2481 +    } ultimately have "EX N. (ALL n>=N. x n : S)" by auto
  2.2482 +  } then show "?P x0" by auto
  2.2483 +qed
  2.2484 +
  2.2485 +
  2.2486 +lemma extreal_lim_mono:
  2.2487 +  fixes X Y :: "nat => extreal"
  2.2488 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
  2.2489 +  assumes "X ----> x" "Y ----> y"
  2.2490 +  shows "x <= y"
  2.2491 +  by (metis extreal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
  2.2492 +
  2.2493 +lemma liminf_subseq_mono:
  2.2494 +  fixes X :: "nat \<Rightarrow> extreal"
  2.2495 +  assumes "subseq r"
  2.2496 +  shows "liminf X \<le> liminf (X \<circ> r) "
  2.2497 +proof-
  2.2498 +  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
  2.2499 +  proof (safe intro!: INF_mono)
  2.2500 +    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
  2.2501 +      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
  2.2502 +  qed
  2.2503 +  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
  2.2504 +qed
  2.2505 +
  2.2506 +lemma limsup_subseq_mono:
  2.2507 +  fixes X :: "nat \<Rightarrow> extreal"
  2.2508 +  assumes "subseq r"
  2.2509 +  shows "limsup (X \<circ> r) \<le> limsup X"
  2.2510 +proof-
  2.2511 +  have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
  2.2512 +  then have "- limsup X \<le> - limsup (X \<circ> r)"
  2.2513 +     using liminf_subseq_mono[of r "(%n. - X n)"]
  2.2514 +       extreal_Liminf_uminus[of sequentially X]
  2.2515 +       extreal_Liminf_uminus[of sequentially "X o r"] assms by auto
  2.2516 +  then show ?thesis by auto
  2.2517 +qed
  2.2518 +
  2.2519 +lemma bounded_abs:
  2.2520 +  assumes "(a::real)<=x" "x<=b"
  2.2521 +  shows "abs x <= max (abs a) (abs b)"
  2.2522 +by (metis abs_less_iff assms leI le_max_iff_disj less_eq_real_def less_le_not_le less_minus_iff minus_minus)
  2.2523 +
  2.2524 +
  2.2525 +lemma bounded_increasing_convergent2: fixes f::"nat => real"
  2.2526 +  assumes "ALL n. f n <= B"  "ALL n m. n>=m --> f n >= f m"
  2.2527 +  shows "EX l. (f ---> l) sequentially"
  2.2528 +proof-
  2.2529 +def N == "max (abs (f 0)) (abs B)"
  2.2530 +{ fix n have "abs (f n) <= N" unfolding N_def apply (subst bounded_abs) using assms by auto }
  2.2531 +hence "bounded {f n| n::nat. True}" unfolding bounded_real by auto
  2.2532 +from this show ?thesis apply(rule Topology_Euclidean_Space.bounded_increasing_convergent)
  2.2533 +   using assms by auto
  2.2534 +qed
  2.2535 +
  2.2536 +
  2.2537 +lemma extreal_real': assumes "x~=\<infinity>" and "x~=(-\<infinity>)" shows "extreal (real x) = x"
  2.2538 +   using assms extreal_real by auto
  2.2539 +
  2.2540 +
  2.2541 +lemma lim_extreal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
  2.2542 +  obtains l where "f ----> (l::extreal)"
  2.2543 +proof(cases "f = (\<lambda>x. - \<infinity>)")
  2.2544 +  case True then show thesis using Lim_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
  2.2545 +next
  2.2546 +  case False
  2.2547 +  from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
  2.2548 +  have "ALL n>=N. f n >= f N" using assms by auto
  2.2549 +  hence minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
  2.2550 +  def Y == "(%n. (if n>=N then f n else f N))"
  2.2551 +  hence incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
  2.2552 +  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
  2.2553 +  show thesis
  2.2554 +  proof(cases "EX B. ALL n. f n < extreal B")
  2.2555 +    case False thus thesis apply- apply(rule that[of \<infinity>]) unfolding Lim_PInfty not_ex not_all
  2.2556 +    apply safe apply(erule_tac x=B in allE,safe) apply(rule_tac x=x in exI,safe)
  2.2557 +    apply(rule order_trans[OF _ assms[rule_format]]) by auto
  2.2558 +  next case True then guess B ..
  2.2559 +    hence "ALL n. Y n < extreal B" using Y_def by auto note B = this[rule_format]
  2.2560 +    { fix n have "Y n < \<infinity>" using B[of n] apply (subst less_le_trans) by auto
  2.2561 +      hence "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
  2.2562 +    } hence *: "ALL n. Y n ~= \<infinity> & Y n ~= (-\<infinity>)" by auto
  2.2563 +    { fix n have "real (Y n) < B" proof- case goal1 thus ?case
  2.2564 +        using B[of n] apply-apply(subst(asm) extreal_real'[THEN sym]) defer defer
  2.2565 +        unfolding extreal_less using * by auto
  2.2566 +      qed
  2.2567 +    }
  2.2568 +    hence B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
  2.2569 +    have "EX l. (%n. real (Y n)) ----> l"
  2.2570 +      apply(rule bounded_increasing_convergent2)
  2.2571 +    proof safe show "!!n. real (Y n) <= B" using B' by auto
  2.2572 +      fix n m::nat assume "n<=m"
  2.2573 +      hence "extreal (real (Y n)) <= extreal (real (Y m))"
  2.2574 +        using incy[rule_format,of n m] apply(subst extreal_real)+
  2.2575 +        using *[rule_format, of n] *[rule_format, of m] by auto
  2.2576 +      thus "real (Y n) <= real (Y m)" by auto
  2.2577 +    qed then guess l .. note l=this
  2.2578 +    have "Y ----> extreal l" using l apply-apply(subst(asm) lim_extreal[THEN sym])
  2.2579 +    unfolding extreal_real using * by auto
  2.2580 +    thus thesis apply-apply(rule that[of "extreal l"])
  2.2581 +       apply (subst tail_same_limit[of Y _ N]) using Y_def by auto
  2.2582 +  qed
  2.2583 +qed
  2.2584 +
  2.2585 +
  2.2586 +lemma lim_extreal_decreasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
  2.2587 +  obtains l where "f ----> (l::extreal)"
  2.2588 +proof -
  2.2589 +  from lim_extreal_increasing[of "\<lambda>x. - f x"] assms
  2.2590 +  obtain l where "(\<lambda>x. - f x) ----> l" by auto
  2.2591 +  from extreal_lim_mult[OF this, of "- 1"] show thesis 
  2.2592 +    by (intro that[of "-l"]) (simp add: extreal_uminus_eq_reorder)
  2.2593 +qed
  2.2594 +
  2.2595 +lemma compact_extreal:
  2.2596 +  fixes X :: "nat \<Rightarrow> extreal"
  2.2597 +  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
  2.2598 +proof -
  2.2599 +  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
  2.2600 +    using seq_monosub[of X] unfolding comp_def by auto
  2.2601 +  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)"
  2.2602 +    by (auto simp add: monoseq_def)
  2.2603 +  then obtain l where "(X\<circ>r) ----> l"
  2.2604 +     using lim_extreal_increasing[of "X \<circ> r"] lim_extreal_decreasing[of "X \<circ> r"] by auto
  2.2605 +  then show ?thesis using `subseq r` by auto
  2.2606 +qed
  2.2607 +
  2.2608 +lemma extreal_Sup_lim:
  2.2609 +  assumes "\<And>n. b n \<in> s" "b ----> (a::extreal)"
  2.2610 +  shows "a \<le> Sup s"
  2.2611 +by (metis Lim_bounded_extreal assms complete_lattice_class.Sup_upper)
  2.2612 +
  2.2613 +lemma extreal_Inf_lim:
  2.2614 +  assumes "\<And>n. b n \<in> s" "b ----> (a::extreal)"
  2.2615 +  shows "Inf s \<le> a"
  2.2616 +by (metis Lim_bounded2_extreal assms complete_lattice_class.Inf_lower)
  2.2617 +
  2.2618 +lemma incseq_le_extreal: assumes inc: "!!n m. n>=m ==> X n >= X m"
  2.2619 +  and lim: "X ----> (L::extreal)" shows "X N <= L"
  2.2620 +proof(cases "X N = (-\<infinity>)")
  2.2621 +case True thus ?thesis by auto
  2.2622 +next
  2.2623 +case False
  2.2624 +   have "ALL n>=N. X n >= X N" using inc by auto
  2.2625 +   hence minf: "ALL n>=N. X n > (-\<infinity>)" using False by auto
  2.2626 +   def Y == "(%n. (if n>=N then X n else X N))"
  2.2627 +   hence incy: "!!n m. n>=m ==> Y n >= Y m" using inc by auto
  2.2628 +   from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
  2.2629 +   from lim have limy: "Y ----> L"
  2.2630 +      apply (subst tail_same_limit[of X _ N]) using Y_def by auto
  2.2631 +show ?thesis
  2.2632 +proof(cases "L = \<infinity> | L=(-\<infinity>)")
  2.2633 +  case False have "ALL n. Y n ~= \<infinity>"
  2.2634 +  proof(rule ccontr,unfold not_all not_not,safe)
  2.2635 +    case goal1 hence "ALL n>=x. Y n = \<infinity>" using incy[of x] by auto
  2.2636 +    hence "Y ----> \<infinity>" unfolding tendsto_def eventually_sequentially
  2.2637 +      apply safe apply(rule_tac x=x in exI) by auto
  2.2638 +    note Lim_unique[OF trivial_limit_sequentially this limy]
  2.2639 +    with False show False by auto
  2.2640 +  qed note * =this[rule_format]
  2.2641 +
  2.2642 +  have **:"ALL m n. m <= n --> extreal (real (Y m)) <= extreal (real (Y n))"
  2.2643 +    unfolding extreal_real using minfy * incy apply (cases "Y m", cases "Y n") by auto
  2.2644 +  have "real (Y N) <= real L" apply-apply(rule incseq_le) defer
  2.2645 +  apply(subst lim_extreal[THEN sym])
  2.2646 +    unfolding extreal_real
  2.2647 +    unfolding incseq_def using minfy * ** limy False by auto
  2.2648 +  hence "extreal (real (Y N)) <= extreal (real L)" by auto
  2.2649 +  hence ***: "Y N <= L" unfolding extreal_real using minfy * False by auto
  2.2650 +  thus ?thesis using Y_def by auto
  2.2651 +next
  2.2652 +case True
  2.2653 +show ?thesis proof(cases "L=(-\<infinity>)")
  2.2654 +  case True
  2.2655 +  have "open {..<X N}" by auto
  2.2656 +  moreover have "(-\<infinity>) : {..<X N}" using False by auto
  2.2657 +  ultimately obtain N1 where "ALL n>=N1. X n : {..<X N}" using lim True
  2.2658 +     unfolding tendsto_def eventually_sequentially by metis
  2.2659 +  hence "X (max N N1) : {..<X N}" by auto
  2.2660 +  with inc[of N "max N N1"] show ?thesis by auto
  2.2661 +next
  2.2662 +case False thus ?thesis using True by auto qed
  2.2663 +qed
  2.2664 +qed
  2.2665 +
  2.2666 +
  2.2667 +lemma decseq_ge_extreal: assumes dec: "!!n m. n>=m ==> X n <= X m"
  2.2668 +  and lim: "X ----> (L::extreal)" shows "X N >= L"
  2.2669 +proof-
  2.2670 +def Y == "(%i. -(X i))"
  2.2671 +hence inc: "!!n m. n>=m ==> Y n >= Y m" using dec extreal_minus_le_minus by auto
  2.2672 +moreover have limy: "Y ----> (-L)" using Y_def extreal_lim_uminus lim by auto
  2.2673 +ultimately have "Y N <= -L" using incseq_le_extreal[of Y "-L"] by auto
  2.2674 +from this show ?thesis using Y_def extreal_minus_le_minus by auto
  2.2675 +qed
  2.2676 +
  2.2677 +
  2.2678 +lemma real_interm:
  2.2679 + assumes "(a::real)<b"
  2.2680 + shows "a + (b-a)/2 < b"
  2.2681 +by (metis Bit0_def assms comm_semiring_1_class.normalizing_semiring_rules(24) diff_minus_eq_add number_of_is_id one_is_num_one pth_2 real_average_minus_second real_gt_half_sum succ_def)
  2.2682 +
  2.2683 +
  2.2684 +lemma SUP_Lim_extreal: assumes "!!n m. n>=m ==> f n >= f m" "f ----> l"
  2.2685 +  shows "(SUP n. f n) = (l::extreal)" unfolding SUPR_def Sup_extreal_def
  2.2686 +proof (safe intro!: Least_equality)
  2.2687 +  fix n::nat show "f n <= l" apply(rule incseq_le_extreal)
  2.2688 +    using assms by auto
  2.2689 +next fix y assume y:"ALL x:range f. x <= y" show "l <= y"
  2.2690 +  proof-
  2.2691 +    { assume ym: "y ~= (-\<infinity>)" and yp: "y ~= \<infinity>"
  2.2692 +      { assume as:"y < l"
  2.2693 +        hence lm: "l ~= (-\<infinity>)" by auto
  2.2694 +        have lp:"l ~= \<infinity>" apply(rule Lim_bounded_PInfty[OF assms(2), of "real y"])
  2.2695 +          using y yp unfolding extreal_real by auto
  2.2696 +        have [simp]: "extreal (1 / 2) = 1 / 2" by (auto simp: divide_extreal_def)
  2.2697 +        have yl:"real y < real l" using as apply-
  2.2698 +          apply(subst(asm) extreal_real'[THEN sym,OF `y~=\<infinity>` `y~=(-\<infinity>)`])
  2.2699 +          apply(subst(asm) extreal_real'[THEN sym,OF `l~=\<infinity>` `l~=(-\<infinity>)`])
  2.2700 +          unfolding extreal_less by auto
  2.2701 +        hence "y + (l - y) * 1 / 2 < l" apply-
  2.2702 +          apply(subst extreal_real'[THEN sym,OF `y~=\<infinity>` `y~=(-\<infinity>)`])
  2.2703 +          apply(subst(2) extreal_real'[THEN sym,OF `y~=\<infinity>` `y~=(-\<infinity>)`])
  2.2704 +          apply(subst extreal_real'[THEN sym,OF `l~=\<infinity>` `l~=(-\<infinity>)`])
  2.2705 +          apply(subst(2) extreal_real'[THEN sym,OF `l~=\<infinity>` `l~=(-\<infinity>)`])
  2.2706 +          using real_interm by auto
  2.2707 +        hence *:"l : {y + (l - y) / 2<..}" by auto
  2.2708 +        have "open {y + (l-y)/2 <..}" by auto
  2.2709 +        note topological_tendstoD[OF assms(2) this *]
  2.2710 +        from this[unfolded eventually_sequentially] guess N .. note this[rule_format, of N]
  2.2711 +        hence "y + (l - y)  / 2 < y" using y[rule_format,of "f N"] by auto
  2.2712 +        hence "extreal (real y) + (extreal (real l) - extreal (real y)) / 2 < extreal (real y)"
  2.2713 +          unfolding extreal_real using `y~=\<infinity>` `y~=(-\<infinity>)` `l~=\<infinity>` `l~=(-\<infinity>)` by auto
  2.2714 +        hence False using yl by auto
  2.2715 +      } hence ?thesis using not_le by auto
  2.2716 +    }
  2.2717 +    moreover
  2.2718 +    { assume "y=(-\<infinity>)" hence "f = (\<lambda>_. -\<infinity>)" using y by (auto simp: fun_eq_iff)
  2.2719 +      hence "l=(-\<infinity>)" using `f ----> l` using tendsto_const[of "-\<infinity>"]
  2.2720 +         Lim_unique[OF trivial_limit_sequentially] by auto
  2.2721 +      hence ?thesis by auto
  2.2722 +    }
  2.2723 +    moreover have "y=\<infinity> --> l <= y" by auto
  2.2724 +    ultimately show ?thesis by blast
  2.2725 +  qed
  2.2726 +qed
  2.2727 +
  2.2728 +lemma INF_Lim_extreal: assumes "!!n m. n>=m ==> f n <= f m" "f ----> l"
  2.2729 +  shows "(INF n. f n) = (l::extreal)"
  2.2730 +proof-
  2.2731 +def Y == "(%i. -(f i))"
  2.2732 +hence inc: "!!n m. n>=m ==> Y n >= Y m" using assms extreal_minus_le_minus by auto
  2.2733 +moreover have limy: "Y ----> (-l)" using Y_def extreal_lim_uminus assms by auto
  2.2734 +ultimately have "(SUP n. Y n) = -l" using SUP_Lim_extreal[of Y "-l"] by auto
  2.2735 +hence "- (INF n. f n) = - l" using Y_def extreal_SUPR_uminus[of "UNIV" f] by auto
  2.2736 +from this show ?thesis by simp
  2.2737 +qed
  2.2738 +
  2.2739 +
  2.2740 +lemma incseq_mono: "mono f <-> incseq f"
  2.2741 +  unfolding mono_def incseq_def by auto
  2.2742 +
  2.2743 +
  2.2744 +lemma SUP_eq_LIMSEQ:
  2.2745 +  assumes "mono f"
  2.2746 +  shows "(SUP n. extreal (f n)) = extreal x <-> f ----> x"
  2.2747 +proof
  2.2748 +  assume x: "(SUP n. extreal (f n)) = extreal x"
  2.2749 +  { fix n
  2.2750 +    have "extreal (f n) <= extreal x" using x[symmetric] by (auto intro: le_SUPI)
  2.2751 +    hence "f n <= x" using assms by simp }
  2.2752 +  show "f ----> x"
  2.2753 +  proof (rule LIMSEQ_I)
  2.2754 +    fix r :: real assume "0 < r"
  2.2755 +    show "EX no. ALL n>=no. norm (f n - x) < r"
  2.2756 +    proof (rule ccontr)
  2.2757 +      assume *: "~ ?thesis"
  2.2758 +      { fix N
  2.2759 +        from * obtain n where "N <= n" "r <= x - f n"
  2.2760 +          using `!!n. f n <= x` by (auto simp: not_less)
  2.2761 +        hence "f N <= f n" using `mono f` by (auto dest: monoD)
  2.2762 +        hence "f N <= x - r" using `r <= x - f n` by auto
  2.2763 +        hence "extreal (f N) <= extreal (x - r)" by auto }
  2.2764 +      hence "(SUP n. extreal (f n)) <= extreal (x - r)"
  2.2765 +        and "extreal (x - r) < extreal x" using `0 < r` by (auto intro: SUP_leI)
  2.2766 +      hence "(SUP n. extreal (f n)) < extreal x" by (rule le_less_trans)
  2.2767 +      thus False using x by auto
  2.2768 +    qed
  2.2769 +  qed
  2.2770 +next
  2.2771 +  assume "f ----> x"
  2.2772 +  show "(SUP n. extreal (f n)) = extreal x"
  2.2773 +  proof (rule extreal_SUPI)
  2.2774 +    fix n
  2.2775 +    from incseq_le[of f x] `mono f` `f ----> x`
  2.2776 +    show "extreal (f n) <= extreal x" using assms incseq_mono by auto
  2.2777 +  next
  2.2778 +    fix y assume *: "!!n. n:UNIV ==> extreal (f n) <= y"
  2.2779 +    show "extreal x <= y"
  2.2780 +    proof-
  2.2781 +    { assume "EX r. y = extreal r"
  2.2782 +      from this obtain r where r_def: "y = extreal r" by auto
  2.2783 +      with * have "EX N. ALL n>=N. f n <= r" using assms by fastsimp
  2.2784 +      from LIMSEQ_le_const2[OF `f ----> x` this]
  2.2785 +      have "extreal x <= y" using r_def by auto
  2.2786 +    }
  2.2787 +    moreover
  2.2788 +    { assume "y=\<infinity> | y=(-\<infinity>)"
  2.2789 +      hence ?thesis using * by auto
  2.2790 +    } ultimately show ?thesis by (cases y) auto
  2.2791 +    qed
  2.2792 +  qed
  2.2793 +qed
  2.2794 +
  2.2795 +
  2.2796 +lemma Liminf_within:
  2.2797 +  fixes f :: "'a::metric_space => extreal"
  2.2798 +  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
  2.2799 +proof-
  2.2800 +let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
  2.2801 +{ fix T assume T_def: "open T & mono T & ?l:T"
  2.2802 +  have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
  2.2803 +  proof-
  2.2804 +  { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
  2.2805 +  moreover
  2.2806 +  { assume "~(T=UNIV)"
  2.2807 +    then obtain B where "T={B<..}" using T_def extreal_open_mono_set[of T] by auto
  2.2808 +    hence "B<?l" using T_def by auto
  2.2809 +    then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
  2.2810 +      unfolding less_SUP_iff by auto
  2.2811 +    { fix y assume "y:S & 0 < dist y x & dist y x < d"
  2.2812 +      hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
  2.2813 +      hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
  2.2814 +    } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
  2.2815 +  } ultimately show ?thesis by auto
  2.2816 +  qed
  2.2817 +}
  2.2818 +moreover
  2.2819 +{ fix z
  2.2820 +  assume a: "ALL T. open T --> mono T --> z : T -->
  2.2821 +     (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
  2.2822 +  { fix B assume "B<z"
  2.2823 +    then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
  2.2824 +       using a[rule_format, of "{B<..}"] mono_greaterThan by auto
  2.2825 +    { fix y assume "y:(S Int ball x d - {x})"
  2.2826 +      hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
  2.2827 +         by (metis dist_eq_0_iff real_less_def zero_le_dist)
  2.2828 +      hence "B <= f y" using d_def by auto
  2.2829 +    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto
  2.2830 +    also have "...<=?l" apply (subst le_SUPI) using d_def by auto
  2.2831 +    finally have "B<=?l" by auto
  2.2832 +  } hence "z <= ?l" using extreal_le_extreal[of z "?l"] by auto
  2.2833 +}
  2.2834 +ultimately show ?thesis unfolding extreal_Liminf_Sup_monoset eventually_within
  2.2835 +   apply (subst extreal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"]) by auto
  2.2836 +qed
  2.2837 +
  2.2838 +lemma Limsup_within:
  2.2839 +  fixes f :: "'a::metric_space => extreal"
  2.2840 +  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
  2.2841 +proof-
  2.2842 +let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
  2.2843 +{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T"
  2.2844 +  have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
  2.2845 +  proof-
  2.2846 +  { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
  2.2847 +  moreover
  2.2848 +  { assume "~(T=UNIV)" hence "~(uminus ` T = UNIV)"
  2.2849 +       by (metis Int_UNIV_right Int_absorb1 image_mono extreal_minus_minus_image subset_UNIV)
  2.2850 +    hence "uminus ` T = {Inf (uminus ` T)<..}" using T_def extreal_open_mono_set[of "uminus ` T"]
  2.2851 +       extreal_open_uminus[of T] by auto
  2.2852 +    then obtain B where "T={..<B}"
  2.2853 +      unfolding extreal_Inf_uminus_image_eq extreal_uminus_lessThan[symmetric]
  2.2854 +      unfolding inj_image_eq_iff[OF extreal_inj_on_uminus] by simp
  2.2855 +    hence "?l<B" using T_def by auto
  2.2856 +    then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
  2.2857 +      unfolding INF_less_iff by auto
  2.2858 +    { fix y assume "y:S & 0 < dist y x & dist y x < d"
  2.2859 +      hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
  2.2860 +      hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
  2.2861 +    } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
  2.2862 +  } ultimately show ?thesis by auto
  2.2863 +  qed
  2.2864 +}
  2.2865 +moreover
  2.2866 +{ fix z
  2.2867 +  assume a: "ALL T. open T --> mono (uminus ` T) --> z : T -->
  2.2868 +     (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
  2.2869 +  { fix B assume "z<B"
  2.2870 +    then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
  2.2871 +       using a[rule_format, of "{..<B}"] by auto
  2.2872 +    { fix y assume "y:(S Int ball x d - {x})"
  2.2873 +      hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
  2.2874 +         by (metis dist_eq_0_iff real_less_def zero_le_dist)
  2.2875 +      hence "f y <= B" using d_def by auto
  2.2876 +    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto
  2.2877 +    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto
  2.2878 +    ultimately have "?l<=B" by auto
  2.2879 +  } hence "?l <= z" using extreal_ge_extreal[of z "?l"] by auto
  2.2880 +}
  2.2881 +ultimately show ?thesis unfolding extreal_Limsup_Inf_monoset eventually_within
  2.2882 +   apply (subst extreal_InfI) by auto
  2.2883 +qed
  2.2884 +
  2.2885 +
  2.2886 +lemma Liminf_within_UNIV:
  2.2887 +  fixes f :: "'a::metric_space => extreal"
  2.2888 +  shows "Liminf (at x) f = Liminf (at x within UNIV) f"
  2.2889 +by (metis within_UNIV)
  2.2890 +
  2.2891 +
  2.2892 +lemma Liminf_at:
  2.2893 +  fixes f :: "'a::metric_space => extreal"
  2.2894 +  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
  2.2895 +using Liminf_within[of x UNIV f] Liminf_within_UNIV[of x f] by auto
  2.2896 +
  2.2897 +
  2.2898 +lemma Limsup_within_UNIV:
  2.2899 +  fixes f :: "'a::metric_space => extreal"
  2.2900 +  shows "Limsup (at x) f = Limsup (at x within UNIV) f"
  2.2901 +by (metis within_UNIV)
  2.2902 +
  2.2903 +
  2.2904 +lemma Limsup_at:
  2.2905 +  fixes f :: "'a::metric_space => extreal"
  2.2906 +  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
  2.2907 +using Limsup_within[of x UNIV f] Limsup_within_UNIV[of x f] by auto
  2.2908 +
  2.2909 +lemma Lim_within_constant:
  2.2910 +  fixes f :: "'a::metric_space => 'b::topological_space"
  2.2911 +  assumes "ALL y:S. f y = C"
  2.2912 +  shows "(f ---> C) (at x within S)"
  2.2913 +unfolding tendsto_def eventually_within
  2.2914 +by (metis assms(1) linorder_le_less_linear n_not_Suc_n real_of_nat_le_zero_cancel_iff)
  2.2915 +
  2.2916 +lemma Liminf_within_constant:
  2.2917 +  fixes f :: "'a::metric_space => extreal"
  2.2918 +  assumes "ALL y:S. f y = C"
  2.2919 +  assumes "~trivial_limit (at x within S)"
  2.2920 +  shows "Liminf (at x within S) f = C"
  2.2921 +by (metis Lim_within_constant assms lim_imp_Liminf)
  2.2922 +
  2.2923 +lemma Limsup_within_constant:
  2.2924 +  fixes f :: "'a::metric_space => extreal"
  2.2925 +  assumes "ALL y:S. f y = C"
  2.2926 +  assumes "~trivial_limit (at x within S)"
  2.2927 +  shows "Limsup (at x within S) f = C"
  2.2928 +by (metis Lim_within_constant assms lim_imp_Limsup)
  2.2929 +
  2.2930 +lemma islimpt_punctured:
  2.2931 +"x islimpt S = x islimpt (S-{x})"
  2.2932 +unfolding islimpt_def by blast
  2.2933 +
  2.2934 +
  2.2935 +lemma islimpt_in_closure:
  2.2936 +"(x islimpt S) = (x:closure(S-{x}))"
  2.2937 +unfolding closure_def using islimpt_punctured by blast
  2.2938 +
  2.2939 +
  2.2940 +lemma not_trivial_limit_within:
  2.2941 +  "~trivial_limit (at x within S) = (x:closure(S-{x}))"
  2.2942 +using islimpt_in_closure by (metis trivial_limit_within)
  2.2943 +
  2.2944 +
  2.2945 +lemma not_trivial_limit_within_ball:
  2.2946 +  "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"
  2.2947 +  (is "?lhs = ?rhs")
  2.2948 +proof-
  2.2949 +{ assume "?lhs"
  2.2950 +  { fix e :: real assume "e>0"
  2.2951 +    then obtain y where "y:(S-{x}) & dist y x < e"
  2.2952 +       using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
  2.2953 +    hence "y : (S Int ball x e - {x})" unfolding ball_def by (simp add: dist_commute)
  2.2954 +    hence "S Int ball x e - {x} ~= {}" by blast
  2.2955 +  } hence "?rhs" by auto
  2.2956 +}
  2.2957 +moreover
  2.2958 +{ assume "?rhs"
  2.2959 +  { fix e :: real assume "e>0"
  2.2960 +    then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
  2.2961 +    hence "y:(S-{x}) & dist y x < e" unfolding ball_def by (simp add: dist_commute)
  2.2962 +    hence "EX y:(S-{x}). dist y x < e" by auto
  2.2963 +  } hence "?lhs" using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
  2.2964 +} ultimately show ?thesis by auto
  2.2965 +qed
  2.2966 +
  2.2967 +subsubsection {* Continuity *}
  2.2968 +
  2.2969 +lemma continuous_imp_tendsto:
  2.2970 +  assumes "continuous (at x0) f"
  2.2971 +  assumes "x ----> x0"
  2.2972 +  shows "(f o x) ----> (f x0)"
  2.2973 +proof-
  2.2974 +{ fix S assume "open S & (f x0):S"
  2.2975 +  from this obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"
  2.2976 +     using assms continuous_at_open by metis
  2.2977 +  hence "(EX N. ALL n>=N. x n : T)" using assms tendsto_explicit T_def by auto
  2.2978 +  hence "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto
  2.2979 +} from this show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto
  2.2980 +qed
  2.2981 +
  2.2982 +
  2.2983 +lemma continuous_at_sequentially2:
  2.2984 +fixes f :: "'a::metric_space => 'b:: topological_space"
  2.2985 +shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"
  2.2986 +proof-
  2.2987 +{ assume "~(continuous (at x0) f)"
  2.2988 +  from this obtain T where T_def:
  2.2989 +     "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"
  2.2990 +     using continuous_at_open[of x0 f] by metis
  2.2991 +  def X == "{x'. f x' ~: T}" hence "x0 islimpt X" unfolding islimpt_def using T_def by auto
  2.2992 +  from this obtain x where x_def: "(ALL n. x n : X) & x ----> x0"
  2.2993 +     using islimpt_sequential[of x0 X] by auto
  2.2994 +  hence "~(f o x) ----> (f x0)" unfolding tendsto_explicit using X_def T_def by auto
  2.2995 +  hence "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto
  2.2996 +}
  2.2997 +from this show ?thesis using continuous_imp_tendsto by auto
  2.2998 +qed
  2.2999 +
  2.3000 +
  2.3001 +lemma continuous_at_extreal:
  2.3002 +fixes x0 :: real
  2.3003 +shows "continuous (at x0) extreal"
  2.3004 +proof-
  2.3005 +{ fix T assume T_def: "open T & extreal x0 : T"
  2.3006 +  from this obtain S where S_def: "open S & extreal ` S = T - {\<infinity>, (-\<infinity>)}"
  2.3007 +     using extreal_openE[of T] by metis
  2.3008 +  moreover hence "x0 : S" using T_def by auto
  2.3009 +  moreover have "ALL y:S. extreal y : T" using S_def by auto
  2.3010 +  ultimately have "EX S. x0 : S & open S & (ALL y:S. extreal y : T)" by auto
  2.3011 +} from this show ?thesis unfolding continuous_at_open by blast
  2.3012 +qed
  2.3013 +
  2.3014 +
  2.3015 +lemma continuous_at_of_extreal:
  2.3016 +fixes x0 :: extreal
  2.3017 +assumes "x0 ~: {\<infinity>, (-\<infinity>)}"
  2.3018 +shows "continuous (at x0) real"
  2.3019 +proof-
  2.3020 +{ fix T assume T_def: "open T & real x0 : T"
  2.3021 +  def S == "extreal ` T"
  2.3022 +  hence "extreal (real x0) : S" using T_def by auto
  2.3023 +  hence "x0 : S" using assms extreal_real by auto
  2.3024 +  moreover have "open S" using open_extreal S_def T_def by auto
  2.3025 +  moreover have "ALL y:S. real y : T" using S_def T_def by auto
  2.3026 +  ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto
  2.3027 +} from this show ?thesis unfolding continuous_at_open by blast
  2.3028 +qed
  2.3029 +
  2.3030 +
  2.3031 +lemma real_extreal_id: "real o extreal = id"
  2.3032 +proof-
  2.3033 +{ fix x have "(real o extreal) x = id x" by auto }
  2.3034 +from this show ?thesis using ext by blast
  2.3035 +qed
  2.3036 +
  2.3037 +
  2.3038 +lemma continuous_at_iff_extreal:
  2.3039 +fixes f :: "'a::t2_space => real"
  2.3040 +shows "continuous (at x0) f <-> continuous (at x0) (extreal o f)"
  2.3041 +proof-
  2.3042 +{ assume "continuous (at x0) f" hence "continuous (at x0) (extreal o f)"
  2.3043 +     using continuous_at_extreal continuous_at_compose[of x0 f extreal] by auto
  2.3044 +}
  2.3045 +moreover
  2.3046 +{ assume "continuous (at x0) (extreal o f)"
  2.3047 +  hence "continuous (at x0) (real o (extreal o f))"
  2.3048 +     using continuous_at_of_extreal by (intro continuous_at_compose[of x0 "extreal o f"]) auto
  2.3049 +  moreover have "real o (extreal o f) = f" using real_extreal_id by (simp add: o_assoc)
  2.3050 +  ultimately have "continuous (at x0) f" by auto
  2.3051 +} ultimately show ?thesis by auto
  2.3052 +qed
  2.3053 +
  2.3054 +
  2.3055 +lemma continuous_on_iff_extreal:
  2.3056 +fixes f :: "'a::t2_space => real"
  2.3057 +fixes A assumes "open A"
  2.3058 +shows "continuous_on A f <-> continuous_on A (extreal o f)"
  2.3059 +   using continuous_at_iff_extreal assms by (auto simp add: continuous_on_eq_continuous_at)
  2.3060 +
  2.3061 +
  2.3062 +lemma continuous_on_extreal: "continuous_on UNIV extreal"
  2.3063 +   using continuous_at_extreal continuous_on_eq_continuous_at by auto
  2.3064 +
  2.3065 +lemma open_image_extreal: "open(UNIV-{\<infinity>,(-\<infinity>)})"
  2.3066 +by (metis range_extreal open_extreal open_UNIV)
  2.3067 +
  2.3068 +lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>)}) real"
  2.3069 +   using continuous_at_of_extreal continuous_on_eq_continuous_at open_image_extreal by auto
  2.3070 +
  2.3071 +
  2.3072 +lemma continuous_on_iff_real:
  2.3073 +fixes f :: "'a::t2_space => extreal"
  2.3074 +assumes "ALL x. x:A --> (f x ~: {\<infinity>,(-\<infinity>)})"
  2.3075 +shows "continuous_on A f <-> continuous_on A (real o f)"
  2.3076 +proof-
  2.3077 +have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by auto
  2.3078 +hence *: "continuous_on (f ` A) real"
  2.3079 +   using continuous_on_real by (simp add: continuous_on_subset)
  2.3080 +have **: "continuous_on ((real o f) ` A) extreal"
  2.3081 +   using continuous_on_extreal continuous_on_subset[of "UNIV" "extreal" "(real o f) ` A"] by blast
  2.3082 +{ assume "continuous_on A f" hence "continuous_on A (real o f)"
  2.3083 +  apply (subst continuous_on_compose) using * by auto
  2.3084 +}
  2.3085 +moreover
  2.3086 +{ assume "continuous_on A (real o f)"
  2.3087 +  hence "continuous_on A (extreal o (real o f))"
  2.3088 +     apply (subst continuous_on_compose) using ** by auto
  2.3089 +  hence "continuous_on A f"
  2.3090 +     apply (subst continuous_on_eq[of A "extreal o (real o f)" f])
  2.3091 +     using assms extreal_real by auto
  2.3092 +}
  2.3093 +ultimately show ?thesis by auto
  2.3094 +qed
  2.3095 +
  2.3096 +
  2.3097 +lemma continuous_at_const:
  2.3098 +  fixes f :: "'a::t2_space => extreal"
  2.3099 +  assumes "ALL x. (f x = C)"
  2.3100 +  shows "ALL x. continuous (at x) f"
  2.3101 +unfolding continuous_at_open using assms t1_space by auto
  2.3102 +
  2.3103 +
  2.3104 +lemma closure_contains_Inf:
  2.3105 +  fixes S :: "real set"
  2.3106 +  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
  2.3107 +  shows "Inf S : closure S"
  2.3108 +proof-
  2.3109 +have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] assms by metis
  2.3110 +{ fix e assume "e>(0 :: real)"
  2.3111 +  from this obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto
  2.3112 +  moreover hence "x > Inf S - e" using * by auto
  2.3113 +  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
  2.3114 +  hence "EX x:S. abs (x - Inf S) < e" using x_def by auto
  2.3115 +} from this show ?thesis apply (subst closure_approachable) unfolding dist_norm by auto
  2.3116 +qed
  2.3117 +
  2.3118 +
  2.3119 +lemma closed_contains_Inf:
  2.3120 +  fixes S :: "real set"
  2.3121 +  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
  2.3122 +  assumes "closed S"
  2.3123 +  shows "Inf S : S"
  2.3124 +by (metis closure_contains_Inf closure_closed assms)
  2.3125 +
  2.3126 +
  2.3127 +lemma mono_closed_real:
  2.3128 +  fixes S :: "real set"
  2.3129 +  assumes mono: "ALL y z. y:S & y<=z --> z:S"
  2.3130 +  assumes "closed S"
  2.3131 +  shows "S = {} | S = UNIV | (EX a. S = {a ..})"
  2.3132 +proof-
  2.3133 +{ assume "S ~= {}"
  2.3134 +  { assume ex: "EX B. ALL x:S. B<=x"
  2.3135 +    hence *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis
  2.3136 +    hence "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
  2.3137 +    hence "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
  2.3138 +    hence "S = {Inf S ..}" by auto
  2.3139 +    hence "EX a. S = {a ..}" by auto
  2.3140 +  }
  2.3141 +  moreover
  2.3142 +  { assume "~(EX B. ALL x:S. B<=x)"
  2.3143 +    hence nex: "ALL B. EX x:S. x<B" by (simp add: not_le)
  2.3144 +    { fix y obtain x where "x:S & x < y" using nex by auto
  2.3145 +      hence "y:S" using mono[rule_format, of x y] by auto
  2.3146 +    } hence "S = UNIV" by auto
  2.3147 +  } ultimately have "S = UNIV | (EX a. S = {a ..})" by blast
  2.3148 +} from this show ?thesis by blast
  2.3149 +qed
  2.3150 +
  2.3151 +
  2.3152 +lemma mono_closed_extreal:
  2.3153 +  fixes S :: "real set"
  2.3154 +  assumes mono: "ALL y z. y:S & y<=z --> z:S"
  2.3155 +  assumes "closed S"
  2.3156 +  shows "EX a. S = {x. a <= extreal x}"
  2.3157 +proof-
  2.3158 +{ assume "S = {}" hence ?thesis apply(rule_tac x=PInfty in exI) by auto }
  2.3159 +moreover
  2.3160 +{ assume "S = UNIV" hence ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto }
  2.3161 +moreover
  2.3162 +{ assume "EX a. S = {a ..}"
  2.3163 +  from this obtain a where "S={a ..}" by auto
  2.3164 +  hence ?thesis apply(rule_tac x="extreal a" in exI) by auto
  2.3165 +} ultimately show ?thesis using mono_closed_real[of S] assms by auto
  2.3166 +qed
  2.3167 +
  2.3168 +lemma extreal_le_distrib:
  2.3169 +  fixes a b c :: extreal shows "c * (a + b) \<le> c * a + c * b"
  2.3170 +  by (cases rule: extreal3_cases[of a b c])
  2.3171 +     (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2.3172 +
  2.3173 +lemma extreal_pos_distrib:
  2.3174 +  fixes a b c :: extreal assumes "0 \<le> c" "c \<noteq> \<infinity>" shows "c * (a + b) = c * a + c * b"
  2.3175 +  using assms by (cases rule: extreal3_cases[of a b c])
  2.3176 +                 (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
  2.3177 +
  2.3178 +lemma extreal_pos_le_distrib:
  2.3179 +fixes a b c :: extreal
  2.3180 +assumes "c>=0"
  2.3181 +shows "c * (a + b) <= c * a + c * b"
  2.3182 +  using assms by (cases rule: extreal3_cases[of a b c])
  2.3183 +                 (auto simp add: field_simps)
  2.3184 +
  2.3185 +lemma extreal_max_mono:
  2.3186 +  "[| (a::extreal) <= b; c <= d |] ==> max a c <= max b d"
  2.3187 +  by (metis sup_extreal_def sup_mono)
  2.3188 +
  2.3189 +
  2.3190 +lemma extreal_max_least:
  2.3191 +  "[| (a::extreal) <= x; c <= x |] ==> max a c <= x"
  2.3192 +  by (metis sup_extreal_def sup_least)
  2.3193 +
  2.3194 +end