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

author | hoelzl |

Fri, 27 Aug 2010 14:06:12 +0200 | |

changeset 39089 | df379a447753 |

parent 39088 | ca17017c10e6 |

child 39090 | a2d38b8b693e |

vimage of measurable function is a measure space

src/HOL/Probability/Measure.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Probability/Probability_Space.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Probability/Measure.thy Fri Aug 27 14:05:16 2010 +0200 +++ b/src/HOL/Probability/Measure.thy Fri Aug 27 14:06:12 2010 +0200 @@ -451,6 +451,32 @@ qed qed +lemma (in measure_space) measure_space_vimage: + assumes "f \<in> measurable M M'" + and "sigma_algebra M'" + shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T") +proof - + interpret M': sigma_algebra M' by fact + + show ?thesis + proof + show "?T {} = 0" by simp + + show "countably_additive M' ?T" + proof (unfold countably_additive_def, safe) + fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A" + hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M" + using `f \<in> measurable M M'` by (auto simp: measurable_def) + moreover have "(\<Union>i. f -` A i \<inter> space M) \<in> sets M" + using * by blast + moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)" + using `disjoint_family A` by (auto simp: disjoint_family_on_def) + ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)" + using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN) + qed + qed +qed + section "@{text \<sigma>}-finite Measures" locale sigma_finite_measure = measure_space +

--- a/src/HOL/Probability/Probability_Space.thy Fri Aug 27 14:05:16 2010 +0200 +++ b/src/HOL/Probability/Probability_Space.thy Fri Aug 27 14:06:12 2010 +0200 @@ -197,35 +197,17 @@ qed lemma distribution_prob_space: - fixes S :: "('c, 'd) algebra_scheme" - assumes "sigma_algebra S" "random_variable S X" + assumes S: "sigma_algebra S" "random_variable S X" shows "prob_space S (distribution X)" proof - - interpret S: sigma_algebra S by fact + interpret S: measure_space S "distribution X" + using measure_space_vimage[OF S(2,1)] unfolding distribution_def . show ?thesis proof - show "distribution X {} = 0" unfolding distribution_def by simp have "X -` space S \<inter> space M = space M" using `random_variable S X` by (auto simp: measurable_def) - then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def) - - show "countably_additive S (distribution X)" - proof (unfold countably_additive_def, safe) - fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets S" "disjoint_family A" - hence *: "\<And>i. X -` A i \<inter> space M \<in> sets M" - using `random_variable S X` by (auto simp: measurable_def) - moreover hence "\<And>i. \<mu> (X -` A i \<inter> space M) \<noteq> \<omega>" - using finite_measure by auto - moreover have "(\<Union>i. X -` A i \<inter> space M) \<in> sets M" - using * by blast - moreover hence "\<mu> (\<Union>i. X -` A i \<inter> space M) \<noteq> \<omega>" - using finite_measure by auto - moreover have **: "disjoint_family (\<lambda>i. X -` A i \<inter> space M)" - using `disjoint_family A` by (auto simp: disjoint_family_on_def) - ultimately show "(\<Sum>\<^isub>\<infinity> i. distribution X (A i)) = distribution X (\<Union>i. A i)" - using measure_countably_additive[OF _ **] - by (auto simp: distribution_def Real_real comp_def vimage_UN) - qed + then show "distribution X (space S) = 1" + using measure_space_1 by (simp add: distribution_def) qed qed