src/HOL/Probability/Probability_Measure.thy

 
 definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
   f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
 
 lemma
-  shows distributed_distr_eq_density: "distributed M N X f \<Longrightarrow> distr M N X = density N f"
-    and distributed_measurable: "distributed M N X f \<Longrightarrow> X \<in> measurable M N"
-    and distributed_borel_measurable: "distributed M N X f \<Longrightarrow> f \<in> borel_measurable N"
-    and distributed_AE: "distributed M N X f \<Longrightarrow> (AE x in N. 0 \<le> f x)"
-  by (simp_all add: distributed_def)
+  assumes "distributed M N X f"
+  shows distributed_distr_eq_density: "distr M N X = density N f"
+    and distributed_measurable: "X \<in> measurable M N"
+    and distributed_borel_measurable: "f \<in> borel_measurable N"
+    and distributed_AE: "(AE x in N. 0 \<le> f x)"
+  using assms by (simp_all add: distributed_def)
+
+lemma
+  assumes D: "distributed M N X f"
+  shows distributed_measurable'[measurable_dest]:
+      "g \<in> measurable L M \<Longrightarrow> (\<lambda>x. X (g x)) \<in> measurable L N"
+    and distributed_borel_measurable'[measurable_dest]:
+      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
+  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
+  by simp_all
 
 lemma
   shows distributed_real_measurable: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> f \<in> borel_measurable N"
     and distributed_real_AE: "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
   by (simp_all add: distributed_def borel_measurable_ereal_iff)
 
+lemma
+  assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
+  shows distributed_real_measurable'[measurable_dest]:
+      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
+  using distributed_real_measurable[OF D]
+  by simp_all
+
+lemma
+  assumes D: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
+  shows joint_distributed_measurable1[measurable_dest]:
+      "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
+    and joint_distributed_measurable2[measurable_dest]:
+      "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
+  using measurable_compose[OF distributed_measurable[OF D] measurable_fst]
+  using measurable_compose[OF distributed_measurable[OF D] measurable_snd]
+  by auto
+
 lemma distributed_count_space:
   assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"
   shows "P a = emeasure M (X -` {a} \<inter> space M)"
 proof -
   have "emeasure M (X -` {a} \<inter> space M) = emeasure (distr M (count_space A) X) {a}"
-    using X a A by (simp add: distributed_measurable emeasure_distr)
+    using X a A by (simp add: emeasure_distr)
   also have "\<dots> = emeasure (density (count_space A) P) {a}"
     using X by (simp add: distributed_distr_eq_density)
   also have "\<dots> = (\<integral>\<^isup>+x. P a * indicator {a} x \<partial>count_space A)"
     using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: positive_integral_cong)
   also have "\<dots> = P a"

   shows "AE x in P. g (T x) = 0 \<longrightarrow> f x = 0"
   using subdensity[OF T, of M X "\<lambda>x. ereal (f x)" Y "\<lambda>x. ereal (g x)"] assms by auto
 
 lemma distributed_emeasure:
   "distributed M N X f \<Longrightarrow> A \<in> sets N \<Longrightarrow> emeasure M (X -` A \<inter> space M) = (\<integral>\<^isup>+x. f x * indicator A x \<partial>N)"
-  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
+  by (auto simp: distributed_AE
                  distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)
 
 lemma distributed_positive_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^isup>+x. f x * g x \<partial>N) = (\<integral>\<^isup>+x. g (X x) \<partial>M)"
-  by (auto simp: distributed_measurable distributed_AE distributed_borel_measurable
+  by (auto simp: distributed_AE
                  distributed_distr_eq_density[symmetric] positive_integral_density[symmetric] positive_integral_distr)
 
 lemma distributed_integral:
   "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow> (\<integral>x. f x * g x \<partial>N) = (\<integral>x. g (X x) \<partial>M)"
-  by (auto simp: distributed_real_measurable distributed_real_AE distributed_measurable
+  by (auto simp: distributed_real_AE
                  distributed_distr_eq_density[symmetric] integral_density[symmetric] integral_distr)
   
 lemma distributed_transform_integral:
   assumes Px: "distributed M N X Px"
   assumes "distributed M P Y Py"

   assumes Px: "distributed M S X Px"
   assumes Py: "distributed M S X Py"
   shows "AE x in S. Px x = Py x"
 proof -
   interpret X: prob_space "distr M S X"
-    using distributed_measurable[OF Px] by (rule prob_space_distr)
+    using Px by (intro prob_space_distr) simp
   have "sigma_finite_measure (distr M S X)" ..
   with sigma_finite_density_unique[of Px S Py ] Px Py
   show ?thesis
     by (auto simp: distributed_def)
 qed
 
 lemma (in prob_space) distributed_jointI:
   assumes "sigma_finite_measure S" "sigma_finite_measure T"
-  assumes X[simp]: "X \<in> measurable M S" and Y[simp]: "Y \<in> measurable M T"
-  assumes f[simp]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
+  assumes X[measurable]: "X \<in> measurable M S" and Y[measurable]: "Y \<in> measurable M T"
+  assumes [measurable]: "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)" and f: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> f x"
   assumes eq: "\<And>A B. A \<in> sets S \<Longrightarrow> B \<in> sets T \<Longrightarrow> 
     emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B} = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. f (x, y) * indicator B y \<partial>T) * indicator A x \<partial>S)"
   shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) f"
   unfolding distributed_def
 proof safe

       by (rule prob_space_distr) (auto intro!: measurable_Pair)
     show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?L (F i) \<noteq> \<infinity>"
       using F by (auto simp: space_pair_measure)
   next
     fix E assume "E \<in> ?E"
-    then obtain A B where E[simp]: "E = A \<times> B" and A[simp]: "A \<in> sets S" and B[simp]: "B \<in> sets T" by auto
+    then obtain A B where E[simp]: "E = A \<times> B"
+      and A[measurable]: "A \<in> sets S" and B[measurable]: "B \<in> sets T" by auto
     have "emeasure ?L E = emeasure M {x \<in> space M. X x \<in> A \<and> Y x \<in> B}"
       by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
     also have "\<dots> = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. (f (x, y) * indicator B y) * indicator A x \<partial>T) \<partial>S)"
-      by (auto simp add: eq measurable_Pair measurable_compose[OF _ f(1)] positive_integral_multc
-               intro!: positive_integral_cong)
+      using f by (auto simp add: eq positive_integral_multc intro!: positive_integral_cong)
     also have "\<dots> = emeasure ?R E"
       by (auto simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric]
                intro!: positive_integral_cong split: split_indicator)
     finally show "emeasure ?L E = emeasure ?R E" .
   qed
-qed (auto intro!: measurable_Pair)
+qed (auto simp: f)
 
 lemma (in prob_space) distributed_swap:
   assumes "sigma_finite_measure S" "sigma_finite_measure T"
   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
   shows "distributed M (T \<Otimes>\<^isub>M S) (\<lambda>x. (Y x, X x)) (\<lambda>(x, y). Pxy (y, x))"

   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T by default
   interpret TS: pair_sigma_finite T S by default
 
-  note measurable_Pxy = measurable_compose[OF _ distributed_borel_measurable[OF Pxy]]
+  note Pxy[measurable]
   show ?thesis 
     apply (subst TS.distr_pair_swap)
     unfolding distributed_def
   proof safe
     let ?D = "distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))"
     show 1: "(\<lambda>(x, y). Pxy (y, x)) \<in> borel_measurable ?D"
-      by (auto simp: measurable_split_conv intro!: measurable_Pair measurable_Pxy)
+      by auto
     with Pxy
     show "AE x in distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x)). 0 \<le> (case x of (x, y) \<Rightarrow> Pxy (y, x))"
       by (subst AE_distr_iff)
          (auto dest!: distributed_AE
                simp: measurable_split_conv split_beta
                intro!: measurable_Pair borel_measurable_ereal_le)
     show 2: "random_variable (distr (S \<Otimes>\<^isub>M T) (T \<Otimes>\<^isub>M S) (\<lambda>(x, y). (y, x))) (\<lambda>x. (Y x, X x))"
-      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_fst]
-      using measurable_compose[OF distributed_measurable[OF Pxy] measurable_snd]
-      by (auto intro!: measurable_Pair)
+      using Pxy by auto
     { fix A assume A: "A \<in> sets (T \<Otimes>\<^isub>M S)"
       let ?B = "(\<lambda>(x, y). (y, x)) -` A \<inter> space (S \<Otimes>\<^isub>M T)"
       from sets_into_space[OF A]
       have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
         emeasure M ((\<lambda>x. (X x, Y x)) -` ?B \<inter> space M)"
         by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
       also have "\<dots> = (\<integral>\<^isup>+ x. Pxy x * indicator ?B x \<partial>(S \<Otimes>\<^isub>M T))"
-        using Pxy A by (intro distributed_emeasure measurable_sets) (auto simp: measurable_split_conv measurable_Pair)
+        using Pxy A by (intro distributed_emeasure) auto
       finally have "emeasure M ((\<lambda>x. (Y x, X x)) -` A \<inter> space M) =
         (\<integral>\<^isup>+ x. Pxy x * indicator A (snd x, fst x) \<partial>(S \<Otimes>\<^isub>M T))"
         by (auto intro!: positive_integral_cong split: split_indicator) }
     note * = this
     show "distr M ?D (\<lambda>x. (Y x, X x)) = density ?D (\<lambda>(x, y). Pxy (y, x))"
       apply (intro measure_eqI)
       apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
       apply (subst positive_integral_distr)
-      apply (auto intro!: measurable_pair measurable_Pxy * simp: comp_def split_beta)
+      apply (auto intro!: * simp: comp_def split_beta)
       done
   qed
 qed
 
 lemma (in prob_space) distr_marginal1:

 proof safe
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T by default
 
-  have XY: "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
-    using Pxy by (rule distributed_measurable)
-  then show X: "X \<in> measurable M S"
-    unfolding measurable_pair_iff by (simp add: comp_def)
-  from XY have Y: "Y \<in> measurable M T"
-    unfolding measurable_pair_iff by (simp add: comp_def)
-
-  from Pxy show borel: "Px \<in> borel_measurable S"
-    by (auto intro!: T.positive_integral_fst_measurable dest!: distributed_borel_measurable simp: Px_def)
+  note Pxy[measurable]
+  show X: "X \<in> measurable M S" by simp
+
+  show borel: "Px \<in> borel_measurable S"
+    by (auto intro!: T.positive_integral_fst_measurable simp: Px_def)
 
   interpret Pxy: prob_space "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
-    using XY by (rule prob_space_distr)
+    by (intro prob_space_distr) simp
   have "(\<integral>\<^isup>+ x. max 0 (- Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>\<^isup>+ x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
     using Pxy
-    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_borel_measurable distributed_AE)
+    by (intro positive_integral_cong_AE) (auto simp: max_def dest: distributed_AE)
 
   show "distr M S X = density S Px"
   proof (rule measure_eqI)
     fix A assume A: "A \<in> sets (distr M S X)"
-    with X Y XY have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
-      by (auto simp add: emeasure_distr
-               intro!: arg_cong[where f="emeasure M"] dest: measurable_space)
+    with X measurable_space[of Y M T]
+    have "emeasure (distr M S X) A = emeasure (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (A \<times> space T)"
+      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
     also have "\<dots> = emeasure (density (S \<Otimes>\<^isub>M T) Pxy) (A \<times> space T)"
       using Pxy by (simp add: distributed_def)
     also have "\<dots> = \<integral>\<^isup>+ x. \<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T \<partial>S"
       using A borel Pxy
-      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric] distributed_def)
+      by (simp add: emeasure_density T.positive_integral_fst_measurable(2)[symmetric])
     also have "\<dots> = \<integral>\<^isup>+ x. Px x * indicator A x \<partial>S"
       apply (rule positive_integral_cong_AE)
       using Pxy[THEN distributed_AE, THEN ST.AE_pair] AE_space
     proof eventually_elim
       fix x assume "x \<in> space S" "AE y in T. 0 \<le> Pxy (x, y)"
       moreover have eq: "\<And>y. y \<in> space T \<Longrightarrow> indicator (A \<times> space T) (x, y) = indicator A x"
         by (auto simp: indicator_def)
       ultimately have "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = (\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) * indicator A x"
-        using Pxy[THEN distributed_borel_measurable] by (simp add: eq positive_integral_multc measurable_Pair2 cong: positive_integral_cong)
+        by (simp add: eq positive_integral_multc cong: positive_integral_cong)
       also have "(\<integral>\<^isup>+ y. Pxy (x, y) \<partial>T) = Px x"
         by (simp add: Px_def ereal_real positive_integral_positive)
       finally show "(\<integral>\<^isup>+ y. Pxy (x, y) * indicator (A \<times> space T) (x, y) \<partial>T) = Px x * indicator A x" .
     qed
     finally show "emeasure (distr M S X) A = emeasure (density S Px) A"

   shows "AE y in T. Py y = (\<integral>\<^isup>+x. Pxy (x, y) \<partial>S)"
   using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)
 
 lemma (in prob_space) distributed_joint_indep':
   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
-  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
+  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
   assumes indep: "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
   shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
   unfolding distributed_def
 proof safe
   interpret S: sigma_finite_measure S by fact
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T by default
 
   interpret X: prob_space "density S Px"
     unfolding distributed_distr_eq_density[OF X, symmetric]
-    using distributed_measurable[OF X]
-    by (rule prob_space_distr)
+    by (rule prob_space_distr) simp
   have sf_X: "sigma_finite_measure (density S Px)" ..
 
   interpret Y: prob_space "density T Py"
     unfolding distributed_distr_eq_density[OF Y, symmetric]
-    using distributed_measurable[OF Y]
-    by (rule prob_space_distr)
+    by (rule prob_space_distr) simp
   have sf_Y: "sigma_finite_measure (density T Py)" ..
 
   show "distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = density (S \<Otimes>\<^isub>M T) (\<lambda>(x, y). Px x * Py y)"
     unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
     using distributed_borel_measurable[OF X] distributed_AE[OF X]
     using distributed_borel_measurable[OF Y] distributed_AE[OF Y]
-    by (rule pair_measure_density[OF _ _ _ _ S T sf_X sf_Y])
-
-  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
-    using distributed_measurable[OF X] distributed_measurable[OF Y]
-    by (auto intro: measurable_Pair)
-
-  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
-    by (auto simp: split_beta' 
-             intro!: measurable_compose[OF _ distributed_borel_measurable[OF X]]
-                     measurable_compose[OF _ distributed_borel_measurable[OF Y]])
+    by (rule pair_measure_density[OF _ _ _ _ T sf_Y])
+
+  show "random_variable (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" by auto
+
+  show Pxy: "(\<lambda>(x, y). Px x * Py y) \<in> borel_measurable (S \<Otimes>\<^isub>M T)" by auto
 
   show "AE x in S \<Otimes>\<^isub>M T. 0 \<le> (case x of (x, y) \<Rightarrow> Px x * Py y)"
     apply (intro ST.AE_pair_measure borel_measurable_ereal_le Pxy borel_measurable_const)
     using distributed_AE[OF X]
     apply eventually_elim