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.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.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.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)))"