summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Tue, 12 Nov 2013 19:28:56 +0100 | |

changeset 54417 | dbb8ecfe1337 |

parent 54416 | 7fb88ed6ff3c |

child 54418 | 3b8e33d1a39a |

add restrict_space measure

--- a/src/HOL/Library/FuncSet.thy Tue Nov 12 19:28:55 2013 +0100 +++ b/src/HOL/Library/FuncSet.thy Tue Nov 12 19:28:56 2013 +0100 @@ -183,18 +183,20 @@ subsection{*Bounded Abstraction: @{term restrict}*} -lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B" +lemma restrict_in_funcset: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> A \<rightarrow> B" by (simp add: Pi_def restrict_def) -lemma restrictI[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B" +lemma restrictI[intro!]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<lambda>x\<in>A. f x) \<in> Pi A B" by (simp add: Pi_def restrict_def) -lemma restrict_apply [simp]: - "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)" +lemma restrict_apply[simp]: "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)" by (simp add: restrict_def) +lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x" + by simp + lemma restrict_ext: - "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)" + "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)" by (simp add: fun_eq_iff Pi_def restrict_def) lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A" @@ -364,6 +366,9 @@ lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}" unfolding PiE_def by simp +lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T" + unfolding PiE_def by simp + lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}" unfolding PiE_def by auto

--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Nov 12 19:28:55 2013 +0100 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Nov 12 19:28:56 2013 +0100 @@ -2521,6 +2521,36 @@ "f \<in> borel_measurable (count_space A)" by simp +section {* Measures with Restricted Space *} + +lemma positive_integral_restrict_space: + assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "\<And>x. x \<in> space M - \<Omega> \<Longrightarrow> f x = 0" + shows "positive_integral (restrict_space M \<Omega>) f = positive_integral M f" +using f proof (induct rule: borel_measurable_induct) + case (cong f g) then show ?case + using positive_integral_cong[of M f g] positive_integral_cong[of "restrict_space M \<Omega>" f g] + sets.sets_into_space[OF `\<Omega> \<in> sets M`] + by (simp add: subset_eq space_restrict_space) +next + case (set A) + then have "A \<subseteq> \<Omega>" + unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space) + with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case + by (subst positive_integral_indicator') + (auto simp add: sets_restrict_space_iff space_restrict_space + emeasure_restrict_space Int_absorb2 + dest: sets.sets_into_space) +next + case (mult f c) then show ?case + by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> positive_integral_cmult) +next + case (add f g) then show ?case + by (simp add: measurable_restrict_space1 \<Omega> positive_integral_add ereal_add_nonneg_eq_0_iff) +next + case (seq F) then show ?case + by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP) +qed + section {* Measure spaces with an associated density *} definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where

--- a/src/HOL/Probability/Measure_Space.thy Tue Nov 12 19:28:55 2013 +0100 +++ b/src/HOL/Probability/Measure_Space.thy Tue Nov 12 19:28:56 2013 +0100 @@ -1118,6 +1118,10 @@ and measurable_distr_eq2[simp]: "measurable Mg' (distr Mg Ng g) = measurable Mg' Ng" by (auto simp: measurable_def) +lemma distr_cong: + "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" + using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong) + lemma emeasure_distr: fixes f :: "'a \<Rightarrow> 'b" assumes f: "f \<in> measurable M N" and A: "A \<in> sets N" @@ -1649,5 +1653,50 @@ show "sigma_finite_measure (count_space A)" .. qed +section {* Measure restricted to space *} + +lemma emeasure_restrict_space: + assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>" + shows "emeasure (restrict_space M \<Omega>) A = emeasure M A" +proof cases + assume "A \<in> sets M" + + have "emeasure (restrict_space M \<Omega>) A = emeasure M (A \<inter> \<Omega>)" + proof (rule emeasure_measure_of[OF restrict_space_def]) + show "op \<inter> \<Omega> ` sets M \<subseteq> Pow \<Omega>" "A \<in> sets (restrict_space M \<Omega>)" + using assms `A \<in> sets M` by (auto simp: sets_restrict_space sets.sets_into_space) + show "positive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))" + by (auto simp: positive_def emeasure_nonneg) + show "countably_additive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))" + proof (rule countably_additiveI) + fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> sets (restrict_space M \<Omega>)" "disjoint_family A" + with assms have "\<And>i. A i \<in> sets M" "\<And>i. A i \<subseteq> space M" "disjoint_family A" + by (auto simp: sets_restrict_space_iff subset_eq dest: sets.sets_into_space) + with `\<Omega> \<in> sets M` show "(\<Sum>i. emeasure M (A i \<inter> \<Omega>)) = emeasure M ((\<Union>i. A i) \<inter> \<Omega>)" + by (subst suminf_emeasure) (auto simp: disjoint_family_subset) + qed + qed + with `A \<subseteq> \<Omega>` show ?thesis + by (simp add: Int_absorb2) +next + assume "A \<notin> sets M" + moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)" + by (simp add: sets_restrict_space_iff) + ultimately show ?thesis + by (simp add: emeasure_notin_sets) +qed + +lemma restrict_count_space: + assumes "A \<subseteq> B" shows "restrict_space (count_space B) A = count_space A" +proof (rule measure_eqI) + show "sets (restrict_space (count_space B) A) = sets (count_space A)" + using `A \<subseteq> B` by (subst sets_restrict_space) auto + moreover fix X assume "X \<in> sets (restrict_space (count_space B) A)" + moreover note `A \<subseteq> B` + ultimately have "X \<subseteq> A" by auto + with `A \<subseteq> B` show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space A) X" + by (cases "finite X") (auto simp add: emeasure_restrict_space) +qed + end

--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 12 19:28:55 2013 +0100 +++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 12 19:28:56 2013 +0100 @@ -1171,16 +1171,13 @@ using assms by(simp_all add: sets_measure_of_conv space_measure_of_conv) -lemma (in sigma_algebra) sets_measure_of_eq[simp]: - "sets (measure_of \<Omega> M \<mu>) = M" +lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \<Omega> M \<mu>) = M" using space_closed by (auto intro!: sigma_sets_eq) -lemma (in sigma_algebra) space_measure_of_eq[simp]: - "space (measure_of \<Omega> M \<mu>) = \<Omega>" - using space_closed by (auto intro!: sigma_sets_eq) +lemma (in sigma_algebra) space_measure_of_eq[simp]: "space (measure_of \<Omega> M \<mu>) = \<Omega>" + by (rule space_measure_of_conv) -lemma measure_of_subset: - "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')" +lemma measure_of_subset: "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')" by (auto intro!: sigma_sets_subseteq) lemma sigma_sets_mono'': @@ -1725,6 +1722,42 @@ qed auto qed +subsection {* Restricted Space \<sigma>-Algebra *} + +definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))" + +lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>" + unfolding restrict_space_def by (subst space_measure_of) auto + +lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M" + using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"] + unfolding restrict_space_def + by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed) + +lemma sets_restrict_space_iff: + "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)" + by (subst sets_restrict_space) (auto dest: sets.sets_into_space) + +lemma measurable_restrict_space1: + assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N" + unfolding measurable_def +proof (intro CollectI conjI ballI) + show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N" + using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space) + + fix A assume "A \<in> sets N" + have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>" + using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space) + also have "\<dots> \<in> sets (restrict_space M \<Omega>)" + unfolding sets_restrict_space_iff[OF \<Omega>] + using measurable_sets[OF f `A \<in> sets N`] \<Omega> by blast + finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" . +qed + +lemma measurable_restrict_space2: + "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)" + by (simp add: measurable_def space_restrict_space sets_restrict_space_iff) + subsection {* A Two-Element Series *} definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "