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>"
```