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

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