reorganized Extended_Real
authorhoelzl
Thu Jul 23 16:39:10 2015 +0200 (2015-07-23)
changeset 607718558e4a37b48
parent 60770 240563fbf41d
child 60772 a0cfa9050fa8
reorganized Extended_Real
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Borel_Space.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jul 23 14:25:05 2015 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:39:10 2015 +0200
     1.3 @@ -1909,6 +1909,9 @@
     1.4    shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
     1.5    unfolding top_ereal_def[symmetric] by auto
     1.6  
     1.7 +lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
     1.8 +  by auto
     1.9 +
    1.10  lemma Sup_ereal_close:
    1.11    fixes e :: ereal
    1.12    assumes "0 < e"
    1.13 @@ -2803,9 +2806,6 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 -lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
    1.18 -  by auto
    1.19 -
    1.20  lemma sup_continuous_add[order_continuous_intros]:
    1.21    fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
    1.22    assumes nn: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" and cont: "sup_continuous f" "sup_continuous g"
    1.23 @@ -2832,6 +2832,747 @@
    1.24    by (rule sup_continuous_compose[OF _ f])
    1.25       (auto simp: sup_continuous_def ereal_of_enat_SUP)
    1.26  
    1.27 +subsubsection \<open>Sums\<close>
    1.28 +
    1.29 +lemma sums_ereal_positive:
    1.30 +  fixes f :: "nat \<Rightarrow> ereal"
    1.31 +  assumes "\<And>i. 0 \<le> f i"
    1.32 +  shows "f sums (SUP n. \<Sum>i<n. f i)"
    1.33 +proof -
    1.34 +  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
    1.35 +    using ereal_add_mono[OF _ assms]
    1.36 +    by (auto intro!: incseq_SucI)
    1.37 +  from LIMSEQ_SUP[OF this]
    1.38 +  show ?thesis unfolding sums_def
    1.39 +    by (simp add: atLeast0LessThan)
    1.40 +qed
    1.41 +
    1.42 +lemma summable_ereal_pos:
    1.43 +  fixes f :: "nat \<Rightarrow> ereal"
    1.44 +  assumes "\<And>i. 0 \<le> f i"
    1.45 +  shows "summable f"
    1.46 +  using sums_ereal_positive[of f, OF assms]
    1.47 +  unfolding summable_def
    1.48 +  by auto
    1.49 +
    1.50 +lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
    1.51 +  unfolding sums_def by simp
    1.52 +
    1.53 +lemma suminf_ereal_eq_SUP:
    1.54 +  fixes f :: "nat \<Rightarrow> ereal"
    1.55 +  assumes "\<And>i. 0 \<le> f i"
    1.56 +  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
    1.57 +  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
    1.58 +  by simp
    1.59 +
    1.60 +lemma suminf_bound:
    1.61 +  fixes f :: "nat \<Rightarrow> ereal"
    1.62 +  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
    1.63 +    and pos: "\<And>n. 0 \<le> f n"
    1.64 +  shows "suminf f \<le> x"
    1.65 +proof (rule Lim_bounded_ereal)
    1.66 +  have "summable f" using pos[THEN summable_ereal_pos] .
    1.67 +  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
    1.68 +    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
    1.69 +  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
    1.70 +    using assms by auto
    1.71 +qed
    1.72 +
    1.73 +lemma suminf_bound_add:
    1.74 +  fixes f :: "nat \<Rightarrow> ereal"
    1.75 +  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
    1.76 +    and pos: "\<And>n. 0 \<le> f n"
    1.77 +    and "y \<noteq> -\<infinity>"
    1.78 +  shows "suminf f + y \<le> x"
    1.79 +proof (cases y)
    1.80 +  case (real r)
    1.81 +  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
    1.82 +    using assms by (simp add: ereal_le_minus)
    1.83 +  then have "(\<Sum> n. f n) \<le> x - y"
    1.84 +    using pos by (rule suminf_bound)
    1.85 +  then show "(\<Sum> n. f n) + y \<le> x"
    1.86 +    using assms real by (simp add: ereal_le_minus)
    1.87 +qed (insert assms, auto)
    1.88 +
    1.89 +lemma suminf_upper:
    1.90 +  fixes f :: "nat \<Rightarrow> ereal"
    1.91 +  assumes "\<And>n. 0 \<le> f n"
    1.92 +  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
    1.93 +  unfolding suminf_ereal_eq_SUP [OF assms]
    1.94 +  by (auto intro: complete_lattice_class.SUP_upper)
    1.95 +
    1.96 +lemma suminf_0_le:
    1.97 +  fixes f :: "nat \<Rightarrow> ereal"
    1.98 +  assumes "\<And>n. 0 \<le> f n"
    1.99 +  shows "0 \<le> (\<Sum>n. f n)"
   1.100 +  using suminf_upper[of f 0, OF assms]
   1.101 +  by simp
   1.102 +
   1.103 +lemma suminf_le_pos:
   1.104 +  fixes f g :: "nat \<Rightarrow> ereal"
   1.105 +  assumes "\<And>N. f N \<le> g N"
   1.106 +    and "\<And>N. 0 \<le> f N"
   1.107 +  shows "suminf f \<le> suminf g"
   1.108 +proof (safe intro!: suminf_bound)
   1.109 +  fix n
   1.110 +  {
   1.111 +    fix N
   1.112 +    have "0 \<le> g N"
   1.113 +      using assms(2,1)[of N] by auto
   1.114 +  }
   1.115 +  have "setsum f {..<n} \<le> setsum g {..<n}"
   1.116 +    using assms by (auto intro: setsum_mono)
   1.117 +  also have "\<dots> \<le> suminf g"
   1.118 +    using \<open>\<And>N. 0 \<le> g N\<close>
   1.119 +    by (rule suminf_upper)
   1.120 +  finally show "setsum f {..<n} \<le> suminf g" .
   1.121 +qed (rule assms(2))
   1.122 +
   1.123 +lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
   1.124 +  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
   1.125 +  by (simp add: one_ereal_def)
   1.126 +
   1.127 +lemma suminf_add_ereal:
   1.128 +  fixes f g :: "nat \<Rightarrow> ereal"
   1.129 +  assumes "\<And>i. 0 \<le> f i"
   1.130 +    and "\<And>i. 0 \<le> g i"
   1.131 +  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
   1.132 +  apply (subst (1 2 3) suminf_ereal_eq_SUP)
   1.133 +  unfolding setsum.distrib
   1.134 +  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
   1.135 +  done
   1.136 +
   1.137 +lemma suminf_cmult_ereal:
   1.138 +  fixes f g :: "nat \<Rightarrow> ereal"
   1.139 +  assumes "\<And>i. 0 \<le> f i"
   1.140 +    and "0 \<le> a"
   1.141 +  shows "(\<Sum>i. a * f i) = a * suminf f"
   1.142 +  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
   1.143 +       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
   1.144 +       intro!: SUP_ereal_mult_left)
   1.145 +
   1.146 +lemma suminf_PInfty:
   1.147 +  fixes f :: "nat \<Rightarrow> ereal"
   1.148 +  assumes "\<And>i. 0 \<le> f i"
   1.149 +    and "suminf f \<noteq> \<infinity>"
   1.150 +  shows "f i \<noteq> \<infinity>"
   1.151 +proof -
   1.152 +  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
   1.153 +  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
   1.154 +    by auto
   1.155 +  then show ?thesis
   1.156 +    unfolding setsum_Pinfty by simp
   1.157 +qed
   1.158 +
   1.159 +lemma suminf_PInfty_fun:
   1.160 +  assumes "\<And>i. 0 \<le> f i"
   1.161 +    and "suminf f \<noteq> \<infinity>"
   1.162 +  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
   1.163 +proof -
   1.164 +  have "\<forall>i. \<exists>r. f i = ereal r"
   1.165 +  proof
   1.166 +    fix i
   1.167 +    show "\<exists>r. f i = ereal r"
   1.168 +      using suminf_PInfty[OF assms] assms(1)[of i]
   1.169 +      by (cases "f i") auto
   1.170 +  qed
   1.171 +  from choice[OF this] show ?thesis
   1.172 +    by auto
   1.173 +qed
   1.174 +
   1.175 +lemma summable_ereal:
   1.176 +  assumes "\<And>i. 0 \<le> f i"
   1.177 +    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   1.178 +  shows "summable f"
   1.179 +proof -
   1.180 +  have "0 \<le> (\<Sum>i. ereal (f i))"
   1.181 +    using assms by (intro suminf_0_le) auto
   1.182 +  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
   1.183 +    by (cases "\<Sum>i. ereal (f i)") auto
   1.184 +  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
   1.185 +  have "summable (\<lambda>x. ereal (f x))"
   1.186 +    using assms by auto
   1.187 +  from summable_sums[OF this]
   1.188 +  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
   1.189 +    by auto
   1.190 +  then show "summable f"
   1.191 +    unfolding r sums_ereal summable_def ..
   1.192 +qed
   1.193 +
   1.194 +lemma suminf_ereal:
   1.195 +  assumes "\<And>i. 0 \<le> f i"
   1.196 +    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   1.197 +  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
   1.198 +proof (rule sums_unique[symmetric])
   1.199 +  from summable_ereal[OF assms]
   1.200 +  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
   1.201 +    unfolding sums_ereal
   1.202 +    using assms
   1.203 +    by (intro summable_sums summable_ereal)
   1.204 +qed
   1.205 +
   1.206 +lemma suminf_ereal_minus:
   1.207 +  fixes f g :: "nat \<Rightarrow> ereal"
   1.208 +  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
   1.209 +    and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
   1.210 +  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
   1.211 +proof -
   1.212 +  {
   1.213 +    fix i
   1.214 +    have "0 \<le> f i"
   1.215 +      using ord[of i] by auto
   1.216 +  }
   1.217 +  moreover
   1.218 +  from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> f i\<close> fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
   1.219 +  from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> g i\<close> fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
   1.220 +  {
   1.221 +    fix i
   1.222 +    have "0 \<le> f i - g i"
   1.223 +      using ord[of i] by (auto simp: ereal_le_minus_iff)
   1.224 +  }
   1.225 +  moreover
   1.226 +  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
   1.227 +    using assms by (auto intro!: suminf_le_pos simp: field_simps)
   1.228 +  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
   1.229 +    using fin by auto
   1.230 +  ultimately show ?thesis
   1.231 +    using assms \<open>\<And>i. 0 \<le> f i\<close>
   1.232 +    apply simp
   1.233 +    apply (subst (1 2 3) suminf_ereal)
   1.234 +    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
   1.235 +    done
   1.236 +qed
   1.237 +
   1.238 +lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
   1.239 +proof -
   1.240 +  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
   1.241 +    by (rule suminf_upper) auto
   1.242 +  then show ?thesis
   1.243 +    by simp
   1.244 +qed
   1.245 +
   1.246 +lemma summable_real_of_ereal:
   1.247 +  fixes f :: "nat \<Rightarrow> ereal"
   1.248 +  assumes f: "\<And>i. 0 \<le> f i"
   1.249 +    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
   1.250 +  shows "summable (\<lambda>i. real (f i))"
   1.251 +proof (rule summable_def[THEN iffD2])
   1.252 +  have "0 \<le> (\<Sum>i. f i)"
   1.253 +    using assms by (auto intro: suminf_0_le)
   1.254 +  with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
   1.255 +    by (cases "(\<Sum>i. f i)") auto
   1.256 +  {
   1.257 +    fix i
   1.258 +    have "f i \<noteq> \<infinity>"
   1.259 +      using f by (intro suminf_PInfty[OF _ fin]) auto
   1.260 +    then have "\<bar>f i\<bar> \<noteq> \<infinity>"
   1.261 +      using f[of i] by auto
   1.262 +  }
   1.263 +  note fin = this
   1.264 +  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
   1.265 +    using f
   1.266 +    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
   1.267 +  also have "\<dots> = ereal r"
   1.268 +    using fin r by (auto simp: ereal_real)
   1.269 +  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
   1.270 +    by (auto simp: sums_ereal)
   1.271 +qed
   1.272 +
   1.273 +lemma suminf_SUP_eq:
   1.274 +  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
   1.275 +  assumes "\<And>i. incseq (\<lambda>n. f n i)"
   1.276 +    and "\<And>n i. 0 \<le> f n i"
   1.277 +  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
   1.278 +proof -
   1.279 +  {
   1.280 +    fix n :: nat
   1.281 +    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
   1.282 +      using assms
   1.283 +      by (auto intro!: SUP_ereal_setsum [symmetric])
   1.284 +  }
   1.285 +  note * = this
   1.286 +  show ?thesis
   1.287 +    using assms
   1.288 +    apply (subst (1 2) suminf_ereal_eq_SUP)
   1.289 +    unfolding *
   1.290 +    apply (auto intro!: SUP_upper2)
   1.291 +    apply (subst SUP_commute)
   1.292 +    apply rule
   1.293 +    done
   1.294 +qed
   1.295 +
   1.296 +lemma suminf_setsum_ereal:
   1.297 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
   1.298 +  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
   1.299 +  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
   1.300 +proof (cases "finite A")
   1.301 +  case True
   1.302 +  then show ?thesis
   1.303 +    using nonneg
   1.304 +    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
   1.305 +next
   1.306 +  case False
   1.307 +  then show ?thesis by simp
   1.308 +qed
   1.309 +
   1.310 +lemma suminf_ereal_eq_0:
   1.311 +  fixes f :: "nat \<Rightarrow> ereal"
   1.312 +  assumes nneg: "\<And>i. 0 \<le> f i"
   1.313 +  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
   1.314 +proof
   1.315 +  assume "(\<Sum>i. f i) = 0"
   1.316 +  {
   1.317 +    fix i
   1.318 +    assume "f i \<noteq> 0"
   1.319 +    with nneg have "0 < f i"
   1.320 +      by (auto simp: less_le)
   1.321 +    also have "f i = (\<Sum>j. if j = i then f i else 0)"
   1.322 +      by (subst suminf_finite[where N="{i}"]) auto
   1.323 +    also have "\<dots> \<le> (\<Sum>i. f i)"
   1.324 +      using nneg
   1.325 +      by (auto intro!: suminf_le_pos)
   1.326 +    finally have False
   1.327 +      using \<open>(\<Sum>i. f i) = 0\<close> by auto
   1.328 +  }
   1.329 +  then show "\<forall>i. f i = 0"
   1.330 +    by auto
   1.331 +qed simp
   1.332 +
   1.333 +lemma suminf_ereal_offset_le:
   1.334 +  fixes f :: "nat \<Rightarrow> ereal"
   1.335 +  assumes f: "\<And>i. 0 \<le> f i"
   1.336 +  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
   1.337 +proof -
   1.338 +  have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
   1.339 +    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
   1.340 +  moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
   1.341 +    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
   1.342 +  then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
   1.343 +    by (rule LIMSEQ_ignore_initial_segment)
   1.344 +  ultimately show ?thesis
   1.345 +  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
   1.346 +    fix n assume "k \<le> n"
   1.347 +    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
   1.348 +      by simp
   1.349 +    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
   1.350 +      by (subst setsum.reindex) auto
   1.351 +    also have "\<dots> \<le> setsum f {..<n + k}"
   1.352 +      by (intro setsum_mono3) (auto simp: f)
   1.353 +    finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
   1.354 +  qed
   1.355 +qed
   1.356 +
   1.357 +lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
   1.358 +  by (metis sums_ereal sums_unique)
   1.359 +
   1.360 +lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
   1.361 +  by (metis sums_ereal sums_unique summable_def)
   1.362 +
   1.363 +lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   1.364 +  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
   1.365 +
   1.366 +lemma suminf_ereal_finite_neg:
   1.367 +  assumes "summable f"
   1.368 +  shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
   1.369 +proof-
   1.370 +  from assms obtain x where "f sums x" by blast
   1.371 +  hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
   1.372 +  from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
   1.373 +  thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
   1.374 +qed
   1.375 +
   1.376 +
   1.377 +lemma convergent_limsup_cl:
   1.378 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   1.379 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
   1.380 +  by (auto simp: convergent_def limI lim_imp_Limsup)
   1.381 +
   1.382 +lemma lim_increasing_cl:
   1.383 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   1.384 +  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
   1.385 +proof
   1.386 +  show "f ----> (SUP n. f n)"
   1.387 +    using assms
   1.388 +    by (intro increasing_tendsto)
   1.389 +       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   1.390 +qed
   1.391 +
   1.392 +lemma lim_decreasing_cl:
   1.393 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   1.394 +  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
   1.395 +proof
   1.396 +  show "f ----> (INF n. f n)"
   1.397 +    using assms
   1.398 +    by (intro decreasing_tendsto)
   1.399 +       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   1.400 +qed
   1.401 +
   1.402 +lemma compact_complete_linorder:
   1.403 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   1.404 +  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
   1.405 +proof -
   1.406 +  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   1.407 +    using seq_monosub[of X]
   1.408 +    unfolding comp_def
   1.409 +    by auto
   1.410 +  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)"
   1.411 +    by (auto simp add: monoseq_def)
   1.412 +  then obtain l where "(X \<circ> r) ----> l"
   1.413 +     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   1.414 +     by auto
   1.415 +  then show ?thesis
   1.416 +    using \<open>subseq r\<close> by auto
   1.417 +qed
   1.418 +
   1.419 +lemma ereal_dense3:
   1.420 +  fixes x y :: ereal
   1.421 +  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
   1.422 +proof (cases x y rule: ereal2_cases, simp_all)
   1.423 +  fix r q :: real
   1.424 +  assume "r < q"
   1.425 +  from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
   1.426 +    by (fastforce simp: Rats_def)
   1.427 +next
   1.428 +  fix r :: real
   1.429 +  show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
   1.430 +    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
   1.431 +    by (auto simp: Rats_def)
   1.432 +qed
   1.433 +
   1.434 +lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
   1.435 +  using continuous_on_eq_continuous_within[of A ereal]
   1.436 +  by (auto intro: continuous_on_ereal continuous_on_id)
   1.437 +
   1.438 +lemma ereal_open_uminus:
   1.439 +  fixes S :: "ereal set"
   1.440 +  assumes "open S"
   1.441 +  shows "open (uminus ` S)"
   1.442 +  using \<open>open S\<close>[unfolded open_generated_order]
   1.443 +proof induct
   1.444 +  have "range uminus = (UNIV :: ereal set)"
   1.445 +    by (auto simp: image_iff ereal_uminus_eq_reorder)
   1.446 +  then show "open (range uminus :: ereal set)"
   1.447 +    by simp
   1.448 +qed (auto simp add: image_Union image_Int)
   1.449 +
   1.450 +lemma ereal_uminus_complement:
   1.451 +  fixes S :: "ereal set"
   1.452 +  shows "uminus ` (- S) = - uminus ` S"
   1.453 +  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
   1.454 +
   1.455 +lemma ereal_closed_uminus:
   1.456 +  fixes S :: "ereal set"
   1.457 +  assumes "closed S"
   1.458 +  shows "closed (uminus ` S)"
   1.459 +  using assms
   1.460 +  unfolding closed_def ereal_uminus_complement[symmetric]
   1.461 +  by (rule ereal_open_uminus)
   1.462 +
   1.463 +lemma ereal_open_affinity_pos:
   1.464 +  fixes S :: "ereal set"
   1.465 +  assumes "open S"
   1.466 +    and m: "m \<noteq> \<infinity>" "0 < m"
   1.467 +    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   1.468 +  shows "open ((\<lambda>x. m * x + t) ` S)"
   1.469 +proof -
   1.470 +  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
   1.471 +    using m t
   1.472 +    apply (intro open_vimage \<open>open S\<close>)
   1.473 +    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
   1.474 +                 tendsto_ident_at tendsto_add_left_ereal)
   1.475 +    apply auto
   1.476 +    done
   1.477 +  also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
   1.478 +    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
   1.479 +                       simp del: uminus_ereal.simps)
   1.480 +  also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
   1.481 +    using m t
   1.482 +    by (simp add: set_eq_iff image_iff)
   1.483 +       (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
   1.484 +              ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
   1.485 +  finally show ?thesis .
   1.486 +qed
   1.487 +
   1.488 +lemma ereal_open_affinity:
   1.489 +  fixes S :: "ereal set"
   1.490 +  assumes "open S"
   1.491 +    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
   1.492 +    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   1.493 +  shows "open ((\<lambda>x. m * x + t) ` S)"
   1.494 +proof cases
   1.495 +  assume "0 < m"
   1.496 +  then show ?thesis
   1.497 +    using ereal_open_affinity_pos[OF \<open>open S\<close> _ _ t, of m] m
   1.498 +    by auto
   1.499 +next
   1.500 +  assume "\<not> 0 < m" then
   1.501 +  have "0 < -m"
   1.502 +    using \<open>m \<noteq> 0\<close>
   1.503 +    by (cases m) auto
   1.504 +  then have m: "-m \<noteq> \<infinity>" "0 < -m"
   1.505 +    using \<open>\<bar>m\<bar> \<noteq> \<infinity>\<close>
   1.506 +    by (auto simp: ereal_uminus_eq_reorder)
   1.507 +  from ereal_open_affinity_pos[OF ereal_open_uminus[OF \<open>open S\<close>] m t] show ?thesis
   1.508 +    unfolding image_image by simp
   1.509 +qed
   1.510 +
   1.511 +lemma open_uminus_iff:
   1.512 +  fixes S :: "ereal set"
   1.513 +  shows "open (uminus ` S) \<longleftrightarrow> open S"
   1.514 +  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
   1.515 +  by auto
   1.516 +
   1.517 +lemma ereal_Liminf_uminus:
   1.518 +  fixes f :: "'a \<Rightarrow> ereal"
   1.519 +  shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
   1.520 +  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
   1.521 +
   1.522 +lemma Liminf_PInfty:
   1.523 +  fixes f :: "'a \<Rightarrow> ereal"
   1.524 +  assumes "\<not> trivial_limit net"
   1.525 +  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
   1.526 +  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
   1.527 +  using Liminf_le_Limsup[OF assms, of f]
   1.528 +  by auto
   1.529 +
   1.530 +lemma Limsup_MInfty:
   1.531 +  fixes f :: "'a \<Rightarrow> ereal"
   1.532 +  assumes "\<not> trivial_limit net"
   1.533 +  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
   1.534 +  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
   1.535 +  using Liminf_le_Limsup[OF assms, of f]
   1.536 +  by auto
   1.537 +
   1.538 +lemma convergent_ereal:
   1.539 +  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   1.540 +  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   1.541 +  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   1.542 +  by (auto simp: convergent_def)
   1.543 +
   1.544 +lemma limsup_le_liminf_real:
   1.545 +  fixes X :: "nat \<Rightarrow> real" and L :: real
   1.546 +  assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
   1.547 +  shows "X ----> L"
   1.548 +proof -
   1.549 +  from 1 2 have "limsup X \<le> liminf X" by auto
   1.550 +  hence 3: "limsup X = liminf X"  
   1.551 +    apply (subst eq_iff, rule conjI)
   1.552 +    by (rule Liminf_le_Limsup, auto)
   1.553 +  hence 4: "convergent (\<lambda>n. ereal (X n))"
   1.554 +    by (subst convergent_ereal)
   1.555 +  hence "limsup X = lim (\<lambda>n. ereal(X n))"
   1.556 +    by (rule convergent_limsup_cl)
   1.557 +  also from 1 2 3 have "limsup X = L" by auto
   1.558 +  finally have "lim (\<lambda>n. ereal(X n)) = L" ..
   1.559 +  hence "(\<lambda>n. ereal (X n)) ----> L"
   1.560 +    apply (elim subst)
   1.561 +    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
   1.562 +  thus ?thesis by simp
   1.563 +qed
   1.564 +
   1.565 +lemma liminf_PInfty:
   1.566 +  fixes X :: "nat \<Rightarrow> ereal"
   1.567 +  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
   1.568 +  by (metis Liminf_PInfty trivial_limit_sequentially)
   1.569 +
   1.570 +lemma limsup_MInfty:
   1.571 +  fixes X :: "nat \<Rightarrow> ereal"
   1.572 +  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   1.573 +  by (metis Limsup_MInfty trivial_limit_sequentially)
   1.574 +
   1.575 +lemma ereal_lim_mono:
   1.576 +  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
   1.577 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
   1.578 +    and "X ----> x"
   1.579 +    and "Y ----> y"
   1.580 +  shows "x \<le> y"
   1.581 +  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   1.582 +
   1.583 +lemma incseq_le_ereal:
   1.584 +  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
   1.585 +  assumes inc: "incseq X"
   1.586 +    and lim: "X ----> L"
   1.587 +  shows "X N \<le> L"
   1.588 +  using inc
   1.589 +  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
   1.590 +
   1.591 +lemma decseq_ge_ereal:
   1.592 +  assumes dec: "decseq X"
   1.593 +    and lim: "X ----> (L::'a::linorder_topology)"
   1.594 +  shows "X N \<ge> L"
   1.595 +  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   1.596 +
   1.597 +lemma bounded_abs:
   1.598 +  fixes a :: real
   1.599 +  assumes "a \<le> x"
   1.600 +    and "x \<le> b"
   1.601 +  shows "abs x \<le> max (abs a) (abs b)"
   1.602 +  by (metis abs_less_iff assms leI le_max_iff_disj
   1.603 +    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   1.604 +
   1.605 +lemma ereal_Sup_lim:
   1.606 +  fixes a :: "'a::{complete_linorder,linorder_topology}"
   1.607 +  assumes "\<And>n. b n \<in> s"
   1.608 +    and "b ----> a"
   1.609 +  shows "a \<le> Sup s"
   1.610 +  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
   1.611 +
   1.612 +lemma ereal_Inf_lim:
   1.613 +  fixes a :: "'a::{complete_linorder,linorder_topology}"
   1.614 +  assumes "\<And>n. b n \<in> s"
   1.615 +    and "b ----> a"
   1.616 +  shows "Inf s \<le> a"
   1.617 +  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   1.618 +
   1.619 +lemma SUP_Lim_ereal:
   1.620 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   1.621 +  assumes inc: "incseq X"
   1.622 +    and l: "X ----> l"
   1.623 +  shows "(SUP n. X n) = l"
   1.624 +  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
   1.625 +  by simp
   1.626 +
   1.627 +lemma INF_Lim_ereal:
   1.628 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   1.629 +  assumes dec: "decseq X"
   1.630 +    and l: "X ----> l"
   1.631 +  shows "(INF n. X n) = l"
   1.632 +  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
   1.633 +  by simp
   1.634 +
   1.635 +lemma SUP_eq_LIMSEQ:
   1.636 +  assumes "mono f"
   1.637 +  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
   1.638 +proof
   1.639 +  have inc: "incseq (\<lambda>i. ereal (f i))"
   1.640 +    using \<open>mono f\<close> unfolding mono_def incseq_def by auto
   1.641 +  {
   1.642 +    assume "f ----> x"
   1.643 +    then have "(\<lambda>i. ereal (f i)) ----> ereal x"
   1.644 +      by auto
   1.645 +    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
   1.646 +  next
   1.647 +    assume "(SUP n. ereal (f n)) = ereal x"
   1.648 +    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
   1.649 +  }
   1.650 +qed
   1.651 +
   1.652 +lemma liminf_ereal_cminus:
   1.653 +  fixes f :: "nat \<Rightarrow> ereal"
   1.654 +  assumes "c \<noteq> -\<infinity>"
   1.655 +  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
   1.656 +proof (cases c)
   1.657 +  case PInf
   1.658 +  then show ?thesis
   1.659 +    by (simp add: Liminf_const)
   1.660 +next
   1.661 +  case (real r)
   1.662 +  then show ?thesis
   1.663 +    unfolding liminf_SUP_INF limsup_INF_SUP
   1.664 +    apply (subst INF_ereal_minus_right)
   1.665 +    apply auto
   1.666 +    apply (subst SUP_ereal_minus_right)
   1.667 +    apply auto
   1.668 +    done
   1.669 +qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
   1.670 +
   1.671 +
   1.672 +subsubsection \<open>Continuity\<close>
   1.673 +
   1.674 +lemma continuous_at_of_ereal:
   1.675 +  "\<bar>x0 :: ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous (at x0) real"
   1.676 +  unfolding continuous_at
   1.677 +  by (rule lim_real_of_ereal) (simp add: ereal_real)
   1.678 +
   1.679 +lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
   1.680 +  by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
   1.681 +
   1.682 +lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
   1.683 +  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   1.684 +
   1.685 +lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
   1.686 +  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   1.687 +
   1.688 +lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
   1.689 +  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   1.690 +
   1.691 +lemma
   1.692 +  shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
   1.693 +    and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
   1.694 +  unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
   1.695 +    eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
   1.696 +  by (auto simp add: ereal_all_split ereal_ex_split)
   1.697 +
   1.698 +lemma ereal_tendsto_simps1:
   1.699 +  "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
   1.700 +  "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
   1.701 +  "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
   1.702 +  "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
   1.703 +  unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
   1.704 +  by (auto simp: filtermap_filtermap filtermap_ident)
   1.705 +
   1.706 +lemma ereal_tendsto_simps2:
   1.707 +  "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
   1.708 +  "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
   1.709 +  "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
   1.710 +  unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
   1.711 +  using lim_ereal by (simp_all add: comp_def)
   1.712 +
   1.713 +lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
   1.714 +
   1.715 +lemma continuous_at_iff_ereal:
   1.716 +  fixes f :: "'a::t2_space \<Rightarrow> real"
   1.717 +  shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
   1.718 +  unfolding continuous_within comp_def lim_ereal ..
   1.719 +
   1.720 +lemma continuous_on_iff_ereal:
   1.721 +  fixes f :: "'a::t2_space => real"
   1.722 +  assumes "open A"
   1.723 +  shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
   1.724 +  unfolding continuous_on_def comp_def lim_ereal ..
   1.725 +
   1.726 +lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
   1.727 +  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
   1.728 +  by auto
   1.729 +
   1.730 +lemma continuous_on_iff_real:
   1.731 +  fixes f :: "'a::t2_space \<Rightarrow> ereal"
   1.732 +  assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   1.733 +  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
   1.734 +proof -
   1.735 +  have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
   1.736 +    using assms by force
   1.737 +  then have *: "continuous_on (f ` A) real"
   1.738 +    using continuous_on_real by (simp add: continuous_on_subset)
   1.739 +  have **: "continuous_on ((real \<circ> f) ` A) ereal"
   1.740 +    by (intro continuous_on_ereal continuous_on_id)
   1.741 +  {
   1.742 +    assume "continuous_on A f"
   1.743 +    then have "continuous_on A (real \<circ> f)"
   1.744 +      apply (subst continuous_on_compose)
   1.745 +      using *
   1.746 +      apply auto
   1.747 +      done
   1.748 +  }
   1.749 +  moreover
   1.750 +  {
   1.751 +    assume "continuous_on A (real \<circ> f)"
   1.752 +    then have "continuous_on A (ereal \<circ> (real \<circ> f))"
   1.753 +      apply (subst continuous_on_compose)
   1.754 +      using **
   1.755 +      apply auto
   1.756 +      done
   1.757 +    then have "continuous_on A f"
   1.758 +      apply (subst continuous_on_cong[of _ A _ "ereal \<circ> (real \<circ> f)"])
   1.759 +      using assms ereal_real
   1.760 +      apply auto
   1.761 +      done
   1.762 +  }
   1.763 +  ultimately show ?thesis
   1.764 +    by auto
   1.765 +qed
   1.766 +
   1.767 +
   1.768  subsubsection \<open>Tests for code generator\<close>
   1.769  
   1.770  (* A small list of simple arithmetic expressions *)
     2.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jul 23 14:25:05 2015 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jul 23 16:39:10 2015 +0200
     2.3 @@ -11,48 +11,6 @@
     2.4    imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
     2.5  begin
     2.6  
     2.7 -lemma convergent_limsup_cl:
     2.8 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
     2.9 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
    2.10 -  by (auto simp: convergent_def limI lim_imp_Limsup)
    2.11 -
    2.12 -lemma lim_increasing_cl:
    2.13 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
    2.14 -  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
    2.15 -proof
    2.16 -  show "f ----> (SUP n. f n)"
    2.17 -    using assms
    2.18 -    by (intro increasing_tendsto)
    2.19 -       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
    2.20 -qed
    2.21 -
    2.22 -lemma lim_decreasing_cl:
    2.23 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
    2.24 -  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
    2.25 -proof
    2.26 -  show "f ----> (INF n. f n)"
    2.27 -    using assms
    2.28 -    by (intro decreasing_tendsto)
    2.29 -       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
    2.30 -qed
    2.31 -
    2.32 -lemma compact_complete_linorder:
    2.33 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
    2.34 -  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
    2.35 -proof -
    2.36 -  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
    2.37 -    using seq_monosub[of X]
    2.38 -    unfolding comp_def
    2.39 -    by auto
    2.40 -  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.41 -    by (auto simp add: monoseq_def)
    2.42 -  then obtain l where "(X \<circ> r) ----> l"
    2.43 -     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
    2.44 -     by auto
    2.45 -  then show ?thesis
    2.46 -    using \<open>subseq r\<close> by auto
    2.47 -qed
    2.48 -
    2.49  lemma compact_UNIV:
    2.50    "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
    2.51    using compact_complete_linorder
    2.52 @@ -94,21 +52,6 @@
    2.53      by simp
    2.54  qed
    2.55  
    2.56 -lemma ereal_dense3:
    2.57 -  fixes x y :: ereal
    2.58 -  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
    2.59 -proof (cases x y rule: ereal2_cases, simp_all)
    2.60 -  fix r q :: real
    2.61 -  assume "r < q"
    2.62 -  from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
    2.63 -    by (fastforce simp: Rats_def)
    2.64 -next
    2.65 -  fix r :: real
    2.66 -  show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
    2.67 -    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
    2.68 -    by (auto simp: Rats_def)
    2.69 -qed
    2.70 -
    2.71  instance ereal :: second_countable_topology
    2.72  proof (default, intro exI conjI)
    2.73    let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
    2.74 @@ -139,43 +82,6 @@
    2.75    qed
    2.76  qed
    2.77  
    2.78 -lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
    2.79 -  unfolding continuous_on_topological open_ereal_def
    2.80 -  by auto
    2.81 -
    2.82 -lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
    2.83 -  using continuous_on_eq_continuous_at[of UNIV]
    2.84 -  by auto
    2.85 -
    2.86 -lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
    2.87 -  using continuous_on_eq_continuous_within[of A]
    2.88 -  by auto
    2.89 -
    2.90 -lemma ereal_open_uminus:
    2.91 -  fixes S :: "ereal set"
    2.92 -  assumes "open S"
    2.93 -  shows "open (uminus ` S)"
    2.94 -  using \<open>open S\<close>[unfolded open_generated_order]
    2.95 -proof induct
    2.96 -  have "range uminus = (UNIV :: ereal set)"
    2.97 -    by (auto simp: image_iff ereal_uminus_eq_reorder)
    2.98 -  then show "open (range uminus :: ereal set)"
    2.99 -    by simp
   2.100 -qed (auto simp add: image_Union image_Int)
   2.101 -
   2.102 -lemma ereal_uminus_complement:
   2.103 -  fixes S :: "ereal set"
   2.104 -  shows "uminus ` (- S) = - uminus ` S"
   2.105 -  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
   2.106 -
   2.107 -lemma ereal_closed_uminus:
   2.108 -  fixes S :: "ereal set"
   2.109 -  assumes "closed S"
   2.110 -  shows "closed (uminus ` S)"
   2.111 -  using assms
   2.112 -  unfolding closed_def ereal_uminus_complement[symmetric]
   2.113 -  by (rule ereal_open_uminus)
   2.114 -
   2.115  lemma ereal_open_closed_aux:
   2.116    fixes S :: "ereal set"
   2.117    assumes "open S"
   2.118 @@ -185,6 +91,7 @@
   2.119  proof (rule ccontr)
   2.120    assume "\<not> ?thesis"
   2.121    then have *: "Inf S \<in> S"
   2.122 +    
   2.123      by (metis assms(2) closed_contains_Inf_cl)
   2.124    {
   2.125      assume "Inf S = -\<infinity>"
   2.126 @@ -243,54 +150,6 @@
   2.127      by auto
   2.128  qed
   2.129  
   2.130 -lemma ereal_open_affinity_pos:
   2.131 -  fixes S :: "ereal set"
   2.132 -  assumes "open S"
   2.133 -    and m: "m \<noteq> \<infinity>" "0 < m"
   2.134 -    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   2.135 -  shows "open ((\<lambda>x. m * x + t) ` S)"
   2.136 -proof -
   2.137 -  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
   2.138 -    using m t
   2.139 -    apply (intro open_vimage \<open>open S\<close>)
   2.140 -    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
   2.141 -                 tendsto_ident_at tendsto_add_left_ereal)
   2.142 -    apply auto
   2.143 -    done
   2.144 -  also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
   2.145 -    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
   2.146 -                       simp del: uminus_ereal.simps)
   2.147 -  also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
   2.148 -    using m t
   2.149 -    by (simp add: set_eq_iff image_iff)
   2.150 -       (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
   2.151 -              ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
   2.152 -  finally show ?thesis .
   2.153 -qed
   2.154 -
   2.155 -lemma ereal_open_affinity:
   2.156 -  fixes S :: "ereal set"
   2.157 -  assumes "open S"
   2.158 -    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
   2.159 -    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   2.160 -  shows "open ((\<lambda>x. m * x + t) ` S)"
   2.161 -proof cases
   2.162 -  assume "0 < m"
   2.163 -  then show ?thesis
   2.164 -    using ereal_open_affinity_pos[OF \<open>open S\<close> _ _ t, of m] m
   2.165 -    by auto
   2.166 -next
   2.167 -  assume "\<not> 0 < m" then
   2.168 -  have "0 < -m"
   2.169 -    using \<open>m \<noteq> 0\<close>
   2.170 -    by (cases m) auto
   2.171 -  then have m: "-m \<noteq> \<infinity>" "0 < -m"
   2.172 -    using \<open>\<bar>m\<bar> \<noteq> \<infinity>\<close>
   2.173 -    by (auto simp: ereal_uminus_eq_reorder)
   2.174 -  from ereal_open_affinity_pos[OF ereal_open_uminus[OF \<open>open S\<close>] m t] show ?thesis
   2.175 -    unfolding image_image by simp
   2.176 -qed
   2.177 -
   2.178  lemma ereal_open_atLeast:
   2.179    fixes x :: ereal
   2.180    shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
   2.181 @@ -310,290 +169,6 @@
   2.182      by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
   2.183  qed
   2.184  
   2.185 -lemma open_uminus_iff:
   2.186 -  fixes S :: "ereal set"
   2.187 -  shows "open (uminus ` S) \<longleftrightarrow> open S"
   2.188 -  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
   2.189 -  by auto
   2.190 -
   2.191 -lemma ereal_Liminf_uminus:
   2.192 -  fixes f :: "'a \<Rightarrow> ereal"
   2.193 -  shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
   2.194 -  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
   2.195 -
   2.196 -lemma Liminf_PInfty:
   2.197 -  fixes f :: "'a \<Rightarrow> ereal"
   2.198 -  assumes "\<not> trivial_limit net"
   2.199 -  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
   2.200 -  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
   2.201 -  using Liminf_le_Limsup[OF assms, of f]
   2.202 -  by auto
   2.203 -
   2.204 -lemma Limsup_MInfty:
   2.205 -  fixes f :: "'a \<Rightarrow> ereal"
   2.206 -  assumes "\<not> trivial_limit net"
   2.207 -  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
   2.208 -  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
   2.209 -  using Liminf_le_Limsup[OF assms, of f]
   2.210 -  by auto
   2.211 -
   2.212 -lemma convergent_ereal:
   2.213 -  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
   2.214 -  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   2.215 -  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   2.216 -  by (auto simp: convergent_def)
   2.217 -
   2.218 -lemma limsup_le_liminf_real:
   2.219 -  fixes X :: "nat \<Rightarrow> real" and L :: real
   2.220 -  assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
   2.221 -  shows "X ----> L"
   2.222 -proof -
   2.223 -  from 1 2 have "limsup X \<le> liminf X" by auto
   2.224 -  hence 3: "limsup X = liminf X"  
   2.225 -    apply (subst eq_iff, rule conjI)
   2.226 -    by (rule Liminf_le_Limsup, auto)
   2.227 -  hence 4: "convergent (\<lambda>n. ereal (X n))"
   2.228 -    by (subst convergent_ereal)
   2.229 -  hence "limsup X = lim (\<lambda>n. ereal(X n))"
   2.230 -    by (rule convergent_limsup_cl)
   2.231 -  also from 1 2 3 have "limsup X = L" by auto
   2.232 -  finally have "lim (\<lambda>n. ereal(X n)) = L" ..
   2.233 -  hence "(\<lambda>n. ereal (X n)) ----> L"
   2.234 -    apply (elim subst)
   2.235 -    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
   2.236 -  thus ?thesis by simp
   2.237 -qed
   2.238 -
   2.239 -lemma liminf_PInfty:
   2.240 -  fixes X :: "nat \<Rightarrow> ereal"
   2.241 -  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
   2.242 -  by (metis Liminf_PInfty trivial_limit_sequentially)
   2.243 -
   2.244 -lemma limsup_MInfty:
   2.245 -  fixes X :: "nat \<Rightarrow> ereal"
   2.246 -  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   2.247 -  by (metis Limsup_MInfty trivial_limit_sequentially)
   2.248 -
   2.249 -lemma ereal_lim_mono:
   2.250 -  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
   2.251 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
   2.252 -    and "X ----> x"
   2.253 -    and "Y ----> y"
   2.254 -  shows "x \<le> y"
   2.255 -  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   2.256 -
   2.257 -lemma incseq_le_ereal:
   2.258 -  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
   2.259 -  assumes inc: "incseq X"
   2.260 -    and lim: "X ----> L"
   2.261 -  shows "X N \<le> L"
   2.262 -  using inc
   2.263 -  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
   2.264 -
   2.265 -lemma decseq_ge_ereal:
   2.266 -  assumes dec: "decseq X"
   2.267 -    and lim: "X ----> (L::'a::linorder_topology)"
   2.268 -  shows "X N \<ge> L"
   2.269 -  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   2.270 -
   2.271 -lemma bounded_abs:
   2.272 -  fixes a :: real
   2.273 -  assumes "a \<le> x"
   2.274 -    and "x \<le> b"
   2.275 -  shows "abs x \<le> max (abs a) (abs b)"
   2.276 -  by (metis abs_less_iff assms leI le_max_iff_disj
   2.277 -    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   2.278 -
   2.279 -lemma ereal_Sup_lim:
   2.280 -  fixes a :: "'a::{complete_linorder,linorder_topology}"
   2.281 -  assumes "\<And>n. b n \<in> s"
   2.282 -    and "b ----> a"
   2.283 -  shows "a \<le> Sup s"
   2.284 -  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
   2.285 -
   2.286 -lemma ereal_Inf_lim:
   2.287 -  fixes a :: "'a::{complete_linorder,linorder_topology}"
   2.288 -  assumes "\<And>n. b n \<in> s"
   2.289 -    and "b ----> a"
   2.290 -  shows "Inf s \<le> a"
   2.291 -  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   2.292 -
   2.293 -lemma SUP_Lim_ereal:
   2.294 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   2.295 -  assumes inc: "incseq X"
   2.296 -    and l: "X ----> l"
   2.297 -  shows "(SUP n. X n) = l"
   2.298 -  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
   2.299 -  by simp
   2.300 -
   2.301 -lemma INF_Lim_ereal:
   2.302 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   2.303 -  assumes dec: "decseq X"
   2.304 -    and l: "X ----> l"
   2.305 -  shows "(INF n. X n) = l"
   2.306 -  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
   2.307 -  by simp
   2.308 -
   2.309 -lemma SUP_eq_LIMSEQ:
   2.310 -  assumes "mono f"
   2.311 -  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
   2.312 -proof
   2.313 -  have inc: "incseq (\<lambda>i. ereal (f i))"
   2.314 -    using \<open>mono f\<close> unfolding mono_def incseq_def by auto
   2.315 -  {
   2.316 -    assume "f ----> x"
   2.317 -    then have "(\<lambda>i. ereal (f i)) ----> ereal x"
   2.318 -      by auto
   2.319 -    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
   2.320 -  next
   2.321 -    assume "(SUP n. ereal (f n)) = ereal x"
   2.322 -    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
   2.323 -  }
   2.324 -qed
   2.325 -
   2.326 -lemma liminf_ereal_cminus:
   2.327 -  fixes f :: "nat \<Rightarrow> ereal"
   2.328 -  assumes "c \<noteq> -\<infinity>"
   2.329 -  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
   2.330 -proof (cases c)
   2.331 -  case PInf
   2.332 -  then show ?thesis
   2.333 -    by (simp add: Liminf_const)
   2.334 -next
   2.335 -  case (real r)
   2.336 -  then show ?thesis
   2.337 -    unfolding liminf_SUP_INF limsup_INF_SUP
   2.338 -    apply (subst INF_ereal_minus_right)
   2.339 -    apply auto
   2.340 -    apply (subst SUP_ereal_minus_right)
   2.341 -    apply auto
   2.342 -    done
   2.343 -qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
   2.344 -
   2.345 -
   2.346 -subsubsection \<open>Continuity\<close>
   2.347 -
   2.348 -lemma continuous_at_of_ereal:
   2.349 -  fixes x0 :: ereal
   2.350 -  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
   2.351 -  shows "continuous (at x0) real"
   2.352 -proof -
   2.353 -  {
   2.354 -    fix T
   2.355 -    assume T: "open T" "real x0 \<in> T"
   2.356 -    def S \<equiv> "ereal ` T"
   2.357 -    then have "ereal (real x0) \<in> S"
   2.358 -      using T by auto
   2.359 -    then have "x0 \<in> S"
   2.360 -      using assms ereal_real by auto
   2.361 -    moreover have "open S"
   2.362 -      using open_ereal S_def T by auto
   2.363 -    moreover have "\<forall>y\<in>S. real y \<in> T"
   2.364 -      using S_def T by auto
   2.365 -    ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)"
   2.366 -      by auto
   2.367 -  }
   2.368 -  then show ?thesis
   2.369 -    unfolding continuous_at_open by blast
   2.370 -qed
   2.371 -
   2.372 -lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
   2.373 -  by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
   2.374 -
   2.375 -lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
   2.376 -  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   2.377 -
   2.378 -lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
   2.379 -  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   2.380 -
   2.381 -lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
   2.382 -  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
   2.383 -
   2.384 -lemma
   2.385 -  shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
   2.386 -    and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
   2.387 -  unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
   2.388 -    eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
   2.389 -  by (auto simp add: ereal_all_split ereal_ex_split)
   2.390 -
   2.391 -lemma ereal_tendsto_simps1:
   2.392 -  "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
   2.393 -  "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
   2.394 -  "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
   2.395 -  "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
   2.396 -  unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
   2.397 -  by (auto simp: filtermap_filtermap filtermap_ident)
   2.398 -
   2.399 -lemma ereal_tendsto_simps2:
   2.400 -  "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
   2.401 -  "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
   2.402 -  "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
   2.403 -  unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
   2.404 -  using lim_ereal by (simp_all add: comp_def)
   2.405 -
   2.406 -lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
   2.407 -
   2.408 -lemma continuous_at_iff_ereal:
   2.409 -  fixes f :: "'a::t2_space \<Rightarrow> real"
   2.410 -  shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
   2.411 -  unfolding continuous_within comp_def lim_ereal ..
   2.412 -
   2.413 -lemma continuous_on_iff_ereal:
   2.414 -  fixes f :: "'a::t2_space => real"
   2.415 -  assumes "open A"
   2.416 -  shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
   2.417 -  unfolding continuous_on_def comp_def lim_ereal ..
   2.418 -
   2.419 -lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
   2.420 -  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
   2.421 -  by auto
   2.422 -
   2.423 -lemma continuous_on_iff_real:
   2.424 -  fixes f :: "'a::t2_space \<Rightarrow> ereal"
   2.425 -  assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   2.426 -  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
   2.427 -proof -
   2.428 -  have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
   2.429 -    using assms by force
   2.430 -  then have *: "continuous_on (f ` A) real"
   2.431 -    using continuous_on_real by (simp add: continuous_on_subset)
   2.432 -  have **: "continuous_on ((real \<circ> f) ` A) ereal"
   2.433 -    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"]
   2.434 -    by blast
   2.435 -  {
   2.436 -    assume "continuous_on A f"
   2.437 -    then have "continuous_on A (real \<circ> f)"
   2.438 -      apply (subst continuous_on_compose)
   2.439 -      using *
   2.440 -      apply auto
   2.441 -      done
   2.442 -  }
   2.443 -  moreover
   2.444 -  {
   2.445 -    assume "continuous_on A (real \<circ> f)"
   2.446 -    then have "continuous_on A (ereal \<circ> (real \<circ> f))"
   2.447 -      apply (subst continuous_on_compose)
   2.448 -      using **
   2.449 -      apply auto
   2.450 -      done
   2.451 -    then have "continuous_on A f"
   2.452 -      apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f])
   2.453 -      using assms ereal_real
   2.454 -      apply auto
   2.455 -      done
   2.456 -  }
   2.457 -  ultimately show ?thesis
   2.458 -    by auto
   2.459 -qed
   2.460 -
   2.461 -lemma continuous_at_const:
   2.462 -  fixes f :: "'a::t2_space \<Rightarrow> ereal"
   2.463 -  assumes "\<forall>x. f x = C"
   2.464 -  shows "\<forall>x. continuous (at x) f"
   2.465 -  unfolding continuous_at_open
   2.466 -  using assms t1_space
   2.467 -  by auto
   2.468 -
   2.469  lemma mono_closed_real:
   2.470    fixes S :: "real set"
   2.471    assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
   2.472 @@ -675,313 +250,6 @@
   2.473      using mono_closed_real[of S] assms by auto
   2.474  qed
   2.475  
   2.476 -
   2.477 -subsection \<open>Sums\<close>
   2.478 -
   2.479 -lemma sums_ereal_positive:
   2.480 -  fixes f :: "nat \<Rightarrow> ereal"
   2.481 -  assumes "\<And>i. 0 \<le> f i"
   2.482 -  shows "f sums (SUP n. \<Sum>i<n. f i)"
   2.483 -proof -
   2.484 -  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
   2.485 -    using ereal_add_mono[OF _ assms]
   2.486 -    by (auto intro!: incseq_SucI)
   2.487 -  from LIMSEQ_SUP[OF this]
   2.488 -  show ?thesis unfolding sums_def
   2.489 -    by (simp add: atLeast0LessThan)
   2.490 -qed
   2.491 -
   2.492 -lemma summable_ereal_pos:
   2.493 -  fixes f :: "nat \<Rightarrow> ereal"
   2.494 -  assumes "\<And>i. 0 \<le> f i"
   2.495 -  shows "summable f"
   2.496 -  using sums_ereal_positive[of f, OF assms]
   2.497 -  unfolding summable_def
   2.498 -  by auto
   2.499 -
   2.500 -lemma suminf_ereal_eq_SUP:
   2.501 -  fixes f :: "nat \<Rightarrow> ereal"
   2.502 -  assumes "\<And>i. 0 \<le> f i"
   2.503 -  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
   2.504 -  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
   2.505 -  by simp
   2.506 -
   2.507 -lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
   2.508 -  unfolding sums_def by simp
   2.509 -
   2.510 -lemma suminf_bound:
   2.511 -  fixes f :: "nat \<Rightarrow> ereal"
   2.512 -  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
   2.513 -    and pos: "\<And>n. 0 \<le> f n"
   2.514 -  shows "suminf f \<le> x"
   2.515 -proof (rule Lim_bounded_ereal)
   2.516 -  have "summable f" using pos[THEN summable_ereal_pos] .
   2.517 -  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
   2.518 -    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
   2.519 -  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
   2.520 -    using assms by auto
   2.521 -qed
   2.522 -
   2.523 -lemma suminf_bound_add:
   2.524 -  fixes f :: "nat \<Rightarrow> ereal"
   2.525 -  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
   2.526 -    and pos: "\<And>n. 0 \<le> f n"
   2.527 -    and "y \<noteq> -\<infinity>"
   2.528 -  shows "suminf f + y \<le> x"
   2.529 -proof (cases y)
   2.530 -  case (real r)
   2.531 -  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
   2.532 -    using assms by (simp add: ereal_le_minus)
   2.533 -  then have "(\<Sum> n. f n) \<le> x - y"
   2.534 -    using pos by (rule suminf_bound)
   2.535 -  then show "(\<Sum> n. f n) + y \<le> x"
   2.536 -    using assms real by (simp add: ereal_le_minus)
   2.537 -qed (insert assms, auto)
   2.538 -
   2.539 -lemma suminf_upper:
   2.540 -  fixes f :: "nat \<Rightarrow> ereal"
   2.541 -  assumes "\<And>n. 0 \<le> f n"
   2.542 -  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
   2.543 -  unfolding suminf_ereal_eq_SUP [OF assms]
   2.544 -  by (auto intro: complete_lattice_class.SUP_upper)
   2.545 -
   2.546 -lemma suminf_0_le:
   2.547 -  fixes f :: "nat \<Rightarrow> ereal"
   2.548 -  assumes "\<And>n. 0 \<le> f n"
   2.549 -  shows "0 \<le> (\<Sum>n. f n)"
   2.550 -  using suminf_upper[of f 0, OF assms]
   2.551 -  by simp
   2.552 -
   2.553 -lemma suminf_le_pos:
   2.554 -  fixes f g :: "nat \<Rightarrow> ereal"
   2.555 -  assumes "\<And>N. f N \<le> g N"
   2.556 -    and "\<And>N. 0 \<le> f N"
   2.557 -  shows "suminf f \<le> suminf g"
   2.558 -proof (safe intro!: suminf_bound)
   2.559 -  fix n
   2.560 -  {
   2.561 -    fix N
   2.562 -    have "0 \<le> g N"
   2.563 -      using assms(2,1)[of N] by auto
   2.564 -  }
   2.565 -  have "setsum f {..<n} \<le> setsum g {..<n}"
   2.566 -    using assms by (auto intro: setsum_mono)
   2.567 -  also have "\<dots> \<le> suminf g"
   2.568 -    using \<open>\<And>N. 0 \<le> g N\<close>
   2.569 -    by (rule suminf_upper)
   2.570 -  finally show "setsum f {..<n} \<le> suminf g" .
   2.571 -qed (rule assms(2))
   2.572 -
   2.573 -lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
   2.574 -  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
   2.575 -  by (simp add: one_ereal_def)
   2.576 -
   2.577 -lemma suminf_add_ereal:
   2.578 -  fixes f g :: "nat \<Rightarrow> ereal"
   2.579 -  assumes "\<And>i. 0 \<le> f i"
   2.580 -    and "\<And>i. 0 \<le> g i"
   2.581 -  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
   2.582 -  apply (subst (1 2 3) suminf_ereal_eq_SUP)
   2.583 -  unfolding setsum.distrib
   2.584 -  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
   2.585 -  done
   2.586 -
   2.587 -lemma suminf_cmult_ereal:
   2.588 -  fixes f g :: "nat \<Rightarrow> ereal"
   2.589 -  assumes "\<And>i. 0 \<le> f i"
   2.590 -    and "0 \<le> a"
   2.591 -  shows "(\<Sum>i. a * f i) = a * suminf f"
   2.592 -  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
   2.593 -       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
   2.594 -       intro!: SUP_ereal_mult_left)
   2.595 -
   2.596 -lemma suminf_PInfty:
   2.597 -  fixes f :: "nat \<Rightarrow> ereal"
   2.598 -  assumes "\<And>i. 0 \<le> f i"
   2.599 -    and "suminf f \<noteq> \<infinity>"
   2.600 -  shows "f i \<noteq> \<infinity>"
   2.601 -proof -
   2.602 -  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
   2.603 -  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
   2.604 -    by auto
   2.605 -  then show ?thesis
   2.606 -    unfolding setsum_Pinfty by simp
   2.607 -qed
   2.608 -
   2.609 -lemma suminf_PInfty_fun:
   2.610 -  assumes "\<And>i. 0 \<le> f i"
   2.611 -    and "suminf f \<noteq> \<infinity>"
   2.612 -  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
   2.613 -proof -
   2.614 -  have "\<forall>i. \<exists>r. f i = ereal r"
   2.615 -  proof
   2.616 -    fix i
   2.617 -    show "\<exists>r. f i = ereal r"
   2.618 -      using suminf_PInfty[OF assms] assms(1)[of i]
   2.619 -      by (cases "f i") auto
   2.620 -  qed
   2.621 -  from choice[OF this] show ?thesis
   2.622 -    by auto
   2.623 -qed
   2.624 -
   2.625 -lemma summable_ereal:
   2.626 -  assumes "\<And>i. 0 \<le> f i"
   2.627 -    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   2.628 -  shows "summable f"
   2.629 -proof -
   2.630 -  have "0 \<le> (\<Sum>i. ereal (f i))"
   2.631 -    using assms by (intro suminf_0_le) auto
   2.632 -  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
   2.633 -    by (cases "\<Sum>i. ereal (f i)") auto
   2.634 -  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
   2.635 -  have "summable (\<lambda>x. ereal (f x))"
   2.636 -    using assms by auto
   2.637 -  from summable_sums[OF this]
   2.638 -  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
   2.639 -    by auto
   2.640 -  then show "summable f"
   2.641 -    unfolding r sums_ereal summable_def ..
   2.642 -qed
   2.643 -
   2.644 -lemma suminf_ereal:
   2.645 -  assumes "\<And>i. 0 \<le> f i"
   2.646 -    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   2.647 -  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
   2.648 -proof (rule sums_unique[symmetric])
   2.649 -  from summable_ereal[OF assms]
   2.650 -  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
   2.651 -    unfolding sums_ereal
   2.652 -    using assms
   2.653 -    by (intro summable_sums summable_ereal)
   2.654 -qed
   2.655 -
   2.656 -lemma suminf_ereal_minus:
   2.657 -  fixes f g :: "nat \<Rightarrow> ereal"
   2.658 -  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
   2.659 -    and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
   2.660 -  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
   2.661 -proof -
   2.662 -  {
   2.663 -    fix i
   2.664 -    have "0 \<le> f i"
   2.665 -      using ord[of i] by auto
   2.666 -  }
   2.667 -  moreover
   2.668 -  from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> f i\<close> fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
   2.669 -  from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> g i\<close> fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
   2.670 -  {
   2.671 -    fix i
   2.672 -    have "0 \<le> f i - g i"
   2.673 -      using ord[of i] by (auto simp: ereal_le_minus_iff)
   2.674 -  }
   2.675 -  moreover
   2.676 -  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
   2.677 -    using assms by (auto intro!: suminf_le_pos simp: field_simps)
   2.678 -  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
   2.679 -    using fin by auto
   2.680 -  ultimately show ?thesis
   2.681 -    using assms \<open>\<And>i. 0 \<le> f i\<close>
   2.682 -    apply simp
   2.683 -    apply (subst (1 2 3) suminf_ereal)
   2.684 -    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
   2.685 -    done
   2.686 -qed
   2.687 -
   2.688 -lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
   2.689 -proof -
   2.690 -  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
   2.691 -    by (rule suminf_upper) auto
   2.692 -  then show ?thesis
   2.693 -    by simp
   2.694 -qed
   2.695 -
   2.696 -lemma summable_real_of_ereal:
   2.697 -  fixes f :: "nat \<Rightarrow> ereal"
   2.698 -  assumes f: "\<And>i. 0 \<le> f i"
   2.699 -    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
   2.700 -  shows "summable (\<lambda>i. real (f i))"
   2.701 -proof (rule summable_def[THEN iffD2])
   2.702 -  have "0 \<le> (\<Sum>i. f i)"
   2.703 -    using assms by (auto intro: suminf_0_le)
   2.704 -  with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
   2.705 -    by (cases "(\<Sum>i. f i)") auto
   2.706 -  {
   2.707 -    fix i
   2.708 -    have "f i \<noteq> \<infinity>"
   2.709 -      using f by (intro suminf_PInfty[OF _ fin]) auto
   2.710 -    then have "\<bar>f i\<bar> \<noteq> \<infinity>"
   2.711 -      using f[of i] by auto
   2.712 -  }
   2.713 -  note fin = this
   2.714 -  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
   2.715 -    using f
   2.716 -    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
   2.717 -  also have "\<dots> = ereal r"
   2.718 -    using fin r by (auto simp: ereal_real)
   2.719 -  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
   2.720 -    by (auto simp: sums_ereal)
   2.721 -qed
   2.722 -
   2.723 -lemma suminf_SUP_eq:
   2.724 -  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
   2.725 -  assumes "\<And>i. incseq (\<lambda>n. f n i)"
   2.726 -    and "\<And>n i. 0 \<le> f n i"
   2.727 -  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
   2.728 -proof -
   2.729 -  {
   2.730 -    fix n :: nat
   2.731 -    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
   2.732 -      using assms
   2.733 -      by (auto intro!: SUP_ereal_setsum [symmetric])
   2.734 -  }
   2.735 -  note * = this
   2.736 -  show ?thesis
   2.737 -    using assms
   2.738 -    apply (subst (1 2) suminf_ereal_eq_SUP)
   2.739 -    unfolding *
   2.740 -    apply (auto intro!: SUP_upper2)
   2.741 -    apply (subst SUP_commute)
   2.742 -    apply rule
   2.743 -    done
   2.744 -qed
   2.745 -
   2.746 -lemma suminf_setsum_ereal:
   2.747 -  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
   2.748 -  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
   2.749 -  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
   2.750 -proof (cases "finite A")
   2.751 -  case True
   2.752 -  then show ?thesis
   2.753 -    using nonneg
   2.754 -    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
   2.755 -next
   2.756 -  case False
   2.757 -  then show ?thesis by simp
   2.758 -qed
   2.759 -
   2.760 -lemma suminf_ereal_eq_0:
   2.761 -  fixes f :: "nat \<Rightarrow> ereal"
   2.762 -  assumes nneg: "\<And>i. 0 \<le> f i"
   2.763 -  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
   2.764 -proof
   2.765 -  assume "(\<Sum>i. f i) = 0"
   2.766 -  {
   2.767 -    fix i
   2.768 -    assume "f i \<noteq> 0"
   2.769 -    with nneg have "0 < f i"
   2.770 -      by (auto simp: less_le)
   2.771 -    also have "f i = (\<Sum>j. if j = i then f i else 0)"
   2.772 -      by (subst suminf_finite[where N="{i}"]) auto
   2.773 -    also have "\<dots> \<le> (\<Sum>i. f i)"
   2.774 -      using nneg
   2.775 -      by (auto intro!: suminf_le_pos)
   2.776 -    finally have False
   2.777 -      using \<open>(\<Sum>i. f i) = 0\<close> by auto
   2.778 -  }
   2.779 -  then show "\<forall>i. f i = 0"
   2.780 -    by auto
   2.781 -qed simp
   2.782 -
   2.783  lemma Liminf_within:
   2.784    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   2.785    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   2.786 @@ -1045,50 +313,6 @@
   2.787    apply (metis INF_absorb centre_in_ball)
   2.788    done
   2.789  
   2.790 -
   2.791 -lemma suminf_ereal_offset_le:
   2.792 -  fixes f :: "nat \<Rightarrow> ereal"
   2.793 -  assumes f: "\<And>i. 0 \<le> f i"
   2.794 -  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
   2.795 -proof -
   2.796 -  have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
   2.797 -    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
   2.798 -  moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
   2.799 -    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
   2.800 -  then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
   2.801 -    by (rule LIMSEQ_ignore_initial_segment)
   2.802 -  ultimately show ?thesis
   2.803 -  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
   2.804 -    fix n assume "k \<le> n"
   2.805 -    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
   2.806 -      by simp
   2.807 -    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
   2.808 -      by (subst setsum.reindex) auto
   2.809 -    also have "\<dots> \<le> setsum f {..<n + k}"
   2.810 -      by (intro setsum_mono3) (auto simp: f)
   2.811 -    finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
   2.812 -  qed
   2.813 -qed
   2.814 -
   2.815 -lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
   2.816 -  by (metis sums_ereal sums_unique)
   2.817 -
   2.818 -lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
   2.819 -  by (metis sums_ereal sums_unique summable_def)
   2.820 -
   2.821 -lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
   2.822 -  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
   2.823 -
   2.824 -lemma suminf_ereal_finite_neg:
   2.825 -  assumes "summable f"
   2.826 -  shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
   2.827 -proof-
   2.828 -  from assms obtain x where "f sums x" by blast
   2.829 -  hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
   2.830 -  from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
   2.831 -  thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
   2.832 -qed
   2.833 -
   2.834  subsection \<open>monoset\<close>
   2.835  
   2.836  definition (in order) mono_set:
   2.837 @@ -1281,5 +505,4 @@
   2.838  lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)"
   2.839    by (simp split: split_indicator)
   2.840  
   2.841 -
   2.842  end
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Jul 23 14:25:05 2015 +0200
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Jul 23 16:39:10 2015 +0200
     3.3 @@ -1111,7 +1111,7 @@
     3.4  
     3.5  lemma borel_measurable_ereal[measurable (raw)]:
     3.6    assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
     3.7 -  using continuous_on_ereal f by (rule borel_measurable_continuous_on)
     3.8 +  using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id)
     3.9  
    3.10  lemma borel_measurable_real_of_ereal[measurable (raw)]:
    3.11    fixes f :: "'a \<Rightarrow> ereal"