# HG changeset patch
# User hoelzl
# Date 1269622981 -3600
# Node ID 30d42bfd01748495653882bca88e335bd1eef9c8
# Parent  71620f11dbbbb1b4ed447518f8174d99ac88a3fd
Added finite measure space.

diff -r 71620f11dbbb -r 30d42bfd0174 src/HOL/Probability/Lebesgue.thy
--- a/src/HOL/Probability/Lebesgue.thy	Thu Mar 25 23:18:42 2010 +0100
+++ b/src/HOL/Probability/Lebesgue.thy	Fri Mar 26 18:03:01 2010 +0100
@@ -1542,31 +1542,6 @@
     integral_cong[of "\<lambda>x. f x * indicator_fn (space M) x" f]
   by (auto simp add: indicator_fn_def)
 
-lemma integral_finite_singleton:
-  assumes fin: "finite (space M)" and "Pow (space M) = sets M"
-  shows "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
-proof -
-  have "f \<in> borel_measurable M"
-    unfolding borel_measurable_le_iff
-    using assms by auto
-  { fix r let ?x = "f -` {r} \<inter> space M"
-    have "?x \<subseteq> space M" by auto
-    with assms have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
-      by (auto intro!: measure_real_sum_image) }
-  note measure_eq_setsum = this
-  show ?thesis
-    unfolding integral_finite[OF `f \<in> borel_measurable M` fin]
-      measure_eq_setsum setsum_right_distrib
-    apply (subst setsum_Sigma)
-    apply (simp add: assms)
-    apply (simp add: assms)
-  proof (rule setsum_reindex_cong[symmetric])
-    fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
-    thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
-      by auto
-  qed (auto intro!: image_eqI inj_onI)
-qed
-
 section "Radon–Nikodym derivative"
 
 definition
@@ -1574,48 +1549,103 @@
     f \<in> borel_measurable M \<and>
     (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
 
-lemma RN_deriv_finite_singleton:
+end
+
+locale finite_measure_space = measure_space +
+  assumes finite_space: "finite (space M)"
+  and sets_eq_Pow: "sets M = Pow (space M)"
+
+lemma sigma_algebra_cong:
+  fixes M :: "('a, 'b) algebra_scheme" and M' :: "('a, 'c) algebra_scheme"
+  assumes *: "sigma_algebra M"
+  and cong: "space M = space M'" "sets M = sets M'"
+  shows "sigma_algebra M'"
+using * unfolding sigma_algebra_def algebra_def sigma_algebra_axioms_def unfolding cong .
+
+lemma finite_Pow_additivity_sufficient:
+  assumes "finite (space M)" and "sets M = Pow (space M)"
+  and "positive M (measure M)" and "additive M (measure M)"
+  shows "finite_measure_space M"
+proof -
+  have "sigma_algebra M"
+    using assms by (auto intro!: sigma_algebra_cong[OF sigma_algebra_Pow])
+
+  have "measure_space M"
+    by (rule Measure.finite_additivity_sufficient) (fact+)
+  thus ?thesis
+    unfolding finite_measure_space_def finite_measure_space_axioms_def
+    using assms by simp
+qed
+
+lemma finite_measure_spaceI:
+  assumes "measure_space M" and "finite (space M)" and "sets M = Pow (space M)"
+  shows "finite_measure_space M"
+  unfolding finite_measure_space_def finite_measure_space_axioms_def
+  using assms by simp
+
+lemma (in finite_measure_space) integral_finite_singleton:
+  "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
+proof -
+  have "f \<in> borel_measurable M"
+    unfolding borel_measurable_le_iff
+    using sets_eq_Pow by auto
+  { fix r let ?x = "f -` {r} \<inter> space M"
+    have "?x \<subseteq> space M" by auto
+    with finite_space sets_eq_Pow have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
+      by (auto intro!: measure_real_sum_image) }
+  note measure_eq_setsum = this
+  show ?thesis
+    unfolding integral_finite[OF `f \<in> borel_measurable M` finite_space]
+      measure_eq_setsum setsum_right_distrib
+    apply (subst setsum_Sigma)
+    apply (simp add: finite_space)
+    apply (simp add: finite_space)
+  proof (rule setsum_reindex_cong[symmetric])
+    fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
+    thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
+      by auto
+  qed (auto intro!: image_eqI inj_onI)
+qed
+
+lemma (in finite_measure_space) RN_deriv_finite_singleton:
   fixes v :: "'a set \<Rightarrow> real"
-  assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M"
-  and ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
+  assumes ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
   and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
   and "x \<in> space M" and "measure M {x} \<noteq> 0"
   shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
   unfolding RN_deriv_def
 proof (rule someI2_ex[where Q = "\<lambda>f. f x = ?v x"], rule exI[where x = ?v], safe)
   show "(\<lambda>a. v {a} / measure_space.measure M {a}) \<in> borel_measurable M"
-    unfolding borel_measurable_le_iff using Pow by auto
+    unfolding borel_measurable_le_iff using sets_eq_Pow by auto
 next
   fix a assume "a \<in> sets M"
   hence "a \<subseteq> space M" and "finite a"
-    using sets_into_space finite by (auto intro: finite_subset)
+    using sets_into_space finite_space by (auto intro: finite_subset)
   have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
     v {x} * indicator_fn a x" using eq_0 by auto
 
   from measure_space.measure_real_sum_image[OF ms_v, of a]
-    Pow `a \<in> sets M` sets_into_space `finite a`
+    sets_eq_Pow `a \<in> sets M` sets_into_space `finite a`
   have "v a = (\<Sum>x\<in>a. v {x})" by auto
   thus "integral (\<lambda>x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a"
-    apply (simp add: eq_0 integral_finite_singleton[OF finite Pow])
+    apply (simp add: eq_0 integral_finite_singleton)
     apply (unfold divide_1)
-    by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \<subseteq> space M` Int_absorb1)
+    by (simp add: * indicator_fn_def if_distrib setsum_cases finite_space `a \<subseteq> space M` Int_absorb1)
 next
   fix w assume "w \<in> borel_measurable M"
   assume int_eq_v: "\<forall>a\<in>sets M. integral (\<lambda>x. w x * indicator_fn a x) = v a"
-  have "{x} \<in> sets M" using Pow `x \<in> space M` by auto
+  have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
 
   have "w x * measure M {x} =
     (\<Sum>y\<in>space M. w y * indicator_fn {x} y * measure M {y})"
     apply (subst (3) mult_commute)
-    unfolding indicator_fn_def if_distrib setsum_cases[OF finite]
+    unfolding indicator_fn_def if_distrib setsum_cases[OF finite_space]
     using `x \<in> space M` by simp
   also have "... = v {x}"
     using int_eq_v[rule_format, OF `{x} \<in> sets M`]
-    by (simp add: integral_finite_singleton[OF finite Pow])
+    by (simp add: integral_finite_singleton)
   finally show "w x = v {x} / measure M {x}"
     using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
 qed fact
 
 end
-
-end
diff -r 71620f11dbbb -r 30d42bfd0174 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Thu Mar 25 23:18:42 2010 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Mar 26 18:03:01 2010 +0100
@@ -10,7 +10,34 @@
   "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
 
 lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
-  by (auto simp add: prod_sets_def) 
+  by (auto simp add: prod_sets_def)
+
+lemma sigma_prod_sets_finite:
+  assumes "finite A" and "finite B"
+  shows "sets (sigma (A \<times> B) (prod_sets (Pow A) (Pow B))) = Pow (A \<times> B)"
+proof (simp add: sigma_def, safe)
+  have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
+
+  fix x assume subset: "x \<subseteq> A \<times> B"
+  hence "finite x" using fin by (rule finite_subset)
+  from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"
+    (is "x \<in> sigma_sets ?prod ?sets")
+  proof (induct x)
+    case empty show ?case by (rule sigma_sets.Empty)
+  next
+    case (insert a x)
+    hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)
+    moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
+    ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
+  qed
+next
+  fix x a b
+  assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"
+  from sigma_sets_into_sp[OF _ this(1)] this(2)
+  show "a \<in> A" and "b \<in> B"
+    by (auto simp: prod_sets_def)
+qed
+
 
 definition
   closed_cdi  where
@@ -26,7 +53,7 @@
   smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
   for M
   where
-    Basic [intro]: 
+    Basic [intro]:
       "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
   | Compl [intro]:
       "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
diff -r 71620f11dbbb -r 30d42bfd0174 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Thu Mar 25 23:18:42 2010 +0100
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Mar 26 18:03:01 2010 +0100
@@ -350,75 +350,6 @@
   assumes "finite (space M) \<and> random_variable borel_space X"
   shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})"
 using assms unfolding distribution_def using finite_expectation1 by auto
-
-lemma finite_marginal_product_space_POW:
-  assumes "Pow (space M) = events"
-  assumes "random_variable \<lparr> space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
-  assumes "random_variable \<lparr> space = Y ` (space M), sets = Pow (Y ` (space M))\<rparr> Y"
-  assumes "finite (space M)"
-  shows "measure_space \<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),
-  sets = Pow ((X ` (space M)) \<times> (Y ` (space M))),
-  measure = (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))\<rparr>"
-  using assms
-proof -
-  let "?S" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))), 
-    sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
-  let "?M" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))), 
-    sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
-  have pos: "positive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
-    unfolding positive_def using positive'[unfolded positive_def] assms by auto
-  { fix x y
-    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
-    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
-    assume "x \<inter> y = {}"
-    from additive[unfolded additive_def, rule_format, OF A B] this
-    have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
-      (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
-      prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
-      prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)" 
-      apply (subst Int_Un_distrib2)
-      by auto }
-  hence add: "additive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
-    unfolding additive_def by auto
-  interpret S: sigma_algebra "?S" 
-    unfolding sigma_algebra_def algebra_def
-      sigma_algebra_axioms_def by auto
-  show ?thesis
-     using add pos S.finite_additivity_sufficient assms by auto
-qed
-
-lemma finite_marginal_product_space_POW2:
-  assumes "Pow (space M) = events"
-  assumes "random_variable \<lparr>space = s1, sets = Pow s1\<rparr> X"
-  assumes "random_variable \<lparr>space = s2, sets = Pow s2\<rparr> Y"
-  assumes "finite (space M)"
-  assumes "finite s1" "finite s2"
-  shows "measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
-proof -
-  let "?S" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2) \<rparr>"
-  let "?M" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y \<rparr>"
-  have pos: "positive ?S (joint_distribution X Y)" using positive'
-    unfolding positive_def joint_distribution_def using assms by auto
-  { fix x y
-    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
-    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
-    assume "x \<inter> y = {}"
-    from additive[unfolded additive_def, rule_format, OF A B] this
-    have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
-      (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
-      prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
-      prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)" 
-      apply (subst Int_Un_distrib2)
-      by auto }
-  hence add: "additive ?S (joint_distribution X Y)"
-    unfolding additive_def joint_distribution_def by auto
-  interpret S: sigma_algebra "?S" 
-    unfolding sigma_algebra_def algebra_def
-      sigma_algebra_axioms_def by auto
-  show ?thesis
-     using add pos S.finite_additivity_sufficient assms by auto
-qed
-
 lemma prob_x_eq_1_imp_prob_y_eq_0:
   assumes "{x} \<in> events"
   assumes "(prob {x} = 1)"
@@ -453,6 +384,45 @@
   ultimately show ?thesis by auto
 qed
 
+
 end
 
+locale finite_prob_space = prob_space + finite_measure_space
+
+lemma (in finite_prob_space) finite_marginal_product_space_POW2:
+  assumes "finite s1" "finite s2"
+  shows "finite_measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
+    (is "finite_measure_space ?M")
+proof (rule finite_Pow_additivity_sufficient)
+  show "positive ?M (measure ?M)"
+    unfolding positive_def using positive'[unfolded positive_def] assms sets_eq_Pow
+    by (simp add: joint_distribution_def)
+
+  show "additive ?M (measure ?M)" unfolding additive_def
+  proof safe
+    fix x y
+    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
+    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms sets_eq_Pow by auto
+    assume "x \<inter> y = {}"
+    from additive[unfolded additive_def, rule_format, OF A B] this
+    show "measure ?M (x \<union> y) = measure ?M x + measure ?M y"
+      apply (simp add: joint_distribution_def)
+      apply (subst Int_Un_distrib2)
+      by auto
+  qed
+
+  show "finite (space ?M)"
+    using assms by auto
+
+  show "sets ?M = Pow (space ?M)"
+    by simp
+qed
+
+lemma (in finite_prob_space) finite_marginal_product_space_POW:
+  shows "finite_measure_space \<lparr> space = X ` space M \<times> Y ` space M,
+                                sets = Pow (X ` space M \<times> Y ` space M),
+                                measure = joint_distribution X Y\<rparr>"
+    (is "finite_measure_space ?M")
+  using finite_space by (auto intro!: finite_marginal_product_space_POW2)
+
 end
diff -r 71620f11dbbb -r 30d42bfd0174 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Thu Mar 25 23:18:42 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy	Fri Mar 26 18:03:01 2010 +0100
@@ -32,129 +32,66 @@
     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
+lemma finite_prod_measure_space:
+  assumes "finite_measure_space M" and "finite_measure_space M'"
+  shows "prod_measure_space M M' =
+      \<lparr> space = space M \<times> space M',
+        sets = Pow (space M \<times> space M'),
+        measure = prod_measure M M' \<rparr>"
+proof -
+  interpret M: finite_measure_space M by fact
+  interpret M': finite_measure_space M' by fact
+  show ?thesis using M.finite_space M'.finite_space
+    by (simp add: sigma_prod_sets_finite M.sets_eq_Pow M'.sets_eq_Pow
+      prod_measure_space_def)
+qed
 
-  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)
+lemma finite_measure_space_finite_prod_measure:
+  assumes "finite_measure_space M" and "finite_measure_space M'"
+  shows "finite_measure_space (prod_measure_space M M')"
+proof (rule finite_Pow_additivity_sufficient)
+  interpret M: finite_measure_space M by fact
+  interpret M': finite_measure_space M' by fact
 
-  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
+  from M.finite_space M'.finite_space
+  show "finite (space (prod_measure_space M M'))" and
+    "sets (prod_measure_space M M') = Pow (space (prod_measure_space M M'))"
+    by (simp_all add: finite_prod_measure_space[OF assms])
 
   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')"
+    unfolding additive_def finite_prod_measure_space[OF assms]
+  proof (simp, safe)
+    fix x y assume subs: "x \<subseteq> space M \<times> space M'" "y \<subseteq> space M \<times> space 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])
+    have "\<And>z. measure M' (Pair z -` x \<union> Pair z -` y) =
+        measure M' (Pair z -` x) + measure M' (Pair z -` y)"
+      using disj_x_y subs by (subst M'.measure_additive) (auto simp: M'.sets_eq_Pow)
+    thus "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y"
+      unfolding prod_measure_def M.integral_finite_singleton
       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
+    by (auto intro!: setsum_nonneg mult_nonneg_nonneg M'.positive M.positive
+      simp add: M.integral_zero finite_prod_measure_space[OF assms]
+        prod_measure_def M.integral_finite_singleton
+        M.sets_eq_Pow M'.sets_eq_Pow)
 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
+lemma finite_measure_space_finite_prod_measure_alterantive:
+  assumes M: "finite_measure_space M" and M': "finite_measure_space M'"
+  shows "finite_measure_space \<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M'), measure = prod_measure M M' \<rparr>"
+    (is "finite_measure_space ?M")
+proof -
+  interpret M: finite_measure_space M by fact
+  interpret M': finite_measure_space M' by fact
 
-  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
+  show ?thesis
+    using finite_measure_space_finite_prod_measure[OF assms]
+    unfolding prod_measure_space_def M.sets_eq_Pow M'.sets_eq_Pow
+    using M.finite_space M'.finite_space
+    by (simp add: sigma_prod_sets_finite)
 qed
 
 end
\ No newline at end of file