# HG changeset patch
# User hoelzl
# Date 1305901383 -7200
# Node ID a61e30bfd0bc83d6fec3c2bcd2dfbfd7ea80ac21
# Parent  e2f4736719377f3cb107e1b00327fe4a4997313f
add lemma prob_finite_product

diff -r e2f473671937 -r a61e30bfd0bc src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri May 20 16:22:24 2011 +0200
+++ b/src/HOL/Probability/Measure.thy	Fri May 20 16:23:03 2011 +0200
@@ -1379,6 +1379,11 @@
     by (auto intro!: finite_measure_spaceI)
 qed
 
+lemma (in finite_measure_space) finite_measure_singleton:
+  assumes A: "A \<subseteq> space M" shows "\<mu>' A = (\<Sum>x\<in>A. \<mu>' {x})"
+  using A finite_subset[OF A finite_space]
+  by (intro finite_measure_finite_singleton) auto
+
 lemma suminf_cmult_indicator:
   fixes f :: "nat \<Rightarrow> extreal"
   assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
diff -r e2f473671937 -r a61e30bfd0bc src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri May 20 16:22:24 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri May 20 16:23:03 2011 +0200
@@ -598,22 +598,22 @@
     using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
 qed
 
+lemma (in product_finite_prob_space) singleton_eq_product:
+  assumes x: "x \<in> space P" shows "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
+proof (safe intro!: ext[of _ x])
+  fix y i assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
+  with x show "y i = x i"
+    by (cases "i \<in> I") (auto simp: extensional_def)
+qed (insert x, auto)
+
 sublocale product_finite_prob_space \<subseteq> finite_prob_space "Pi\<^isub>M I M"
 proof
   show "finite (space P)"
     using finite_index M.finite_space by auto
 
   { fix x assume "x \<in> space P"
-    then have x: "{x} = (\<Pi>\<^isub>E i\<in>I. {x i})"
-    proof safe
-      fix y assume *: "y \<in> (\<Pi> i\<in>I. {x i})" "y \<in> extensional I"
-      show "y = x"
-      proof
-        fix i show "y i = x i"
-          using * `x \<in> space P` by (cases "i \<in> I") (auto simp: extensional_def)
-      qed
-    qed auto
-    with `x \<in> space P` have "{x} \<in> sets P"
+    with this[THEN singleton_eq_product]
+    have "{x} \<in> sets P"
       by (auto intro!: in_P) }
   note x_in_P = this
 
@@ -628,7 +628,6 @@
   qed
   with space_closed show [simp]: "sets P = Pow (space P)" ..
 
-
   { fix x assume "x \<in> space P"
     from this top have "\<mu> {x} \<le> \<mu> (space P)" by (intro measure_mono) auto
     then show "\<mu> {x} \<noteq> \<infinity>"
@@ -639,7 +638,12 @@
   "(\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)) \<Longrightarrow> \<mu> (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.\<mu> i (X i))"
   by (rule measure_times) simp
 
-lemma (in product_finite_prob_space) prob_times:
+lemma (in product_finite_prob_space) measure_singleton_times:
+  assumes x: "x \<in> space P" shows "\<mu> {x} = (\<Prod>i\<in>I. M.\<mu> i {x i})"
+  unfolding singleton_eq_product[OF x] using x
+  by (intro measure_finite_times) auto
+
+lemma (in product_finite_prob_space) prob_finite_times:
   assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<subseteq> space (M i)"
   shows "prob (\<Pi>\<^isub>E i\<in>I. X i) = (\<Prod>i\<in>I. M.prob i (X i))"
 proof -
@@ -652,6 +656,18 @@
   finally show ?thesis by simp
 qed
 
+lemma (in product_finite_prob_space) prob_singleton_times:
+  assumes x: "x \<in> space P"
+  shows "prob {x} = (\<Prod>i\<in>I. M.prob i {x i})"
+  unfolding singleton_eq_product[OF x] using x
+  by (intro prob_finite_times) auto
+
+lemma (in product_finite_prob_space) prob_finite_product:
+  "A \<subseteq> space P \<Longrightarrow> prob A = (\<Sum>x\<in>A. \<Prod>i\<in>I. M.prob i {x i})"
+  by (auto simp add: finite_measure_singleton prob_singleton_times
+           simp del: space_product_algebra
+           intro!: setsum_cong prob_singleton_times)
+
 lemma (in prob_space) joint_distribution_finite_prob_space:
   assumes X: "finite_random_variable MX X"
   assumes Y: "finite_random_variable MY Y"