# 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: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)" + assumes A: "range A \ prod_algebra I M" "(\i. A i) = space (PiM I M)" "\i::nat. P (A i) \ \" + shows "P = Q" +proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space]) + show "range A \ prod_algebra I M" "(\i. A i) = (\\<^sub>E i\I. space (M i))" "\i. P (A i) \ \" + unfolding space_PiM[symmetric] by fact+ + fix X assume "X \ 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 \ I" "\j. j \ J \ E j \ 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: "\A J. finite J \ J \ I \ (\i. i \ J \ A i \ sets (M i)) \ + 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 \ "SOME i. i \ I" + have i: "I \ {} \ i \ I" + unfolding i_def by (rule someI_ex) auto + def A \ "\n::nat. if I = {} then prod_emb I M {} (\\<^sub>E i\{}. {}) else prod_emb I M {i} (\\<^sub>E i\{i}. space (M i))" + then show "range A \ prod_algebra I M" + using prod_algebraI[of "{}" I "\i. space (M i)" M] by (auto intro!: prod_algebraI i) + have "\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 "(\i. A i) = (\\<^sub>E i\I. space (M i))" "\i. emeasure P (A i) \ \" + by (auto simp: space_PiM) +next + fix X assume X: "X \ 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 \ I" "\j. j \ J \ E j \ 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 \ 'a measure" assumes sigma_finite_measures: "\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: "\A. (\i. i \ I \ A i \ sets (M i)) \ P (Pi\<^sub>E I A) = (\i\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 (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" - by (rule sets_PiM) - then show "sets P = sigma_sets (\\<^sub>E i\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 "(\i. i \ I \ A i \ sets (M i)) \ (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 \ "\n. \\<^sub>E i\I. C i n" - show "range A \ prod_algebra I M" "\i. emeasure (Pi\<^sub>M I M) (A i) \ \" - using C \finite I\ - by (auto intro!: prod_algebraI_finite simp: A_def emeasure_PiM subset_eq setprod_PInf emeasure_nonneg) - show "(\i. A i) = (\\<^sub>E i\I. space (M i))" - using C by (simp add: A_def space_PiM) - - fix X assume X: "X \ 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 \ I" "\j. j \ J \ E j \ 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 \finite I\) + with C show "range A \ prod_algebra I M" "\i. emeasure (Pi\<^sub>M I M) (A i) \ \" "(\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: "\J F. finite J \ J \ I \ (\j. j \ J \ F j \ sets (M j)) \ emeasure M' (prod_emb I M J (\\<^sub>E j\J. F j)) = (\j\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 (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" - by (rule sets_PiM) - then show "sets M' = sigma_sets (\\<^sub>E i\I. space (M i)) (prod_algebra I M)" - unfolding `sets M' = sets (PiM I M)` by simp - - def i \ "SOME i. i \ I" - have i: "I \ {} \ i \ I" - unfolding i_def by (rule someI_ex) auto - - def A \ "\n::nat. if I = {} then prod_emb I M {} (\\<^sub>E i\{}. {}) else prod_emb I M {i} (\\<^sub>E i\{i}. space (M i))" - then show "range A \ prod_algebra I M" - using prod_algebraI[of "{}" I "\i. space (M i)" M] by (auto intro!: prod_algebraI i) - - have A_eq: "\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 "(\i. A i) = (\\<^sub>E i\I. space (M i))" - unfolding A_eq by (auto simp: space_PiM) - show "\i. emeasure (PiM I M) (A i) \ \" - unfolding A_eq P.emeasure_space_1 by simp -next - fix X assume X: "X \ 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 \ I" "\j. j \ J \ E j \ sets (M j)" - by (force elim!: prod_algebraE) - from eq[OF J] have "emeasure M' X = (\j\J. emeasure (M j) (E j))" - by (simp add: X) - also have "\ = 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 \ I \ AE x in M i. P x \ AE x in PiM I M. P (x i)" apply (rule AE_distrD[of "\\. \ i" "PiM I M" "M i" P])