author hoelzl Mon, 23 Mar 2015 10:16:20 +0100 changeset 59778 fe5b796d6b2a parent 59777 9ad96e97e72d child 59779 b6bda9140e39 child 59780 23b67731f4f0
```--- a/src/HOL/Probability/Giry_Monad.thy	Mon Mar 23 08:45:54 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Mon Mar 23 10:16:20 2015 +0100
@@ -221,6 +221,22 @@
K \<in> measurable M (subprob_algebra N)"
by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)

+lemma measurable_submarkov:
+  "K \<in> measurable M (subprob_algebra M) \<longleftrightarrow>
+    (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
+    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)"
+proof
+  assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
+    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
+  then show "K \<in> measurable M (subprob_algebra M)"
+    by (intro measurable_subprob_algebra) auto
+next
+  assume "K \<in> measurable M (subprob_algebra M)"
+  then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
+    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
+    by (auto dest: subprob_space_kernel sets_kernel)
+qed
+
lemma space_subprob_algebra_empty_iff:
"space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
proof```