src/HOL/Probability/Measure_Space.thy
 changeset 57025 e7fd64f82876 parent 56994 8d5e5ec1cac3 child 57137 f174712d0a84
```     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue May 20 16:52:59 2014 +0200
1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue May 20 19:24:39 2014 +0200
1.3 @@ -1632,15 +1632,24 @@
1.4  lemma AE_count_space: "(AE x in count_space A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P x)"
1.5    unfolding eventually_ae_filter by (auto simp add: null_sets_count_space)
1.6
1.7 -lemma sigma_finite_measure_count_space:
1.8 -  fixes A :: "'a::countable set"
1.9 +lemma sigma_finite_measure_count_space_countable:
1.10 +  assumes A: "countable A"
1.11    shows "sigma_finite_measure (count_space A)"
1.12  proof
1.13    show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (count_space A) \<and> (\<Union>i. F i) = space (count_space A) \<and>
1.14       (\<forall>i. emeasure (count_space A) (F i) \<noteq> \<infinity>)"
1.15 -     using surj_from_nat by (intro exI[of _ "\<lambda>i. {from_nat i} \<inter> A"]) (auto simp del: surj_from_nat)
1.16 +     using A
1.17 +     apply (intro exI[of _ "\<lambda>i. {from_nat_into A i} \<inter> A"])
1.18 +     apply auto
1.19 +     apply (rule_tac x="to_nat_on A x" in exI)
1.20 +     apply simp
1.21 +     done
1.22  qed
1.23
1.24 +lemma sigma_finite_measure_count_space:
1.25 +  fixes A :: "'a::countable set" shows "sigma_finite_measure (count_space A)"
1.26 +  by (rule sigma_finite_measure_count_space_countable) auto
1.27 +
1.28  lemma finite_measure_count_space:
1.29    assumes [simp]: "finite A"
1.30    shows "finite_measure (count_space A)"
1.31 @@ -1656,28 +1665,26 @@
1.32  subsection {* Measure restricted to space *}
1.33
1.34  lemma emeasure_restrict_space:
1.35 -  assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
1.36 +  assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
1.37    shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
1.38  proof cases
1.39    assume "A \<in> sets M"
1.40 -
1.41 -  have "emeasure (restrict_space M \<Omega>) A = emeasure M (A \<inter> \<Omega>)"
1.42 +  show ?thesis
1.43    proof (rule emeasure_measure_of[OF restrict_space_def])
1.44 -    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow \<Omega>" "A \<in> sets (restrict_space M \<Omega>)"
1.45 -      using assms `A \<in> sets M` by (auto simp: sets_restrict_space sets.sets_into_space)
1.46 -    show "positive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
1.47 +    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
1.48 +      using `A \<subseteq> \<Omega>` `A \<in> sets M` sets.space_closed by (auto simp: sets_restrict_space)
1.49 +    show "positive (sets (restrict_space M \<Omega>)) (emeasure M)"
1.50        by (auto simp: positive_def emeasure_nonneg)
1.51 -    show "countably_additive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
1.52 +    show "countably_additive (sets (restrict_space M \<Omega>)) (emeasure M)"
1.54        fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> sets (restrict_space M \<Omega>)" "disjoint_family A"
1.55        with assms have "\<And>i. A i \<in> sets M" "\<And>i. A i \<subseteq> space M" "disjoint_family A"
1.56 -        by (auto simp: sets_restrict_space_iff subset_eq dest: sets.sets_into_space)
1.57 -      with `\<Omega> \<in> sets M` show "(\<Sum>i. emeasure M (A i \<inter> \<Omega>)) = emeasure M ((\<Union>i. A i) \<inter> \<Omega>)"
1.58 +        by (fastforce simp: sets_restrict_space_iff[OF assms(1)] image_subset_iff
1.59 +                      dest: sets.sets_into_space)+
1.60 +      then show "(\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)"
1.61          by (subst suminf_emeasure) (auto simp: disjoint_family_subset)
1.62      qed
1.63    qed
1.64 -  with `A \<subseteq> \<Omega>` show ?thesis
1.65 -    by (simp add: Int_absorb2)
1.66  next
1.67    assume "A \<notin> sets M"
1.68    moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
1.69 @@ -1686,15 +1693,28 @@
1.71  qed
1.72
1.73 -lemma restrict_count_space:
1.74 -  assumes "A \<subseteq> B" shows "restrict_space (count_space B) A = count_space A"
1.75 +lemma restrict_restrict_space:
1.76 +  assumes "A \<inter> space M \<in> sets M" "B \<inter> space M \<in> sets M"
1.77 +  shows "restrict_space (restrict_space M A) B = restrict_space M (A \<inter> B)" (is "?l = ?r")
1.78 +proof (rule measure_eqI[symmetric])
1.79 +  show "sets ?r = sets ?l"
1.80 +    unfolding sets_restrict_space image_comp by (intro image_cong) auto
1.81 +next
1.82 +  fix X assume "X \<in> sets (restrict_space M (A \<inter> B))"
1.83 +  then obtain Y where "Y \<in> sets M" "X = Y \<inter> A \<inter> B"
1.84 +    by (auto simp: sets_restrict_space)
1.85 +  with assms sets.Int[OF assms] show "emeasure ?r X = emeasure ?l X"
1.86 +    by (subst (1 2) emeasure_restrict_space)
1.87 +       (auto simp: space_restrict_space sets_restrict_space_iff emeasure_restrict_space ac_simps)
1.88 +qed
1.89 +
1.90 +lemma restrict_count_space: "restrict_space (count_space B) A = count_space (A \<inter> B)"
1.91  proof (rule measure_eqI)
1.92 -  show "sets (restrict_space (count_space B) A) = sets (count_space A)"
1.93 -    using `A \<subseteq> B` by (subst sets_restrict_space) auto
1.94 +  show "sets (restrict_space (count_space B) A) = sets (count_space (A \<inter> B))"
1.95 +    by (subst sets_restrict_space) auto
1.96    moreover fix X assume "X \<in> sets (restrict_space (count_space B) A)"
1.97 -  moreover note `A \<subseteq> B`
1.98 -  ultimately have "X \<subseteq> A" by auto
1.99 -  with `A \<subseteq> B` show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space A) X"
1.100 +  ultimately have "X \<subseteq> A \<inter> B" by auto
1.101 +  then show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space (A \<inter> B)) X"
1.102      by (cases "finite X") (auto simp add: emeasure_restrict_space)
1.103  qed
1.104
```