# HG changeset patch
# User hoelzl
# Date 1437662350 -7200
# Node ID 8558e4a37b489ba38122b288389ed9722511fea9
# Parent  240563fbf41d9b03f877c415dcab2bdd9d781cd7
reorganized Extended_Real

diff -r 240563fbf41d -r 8558e4a37b48 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 23 14:25:05 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:39:10 2015 +0200
@@ -1909,6 +1909,9 @@
   shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
   unfolding top_ereal_def[symmetric] by auto
 
+lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
+  by auto
+
 lemma Sup_ereal_close:
   fixes e :: ereal
   assumes "0 < e"
@@ -2803,9 +2806,6 @@
   qed
 qed
 
-lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
-  by auto
-
 lemma sup_continuous_add[order_continuous_intros]:
   fixes f g :: "'a::complete_lattice \<Rightarrow> ereal"
   assumes nn: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x" and cont: "sup_continuous f" "sup_continuous g"
@@ -2832,6 +2832,747 @@
   by (rule sup_continuous_compose[OF _ f])
      (auto simp: sup_continuous_def ereal_of_enat_SUP)
 
+subsubsection \<open>Sums\<close>
+
+lemma sums_ereal_positive:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<And>i. 0 \<le> f i"
+  shows "f sums (SUP n. \<Sum>i<n. f i)"
+proof -
+  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
+    using ereal_add_mono[OF _ assms]
+    by (auto intro!: incseq_SucI)
+  from LIMSEQ_SUP[OF this]
+  show ?thesis unfolding sums_def
+    by (simp add: atLeast0LessThan)
+qed
+
+lemma summable_ereal_pos:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<And>i. 0 \<le> f i"
+  shows "summable f"
+  using sums_ereal_positive[of f, OF assms]
+  unfolding summable_def
+  by auto
+
+lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
+  unfolding sums_def by simp
+
+lemma suminf_ereal_eq_SUP:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<And>i. 0 \<le> f i"
+  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
+  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
+  by simp
+
+lemma suminf_bound:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
+    and pos: "\<And>n. 0 \<le> f n"
+  shows "suminf f \<le> x"
+proof (rule Lim_bounded_ereal)
+  have "summable f" using pos[THEN summable_ereal_pos] .
+  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
+    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
+  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
+    using assms by auto
+qed
+
+lemma suminf_bound_add:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
+    and pos: "\<And>n. 0 \<le> f n"
+    and "y \<noteq> -\<infinity>"
+  shows "suminf f + y \<le> x"
+proof (cases y)
+  case (real r)
+  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
+    using assms by (simp add: ereal_le_minus)
+  then have "(\<Sum> n. f n) \<le> x - y"
+    using pos by (rule suminf_bound)
+  then show "(\<Sum> n. f n) + y \<le> x"
+    using assms real by (simp add: ereal_le_minus)
+qed (insert assms, auto)
+
+lemma suminf_upper:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<And>n. 0 \<le> f n"
+  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
+  unfolding suminf_ereal_eq_SUP [OF assms]
+  by (auto intro: complete_lattice_class.SUP_upper)
+
+lemma suminf_0_le:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<And>n. 0 \<le> f n"
+  shows "0 \<le> (\<Sum>n. f n)"
+  using suminf_upper[of f 0, OF assms]
+  by simp
+
+lemma suminf_le_pos:
+  fixes f g :: "nat \<Rightarrow> ereal"
+  assumes "\<And>N. f N \<le> g N"
+    and "\<And>N. 0 \<le> f N"
+  shows "suminf f \<le> suminf g"
+proof (safe intro!: suminf_bound)
+  fix n
+  {
+    fix N
+    have "0 \<le> g N"
+      using assms(2,1)[of N] by auto
+  }
+  have "setsum f {..<n} \<le> setsum g {..<n}"
+    using assms by (auto intro: setsum_mono)
+  also have "\<dots> \<le> suminf g"
+    using \<open>\<And>N. 0 \<le> g N\<close>
+    by (rule suminf_upper)
+  finally show "setsum f {..<n} \<le> suminf g" .
+qed (rule assms(2))
+
+lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
+  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
+  by (simp add: one_ereal_def)
+
+lemma suminf_add_ereal:
+  fixes f g :: "nat \<Rightarrow> ereal"
+  assumes "\<And>i. 0 \<le> f i"
+    and "\<And>i. 0 \<le> g i"
+  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
+  apply (subst (1 2 3) suminf_ereal_eq_SUP)
+  unfolding setsum.distrib
+  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
+  done
+
+lemma suminf_cmult_ereal:
+  fixes f g :: "nat \<Rightarrow> ereal"
+  assumes "\<And>i. 0 \<le> f i"
+    and "0 \<le> a"
+  shows "(\<Sum>i. a * f i) = a * suminf f"
+  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
+       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
+       intro!: SUP_ereal_mult_left)
+
+lemma suminf_PInfty:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "\<And>i. 0 \<le> f i"
+    and "suminf f \<noteq> \<infinity>"
+  shows "f i \<noteq> \<infinity>"
+proof -
+  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
+  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
+    by auto
+  then show ?thesis
+    unfolding setsum_Pinfty by simp
+qed
+
+lemma suminf_PInfty_fun:
+  assumes "\<And>i. 0 \<le> f i"
+    and "suminf f \<noteq> \<infinity>"
+  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
+proof -
+  have "\<forall>i. \<exists>r. f i = ereal r"
+  proof
+    fix i
+    show "\<exists>r. f i = ereal r"
+      using suminf_PInfty[OF assms] assms(1)[of i]
+      by (cases "f i") auto
+  qed
+  from choice[OF this] show ?thesis
+    by auto
+qed
+
+lemma summable_ereal:
+  assumes "\<And>i. 0 \<le> f i"
+    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
+  shows "summable f"
+proof -
+  have "0 \<le> (\<Sum>i. ereal (f i))"
+    using assms by (intro suminf_0_le) auto
+  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
+    by (cases "\<Sum>i. ereal (f i)") auto
+  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
+  have "summable (\<lambda>x. ereal (f x))"
+    using assms by auto
+  from summable_sums[OF this]
+  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
+    by auto
+  then show "summable f"
+    unfolding r sums_ereal summable_def ..
+qed
+
+lemma suminf_ereal:
+  assumes "\<And>i. 0 \<le> f i"
+    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
+  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
+proof (rule sums_unique[symmetric])
+  from summable_ereal[OF assms]
+  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
+    unfolding sums_ereal
+    using assms
+    by (intro summable_sums summable_ereal)
+qed
+
+lemma suminf_ereal_minus:
+  fixes f g :: "nat \<Rightarrow> ereal"
+  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
+    and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
+  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
+proof -
+  {
+    fix i
+    have "0 \<le> f i"
+      using ord[of i] by auto
+  }
+  moreover
+  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))" ..
+  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))" ..
+  {
+    fix i
+    have "0 \<le> f i - g i"
+      using ord[of i] by (auto simp: ereal_le_minus_iff)
+  }
+  moreover
+  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
+    using assms by (auto intro!: suminf_le_pos simp: field_simps)
+  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
+    using fin by auto
+  ultimately show ?thesis
+    using assms \<open>\<And>i. 0 \<le> f i\<close>
+    apply simp
+    apply (subst (1 2 3) suminf_ereal)
+    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
+    done
+qed
+
+lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
+proof -
+  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
+    by (rule suminf_upper) auto
+  then show ?thesis
+    by simp
+qed
+
+lemma summable_real_of_ereal:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes f: "\<And>i. 0 \<le> f i"
+    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
+  shows "summable (\<lambda>i. real (f i))"
+proof (rule summable_def[THEN iffD2])
+  have "0 \<le> (\<Sum>i. f i)"
+    using assms by (auto intro: suminf_0_le)
+  with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
+    by (cases "(\<Sum>i. f i)") auto
+  {
+    fix i
+    have "f i \<noteq> \<infinity>"
+      using f by (intro suminf_PInfty[OF _ fin]) auto
+    then have "\<bar>f i\<bar> \<noteq> \<infinity>"
+      using f[of i] by auto
+  }
+  note fin = this
+  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
+    using f
+    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
+  also have "\<dots> = ereal r"
+    using fin r by (auto simp: ereal_real)
+  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
+    by (auto simp: sums_ereal)
+qed
+
+lemma suminf_SUP_eq:
+  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
+  assumes "\<And>i. incseq (\<lambda>n. f n i)"
+    and "\<And>n i. 0 \<le> f n i"
+  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
+proof -
+  {
+    fix n :: nat
+    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
+      using assms
+      by (auto intro!: SUP_ereal_setsum [symmetric])
+  }
+  note * = this
+  show ?thesis
+    using assms
+    apply (subst (1 2) suminf_ereal_eq_SUP)
+    unfolding *
+    apply (auto intro!: SUP_upper2)
+    apply (subst SUP_commute)
+    apply rule
+    done
+qed
+
+lemma suminf_setsum_ereal:
+  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
+  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
+  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
+proof (cases "finite A")
+  case True
+  then show ?thesis
+    using nonneg
+    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
+next
+  case False
+  then show ?thesis by simp
+qed
+
+lemma suminf_ereal_eq_0:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes nneg: "\<And>i. 0 \<le> f i"
+  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
+proof
+  assume "(\<Sum>i. f i) = 0"
+  {
+    fix i
+    assume "f i \<noteq> 0"
+    with nneg have "0 < f i"
+      by (auto simp: less_le)
+    also have "f i = (\<Sum>j. if j = i then f i else 0)"
+      by (subst suminf_finite[where N="{i}"]) auto
+    also have "\<dots> \<le> (\<Sum>i. f i)"
+      using nneg
+      by (auto intro!: suminf_le_pos)
+    finally have False
+      using \<open>(\<Sum>i. f i) = 0\<close> by auto
+  }
+  then show "\<forall>i. f i = 0"
+    by auto
+qed simp
+
+lemma suminf_ereal_offset_le:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes f: "\<And>i. 0 \<le> f i"
+  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
+proof -
+  have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
+    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
+  moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
+    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
+  then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
+    by (rule LIMSEQ_ignore_initial_segment)
+  ultimately show ?thesis
+  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
+    fix n assume "k \<le> n"
+    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
+      by simp
+    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
+      by (subst setsum.reindex) auto
+    also have "\<dots> \<le> setsum f {..<n + k}"
+      by (intro setsum_mono3) (auto simp: f)
+    finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
+  qed
+qed
+
+lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
+  by (metis sums_ereal sums_unique)
+
+lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
+  by (metis sums_ereal sums_unique summable_def)
+
+lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
+  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
+
+lemma suminf_ereal_finite_neg:
+  assumes "summable f"
+  shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
+proof-
+  from assms obtain x where "f sums x" by blast
+  hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
+  from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
+  thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
+qed
+
+
+lemma convergent_limsup_cl:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  shows "convergent X \<Longrightarrow> limsup X = lim X"
+  by (auto simp: convergent_def limI lim_imp_Limsup)
+
+lemma lim_increasing_cl:
+  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
+  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+proof
+  show "f ----> (SUP n. f n)"
+    using assms
+    by (intro increasing_tendsto)
+       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
+qed
+
+lemma lim_decreasing_cl:
+  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
+  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
+proof
+  show "f ----> (INF n. f n)"
+    using assms
+    by (intro decreasing_tendsto)
+       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
+qed
+
+lemma compact_complete_linorder:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
+proof -
+  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
+    using seq_monosub[of X]
+    unfolding comp_def
+    by auto
+  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)"
+    by (auto simp add: monoseq_def)
+  then obtain l where "(X \<circ> r) ----> l"
+     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
+     by auto
+  then show ?thesis
+    using \<open>subseq r\<close> by auto
+qed
+
+lemma ereal_dense3:
+  fixes x y :: ereal
+  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
+proof (cases x y rule: ereal2_cases, simp_all)
+  fix r q :: real
+  assume "r < q"
+  from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
+    by (fastforce simp: Rats_def)
+next
+  fix r :: real
+  show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
+    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
+    by (auto simp: Rats_def)
+qed
+
+lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
+  using continuous_on_eq_continuous_within[of A ereal]
+  by (auto intro: continuous_on_ereal continuous_on_id)
+
+lemma ereal_open_uminus:
+  fixes S :: "ereal set"
+  assumes "open S"
+  shows "open (uminus ` S)"
+  using \<open>open S\<close>[unfolded open_generated_order]
+proof induct
+  have "range uminus = (UNIV :: ereal set)"
+    by (auto simp: image_iff ereal_uminus_eq_reorder)
+  then show "open (range uminus :: ereal set)"
+    by simp
+qed (auto simp add: image_Union image_Int)
+
+lemma ereal_uminus_complement:
+  fixes S :: "ereal set"
+  shows "uminus ` (- S) = - uminus ` S"
+  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
+
+lemma ereal_closed_uminus:
+  fixes S :: "ereal set"
+  assumes "closed S"
+  shows "closed (uminus ` S)"
+  using assms
+  unfolding closed_def ereal_uminus_complement[symmetric]
+  by (rule ereal_open_uminus)
+
+lemma ereal_open_affinity_pos:
+  fixes S :: "ereal set"
+  assumes "open S"
+    and m: "m \<noteq> \<infinity>" "0 < m"
+    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
+  shows "open ((\<lambda>x. m * x + t) ` S)"
+proof -
+  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
+    using m t
+    apply (intro open_vimage \<open>open S\<close>)
+    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
+                 tendsto_ident_at tendsto_add_left_ereal)
+    apply auto
+    done
+  also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
+    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
+                       simp del: uminus_ereal.simps)
+  also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
+    using m t
+    by (simp add: set_eq_iff image_iff)
+       (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
+              ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
+  finally show ?thesis .
+qed
+
+lemma ereal_open_affinity:
+  fixes S :: "ereal set"
+  assumes "open S"
+    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
+    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
+  shows "open ((\<lambda>x. m * x + t) ` S)"
+proof cases
+  assume "0 < m"
+  then show ?thesis
+    using ereal_open_affinity_pos[OF \<open>open S\<close> _ _ t, of m] m
+    by auto
+next
+  assume "\<not> 0 < m" then
+  have "0 < -m"
+    using \<open>m \<noteq> 0\<close>
+    by (cases m) auto
+  then have m: "-m \<noteq> \<infinity>" "0 < -m"
+    using \<open>\<bar>m\<bar> \<noteq> \<infinity>\<close>
+    by (auto simp: ereal_uminus_eq_reorder)
+  from ereal_open_affinity_pos[OF ereal_open_uminus[OF \<open>open S\<close>] m t] show ?thesis
+    unfolding image_image by simp
+qed
+
+lemma open_uminus_iff:
+  fixes S :: "ereal set"
+  shows "open (uminus ` S) \<longleftrightarrow> open S"
+  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
+  by auto
+
+lemma ereal_Liminf_uminus:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
+  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
+
+lemma Liminf_PInfty:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "\<not> trivial_limit net"
+  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
+  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
+  using Liminf_le_Limsup[OF assms, of f]
+  by auto
+
+lemma Limsup_MInfty:
+  fixes f :: "'a \<Rightarrow> ereal"
+  assumes "\<not> trivial_limit net"
+  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
+  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
+  using Liminf_le_Limsup[OF assms, of f]
+  by auto
+
+lemma convergent_ereal:
+  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
+  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
+  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
+  by (auto simp: convergent_def)
+
+lemma limsup_le_liminf_real:
+  fixes X :: "nat \<Rightarrow> real" and L :: real
+  assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
+  shows "X ----> L"
+proof -
+  from 1 2 have "limsup X \<le> liminf X" by auto
+  hence 3: "limsup X = liminf X"  
+    apply (subst eq_iff, rule conjI)
+    by (rule Liminf_le_Limsup, auto)
+  hence 4: "convergent (\<lambda>n. ereal (X n))"
+    by (subst convergent_ereal)
+  hence "limsup X = lim (\<lambda>n. ereal(X n))"
+    by (rule convergent_limsup_cl)
+  also from 1 2 3 have "limsup X = L" by auto
+  finally have "lim (\<lambda>n. ereal(X n)) = L" ..
+  hence "(\<lambda>n. ereal (X n)) ----> L"
+    apply (elim subst)
+    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
+  thus ?thesis by simp
+qed
+
+lemma liminf_PInfty:
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
+  by (metis Liminf_PInfty trivial_limit_sequentially)
+
+lemma limsup_MInfty:
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
+  by (metis Limsup_MInfty trivial_limit_sequentially)
+
+lemma ereal_lim_mono:
+  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
+  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
+    and "X ----> x"
+    and "Y ----> y"
+  shows "x \<le> y"
+  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
+
+lemma incseq_le_ereal:
+  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
+  assumes inc: "incseq X"
+    and lim: "X ----> L"
+  shows "X N \<le> L"
+  using inc
+  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
+
+lemma decseq_ge_ereal:
+  assumes dec: "decseq X"
+    and lim: "X ----> (L::'a::linorder_topology)"
+  shows "X N \<ge> L"
+  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
+
+lemma bounded_abs:
+  fixes a :: real
+  assumes "a \<le> x"
+    and "x \<le> b"
+  shows "abs x \<le> max (abs a) (abs b)"
+  by (metis abs_less_iff assms leI le_max_iff_disj
+    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
+
+lemma ereal_Sup_lim:
+  fixes a :: "'a::{complete_linorder,linorder_topology}"
+  assumes "\<And>n. b n \<in> s"
+    and "b ----> a"
+  shows "a \<le> Sup s"
+  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
+
+lemma ereal_Inf_lim:
+  fixes a :: "'a::{complete_linorder,linorder_topology}"
+  assumes "\<And>n. b n \<in> s"
+    and "b ----> a"
+  shows "Inf s \<le> a"
+  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
+
+lemma SUP_Lim_ereal:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  assumes inc: "incseq X"
+    and l: "X ----> l"
+  shows "(SUP n. X n) = l"
+  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
+  by simp
+
+lemma INF_Lim_ereal:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+  assumes dec: "decseq X"
+    and l: "X ----> l"
+  shows "(INF n. X n) = l"
+  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
+  by simp
+
+lemma SUP_eq_LIMSEQ:
+  assumes "mono f"
+  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
+proof
+  have inc: "incseq (\<lambda>i. ereal (f i))"
+    using \<open>mono f\<close> unfolding mono_def incseq_def by auto
+  {
+    assume "f ----> x"
+    then have "(\<lambda>i. ereal (f i)) ----> ereal x"
+      by auto
+    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
+  next
+    assume "(SUP n. ereal (f n)) = ereal x"
+    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
+  }
+qed
+
+lemma liminf_ereal_cminus:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "c \<noteq> -\<infinity>"
+  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
+proof (cases c)
+  case PInf
+  then show ?thesis
+    by (simp add: Liminf_const)
+next
+  case (real r)
+  then show ?thesis
+    unfolding liminf_SUP_INF limsup_INF_SUP
+    apply (subst INF_ereal_minus_right)
+    apply auto
+    apply (subst SUP_ereal_minus_right)
+    apply auto
+    done
+qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
+
+
+subsubsection \<open>Continuity\<close>
+
+lemma continuous_at_of_ereal:
+  "\<bar>x0 :: ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous (at x0) real"
+  unfolding continuous_at
+  by (rule lim_real_of_ereal) (simp add: ereal_real)
+
+lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
+  by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
+
+lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
+  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
+
+lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
+  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
+
+lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
+  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
+
+lemma
+  shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
+    and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
+  unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
+    eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
+  by (auto simp add: ereal_all_split ereal_ex_split)
+
+lemma ereal_tendsto_simps1:
+  "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
+  "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
+  "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
+  "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
+  unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
+  by (auto simp: filtermap_filtermap filtermap_ident)
+
+lemma ereal_tendsto_simps2:
+  "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
+  "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
+  "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
+  unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
+  using lim_ereal by (simp_all add: comp_def)
+
+lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
+
+lemma continuous_at_iff_ereal:
+  fixes f :: "'a::t2_space \<Rightarrow> real"
+  shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
+  unfolding continuous_within comp_def lim_ereal ..
+
+lemma continuous_on_iff_ereal:
+  fixes f :: "'a::t2_space => real"
+  assumes "open A"
+  shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
+  unfolding continuous_on_def comp_def lim_ereal ..
+
+lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
+  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
+  by auto
+
+lemma continuous_on_iff_real:
+  fixes f :: "'a::t2_space \<Rightarrow> ereal"
+  assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
+  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
+proof -
+  have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
+    using assms by force
+  then have *: "continuous_on (f ` A) real"
+    using continuous_on_real by (simp add: continuous_on_subset)
+  have **: "continuous_on ((real \<circ> f) ` A) ereal"
+    by (intro continuous_on_ereal continuous_on_id)
+  {
+    assume "continuous_on A f"
+    then have "continuous_on A (real \<circ> f)"
+      apply (subst continuous_on_compose)
+      using *
+      apply auto
+      done
+  }
+  moreover
+  {
+    assume "continuous_on A (real \<circ> f)"
+    then have "continuous_on A (ereal \<circ> (real \<circ> f))"
+      apply (subst continuous_on_compose)
+      using **
+      apply auto
+      done
+    then have "continuous_on A f"
+      apply (subst continuous_on_cong[of _ A _ "ereal \<circ> (real \<circ> f)"])
+      using assms ereal_real
+      apply auto
+      done
+  }
+  ultimately show ?thesis
+    by auto
+qed
+
+
 subsubsection \<open>Tests for code generator\<close>
 
 (* A small list of simple arithmetic expressions *)
diff -r 240563fbf41d -r 8558e4a37b48 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jul 23 14:25:05 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jul 23 16:39:10 2015 +0200
@@ -11,48 +11,6 @@
   imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
 begin
 
-lemma convergent_limsup_cl:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "convergent X \<Longrightarrow> limsup X = lim X"
-  by (auto simp: convergent_def limI lim_imp_Limsup)
-
-lemma lim_increasing_cl:
-  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
-  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
-proof
-  show "f ----> (SUP n. f n)"
-    using assms
-    by (intro increasing_tendsto)
-       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
-qed
-
-lemma lim_decreasing_cl:
-  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
-  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
-proof
-  show "f ----> (INF n. f n)"
-    using assms
-    by (intro decreasing_tendsto)
-       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
-qed
-
-lemma compact_complete_linorder:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
-proof -
-  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
-    using seq_monosub[of X]
-    unfolding comp_def
-    by auto
-  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)"
-    by (auto simp add: monoseq_def)
-  then obtain l where "(X \<circ> r) ----> l"
-     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
-     by auto
-  then show ?thesis
-    using \<open>subseq r\<close> by auto
-qed
-
 lemma compact_UNIV:
   "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
   using compact_complete_linorder
@@ -94,21 +52,6 @@
     by simp
 qed
 
-lemma ereal_dense3:
-  fixes x y :: ereal
-  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
-proof (cases x y rule: ereal2_cases, simp_all)
-  fix r q :: real
-  assume "r < q"
-  from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
-    by (fastforce simp: Rats_def)
-next
-  fix r :: real
-  show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
-    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
-    by (auto simp: Rats_def)
-qed
-
 instance ereal :: second_countable_topology
 proof (default, intro exI conjI)
   let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
@@ -139,43 +82,6 @@
   qed
 qed
 
-lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
-  unfolding continuous_on_topological open_ereal_def
-  by auto
-
-lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
-  using continuous_on_eq_continuous_at[of UNIV]
-  by auto
-
-lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
-  using continuous_on_eq_continuous_within[of A]
-  by auto
-
-lemma ereal_open_uminus:
-  fixes S :: "ereal set"
-  assumes "open S"
-  shows "open (uminus ` S)"
-  using \<open>open S\<close>[unfolded open_generated_order]
-proof induct
-  have "range uminus = (UNIV :: ereal set)"
-    by (auto simp: image_iff ereal_uminus_eq_reorder)
-  then show "open (range uminus :: ereal set)"
-    by simp
-qed (auto simp add: image_Union image_Int)
-
-lemma ereal_uminus_complement:
-  fixes S :: "ereal set"
-  shows "uminus ` (- S) = - uminus ` S"
-  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
-
-lemma ereal_closed_uminus:
-  fixes S :: "ereal set"
-  assumes "closed S"
-  shows "closed (uminus ` S)"
-  using assms
-  unfolding closed_def ereal_uminus_complement[symmetric]
-  by (rule ereal_open_uminus)
-
 lemma ereal_open_closed_aux:
   fixes S :: "ereal set"
   assumes "open S"
@@ -185,6 +91,7 @@
 proof (rule ccontr)
   assume "\<not> ?thesis"
   then have *: "Inf S \<in> S"
+    
     by (metis assms(2) closed_contains_Inf_cl)
   {
     assume "Inf S = -\<infinity>"
@@ -243,54 +150,6 @@
     by auto
 qed
 
-lemma ereal_open_affinity_pos:
-  fixes S :: "ereal set"
-  assumes "open S"
-    and m: "m \<noteq> \<infinity>" "0 < m"
-    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
-  shows "open ((\<lambda>x. m * x + t) ` S)"
-proof -
-  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
-    using m t
-    apply (intro open_vimage \<open>open S\<close>)
-    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
-                 tendsto_ident_at tendsto_add_left_ereal)
-    apply auto
-    done
-  also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
-    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
-                       simp del: uminus_ereal.simps)
-  also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
-    using m t
-    by (simp add: set_eq_iff image_iff)
-       (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
-              ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
-  finally show ?thesis .
-qed
-
-lemma ereal_open_affinity:
-  fixes S :: "ereal set"
-  assumes "open S"
-    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
-    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
-  shows "open ((\<lambda>x. m * x + t) ` S)"
-proof cases
-  assume "0 < m"
-  then show ?thesis
-    using ereal_open_affinity_pos[OF \<open>open S\<close> _ _ t, of m] m
-    by auto
-next
-  assume "\<not> 0 < m" then
-  have "0 < -m"
-    using \<open>m \<noteq> 0\<close>
-    by (cases m) auto
-  then have m: "-m \<noteq> \<infinity>" "0 < -m"
-    using \<open>\<bar>m\<bar> \<noteq> \<infinity>\<close>
-    by (auto simp: ereal_uminus_eq_reorder)
-  from ereal_open_affinity_pos[OF ereal_open_uminus[OF \<open>open S\<close>] m t] show ?thesis
-    unfolding image_image by simp
-qed
-
 lemma ereal_open_atLeast:
   fixes x :: ereal
   shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
@@ -310,290 +169,6 @@
     by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
 qed
 
-lemma open_uminus_iff:
-  fixes S :: "ereal set"
-  shows "open (uminus ` S) \<longleftrightarrow> open S"
-  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
-  by auto
-
-lemma ereal_Liminf_uminus:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
-  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
-
-lemma Liminf_PInfty:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<not> trivial_limit net"
-  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
-  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
-  using Liminf_le_Limsup[OF assms, of f]
-  by auto
-
-lemma Limsup_MInfty:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<not> trivial_limit net"
-  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
-  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
-  using Liminf_le_Limsup[OF assms, of f]
-  by auto
-
-lemma convergent_ereal:
-  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
-  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
-  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
-  by (auto simp: convergent_def)
-
-lemma limsup_le_liminf_real:
-  fixes X :: "nat \<Rightarrow> real" and L :: real
-  assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
-  shows "X ----> L"
-proof -
-  from 1 2 have "limsup X \<le> liminf X" by auto
-  hence 3: "limsup X = liminf X"  
-    apply (subst eq_iff, rule conjI)
-    by (rule Liminf_le_Limsup, auto)
-  hence 4: "convergent (\<lambda>n. ereal (X n))"
-    by (subst convergent_ereal)
-  hence "limsup X = lim (\<lambda>n. ereal(X n))"
-    by (rule convergent_limsup_cl)
-  also from 1 2 3 have "limsup X = L" by auto
-  finally have "lim (\<lambda>n. ereal(X n)) = L" ..
-  hence "(\<lambda>n. ereal (X n)) ----> L"
-    apply (elim subst)
-    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
-  thus ?thesis by simp
-qed
-
-lemma liminf_PInfty:
-  fixes X :: "nat \<Rightarrow> ereal"
-  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
-  by (metis Liminf_PInfty trivial_limit_sequentially)
-
-lemma limsup_MInfty:
-  fixes X :: "nat \<Rightarrow> ereal"
-  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
-  by (metis Limsup_MInfty trivial_limit_sequentially)
-
-lemma ereal_lim_mono:
-  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
-    and "X ----> x"
-    and "Y ----> y"
-  shows "x \<le> y"
-  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
-
-lemma incseq_le_ereal:
-  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
-  assumes inc: "incseq X"
-    and lim: "X ----> L"
-  shows "X N \<le> L"
-  using inc
-  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
-
-lemma decseq_ge_ereal:
-  assumes dec: "decseq X"
-    and lim: "X ----> (L::'a::linorder_topology)"
-  shows "X N \<ge> L"
-  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-
-lemma bounded_abs:
-  fixes a :: real
-  assumes "a \<le> x"
-    and "x \<le> b"
-  shows "abs x \<le> max (abs a) (abs b)"
-  by (metis abs_less_iff assms leI le_max_iff_disj
-    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-
-lemma ereal_Sup_lim:
-  fixes a :: "'a::{complete_linorder,linorder_topology}"
-  assumes "\<And>n. b n \<in> s"
-    and "b ----> a"
-  shows "a \<le> Sup s"
-  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
-
-lemma ereal_Inf_lim:
-  fixes a :: "'a::{complete_linorder,linorder_topology}"
-  assumes "\<And>n. b n \<in> s"
-    and "b ----> a"
-  shows "Inf s \<le> a"
-  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
-
-lemma SUP_Lim_ereal:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  assumes inc: "incseq X"
-    and l: "X ----> l"
-  shows "(SUP n. X n) = l"
-  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
-  by simp
-
-lemma INF_Lim_ereal:
-  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  assumes dec: "decseq X"
-    and l: "X ----> l"
-  shows "(INF n. X n) = l"
-  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
-  by simp
-
-lemma SUP_eq_LIMSEQ:
-  assumes "mono f"
-  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
-proof
-  have inc: "incseq (\<lambda>i. ereal (f i))"
-    using \<open>mono f\<close> unfolding mono_def incseq_def by auto
-  {
-    assume "f ----> x"
-    then have "(\<lambda>i. ereal (f i)) ----> ereal x"
-      by auto
-    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
-  next
-    assume "(SUP n. ereal (f n)) = ereal x"
-    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
-  }
-qed
-
-lemma liminf_ereal_cminus:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "c \<noteq> -\<infinity>"
-  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
-proof (cases c)
-  case PInf
-  then show ?thesis
-    by (simp add: Liminf_const)
-next
-  case (real r)
-  then show ?thesis
-    unfolding liminf_SUP_INF limsup_INF_SUP
-    apply (subst INF_ereal_minus_right)
-    apply auto
-    apply (subst SUP_ereal_minus_right)
-    apply auto
-    done
-qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
-
-
-subsubsection \<open>Continuity\<close>
-
-lemma continuous_at_of_ereal:
-  fixes x0 :: ereal
-  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
-  shows "continuous (at x0) real"
-proof -
-  {
-    fix T
-    assume T: "open T" "real x0 \<in> T"
-    def S \<equiv> "ereal ` T"
-    then have "ereal (real x0) \<in> S"
-      using T by auto
-    then have "x0 \<in> S"
-      using assms ereal_real by auto
-    moreover have "open S"
-      using open_ereal S_def T by auto
-    moreover have "\<forall>y\<in>S. real y \<in> T"
-      using S_def T by auto
-    ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)"
-      by auto
-  }
-  then show ?thesis
-    unfolding continuous_at_open by blast
-qed
-
-lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
-  by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
-
-lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
-  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
-
-lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
-  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
-
-lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
-  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
-
-lemma
-  shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
-    and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
-  unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
-    eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
-  by (auto simp add: ereal_all_split ereal_ex_split)
-
-lemma ereal_tendsto_simps1:
-  "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
-  "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
-  "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
-  "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
-  unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
-  by (auto simp: filtermap_filtermap filtermap_ident)
-
-lemma ereal_tendsto_simps2:
-  "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
-  "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
-  "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
-  unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
-  using lim_ereal by (simp_all add: comp_def)
-
-lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
-
-lemma continuous_at_iff_ereal:
-  fixes f :: "'a::t2_space \<Rightarrow> real"
-  shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
-  unfolding continuous_within comp_def lim_ereal ..
-
-lemma continuous_on_iff_ereal:
-  fixes f :: "'a::t2_space => real"
-  assumes "open A"
-  shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
-  unfolding continuous_on_def comp_def lim_ereal ..
-
-lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
-  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
-  by auto
-
-lemma continuous_on_iff_real:
-  fixes f :: "'a::t2_space \<Rightarrow> ereal"
-  assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
-  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
-proof -
-  have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
-    using assms by force
-  then have *: "continuous_on (f ` A) real"
-    using continuous_on_real by (simp add: continuous_on_subset)
-  have **: "continuous_on ((real \<circ> f) ` A) ereal"
-    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"]
-    by blast
-  {
-    assume "continuous_on A f"
-    then have "continuous_on A (real \<circ> f)"
-      apply (subst continuous_on_compose)
-      using *
-      apply auto
-      done
-  }
-  moreover
-  {
-    assume "continuous_on A (real \<circ> f)"
-    then have "continuous_on A (ereal \<circ> (real \<circ> f))"
-      apply (subst continuous_on_compose)
-      using **
-      apply auto
-      done
-    then have "continuous_on A f"
-      apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f])
-      using assms ereal_real
-      apply auto
-      done
-  }
-  ultimately show ?thesis
-    by auto
-qed
-
-lemma continuous_at_const:
-  fixes f :: "'a::t2_space \<Rightarrow> ereal"
-  assumes "\<forall>x. f x = C"
-  shows "\<forall>x. continuous (at x) f"
-  unfolding continuous_at_open
-  using assms t1_space
-  by auto
-
 lemma mono_closed_real:
   fixes S :: "real set"
   assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
@@ -675,313 +250,6 @@
     using mono_closed_real[of S] assms by auto
 qed
 
-
-subsection \<open>Sums\<close>
-
-lemma sums_ereal_positive:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-  shows "f sums (SUP n. \<Sum>i<n. f i)"
-proof -
-  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
-    using ereal_add_mono[OF _ assms]
-    by (auto intro!: incseq_SucI)
-  from LIMSEQ_SUP[OF this]
-  show ?thesis unfolding sums_def
-    by (simp add: atLeast0LessThan)
-qed
-
-lemma summable_ereal_pos:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-  shows "summable f"
-  using sums_ereal_positive[of f, OF assms]
-  unfolding summable_def
-  by auto
-
-lemma suminf_ereal_eq_SUP:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
-  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
-  by simp
-
-lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
-  unfolding sums_def by simp
-
-lemma suminf_bound:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
-    and pos: "\<And>n. 0 \<le> f n"
-  shows "suminf f \<le> x"
-proof (rule Lim_bounded_ereal)
-  have "summable f" using pos[THEN summable_ereal_pos] .
-  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
-    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
-  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
-    using assms by auto
-qed
-
-lemma suminf_bound_add:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
-    and pos: "\<And>n. 0 \<le> f n"
-    and "y \<noteq> -\<infinity>"
-  shows "suminf f + y \<le> x"
-proof (cases y)
-  case (real r)
-  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
-    using assms by (simp add: ereal_le_minus)
-  then have "(\<Sum> n. f n) \<le> x - y"
-    using pos by (rule suminf_bound)
-  then show "(\<Sum> n. f n) + y \<le> x"
-    using assms real by (simp add: ereal_le_minus)
-qed (insert assms, auto)
-
-lemma suminf_upper:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>n. 0 \<le> f n"
-  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
-  unfolding suminf_ereal_eq_SUP [OF assms]
-  by (auto intro: complete_lattice_class.SUP_upper)
-
-lemma suminf_0_le:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>n. 0 \<le> f n"
-  shows "0 \<le> (\<Sum>n. f n)"
-  using suminf_upper[of f 0, OF assms]
-  by simp
-
-lemma suminf_le_pos:
-  fixes f g :: "nat \<Rightarrow> ereal"
-  assumes "\<And>N. f N \<le> g N"
-    and "\<And>N. 0 \<le> f N"
-  shows "suminf f \<le> suminf g"
-proof (safe intro!: suminf_bound)
-  fix n
-  {
-    fix N
-    have "0 \<le> g N"
-      using assms(2,1)[of N] by auto
-  }
-  have "setsum f {..<n} \<le> setsum g {..<n}"
-    using assms by (auto intro: setsum_mono)
-  also have "\<dots> \<le> suminf g"
-    using \<open>\<And>N. 0 \<le> g N\<close>
-    by (rule suminf_upper)
-  finally show "setsum f {..<n} \<le> suminf g" .
-qed (rule assms(2))
-
-lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
-  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
-  by (simp add: one_ereal_def)
-
-lemma suminf_add_ereal:
-  fixes f g :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-    and "\<And>i. 0 \<le> g i"
-  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
-  apply (subst (1 2 3) suminf_ereal_eq_SUP)
-  unfolding setsum.distrib
-  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
-  done
-
-lemma suminf_cmult_ereal:
-  fixes f g :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-    and "0 \<le> a"
-  shows "(\<Sum>i. a * f i) = a * suminf f"
-  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
-       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
-       intro!: SUP_ereal_mult_left)
-
-lemma suminf_PInfty:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-    and "suminf f \<noteq> \<infinity>"
-  shows "f i \<noteq> \<infinity>"
-proof -
-  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
-  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
-    by auto
-  then show ?thesis
-    unfolding setsum_Pinfty by simp
-qed
-
-lemma suminf_PInfty_fun:
-  assumes "\<And>i. 0 \<le> f i"
-    and "suminf f \<noteq> \<infinity>"
-  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
-proof -
-  have "\<forall>i. \<exists>r. f i = ereal r"
-  proof
-    fix i
-    show "\<exists>r. f i = ereal r"
-      using suminf_PInfty[OF assms] assms(1)[of i]
-      by (cases "f i") auto
-  qed
-  from choice[OF this] show ?thesis
-    by auto
-qed
-
-lemma summable_ereal:
-  assumes "\<And>i. 0 \<le> f i"
-    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
-  shows "summable f"
-proof -
-  have "0 \<le> (\<Sum>i. ereal (f i))"
-    using assms by (intro suminf_0_le) auto
-  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
-    by (cases "\<Sum>i. ereal (f i)") auto
-  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
-  have "summable (\<lambda>x. ereal (f x))"
-    using assms by auto
-  from summable_sums[OF this]
-  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
-    by auto
-  then show "summable f"
-    unfolding r sums_ereal summable_def ..
-qed
-
-lemma suminf_ereal:
-  assumes "\<And>i. 0 \<le> f i"
-    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
-  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
-proof (rule sums_unique[symmetric])
-  from summable_ereal[OF assms]
-  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
-    unfolding sums_ereal
-    using assms
-    by (intro summable_sums summable_ereal)
-qed
-
-lemma suminf_ereal_minus:
-  fixes f g :: "nat \<Rightarrow> ereal"
-  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
-    and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
-  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
-proof -
-  {
-    fix i
-    have "0 \<le> f i"
-      using ord[of i] by auto
-  }
-  moreover
-  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))" ..
-  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))" ..
-  {
-    fix i
-    have "0 \<le> f i - g i"
-      using ord[of i] by (auto simp: ereal_le_minus_iff)
-  }
-  moreover
-  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
-    using assms by (auto intro!: suminf_le_pos simp: field_simps)
-  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
-    using fin by auto
-  ultimately show ?thesis
-    using assms \<open>\<And>i. 0 \<le> f i\<close>
-    apply simp
-    apply (subst (1 2 3) suminf_ereal)
-    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
-    done
-qed
-
-lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
-proof -
-  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
-    by (rule suminf_upper) auto
-  then show ?thesis
-    by simp
-qed
-
-lemma summable_real_of_ereal:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes f: "\<And>i. 0 \<le> f i"
-    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
-  shows "summable (\<lambda>i. real (f i))"
-proof (rule summable_def[THEN iffD2])
-  have "0 \<le> (\<Sum>i. f i)"
-    using assms by (auto intro: suminf_0_le)
-  with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
-    by (cases "(\<Sum>i. f i)") auto
-  {
-    fix i
-    have "f i \<noteq> \<infinity>"
-      using f by (intro suminf_PInfty[OF _ fin]) auto
-    then have "\<bar>f i\<bar> \<noteq> \<infinity>"
-      using f[of i] by auto
-  }
-  note fin = this
-  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
-    using f
-    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
-  also have "\<dots> = ereal r"
-    using fin r by (auto simp: ereal_real)
-  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
-    by (auto simp: sums_ereal)
-qed
-
-lemma suminf_SUP_eq:
-  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
-  assumes "\<And>i. incseq (\<lambda>n. f n i)"
-    and "\<And>n i. 0 \<le> f n i"
-  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
-proof -
-  {
-    fix n :: nat
-    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
-      using assms
-      by (auto intro!: SUP_ereal_setsum [symmetric])
-  }
-  note * = this
-  show ?thesis
-    using assms
-    apply (subst (1 2) suminf_ereal_eq_SUP)
-    unfolding *
-    apply (auto intro!: SUP_upper2)
-    apply (subst SUP_commute)
-    apply rule
-    done
-qed
-
-lemma suminf_setsum_ereal:
-  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
-  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
-  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
-proof (cases "finite A")
-  case True
-  then show ?thesis
-    using nonneg
-    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
-next
-  case False
-  then show ?thesis by simp
-qed
-
-lemma suminf_ereal_eq_0:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes nneg: "\<And>i. 0 \<le> f i"
-  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
-proof
-  assume "(\<Sum>i. f i) = 0"
-  {
-    fix i
-    assume "f i \<noteq> 0"
-    with nneg have "0 < f i"
-      by (auto simp: less_le)
-    also have "f i = (\<Sum>j. if j = i then f i else 0)"
-      by (subst suminf_finite[where N="{i}"]) auto
-    also have "\<dots> \<le> (\<Sum>i. f i)"
-      using nneg
-      by (auto intro!: suminf_le_pos)
-    finally have False
-      using \<open>(\<Sum>i. f i) = 0\<close> by auto
-  }
-  then show "\<forall>i. f i = 0"
-    by auto
-qed simp
-
 lemma Liminf_within:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
@@ -1045,50 +313,6 @@
   apply (metis INF_absorb centre_in_ball)
   done
 
-
-lemma suminf_ereal_offset_le:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes f: "\<And>i. 0 \<le> f i"
-  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
-proof -
-  have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
-    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
-  moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
-    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
-  then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
-    by (rule LIMSEQ_ignore_initial_segment)
-  ultimately show ?thesis
-  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
-    fix n assume "k \<le> n"
-    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
-      by simp
-    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
-      by (subst setsum.reindex) auto
-    also have "\<dots> \<le> setsum f {..<n + k}"
-      by (intro setsum_mono3) (auto simp: f)
-    finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
-  qed
-qed
-
-lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
-  by (metis sums_ereal sums_unique)
-
-lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
-  by (metis sums_ereal sums_unique summable_def)
-
-lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
-  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
-
-lemma suminf_ereal_finite_neg:
-  assumes "summable f"
-  shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
-proof-
-  from assms obtain x where "f sums x" by blast
-  hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
-  from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
-  thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
-qed
-
 subsection \<open>monoset\<close>
 
 definition (in order) mono_set:
@@ -1281,5 +505,4 @@
 lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)"
   by (simp split: split_indicator)
 
-
 end
diff -r 240563fbf41d -r 8558e4a37b48 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Thu Jul 23 14:25:05 2015 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Jul 23 16:39:10 2015 +0200
@@ -1111,7 +1111,7 @@
 
 lemma borel_measurable_ereal[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
-  using continuous_on_ereal f by (rule borel_measurable_continuous_on)
+  using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id)
 
 lemma borel_measurable_real_of_ereal[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> ereal"