src/HOL/Probability/Bochner_Integration.thy
 changeset 57025 e7fd64f82876 parent 56996 891e992e510f child 57036 22568fb89165
```     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue May 20 16:52:59 2014 +0200
1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue May 20 19:24:39 2014 +0200
1.3 @@ -1519,6 +1519,39 @@
1.4      integral\<^sup>L M f \<le> integral\<^sup>L M g"
1.5    by (intro integral_mono_AE) auto
1.6
1.7 +lemma (in finite_measure) integrable_measure:
1.8 +  assumes I: "disjoint_family_on X I" "countable I"
1.9 +  shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
1.10 +proof -
1.11 +  have "(\<integral>\<^sup>+i. measure M (X i) \<partial>count_space I) = (\<integral>\<^sup>+i. measure M (if X i \<in> sets M then X i else {}) \<partial>count_space I)"
1.12 +    by (auto intro!: nn_integral_cong measure_notin_sets)
1.13 +  also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
1.14 +    using I unfolding emeasure_eq_measure[symmetric]
1.15 +    by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def)
1.16 +  finally show ?thesis
1.17 +    by (auto intro!: integrableI_bounded simp: measure_nonneg)
1.18 +qed
1.19 +
1.20 +lemma integrableI_real_bounded:
1.21 +  assumes f: "f \<in> borel_measurable M" and ae: "AE x in M. 0 \<le> f x" and fin: "integral\<^sup>N M f < \<infinity>"
1.22 +  shows "integrable M f"
1.23 +proof (rule integrableI_bounded)
1.24 +  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = \<integral>\<^sup>+ x. ereal (f x) \<partial>M"
1.25 +    using ae by (auto intro: nn_integral_cong_AE)
1.26 +  also note fin
1.27 +  finally show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>" .
1.28 +qed fact
1.29 +
1.30 +lemma integral_real_bounded:
1.31 +  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "integral\<^sup>N M f \<le> ereal r"
1.32 +  shows "integral\<^sup>L M f \<le> r"
1.33 +proof -
1.34 +  have "integrable M f"
1.35 +    using assms by (intro integrableI_real_bounded) auto
1.36 +  from nn_integral_eq_integral[OF this] assms show ?thesis
1.37 +    by simp
1.38 +qed
1.39 +
1.40  subsection {* Measure spaces with an associated density *}
1.41
1.42  lemma integrable_density:
```