# HG changeset patch
# User eberlm
# Date 1491289041 -7200
# Node ID 7504569a73c74963ff9ac1cec861419fa10fe953
# Parent 4ff2ba82d6681143c26924f604eecd0f88a43b0a
moved material from AFP to distribution
diff -r 4ff2ba82d668 -r 7504569a73c7 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Tue Apr 04 08:57:21 2017 +0200
@@ -37,6 +37,9 @@
lemma of_real_harm: "of_real (harm n) = harm n"
unfolding harm_def by simp
+lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n"
+ using harm_nonneg[of n] by (rule abs_of_nonneg)
+
lemma norm_harm: "norm (harm n) = harm n"
by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)
@@ -91,6 +94,15 @@
finally show "ln (real (Suc n) + 1) \ harm (Suc n)" by - simp
qed (simp_all add: harm_def)
+lemma harm_at_top: "filterlim (harm :: nat \ real) at_top sequentially"
+proof (rule filterlim_at_top_mono)
+ show "eventually (\n. harm n \ ln (real (Suc n))) at_top"
+ using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac)
+ show "filterlim (\n. ln (real (Suc n))) at_top sequentially"
+ by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially]
+ filterlim_Suc)
+qed
+
subsection \The Euler--Mascheroni constant\
diff -r 4ff2ba82d668 -r 7504569a73c7 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Apr 04 08:57:21 2017 +0200
@@ -663,6 +663,7 @@
lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\x. x \ set_pmf M)"
by simp
+
subsection \ PMFs as function \
context
@@ -754,6 +755,39 @@
apply (subst lebesgue_integral_count_space_finite_support)
apply (auto intro!: finite_subset[OF _ \finite A\] sum.mono_neutral_left simp: pmf_eq_0_set_pmf)
done
+
+lemma expectation_return_pmf [simp]:
+ fixes f :: "'a \ 'b::{banach, second_countable_topology}"
+ shows "measure_pmf.expectation (return_pmf x) f = f x"
+ by (subst integral_measure_pmf[of "{x}"]) simp_all
+
+lemma pmf_expectation_bind:
+ fixes p :: "'a pmf" and f :: "'a \ 'b pmf"
+ and h :: "'b \ 'c::{banach, second_countable_topology}"
+ assumes "finite A" "\x. x \ A \ finite (set_pmf (f x))" "set_pmf p \ A"
+ shows "measure_pmf.expectation (p \ f) h =
+ (\a\A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)"
+proof -
+ have "measure_pmf.expectation (p \ f) h = (\a\(\x\A. set_pmf (f x)). pmf (p \ f) a *\<^sub>R h a)"
+ using assms by (intro integral_measure_pmf) auto
+ also have "\ = (\x\(\x\A. set_pmf (f x)). (\a\A. (pmf p a * pmf (f a) x) *\<^sub>R h x))"
+ proof (intro sum.cong refl, goal_cases)
+ case (1 x)
+ thus ?case
+ by (subst pmf_bind, subst integral_measure_pmf[of A])
+ (insert assms, auto simp: scaleR_sum_left)
+ qed
+ also have "\ = (\j\A. pmf p j *\<^sub>R (\i\(\x\A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))"
+ by (subst sum.commute) (simp add: scaleR_sum_right)
+ also have "\ = (\j\A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)"
+ proof (intro sum.cong refl, goal_cases)
+ case (1 x)
+ thus ?case
+ by (subst integral_measure_pmf[of "(\x\A. set_pmf (f x))"])
+ (insert assms, auto simp: scaleR_sum_left)
+ qed
+ finally show ?thesis .
+qed
lemma continuous_on_LINT_pmf: -- \This is dominated convergence!?\
fixes f :: "'i \ 'a::topological_space \ 'b::{banach, second_countable_topology}"
@@ -1725,6 +1759,14 @@
by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
end
+
+lemma pmf_expectation_bind_pmf_of_set:
+ fixes A :: "'a set" and f :: "'a \ 'b pmf"
+ and h :: "'b \ 'c::{banach, second_countable_topology}"
+ assumes "A \ {}" "finite A" "\x. x \ A \ finite (set_pmf (f x))"
+ shows "measure_pmf.expectation (pmf_of_set A \ f) h =
+ (\a\A. measure_pmf.expectation (f a) h /\<^sub>R real (card A))"
+ using assms by (subst pmf_expectation_bind[of A]) (auto simp: divide_simps)
lemma map_pmf_of_set:
assumes "finite A" "A \ {}"
@@ -1773,6 +1815,16 @@
qed
qed
+lemma map_pmf_of_set_bij_betw:
+ assumes "bij_betw f A B" "A \ {}" "finite A"
+ shows "map_pmf f (pmf_of_set A) = pmf_of_set B"
+proof -
+ have "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)"
+ by (intro map_pmf_of_set_inj assms bij_betw_imp_inj_on[OF assms(1)])
+ also from assms have "f ` A = B" by (simp add: bij_betw_def)
+ finally show ?thesis .
+qed
+
text \
Choosing an element uniformly at random from the union of a disjoint family
of finite non-empty sets with the same size is the same as first choosing a set
diff -r 4ff2ba82d668 -r 7504569a73c7 src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy Tue Apr 04 08:57:21 2017 +0200
@@ -176,4 +176,56 @@
using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf
fold_random_permutation_fold bind_return_pmf map_pmf_def)
+text \
+ The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a
+ predicate and drawing a random permutation of that set.
+\
+lemma partition_random_permutations:
+ assumes "finite A"
+ shows "map_pmf (partition P) (pmf_of_set (permutations_of_set A)) =
+ pair_pmf (pmf_of_set (permutations_of_set {x\A. P x}))
+ (pmf_of_set (permutations_of_set {x\A. \P x}))" (is "?lhs = ?rhs")
+proof (rule pmf_eqI, clarify, goal_cases)
+ case (1 xs ys)
+ show ?case
+ proof (cases "xs \ permutations_of_set {x\A. P x} \ ys \ permutations_of_set {x\A. \P x}")
+ case True
+ let ?n1 = "card {x\A. P x}" and ?n2 = "card {x\A. \P x}"
+ have card_eq: "card A = ?n1 + ?n2"
+ proof -
+ have "?n1 + ?n2 = card ({x\A. P x} \ {x\A. \P x})"
+ using assms by (intro card_Un_disjoint [symmetric]) auto
+ also have "{x\A. P x} \ {x\A. \P x} = A" by blast
+ finally show ?thesis ..
+ qed
+
+ from True have lengths [simp]: "length xs = ?n1" "length ys = ?n2"
+ by (auto intro!: length_finite_permutations_of_set)
+ have "pmf ?lhs (xs, ys) =
+ real (card (permutations_of_set A \ partition P -` {(xs, ys)})) / fact (card A)"
+ using assms by (auto simp: pmf_map measure_pmf_of_set)
+ also have "partition P -` {(xs, ys)} = shuffle xs ys"
+ using True by (intro inv_image_partition) (auto simp: permutations_of_set_def)
+ also have "permutations_of_set A \ shuffle xs ys = shuffle xs ys"
+ using True distinct_disjoint_shuffle[of xs ys]
+ by (auto simp: permutations_of_set_def dest: set_shuffle)
+ also have "card (shuffle xs ys) = length xs + length ys choose length xs"
+ using True by (intro card_disjoint_shuffle) (auto simp: permutations_of_set_def)
+ also have "length xs + length ys = card A" by (simp add: card_eq)
+ also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))"
+ by (subst binomial_fact) (auto intro!: card_mono assms)
+ also have "\ / fact (card A) = 1 / (fact ?n1 * fact ?n2)"
+ by (simp add: divide_simps card_eq)
+ also have "\ = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair)
+ finally show ?thesis .
+ next
+ case False
+ hence *: "xs \ permutations_of_set {x\A. P x} \ ys \ permutations_of_set {x\A. \P x}" by blast
+ hence eq: "permutations_of_set A \ (partition P -` {(xs, ys)}) = {}"
+ by (auto simp: o_def permutations_of_set_def)
+ from * show ?thesis
+ by (elim disjE) (insert assms eq, simp_all add: pmf_pair pmf_map measure_pmf_of_set)
+ qed
+qed
+
end