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: