add various lemmas
authorhoelzl
Tue May 20 19:24:39 2014 +0200 (2014-05-20)
changeset 57025e7fd64f82876
parent 57024 c9e98c2498fd
child 57026 90a3e39be0ca
add various lemmas
src/HOL/Finite_Set.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Library.thy
src/HOL/Library/NthRoot_Limits.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -415,10 +415,13 @@
     1.4      by (auto simp add: finite_conv_nat_seg_image)
     1.5  qed
     1.6  
     1.7 +lemma finite_cartesian_product_iff:
     1.8 +  "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))"
     1.9 +  by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
    1.10 +
    1.11  lemma finite_prod: 
    1.12    "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
    1.13 -by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV 
    1.14 -   dest: finite_cartesian_productD1 finite_cartesian_productD2)
    1.15 +  using finite_cartesian_product_iff[of UNIV UNIV] by simp
    1.16  
    1.17  lemma finite_Pow_iff [iff]:
    1.18    "finite (Pow A) \<longleftrightarrow> finite A"
     2.1 --- a/src/HOL/Library/Countable_Set.thy	Tue May 20 16:52:59 2014 +0200
     2.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue May 20 19:24:39 2014 +0200
     2.3 @@ -283,4 +283,17 @@
     2.4    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))"
     2.5    using S[THEN subset_range_from_nat_into] by auto
     2.6  
     2.7 +lemma finite_sequence_to_countable_set:
     2.8 +   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"
     2.9 +proof -  show thesis
    2.10 +    apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
    2.11 +    apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
    2.12 +  proof -
    2.13 +    fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
    2.14 +    with from_nat_into_surj[OF `countable X` `x \<in> X`]
    2.15 +    show False
    2.16 +      by auto
    2.17 +  qed
    2.18 +qed
    2.19 +
    2.20  end
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Tue May 20 16:52:59 2014 +0200
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue May 20 19:24:39 2014 +0200
     3.3 @@ -2168,6 +2168,10 @@
     3.4      by (auto simp: order_tendsto_iff)
     3.5  qed
     3.6  
     3.7 +lemma tendsto_PInfty_eq_at_top:
     3.8 +  "((\<lambda>z. ereal (f z)) ---> \<infinity>) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
     3.9 +  unfolding tendsto_PInfty filterlim_at_top_dense by simp
    3.10 +
    3.11  lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
    3.12    unfolding tendsto_def
    3.13  proof safe
     4.1 --- a/src/HOL/Library/Library.thy	Tue May 20 16:52:59 2014 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Tue May 20 19:24:39 2014 +0200
     4.3 @@ -39,6 +39,7 @@
     4.4    Monad_Syntax
     4.5    Multiset
     4.6    Numeral_Type
     4.7 +  NthRoot_Limits
     4.8    OptionalSugar
     4.9    Option_ord
    4.10    Order_Continuity
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/NthRoot_Limits.thy	Tue May 20 19:24:39 2014 +0200
     5.3 @@ -0,0 +1,94 @@
     5.4 +theory NthRoot_Limits
     5.5 +  imports Complex_Main "~~/src/HOL/Number_Theory/Binomial"
     5.6 +begin
     5.7 +
     5.8 +text {*
     5.9 +
    5.10 +This does not fit into @{text Complex_Main}, as it depends on @{text Binomial}
    5.11 +
    5.12 +*}
    5.13 +
    5.14 +lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
    5.15 +proof -
    5.16 +  def x \<equiv> "\<lambda>n. root n n - 1"
    5.17 +  have "x ----> sqrt 0"
    5.18 +  proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    5.19 +    show "(\<lambda>x. sqrt (2 / x)) ----> sqrt 0"
    5.20 +      by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    5.21 +         (simp_all add: at_infinity_eq_at_top_bot)
    5.22 +    { fix n :: nat assume "2 < n"
    5.23 +      have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
    5.24 +        using `2 < n` unfolding gbinomial_def binomial_gbinomial
    5.25 +        by (simp add: atLeast0AtMost atMost_Suc field_simps real_of_nat_diff numeral_2_eq_2 real_eq_of_nat[symmetric])
    5.26 +      also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    5.27 +        by (simp add: x_def)
    5.28 +      also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    5.29 +        using `2 < n` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    5.30 +      also have "\<dots> = (x n + 1) ^ n"
    5.31 +        by (simp add: binomial_ring)
    5.32 +      also have "\<dots> = n"
    5.33 +        using `2 < n` by (simp add: x_def)
    5.34 +      finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
    5.35 +        by simp
    5.36 +      then have "(x n)\<^sup>2 \<le> 2 / real n"
    5.37 +        using `2 < n` unfolding mult_le_cancel_left by (simp add: field_simps)
    5.38 +      from real_sqrt_le_mono[OF this] have "x n \<le> sqrt (2 / real n)"
    5.39 +        by simp }
    5.40 +    then show "eventually (\<lambda>n. x n \<le> sqrt (2 / real n)) sequentially"
    5.41 +      by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    5.42 +    show "eventually (\<lambda>n. sqrt 0 \<le> x n) sequentially"
    5.43 +      by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    5.44 +  qed
    5.45 +  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis
    5.46 +    by (simp add: x_def)
    5.47 +qed
    5.48 +
    5.49 +lemma LIMSEQ_root_const:
    5.50 +  assumes "0 < c"
    5.51 +  shows "(\<lambda>n. root n c) ----> 1"
    5.52 +proof -
    5.53 +  { fix c :: real assume "1 \<le> c"
    5.54 +    def x \<equiv> "\<lambda>n. root n c - 1"
    5.55 +    have "x ----> 0"
    5.56 +    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    5.57 +      show "(\<lambda>n. c / n) ----> 0"
    5.58 +        by (intro tendsto_divide_0[OF tendsto_const] filterlim_mono[OF filterlim_real_sequentially])
    5.59 +           (simp_all add: at_infinity_eq_at_top_bot)
    5.60 +      { fix n :: nat assume "1 < n"
    5.61 +        have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
    5.62 +          using `1 < n` unfolding gbinomial_def binomial_gbinomial by (simp add: real_eq_of_nat[symmetric])
    5.63 +        also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
    5.64 +          by (simp add: x_def)
    5.65 +        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
    5.66 +          using `1 < n` `1 \<le> c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
    5.67 +        also have "\<dots> = (x n + 1) ^ n"
    5.68 +          by (simp add: binomial_ring)
    5.69 +        also have "\<dots> = c"
    5.70 +          using `1 < n` `1 \<le> c` by (simp add: x_def)
    5.71 +        finally have "x n \<le> c / n"
    5.72 +          using `1 \<le> c` `1 < n` by (simp add: field_simps) }
    5.73 +      then show "eventually (\<lambda>n. x n \<le> c / n) sequentially"
    5.74 +        by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
    5.75 +      show "eventually (\<lambda>n. 0 \<le> x n) sequentially"
    5.76 +        using `1 \<le> c` by (auto intro!: exI[of _ 1] simp: eventually_sequentially le_diff_eq x_def)
    5.77 +    qed
    5.78 +    from tendsto_add[OF this tendsto_const[of 1]] have "(\<lambda>n. root n c) ----> 1"
    5.79 +      by (simp add: x_def) }
    5.80 +  note ge_1 = this
    5.81 +
    5.82 +  show ?thesis
    5.83 +  proof cases
    5.84 +    assume "1 \<le> c" with ge_1 show ?thesis by blast
    5.85 +  next
    5.86 +    assume "\<not> 1 \<le> c"
    5.87 +    with `0 < c` have "1 \<le> 1 / c"
    5.88 +      by simp
    5.89 +    then have "(\<lambda>n. 1 / root n (1 / c)) ----> 1 / 1"
    5.90 +      by (intro tendsto_divide tendsto_const ge_1 `1 \<le> 1 / c` one_neq_zero)
    5.91 +    then show ?thesis
    5.92 +      by (rule filterlim_cong[THEN iffD1, rotated 3])
    5.93 +         (auto intro!: exI[of _ 1] simp: eventually_sequentially real_root_divide)
    5.94 +  qed
    5.95 +qed
    5.96 +
    5.97 +end
     6.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue May 20 16:52:59 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue May 20 19:24:39 2014 +0200
     6.3 @@ -1220,6 +1220,39 @@
     6.4    by (metis INF_absorb centre_in_ball)
     6.5  
     6.6  
     6.7 +lemma suminf_ereal_offset_le:
     6.8 +  fixes f :: "nat \<Rightarrow> ereal"
     6.9 +  assumes f: "\<And>i. 0 \<le> f i"
    6.10 +  shows "(\<Sum>i. f (i + k)) \<le> suminf f"
    6.11 +proof -
    6.12 +  have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
    6.13 +    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
    6.14 +  moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
    6.15 +    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
    6.16 +  then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
    6.17 +    by (rule LIMSEQ_ignore_initial_segment)
    6.18 +  ultimately show ?thesis
    6.19 +  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
    6.20 +    fix n assume "k \<le> n"
    6.21 +    have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
    6.22 +      by simp
    6.23 +    also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
    6.24 +      by (subst setsum_reindex) auto
    6.25 +    also have "\<dots> \<le> setsum f {..<n + k}"
    6.26 +      by (intro setsum_mono3) (auto simp: f)
    6.27 +    finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
    6.28 +  qed
    6.29 +qed
    6.30 +
    6.31 +lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
    6.32 +  by (metis sums_ereal sums_unique)
    6.33 +
    6.34 +lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
    6.35 +  by (metis sums_ereal sums_unique summable_def)
    6.36 +
    6.37 +lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
    6.38 +  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
    6.39 +
    6.40  subsection {* monoset *}
    6.41  
    6.42  definition (in order) mono_set:
     7.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue May 20 16:52:59 2014 +0200
     7.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue May 20 19:24:39 2014 +0200
     7.3 @@ -700,5 +700,41 @@
     7.4        by simp
     7.5    qed
     7.6  qed
     7.7 +  
     7.8 +lemma sets_pair_countable:
     7.9 +  assumes "countable S1" "countable S2"
    7.10 +  assumes M: "sets M = Pow S1" and N: "sets N = Pow S2"
    7.11 +  shows "sets (M \<Otimes>\<^sub>M N) = Pow (S1 \<times> S2)"
    7.12 +proof auto
    7.13 +  fix x a b assume x: "x \<in> sets (M \<Otimes>\<^sub>M N)" "(a, b) \<in> x"
    7.14 +  from sets.sets_into_space[OF x(1)] x(2)
    7.15 +    sets_eq_imp_space_eq[of N "count_space S2"] sets_eq_imp_space_eq[of M "count_space S1"] M N
    7.16 +  show "a \<in> S1" "b \<in> S2"
    7.17 +    by (auto simp: space_pair_measure)
    7.18 +next
    7.19 +  fix X assume X: "X \<subseteq> S1 \<times> S2"
    7.20 +  then have "countable X"
    7.21 +    by (metis countable_subset `countable S1` `countable S2` countable_SIGMA)
    7.22 +  have "X = (\<Union>(a, b)\<in>X. {a} \<times> {b})" by auto
    7.23 +  also have "\<dots> \<in> sets (M \<Otimes>\<^sub>M N)"
    7.24 +    using X
    7.25 +    by (safe intro!: sets.countable_UN' `countable X` subsetI pair_measureI) (auto simp: M N)
    7.26 +  finally show "X \<in> sets (M \<Otimes>\<^sub>M N)" .
    7.27 +qed
    7.28 +
    7.29 +lemma pair_measure_countable:
    7.30 +  assumes "countable S1" "countable S2"
    7.31 +  shows "count_space S1 \<Otimes>\<^sub>M count_space S2 = count_space (S1 \<times> S2)"
    7.32 +proof (rule pair_measure_eqI)
    7.33 +  show "sigma_finite_measure (count_space S1)" "sigma_finite_measure (count_space S2)"
    7.34 +    using assms by (auto intro!: sigma_finite_measure_count_space_countable)
    7.35 +  show "sets (count_space S1 \<Otimes>\<^sub>M count_space S2) = sets (count_space (S1 \<times> S2))"
    7.36 +    by (subst sets_pair_countable[OF assms]) auto
    7.37 +next
    7.38 +  fix A B assume "A \<in> sets (count_space S1)" "B \<in> sets (count_space S2)"
    7.39 +  then show "emeasure (count_space S1) A * emeasure (count_space S2) B = 
    7.40 +    emeasure (count_space (S1 \<times> S2)) (A \<times> B)"
    7.41 +    by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff)
    7.42 +qed
    7.43  
    7.44  end
    7.45 \ No newline at end of file
     8.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue May 20 16:52:59 2014 +0200
     8.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue May 20 19:24:39 2014 +0200
     8.3 @@ -1519,6 +1519,39 @@
     8.4      integral\<^sup>L M f \<le> integral\<^sup>L M g"
     8.5    by (intro integral_mono_AE) auto
     8.6  
     8.7 +lemma (in finite_measure) integrable_measure: 
     8.8 +  assumes I: "disjoint_family_on X I" "countable I"
     8.9 +  shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
    8.10 +proof -
    8.11 +  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)"
    8.12 +    by (auto intro!: nn_integral_cong measure_notin_sets)
    8.13 +  also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
    8.14 +    using I unfolding emeasure_eq_measure[symmetric]
    8.15 +    by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
    8.16 +  finally show ?thesis
    8.17 +    by (auto intro!: integrableI_bounded simp: measure_nonneg)
    8.18 +qed
    8.19 +
    8.20 +lemma integrableI_real_bounded:
    8.21 +  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>"
    8.22 +  shows "integrable M f"
    8.23 +proof (rule integrableI_bounded)
    8.24 +  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ereal (f x) \<partial>M"
    8.25 +    using ae by (auto intro: nn_integral_cong_AE)
    8.26 +  also note fin
    8.27 +  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
    8.28 +qed fact
    8.29 +
    8.30 +lemma integral_real_bounded:
    8.31 +  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
    8.32 +  shows "integral\<^sup>L M f \<le> r"
    8.33 +proof -
    8.34 +  have "integrable M f"
    8.35 +    using assms by (intro integrableI_real_bounded) auto
    8.36 +  from nn_integral_eq_integral[OF this] assms show ?thesis
    8.37 +    by simp
    8.38 +qed
    8.39 +
    8.40  subsection {* Measure spaces with an associated density *}
    8.41  
    8.42  lemma integrable_density:
     9.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue May 20 16:52:59 2014 +0200
     9.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue May 20 19:24:39 2014 +0200
     9.3 @@ -497,6 +497,10 @@
     9.4      using A X by (auto intro!: measurable_sets)
     9.5  qed (insert X, auto simp add: PiE_def dest: measurable_space)
     9.6  
     9.7 +lemma measurable_abs_UNIV: 
     9.8 +  "(\<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)"
     9.9 +  by (intro measurable_PiM_single) (auto dest: measurable_space)
    9.10 +
    9.11  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)"
    9.12    by (intro measurable_restrict measurable_component_singleton) auto
    9.13  
    10.1 --- a/src/HOL/Probability/Measurable.thy	Tue May 20 16:52:59 2014 +0200
    10.2 +++ b/src/HOL/Probability/Measurable.thy	Tue May 20 19:24:39 2014 +0200
    10.3 @@ -330,6 +330,31 @@
    10.4    "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
    10.5    by simp
    10.6  
    10.7 +lemma measurable_card[measurable]:
    10.8 +  fixes S :: "'a \<Rightarrow> nat set"
    10.9 +  assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
   10.10 +  shows "(\<lambda>x. card (S x)) \<in> measurable M (count_space UNIV)"
   10.11 +  unfolding measurable_count_space_eq2_countable
   10.12 +proof safe
   10.13 +  fix n show "(\<lambda>x. card (S x)) -` {n} \<inter> space M \<in> sets M"
   10.14 +  proof (cases n)
   10.15 +    case 0
   10.16 +    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)}"
   10.17 +      by auto
   10.18 +    also have "\<dots> \<in> sets M"
   10.19 +      by measurable
   10.20 +    finally show ?thesis .
   10.21 +  next
   10.22 +    case (Suc i)
   10.23 +    then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M =
   10.24 +      (\<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)})"
   10.25 +      unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
   10.26 +    also have "\<dots> \<in> sets M"
   10.27 +      by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
   10.28 +    finally show ?thesis .
   10.29 +  qed
   10.30 +qed rule
   10.31 +
   10.32  subsection {* Measurability for (co)inductive predicates *}
   10.33  
   10.34  lemma measurable_lfp:
    11.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue May 20 16:52:59 2014 +0200
    11.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue May 20 19:24:39 2014 +0200
    11.3 @@ -1632,15 +1632,24 @@
    11.4  lemma AE_count_space: "(AE x in count_space A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
    11.5    unfolding eventually_ae_filter by (auto simp add: null_sets_count_space)
    11.6  
    11.7 -lemma sigma_finite_measure_count_space:
    11.8 -  fixes A :: "'a::countable set"
    11.9 +lemma sigma_finite_measure_count_space_countable:
   11.10 +  assumes A: "countable A"
   11.11    shows "sigma_finite_measure (count_space A)"
   11.12  proof
   11.13    show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (count_space A) \<and> (\<Union>i. F i) = space (count_space A) \<and>
   11.14       (\<forall>i. emeasure (count_space A) (F i) \<noteq> \<infinity>)"
   11.15 -     using surj_from_nat by (intro exI[of _ "\<lambda>i. {from_nat i} \<inter> A"]) (auto simp del: surj_from_nat)
   11.16 +     using A
   11.17 +     apply (intro exI[of _ "\<lambda>i. {from_nat_into A i} \<inter> A"])
   11.18 +     apply auto
   11.19 +     apply (rule_tac x="to_nat_on A x" in exI)
   11.20 +     apply simp
   11.21 +     done
   11.22  qed
   11.23  
   11.24 +lemma sigma_finite_measure_count_space:
   11.25 +  fixes A :: "'a::countable set" shows "sigma_finite_measure (count_space A)"
   11.26 +  by (rule sigma_finite_measure_count_space_countable) auto
   11.27 +
   11.28  lemma finite_measure_count_space:
   11.29    assumes [simp]: "finite A"
   11.30    shows "finite_measure (count_space A)"
   11.31 @@ -1656,28 +1665,26 @@
   11.32  subsection {* Measure restricted to space *}
   11.33  
   11.34  lemma emeasure_restrict_space:
   11.35 -  assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
   11.36 +  assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
   11.37    shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
   11.38  proof cases
   11.39    assume "A \<in> sets M"
   11.40 -  
   11.41 -  have "emeasure (restrict_space M \<Omega>) A = emeasure M (A \<inter> \<Omega>)"
   11.42 +  show ?thesis
   11.43    proof (rule emeasure_measure_of[OF restrict_space_def])
   11.44 -    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow \<Omega>" "A \<in> sets (restrict_space M \<Omega>)"
   11.45 -      using assms `A \<in> sets M` by (auto simp: sets_restrict_space sets.sets_into_space)
   11.46 -    show "positive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
   11.47 +    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
   11.48 +      using `A \<subseteq> \<Omega>` `A \<in> sets M` sets.space_closed by (auto simp: sets_restrict_space)
   11.49 +    show "positive (sets (restrict_space M \<Omega>)) (emeasure M)"
   11.50        by (auto simp: positive_def emeasure_nonneg)
   11.51 -    show "countably_additive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
   11.52 +    show "countably_additive (sets (restrict_space M \<Omega>)) (emeasure M)"
   11.53      proof (rule countably_additiveI)
   11.54        fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> sets (restrict_space M \<Omega>)" "disjoint_family A"
   11.55        with assms have "\<And>i. A i \<in> sets M" "\<And>i. A i \<subseteq> space M" "disjoint_family A"
   11.56 -        by (auto simp: sets_restrict_space_iff subset_eq dest: sets.sets_into_space)
   11.57 -      with `\<Omega> \<in> sets M` show "(\<Sum>i. emeasure M (A i \<inter> \<Omega>)) = emeasure M ((\<Union>i. A i) \<inter> \<Omega>)"
   11.58 +        by (fastforce simp: sets_restrict_space_iff[OF assms(1)] image_subset_iff
   11.59 +                      dest: sets.sets_into_space)+
   11.60 +      then show "(\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
   11.61          by (subst suminf_emeasure) (auto simp: disjoint_family_subset)
   11.62      qed
   11.63    qed
   11.64 -  with `A \<subseteq> \<Omega>` show ?thesis
   11.65 -    by (simp add: Int_absorb2)
   11.66  next
   11.67    assume "A \<notin> sets M"
   11.68    moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
   11.69 @@ -1686,15 +1693,28 @@
   11.70      by (simp add: emeasure_notin_sets)
   11.71  qed
   11.72  
   11.73 -lemma restrict_count_space:
   11.74 -  assumes "A \<subseteq> B" shows "restrict_space (count_space B) A = count_space A"
   11.75 +lemma restrict_restrict_space:
   11.76 +  assumes "A \<inter> space M \<in> sets M" "B \<inter> space M \<in> sets M"
   11.77 +  shows "restrict_space (restrict_space M A) B = restrict_space M (A \<inter> B)" (is "?l = ?r")
   11.78 +proof (rule measure_eqI[symmetric])
   11.79 +  show "sets ?r = sets ?l"
   11.80 +    unfolding sets_restrict_space image_comp by (intro image_cong) auto
   11.81 +next
   11.82 +  fix X assume "X \<in> sets (restrict_space M (A \<inter> B))"
   11.83 +  then obtain Y where "Y \<in> sets M" "X = Y \<inter> A \<inter> B"
   11.84 +    by (auto simp: sets_restrict_space)
   11.85 +  with assms sets.Int[OF assms] show "emeasure ?r X = emeasure ?l X"
   11.86 +    by (subst (1 2) emeasure_restrict_space)
   11.87 +       (auto simp: space_restrict_space sets_restrict_space_iff emeasure_restrict_space ac_simps)
   11.88 +qed
   11.89 +
   11.90 +lemma restrict_count_space: "restrict_space (count_space B) A = count_space (A \<inter> B)"
   11.91  proof (rule measure_eqI)
   11.92 -  show "sets (restrict_space (count_space B) A) = sets (count_space A)"
   11.93 -    using `A \<subseteq> B` by (subst sets_restrict_space) auto
   11.94 +  show "sets (restrict_space (count_space B) A) = sets (count_space (A \<inter> B))"
   11.95 +    by (subst sets_restrict_space) auto
   11.96    moreover fix X assume "X \<in> sets (restrict_space (count_space B) A)"
   11.97 -  moreover note `A \<subseteq> B`
   11.98 -  ultimately have "X \<subseteq> A" by auto
   11.99 -  with `A \<subseteq> B` show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space A) X"
  11.100 +  ultimately have "X \<subseteq> A \<inter> B" by auto
  11.101 +  then show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space (A \<inter> B)) X"
  11.102      by (cases "finite X") (auto simp add: emeasure_restrict_space)
  11.103  qed
  11.104  
    12.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue May 20 16:52:59 2014 +0200
    12.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue May 20 19:24:39 2014 +0200
    12.3 @@ -745,8 +745,7 @@
    12.4  translations
    12.5    "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
    12.6  
    12.7 -lemma nn_integral_nonneg:
    12.8 -  "0 \<le> integral\<^sup>N M f"
    12.9 +lemma nn_integral_nonneg: "0 \<le> integral\<^sup>N M f"
   12.10    by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
   12.11  
   12.12  lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
   12.13 @@ -1389,6 +1388,20 @@
   12.14      by (rule ereal_mono_minus_cancel) (intro w nn_integral_nonneg)+
   12.15  qed
   12.16  
   12.17 +lemma nn_integral_LIMSEQ:
   12.18 +  assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>n x. 0 \<le> f n x"
   12.19 +    and u: "\<And>x. (\<lambda>i. f i x) ----> u x"
   12.20 +  shows "(\<lambda>n. integral\<^sup>N M (f n)) ----> integral\<^sup>N M u"
   12.21 +proof -
   12.22 +  have "(\<lambda>n. integral\<^sup>N M (f n)) ----> (SUP n. integral\<^sup>N M (f n))"
   12.23 +    using f by (intro LIMSEQ_SUP[of "\<lambda>n. integral\<^sup>N M (f n)"] incseq_nn_integral)
   12.24 +  also have "(SUP n. integral\<^sup>N M (f n)) = integral\<^sup>N M (\<lambda>x. SUP n. f n x)"
   12.25 +    using f by (intro nn_integral_monotone_convergence_SUP[symmetric])
   12.26 +  also have "integral\<^sup>N M (\<lambda>x. SUP n. f n x) = integral\<^sup>N M (\<lambda>x. u x)"
   12.27 +    using f by (subst SUP_Lim_ereal[OF _ u]) (auto simp: incseq_def le_fun_def)
   12.28 +  finally show ?thesis .
   12.29 +qed
   12.30 +
   12.31  lemma nn_integral_dominated_convergence:
   12.32    assumes [measurable]:
   12.33         "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
   12.34 @@ -1668,6 +1681,56 @@
   12.35    finally show ?thesis .
   12.36  qed
   12.37  
   12.38 +lemma nn_integral_count_space_nat:
   12.39 +  fixes f :: "nat \<Rightarrow> ereal"
   12.40 +  assumes nonneg: "\<And>i. 0 \<le> f i"
   12.41 +  shows "(\<integral>\<^sup>+i. f i \<partial>count_space UNIV) = (\<Sum>i. f i)"
   12.42 +proof -
   12.43 +  have "(\<integral>\<^sup>+i. f i \<partial>count_space UNIV) =
   12.44 +    (\<integral>\<^sup>+i. (\<Sum>j. f j * indicator {j} i) \<partial>count_space UNIV)"
   12.45 +  proof (intro nn_integral_cong)
   12.46 +    fix i
   12.47 +    have "f i = (\<Sum>j\<in>{i}. f j * indicator {j} i)"
   12.48 +      by simp
   12.49 +    also have "\<dots> = (\<Sum>j. f j * indicator {j} i)"
   12.50 +      by (rule suminf_finite[symmetric]) auto
   12.51 +    finally show "f i = (\<Sum>j. f j * indicator {j} i)" .
   12.52 +  qed
   12.53 +  also have "\<dots> = (\<Sum>j. (\<integral>\<^sup>+i. f j * indicator {j} i \<partial>count_space UNIV))"
   12.54 +    by (rule nn_integral_suminf) (auto simp: nonneg)
   12.55 +  also have "\<dots> = (\<Sum>j. f j)"
   12.56 +    by (simp add: nonneg nn_integral_cmult_indicator one_ereal_def[symmetric])
   12.57 +  finally show ?thesis .
   12.58 +qed
   12.59 +
   12.60 +lemma emeasure_countable_singleton:
   12.61 +  assumes sets: "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" and X: "countable X"
   12.62 +  shows "emeasure M X = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)"
   12.63 +proof -
   12.64 +  have "emeasure M (\<Union>i\<in>X. {i}) = (\<integral>\<^sup>+x. emeasure M {x} \<partial>count_space X)"
   12.65 +    using assms by (intro emeasure_UN_countable) (auto simp: disjoint_family_on_def)
   12.66 +  also have "(\<Union>i\<in>X. {i}) = X" by auto
   12.67 +  finally show ?thesis .
   12.68 +qed
   12.69 +
   12.70 +lemma measure_eqI_countable:
   12.71 +  assumes [simp]: "sets M = Pow A" "sets N = Pow A" and A: "countable A"
   12.72 +  assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
   12.73 +  shows "M = N"
   12.74 +proof (rule measure_eqI)
   12.75 +  fix X assume "X \<in> sets M"
   12.76 +  then have X: "X \<subseteq> A" by auto
   12.77 +  moreover with A have "countable X" by (auto dest: countable_subset)
   12.78 +  ultimately have
   12.79 +    "emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)"
   12.80 +    "emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
   12.81 +    by (auto intro!: emeasure_countable_singleton)
   12.82 +  moreover have "(\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X) = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
   12.83 +    using X by (intro nn_integral_cong eq) auto
   12.84 +  ultimately show "emeasure M X = emeasure N X"
   12.85 +    by simp
   12.86 +qed simp
   12.87 +
   12.88  subsubsection {* Measures with Restricted Space *}
   12.89  
   12.90  lemma nn_integral_restrict_space:
    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue May 20 16:52:59 2014 +0200
    13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue May 20 19:24:39 2014 +0200
    13.3 @@ -111,6 +111,26 @@
    13.4    then show False by auto
    13.5  qed
    13.6  
    13.7 +lemma (in prob_space) integral_ge_const:
    13.8 +  fixes c :: real
    13.9 +  shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)"
   13.10 +  using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp
   13.11 +
   13.12 +lemma (in prob_space) integral_le_const:
   13.13 +  fixes c :: real
   13.14 +  shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c"
   13.15 +  using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp
   13.16 +
   13.17 +lemma (in prob_space) nn_integral_ge_const:
   13.18 +  "(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
   13.19 +  using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
   13.20 +  by (simp add: nn_integral_const_If split: split_if_asm)
   13.21 +
   13.22 +lemma (in prob_space) nn_integral_le_const:
   13.23 +  "0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
   13.24 +  using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1
   13.25 +  by (simp add: nn_integral_const_If split: split_if_asm)
   13.26 +
   13.27  lemma (in prob_space) expectation_less:
   13.28    fixes X :: "_ \<Rightarrow> real"
   13.29    assumes [simp]: "integrable M X"
    14.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 20 16:52:59 2014 +0200
    14.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 20 19:24:39 2014 +0200
    14.3 @@ -2299,29 +2299,50 @@
    14.4  
    14.5  subsubsection {* Restricted Space Sigma Algebra *}
    14.6  
    14.7 -definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
    14.8 +definition restrict_space where
    14.9 +  "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) ((op \<inter> \<Omega>) ` sets M) (emeasure M)"
   14.10  
   14.11 -lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
   14.12 -  unfolding restrict_space_def by (subst space_measure_of) auto
   14.13 +lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
   14.14 +  using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
   14.15 +
   14.16 +lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
   14.17 +  by (simp add: space_restrict_space sets.sets_into_space)
   14.18  
   14.19 -lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
   14.20 -  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
   14.21 -  unfolding restrict_space_def
   14.22 -  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
   14.23 +lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
   14.24 +proof -
   14.25 +  have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) =
   14.26 +    (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
   14.27 +    using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M]
   14.28 +    by (simp add: sets.sigma_sets_eq)
   14.29 +  moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
   14.30 +    using sets.sets_into_space by (intro image_cong) auto
   14.31 +  ultimately show ?thesis
   14.32 +    using sets.sets_into_space[of _ M] unfolding restrict_space_def
   14.33 +    by (subst sets_measure_of) fastforce+
   14.34 +qed
   14.35  
   14.36  lemma sets_restrict_space_iff:
   14.37 -  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
   14.38 -  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
   14.39 +  "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
   14.40 +proof (subst sets_restrict_space, safe)
   14.41 +  fix A assume "\<Omega> \<inter> space M \<in> sets M" and A: "A \<in> sets M"
   14.42 +  then have "(\<Omega> \<inter> space M) \<inter> A \<in> sets M"
   14.43 +    by rule
   14.44 +  also have "(\<Omega> \<inter> space M) \<inter> A = \<Omega> \<inter> A"
   14.45 +    using sets.sets_into_space[OF A] by auto
   14.46 +  finally show "\<Omega> \<inter> A \<in> sets M"
   14.47 +    by auto
   14.48 +qed auto
   14.49  
   14.50  lemma measurable_restrict_space1:
   14.51 -  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
   14.52 +  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" and f: "f \<in> measurable M N"
   14.53 +  shows "f \<in> measurable (restrict_space M \<Omega>) N"
   14.54    unfolding measurable_def
   14.55  proof (intro CollectI conjI ballI)
   14.56    show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
   14.57      using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
   14.58  
   14.59    fix A assume "A \<in> sets N"
   14.60 -  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
   14.61 +  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> (\<Omega> \<inter> space M)"
   14.62      using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
   14.63    also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
   14.64      unfolding sets_restrict_space_iff[OF \<Omega>]
   14.65 @@ -2330,7 +2351,9 @@
   14.66  qed
   14.67  
   14.68  lemma measurable_restrict_space2:
   14.69 -  "\<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>)"
   14.70 +  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
   14.71 +    f \<in> measurable M (restrict_space N \<Omega>)"
   14.72    by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
   14.73  
   14.74  end
   14.75 +
    15.1 --- a/src/HOL/Series.thy	Tue May 20 16:52:59 2014 +0200
    15.2 +++ b/src/HOL/Series.thy	Tue May 20 19:24:39 2014 +0200
    15.3 @@ -316,6 +316,21 @@
    15.4  
    15.5  end
    15.6  
    15.7 +context
    15.8 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
    15.9 +begin
   15.10 +
   15.11 +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)"
   15.12 +  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
   15.13 +
   15.14 +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)"
   15.15 +  using sums_unique[OF sums_setsum, OF summable_sums] by simp
   15.16 +
   15.17 +lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
   15.18 +  using sums_summable[OF sums_setsum[OF summable_sums]] .
   15.19 +
   15.20 +end
   15.21 +
   15.22  lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   15.23    unfolding sums_def by (drule tendsto, simp only: setsum)
   15.24  
    16.1 --- a/src/HOL/Topological_Spaces.thy	Tue May 20 16:52:59 2014 +0200
    16.2 +++ b/src/HOL/Topological_Spaces.thy	Tue May 20 19:24:39 2014 +0200
    16.3 @@ -1230,6 +1230,22 @@
    16.4    "filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
    16.5    by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
    16.6  
    16.7 +lemma eventually_nhds_top:
    16.8 +  fixes P :: "'a :: {order_top, linorder_topology} \<Rightarrow> bool"
    16.9 +  assumes "(b::'a) < top"
   16.10 +  shows "eventually P (nhds top) \<longleftrightarrow> (\<exists>b<top. (\<forall>z. b < z \<longrightarrow> P z))"
   16.11 +  unfolding eventually_nhds
   16.12 +proof safe
   16.13 +  fix S :: "'a set" assume "open S" "top \<in> S"
   16.14 +  note open_left[OF this `b < top`]
   16.15 +  moreover assume "\<forall>s\<in>S. P s"
   16.16 +  ultimately show "\<exists>b<top. \<forall>z>b. P z"
   16.17 +    by (auto simp: subset_eq Ball_def)
   16.18 +next
   16.19 +  fix b assume "b < top" "\<forall>z>b. P z"
   16.20 +  then show "\<exists>S. open S \<and> top \<in> S \<and> (\<forall>xa\<in>S. P xa)"
   16.21 +    by (intro exI[of _ "{b <..}"]) auto
   16.22 +qed
   16.23  
   16.24  subsection {* Limits on sequences *}
   16.25  
   16.26 @@ -1724,6 +1740,50 @@
   16.27     (X -- a --> (L::'b::topological_space))"
   16.28    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
   16.29  
   16.30 +lemma sequentially_imp_eventually_at_left:
   16.31 +  fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
   16.32 +  assumes b[simp]: "b < a"
   16.33 +  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"
   16.34 +  shows "eventually P (at_left a)"
   16.35 +proof (safe intro!: sequentially_imp_eventually_within)
   16.36 +  fix X assume X: "\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a" "X ----> a"
   16.37 +  show "eventually (\<lambda>n. P (X n)) sequentially"
   16.38 +  proof (rule ccontr)
   16.39 +    assume "\<not> eventually (\<lambda>n. P (X n)) sequentially"
   16.40 +    from not_eventually_sequentiallyD[OF this]
   16.41 +    obtain r where "subseq r" "\<And>n. \<not> P (X (r n))"
   16.42 +      by auto
   16.43 +    with X have "(X \<circ> r) ----> a"
   16.44 +      by (auto intro: LIMSEQ_subseq_LIMSEQ)
   16.45 +    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)"
   16.46 +      unfolding eventually_sequentially comp_def by metis
   16.47 +    def s \<equiv> "rec_nat (s' b) (\<lambda>_ i. max (s' (X (r i))) (Suc i))"
   16.48 +    then have [simp]: "s 0 = s' b" "\<And>n. s (Suc n) = max (s' (X (r (s n)))) (Suc (s n))"
   16.49 +      by auto
   16.50 +    have "eventually (\<lambda>n. P (((X \<circ> r) \<circ> s) n)) sequentially"
   16.51 +    proof (rule *)
   16.52 +      from X show inc: "incseq (X \<circ> r \<circ> s)"
   16.53 +        unfolding incseq_Suc_iff comp_def by (intro allI s'[THEN less_imp_le]) auto
   16.54 +      { fix n show "b < (X \<circ> r \<circ> s) n"
   16.55 +          using inc[THEN incseqD, of 0 n] s'[OF b order_refl] by simp }
   16.56 +      { fix n show "(X \<circ> r \<circ> s) n < a"
   16.57 +          using X by simp }
   16.58 +      from `(X \<circ> r) ----> a` show "(X \<circ> r \<circ> s) ----> a"
   16.59 +        by (rule LIMSEQ_subseq_LIMSEQ) (auto simp: subseq_Suc_iff)
   16.60 +    qed
   16.61 +    with `\<And>n. \<not> P (X (r n))` show False
   16.62 +      by auto
   16.63 +  qed
   16.64 +qed
   16.65 +
   16.66 +lemma tendsto_at_left_sequentially:
   16.67 +  fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
   16.68 +  assumes "b < a"
   16.69 +  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"
   16.70 +  shows "(X ---> L) (at_left a)"
   16.71 +  using assms unfolding tendsto_def [where l=L]
   16.72 +  by (simp add: sequentially_imp_eventually_at_left)
   16.73 +
   16.74  subsection {* Continuity *}
   16.75  
   16.76  subsubsection {* Continuity on a set *}
    17.1 --- a/src/HOL/Transcendental.thy	Tue May 20 16:52:59 2014 +0200
    17.2 +++ b/src/HOL/Transcendental.thy	Tue May 20 19:24:39 2014 +0200
    17.3 @@ -10,6 +10,32 @@
    17.4  imports Fact Series Deriv NthRoot
    17.5  begin
    17.6  
    17.7 +lemma root_test_convergence:
    17.8 +  fixes f :: "nat \<Rightarrow> 'a::banach"
    17.9 +  assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
   17.10 +  assumes "x < 1"
   17.11 +  shows "summable f"
   17.12 +proof -
   17.13 +  have "0 \<le> x"
   17.14 +    by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
   17.15 +  from `x < 1` obtain z where z: "x < z" "z < 1"
   17.16 +    by (metis dense)
   17.17 +  from f `x < z`
   17.18 +  have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
   17.19 +    by (rule order_tendstoD)
   17.20 +  then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
   17.21 +    using eventually_ge_at_top
   17.22 +  proof eventually_elim
   17.23 +    fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
   17.24 +    from power_strict_mono[OF less, of n] n
   17.25 +    show "norm (f n) \<le> z ^ n"
   17.26 +      by simp
   17.27 +  qed
   17.28 +  then show "summable f"
   17.29 +    unfolding eventually_sequentially
   17.30 +    using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
   17.31 +qed
   17.32 +
   17.33  subsection {* Properties of Power Series *}
   17.34  
   17.35  lemma lemma_realpow_diff: