--- 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"
--- 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
--- 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
--- 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
--- /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
--- 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:
--- 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
--- 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:
--- 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
--- 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:
--- 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
--- 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:
--- 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"
--- 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
+
--- 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)
--- 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 *}
--- 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: