# 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