src/HOL/Probability/Measure_Space.thy
changeset 54417 dbb8ecfe1337
parent 53374 a14d2a854c02
child 56154 f0a927235162
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Nov 12 19:28:55 2013 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Nov 12 19:28:56 2013 +0100
     1.3 @@ -1118,6 +1118,10 @@
     1.4      and measurable_distr_eq2[simp]: "measurable Mg' (distr Mg Ng g) = measurable Mg' Ng"
     1.5    by (auto simp: measurable_def)
     1.6  
     1.7 +lemma distr_cong:
     1.8 +  "M = K \<Longrightarrow> sets N = sets L \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> distr M N f = distr K L g"
     1.9 +  using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong)
    1.10 +
    1.11  lemma emeasure_distr:
    1.12    fixes f :: "'a \<Rightarrow> 'b"
    1.13    assumes f: "f \<in> measurable M N" and A: "A \<in> sets N"
    1.14 @@ -1649,5 +1653,50 @@
    1.15    show "sigma_finite_measure (count_space A)" ..
    1.16  qed
    1.17  
    1.18 +section {* Measure restricted to space *}
    1.19 +
    1.20 +lemma emeasure_restrict_space:
    1.21 +  assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
    1.22 +  shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
    1.23 +proof cases
    1.24 +  assume "A \<in> sets M"
    1.25 +  
    1.26 +  have "emeasure (restrict_space M \<Omega>) A = emeasure M (A \<inter> \<Omega>)"
    1.27 +  proof (rule emeasure_measure_of[OF restrict_space_def])
    1.28 +    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow \<Omega>" "A \<in> sets (restrict_space M \<Omega>)"
    1.29 +      using assms `A \<in> sets M` by (auto simp: sets_restrict_space sets.sets_into_space)
    1.30 +    show "positive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
    1.31 +      by (auto simp: positive_def emeasure_nonneg)
    1.32 +    show "countably_additive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
    1.33 +    proof (rule countably_additiveI)
    1.34 +      fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> sets (restrict_space M \<Omega>)" "disjoint_family A"
    1.35 +      with assms have "\<And>i. A i \<in> sets M" "\<And>i. A i \<subseteq> space M" "disjoint_family A"
    1.36 +        by (auto simp: sets_restrict_space_iff subset_eq dest: sets.sets_into_space)
    1.37 +      with `\<Omega> \<in> sets M` show "(\<Sum>i. emeasure M (A i \<inter> \<Omega>)) = emeasure M ((\<Union>i. A i) \<inter> \<Omega>)"
    1.38 +        by (subst suminf_emeasure) (auto simp: disjoint_family_subset)
    1.39 +    qed
    1.40 +  qed
    1.41 +  with `A \<subseteq> \<Omega>` show ?thesis
    1.42 +    by (simp add: Int_absorb2)
    1.43 +next
    1.44 +  assume "A \<notin> sets M"
    1.45 +  moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
    1.46 +    by (simp add: sets_restrict_space_iff)
    1.47 +  ultimately show ?thesis
    1.48 +    by (simp add: emeasure_notin_sets)
    1.49 +qed
    1.50 +
    1.51 +lemma restrict_count_space:
    1.52 +  assumes "A \<subseteq> B" shows "restrict_space (count_space B) A = count_space A"
    1.53 +proof (rule measure_eqI)
    1.54 +  show "sets (restrict_space (count_space B) A) = sets (count_space A)"
    1.55 +    using `A \<subseteq> B` by (subst sets_restrict_space) auto
    1.56 +  moreover fix X assume "X \<in> sets (restrict_space (count_space B) A)"
    1.57 +  moreover note `A \<subseteq> B`
    1.58 +  ultimately have "X \<subseteq> A" by auto
    1.59 +  with `A \<subseteq> B` show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space A) X"
    1.60 +    by (cases "finite X") (auto simp add: emeasure_restrict_space)
    1.61 +qed
    1.62 +
    1.63  end
    1.64