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 +