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