# HG changeset patch # User hoelzl # Date 1305627888 -7200 # Node ID 36353d913424e4da066d666ed149d7e5730c76a3 # Parent 403e1cba11232fb8413ea826fe0d40840b0d274d add some lemmas for infinite product measure diff -r 403e1cba1123 -r 36353d913424 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue May 17 12:22:58 2011 +0200 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue May 17 12:24:48 2011 +0200 @@ -941,6 +941,57 @@ (auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def) qed +lemma (in product_prob_space) measurable_singleton_infprod: + assumes "i \ I" + shows "(\x. x i) \ measurable (Pi\<^isub>P I M) (M i)" +proof (unfold measurable_def, intro CollectI conjI ballI) + show "(\x. x i) \ space (Pi\<^isub>P I M) \ space (M i)" + using M.sets_into_space `i \ I` + by (auto simp: infprod_algebra_def generator_def) + fix A assume "A \ sets (M i)" + have "(\x. x i) -` A \ space (Pi\<^isub>P I M) = emb I {i} (\\<^isub>E _\{i}. A)" + by (auto simp: infprod_algebra_def generator_def emb_def) + also have "\ \ sets (Pi\<^isub>P I M)" + using `i \ I` `A \ sets (M i)` + by (intro emb_in_infprod_algebra product_algebraI) auto + finally show "(\x. x i) -` A \ space (Pi\<^isub>P I M) \ sets (Pi\<^isub>P I M)" . +qed + +lemma (in product_prob_space) sigma_product_algebra_sigma_eq: + assumes M: "\i. i \ I \ M i = sigma (E i)" + shows "sets (Pi\<^isub>P I M) = sigma_sets (space (Pi\<^isub>P I M)) (\i\I. (\A. (\x. x i) -` A \ space (Pi\<^isub>P I M)) ` sets (E i))" +proof - + let ?E = "(\i\I. (\A. (\x. x i) -` A \ space (Pi\<^isub>P I M)) ` sets (E i))" + let ?M = "(\i\I. (\A. (\x. x i) -` A \ space (Pi\<^isub>P I M)) ` sets (M i))" + { fix i A assume "i\I" "A \ sets (E i)" + then have "A \ sets (M i)" using M by auto + then have "A \ Pow (space (M i))" using M.sets_into_space by auto + then have "A \ Pow (space (E i))" using M[OF `i \ I`] by auto } + moreover + have "\i. i \ I \ (\x. x i) \ space infprod_algebra \ space (E i)" + by (auto simp: M infprod_algebra_def generator_def Pi_iff) + ultimately have "sigma_sets (space (Pi\<^isub>P I M)) ?M \ sigma_sets (space (Pi\<^isub>P I M)) ?E" + apply (intro sigma_sets_mono UN_least) + apply (simp add: sets_sigma M) + apply (subst sigma_sets_vimage[symmetric]) + apply (auto intro!: sigma_sets_mono') + done + moreover have "sigma_sets (space (Pi\<^isub>P I M)) ?E \ sigma_sets (space (Pi\<^isub>P I M)) ?M" + by (intro sigma_sets_mono') (auto simp: M) + ultimately show ?thesis + by (subst infprod_algebra_alt2) (auto simp: sets_sigma) +qed + +lemma (in product_prob_space) Int_proj_eq_emb: + assumes "J \ {}" "J \ I" + shows "(\i\J. (\x. x i) -` A i \ space (Pi\<^isub>P I M)) = emb I J (Pi\<^isub>E J A)" + using assms by (auto simp: infprod_algebra_def generator_def emb_def Pi_iff) + +lemma (in product_prob_space) emb_insert: + "i \ J \ emb I J (Pi\<^isub>E J f) \ ((\x. x i) -` A \ space (Pi\<^isub>P I M)) = + emb I (insert i J) (Pi\<^isub>E (insert i J) (f(i := A)))" + by (auto simp: emb_def Pi_iff infprod_algebra_def generator_def split: split_if_asm) + subsection {* Sequence space *} locale sequence_space = product_prob_space M "UNIV :: nat set" for M