add restrict_space measure
authorhoelzl
Tue Nov 12 19:28:56 2013 +0100 (2013-11-12)
changeset 54417dbb8ecfe1337
parent 54416 7fb88ed6ff3c
child 54418 3b8e33d1a39a
add restrict_space measure
src/HOL/Library/FuncSet.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Nov 12 19:28:55 2013 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Nov 12 19:28:56 2013 +0100
     1.3 @@ -183,18 +183,20 @@
     1.4  
     1.5  subsection{*Bounded Abstraction: @{term restrict}*}
     1.6  
     1.7 -lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
     1.8 +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"
     1.9    by (simp add: Pi_def restrict_def)
    1.10  
    1.11 -lemma restrictI[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
    1.12 +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"
    1.13    by (simp add: Pi_def restrict_def)
    1.14  
    1.15 -lemma restrict_apply [simp]:
    1.16 -    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
    1.17 +lemma restrict_apply[simp]: "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
    1.18    by (simp add: restrict_def)
    1.19  
    1.20 +lemma restrict_apply': "x \<in> A \<Longrightarrow> (\<lambda>y\<in>A. f y) x = f x"
    1.21 +  by simp
    1.22 +
    1.23  lemma restrict_ext:
    1.24 -    "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    1.25 +    "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    1.26    by (simp add: fun_eq_iff Pi_def restrict_def)
    1.27  
    1.28  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    1.29 @@ -364,6 +366,9 @@
    1.30  lemma PiE_empty_domain[simp]: "PiE {} T = {%x. undefined}"
    1.31    unfolding PiE_def by simp
    1.32  
    1.33 +lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T"
    1.34 +  unfolding PiE_def by simp
    1.35 +
    1.36  lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (PIE i:I. F i) = {}"
    1.37    unfolding PiE_def by auto
    1.38  
     2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Nov 12 19:28:55 2013 +0100
     2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Nov 12 19:28:56 2013 +0100
     2.3 @@ -2521,6 +2521,36 @@
     2.4    "f \<in> borel_measurable (count_space A)"
     2.5    by simp
     2.6  
     2.7 +section {* Measures with Restricted Space *}
     2.8 +
     2.9 +lemma positive_integral_restrict_space:
    2.10 +  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"
    2.11 +  shows "positive_integral (restrict_space M \<Omega>) f = positive_integral M f"
    2.12 +using f proof (induct rule: borel_measurable_induct)
    2.13 +  case (cong f g) then show ?case
    2.14 +    using positive_integral_cong[of M f g] positive_integral_cong[of "restrict_space M \<Omega>" f g]
    2.15 +      sets.sets_into_space[OF `\<Omega> \<in> sets M`]
    2.16 +    by (simp add: subset_eq space_restrict_space)
    2.17 +next
    2.18 +  case (set A)
    2.19 +  then have "A \<subseteq> \<Omega>"
    2.20 +    unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space)
    2.21 +  with set `\<Omega> \<in> sets M` sets.sets_into_space[OF `\<Omega> \<in> sets M`] show ?case
    2.22 +    by (subst positive_integral_indicator')
    2.23 +       (auto simp add: sets_restrict_space_iff space_restrict_space
    2.24 +                  emeasure_restrict_space Int_absorb2
    2.25 +                dest: sets.sets_into_space)
    2.26 +next
    2.27 +  case (mult f c) then show ?case
    2.28 +    by (cases "c = 0") (simp_all add: measurable_restrict_space1 \<Omega> positive_integral_cmult)
    2.29 +next
    2.30 +  case (add f g) then show ?case
    2.31 +    by (simp add: measurable_restrict_space1 \<Omega> positive_integral_add ereal_add_nonneg_eq_0_iff)
    2.32 +next
    2.33 +  case (seq F) then show ?case
    2.34 +    by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP)
    2.35 +qed
    2.36 +
    2.37  section {* Measure spaces with an associated density *}
    2.38  
    2.39  definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
     3.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Nov 12 19:28:55 2013 +0100
     3.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Nov 12 19:28:56 2013 +0100
     3.3 @@ -1118,6 +1118,10 @@
     3.4      and measurable_distr_eq2[simp]: "measurable Mg' (distr Mg Ng g) = measurable Mg' Ng"
     3.5    by (auto simp: measurable_def)
     3.6  
     3.7 +lemma distr_cong:
     3.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"
     3.9 +  using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong)
    3.10 +
    3.11  lemma emeasure_distr:
    3.12    fixes f :: "'a \<Rightarrow> 'b"
    3.13    assumes f: "f \<in> measurable M N" and A: "A \<in> sets N"
    3.14 @@ -1649,5 +1653,50 @@
    3.15    show "sigma_finite_measure (count_space A)" ..
    3.16  qed
    3.17  
    3.18 +section {* Measure restricted to space *}
    3.19 +
    3.20 +lemma emeasure_restrict_space:
    3.21 +  assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
    3.22 +  shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
    3.23 +proof cases
    3.24 +  assume "A \<in> sets M"
    3.25 +  
    3.26 +  have "emeasure (restrict_space M \<Omega>) A = emeasure M (A \<inter> \<Omega>)"
    3.27 +  proof (rule emeasure_measure_of[OF restrict_space_def])
    3.28 +    show "op \<inter> \<Omega> ` sets M \<subseteq> Pow \<Omega>" "A \<in> sets (restrict_space M \<Omega>)"
    3.29 +      using assms `A \<in> sets M` by (auto simp: sets_restrict_space sets.sets_into_space)
    3.30 +    show "positive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
    3.31 +      by (auto simp: positive_def emeasure_nonneg)
    3.32 +    show "countably_additive (sets (restrict_space M \<Omega>)) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
    3.33 +    proof (rule countably_additiveI)
    3.34 +      fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> sets (restrict_space M \<Omega>)" "disjoint_family A"
    3.35 +      with assms have "\<And>i. A i \<in> sets M" "\<And>i. A i \<subseteq> space M" "disjoint_family A"
    3.36 +        by (auto simp: sets_restrict_space_iff subset_eq dest: sets.sets_into_space)
    3.37 +      with `\<Omega> \<in> sets M` show "(\<Sum>i. emeasure M (A i \<inter> \<Omega>)) = emeasure M ((\<Union>i. A i) \<inter> \<Omega>)"
    3.38 +        by (subst suminf_emeasure) (auto simp: disjoint_family_subset)
    3.39 +    qed
    3.40 +  qed
    3.41 +  with `A \<subseteq> \<Omega>` show ?thesis
    3.42 +    by (simp add: Int_absorb2)
    3.43 +next
    3.44 +  assume "A \<notin> sets M"
    3.45 +  moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
    3.46 +    by (simp add: sets_restrict_space_iff)
    3.47 +  ultimately show ?thesis
    3.48 +    by (simp add: emeasure_notin_sets)
    3.49 +qed
    3.50 +
    3.51 +lemma restrict_count_space:
    3.52 +  assumes "A \<subseteq> B" shows "restrict_space (count_space B) A = count_space A"
    3.53 +proof (rule measure_eqI)
    3.54 +  show "sets (restrict_space (count_space B) A) = sets (count_space A)"
    3.55 +    using `A \<subseteq> B` by (subst sets_restrict_space) auto
    3.56 +  moreover fix X assume "X \<in> sets (restrict_space (count_space B) A)"
    3.57 +  moreover note `A \<subseteq> B`
    3.58 +  ultimately have "X \<subseteq> A" by auto
    3.59 +  with `A \<subseteq> B` show "emeasure (restrict_space (count_space B) A) X = emeasure (count_space A) X"
    3.60 +    by (cases "finite X") (auto simp add: emeasure_restrict_space)
    3.61 +qed
    3.62 +
    3.63  end
    3.64  
     4.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 12 19:28:55 2013 +0100
     4.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 12 19:28:56 2013 +0100
     4.3 @@ -1171,16 +1171,13 @@
     4.4  using assms
     4.5  by(simp_all add: sets_measure_of_conv space_measure_of_conv)
     4.6  
     4.7 -lemma (in sigma_algebra) sets_measure_of_eq[simp]:
     4.8 -  "sets (measure_of \<Omega> M \<mu>) = M"
     4.9 +lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \<Omega> M \<mu>) = M"
    4.10    using space_closed by (auto intro!: sigma_sets_eq)
    4.11  
    4.12 -lemma (in sigma_algebra) space_measure_of_eq[simp]:
    4.13 -  "space (measure_of \<Omega> M \<mu>) = \<Omega>"
    4.14 -  using space_closed by (auto intro!: sigma_sets_eq)
    4.15 +lemma (in sigma_algebra) space_measure_of_eq[simp]: "space (measure_of \<Omega> M \<mu>) = \<Omega>"
    4.16 +  by (rule space_measure_of_conv)
    4.17  
    4.18 -lemma measure_of_subset:
    4.19 -  "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
    4.20 +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>')"
    4.21    by (auto intro!: sigma_sets_subseteq)
    4.22  
    4.23  lemma sigma_sets_mono'':
    4.24 @@ -1725,6 +1722,42 @@
    4.25    qed auto
    4.26  qed
    4.27  
    4.28 +subsection {* Restricted Space \<sigma>-Algebra *}
    4.29 +
    4.30 +definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
    4.31 +
    4.32 +lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
    4.33 +  unfolding restrict_space_def by (subst space_measure_of) auto
    4.34 +
    4.35 +lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
    4.36 +  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
    4.37 +  unfolding restrict_space_def
    4.38 +  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
    4.39 +
    4.40 +lemma sets_restrict_space_iff:
    4.41 +  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
    4.42 +  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
    4.43 +
    4.44 +lemma measurable_restrict_space1:
    4.45 +  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
    4.46 +  unfolding measurable_def
    4.47 +proof (intro CollectI conjI ballI)
    4.48 +  show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
    4.49 +    using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
    4.50 +
    4.51 +  fix A assume "A \<in> sets N"
    4.52 +  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
    4.53 +    using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
    4.54 +  also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
    4.55 +    unfolding sets_restrict_space_iff[OF \<Omega>]
    4.56 +    using measurable_sets[OF f `A \<in> sets N`] \<Omega> by blast
    4.57 +  finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" .
    4.58 +qed
    4.59 +
    4.60 +lemma measurable_restrict_space2:
    4.61 +  "\<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>)"
    4.62 +  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
    4.63 +
    4.64  subsection {* A Two-Element Series *}
    4.65  
    4.66  definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "