src/HOL/Probability/Sigma_Algebra.thy
 changeset 57025 e7fd64f82876 parent 56994 8d5e5ec1cac3 child 57137 f174712d0a84
```     1.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 20 16:52:59 2014 +0200
1.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 20 19:24:39 2014 +0200
1.3 @@ -2299,29 +2299,50 @@
1.4
1.5  subsubsection {* Restricted Space Sigma Algebra *}
1.6
1.7 -definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
1.8 +definition restrict_space where
1.9 +  "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) ((op \<inter> \<Omega>) ` sets M) (emeasure M)"
1.10
1.11 -lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
1.12 -  unfolding restrict_space_def by (subst space_measure_of) auto
1.13 +lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
1.14 +  using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
1.15 +
1.16 +lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
1.17 +  by (simp add: space_restrict_space sets.sets_into_space)
1.18
1.19 -lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
1.20 -  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
1.21 -  unfolding restrict_space_def
1.22 -  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
1.23 +lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
1.24 +proof -
1.25 +  have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) =
1.26 +    (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
1.27 +    using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M]
1.28 +    by (simp add: sets.sigma_sets_eq)
1.29 +  moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
1.30 +    using sets.sets_into_space by (intro image_cong) auto
1.31 +  ultimately show ?thesis
1.32 +    using sets.sets_into_space[of _ M] unfolding restrict_space_def
1.33 +    by (subst sets_measure_of) fastforce+
1.34 +qed
1.35
1.36  lemma sets_restrict_space_iff:
1.37 -  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
1.38 -  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
1.39 +  "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
1.40 +proof (subst sets_restrict_space, safe)
1.41 +  fix A assume "\<Omega> \<inter> space M \<in> sets M" and A: "A \<in> sets M"
1.42 +  then have "(\<Omega> \<inter> space M) \<inter> A \<in> sets M"
1.43 +    by rule
1.44 +  also have "(\<Omega> \<inter> space M) \<inter> A = \<Omega> \<inter> A"
1.45 +    using sets.sets_into_space[OF A] by auto
1.46 +  finally show "\<Omega> \<inter> A \<in> sets M"
1.47 +    by auto
1.48 +qed auto
1.49
1.50  lemma measurable_restrict_space1:
1.51 -  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
1.52 +  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M" and f: "f \<in> measurable M N"
1.53 +  shows "f \<in> measurable (restrict_space M \<Omega>) N"
1.54    unfolding measurable_def
1.55  proof (intro CollectI conjI ballI)
1.56    show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
1.57      using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
1.58
1.59    fix A assume "A \<in> sets N"
1.60 -  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
1.61 +  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> (\<Omega> \<inter> space M)"
1.62      using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
1.63    also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
1.64      unfolding sets_restrict_space_iff[OF \<Omega>]
1.65 @@ -2330,7 +2351,9 @@
1.66  qed
1.67
1.68  lemma measurable_restrict_space2:
1.69 -  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)"
1.70 +  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow>
1.71 +    f \<in> measurable M (restrict_space N \<Omega>)"
1.72    by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
1.73
1.74  end
1.75 +
```