moved material from AFP to distribution
authoreberlm <eberlm@in.tum.de>
Tue Apr 04 08:57:21 2017 +0200 (2017-04-04)
changeset 653957504569a73c7
parent 65354 4ff2ba82d668
child 65396 b42167902f57
moved material from AFP to distribution
src/HOL/Analysis/Harmonic_Numbers.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Random_Permutations.thy
     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