src/HOL/Probability/Bochner_Integration.thy
changeset 57235 b0b9a10e4bf4
parent 57166 5cfcc616d485
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 11 13:39:38 2014 +0200
     1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Jun 12 15:47:36 2014 +0200
     1.3 @@ -1518,9 +1518,37 @@
     1.4    using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
     1.5    using integral_norm_bound_ereal[of M f] by simp
     1.6    
     1.7 +lemma integrableI_nn_integral_finite:
     1.8 +  assumes [measurable]: "f \<in> borel_measurable M"
     1.9 +    and nonneg: "AE x in M. 0 \<le> f x"
    1.10 +    and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
    1.11 +  shows "integrable M f"
    1.12 +proof (rule integrableI_bounded)
    1.13 +  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
    1.14 +    using nonneg by (intro nn_integral_cong_AE) auto
    1.15 +  with finite show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
    1.16 +    by auto
    1.17 +qed simp
    1.18 +
    1.19  lemma integral_eq_nn_integral:
    1.20 -  "integrable M f \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
    1.21 -  by (subst nn_integral_eq_integral) auto
    1.22 +  assumes [measurable]: "f \<in> borel_measurable M"
    1.23 +  assumes nonneg: "AE x in M. 0 \<le> f x"
    1.24 +  shows "integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
    1.25 +proof cases
    1.26 +  assume *: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = \<infinity>"
    1.27 +  also have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
    1.28 +    using nonneg by (intro nn_integral_cong_AE) auto
    1.29 +  finally have "\<not> integrable M f"
    1.30 +    by (auto simp: integrable_iff_bounded)
    1.31 +  then show ?thesis
    1.32 +    by (simp add: * not_integrable_integral_eq)
    1.33 +next
    1.34 +  assume "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
    1.35 +  then have "integrable M f"
    1.36 +    by (cases "\<integral>\<^sup>+ x. ereal (f x) \<partial>M") (auto intro!: integrableI_nn_integral_finite assms)
    1.37 +  from nn_integral_eq_integral[OF this nonneg] show ?thesis
    1.38 +    by simp
    1.39 +qed
    1.40    
    1.41  lemma integrableI_simple_bochner_integrable:
    1.42    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    1.43 @@ -1933,7 +1961,7 @@
    1.44  subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
    1.45  
    1.46  lemma real_lebesgue_integral_def:
    1.47 -  assumes f: "integrable M f"
    1.48 +  assumes f[measurable]: "integrable M f"
    1.49    shows "integral\<^sup>L M f = real (\<integral>\<^sup>+x. f x \<partial>M) - real (\<integral>\<^sup>+x. - f x \<partial>M)"
    1.50  proof -
    1.51    have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
    1.52 @@ -1941,9 +1969,9 @@
    1.53    also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
    1.54      by (intro integral_diff integrable_max integrable_minus integrable_zero f)
    1.55    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
    1.56 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
    1.57 +    by (subst integral_eq_nn_integral[symmetric]) auto
    1.58    also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
    1.59 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
    1.60 +    by (subst integral_eq_nn_integral[symmetric]) auto
    1.61    also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
    1.62      by (auto simp: max_def)
    1.63    also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"