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.53      proof (rule countably_additiveI)
    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.70      by (simp add: emeasure_notin_sets)
    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