# 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 \ B) \ (A = {} \ B = {} \ (finite A \ finite B))"
+ by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
+
lemma finite_prod:
"finite (UNIV :: ('a \ 'b) set) \ finite (UNIV :: 'a set) \ 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) \ 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 "(\s\S. P s) \ (\n::nat. from_nat_into S n \ S \ 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 "\i. F i \ X" "\i. F i \ F (Suc i)" "\i. finite (F i)" "(\i. F i) = X"
+proof  show thesis
+ apply (rule that[of "\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 \ X" "\i m. m \ i \ x \ from_nat_into X m"
+ with from_nat_into_surj[OF `countable X` `x \ 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:
+ "((\z. ereal (f z)) > \) F \ (LIM z F. f z :> at_top)"
+ unfolding tendsto_PInfty filterlim_at_top_dense by simp
+
lemma tendsto_MInfty: "(f > \) F \ (\r. eventually (\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: "(\n. root n n) > 1"
+proof 
+ def x \ "\n. root n n  1"
+ have "x > sqrt 0"
+ proof (rule tendsto_sandwich[OF _ _ tendsto_const])
+ show "(\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 "\ \ (\k\{0, 2}. of_nat (n choose k) * x n^k)"
+ by (simp add: x_def)
+ also have "\ \ (\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 "\ = (x n + 1) ^ n"
+ by (simp add: binomial_ring)
+ also have "\ = n"
+ using `2 < n` by (simp add: x_def)
+ finally have "real (n  1) * (real n / 2 * (x n)\<^sup>2) \ real (n  1) * 1"
+ by simp
+ then have "(x n)\<^sup>2 \ 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 \ sqrt (2 / real n)"
+ by simp }
+ then show "eventually (\n. x n \ sqrt (2 / real n)) sequentially"
+ by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
+ show "eventually (\n. sqrt 0 \ 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 "(\n. root n c) > 1"
+proof 
+ { fix c :: real assume "1 \ c"
+ def x \ "\n. root n c  1"
+ have "x > 0"
+ proof (rule tendsto_sandwich[OF _ _ tendsto_const])
+ show "(\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 "\ \ (\k\{0, 1}. of_nat (n choose k) * x n^k)"
+ by (simp add: x_def)
+ also have "\ \ (\k=0..n. of_nat (n choose k) * x n^k)"
+ using `1 < n` `1 \ c` by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq)
+ also have "\ = (x n + 1) ^ n"
+ by (simp add: binomial_ring)
+ also have "\ = c"
+ using `1 < n` `1 \ c` by (simp add: x_def)
+ finally have "x n \ c / n"
+ using `1 \ c` `1 < n` by (simp add: field_simps) }
+ then show "eventually (\n. x n \ c / n) sequentially"
+ by (auto intro!: exI[of _ 3] simp: eventually_sequentially)
+ show "eventually (\n. 0 \ x n) sequentially"
+ using `1 \ 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 "(\n. root n c) > 1"
+ by (simp add: x_def) }
+ note ge_1 = this
+
+ show ?thesis
+ proof cases
+ assume "1 \ c" with ge_1 show ?thesis by blast
+ next
+ assume "\ 1 \ c"
+ with `0 < c` have "1 \ 1 / c"
+ by simp
+ then have "(\n. 1 / root n (1 / c)) > 1 / 1"
+ by (intro tendsto_divide tendsto_const ge_1 `1 \ 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 \ ereal"
+ assumes f: "\i. 0 \ f i"
+ shows "(\i. f (i + k)) \ suminf f"
+proof 
+ have "(\n. \i (\i. f (i + k))"
+ using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
+ moreover have "(\n. \i (\i. f i)"
+ using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
+ then have "(\n. \i (\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 \ n"
+ have "(\ii (\i. i + k)) i)"
+ by simp
+ also have "\ = (\i\(\i. i + k) ` {.. \ setsum f {..i setsum f {.. (\i. ereal (f i)) = ereal x"
+ by (metis sums_ereal sums_unique)
+
+lemma suminf_ereal': "summable f \ (\i. ereal (f i)) = ereal (\i. f i)"
+ by (metis sums_ereal sums_unique summable_def)
+
+lemma suminf_ereal_finite: "summable f \ (\i. ereal (f i)) \ \"
+ 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 \\<^sub>M N) = Pow (S1 \ S2)"
+proof auto
+ fix x a b assume x: "x \ sets (M \\<^sub>M N)" "(a, b) \ 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 \ S1" "b \ S2"
+ by (auto simp: space_pair_measure)
+next
+ fix X assume X: "X \ S1 \ S2"
+ then have "countable X"
+ by (metis countable_subset `countable S1` `countable S2` countable_SIGMA)
+ have "X = (\(a, b)\X. {a} \ {b})" by auto
+ also have "\ \ sets (M \\<^sub>M N)"
+ using X
+ by (safe intro!: sets.countable_UN' `countable X` subsetI pair_measureI) (auto simp: M N)
+ finally show "X \ sets (M \\<^sub>M N)" .
+qed
+
+lemma pair_measure_countable:
+ assumes "countable S1" "countable S2"
+ shows "count_space S1 \\<^sub>M count_space S2 = count_space (S1 \ 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 \\<^sub>M count_space S2) = sets (count_space (S1 \ S2))"
+ by (subst sets_pair_countable[OF assms]) auto
+next
+ fix A B assume "A \ sets (count_space S1)" "B \ sets (count_space S2)"
+ then show "emeasure (count_space S1) A * emeasure (count_space S2) B =
+ emeasure (count_space (S1 \ S2)) (A \ 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 \ 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) (\i. measure M (X i))"
+proof 
+ have "(\\<^sup>+i. measure M (X i) \count_space I) = (\\<^sup>+i. measure M (if X i \ sets M then X i else {}) \count_space I)"
+ by (auto intro!: nn_integral_cong measure_notin_sets)
+ also have "\ = measure M (\i\I. if X i \ 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 \ borel_measurable M" and ae: "AE x in M. 0 \ f x" and fin: "integral\<^sup>N M f < \"
+ shows "integrable M f"
+proof (rule integrableI_bounded)
+ have "(\\<^sup>+ x. ereal (norm (f x)) \M) = \\<^sup>+ x. ereal (f x) \M"
+ using ae by (auto intro: nn_integral_cong_AE)
+ also note fin
+ finally show "(\\<^sup>+ x. ereal (norm (f x)) \M) < \" .
+qed fact
+
+lemma integral_real_bounded:
+ assumes "f \ borel_measurable M" "AE x in M. 0 \ f x" "integral\<^sup>N M f \ ereal r"
+ shows "integral\<^sup>L M f \ 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:
+ "(\n. (\\. f n \) \ measurable M (N n)) \ (\\ n. f n \) \ measurable M (PiM UNIV N)"
+ by (intro measurable_PiM_single) (auto dest: measurable_space)
+
lemma measurable_restrict_subset: "J \ L \ (\f. restrict f J) \ 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 \ S \ A \ sets (count_space S) \ insert s A \ sets (count_space S)"
by simp
+lemma measurable_card[measurable]:
+ fixes S :: "'a \ nat set"
+ assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M"
+ shows "(\x. card (S x)) \ measurable M (count_space UNIV)"
+ unfolding measurable_count_space_eq2_countable
+proof safe
+ fix n show "(\x. card (S x)) ` {n} \ space M \ sets M"
+ proof (cases n)
+ case 0
+ then have "(\x. card (S x)) ` {n} \ space M = {x\space M. infinite (S x) \ (\i. i \ S x)}"
+ by auto
+ also have "\ \ sets M"
+ by measurable
+ finally show ?thesis .
+ next
+ case (Suc i)
+ then have "(\x. card (S x)) ` {n} \ space M =
+ (\F\{A\{A. finite A}. card A = n}. {x\space M. (\i. i \ S x \ i \ F)})"
+ unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
+ also have "\ \ 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) \ (\x\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 "\F::nat \ 'a set. range F \ sets (count_space A) \ (\i. F i) = space (count_space A) \
(\i. emeasure (count_space A) (F i) \ \)"
 using surj_from_nat by (intro exI[of _ "\i. {from_nat i} \ A"]) (auto simp del: surj_from_nat)
+ using A
+ apply (intro exI[of _ "\i. {from_nat_into A i} \ 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 "\ \ sets M" "A \ \"
+ assumes "\ \ space M \ sets M" "A \ \"
shows "emeasure (restrict_space M \) A = emeasure M A"
proof cases
assume "A \ sets M"

 have "emeasure (restrict_space M \) A = emeasure M (A \ \)"
+ show ?thesis
proof (rule emeasure_measure_of[OF restrict_space_def])
 show "op \ \ ` sets M \