src/HOL/Probability/Bochner_Integration.thy
 changeset 61424 c3658c18b7bc parent 61169 4de9ff3ea29a child 61609 77b453bd616f
```     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue Oct 13 09:21:14 2015 +0200
1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Oct 13 09:21:15 2015 +0200
1.3 @@ -2453,7 +2453,7 @@
1.4
1.5  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
1.6    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
1.7 -  assumes [measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
1.8 +  assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
1.9    shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
1.10  proof -
1.11    have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
1.12 @@ -2472,7 +2472,7 @@
1.13
1.14  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
1.15    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
1.16 -  assumes f[measurable]: "split f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
1.17 +  assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
1.18    shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
1.19  proof -
1.20    from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
1.21 @@ -2738,7 +2738,7 @@
1.22
1.23  lemma (in pair_sigma_finite)
1.24    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
1.25 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
1.26 +  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
1.27    shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
1.28      and integrable_fst: "integrable M1 (\<lambda>x. \<integral>y. f x y \<partial>M2)" (is "?INT")
1.29      and integral_fst: "(\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). f x y)" (is "?EQ")
1.30 @@ -2746,10 +2746,10 @@
1.31
1.32  lemma (in pair_sigma_finite)
1.33    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
1.34 -  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
1.35 +  assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
1.36    shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
1.37      and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
1.38 -    and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (split f)" (is "?EQ")
1.39 +    and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (case_prod f)" (is "?EQ")
1.40  proof -
1.41    interpret Q: pair_sigma_finite M2 M1 ..
1.42    have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
1.43 @@ -2757,12 +2757,12 @@
1.44    show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
1.45    show ?INT using Q.integrable_fst'[OF Q_int] by simp
1.46    show ?EQ using Q.integral_fst'[OF Q_int]
1.47 -    using integral_product_swap[of "split f"] by simp
1.48 +    using integral_product_swap[of "case_prod f"] by simp
1.49  qed
1.50
1.51  lemma (in pair_sigma_finite) Fubini_integral:
1.52    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
1.53 -  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (split f)"
1.54 +  assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
1.55    shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
1.56    unfolding integral_snd[OF assms] integral_fst[OF assms] ..
1.57
```