src/HOL/Probability/Measure.thy

--- a/src/HOL/Probability/Measure.thy	Fri Feb 04 14:16:55 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Feb 04 14:16:55 2011 +0100
@@ -624,6 +624,59 @@
   ultimately show ?thesis by (simp add: isoton_def)
 qed
 
+lemma (in measure_space) measure_space_vimage:
+  fixes M' :: "('c, 'd) measure_space_scheme"
+  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
+  shows "measure_space M'"
+proof -
+  interpret M': sigma_algebra M' by fact
+  show ?thesis
+  proof
+    show "measure M' {} = 0" using \<nu>[of "{}"] by simp
+
+    show "countably_additive M' (measure M')"
+    proof (intro countably_additiveI)
+      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
+      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
+        using `T \<in> measurable M M'` by (auto simp: measurable_def)
+      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
+        using * by blast
+      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
+        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+      ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
+        using measure_countably_additive[OF _ **] A
+        by (auto simp: comp_def vimage_UN \<nu>)
+    qed
+  qed
+qed
+
+lemma measure_unique_Int_stable_vimage:
+  fixes A :: "nat \<Rightarrow> 'a set"
+  assumes E: "Int_stable E"
+  and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
+  and N: "measure_space N" "T \<in> measurable N M"
+  and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
+  and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
+  assumes X: "X \<in> sets (sigma E)"
+  shows "measure M X = measure N (T -` X \<inter> space N)"
+proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
+  interpret M: measure_space M by fact
+  interpret N: measure_space N by fact
+  let "?T X" = "T -` X \<inter> space N"
+  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
+    by (rule M.measure_space_cong) (auto simp: M)
+  show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
+  proof (rule N.measure_space_vimage)
+    show "sigma_algebra ?E"
+      by (rule M.sigma_algebra_cong) (auto simp: M)
+    show "T \<in> measurable N ?E"
+      using `T \<in> measurable N M` by (auto simp: M measurable_def)
+  qed simp
+  show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
+qed
+
 section "@{text \<mu>}-null sets"
 
 abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
@@ -836,34 +889,6 @@
   qed
 qed
 
-lemma (in measure_space) measure_space_vimage:
-  fixes M' :: "('c, 'd) measure_space_scheme"
-  assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
-    and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
-  shows "measure_space M'"
-proof -
-  interpret M': sigma_algebra M' by fact
-  show ?thesis
-  proof
-    show "measure M' {} = 0" using \<nu>[of "{}"] by simp
-
-    show "countably_additive M' (measure M')"
-    proof (intro countably_additiveI)
-      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
-      then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
-      then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
-        using `T \<in> measurable M M'` by (auto simp: measurable_def)
-      moreover have "(\<Union>i. T -`  A i \<inter> space M) \<in> sets M"
-        using * by blast
-      moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
-        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
-      ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
-        using measure_countably_additive[OF _ **] A
-        by (auto simp: comp_def vimage_UN \<nu>)
-    qed
-  qed
-qed
-
 lemma (in measure_space) measure_space_subalgebra:
   assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M"
   and measure[simp]: "\<And>X. X \<in> sets N \<Longrightarrow> measure N X = measure M X"