# HG changeset patch
# User hoelzl
# Date 1400606679 -7200
# Node ID e7fd64f828760fb1c717fb5086bf86ed430b0335
# Parent  c9e98c2498fdaa4b35426aaf583c6bf4bd7d6387
add various lemmas

diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 20 19:24:39 2014 +0200
@@ -415,10 +415,13 @@
     by (auto simp add: finite_conv_nat_seg_image)
 qed
 
+lemma finite_cartesian_product_iff:
+  "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))"
+  by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
+
 lemma finite_prod: 
   "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
-by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV 
-   dest: finite_cartesian_productD1 finite_cartesian_productD2)
+  using finite_cartesian_product_iff[of UNIV UNIV] by simp
 
 lemma finite_Pow_iff [iff]:
   "finite (Pow A) \<longleftrightarrow> finite A"
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue May 20 19:24:39 2014 +0200
@@ -283,4 +283,17 @@
   shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"
   using S[THEN subset_range_from_nat_into] by auto
 
+lemma finite_sequence_to_countable_set:
+   assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
+proof -  show thesis
+    apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
+    apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
+  proof -
+    fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
+    with from_nat_into_surj[OF `countable X` `x \<in> X`]
+    show False
+      by auto
+  qed
+qed
+
 end
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue May 20 19:24:39 2014 +0200
@@ -2168,6 +2168,10 @@
     by (auto simp: order_tendsto_iff)
 qed
 
+lemma tendsto_PInfty_eq_at_top:
+  "((\<lambda>z. ereal (f z)) ---> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
+  unfolding tendsto_PInfty filterlim_at_top_dense by simp
+
 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
   unfolding tendsto_def
 proof safe
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Library/Library.thy	Tue May 20 19:24:39 2014 +0200
@@ -39,6 +39,7 @@
   Monad_Syntax
   Multiset
   Numeral_Type
+  NthRoot_Limits
   OptionalSugar
   Option_ord
   Order_Continuity
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Library/NthRoot_Limits.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/NthRoot_Limits.thy	Tue May 20 19:24:39 2014 +0200
@@ -0,0 +1,94 @@
+theory NthRoot_Limits
+  imports Complex_Main "~~/src/HOL/Number_Theory/Binomial"
+begin
+
+text {*
+
+This does not fit into @{text Complex_Main}, as it depends on @{text Binomial}
+
+*}
+
+lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
+proof -
+  def x \<equiv> "\<lambda>n. root n n - 1"
+  have "x ----> sqrt 0"
+  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
+    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
+      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
+         (simp_all add: at_infinity_eq_at_top_bot)
+    { fix n :: nat assume "2 < n"
+      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
+        using `2 < n` unfolding gbinomial_def binomial_gbinomial
+        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
+      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
+        by (simp add: x_def)
+      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
+        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
+      also have "\<dots> = (x n + 1) ^ n"
+        by (simp add: binomial_ring)
+      also have "\<dots> = n"
+        using `2 < n` by (simp add: x_def)
+      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
+        by simp
+      then have "(x n)\<^sup>2 \<le> 2 / real n"
+        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
+      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
+        by simp }
+    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
+      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
+    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
+      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
+  qed
+  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
+    by (simp add: x_def)
+qed
+
+lemma LIMSEQ_root_const:
+  assumes "0 < c"
+  shows "(\<lambda>n. root n c) ----> 1"
+proof -
+  { fix c :: real assume "1 \<le> c"
+    def x \<equiv> "\<lambda>n. root n c - 1"
+    have "x ----> 0"
+    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
+      show "(\<lambda>n. c / n) ----> 0"
+        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
+           (simp_all add: at_infinity_eq_at_top_bot)
+      { fix n :: nat assume "1 < n"
+        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
+          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
+        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
+          by (simp add: x_def)
+        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
+          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
+        also have "\<dots> = (x n + 1) ^ n"
+          by (simp add: binomial_ring)
+        also have "\<dots> = c"
+          using `1 < n` `1 \<le> c` by (simp add: x_def)
+        finally have "x n \<le> c / n"
+          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
+      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
+        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
+      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
+        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
+    qed
+    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
+      by (simp add: x_def) }
+  note ge_1 = this
+
+  show ?thesis
+  proof cases
+    assume "1 \<le> c" with ge_1 show ?thesis by blast
+  next
+    assume "\<not> 1 \<le> c"
+    with `0 < c` have "1 \<le> 1 / c"
+      by simp
+    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
+      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
+    then show ?thesis
+      by (rule filterlim_cong[THEN iffD1, rotated 3])
+         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
+  qed
+qed
+
+end
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue May 20 19:24:39 2014 +0200
@@ -1220,6 +1220,39 @@
   by (metis INF_absorb centre_in_ball)
 
 
+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])
+
 subsection {* monoset *}
 
 definition (in order) mono_set:
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue May 20 19:24:39 2014 +0200
@@ -700,5 +700,41 @@
       by simp
   qed
 qed
+  
+lemma sets_pair_countable:
+  assumes "countable S1" "countable S2"
+  assumes M: "sets M = Pow S1" and N: "sets N = Pow S2"
+  shows "sets (M \<Otimes>\<^sub>M N) = Pow (S1 \<times> S2)"
+proof auto
+  fix x a b assume x: "x \<in> sets (M \<Otimes>\<^sub>M N)" "(a, b) \<in> x"
+  from sets.sets_into_space[OF x(1)] x(2)
+    sets_eq_imp_space_eq[of N "count_space S2"] sets_eq_imp_space_eq[of M "count_space S1"] M N
+  show "a \<in> S1" "b \<in> S2"
+    by (auto simp: space_pair_measure)
+next
+  fix X assume X: "X \<subseteq> S1 \<times> S2"
+  then have "countable X"
+    by (metis countable_subset `countable S1` `countable S2` countable_SIGMA)
+  have "X = (\<Union>(a, b)\<in>X. {a} \<times> {b})" by auto
+  also have "\<dots> \<in> sets (M \<Otimes>\<^sub>M N)"
+    using X
+    by (safe intro!: sets.countable_UN' `countable X` subsetI pair_measureI) (auto simp: M N)
+  finally show "X \<in> sets (M \<Otimes>\<^sub>M N)" .
+qed
+
+lemma pair_measure_countable:
+  assumes "countable S1" "countable S2"
+  shows "count_space S1 \<Otimes>\<^sub>M count_space S2 = count_space (S1 \<times> S2)"
+proof (rule pair_measure_eqI)
+  show "sigma_finite_measure (count_space S1)" "sigma_finite_measure (count_space S2)"
+    using assms by (auto intro!: sigma_finite_measure_count_space_countable)
+  show "sets (count_space S1 \<Otimes>\<^sub>M count_space S2) = sets (count_space (S1 \<times> S2))"
+    by (subst sets_pair_countable[OF assms]) auto
+next
+  fix A B assume "A \<in> sets (count_space S1)" "B \<in> sets (count_space S2)"
+  then show "emeasure (count_space S1) A * emeasure (count_space S2) B = 
+    emeasure (count_space (S1 \<times> S2)) (A \<times> B)"
+    by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff)
+qed
 
 end
\ No newline at end of file
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Tue May 20 19:24:39 2014 +0200
@@ -1519,6 +1519,39 @@
     integral\<^sup>L M f \<le> integral\<^sup>L M g"
   by (intro integral_mono_AE) auto
 
+lemma (in finite_measure) integrable_measure: 
+  assumes I: "disjoint_family_on X I" "countable I"
+  shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
+proof -
+  have "(\<integral>\<^sup>+i. measure M (X i) \<partial>count_space I) = (\<integral>\<^sup>+i. measure M (if X i \<in> sets M then X i else {}) \<partial>count_space I)"
+    by (auto intro!: nn_integral_cong measure_notin_sets)
+  also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
+    using I unfolding emeasure_eq_measure[symmetric]
+    by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
+  finally show ?thesis
+    by (auto intro!: integrableI_bounded simp: measure_nonneg)
+qed
+
+lemma integrableI_real_bounded:
+  assumes f: "f \<in> borel_measurable M" and ae: "AE x in M. 0 \<le> f x" and fin: "integral\<^sup>N M f < \<infinity>"
+  shows "integrable M f"
+proof (rule integrableI_bounded)
+  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ereal (f x) \<partial>M"
+    using ae by (auto intro: nn_integral_cong_AE)
+  also note fin
+  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
+qed fact
+
+lemma integral_real_bounded:
+  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
+  shows "integral\<^sup>L M f \<le> r"
+proof -
+  have "integrable M f"
+    using assms by (intro integrableI_real_bounded) auto
+  from nn_integral_eq_integral[OF this] assms show ?thesis
+    by simp
+qed
+
 subsection {* Measure spaces with an associated density *}
 
 lemma integrable_density:
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue May 20 19:24:39 2014 +0200
@@ -497,6 +497,10 @@
     using A X by (auto intro!: measurable_sets)
 qed (insert X, auto simp add: PiE_def dest: measurable_space)
 
+lemma measurable_abs_UNIV: 
+  "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
+  by (intro measurable_PiM_single) (auto dest: measurable_space)
+
 lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
   by (intro measurable_restrict measurable_component_singleton) auto
 
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Measurable.thy	Tue May 20 19:24:39 2014 +0200
@@ -330,6 +330,31 @@
   "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
   by simp
 
+lemma measurable_card[measurable]:
+  fixes S :: "'a \<Rightarrow> nat set"
+  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
+  shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)"
+  unfolding measurable_count_space_eq2_countable
+proof safe
+  fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M"
+  proof (cases n)
+    case 0
+    then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M = {x\<in>space M. infinite (S x) \<or> (\<forall>i. i \<notin> S x)}"
+      by auto
+    also have "\<dots> \<in> sets M"
+      by measurable
+    finally show ?thesis .
+  next
+    case (Suc i)
+    then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M =
+      (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})"
+      unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
+    also have "\<dots> \<in> sets M"
+      by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
+    finally show ?thesis .
+  qed
+qed rule
+
 subsection {* Measurability for (co)inductive predicates *}
 
 lemma measurable_lfp:
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Tue May 20 19:24:39 2014 +0200
@@ -1632,15 +1632,24 @@
 lemma AE_count_space: "(AE x in count_space A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
   unfolding eventually_ae_filter by (auto simp add: null_sets_count_space)
 
-lemma sigma_finite_measure_count_space:
-  fixes A :: "'a::countable set"
+lemma sigma_finite_measure_count_space_countable:
+  assumes A: "countable A"
   shows "sigma_finite_measure (count_space A)"
 proof
   show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (count_space A) \<and> (\<Union>i. F i) = space (count_space A) \<and>
      (\<forall>i. emeasure (count_space A) (F i) \<noteq> \<infinity>)"
-     using surj_from_nat by (intro exI[of _ "\<lambda>i. {from_nat i} \<inter> A"]) (auto simp del: surj_from_nat)
+     using A
+     apply (intro exI[of _ "\<lambda>i. {from_nat_into A i} \<inter> A"])
+     apply auto
+     apply (rule_tac x="to_nat_on A x" in exI)
+     apply simp
+     done
 qed
 
+lemma sigma_finite_measure_count_space:
+  fixes A :: "'a::countable set" shows "sigma_finite_measure (count_space A)"
+  by (rule sigma_finite_measure_count_space_countable) auto
+
 lemma finite_measure_count_space:
   assumes [simp]: "finite A"
   shows "finite_measure (count_space A)"
@@ -1656,28 +1665,26 @@
 subsection {* Measure restricted to space *}
 
 lemma emeasure_restrict_space:
-  assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
+  assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
   shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
 proof cases
   assume "A \<in> sets M"
-  
-  have "emeasure (restrict_space M \<Omega>) A = emeasure M (A \<inter> \<Omega>)"
+  show ?thesis
   proof (rule emeasure_measure_of[OF restrict_space_def])
-    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow \<Omega>" "A \<in> sets (restrict_space M \<Omega>)"
-      using assms `A \<in> sets M` by (auto simp: sets_restrict_space sets.sets_into_space)
-    show "positive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
+    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
+      using `A \<subseteq> \<Omega>` `A \<in> sets M` sets.space_closed by (auto simp: sets_restrict_space)
+    show "positive (sets (restrict_space M \<Omega>)) (emeasure M)"
       by (auto simp: positive_def emeasure_nonneg)
-    show "countably_additive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
+    show "countably_additive (sets (restrict_space M \<Omega>)) (emeasure M)"
     proof (rule countably_additiveI)
       fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> sets (restrict_space M \<Omega>)" "disjoint_family A"
       with assms have "\<And>i. A i \<in> sets M" "\<And>i. A i \<subseteq> space M" "disjoint_family A"
-        by (auto simp: sets_restrict_space_iff subset_eq dest: sets.sets_into_space)
-      with `\<Omega> \<in> sets M` show "(\<Sum>i. emeasure M (A i \<inter> \<Omega>)) = emeasure M ((\<Union>i. A i) \<inter> \<Omega>)"
+        by (fastforce simp: sets_restrict_space_iff[OF assms(1)] image_subset_iff
+                      dest: sets.sets_into_space)+
+      then show "(\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
         by (subst suminf_emeasure) (auto simp: disjoint_family_subset)
     qed
   qed
-  with `A \<subseteq> \<Omega>` show ?thesis
-    by (simp add: Int_absorb2)
 next
   assume "A \<notin> sets M"
   moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
@@ -1686,15 +1693,28 @@
     by (simp add: emeasure_notin_sets)
 qed
 
-lemma restrict_count_space:
-  assumes "A \<subseteq> B" shows "restrict_space (count_space B) A = count_space A"
+lemma restrict_restrict_space:
+  assumes "A \<inter> space M \<in> sets M" "B \<inter> space M \<in> sets M"
+  shows "restrict_space (restrict_space M A) B = restrict_space M (A \<inter> B)" (is "?l = ?r")
+proof (rule measure_eqI[symmetric])
+  show "sets ?r = sets ?l"
+    unfolding sets_restrict_space image_comp by (intro image_cong) auto
+next
+  fix X assume "X \<in> sets (restrict_space M (A \<inter> B))"
+  then obtain Y where "Y \<in> sets M" "X = Y \<inter> A \<inter> B"
+    by (auto simp: sets_restrict_space)
+  with assms sets.Int[OF assms] show "emeasure ?r X = emeasure ?l X"
+    by (subst (1 2) emeasure_restrict_space)
+       (auto simp: space_restrict_space sets_restrict_space_iff emeasure_restrict_space ac_simps)
+qed
+
+lemma restrict_count_space: "restrict_space (count_space B) A = count_space (A \<inter> B)"
 proof (rule measure_eqI)
-  show "sets (restrict_space (count_space B) A) = sets (count_space A)"
-    using `A \<subseteq> B` by (subst sets_restrict_space) auto
+  show "sets (restrict_space (count_space B) A) = sets (count_space (A \<inter> B))"
+    by (subst sets_restrict_space) auto
   moreover fix X assume "X \<in> sets (restrict_space (count_space B) A)"
-  moreover note `A \<subseteq> B`
-  ultimately have "X \<subseteq> A" by auto
-  with `A \<subseteq> B` show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space A) X"
+  ultimately have "X \<subseteq> A \<inter> B" by auto
+  then show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space (A \<inter> B)) X"
     by (cases "finite X") (auto simp add: emeasure_restrict_space)
 qed
 
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue May 20 19:24:39 2014 +0200
@@ -745,8 +745,7 @@
 translations
   "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
 
-lemma nn_integral_nonneg:
-  "0 \<le> integral\<^sup>N M f"
+lemma nn_integral_nonneg: "0 \<le> integral\<^sup>N M f"
   by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
 
 lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
@@ -1389,6 +1388,20 @@
     by (rule ereal_mono_minus_cancel) (intro w nn_integral_nonneg)+
 qed
 
+lemma nn_integral_LIMSEQ:
+  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>n x. 0 \<le> f n x"
+    and u: "\<And>x. (\<lambda>i. f i x) ----> u x"
+  shows "(\<lambda>n. integral\<^sup>N M (f n)) ----> integral\<^sup>N M u"
+proof -
+  have "(\<lambda>n. integral\<^sup>N M (f n)) ----> (SUP n. integral\<^sup>N M (f n))"
+    using f by (intro LIMSEQ_SUP[of "\<lambda>n. integral\<^sup>N M (f n)"] incseq_nn_integral)
+  also have "(SUP n. integral\<^sup>N M (f n)) = integral\<^sup>N M (\<lambda>x. SUP n. f n x)"
+    using f by (intro nn_integral_monotone_convergence_SUP[symmetric])
+  also have "integral\<^sup>N M (\<lambda>x. SUP n. f n x) = integral\<^sup>N M (\<lambda>x. u x)"
+    using f by (subst SUP_Lim_ereal[OF _ u]) (auto simp: incseq_def le_fun_def)
+  finally show ?thesis .
+qed
+
 lemma nn_integral_dominated_convergence:
   assumes [measurable]:
        "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
@@ -1668,6 +1681,56 @@
   finally show ?thesis .
 qed
 
+lemma nn_integral_count_space_nat:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes nonneg: "\<And>i. 0 \<le> f i"
+  shows "(\<integral>\<^sup>+i. f i \<partial>count_space UNIV) = (\<Sum>i. f i)"
+proof -
+  have "(\<integral>\<^sup>+i. f i \<partial>count_space UNIV) =
+    (\<integral>\<^sup>+i. (\<Sum>j. f j * indicator {j} i) \<partial>count_space UNIV)"
+  proof (intro nn_integral_cong)
+    fix i
+    have "f i = (\<Sum>j\<in>{i}. f j * indicator {j} i)"
+      by simp
+    also have "\<dots> = (\<Sum>j. f j * indicator {j} i)"
+      by (rule suminf_finite[symmetric]) auto
+    finally show "f i = (\<Sum>j. f j * indicator {j} i)" .
+  qed
+  also have "\<dots> = (\<Sum>j. (\<integral>\<^sup>+i. f j * indicator {j} i \<partial>count_space UNIV))"
+    by (rule nn_integral_suminf) (auto simp: nonneg)
+  also have "\<dots> = (\<Sum>j. f j)"
+    by (simp add: nonneg nn_integral_cmult_indicator one_ereal_def[symmetric])
+  finally show ?thesis .
+qed
+
+lemma emeasure_countable_singleton:
+  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" and X: "countable X"
+  shows "emeasure M X = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)"
+proof -
+  have "emeasure M (\<Union>i\<in>X. {i}) = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)"
+    using assms by (intro emeasure_UN_countable) (auto simp: disjoint_family_on_def)
+  also have "(\<Union>i\<in>X. {i}) = X" by auto
+  finally show ?thesis .
+qed
+
+lemma measure_eqI_countable:
+  assumes [simp]: "sets M = Pow A" "sets N = Pow A" and A: "countable A"
+  assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
+  shows "M = N"
+proof (rule measure_eqI)
+  fix X assume "X \<in> sets M"
+  then have X: "X \<subseteq> A" by auto
+  moreover with A have "countable X" by (auto dest: countable_subset)
+  ultimately have
+    "emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)"
+    "emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
+    by (auto intro!: emeasure_countable_singleton)
+  moreover have "(\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X) = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
+    using X by (intro nn_integral_cong eq) auto
+  ultimately show "emeasure M X = emeasure N X"
+    by simp
+qed simp
+
 subsubsection {* Measures with Restricted Space *}
 
 lemma nn_integral_restrict_space:
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Tue May 20 19:24:39 2014 +0200
@@ -111,6 +111,26 @@
   then show False by auto
 qed
 
+lemma (in prob_space) integral_ge_const:
+  fixes c :: real
+  shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)"
+  using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp
+
+lemma (in prob_space) integral_le_const:
+  fixes c :: real
+  shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c"
+  using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp
+
+lemma (in prob_space) nn_integral_ge_const:
+  "(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
+  using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
+  by (simp add: nn_integral_const_If split: split_if_asm)
+
+lemma (in prob_space) nn_integral_le_const:
+  "0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
+  using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1
+  by (simp add: nn_integral_const_If split: split_if_asm)
+
 lemma (in prob_space) expectation_less:
   fixes X :: "_ \<Rightarrow> real"
   assumes [simp]: "integrable M X"
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 20 19:24:39 2014 +0200
@@ -2299,29 +2299,50 @@
 
 subsubsection {* Restricted Space Sigma Algebra *}
 
-definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
+definition restrict_space where
+  "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) ((op \<inter> \<Omega>) ` sets M) (emeasure M)"
 
-lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
-  unfolding restrict_space_def by (subst space_measure_of) auto
+lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
+  using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
+
+lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
+  by (simp add: space_restrict_space sets.sets_into_space)
 
-lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
-  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
-  unfolding restrict_space_def
-  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
+lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
+proof -
+  have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) =
+    (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
+    using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M]
+    by (simp add: sets.sigma_sets_eq)
+  moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
+    using sets.sets_into_space by (intro image_cong) auto
+  ultimately show ?thesis
+    using sets.sets_into_space[of _ M] unfolding restrict_space_def
+    by (subst sets_measure_of) fastforce+
+qed
 
 lemma sets_restrict_space_iff:
-  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
-  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
+  "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
+proof (subst sets_restrict_space, safe)
+  fix A assume "\<Omega> \<inter> space M \<in> sets M" and A: "A \<in> sets M"
+  then have "(\<Omega> \<inter> space M) \<inter> A \<in> sets M"
+    by rule
+  also have "(\<Omega> \<inter> space M) \<inter> A = \<Omega> \<inter> A"
+    using sets.sets_into_space[OF A] by auto
+  finally show "\<Omega> \<inter> A \<in> sets M"
+    by auto
+qed auto
 
 lemma measurable_restrict_space1:
-  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" and f: "f \<in> measurable M N"
+  shows "f \<in> measurable (restrict_space M \<Omega>) N"
   unfolding measurable_def
 proof (intro CollectI conjI ballI)
   show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
     using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
 
   fix A assume "A \<in> sets N"
-  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
+  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> (\<Omega> \<inter> space M)"
     using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
   also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
     unfolding sets_restrict_space_iff[OF \<Omega>]
@@ -2330,7 +2351,9 @@
 qed
 
 lemma measurable_restrict_space2:
-  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)"
+  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
+    f \<in> measurable M (restrict_space N \<Omega>)"
   by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
 
 end
+
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Series.thy	Tue May 20 19:24:39 2014 +0200
@@ -316,6 +316,21 @@
 
 end
 
+context
+  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
+begin
+
+lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
+  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
+
+lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
+  using sums_unique[OF sums_setsum, OF summable_sums] by simp
+
+lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
+  using sums_summable[OF sums_setsum[OF summable_sums]] .
+
+end
+
 lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   unfolding sums_def by (drule tendsto, simp only: setsum)
 
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue May 20 19:24:39 2014 +0200
@@ -1230,6 +1230,22 @@
   "filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
   by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
 
+lemma eventually_nhds_top:
+  fixes P :: "'a :: {order_top, linorder_topology} \<Rightarrow> bool"
+  assumes "(b::'a) < top"
+  shows "eventually P (nhds top) \<longleftrightarrow> (\<exists>b<top. (\<forall>z. b < z \<longrightarrow> P z))"
+  unfolding eventually_nhds
+proof safe
+  fix S :: "'a set" assume "open S" "top \<in> S"
+  note open_left[OF this `b < top`]
+  moreover assume "\<forall>s\<in>S. P s"
+  ultimately show "\<exists>b<top. \<forall>z>b. P z"
+    by (auto simp: subset_eq Ball_def)
+next
+  fix b assume "b < top" "\<forall>z>b. P z"
+  then show "\<exists>S. open S \<and> top \<in> S \<and> (\<forall>xa\<in>S. P xa)"
+    by (intro exI[of _ "{b <..}"]) auto
+qed
 
 subsection {* Limits on sequences *}
 
@@ -1724,6 +1740,50 @@
    (X -- a --> (L::'b::topological_space))"
   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
 
+lemma sequentially_imp_eventually_at_left:
+  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
+  assumes b[simp]: "b < a"
+  assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
+  shows "eventually P (at_left a)"
+proof (safe intro!: sequentially_imp_eventually_within)
+  fix X assume X: "\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a" "X ----> a"
+  show "eventually (\<lambda>n. P (X n)) sequentially"
+  proof (rule ccontr)
+    assume "\<not> eventually (\<lambda>n. P (X n)) sequentially"
+    from not_eventually_sequentiallyD[OF this]
+    obtain r where "subseq r" "\<And>n. \<not> P (X (r n))"
+      by auto
+    with X have "(X \<circ> r) ----> a"
+      by (auto intro: LIMSEQ_subseq_LIMSEQ)
+    from order_tendstoD(1)[OF this] obtain s' where s': "\<And>b i. b < a \<Longrightarrow> s' b \<le> i \<Longrightarrow> b < X (r i)"
+      unfolding eventually_sequentially comp_def by metis
+    def s \<equiv> "rec_nat (s' b) (\<lambda>_ i. max (s' (X (r i))) (Suc i))"
+    then have [simp]: "s 0 = s' b" "\<And>n. s (Suc n) = max (s' (X (r (s n)))) (Suc (s n))"
+      by auto
+    have "eventually (\<lambda>n. P (((X \<circ> r) \<circ> s) n)) sequentially"
+    proof (rule *)
+      from X show inc: "incseq (X \<circ> r \<circ> s)"
+        unfolding incseq_Suc_iff comp_def by (intro allI s'[THEN less_imp_le]) auto
+      { fix n show "b < (X \<circ> r \<circ> s) n"
+          using inc[THEN incseqD, of 0 n] s'[OF b order_refl] by simp }
+      { fix n show "(X \<circ> r \<circ> s) n < a"
+          using X by simp }
+      from `(X \<circ> r) ----> a` show "(X \<circ> r \<circ> s) ----> a"
+        by (rule LIMSEQ_subseq_LIMSEQ) (auto simp: subseq_Suc_iff)
+    qed
+    with `\<And>n. \<not> P (X (r n))` show False
+      by auto
+  qed
+qed
+
+lemma tendsto_at_left_sequentially:
+  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
+  assumes "b < a"
+  assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
+  shows "(X ---> L) (at_left a)"
+  using assms unfolding tendsto_def [where l=L]
+  by (simp add: sequentially_imp_eventually_at_left)
+
 subsection {* Continuity *}
 
 subsubsection {* Continuity on a set *}
diff -r c9e98c2498fd -r e7fd64f82876 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue May 20 16:52:59 2014 +0200
+++ b/src/HOL/Transcendental.thy	Tue May 20 19:24:39 2014 +0200
@@ -10,6 +10,32 @@
 imports Fact Series Deriv NthRoot
 begin
 
+lemma root_test_convergence:
+  fixes f :: "nat \<Rightarrow> 'a::banach"
+  assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
+  assumes "x < 1"
+  shows "summable f"
+proof -
+  have "0 \<le> x"
+    by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
+  from `x < 1` obtain z where z: "x < z" "z < 1"
+    by (metis dense)
+  from f `x < z`
+  have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
+    by (rule order_tendstoD)
+  then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
+    using eventually_ge_at_top
+  proof eventually_elim
+    fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
+    from power_strict_mono[OF less, of n] n
+    show "norm (f n) \<le> z ^ n"
+      by simp
+  qed
+  then show "summable f"
+    unfolding eventually_sequentially
+    using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
+qed
+
 subsection {* Properties of Power Series *}
 
 lemma lemma_realpow_diff: