# HG changeset patch
# User hoelzl
# Date 1444295983 -7200
# Node ID 48d1b147f0948029ef5ad3128382f56f2a3283e3
# Parent  8b5f00202e1a34b45c3291e77dbd74c7f889d691
generalize eqI theorems for product measures

diff -r 8b5f00202e1a -r 48d1b147f094 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Oct 07 23:28:49 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Thu Oct 08 11:19:43 2015 +0200
@@ -740,6 +740,49 @@
   unfolding pred_def
   by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
 
+lemma measure_eqI_PiM_finite:
+  assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M"
+  assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)"
+  assumes A: "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = space (PiM I M)" "\<And>i::nat. P (A i) \<noteq> \<infinity>"
+  shows "P = Q"
+proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
+  show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>"
+    unfolding space_PiM[symmetric] by fact+
+  fix X assume "X \<in> prod_algebra I M"
+  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
+    and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
+    by (force elim!: prod_algebraE)
+  then show "emeasure P X = emeasure Q X"
+    unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq)
+qed (simp_all add: sets_PiM)
+
+lemma measure_eqI_PiM_infinite:
+  assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M"
+  assumes eq: "\<And>A J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow>
+    P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))"
+  assumes A: "finite_measure P"
+  shows "P = Q"
+proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
+  interpret finite_measure P by fact
+  def i \<equiv> "SOME i. i \<in> I"
+  have i: "I \<noteq> {} \<Longrightarrow> i \<in> I"
+    unfolding i_def by (rule someI_ex) auto
+  def A \<equiv> "\<lambda>n::nat. if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
+  then show "range A \<subseteq> prod_algebra I M"
+    using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i)
+  have "\<And>i. A i = space (PiM I M)"
+    by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI)
+  then show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. emeasure P (A i) \<noteq> \<infinity>"
+    by (auto simp: space_PiM)
+next
+  fix X assume X: "X \<in> prod_algebra I M"
+  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
+    and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
+    by (force elim!: prod_algebraE)
+  then show "emeasure P X = emeasure Q X"
+    by (auto intro!: eq)
+qed (auto simp: sets_PiM)
+
 locale product_sigma_finite =
   fixes M :: "'i \<Rightarrow> 'a measure"
   assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
@@ -860,7 +903,7 @@
 qed simp
 
 lemma (in product_sigma_finite) PiM_eqI:
-  assumes "finite I" "sets P = PiM I M"
+  assumes I[simp]: "finite I" and P: "sets P = PiM I M"
   assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   shows "P = PiM I M"
 proof -
@@ -868,24 +911,12 @@
     proof qed fact
   from sigma_finite_pairs guess C .. note C = this
   show ?thesis
-  proof (rule measure_eqI_generator_eq[symmetric, OF Int_stable_prod_algebra prod_algebra_sets_into_space])
-    show "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
-      by (rule sets_PiM)
-    then show "sets P = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
-      unfolding `sets P = sets (PiM I M)` by simp
+  proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric])
+    show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A
+      by (simp add: eq emeasure_PiM)
     def A \<equiv> "\<lambda>n. \<Pi>\<^sub>E i\<in>I. C i n"
-    show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>"
-      using C \<open>finite I\<close>
-      by (auto intro!: prod_algebraI_finite simp: A_def emeasure_PiM subset_eq setprod_PInf emeasure_nonneg)
-    show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
-      using C by (simp add: A_def space_PiM)
-
-    fix X assume X: "X \<in> prod_algebra I M"
-    then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
-      and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
-      by (force elim!: prod_algebraE)
-    show "emeasure (PiM I M) X = emeasure P X"
-      unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq emeasure_PiM J \<open>finite I\<close>)
+    with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)"
+      by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq setprod_PInf emeasure_nonneg)
   qed
 qed
 
diff -r 8b5f00202e1a -r 48d1b147f094 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 07 23:28:49 2015 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Thu Oct 08 11:19:43 2015 +0200
@@ -102,41 +102,14 @@
 qed simp
 
 lemma (in product_prob_space) PiM_eq:
-  assumes "sets M' = sets (PiM I M)"
+  assumes M': "sets M' = sets (PiM I M)"
   assumes eq: "\<And>J F. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>j. j \<in> J \<Longrightarrow> F j \<in> sets (M j)) \<Longrightarrow>
     emeasure M' (prod_emb I M J (\<Pi>\<^sub>E j\<in>J. F j)) = (\<Prod>j\<in>J. emeasure (M j) (F j))"
   shows "M' = (PiM I M)"
-proof (rule measure_eqI_generator_eq[symmetric, OF Int_stable_prod_algebra prod_algebra_sets_into_space])
-  show "sets (PiM I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
-    by (rule sets_PiM)
-  then show "sets M' = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
-    unfolding `sets M' = sets (PiM I M)` by simp
-
-  def i \<equiv> "SOME i. i \<in> I"
-  have i: "I \<noteq> {} \<Longrightarrow> i \<in> I"
-    unfolding i_def by (rule someI_ex) auto
-
-  def A \<equiv> "\<lambda>n::nat. if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
-  then show "range A \<subseteq> prod_algebra I M"
-    using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i)
-
-  have A_eq: "\<And>i. A i = space (PiM I M)"
-    by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI)
-  show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
-    unfolding A_eq by (auto simp: space_PiM)
-  show "\<And>i. emeasure (PiM I M) (A i) \<noteq> \<infinity>"
-    unfolding A_eq P.emeasure_space_1 by simp
-next
-  fix X assume X: "X \<in> prod_algebra I M"
-  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
-    and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
-    by (force elim!: prod_algebraE)
-  from eq[OF J] have "emeasure M' X = (\<Prod>j\<in>J. emeasure (M j) (E j))"
-    by (simp add: X)
-  also have "\<dots> = emeasure (PiM I M) X"
-    unfolding X using J by (intro emeasure_PiM_emb[symmetric]) auto
-  finally show "emeasure (PiM I M) X = emeasure M' X" ..
-qed
+proof (rule measure_eqI_PiM_infinite[symmetric, OF refl M'])
+  show "finite_measure (Pi\<^sub>M I M)"
+    by standard (simp add: P.emeasure_space_1)
+qed (simp add: eq emeasure_PiM_emb)
 
 lemma (in product_prob_space) AE_component: "i \<in> I \<Longrightarrow> AE x in M i. P x \<Longrightarrow> AE x in PiM I M. P (x i)"
   apply (rule AE_distrD[of "\<lambda>\<omega>. \<omega> i" "PiM I M" "M i" P])