src/HOL/Probability/Bochner_Integration.thy
changeset 59353 f0707dc3d9aa
parent 59048 7dc8ac6f0895
child 59357 f366643536cd
     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sun Jan 11 21:06:47 2015 +0100
     1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Jan 13 19:10:36 2015 +0100
     1.3 @@ -534,9 +534,13 @@
     1.4              nn_integral_cong_AE)
     1.5       auto
     1.6  
     1.7 -lemma borel_measurable_has_bochner_integral[measurable_dest]:
     1.8 +lemma borel_measurable_has_bochner_integral:
     1.9    "has_bochner_integral M f x \<Longrightarrow> f \<in> borel_measurable M"
    1.10 -  by (auto elim: has_bochner_integral.cases)
    1.11 +  by (rule has_bochner_integral.cases)
    1.12 +
    1.13 +lemma borel_measurable_has_bochner_integral'[measurable_dest]:
    1.14 +  "has_bochner_integral M f x \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
    1.15 +  using borel_measurable_has_bochner_integral[measurable] by measurable
    1.16  
    1.17  lemma has_bochner_integral_simple_bochner_integrable:
    1.18    "simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)"
    1.19 @@ -922,6 +926,10 @@
    1.20  lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
    1.21    by (auto elim: integrable.cases has_bochner_integral.cases)
    1.22  
    1.23 +lemma borel_measurable_integrable'[measurable_dest]:
    1.24 +  "integrable M f \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
    1.25 +  using borel_measurable_integrable[measurable] by measurable
    1.26 +
    1.27  lemma integrable_cong:
    1.28    "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
    1.29    using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
    1.30 @@ -2765,6 +2773,7 @@
    1.31    shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
    1.32  proof (unfold integrable_iff_bounded, intro conjI)
    1.33    interpret finite_product_sigma_finite M I by default fact
    1.34 +
    1.35    show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
    1.36      using assms by simp
    1.37    have "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) = 
    1.38 @@ -2854,3 +2863,4 @@
    1.39  hide_const simple_bochner_integrable
    1.40  
    1.41  end
    1.42 +