# HG changeset patch
# User hoelzl
# Date 1301500450 -7200
# Node ID efd229daeb2c6c45e7e7c3f95cc6dd90de58f88a
# Parent  a28e87ed996f690d93a1008f0092a674880ed130
products of probability measures are probability measures

diff -r a28e87ed996f -r efd229daeb2c src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Mar 30 17:54:01 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Mar 30 17:54:10 2011 +0200
@@ -750,4 +750,38 @@
   with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
 qed
 
+sublocale product_prob_space \<subseteq> prob_space "Pi\<^isub>P I M"
+proof
+  obtain i where "i \<in> I" using I_not_empty by auto
+  interpret i: finite_product_sigma_finite M "{i}" by default auto
+  let ?X = "\<Pi>\<^isub>E i\<in>{i}. space (M i)"
+  have "?X \<in> sets (Pi\<^isub>M {i} M)"
+    by auto
+  from measure_infprod_emb[OF _ _ _ this] `i \<in> I`
+  have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))"
+    by (simp add: i.measure_times)
+  also have "emb I {i} ?X = space (Pi\<^isub>P I M)"
+    using `i \<in> I` by (auto simp: emb_def infprod_algebra_def generator_def)
+  finally show "measure (Pi\<^isub>P I M) (space (Pi\<^isub>P I M)) = 1"
+    using M.measure_space_1 by simp
+qed
+
+lemma (in product_prob_space) measurable_component:
+  assumes "i \<in> I"
+  shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>P I M) (M i)"
+proof (unfold measurable_def, safe)
+  fix x assume "x \<in> space (Pi\<^isub>P I M)"
+  then show "x i \<in> space (M i)"
+    using `i \<in> I` by (auto simp: infprod_algebra_def generator_def)
+next
+  fix A assume "A \<in> sets (M i)"
+  with `i \<in> I` have
+    "(\<Pi>\<^isub>E x \<in> {i}. A) \<in> sets (Pi\<^isub>M {i} M)"
+    "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) = emb I {i} (\<Pi>\<^isub>E x \<in> {i}. A)"
+    by (auto simp: infprod_algebra_def generator_def emb_def)
+  from generatorI[OF _ _ _ this] `i \<in> I`
+  show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M) \<in> sets (Pi\<^isub>P I M)"
+    unfolding infprod_algebra_def by auto
+qed
+
 end
\ No newline at end of file