changeset 39097 943c7b348524 parent 39092 98de40859858 child 40859 de0b30e6c2d2
1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 02 17:28:00 2010 +0200
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 02 19:51:53 2010 +0200
1.3 @@ -64,6 +64,30 @@
1.4  definition (in measure_space)
1.5    "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
1.7 +lemma (in finite_measure_space) absolutely_continuousI:
1.8 +  assumes "finite_measure_space M \<nu>"
1.9 +  assumes v: "\<And>x. \<lbrakk> x \<in> space M ; \<mu> {x} = 0 \<rbrakk> \<Longrightarrow> \<nu> {x} = 0"
1.10 +  shows "absolutely_continuous \<nu>"
1.11 +proof (unfold absolutely_continuous_def sets_eq_Pow, safe)
1.12 +  fix N assume "\<mu> N = 0" "N \<subseteq> space M"
1.13 +  interpret v: finite_measure_space M \<nu> by fact
1.14 +  have "\<nu> N = \<nu> (\<Union>x\<in>N. {x})" by simp
1.15 +  also have "\<dots> = (\<Sum>x\<in>N. \<nu> {x})"
1.16 +  proof (rule v.measure_finitely_additive''[symmetric])
1.17 +    show "finite N" using `N \<subseteq> space M` finite_space by (auto intro: finite_subset)
1.18 +    show "disjoint_family_on (\<lambda>i. {i}) N" unfolding disjoint_family_on_def by auto
1.19 +    fix x assume "x \<in> N" thus "{x} \<in> sets M" using `N \<subseteq> space M` sets_eq_Pow by auto
1.20 +  qed
1.21 +  also have "\<dots> = 0"
1.22 +  proof (safe intro!: setsum_0')
1.23 +    fix x assume "x \<in> N"
1.24 +    hence "\<mu> {x} \<le> \<mu> N" using sets_eq_Pow `N \<subseteq> space M` by (auto intro!: measure_mono)
1.25 +    hence "\<mu> {x} = 0" using `\<mu> N = 0` by simp
1.26 +    thus "\<nu> {x} = 0" using v[of x] `x \<in> N` `N \<subseteq> space M` by auto
1.27 +  qed
1.28 +  finally show "\<nu> N = 0" .
1.29 +qed
1.30 +
1.31  lemma (in finite_measure) Radon_Nikodym_aux_epsilon:
1.32    fixes e :: real assumes "0 < e"
1.33    assumes "finite_measure M s"