src/HOL/Probability/Bochner_Integration.thy
changeset 61880 ff4d33058566
parent 61810 3c5040d5694a
child 61897 bc0fc5499085
     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sun Dec 20 13:56:02 2015 +0100
     1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Dec 17 16:43:36 2015 +0100
     1.3 @@ -904,6 +904,12 @@
     1.4  translations
     1.5    "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
     1.6  
     1.7 +syntax
     1.8 +  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
     1.9 +
    1.10 +translations
    1.11 +  "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
    1.12 +
    1.13  lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
    1.14    by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
    1.15  
    1.16 @@ -2581,6 +2587,33 @@
    1.17      by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
    1.18  qed
    1.19  
    1.20 +lemma (in pair_sigma_finite) Fubini_integrable:
    1.21 +  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
    1.22 +  assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
    1.23 +    and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
    1.24 +    and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
    1.25 +  shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
    1.26 +proof (rule integrableI_bounded)
    1.27 +  have "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
    1.28 +    by (simp add: M2.nn_integral_fst [symmetric])
    1.29 +  also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
    1.30 +    apply (intro nn_integral_cong_AE)
    1.31 +    using integ2
    1.32 +  proof eventually_elim
    1.33 +    fix x assume "integrable M2 (\<lambda>y. f (x, y))"
    1.34 +    then have f: "integrable M2 (\<lambda>y. norm (f (x, y)))"
    1.35 +      by simp
    1.36 +    then have "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal (LINT y|M2. norm (f (x, y)))"
    1.37 +      by (rule nn_integral_eq_integral) simp
    1.38 +    also have "\<dots> = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>"
    1.39 +      using f by (auto intro!: abs_of_nonneg[symmetric] integral_nonneg_AE)
    1.40 +    finally show "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>" .
    1.41 +  qed
    1.42 +  also have "\<dots> < \<infinity>"
    1.43 +    using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
    1.44 +  finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
    1.45 +qed fact
    1.46 +
    1.47  lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
    1.48    assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
    1.49    shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"