src/HOL/Probability/Radon_Nikodym.thy
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.6  
     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"