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) (\<lambda>x. x \<in> set_pmf M)"
   by simp
 
+
 subsection \<open> PMFs as function \<close>
 
 context
@@ -754,6 +755,39 @@
   apply (subst lebesgue_integral_count_space_finite_support)
   apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] sum.mono_neutral_left simp: pmf_eq_0_set_pmf)
   done
+    
+lemma expectation_return_pmf [simp]:
+  fixes f :: "'a \<Rightarrow> '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 \<Rightarrow> 'b pmf"
+    and  h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}"
+  assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))" "set_pmf p \<subseteq> A"
+  shows "measure_pmf.expectation (p \<bind> f) h =
+           (\<Sum>a\<in>A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)"
+proof -
+  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)"
+    using assms by (intro integral_measure_pmf) auto
+  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))"
+  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 "\<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))"
+    by (subst sum.commute) (simp add: scaleR_sum_right)
+  also have "\<dots> = (\<Sum>j\<in>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 "(\<Union>x\<in>A. set_pmf (f x))"]) 
+         (insert assms, auto simp: scaleR_sum_left)
+  qed
+  finally show ?thesis .
+qed
 
 lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close>
   fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> '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 \<Rightarrow> 'b pmf"
+    and  h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}"
+  assumes "A \<noteq> {}" "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))"
+  shows "measure_pmf.expectation (pmf_of_set A \<bind> f) h =
+           (\<Sum>a\<in>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 \<noteq> {}"
@@ -1773,6 +1815,16 @@
   qed
 qed
 
+lemma map_pmf_of_set_bij_betw:
+  assumes "bij_betw f A B" "A \<noteq> {}" "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 \<open>
   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