summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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