--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Apr 06 10:58:18 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Apr 06 13:08:44 2011 +0200
@@ -319,7 +319,7 @@
translations
"PIP x:I. M" == "CONST Pi\<^isub>P I (%x. M)"
-sublocale product_prob_space \<subseteq> G: algebra generator
+sublocale product_prob_space \<subseteq> G!: algebra generator
proof
let ?G = generator
show "sets ?G \<subseteq> Pow (space ?G)"
@@ -738,19 +738,19 @@
done
qed
-sublocale product_prob_space \<subseteq> measure_space "Pi\<^isub>P I M"
+sublocale product_prob_space \<subseteq> P: measure_space "Pi\<^isub>P I M"
using infprod_spec by auto
lemma (in product_prob_space) measure_infprod_emb:
assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> 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 "\<mu> (emb I J X) = measure (Pi\<^isub>M J M) X"
proof -
have "emb I J X \<in> sets generator"
using assms by (rule generatorI')
with \<mu>G_eq[OF assms] infprod_spec show ?thesis by auto
qed
-sublocale product_prob_space \<subseteq> prob_space "Pi\<^isub>P I M"
+sublocale product_prob_space \<subseteq> P: prob_space "Pi\<^isub>P I M"
proof
obtain i where "i \<in> I" using I_not_empty by auto
interpret i: finite_product_sigma_finite M "{i}" by default auto
@@ -758,11 +758,11 @@
have "?X \<in> sets (Pi\<^isub>M {i} M)"
by auto
from measure_infprod_emb[OF _ _ _ this] `i \<in> I`
- have "measure (Pi\<^isub>P I M) (emb I {i} ?X) = measure (M i) (space (M i))"
+ have "\<mu> (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 \<in> 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 "\<mu> (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 \<subseteq> I" and X: "X \<in> sets (Pi\<^isub>M J M)"
+ shows "emb I J X \<in> sets (\<Pi>\<^isub>P i\<in>I. M i)"
+proof cases
+ assume "J = {}"
+ with X have "emb I J X = space (\<Pi>\<^isub>P i\<in>I. M i) \<or> 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 \<noteq> {}"
+ show ?thesis unfolding infprod_algebra_def
+ by simp (intro in_sigma generatorI' `J \<noteq> {}` J X)
+qed
+
+lemma (in product_prob_space) finite_measure_infprod_emb:
+ assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" "X \<in> sets (Pi\<^isub>M J M)"
+ shows "\<mu>' (emb I J X) = finite_measure.\<mu>' (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 \<in> sets (Pi\<^isub>P I M)" by auto
+ with assms show "\<mu>' (emb I J X) = J.\<mu>' X"
+ unfolding \<mu>'_def J.\<mu>'_def
+ unfolding measure_infprod_emb[OF assms]
+ by auto
+qed
+
+lemma (in finite_product_prob_space) finite_measure_times:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)"
+ shows "\<mu>' (Pi\<^isub>E I A) = (\<Prod>i\<in>I. M.\<mu>' i (A i))"
+ using assms
+ unfolding \<mu>'_def M.\<mu>'_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 \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> X j \<in> sets (M j)"
+ shows "\<mu>' (emb I J (Pi\<^isub>E J X)) = (\<Prod>j\<in>J. M.\<mu>' 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 \<noteq> {}"
+ interpret J: finite_product_prob_space M J by default fact+
+ have "(\<Prod>i\<in>J. M.\<mu>' i (X i)) = J.\<mu>' (Pi\<^isub>E J X)"
+ using J `J \<noteq> {}` by (subst J.finite_measure_times) auto
+ also have "\<dots> = \<mu>' (emb I J (Pi\<^isub>E J X))"
+ using J `J \<noteq> {}` by (intro finite_measure_infprod_emb[symmetric]) auto
+ finally show ?thesis by simp
+qed
+
+lemma sigma_sets_mono: assumes "A \<subseteq> sigma_sets X B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
+proof
+ fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
+ by induct (insert `A \<subseteq> sigma_sets X B`, auto intro: sigma_sets.intros)
+qed
+
+lemma sigma_sets_mono': assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
+proof
+ fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
+ by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros)
+qed
+
+lemma sigma_sets_subseteq: "A \<subseteq> sigma_sets X A"
+ by (auto intro: sigma_sets.Basic)
+
+lemma (in product_prob_space) infprod_algebra_alt:
+ "Pi\<^isub>P I M = sigma \<lparr> space = space (Pi\<^isub>P I M),
+ sets = (\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i))),
+ measure = measure (Pi\<^isub>P I M) \<rparr>"
+ (is "_ = sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>")
+proof (rule measure_space.equality)
+ let ?G = "\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> 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 \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}"
+ have "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> emb I J ` sets (Pi\<^isub>M J M)" by auto
+ also have "\<dots> \<subseteq> ?G" using J by (rule UN_upper)
+ also have "\<dots> \<subseteq> sigma_sets ?O ?G" by (rule sigma_sets_subseteq)
+ finally show "emb I J ` Pi\<^isub>E J ` (\<Pi> i\<in>J. sets (M i)) \<subseteq> 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 ` (\<Pi> i \<in> J. sets (M i)))"
+ by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
+ also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
+ using J M.sets_into_space
+ by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
+ also have "\<dots> \<subseteq> 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) \<subseteq> sigma_sets ?O ?M"
+ by (simp add: infprod_algebra_def generator_def)
+ qed
+ then show "sets (Pi\<^isub>P I M) = sets (sigma \<lparr> space = ?O, sets = ?M, measure = ?m \<rparr>)"
+ 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 \<lparr> space = space (Pi\<^isub>P I M),
+ sets = (\<Union>i\<in>I. (\<lambda>A. (\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>P I M)) ` sets (M i)),
+ measure = measure (Pi\<^isub>P I M) \<rparr>"
+ (is "_ = ?S")
+proof (rule measure_space.equality)
+ let "sigma \<lparr> space = ?O, sets = ?A, \<dots> = _ \<rparr>" = ?S
+ let ?G = "(\<Union>J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> 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 "\<dots> = 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 \<in> ?G"
+ then obtain J B where "finite J" "J \<noteq> {}" "J \<subseteq> I" "A = emb I J (Pi\<^isub>E J B)"
+ and B: "\<And>i. i \<in> J \<Longrightarrow> B i \<in> sets (M i)"
+ by auto
+ then have A: "A = (\<Inter>j\<in>J. (\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M))"
+ by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
+ { fix j assume "j\<in>J"
+ with `J \<subseteq> I` have "j \<in> I" by auto
+ with `j \<in> J` B have "(\<lambda>x. x j) -` (B j) \<inter> space (Pi\<^isub>P I M) \<in> sets ?S"
+ by (auto simp: sets_sigma intro: sigma_sets.Basic) }
+ with `finite J` `J \<noteq> {}` have "A \<in> sets ?S"
+ unfolding A by (intro A.finite_INT) auto
+ then show "A \<in> sigma_sets ?O ?A" by (simp add: sets_sigma)
+ next
+ fix A assume "A \<in> ?A"
+ then obtain i B where i: "i \<in> I" "B \<in> sets (M i)"
+ and "A = (\<lambda>x. x i) -` B \<inter> space (Pi\<^isub>P I M)"
+ by auto
+ then have "A = emb I {i} (Pi\<^isub>E {i} (\<lambda>_. B))"
+ by (auto simp: emb_def infprod_algebra_def generator_def Pi_iff)
+ with i show "A \<in> 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: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> measurable N (M i)"
+ assumes ext: "\<And>x. x \<in> space N \<Longrightarrow> f x \<in> extensional I"
+ shows "f \<in> measurable N (Pi\<^isub>P I M)"
+proof -
+ interpret N: sigma_algebra N by fact
+ have f_in: "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f x i) \<in> space N \<rightarrow> space (M i)"
+ using f by (auto simp: measurable_def)
+ { fix i A assume i: "i \<in> I" "A \<in> sets (M i)"
+ then have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N = (\<lambda>x. f x i) -` A \<inter> space N"
+ using f_in ext by (auto simp: infprod_algebra_def generator_def)
+ also have "\<dots> \<in> sets N"
+ by (rule measurable_sets f i)+
+ finally have "f -` (\<lambda>x. x i) -` A \<inter> f -` space infprod_algebra \<inter> space N \<in> 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 \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
+ shows "Pi UNIV E \<in> sets (Pi\<^isub>P UNIV M)"
+proof -
+ have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^isub>E j\<in>{..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 \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
+ shows "(\<lambda>n. \<Prod>i\<le>n. M.\<mu>' i (E i)) ----> \<mu>' (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 "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = n.\<mu>' (Pi\<^isub>E {.. n} E)"
+ using E by (subst n.finite_measure_times) auto
+ also have "\<dots> = \<mu>' (?E n)"
+ using E by (intro finite_measure_infprod_emb[symmetric]) auto
+ finally have "(\<Prod>i\<le>n. M.\<mu>' i (E i)) = \<mu>' (?E n)" . }
+ moreover have "Pi UNIV E = (\<Inter>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 \<subseteq> 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
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Apr 06 10:58:18 2011 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Apr 06 13:08:44 2011 +0200
@@ -95,11 +95,11 @@
lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
by auto
-definition extensional :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
- "extensional d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
+definition extensionalD :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+ "extensionalD d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
-lemma extensional_empty[simp]: "extensional d {} = {\<lambda>x. d}"
- unfolding extensional_def by (simp add: set_eq_iff fun_eq_iff)
+lemma extensionalD_empty[simp]: "extensionalD d {} = {\<lambda>x. d}"
+ unfolding extensionalD_def by (simp add: set_eq_iff fun_eq_iff)
lemma funset_eq_UN_fun_upd_I:
assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
@@ -121,16 +121,16 @@
from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
qed
-lemma extensional_insert[simp]:
+lemma extensionalD_insert[simp]:
assumes "a \<notin> A"
- shows "extensional d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
+ shows "extensionalD d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensionalD d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
apply (rule funset_eq_UN_fun_upd_I)
using assms
- by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
+ by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensionalD_def)
-lemma finite_extensional_funcset[simp, intro]:
+lemma finite_extensionalD_funcset[simp, intro]:
assumes "finite A" "finite B"
- shows "finite (extensional d A \<inter> (A \<rightarrow> B))"
+ shows "finite (extensionalD d A \<inter> (A \<rightarrow> B))"
using assms by induct auto
lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)"
@@ -138,27 +138,27 @@
lemma card_funcset:
assumes "finite A" "finite B"
- shows "card (extensional d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
+ shows "card (extensionalD d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
using `finite A` proof induct
- case (insert a A) thus ?case unfolding extensional_insert[OF `a \<notin> A`]
+ case (insert a A) thus ?case unfolding extensionalD_insert[OF `a \<notin> A`]
proof (subst card_UN_disjoint, safe, simp_all)
- show "finite (extensional d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
+ show "finite (extensionalD d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
using `finite B` `finite A` by simp_all
next
fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and
- ext: "f \<in> extensional d A" "g \<in> extensional d A"
+ ext: "f \<in> extensionalD d A" "g \<in> extensionalD d A"
have "f a = d" "g a = d"
- using ext `a \<notin> A` by (auto simp add: extensional_def)
+ using ext `a \<notin> A` by (auto simp add: extensionalD_def)
with `f \<noteq> g` eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
by (auto simp: fun_upd_idem fun_upd_eq_iff)
next
- { fix f assume "f \<in> extensional d A \<inter> (A \<rightarrow> B)"
+ { fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)"
have "card (fun_upd f a ` B) = card B"
proof (auto intro!: card_image inj_onI)
fix b b' assume "f(a := b) = f(a := b')"
from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
qed }
- then show "(\<Sum>i\<in>extensional d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
+ then show "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
using insert by simp
qed
qed simp
@@ -301,11 +301,11 @@
lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
proof -
- have "(t\<circ>OB)`msgs \<subseteq> extensional 0 observations \<inter> (observations \<rightarrow> {.. n})"
- unfolding observations_def extensional_def OB_def msgs_def
+ have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})"
+ unfolding observations_def extensionalD_def OB_def msgs_def
by (auto simp add: t_def comp_def image_iff)
- with finite_extensional_funcset
- have "card ((t\<circ>OB)`msgs) \<le> card (extensional 0 observations \<inter> (observations \<rightarrow> {.. n}))"
+ with finite_extensionalD_funcset
+ have "card ((t\<circ>OB)`msgs) \<le> card (extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n}))"
by (rule card_mono) auto
also have "\<dots> = (n + 1) ^ card observations"
by (subst card_funcset) auto