# HG changeset patch # User hoelzl # Date 1302026104 -7200 # Node ID 08d717c828282fd4113ab264e0964cba2699323a # Parent 461624ffd382a905f4c7f4af0a9c3ab1dd1bd47a prove measurable_into_infprod_algebra and measure_infprod diff -r 461624ffd382 -r 08d717c82828 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Apr 05 17:10:51 2011 +0200 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Apr 05 19:55:04 2011 +0200 @@ -319,7 +319,7 @@ translations "PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)" -sublocale product_prob_space \ G: algebra generator +sublocale product_prob_space \ G!: algebra generator proof let ?G = generator show "sets ?G \ Pow (space ?G)" @@ -738,19 +738,19 @@ done qed -sublocale product_prob_space \ measure_space "Pi\<^isub>P I M" +sublocale product_prob_space \ P: measure_space "Pi\<^isub>P I M" using infprod_spec by auto lemma (in product_prob_space) measure_infprod_emb: assumes "J \ {}" "finite J" "J \ I" "X \ sets (Pi\<^isub>M J M)" - shows "measure (Pi\<^isub>P I M) (emb I J X) = measure (Pi\<^isub>M J M) X" + shows "\ (emb I J X) = measure (Pi\<^isub>M J M) X" proof - have "emb I J X \ sets generator" using assms by (rule generatorI') with \G_eq[OF assms] infprod_spec show ?thesis by auto qed -sublocale product_prob_space \ prob_space "Pi\<^isub>P I M" +sublocale product_prob_space \ P: prob_space "Pi\<^isub>P I M" proof obtain i where "i \ I" using I_not_empty by auto interpret i: finite_product_sigma_finite M "{i}" by default auto @@ -758,11 +758,11 @@ have "?X \ sets (Pi\<^isub>M {i} M)" by auto from measure_infprod_emb[OF _ _ _ this] `i \ I` - have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))" + have "\ (emb I {i} ?X) = measure (M i) (space (M i))" by (simp add: i.measure_times) also have "emb I {i} ?X = space (Pi\<^isub>P I M)" using `i \ I` by (auto simp: emb_def infprod_algebra_def generator_def) - finally show "measure (Pi\<^isub>P I M) (space (Pi\<^isub>P I M)) = 1" + finally show "\ (space (Pi\<^isub>P I M)) = 1" using M.measure_space_1 by simp qed @@ -784,4 +784,199 @@ unfolding infprod_algebra_def by auto qed +lemma (in product_prob_space) emb_in_infprod_algebra[intro]: + fixes J assumes J: "finite J" "J \ I" and X: "X \ sets (Pi\<^isub>M J M)" + shows "emb I J X \ sets (\\<^isub>P i\I. M i)" +proof cases + assume "J = {}" + with X have "emb I J X = space (\\<^isub>P i\I. M i) \ emb I J X = {}" + by (auto simp: emb_def infprod_algebra_def generator_def + product_algebra_def product_algebra_generator_def image_constant sigma_def) + then show ?thesis by auto +next + assume "J \ {}" + show ?thesis unfolding infprod_algebra_def + by simp (intro in_sigma generatorI' `J \ {}` J X) +qed + +lemma (in product_prob_space) finite_measure_infprod_emb: + assumes "J \ {}" "finite J" "J \ I" "X \ sets (Pi\<^isub>M J M)" + shows "\' (emb I J X) = finite_measure.\' (Pi\<^isub>M J M) X" +proof - + interpret J: finite_product_prob_space M J by default fact+ + from assms have "emb I J X \ sets (Pi\<^isub>P I M)" by auto + with assms show "\' (emb I J X) = J.\' X" + unfolding \'_def J.\'_def + unfolding measure_infprod_emb[OF assms] + by auto +qed + +lemma (in finite_product_prob_space) finite_measure_times: + assumes "\i. i \ I \ A i \ sets (M i)" + shows "\' (Pi\<^isub>E I A) = (\i\I. M.\' i (A i))" + using assms + unfolding \'_def M.\'_def + by (subst measure_times[OF assms]) + (auto simp: finite_measure_eq M.finite_measure_eq setprod_extreal) + +lemma (in product_prob_space) finite_measure_infprod_emb_Pi: + assumes J: "finite J" "J \ I" "\j. j \ J \ X j \ sets (M j)" + shows "\' (emb I J (Pi\<^isub>E J X)) = (\j\J. M.\' j (X j))" +proof cases + assume "J = {}" + then have "emb I J (Pi\<^isub>E J X) = space infprod_algebra" + by (auto simp: infprod_algebra_def generator_def sigma_def emb_def) + then show ?thesis using `J = {}` prob_space by simp +next + assume "J \ {}" + interpret J: finite_product_prob_space M J by default fact+ + have "(\i\J. M.\' i (X i)) = J.\' (Pi\<^isub>E J X)" + using J `J \ {}` by (subst J.finite_measure_times) auto + also have "\ = \' (emb I J (Pi\<^isub>E J X))" + using J `J \ {}` by (intro finite_measure_infprod_emb[symmetric]) auto + finally show ?thesis by simp +qed + +lemma sigma_sets_mono: assumes "A \ sigma_sets X B" shows "sigma_sets X A \ sigma_sets X B" +proof + fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B" + by induct (insert `A \ sigma_sets X B`, auto intro: sigma_sets.intros) +qed + +lemma sigma_sets_mono': assumes "A \ B" shows "sigma_sets X A \ sigma_sets X B" +proof + fix x assume "x \ sigma_sets X A" then show "x \ sigma_sets X B" + by induct (insert `A \ B`, auto intro: sigma_sets.intros) +qed + +lemma sigma_sets_subseteq: "A \ sigma_sets X A" + by (auto intro: sigma_sets.Basic) + +lemma (in product_prob_space) infprod_algebra_alt: + "Pi\<^isub>P I M = sigma \ space = space (Pi\<^isub>P I M), + sets = (\J\{J. J \ {} \ finite J \ J \ I}. emb I J ` Pi\<^isub>E J ` (\ i \ J. sets (M i))), + measure = measure (Pi\<^isub>P I M) \" + (is "_ = sigma \ space = ?O, sets = ?M, measure = ?m \") +proof (rule measure_space.equality) + let ?G = "\J\{J. J \ {} \ finite J \ J \ I}. emb I J ` sets (Pi\<^isub>M J M)" + have "sigma_sets ?O ?M = sigma_sets ?O ?G" + proof (intro equalityI sigma_sets_mono UN_least) + fix J assume J: "J \ {J. J \ {} \ finite J \ J \ I}" + have "emb I J ` Pi\<^isub>E J ` (\ i\J. sets (M i)) \ emb I J ` sets (Pi\<^isub>M J M)" by auto + also have "\ \ ?G" using J by (rule UN_upper) + also have "\ \ sigma_sets ?O ?G" by (rule sigma_sets_subseteq) + finally show "emb I J ` Pi\<^isub>E J ` (\ i\J. sets (M i)) \ sigma_sets ?O ?G" . + have "emb I J ` sets (Pi\<^isub>M J M) = emb I J ` sigma_sets (space (Pi\<^isub>M J M)) (Pi\<^isub>E J ` (\ i \ J. sets (M i)))" + by (simp add: sets_sigma product_algebra_generator_def product_algebra_def) + also have "\ = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\ i \ J. sets (M i)))" + using J M.sets_into_space + by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast + also have "\ \ sigma_sets (space (Pi\<^isub>M I M)) ?M" + using J by (intro sigma_sets_mono') auto + finally show "emb I J ` sets (Pi\<^isub>M J M) \ sigma_sets ?O ?M" + by (simp add: infprod_algebra_def generator_def) + qed + then show "sets (Pi\<^isub>P I M) = sets (sigma \ space = ?O, sets = ?M, measure = ?m \)" + by (simp_all add: infprod_algebra_def generator_def sets_sigma) +qed simp_all + +lemma (in product_prob_space) infprod_algebra_alt2: + "Pi\<^isub>P I M = sigma \ space = space (Pi\<^isub>P I M), + sets = (\i\I. (\A. (\x. x i) -` A \ space (Pi\<^isub>P I M)) ` sets (M i)), + measure = measure (Pi\<^isub>P I M) \" + (is "_ = ?S") +proof (rule measure_space.equality) + let "sigma \ space = ?O, sets = ?A, \ = _ \" = ?S + let ?G = "(\J\{J. J \ {} \ finite J \ J \ I}. emb I J ` Pi\<^isub>E J ` (\ i \ J. sets (M i)))" + have "sets (Pi\<^isub>P I M) = sigma_sets ?O ?G" + by (subst infprod_algebra_alt) (simp add: sets_sigma) + also have "\ = sigma_sets ?O ?A" + proof (intro equalityI sigma_sets_mono subsetI) + interpret A: sigma_algebra ?S + by (rule sigma_algebra_sigma) auto + fix A assume "A \ ?G" + then obtain J B where "finite J" "J \ {}" "J \ I" "A = emb I J (Pi\<^isub>E J B)" + and B: "\i. i \ J \ B i \ sets (M i)" + by auto + then have A: "A = (\j\J. (\x. x j) -` (B j) \ space (Pi\<^isub>P I M))" + by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff) + { fix j assume "j\J" + with `J \ I` have "j \ I" by auto + with `j \ J` B have "(\x. x j) -` (B j) \ space (Pi\<^isub>P I M) \ sets ?S" + by (auto simp: sets_sigma intro: sigma_sets.Basic) } + with `finite J` `J \ {}` have "A \ sets ?S" + unfolding A by (intro A.finite_INT) auto + then show "A \ sigma_sets ?O ?A" by (simp add: sets_sigma) + next + fix A assume "A \ ?A" + then obtain i B where i: "i \ I" "B \ sets (M i)" + and "A = (\x. x i) -` B \ space (Pi\<^isub>P I M)" + by auto + then have "A = emb I {i} (Pi\<^isub>E {i} (\_. B))" + by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff) + with i show "A \ sigma_sets ?O ?G" + by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto + qed + finally show "sets (Pi\<^isub>P I M) = sets ?S" + by (simp add: sets_sigma) +qed simp_all + +lemma (in product_prob_space) measurable_into_infprod_algebra: + assumes "sigma_algebra N" + assumes f: "\i. i \ I \ (\x. f x i) \ measurable N (M i)" + assumes ext: "\x. x \ space N \ f x \ extensional I" + shows "f \ measurable N (Pi\<^isub>P I M)" +proof - + interpret N: sigma_algebra N by fact + have f_in: "\i. i \ I \ (\x. f x i) \ space N \ space (M i)" + using f by (auto simp: measurable_def) + { fix i A assume i: "i \ I" "A \ sets (M i)" + then have "f -` (\x. x i) -` A \ f -` space infprod_algebra \ space N = (\x. f x i) -` A \ space N" + using f_in ext by (auto simp: infprod_algebra_def generator_def) + also have "\ \ sets N" + by (rule measurable_sets f i)+ + finally have "f -` (\x. x i) -` A \ f -` space infprod_algebra \ space N \ sets N" . } + with f_in ext show ?thesis + by (subst infprod_algebra_alt2) + (auto intro!: N.measurable_sigma simp: Pi_iff infprod_algebra_def generator_def) +qed + +subsection {* Sequence space *} + +locale sequence_space = product_prob_space M "UNIV :: nat set" for M + +lemma (in sequence_space) infprod_in_sets[intro]: + fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets (M i)" + shows "Pi UNIV E \ sets (Pi\<^isub>P UNIV M)" +proof - + have "Pi UNIV E = (\i. emb UNIV {..i} (\\<^isub>E j\{..i}. E j))" + using E E[THEN M.sets_into_space] + by (auto simp: emb_def Pi_iff extensional_def) blast + with E show ?thesis + by (auto intro: emb_in_infprod_algebra) +qed + +lemma (in sequence_space) measure_infprod: + fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets (M i)" + shows "(\n. \i\n. M.\' i (E i)) ----> \' (Pi UNIV E)" +proof - + let "?E n" = "emb UNIV {..n} (Pi\<^isub>E {.. n} E)" + { fix n :: nat + interpret n: finite_product_prob_space M "{..n}" by default auto + have "(\i\n. M.\' i (E i)) = n.\' (Pi\<^isub>E {.. n} E)" + using E by (subst n.finite_measure_times) auto + also have "\ = \' (?E n)" + using E by (intro finite_measure_infprod_emb[symmetric]) auto + finally have "(\i\n. M.\' i (E i)) = \' (?E n)" . } + moreover have "Pi UNIV E = (\n. ?E n)" + using E E[THEN M.sets_into_space] + by (auto simp: emb_def extensional_def Pi_iff) blast + moreover have "range ?E \ sets (Pi\<^isub>P UNIV M)" + using E by auto + moreover have "decseq ?E" + by (auto simp: emb_def Pi_iff decseq_def) + ultimately show ?thesis + by (simp add: finite_continuity_from_above) +qed + end \ No newline at end of file