--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Oct 06 16:27:07 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Oct 06 16:27:31 2014 +0200
@@ -2214,122 +2214,101 @@
using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j`
by (auto simp: subset_eq)
-subsubsection {* Sigma algebra generated by function preimages *}
+subsubsection {* Supremum of a set of \sigma-algebras *}
+
+definition "Sup_sigma M = sigma (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
+
+syntax
+ "_SUP_sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>\<^sub>\<sigma> _\<in>_./ _)" [0, 0, 10] 10)
-definition
- "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)"
+translations
+ "\<Squnion>\<^sub>\<sigma> x\<in>A. B" == "CONST Sup_sigma ((\<lambda>x. B) ` A)"
+
+lemma space_Sup_sigma: "space (Sup_sigma M) = (\<Union>x\<in>M. space x)"
+ unfolding Sup_sigma_def by (rule space_measure_of) (auto dest: sets.sets_into_space)
+
+lemma sets_Sup_sigma: "sets (Sup_sigma M) = sigma_sets (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
+ unfolding Sup_sigma_def by (rule sets_measure_of) (auto dest: sets.sets_into_space)
+
+lemma in_Sup_sigma: "m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup_sigma M)"
+ unfolding sets_Sup_sigma by auto
-lemma sigma_algebra_preimages:
- fixes f :: "'x \<Rightarrow> 'a"
- assumes "f \<in> S \<rightarrow> space M"
- shows "sigma_algebra S ((\<lambda>A. f -` A \<inter> S) ` sets M)"
- (is "sigma_algebra _ (?F ` sets M)")
-proof (simp add: sigma_algebra_iff2, safe)
- show "{} \<in> ?F ` sets M" by blast
-next
- fix A assume "A \<in> sets M"
- moreover have "S - ?F A = ?F (space M - A)"
+lemma sets_Sup_in_sets:
+ assumes "M \<noteq> {}"
+ assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N"
+ assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
+ shows "sets (Sup_sigma M) \<subseteq> sets N"
+proof -
+ have *: "UNION M space = space N"
using assms by auto
- ultimately show "S - ?F A \<in> ?F ` sets M"
- by blast
-next
- fix A :: "nat \<Rightarrow> 'x set" assume *: "range A \<subseteq> ?F ` M"
- have "\<forall>i. \<exists>b. b \<in> M \<and> A i = ?F b"
- proof safe
- fix i
- have "A i \<in> ?F ` M" using * by auto
- then show "\<exists>b. b \<in> M \<and> A i = ?F b" by auto
- qed
- from choice[OF this] obtain b where b: "range b \<subseteq> M" "\<And>i. A i = ?F (b i)"
- by auto
- then have "(\<Union>i. A i) = ?F (\<Union>i. b i)" by auto
- then show "(\<Union>i. A i) \<in> ?F ` M" using b(1) by blast
+ show ?thesis
+ unfolding sets_Sup_sigma * using assms by (auto intro!: sets.sigma_sets_subset)
+qed
+
+lemma measurable_Sup_sigma1:
+ assumes m: "m \<in> M" and f: "f \<in> measurable m N"
+ and const_space: "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> space m = space n"
+ shows "f \<in> measurable (Sup_sigma M) N"
+proof -
+ have "space (Sup_sigma M) = space m"
+ using m by (auto simp add: space_Sup_sigma dest: const_space)
+ then show ?thesis
+ using m f unfolding measurable_def by (auto intro: in_Sup_sigma)
qed
-lemma sets_vimage_algebra[simp]:
- "f \<in> S \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra M S f) = (\<lambda>A. f -` A \<inter> S) ` sets M"
- using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_preimages, of f S M]
- by (simp add: vimage_algebra_def)
+lemma measurable_Sup_sigma2:
+ assumes M: "M \<noteq> {}"
+ assumes f: "\<And>m. m \<in> M \<Longrightarrow> f \<in> measurable N m"
+ shows "f \<in> measurable N (Sup_sigma M)"
+ unfolding Sup_sigma_def
+proof (rule measurable_measure_of)
+ show "f \<in> space N \<rightarrow> UNION M space"
+ using measurable_space[OF f] M by auto
+qed (auto intro: measurable_sets f dest: sets.sets_into_space)
-lemma space_vimage_algebra[simp]:
- "f \<in> S \<rightarrow> space M \<Longrightarrow> space (vimage_algebra M S f) = S"
- using sigma_algebra.space_measure_of_eq[OF sigma_algebra_preimages, of f S M]
- by (simp add: vimage_algebra_def)
-
-lemma in_vimage_algebra[simp]:
- "f \<in> S \<rightarrow> space M \<Longrightarrow> A \<in> sets (vimage_algebra M S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
- by (simp add: image_iff)
+subsection {* The smallest \sigma-algebra regarding a function *}
-lemma measurable_vimage_algebra:
- fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
- shows "f \<in> measurable (vimage_algebra M S f) M"
- unfolding measurable_def using assms by force
+definition
+ "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
+
+lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
+ unfolding vimage_algebra_def by (rule space_measure_of) auto
-lemma measurable_vimage:
- fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
- assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
- shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra M S f) M2"
-proof -
- note measurable_vimage_algebra[OF assms(2)]
- from measurable_comp[OF this assms(1)]
- show ?thesis by (simp add: comp_def)
-qed
+lemma sets_vimage_algebra: "sets (vimage_algebra X f M) = sigma_sets X {f -` A \<inter> X | A. A \<in> sets M}"
+ unfolding vimage_algebra_def by (rule sets_measure_of) auto
+
+lemma sets_vimage_algebra2:
+ "f \<in> X \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra X f M) = {f -` A \<inter> X | A. A \<in> sets M}"
+ using sigma_sets_vimage_commute[of f X "space M" "sets M"]
+ unfolding sets_vimage_algebra sets.sigma_sets_eq by simp
-lemma sigma_sets_vimage:
- assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
- shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
-proof (intro set_eqI iffI)
- let ?F = "\<lambda>X. f -` X \<inter> S'"
- fix X assume "X \<in> sigma_sets S' (?F ` A)"
- then show "X \<in> ?F ` sigma_sets S A"
- proof induct
- case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
- by auto
- then show ?case by auto
- next
- case Empty then show ?case
- by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
- next
- case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
- by auto
- then have "S - X' \<in> sigma_sets S A"
- by (auto intro!: sigma_sets.Compl)
- then show ?case
- using X assms by (auto intro!: image_eqI[where x="S - X'"])
- next
- case (Union F)
- then have "\<forall>i. \<exists>F'. F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
- by (auto simp: image_iff Bex_def)
- from choice[OF this] obtain F' where
- "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
- by auto
- then show ?case
- by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
- qed
-next
- let ?F = "\<lambda>X. f -` X \<inter> S'"
- fix X assume "X \<in> ?F ` sigma_sets S A"
- then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
- then show "X \<in> sigma_sets S' (?F ` A)"
- proof (induct arbitrary: X)
- case Empty then show ?case by (auto intro: sigma_sets.Empty)
- next
- case (Compl X')
- have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
- apply (rule sigma_sets.Compl)
- using assms by (auto intro!: Compl.hyps simp: Compl.prems)
- also have "S' - (S' - X) = X"
- using assms Compl by auto
- finally show ?case .
- next
- case (Union F)
- have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
- by (intro sigma_sets.Union Union.hyps) simp
- also have "(\<Union>i. f -` F i \<inter> S') = X"
- using assms Union by auto
- finally show ?case .
- qed auto
-qed
+lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)"
+ by (auto simp: vimage_algebra_def)
+
+lemma sets_image_in_sets:
+ assumes N: "space N = X"
+ assumes f: "f \<in> measurable N M"
+ shows "sets (vimage_algebra X f M) \<subseteq> sets N"
+ unfolding sets_vimage_algebra N[symmetric]
+ by (rule sets.sigma_sets_subset) (auto intro!: measurable_sets f)
+
+lemma measurable_vimage_algebra1: "f \<in> X \<rightarrow> space M \<Longrightarrow> f \<in> measurable (vimage_algebra X f M) M"
+ unfolding measurable_def by (auto intro: in_vimage_algebra)
+
+lemma measurable_vimage_algebra2:
+ assumes g: "g \<in> space N \<rightarrow> X" and f: "(\<lambda>x. f (g x)) \<in> measurable N M"
+ shows "g \<in> measurable N (vimage_algebra X f M)"
+ unfolding vimage_algebra_def
+proof (rule measurable_measure_of)
+ fix A assume "A \<in> {f -` A \<inter> X | A. A \<in> sets M}"
+ then obtain Y where Y: "Y \<in> sets M" and A: "A = f -` Y \<inter> X"
+ by auto
+ then have "g -` A \<inter> space N = (\<lambda>x. f (g x)) -` Y \<inter> space N"
+ using g by auto
+ also have "\<dots> \<in> sets N"
+ using f Y by (rule measurable_sets)
+ finally show "g -` A \<inter> space N \<in> sets N" .
+qed (insert g, auto)
subsubsection {* Restricted Space Sigma Algebra *}
@@ -2343,16 +2322,20 @@
by (simp add: space_restrict_space sets.sets_into_space)
lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
-proof -
- have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) =
+ unfolding restrict_space_def
+proof (subst sets_measure_of)
+ show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)"
+ by (auto dest: sets.sets_into_space)
+ have "sigma_sets (\<Omega> \<inter> space M) {((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} =
(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
- using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M]
- by (simp add: sets.sigma_sets_eq)
- moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
- using sets.sets_into_space by (intro image_cong) auto
- ultimately show ?thesis
- using sets.sets_into_space[of _ M] unfolding restrict_space_def
- by (subst sets_measure_of) fastforce+
+ by (subst sigma_sets_vimage_commute[symmetric, where \<Omega>' = "space M"])
+ (auto simp add: sets.sigma_sets_eq)
+ moreover have "{((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
+ by auto
+ moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
+ by (intro image_cong) (auto dest: sets.sets_into_space)
+ ultimately show "sigma_sets (\<Omega> \<inter> space M) (op \<inter> \<Omega> ` sets M) = op \<inter> \<Omega> ` sets M"
+ by simp
qed
lemma sets_restrict_space_iff: