# HG changeset patch
# User hoelzl
# Date 1268753248 -3600
# Node ID 7b7ae5aa396dde63e180cbed80511d54659c3ae3
# Parent  1dac16f00cd2ae85e9200be2d1b3984481ebd318
Added product measure space

diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 18 14:52:11 2010 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 16 16:27:28 2010 +0100
@@ -1093,6 +1093,7 @@
   Probability/Borel.thy						\
   Probability/Measure.thy					\
   Probability/Lebesgue.thy					\
+  Probability/Product_Measure.thy				\
   Probability/Probability_Space.thy
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
 
diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/Probability/Lebesgue.thy
--- a/src/HOL/Probability/Lebesgue.thy	Thu Mar 18 14:52:11 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy	Tue Mar 16 16:27:28 2010 +0100
@@ -1389,6 +1389,7 @@
 qed
 
 lemma integral_on_countable:
+  fixes enum :: "nat \<Rightarrow> real"
   assumes borel: "f \<in> borel_measurable M"
   and bij: "bij_betw enum S (f ` space M)"
   and enum_zero: "enum ` (-S) \<subseteq> {0}"
diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Thu Mar 18 14:52:11 2010 +0100
+++ b/src/HOL/Probability/Probability.thy	Tue Mar 16 16:27:28 2010 +0100
@@ -1,5 +1,5 @@
 theory Probability
-imports Probability_Space
+imports Probability_Space Product_Measure
 begin
 
 end
diff -r 1dac16f00cd2 -r 7b7ae5aa396d src/HOL/Probability/Product_Measure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Product_Measure.thy	Tue Mar 16 16:27:28 2010 +0100
@@ -0,0 +1,160 @@
+theory Product_Measure
+imports "~~/src/HOL/Probability/Lebesgue"
+begin
+
+definition
+  "prod_measure M M' = (\<lambda>a. measure_space.integral M (\<lambda>s0. measure M' ((\<lambda>s1. (s0, s1)) -` a)))"
+
+definition
+  "prod_measure_space M M' \<equiv>
+    \<lparr> space = space M \<times> space M',
+      sets = sets (sigma (space M \<times> space M') (prod_sets (sets M) (sets M'))),
+      measure = prod_measure M M' \<rparr>"
+
+lemma prod_measure_times:
+  assumes "measure_space M" and "measure_space M'" and a: "a \<in> sets M"
+  shows "prod_measure M M' (a \<times> a') = measure M a * measure M' a'"
+proof -
+  interpret M: measure_space M by fact
+  interpret M': measure_space M' by fact
+
+  { fix \<omega>
+    have "(\<lambda>\<omega>'. (\<omega>, \<omega>')) -` (a \<times> a') = (if \<omega> \<in> a then a' else {})"
+      by auto
+    hence "measure M' ((\<lambda>\<omega>'. (\<omega>, \<omega>')) -` (a \<times> a')) =
+      measure M' a' * indicator_fn a \<omega>"
+      unfolding indicator_fn_def by auto }
+  note vimage_eq_indicator = this
+
+  show ?thesis
+    unfolding prod_measure_def vimage_eq_indicator
+      M.integral_cmul_indicator(1)[OF `a \<in> sets M`]
+    by simp
+qed
+
+
+
+lemma measure_space_finite_prod_measure:
+  fixes M :: "('a, 'b) measure_space_scheme"
+    and M' :: "('c, 'd) measure_space_scheme"
+  assumes "measure_space M" and "measure_space M'"
+  and finM: "finite (space M)" "Pow (space M) = sets M"
+  and finM': "finite (space M')" "Pow (space M') = sets M'"
+  shows "measure_space (prod_measure_space M M')"
+proof (rule finite_additivity_sufficient)
+  interpret M: measure_space M by fact
+  interpret M': measure_space M' by fact
+
+  have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"
+    unfolding prod_measure_space_def by simp
+
+  have prod_sets: "prod_sets (sets M) (sets M') \<subseteq> Pow (space M \<times> space M')"
+    using M.sets_into_space M'.sets_into_space unfolding prod_sets_def by auto
+  show sigma: "sigma_algebra (prod_measure_space M M')" unfolding prod_measure_space_def
+    by (rule sigma_algebra_sigma_sets[where a="prod_sets (sets M) (sets M')"])
+       (simp_all add: sigma_def prod_sets)
+
+  then interpret sa: sigma_algebra "prod_measure_space M M'" .
+
+  { fix x y assume "y \<in> sets (prod_measure_space M M')" and "x \<in> space M"
+    hence "y \<subseteq> space M \<times> space M'"
+      using sa.sets_into_space unfolding prod_measure_space_def by simp
+    hence "Pair x -` y \<in> sets M'"
+      using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }
+  note Pair_in_sets = this
+
+  show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))"
+    unfolding measure additive_def
+  proof safe
+    fix x y assume x: "x \<in> sets (prod_measure_space M M')" and y: "y \<in> sets (prod_measure_space M M')"
+      and disj_x_y: "x \<inter> y = {}"
+    { fix z have "Pair z -` x \<inter> Pair z -` y = {}" using disj_x_y by auto }
+    note Pair_disj = this
+
+    from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]
+    show "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y"
+      unfolding prod_measure_def
+      apply (subst (1 2 3) M.integral_finite_singleton[OF finM])
+      by (simp_all add: setsum_addf[symmetric] field_simps)
+  qed
+
+  show "finite (space (prod_measure_space M M'))"
+    unfolding prod_measure_space_def using finM finM' by simp
+
+  have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"
+    unfolding finM(2)[symmetric] by simp
+
+  show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))"
+    unfolding positive_def
+  proof (safe, simp add: M.integral_zero prod_measure_space_def prod_measure_def)
+    fix Q assume "Q \<in> sets (prod_measure_space M M')"
+    from Pair_in_sets[OF this]
+    show "0 \<le> measure (prod_measure_space M M') Q"
+      unfolding prod_measure_space_def prod_measure_def
+      apply (subst M.integral_finite_singleton[OF finM])
+      using M.positive M'.positive singletonM
+      by (auto intro!: setsum_nonneg mult_nonneg_nonneg)
+  qed
+qed
+
+lemma measure_space_finite_prod_measure_alterantive:
+  assumes "measure_space M" and "measure_space M'"
+  and finM: "finite (space M)" "Pow (space M) = sets M"
+  and finM': "finite (space M')" "Pow (space M') = sets M'"
+  shows "measure_space \<lparr> space = space M \<times> space M',
+                         sets = Pow (space M \<times> space M'),
+		         measure = prod_measure M M' \<rparr>"
+  (is "measure_space ?space")
+proof (rule finite_additivity_sufficient)
+  interpret M: measure_space M by fact
+  interpret M': measure_space M' by fact
+
+  show "sigma_algebra ?space"
+    using sigma_algebra.sigma_algebra_extend[where M="\<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M') \<rparr>"]
+    by (auto intro!: sigma_algebra_Pow)
+  then interpret sa: sigma_algebra ?space .
+
+  have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"
+    unfolding prod_measure_space_def by simp
+
+  { fix x y assume "y \<in> sets ?space" and "x \<in> space M"
+    hence "y \<subseteq> space M \<times> space M'"
+      using sa.sets_into_space by simp
+    hence "Pair x -` y \<in> sets M'"
+      using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }
+  note Pair_in_sets = this
+
+  show "additive ?space (measure ?space)"
+    unfolding measure additive_def
+  proof safe
+    fix x y assume x: "x \<in> sets ?space" and y: "y \<in> sets ?space"
+      and disj_x_y: "x \<inter> y = {}"
+    { fix z have "Pair z -` x \<inter> Pair z -` y = {}" using disj_x_y by auto }
+    note Pair_disj = this
+
+    from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]
+    show "measure ?space (x \<union> y) = measure ?space x + measure ?space y"
+      apply (simp add: prod_measure_def)
+      apply (subst (1 2 3) M.integral_finite_singleton[OF finM])
+      by (simp_all add: setsum_addf[symmetric] field_simps)
+  qed
+
+  show "finite (space ?space)" using finM finM' by simp
+
+  have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"
+    unfolding finM(2)[symmetric] by simp
+
+  show "positive ?space (measure ?space)"
+    unfolding positive_def
+  proof (safe, simp add: M.integral_zero prod_measure_def)
+    fix Q assume "Q \<in> sets ?space"
+    from Pair_in_sets[OF this]
+    show "0 \<le> measure ?space Q"
+      unfolding prod_measure_space_def prod_measure_def
+      apply (subst M.integral_finite_singleton[OF finM])
+      using M.positive M'.positive singletonM
+      by (auto intro!: setsum_nonneg mult_nonneg_nonneg)
+  qed
+qed
+
+end
\ No newline at end of file