author | eberlm <eberlm@in.tum.de> |

Tue Apr 04 08:57:21 2017 +0200 (2017-04-04) | |

changeset 65395 | 7504569a73c7 |

parent 65354 | 4ff2ba82d668 |

child 65396 | b42167902f57 |

moved material from AFP to distribution

1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy Mon Apr 03 22:18:56 2017 +0200 1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy Tue Apr 04 08:57:21 2017 +0200 1.3 @@ -37,6 +37,9 @@ 1.4 lemma of_real_harm: "of_real (harm n) = harm n" 1.5 unfolding harm_def by simp 1.6 1.7 +lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n" 1.8 + using harm_nonneg[of n] by (rule abs_of_nonneg) 1.9 + 1.10 lemma norm_harm: "norm (harm n) = harm n" 1.11 by (subst of_real_harm [symmetric]) (simp add: harm_nonneg) 1.12 1.13 @@ -91,6 +94,15 @@ 1.14 finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp 1.15 qed (simp_all add: harm_def) 1.16 1.17 +lemma harm_at_top: "filterlim (harm :: nat \<Rightarrow> real) at_top sequentially" 1.18 +proof (rule filterlim_at_top_mono) 1.19 + show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top" 1.20 + using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac) 1.21 + show "filterlim (\<lambda>n. ln (real (Suc n))) at_top sequentially" 1.22 + by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially] 1.23 + filterlim_Suc) 1.24 +qed 1.25 + 1.26 1.27 subsection \<open>The Euler--Mascheroni constant\<close> 1.28

2.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Apr 03 22:18:56 2017 +0200 2.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Apr 04 08:57:21 2017 +0200 2.3 @@ -663,6 +663,7 @@ 2.4 lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\<lambda>x. x \<in> set_pmf M)" 2.5 by simp 2.6 2.7 + 2.8 subsection \<open> PMFs as function \<close> 2.9 2.10 context 2.11 @@ -754,6 +755,39 @@ 2.12 apply (subst lebesgue_integral_count_space_finite_support) 2.13 apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] sum.mono_neutral_left simp: pmf_eq_0_set_pmf) 2.14 done 2.15 + 2.16 +lemma expectation_return_pmf [simp]: 2.17 + fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 2.18 + shows "measure_pmf.expectation (return_pmf x) f = f x" 2.19 + by (subst integral_measure_pmf[of "{x}"]) simp_all 2.20 + 2.21 +lemma pmf_expectation_bind: 2.22 + fixes p :: "'a pmf" and f :: "'a \<Rightarrow> 'b pmf" 2.23 + and h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}" 2.24 + assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))" "set_pmf p \<subseteq> A" 2.25 + shows "measure_pmf.expectation (p \<bind> f) h = 2.26 + (\<Sum>a\<in>A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)" 2.27 +proof - 2.28 + have "measure_pmf.expectation (p \<bind> f) h = (\<Sum>a\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (p \<bind> f) a *\<^sub>R h a)" 2.29 + using assms by (intro integral_measure_pmf) auto 2.30 + also have "\<dots> = (\<Sum>x\<in>(\<Union>x\<in>A. set_pmf (f x)). (\<Sum>a\<in>A. (pmf p a * pmf (f a) x) *\<^sub>R h x))" 2.31 + proof (intro sum.cong refl, goal_cases) 2.32 + case (1 x) 2.33 + thus ?case 2.34 + by (subst pmf_bind, subst integral_measure_pmf[of A]) 2.35 + (insert assms, auto simp: scaleR_sum_left) 2.36 + qed 2.37 + also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R (\<Sum>i\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))" 2.38 + by (subst sum.commute) (simp add: scaleR_sum_right) 2.39 + also have "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)" 2.40 + proof (intro sum.cong refl, goal_cases) 2.41 + case (1 x) 2.42 + thus ?case 2.43 + by (subst integral_measure_pmf[of "(\<Union>x\<in>A. set_pmf (f x))"]) 2.44 + (insert assms, auto simp: scaleR_sum_left) 2.45 + qed 2.46 + finally show ?thesis . 2.47 +qed 2.48 2.49 lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close> 2.50 fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::{banach, second_countable_topology}" 2.51 @@ -1725,6 +1759,14 @@ 2.52 by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure) 2.53 2.54 end 2.55 + 2.56 +lemma pmf_expectation_bind_pmf_of_set: 2.57 + fixes A :: "'a set" and f :: "'a \<Rightarrow> 'b pmf" 2.58 + and h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}" 2.59 + assumes "A \<noteq> {}" "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))" 2.60 + shows "measure_pmf.expectation (pmf_of_set A \<bind> f) h = 2.61 + (\<Sum>a\<in>A. measure_pmf.expectation (f a) h /\<^sub>R real (card A))" 2.62 + using assms by (subst pmf_expectation_bind[of A]) (auto simp: divide_simps) 2.63 2.64 lemma map_pmf_of_set: 2.65 assumes "finite A" "A \<noteq> {}" 2.66 @@ -1773,6 +1815,16 @@ 2.67 qed 2.68 qed 2.69 2.70 +lemma map_pmf_of_set_bij_betw: 2.71 + assumes "bij_betw f A B" "A \<noteq> {}" "finite A" 2.72 + shows "map_pmf f (pmf_of_set A) = pmf_of_set B" 2.73 +proof - 2.74 + have "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" 2.75 + by (intro map_pmf_of_set_inj assms bij_betw_imp_inj_on[OF assms(1)]) 2.76 + also from assms have "f ` A = B" by (simp add: bij_betw_def) 2.77 + finally show ?thesis . 2.78 +qed 2.79 + 2.80 text \<open> 2.81 Choosing an element uniformly at random from the union of a disjoint family 2.82 of finite non-empty sets with the same size is the same as first choosing a set

3.1 --- a/src/HOL/Probability/Random_Permutations.thy Mon Apr 03 22:18:56 2017 +0200 3.2 +++ b/src/HOL/Probability/Random_Permutations.thy Tue Apr 04 08:57:21 2017 +0200 3.3 @@ -176,4 +176,56 @@ 3.4 using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf 3.5 fold_random_permutation_fold bind_return_pmf map_pmf_def) 3.6 3.7 +text \<open> 3.8 + The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a 3.9 + predicate and drawing a random permutation of that set. 3.10 +\<close> 3.11 +lemma partition_random_permutations: 3.12 + assumes "finite A" 3.13 + shows "map_pmf (partition P) (pmf_of_set (permutations_of_set A)) = 3.14 + pair_pmf (pmf_of_set (permutations_of_set {x\<in>A. P x})) 3.15 + (pmf_of_set (permutations_of_set {x\<in>A. \<not>P x}))" (is "?lhs = ?rhs") 3.16 +proof (rule pmf_eqI, clarify, goal_cases) 3.17 + case (1 xs ys) 3.18 + show ?case 3.19 + proof (cases "xs \<in> permutations_of_set {x\<in>A. P x} \<and> ys \<in> permutations_of_set {x\<in>A. \<not>P x}") 3.20 + case True 3.21 + let ?n1 = "card {x\<in>A. P x}" and ?n2 = "card {x\<in>A. \<not>P x}" 3.22 + have card_eq: "card A = ?n1 + ?n2" 3.23 + proof - 3.24 + have "?n1 + ?n2 = card ({x\<in>A. P x} \<union> {x\<in>A. \<not>P x})" 3.25 + using assms by (intro card_Un_disjoint [symmetric]) auto 3.26 + also have "{x\<in>A. P x} \<union> {x\<in>A. \<not>P x} = A" by blast 3.27 + finally show ?thesis .. 3.28 + qed 3.29 + 3.30 + from True have lengths [simp]: "length xs = ?n1" "length ys = ?n2" 3.31 + by (auto intro!: length_finite_permutations_of_set) 3.32 + have "pmf ?lhs (xs, ys) = 3.33 + real (card (permutations_of_set A \<inter> partition P -` {(xs, ys)})) / fact (card A)" 3.34 + using assms by (auto simp: pmf_map measure_pmf_of_set) 3.35 + also have "partition P -` {(xs, ys)} = shuffle xs ys" 3.36 + using True by (intro inv_image_partition) (auto simp: permutations_of_set_def) 3.37 + also have "permutations_of_set A \<inter> shuffle xs ys = shuffle xs ys" 3.38 + using True distinct_disjoint_shuffle[of xs ys] 3.39 + by (auto simp: permutations_of_set_def dest: set_shuffle) 3.40 + also have "card (shuffle xs ys) = length xs + length ys choose length xs" 3.41 + using True by (intro card_disjoint_shuffle) (auto simp: permutations_of_set_def) 3.42 + also have "length xs + length ys = card A" by (simp add: card_eq) 3.43 + also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))" 3.44 + by (subst binomial_fact) (auto intro!: card_mono assms) 3.45 + also have "\<dots> / fact (card A) = 1 / (fact ?n1 * fact ?n2)" 3.46 + by (simp add: divide_simps card_eq) 3.47 + also have "\<dots> = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair) 3.48 + finally show ?thesis . 3.49 + next 3.50 + case False 3.51 + hence *: "xs \<notin> permutations_of_set {x\<in>A. P x} \<or> ys \<notin> permutations_of_set {x\<in>A. \<not>P x}" by blast 3.52 + hence eq: "permutations_of_set A \<inter> (partition P -` {(xs, ys)}) = {}" 3.53 + by (auto simp: o_def permutations_of_set_def) 3.54 + from * show ?thesis 3.55 + by (elim disjE) (insert assms eq, simp_all add: pmf_pair pmf_map measure_pmf_of_set) 3.56 + qed 3.57 +qed 3.58 + 3.59 end