Connecting PMFs to infinite sums
authoreberlm <eberlm@in.tum.de>
Thu Aug 31 17:48:20 2017 +0200 (20 months ago)
changeset 6656852b5cf533fd6
parent 66567 dd47c9843598
child 66578 6a034c6c423f
child 66704 7551bd9ff5c7
Connecting PMFs to infinite sums
src/HOL/Analysis/Infinite_Set_Sum.thy
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Aug 31 14:32:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Aug 31 17:48:20 2017 +0200
     1.3 @@ -350,6 +350,25 @@
     1.4    shows   "(\<lambda>x. f x * c) abs_summable_on A"
     1.5    using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
     1.6  
     1.7 +lemma abs_summable_on_prod_PiE:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
     1.9 +  assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
    1.10 +  assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
    1.11 +  shows   "(\<lambda>g. \<Prod>x\<in>A. f x (g x)) abs_summable_on PiE A B"
    1.12 +proof -
    1.13 +  define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
    1.14 +  from assms have [simp]: "countable (B' x)" for x
    1.15 +    by (auto simp: B'_def)
    1.16 +  then interpret product_sigma_finite "count_space \<circ> B'"
    1.17 +    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
    1.18 +  from assms have "integrable (PiM A (count_space \<circ> B')) (\<lambda>g. \<Prod>x\<in>A. f x (g x))"
    1.19 +    by (intro product_integrable_prod) (auto simp: abs_summable_on_def B'_def)
    1.20 +  also have "PiM A (count_space \<circ> B') = count_space (PiE A B')"
    1.21 +    unfolding o_def using finite by (intro count_space_PiM_finite) simp_all
    1.22 +  also have "PiE A B' = PiE A B" by (intro PiE_cong) (simp_all add: B'_def)
    1.23 +  finally show ?thesis by (simp add: abs_summable_on_def)
    1.24 +qed
    1.25 +
    1.26  
    1.27  
    1.28  lemma not_summable_infsetsum_eq:
    1.29 @@ -366,6 +385,18 @@
    1.30    by (subst integral_restrict_space [symmetric])
    1.31       (auto simp: restrict_count_space_subset infsetsum_def)
    1.32  
    1.33 +lemma nn_integral_conv_infsetsum:
    1.34 +  assumes "f abs_summable_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
    1.35 +  shows   "nn_integral (count_space A) f = ennreal (infsetsum f A)"
    1.36 +  using assms unfolding infsetsum_def abs_summable_on_def
    1.37 +  by (subst nn_integral_eq_integral) auto
    1.38 +
    1.39 +lemma infsetsum_conv_nn_integral:
    1.40 +  assumes "nn_integral (count_space A) f \<noteq> \<infinity>" "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
    1.41 +  shows   "infsetsum f A = enn2real (nn_integral (count_space A) f)"
    1.42 +  unfolding infsetsum_def using assms
    1.43 +  by (subst integral_eq_nn_integral) auto
    1.44 +
    1.45  lemma infsetsum_cong [cong]:
    1.46    "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B"
    1.47    unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
     2.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Aug 31 14:32:23 2017 +0200
     2.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Aug 31 17:48:20 2017 +0200
     2.3 @@ -529,6 +529,25 @@
     2.4    shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\<lambda>x. f (g x))"
     2.5    by (simp add: integral_distr map_pmf_rep_eq)
     2.6  
     2.7 +lemma pmf_abs_summable [intro]: "pmf p abs_summable_on A"
     2.8 +  by (rule abs_summable_on_subset[OF _ subset_UNIV]) 
     2.9 +     (auto simp:  abs_summable_on_def integrable_iff_bounded nn_integral_pmf)
    2.10 +
    2.11 +lemma measure_pmf_conv_infsetsum: "measure (measure_pmf p) A = infsetsum (pmf p) A"
    2.12 +  unfolding infsetsum_def by (simp add: integral_eq_nn_integral nn_integral_pmf measure_def)  
    2.13 +
    2.14 +lemma infsetsum_pmf_eq_1:
    2.15 +  assumes "set_pmf p \<subseteq> A"
    2.16 +  shows   "infsetsum (pmf p) A = 1"
    2.17 +proof -
    2.18 +  have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)"
    2.19 +    using assms unfolding infsetsum_altdef
    2.20 +    by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq)
    2.21 +  also have "\<dots> = 1"
    2.22 +    by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf)
    2.23 +  finally show ?thesis .
    2.24 +qed
    2.25 +
    2.26  lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
    2.27    by transfer (simp add: distr_return)
    2.28  
    2.29 @@ -2079,6 +2098,20 @@
    2.30    "measure (measure_pmf p) (A \<inter> set_pmf p) = measure (measure_pmf p) A"
    2.31    using emeasure_Int_set_pmf[of p A] by (simp add: Sigma_Algebra.measure_def)
    2.32  
    2.33 +lemma measure_prob_cong_0:
    2.34 +  assumes "\<And>x. x \<in> A - B \<Longrightarrow> pmf p x = 0"
    2.35 +  assumes "\<And>x. x \<in> B - A \<Longrightarrow> pmf p x = 0"
    2.36 +  shows   "measure (measure_pmf p) A = measure (measure_pmf p) B"
    2.37 +proof -
    2.38 +  have "measure_pmf.prob p A = measure_pmf.prob p (A \<inter> set_pmf p)"
    2.39 +    by (simp add: measure_Int_set_pmf)
    2.40 +  also have "A \<inter> set_pmf p = B \<inter> set_pmf p"
    2.41 +    using assms by (auto simp: set_pmf_eq)
    2.42 +  also have "measure_pmf.prob p \<dots> = measure_pmf.prob p B"
    2.43 +    by (simp add: measure_Int_set_pmf)
    2.44 +  finally show ?thesis .
    2.45 +qed
    2.46 +
    2.47  lemma emeasure_pmf_of_list:
    2.48    assumes "pmf_of_list_wf xs"
    2.49    shows   "emeasure (pmf_of_list xs) A = ennreal (sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs)))"