author  hoelzl 
Mon, 14 Mar 2011 14:37:49 +0100  
changeset 41981  cdf7693bbe08 
parent 41832  27cb9113b1a0 
child 42067  66c8281349ec 
permissions  rwrr 
38656  1 
theory Radon_Nikodym 
2 
imports Lebesgue_Integration 

3 
begin 

4 

5 
lemma (in sigma_finite_measure) Ex_finite_integrable_function: 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

6 
shows "\<exists>h\<in>borel_measurable M. integral\<^isup>P M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>) \<and> (\<forall>x. 0 \<le> h x)" 
38656  7 
proof  
8 
obtain A :: "nat \<Rightarrow> 'a set" where 

9 
range: "range A \<subseteq> sets M" and 

10 
space: "(\<Union>i. A i) = space M" and 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

11 
measure: "\<And>i. \<mu> (A i) \<noteq> \<infinity>" and 
38656  12 
disjoint: "disjoint_family A" 
13 
using disjoint_sigma_finite by auto 

14 
let "?B i" = "2^Suc i * \<mu> (A i)" 

15 
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)" 

16 
proof 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

17 
fix i have Ai: "A i \<in> sets M" using range by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

18 
from measure positive_measure[OF this] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

19 
show "\<exists>x. 0 < x \<and> x < inverse (?B i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

20 
by (auto intro!: extreal_dense simp: extreal_0_gt_inverse) 
38656  21 
qed 
22 
from choice[OF this] obtain n where n: "\<And>i. 0 < n i" 

23 
"\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

24 
{ fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

25 
let "?h x" = "\<Sum>i. n i * indicator (A i) x" 
38656  26 
show ?thesis 
27 
proof (safe intro!: bexI[of _ ?h] del: notI) 

39092  28 
have "\<And>i. A i \<in> sets M" 
29 
using range by fastsimp+ 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

30 
then have "integral\<^isup>P M ?h = (\<Sum>i. n i * \<mu> (A i))" using pos 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

31 
by (simp add: positive_integral_suminf positive_integral_cmult_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

32 
also have "\<dots> \<le> (\<Sum>i. (1 / 2)^Suc i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

33 
proof (rule suminf_le_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

34 
fix N 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

35 
have "n N * \<mu> (A N) \<le> inverse (2^Suc N * \<mu> (A N)) * \<mu> (A N)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

36 
using positive_measure[OF `A N \<in> sets M`] n[of N] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

37 
by (intro extreal_mult_right_mono) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

38 
also have "\<dots> \<le> (1 / 2) ^ Suc N" 
38656  39 
using measure[of N] n[of N] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

40 
by (cases rule: extreal2_cases[of "n N" "\<mu> (A N)"]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

41 
(simp_all add: inverse_eq_divide power_divide one_extreal_def extreal_power_divide) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

42 
finally show "n N * \<mu> (A N) \<le> (1 / 2) ^ Suc N" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

43 
show "0 \<le> n N * \<mu> (A N)" using n[of N] `A N \<in> sets M` by simp 
38656  44 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

45 
finally show "integral\<^isup>P M ?h \<noteq> \<infinity>" unfolding suminf_half_series_extreal by auto 
38656  46 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

47 
{ fix x assume "x \<in> space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

48 
then obtain i where "x \<in> A i" using space[symmetric] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

49 
with disjoint n have "?h x = n i" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

50 
by (auto intro!: suminf_cmult_indicator intro: less_imp_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

51 
then show "0 < ?h x" and "?h x < \<infinity>" using n[of i] by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

52 
note pos = this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

53 
fix x show "0 \<le> ?h x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

54 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

55 
assume "x \<in> space M" then show "0 \<le> ?h x" using pos by (auto intro: less_imp_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

56 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

57 
assume "x \<notin> space M" then have "\<And>i. x \<notin> A i" using space by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

58 
then show "0 \<le> ?h x" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

59 
qed 
38656  60 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

61 
show "?h \<in> borel_measurable M" using range n 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

62 
by (auto intro!: borel_measurable_psuminf borel_measurable_extreal_times extreal_0_le_mult intro: less_imp_le) 
38656  63 
qed 
64 
qed 

65 

40871  66 
subsection "Absolutely continuous" 
67 

38656  68 
definition (in measure_space) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

69 
"absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: extreal))" 
38656  70 

41832  71 
lemma (in measure_space) absolutely_continuous_AE: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

72 
assumes "measure_space M'" and [simp]: "sets M' = sets M" "space M' = space M" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

73 
and "absolutely_continuous (measure M')" "AE x. P x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

74 
shows "AE x in M'. P x" 
40859  75 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

76 
interpret \<nu>: measure_space M' by fact 
40859  77 
from `AE x. P x` obtain N where N: "N \<in> null_sets" and "{x\<in>space M. \<not> P x} \<subseteq> N" 
78 
unfolding almost_everywhere_def by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

79 
show "AE x in M'. P x" 
40859  80 
proof (rule \<nu>.AE_I') 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

81 
show "{x\<in>space M'. \<not> P x} \<subseteq> N" by simp fact 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

82 
from `absolutely_continuous (measure M')` show "N \<in> \<nu>.null_sets" 
40859  83 
using N unfolding absolutely_continuous_def by auto 
84 
qed 

85 
qed 

86 

39097  87 
lemma (in finite_measure_space) absolutely_continuousI: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

88 
assumes "finite_measure_space (M\<lparr> measure := \<nu>\<rparr>)" (is "finite_measure_space ?\<nu>") 
39097  89 
assumes v: "\<And>x. \<lbrakk> x \<in> space M ; \<mu> {x} = 0 \<rbrakk> \<Longrightarrow> \<nu> {x} = 0" 
90 
shows "absolutely_continuous \<nu>" 

91 
proof (unfold absolutely_continuous_def sets_eq_Pow, safe) 

92 
fix N assume "\<mu> N = 0" "N \<subseteq> space M" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

93 
interpret v: finite_measure_space ?\<nu> by fact 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

94 
have "\<nu> N = measure ?\<nu> (\<Union>x\<in>N. {x})" by simp 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

95 
also have "\<dots> = (\<Sum>x\<in>N. measure ?\<nu> {x})" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

96 
proof (rule v.measure_setsum[symmetric]) 
39097  97 
show "finite N" using `N \<subseteq> space M` finite_space by (auto intro: finite_subset) 
98 
show "disjoint_family_on (\<lambda>i. {i}) N" unfolding disjoint_family_on_def by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

99 
fix x assume "x \<in> N" thus "{x} \<in> sets ?\<nu>" using `N \<subseteq> space M` sets_eq_Pow by auto 
39097  100 
qed 
101 
also have "\<dots> = 0" 

102 
proof (safe intro!: setsum_0') 

103 
fix x assume "x \<in> N" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

104 
hence "\<mu> {x} \<le> \<mu> N" "0 \<le> \<mu> {x}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

105 
using sets_eq_Pow `N \<subseteq> space M` positive_measure[of "{x}"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

106 
by (auto intro!: measure_mono) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

107 
then have "\<mu> {x} = 0" using `\<mu> N = 0` by simp 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

108 
thus "measure ?\<nu> {x} = 0" using v[of x] `x \<in> N` `N \<subseteq> space M` by auto 
39097  109 
qed 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

110 
finally show "\<nu> N = 0" by simp 
39097  111 
qed 
112 

40871  113 
lemma (in measure_space) density_is_absolutely_continuous: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

114 
assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)" 
40871  115 
shows "absolutely_continuous \<nu>" 
116 
using assms unfolding absolutely_continuous_def 

117 
by (simp add: positive_integral_null_set) 

118 

119 
subsection "Existence of the RadonNikodym derivative" 

120 

38656  121 
lemma (in finite_measure) Radon_Nikodym_aux_epsilon: 
122 
fixes e :: real assumes "0 < e" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

123 
assumes "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

124 
shows "\<exists>A\<in>sets M. \<mu>' (space M)  finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) (space M) \<le> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

125 
\<mu>' A  finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) A \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

126 
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow>  e < \<mu>' B  finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) B)" 
38656  127 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

128 
interpret M': finite_measure "M\<lparr>measure := \<nu>\<rparr>" by fact 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

129 
let "?d A" = "\<mu>' A  M'.\<mu>' A" 
38656  130 
let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M  A \<longrightarrow> e < ?d B) 
131 
then {} 

132 
else (SOME B. B \<in> sets M \<and> B \<subseteq> space M  A \<and> ?d B \<le> e)" 

133 
def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}" 

134 
have A_simps[simp]: 

135 
"A 0 = {}" 

136 
"\<And>n. A (Suc n) = (A n \<union> ?A (A n))" unfolding A_def by simp_all 

137 
{ fix A assume "A \<in> sets M" 

138 
have "?A A \<in> sets M" 

139 
by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) } 

140 
note A'_in_sets = this 

141 
{ fix n have "A n \<in> sets M" 

142 
proof (induct n) 

143 
case (Suc n) thus "A (Suc n) \<in> sets M" 

144 
using A'_in_sets[of "A n"] by (auto split: split_if_asm) 

145 
qed (simp add: A_def) } 

146 
note A_in_sets = this 

147 
hence "range A \<subseteq> sets M" by auto 

148 
{ fix n B 

149 
assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M  A n \<and> ?d B \<le> e" 

150 
hence False: "\<not> (\<forall>B\<in>sets M. B \<subseteq> space M  A n \<longrightarrow> e < ?d B)" by (auto simp: not_less) 

151 
have "?d (A (Suc n)) \<le> ?d (A n)  e" unfolding A_simps if_not_P[OF False] 

152 
proof (rule someI2_ex[OF Ex]) 

153 
fix B assume "B \<in> sets M \<and> B \<subseteq> space M  A n \<and> ?d B \<le>  e" 

154 
hence "A n \<inter> B = {}" "B \<in> sets M" and dB: "?d B \<le> e" by auto 

155 
hence "?d (A n \<union> B) = ?d (A n) + ?d B" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

156 
using `A n \<in> sets M` finite_measure_Union M'.finite_measure_Union by simp 
38656  157 
also have "\<dots> \<le> ?d (A n)  e" using dB by simp 
158 
finally show "?d (A n \<union> B) \<le> ?d (A n)  e" . 

159 
qed } 

160 
note dA_epsilon = this 

161 
{ fix n have "?d (A (Suc n)) \<le> ?d (A n)" 

162 
proof (cases "\<exists>B. B\<in>sets M \<and> B \<subseteq> space M  A n \<and> ?d B \<le>  e") 

163 
case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp 

164 
next 

165 
case False 

166 
hence "\<forall>B\<in>sets M. B \<subseteq> space M  A n \<longrightarrow> e < ?d B" by (auto simp: not_le) 

167 
thus ?thesis by simp 

168 
qed } 

169 
note dA_mono = this 

170 
show ?thesis 

171 
proof (cases "\<exists>n. \<forall>B\<in>sets M. B \<subseteq> space M  A n \<longrightarrow> e < ?d B") 

172 
case True then obtain n where B: "\<And>B. \<lbrakk> B \<in> sets M; B \<subseteq> space M  A n\<rbrakk> \<Longrightarrow> e < ?d B" by blast 

173 
show ?thesis 

174 
proof (safe intro!: bexI[of _ "space M  A n"]) 

175 
fix B assume "B \<in> sets M" "B \<subseteq> space M  A n" 

176 
from B[OF this] show "e < ?d B" . 

177 
next 

178 
show "space M  A n \<in> sets M" by (rule compl_sets) fact 

179 
next 

180 
show "?d (space M) \<le> ?d (space M  A n)" 

181 
proof (induct n) 

182 
fix n assume "?d (space M) \<le> ?d (space M  A n)" 

183 
also have "\<dots> \<le> ?d (space M  A (Suc n))" 

184 
using A_in_sets sets_into_space dA_mono[of n] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

185 
by (simp del: A_simps add: finite_measure_Diff M'.finite_measure_Diff) 
38656  186 
finally show "?d (space M) \<le> ?d (space M  A (Suc n))" . 
187 
qed simp 

188 
qed 

189 
next 

190 
case False hence B: "\<And>n. \<exists>B. B\<in>sets M \<and> B \<subseteq> space M  A n \<and> ?d B \<le>  e" 

191 
by (auto simp add: not_less) 

192 
{ fix n have "?d (A n) \<le>  real n * e" 

193 
proof (induct n) 

194 
case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

195 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

196 
case 0 with M'.empty_measure show ?case by (simp add: zero_extreal_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

197 
qed } note dA_less = this 
38656  198 
have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq 
199 
proof (rule incseq_SucI) 

200 
fix n show " ?d (A n) \<le>  ?d (A (Suc n))" using dA_mono[of n] by auto 

201 
qed 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

202 
have A: "incseq A" by (auto intro!: incseq_SucI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

203 
from finite_continuity_from_below[OF _ A] `range A \<subseteq> sets M` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

204 
M'.finite_continuity_from_below[OF _ A] 
38656  205 
have convergent: "(\<lambda>i. ?d (A i)) > ?d (\<Union>i. A i)" 
206 
by (auto intro!: LIMSEQ_diff) 

207 
obtain n :: nat where " ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto 

208 
moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less] 

209 
have "real n \<le>  ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps) 

210 
ultimately show ?thesis by auto 

211 
qed 

212 
qed 

213 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

214 
lemma (in finite_measure) restricted_measure_subset: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

215 
assumes S: "S \<in> sets M" and X: "X \<subseteq> S" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

216 
shows "finite_measure.\<mu>' (restricted_space S) X = \<mu>' X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

217 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

218 
note r = restricted_finite_measure[OF S] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

219 
{ assume "X \<in> sets M" with S X show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

220 
unfolding finite_measure.\<mu>'_def[OF r] \<mu>'_def by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

221 
{ assume "X \<notin> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

222 
moreover then have "S \<inter> X \<notin> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

223 
using X by (simp add: Int_absorb1) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

224 
ultimately show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

225 
unfolding finite_measure.\<mu>'_def[OF r] \<mu>'_def using S by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

226 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

227 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

228 
lemma (in finite_measure) restricted_measure: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

229 
assumes X: "S \<in> sets M" "X \<in> sets (restricted_space S)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

230 
shows "finite_measure.\<mu>' (restricted_space S) X = \<mu>' X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

231 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

232 
from X have "S \<in> sets M" "X \<subseteq> S" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

233 
from restricted_measure_subset[OF this] show ?thesis . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

234 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

235 

38656  236 
lemma (in finite_measure) Radon_Nikodym_aux: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

237 
assumes "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" (is "finite_measure ?M'") 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

238 
shows "\<exists>A\<in>sets M. \<mu>' (space M)  finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) (space M) \<le> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

239 
\<mu>' A  finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) A \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

240 
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> \<mu>' B  finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) B)" 
38656  241 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

242 
interpret M': finite_measure ?M' where 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

243 
"space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \<nu>" by fact auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

244 
let "?d A" = "\<mu>' A  M'.\<mu>' A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

245 
let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow>  1 / real (Suc n) < ?d C)" 
39092  246 
let "?r S" = "restricted_space S" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

247 
{ fix S n assume S: "S \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

248 
note r = M'.restricted_finite_measure[of S] restricted_finite_measure[OF S] S 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

249 
then have "finite_measure (?r S)" "0 < 1 / real (Suc n)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

250 
"finite_measure (?r S\<lparr>measure := \<nu>\<rparr>)" by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

251 
from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

252 
have "?P X S n" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

253 
proof (intro conjI ballI impI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

254 
show "X \<in> sets M" "X \<subseteq> S" using X(1) `S \<in> sets M` by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

255 
have "S \<in> op \<inter> S ` sets M" using `S \<in> sets M` by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

256 
then show "?d S \<le> ?d X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

257 
using S X restricted_measure[OF S] M'.restricted_measure[OF S] by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

258 
fix C assume "C \<in> sets M" "C \<subseteq> X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

259 
then have "C \<in> sets (restricted_space S)" "C \<subseteq> X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

260 
using `S \<in> sets M` `X \<subseteq> S` by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

261 
with X(2) show " 1 / real (Suc n) < ?d C" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

262 
using S X restricted_measure[OF S] M'.restricted_measure[OF S] by auto 
38656  263 
qed 
264 
hence "\<exists>A. ?P A S n" by auto } 

265 
note Ex_P = this 

266 
def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)" 

267 
have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def) 

268 
have A_0[simp]: "A 0 = space M" unfolding A_def by simp 

269 
{ fix i have "A i \<in> sets M" unfolding A_def 

270 
proof (induct i) 

271 
case (Suc i) 

272 
from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc 

273 
by (rule someI2_ex) simp 

274 
qed simp } 

275 
note A_in_sets = this 

276 
{ fix n have "?P (A (Suc n)) (A n) n" 

277 
using Ex_P[OF A_in_sets] unfolding A_Suc 

278 
by (rule someI2_ex) simp } 

279 
note P_A = this 

280 
have "range A \<subseteq> sets M" using A_in_sets by auto 

281 
have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp 

282 
have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc) 

283 
have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow>  1 / real (Suc i) < ?d C" 

284 
using P_A by auto 

285 
show ?thesis 

286 
proof (safe intro!: bexI[of _ "\<Inter>i. A i"]) 

287 
show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

288 
have A: "decseq A" using A_mono by (auto intro!: decseq_SucI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

289 
from 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

290 
finite_continuity_from_above[OF `range A \<subseteq> sets M` A] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

291 
M'.finite_continuity_from_above[OF `range A \<subseteq> sets M` A] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

292 
have "(\<lambda>i. ?d (A i)) > ?d (\<Inter>i. A i)" by (intro LIMSEQ_diff) 
38656  293 
thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _] 
294 
by (rule_tac LIMSEQ_le_const) (auto intro!: exI) 

295 
next 

296 
fix B assume B: "B \<in> sets M" "B \<subseteq> (\<Inter>i. A i)" 

297 
show "0 \<le> ?d B" 

298 
proof (rule ccontr) 

299 
assume "\<not> 0 \<le> ?d B" 

300 
hence "0 <  ?d B" by auto 

301 
from ex_inverse_of_nat_Suc_less[OF this] 

302 
obtain n where *: "?d B <  1 / real (Suc n)" 

303 
by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) 

304 
have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc) 

305 
from epsilon[OF B(1) this] * 

306 
show False by auto 

307 
qed 

308 
qed 

309 
qed 

310 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

311 
lemma (in finite_measure) real_measure: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

312 
assumes A: "A \<in> sets M" shows "\<exists>r. 0 \<le> r \<and> \<mu> A = extreal r" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

313 
using finite_measure[OF A] positive_measure[OF A] by (cases "\<mu> A") auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

314 

38656  315 
lemma (in finite_measure) Radon_Nikodym_finite_measure: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

316 
assumes "finite_measure (M\<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?M'") 
38656  317 
assumes "absolutely_continuous \<nu>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

318 
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)" 
38656  319 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

320 
interpret M': finite_measure ?M' 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

321 
where "space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \<nu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

322 
using assms(1) by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

323 
def G \<equiv> "{g \<in> borel_measurable M. (\<forall>x. 0 \<le> g x) \<and> (\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> \<nu> A)}" 
38656  324 
have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto 
325 
hence "G \<noteq> {}" by auto 

326 
{ fix f g assume f: "f \<in> G" and g: "g \<in> G" 

327 
have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def 

328 
proof safe 

329 
show "?max \<in> borel_measurable M" using f g unfolding G_def by auto 

330 
let ?A = "{x \<in> space M. f x \<le> g x}" 

331 
have "?A \<in> sets M" using f g unfolding G_def by auto 

332 
fix A assume "A \<in> sets M" 

333 
hence sets: "?A \<inter> A \<in> sets M" "(space M  ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto 

334 
have union: "((?A \<inter> A) \<union> ((space M  ?A) \<inter> A)) = A" 

335 
using sets_into_space[OF `A \<in> sets M`] by auto 

336 
have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x = 

337 
g x * indicator (?A \<inter> A) x + f x * indicator ((space M  ?A) \<inter> A) x" 

338 
by (auto simp: indicator_def max_def) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

339 
hence "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x \<partial>M) = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

340 
(\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x \<partial>M) + 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

341 
(\<integral>\<^isup>+x. f x * indicator ((space M  ?A) \<inter> A) x \<partial>M)" 
38656  342 
using f g sets unfolding G_def 
343 
by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator) 

344 
also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M  ?A) \<inter> A)" 

345 
using f g sets unfolding G_def by (auto intro!: add_mono) 

346 
also have "\<dots> = \<nu> A" 

347 
using M'.measure_additive[OF sets] union by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

348 
finally show "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x \<partial>M) \<le> \<nu> A" . 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

349 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

350 
fix x show "0 \<le> max (g x) (f x)" using f g by (auto simp: G_def split: split_max) 
38656  351 
qed } 
352 
note max_in_G = this 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

353 
{ fix f assume "incseq f" and f: "\<And>i. f i \<in> G" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

354 
have "(\<lambda>x. SUP i. f i x) \<in> G" unfolding G_def 
38656  355 
proof safe 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

356 
show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

357 
using f by (auto simp: G_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

358 
{ fix x show "0 \<le> (SUP i. f i x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

359 
using f by (auto simp: G_def intro: le_SUPI2) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

360 
next 
38656  361 
fix A assume "A \<in> sets M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

362 
have "(\<integral>\<^isup>+x. (SUP i. f i x) * indicator A x \<partial>M) = 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

363 
(\<integral>\<^isup>+x. (SUP i. f i x * indicator A x) \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

364 
by (intro positive_integral_cong) (simp split: split_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

365 
also have "\<dots> = (SUP i. (\<integral>\<^isup>+x. f i x * indicator A x \<partial>M))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

366 
using `incseq f` f `A \<in> sets M` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

367 
by (intro positive_integral_monotone_convergence_SUP) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

368 
(auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

369 
finally show "(\<integral>\<^isup>+x. (SUP i. f i x) * indicator A x \<partial>M) \<le> \<nu> A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

370 
using f `A \<in> sets M` by (auto intro!: SUP_leI simp: G_def) 
38656  371 
qed } 
372 
note SUP_in_G = this 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

373 
let ?y = "SUP g : G. integral\<^isup>P M g" 
38656  374 
have "?y \<le> \<nu> (space M)" unfolding G_def 
375 
proof (safe intro!: SUP_leI) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

376 
fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> \<nu> A" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

377 
from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> \<nu> (space M)" 
38656  378 
by (simp cong: positive_integral_cong) 
379 
qed 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

380 
from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^isup>P M"] guess ys .. note ys = this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

381 
then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^isup>P M g = ys n" 
38656  382 
proof safe 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

383 
fix n assume "range ys \<subseteq> integral\<^isup>P M ` G" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

384 
hence "ys n \<in> integral\<^isup>P M ` G" by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

385 
thus "\<exists>g. g\<in>G \<and> integral\<^isup>P M g = ys n" by auto 
38656  386 
qed 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

387 
from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^isup>P M (gs n) = ys n" by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

388 
hence y_eq: "?y = (SUP i. integral\<^isup>P M (gs i))" using ys by auto 
38656  389 
let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

390 
def f \<equiv> "\<lambda>x. SUP i. ?g i x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

391 
let "?F A x" = "f x * indicator A x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

392 
have gs_not_empty: "\<And>i x. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto 
38656  393 
{ fix i have "?g i \<in> G" 
394 
proof (induct i) 

395 
case 0 thus ?case by simp fact 

396 
next 

397 
case (Suc i) 

398 
with Suc gs_not_empty `gs (Suc i) \<in> G` show ?case 

399 
by (auto simp add: atMost_Suc intro!: max_in_G) 

400 
qed } 

401 
note g_in_G = this 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

402 
have "incseq ?g" using gs_not_empty 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

403 
by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

404 
from SUP_in_G[OF this g_in_G] have "f \<in> G" unfolding f_def . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

405 
then have [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

406 
have "integral\<^isup>P M f = (SUP i. integral\<^isup>P M (?g i))" unfolding f_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

407 
using g_in_G `incseq ?g` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

408 
by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def) 
38656  409 
also have "\<dots> = ?y" 
410 
proof (rule antisym) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

411 
show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y" 
38656  412 
using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

413 
show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq 
38656  414 
by (auto intro!: SUP_mono positive_integral_mono Max_ge) 
415 
qed 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

416 
finally have int_f_eq_y: "integral\<^isup>P M f = ?y" . 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

417 
have "\<And>x. 0 \<le> f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

418 
unfolding f_def using `\<And>i. gs i \<in> G` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

419 
by (auto intro!: le_SUPI2 Max_ge_iff[THEN iffD2] simp: G_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

420 
let "?t A" = "\<nu> A  (\<integral>\<^isup>+x. ?F A x \<partial>M)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

421 
let ?M = "M\<lparr> measure := ?t\<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

422 
interpret M: sigma_algebra ?M 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

423 
by (intro sigma_algebra_cong) auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

424 
have f_le_\<nu>: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. ?F A x \<partial>M) \<le> \<nu> A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

425 
using `f \<in> G` unfolding G_def by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

426 
have fmM: "finite_measure ?M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

427 
proof (default, simp_all add: countably_additive_def positive_def, safe del: notI) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

428 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

429 
have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. (\<Sum>n. ?F (A n) x) \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

430 
using `range A \<subseteq> sets M` `\<And>x. 0 \<le> f x` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

431 
by (intro positive_integral_suminf[symmetric]) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

432 
also have "\<dots> = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

433 
using `\<And>x. 0 \<le> f x` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

434 
by (intro positive_integral_cong) (simp add: suminf_cmult_extreal suminf_indicator[OF `disjoint_family A`]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

435 
finally have "(\<Sum>n. (\<integral>\<^isup>+x. ?F (A n) x \<partial>M)) = (\<integral>\<^isup>+x. ?F (\<Union>n. A n) x \<partial>M)" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

436 
moreover have "(\<Sum>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

437 
using M'.measure_countably_additive A by (simp add: comp_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

438 
moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<infinity>" using M'.finite_measure A by (simp add: countable_UN) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

439 
moreover { 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

440 
have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<le> \<nu> (\<Union>i. A i)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

441 
using A `f \<in> G` unfolding G_def by (auto simp: countable_UN) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

442 
also have "\<nu> (\<Union>i. A i) < \<infinity>" using v_fin by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

443 
finally have "(\<integral>\<^isup>+x. ?F (\<Union>i. A i) x \<partial>M) \<noteq> \<infinity>" by simp } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

444 
moreover have "\<And>i. (\<integral>\<^isup>+x. ?F (A i) x \<partial>M) \<le> \<nu> (A i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

445 
using A by (intro f_le_\<nu>) auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

446 
ultimately 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

447 
show "(\<Sum>n. ?t (A n)) = ?t (\<Union>i. A i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

448 
by (subst suminf_extreal_minus) (simp_all add: positive_integral_positive) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

449 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

450 
fix A assume A: "A \<in> sets M" show "0 \<le> \<nu> A  \<integral>\<^isup>+ x. ?F A x \<partial>M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

451 
using f_le_\<nu>[OF A] `f \<in> G` M'.finite_measure[OF A] by (auto simp: G_def extreal_le_minus_iff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

452 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

453 
show "\<nu> (space M)  (\<integral>\<^isup>+ x. ?F (space M) x \<partial>M) \<noteq> \<infinity>" (is "?a  ?b \<noteq> _") 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

454 
using positive_integral_positive[of "?F (space M)"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

455 
by (cases rule: extreal2_cases[of ?a ?b]) auto 
38656  456 
qed 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

457 
then interpret M: finite_measure ?M 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

458 
where "space ?M = space M" and "sets ?M = sets M" and "measure ?M = ?t" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

459 
by (simp_all add: fmM) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

460 
have ac: "absolutely_continuous ?t" unfolding absolutely_continuous_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

461 
proof 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

462 
fix N assume N: "N \<in> null_sets" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

463 
with `absolutely_continuous \<nu>` have "\<nu> N = 0" unfolding absolutely_continuous_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

464 
moreover with N have "(\<integral>\<^isup>+ x. ?F N x \<partial>M) \<le> \<nu> N" using `f \<in> G` by (auto simp: G_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

465 
ultimately show "\<nu> N  (\<integral>\<^isup>+ x. ?F N x \<partial>M) = 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

466 
using positive_integral_positive by (auto intro!: antisym) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

467 
qed 
38656  468 
have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0" 
469 
proof (rule ccontr) 

470 
assume "\<not> ?thesis" 

471 
then obtain A where A: "A \<in> sets M" and pos: "0 < ?t A" 

472 
by (auto simp: not_le) 

473 
note pos 

474 
also have "?t A \<le> ?t (space M)" 

475 
using M.measure_mono[of A "space M"] A sets_into_space by simp 

476 
finally have pos_t: "0 < ?t (space M)" by simp 

477 
moreover 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

478 
then have "\<mu> (space M) \<noteq> 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

479 
using ac unfolding absolutely_continuous_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

480 
then have pos_M: "0 < \<mu> (space M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

481 
using positive_measure[OF top] by (simp add: le_less) 
38656  482 
moreover 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

483 
have "(\<integral>\<^isup>+x. f x * indicator (space M) x \<partial>M) \<le> \<nu> (space M)" 
38656  484 
using `f \<in> G` unfolding G_def by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

485 
hence "(\<integral>\<^isup>+x. f x * indicator (space M) x \<partial>M) \<noteq> \<infinity>" 
38656  486 
using M'.finite_measure_of_space by auto 
487 
moreover 

488 
def b \<equiv> "?t (space M) / \<mu> (space M) / 2" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

489 
ultimately have b: "b \<noteq> 0 \<and> 0 \<le> b \<and> b \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

490 
using M'.finite_measure_of_space positive_integral_positive[of "?F (space M)"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

491 
by (cases rule: extreal3_cases[of "integral\<^isup>P M (?F (space M))" "\<nu> (space M)" "\<mu> (space M)"]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

492 
(simp_all add: field_simps) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

493 
then have b: "b \<noteq> 0" "0 \<le> b" "0 < b" "b \<noteq> \<infinity>" by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

494 
let ?Mb = "?M\<lparr>measure := \<lambda>A. b * \<mu> A\<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

495 
interpret b: sigma_algebra ?Mb by (intro sigma_algebra_cong) auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

496 
have Mb: "finite_measure ?Mb" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

497 
proof 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

498 
show "positive ?Mb (measure ?Mb)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

499 
using `0 \<le> b` by (auto simp: positive_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

500 
show "countably_additive ?Mb (measure ?Mb)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

501 
using `0 \<le> b` measure_countably_additive 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

502 
by (auto simp: countably_additive_def suminf_cmult_extreal subset_eq) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

503 
show "measure ?Mb (space ?Mb) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

504 
using b by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

505 
qed 
38656  506 
from M.Radon_Nikodym_aux[OF this] 
507 
obtain A0 where "A0 \<in> sets M" and 

508 
space_less_A0: "real (?t (space M))  real (b * \<mu> (space M)) \<le> real (?t A0)  real (b * \<mu> A0)" and 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

509 
*: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B)  real (b * \<mu> B)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

510 
unfolding M.\<mu>'_def finite_measure.\<mu>'_def[OF Mb] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

511 
{ fix B assume B: "B \<in> sets M" "B \<subseteq> A0" 
38656  512 
with *[OF this] have "b * \<mu> B \<le> ?t B" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

513 
using M'.finite_measure b finite_measure M.positive_measure[OF B(1)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

514 
by (cases rule: extreal2_cases[of "?t B" "b * \<mu> B"]) auto } 
38656  515 
note bM_le_t = this 
516 
let "?f0 x" = "f x + b * indicator A0 x" 

517 
{ fix A assume A: "A \<in> sets M" 

518 
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

519 
have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

520 
(\<integral>\<^isup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

521 
by (auto intro!: positive_integral_cong split: split_indicator) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

522 
hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

523 
(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + b * \<mu> (A \<inter> A0)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

524 
using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A b `f \<in> G` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

525 
by (simp add: G_def positive_integral_add positive_integral_cmult_indicator) } 
38656  526 
note f0_eq = this 
527 
{ fix A assume A: "A \<in> sets M" 

528 
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

529 
have f_le_v: "(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) \<le> \<nu> A" 
38656  530 
using `f \<in> G` A unfolding G_def by auto 
531 
note f0_eq[OF A] 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

532 
also have "(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + b * \<mu> (A \<inter> A0) \<le> 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

533 
(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + ?t (A \<inter> A0)" 
38656  534 
using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M` 
535 
by (auto intro!: add_left_mono) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

536 
also have "\<dots> \<le> (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) + ?t A" 
38656  537 
using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`] 
538 
by (auto intro!: add_left_mono) 

539 
also have "\<dots> \<le> \<nu> A" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

540 
using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`] positive_integral_positive[of "?F A"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

541 
by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "\<nu> A") auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

542 
finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> \<nu> A" . } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

543 
hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

544 
by (auto intro!: borel_measurable_indicator borel_measurable_extreal_add 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

545 
borel_measurable_extreal_times extreal_add_nonneg_nonneg) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

546 
have real: "?t (space M) \<noteq> \<infinity>" "?t A0 \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

547 
"b * \<mu> (space M) \<noteq> \<infinity>" "b * \<mu> A0 \<noteq> \<infinity>" 
38656  548 
using `A0 \<in> sets M` b 
549 
finite_measure[of A0] M.finite_measure[of A0] 

550 
finite_measure_of_space M.finite_measure_of_space 

551 
by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

552 
have int_f_finite: "integral\<^isup>P M f \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

553 
using M'.finite_measure_of_space pos_t unfolding extreal_less_minus_iff 
38656  554 
by (auto cong: positive_integral_cong) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

555 
have "0 < ?t (space M)  b * \<mu> (space M)" unfolding b_def 
38656  556 
using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

557 
using positive_integral_positive[of "?F (space M)"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

558 
by (cases rule: extreal3_cases[of "\<mu> (space M)" "\<nu> (space M)" "integral\<^isup>P M (?F (space M))"]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

559 
(auto simp: field_simps mult_less_cancel_left) 
38656  560 
also have "\<dots> \<le> ?t A0  b * \<mu> A0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

561 
using space_less_A0 b 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

562 
using 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

563 
`A0 \<in> sets M`[THEN M.real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

564 
top[THEN M.real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

565 
apply safe 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

566 
apply simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

567 
using 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

568 
`A0 \<in> sets M`[THEN real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

569 
`A0 \<in> sets M`[THEN M'.real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

570 
top[THEN real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

571 
top[THEN M'.real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

572 
by (cases b) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

573 
finally have 1: "b * \<mu> A0 < ?t A0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

574 
using 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

575 
`A0 \<in> sets M`[THEN M.real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

576 
apply safe 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

577 
apply simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

578 
using 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

579 
`A0 \<in> sets M`[THEN real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

580 
`A0 \<in> sets M`[THEN M'.real_measure] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

581 
by (cases b) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

582 
have "0 < ?t A0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

583 
using b `A0 \<in> sets M` by (auto intro!: le_less_trans[OF _ 1]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

584 
then have "\<mu> A0 \<noteq> 0" using ac unfolding absolutely_continuous_def 
38656  585 
using `A0 \<in> sets M` by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

586 
then have "0 < \<mu> A0" using positive_measure[OF `A0 \<in> sets M`] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

587 
hence "0 < b * \<mu> A0" using b by (auto simp: extreal_zero_less_0_iff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

588 
with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * \<mu> A0" unfolding int_f_eq_y 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

589 
using `f \<in> G` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

590 
by (intro extreal_add_strict_mono) (auto intro!: le_SUPI2 positive_integral_positive) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

591 
also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space 
38656  592 
by (simp cong: positive_integral_cong) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

593 
finally have "?y < integral\<^isup>P M ?f0" by simp 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

594 
moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: le_SUPI) 
38656  595 
ultimately show False by auto 
596 
qed 

597 
show ?thesis 

598 
proof (safe intro!: bexI[of _ f]) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

599 
fix A assume A: "A\<in>sets M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

600 
show "\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)" 
38656  601 
proof (rule antisym) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

602 
show "(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) \<le> \<nu> A" 
38656  603 
using `f \<in> G` `A \<in> sets M` unfolding G_def by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

604 
show "\<nu> A \<le> (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)" 
38656  605 
using upper_bound[THEN bspec, OF `A \<in> sets M`] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

606 
using M'.real_measure[OF A] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

607 
by (cases "integral\<^isup>P M (?F A)") auto 
38656  608 
qed 
609 
qed simp 

610 
qed 

611 

40859  612 
lemma (in finite_measure) split_space_into_finite_sets_and_rest: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

613 
assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?N") 
40859  614 
assumes ac: "absolutely_continuous \<nu>" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

615 
shows "\<exists>A0\<in>sets M. \<exists>B::nat\<Rightarrow>'a set. disjoint_family B \<and> range B \<subseteq> sets M \<and> A0 = space M  (\<Union>i. B i) \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

616 
(\<forall>A\<in>sets M. A \<subseteq> A0 \<longrightarrow> (\<mu> A = 0 \<and> \<nu> A = 0) \<or> (\<mu> A > 0 \<and> \<nu> A = \<infinity>)) \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

617 
(\<forall>i. \<nu> (B i) \<noteq> \<infinity>)" 
38656  618 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

619 
interpret v: measure_space ?N 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

620 
where "space ?N = space M" and "sets ?N = sets M" and "measure ?N = \<nu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

621 
by fact auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

622 
let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<infinity>}" 
38656  623 
let ?a = "SUP Q:?Q. \<mu> Q" 
624 
have "{} \<in> ?Q" using v.empty_measure by auto 

625 
then have Q_not_empty: "?Q \<noteq> {}" by blast 

626 
have "?a \<le> \<mu> (space M)" using sets_into_space 

627 
by (auto intro!: SUP_leI measure_mono top) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

628 
then have "?a \<noteq> \<infinity>" using finite_measure_of_space 
38656  629 
by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

630 
from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>] 
38656  631 
obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)" 
632 
by auto 

633 
then have "\<forall>i. \<exists>Q'. Q'' i = \<mu> Q' \<and> Q' \<in> ?Q" by auto 

634 
from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q" 

635 
by auto 

636 
then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp 

637 
let "?O n" = "\<Union>i\<le>n. Q' i" 

638 
have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)" 

639 
proof (rule continuity_from_below[of ?O]) 

640 
show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

641 
show "incseq ?O" by (fastsimp intro!: incseq_SucI) 
38656  642 
qed 
643 
have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto 

644 
have O_sets: "\<And>i. ?O i \<in> sets M" 

645 
using Q' by (auto intro!: finite_UN Un) 

646 
then have O_in_G: "\<And>i. ?O i \<in> ?Q" 

647 
proof (safe del: notI) 

648 
fix i have "Q' ` {..i} \<subseteq> sets M" 

649 
using Q' by (auto intro: finite_UN) 

650 
with v.measure_finitely_subadditive[of "{.. i}" Q'] 

651 
have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

652 
also have "\<dots> < \<infinity>" using Q' by (simp add: setsum_Pinfty) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

653 
finally show "\<nu> (?O i) \<noteq> \<infinity>" by simp 
38656  654 
qed auto 
655 
have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp 

656 
have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric] 

657 
proof (rule antisym) 

658 
show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim 

659 
using Q' by (auto intro!: SUP_mono measure_mono finite_UN) 

660 
show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def 

661 
proof (safe intro!: Sup_mono, unfold bex_simps) 

662 
fix i 

663 
have *: "(\<Union>Q' ` {..i}) = ?O i" by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

664 
then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<infinity>) \<and> 
38656  665 
\<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x" 
666 
using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) 

667 
qed 

668 
qed 

669 
let "?O_0" = "(\<Union>i. ?O i)" 

670 
have "?O_0 \<in> sets M" using Q' by auto 

40859  671 
def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0  Suc n \<Rightarrow> ?O (Suc n)  ?O n" 
38656  672 
{ fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) } 
673 
note Q_sets = this 

40859  674 
show ?thesis 
675 
proof (intro bexI exI conjI ballI impI allI) 

676 
show "disjoint_family Q" 

677 
by (fastsimp simp: disjoint_family_on_def Q_def 

678 
split: nat.split_asm) 

679 
show "range Q \<subseteq> sets M" 

680 
using Q_sets by auto 

681 
{ fix A assume A: "A \<in> sets M" "A \<subseteq> space M  ?O_0" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

682 
show "\<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<infinity>" 
40859  683 
proof (rule disjCI, simp) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

684 
assume *: "0 < \<mu> A \<longrightarrow> \<nu> A \<noteq> \<infinity>" 
40859  685 
show "\<mu> A = 0 \<and> \<nu> A = 0" 
686 
proof cases 

687 
assume "\<mu> A = 0" moreover with ac A have "\<nu> A = 0" 

688 
unfolding absolutely_continuous_def by auto 

689 
ultimately show ?thesis by simp 

690 
next 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

691 
assume "\<mu> A \<noteq> 0" with * have "\<nu> A \<noteq> \<infinity>" using positive_measure[OF A(1)] by auto 
40859  692 
with A have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)" 
693 
using Q' by (auto intro!: measure_additive countable_UN) 

694 
also have "\<dots> = (SUP i. \<mu> (?O i \<union> A))" 

695 
proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified]) 

696 
show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

697 
using `\<nu> A \<noteq> \<infinity>` O_sets A by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

698 
qed (fastsimp intro!: incseq_SucI) 
40859  699 
also have "\<dots> \<le> ?a" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

700 
proof (safe intro!: SUP_leI) 
40859  701 
fix i have "?O i \<union> A \<in> ?Q" 
702 
proof (safe del: notI) 

703 
show "?O i \<union> A \<in> sets M" using O_sets A by auto 

704 
from O_in_G[of i] 

705 
moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A" 

706 
using v.measure_subadditive[of "?O i" A] A O_sets by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

707 
ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

708 
using `\<nu> A \<noteq> \<infinity>` by auto 
40859  709 
qed 
710 
then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI) 

711 
qed 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

712 
finally have "\<mu> A = 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

713 
unfolding a_eq using real_measure[OF `?O_0 \<in> sets M`] real_measure[OF A(1)] by auto 
40859  714 
with `\<mu> A \<noteq> 0` show ?thesis by auto 
715 
qed 

716 
qed } 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

717 
{ fix i show "\<nu> (Q i) \<noteq> \<infinity>" 
40859  718 
proof (cases i) 
719 
case 0 then show ?thesis 

720 
unfolding Q_def using Q'[of 0] by simp 

721 
next 

722 
case (Suc n) 

723 
then show ?thesis unfolding Q_def 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

724 
using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

725 
using v.measure_mono[OF O_mono, of n] v.positive_measure[of "?O n"] v.positive_measure[of "?O (Suc n)"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

726 
using v.measure_Diff[of "?O n" "?O (Suc n)", OF _ _ _ O_mono] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

727 
by (cases rule: extreal2_cases[of "\<nu> (\<Union> x\<le>Suc n. Q' x)" "\<nu> (\<Union> i\<le>n. Q' i)"]) auto 
40859  728 
qed } 
729 
show "space M  ?O_0 \<in> sets M" using Q'_sets by auto 

730 
{ fix j have "(\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q i)" 

731 
proof (induct j) 

732 
case 0 then show ?case by (simp add: Q_def) 

733 
next 

734 
case (Suc j) 

735 
have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp 

736 
have "{..j} \<union> {..Suc j} = {..Suc j}" by auto 

737 
then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)" 

738 
by (simp add: UN_Un[symmetric] Q_def del: UN_Un) 

739 
then show ?case using Suc by (auto simp add: eq atMost_Suc) 

740 
qed } 

741 
then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp 

742 
then show "space M  ?O_0 = space M  (\<Union>i. Q i)" by fastsimp 

743 
qed 

744 
qed 

745 

746 
lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

747 
assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?N") 
40859  748 
assumes "absolutely_continuous \<nu>" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

749 
shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> (\<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M))" 
40859  750 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

751 
interpret v: measure_space ?N 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

752 
where "space ?N = space M" and "sets ?N = sets M" and "measure ?N = \<nu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

753 
by fact auto 
40859  754 
from split_space_into_finite_sets_and_rest[OF assms] 
755 
obtain Q0 and Q :: "nat \<Rightarrow> 'a set" 

756 
where Q: "disjoint_family Q" "range Q \<subseteq> sets M" 

757 
and Q0: "Q0 \<in> sets M" "Q0 = space M  (\<Union>i. Q i)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

758 
and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

759 
and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<infinity>" by force 
40859  760 
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

761 
have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>x. 0 \<le> f x) \<and> (\<forall>A\<in>sets M. 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

762 
\<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x \<partial>M))" 
38656  763 
proof 
764 
fix i 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

765 
have indicator_eq: "\<And>f x A. (f x :: extreal) * indicator (Q i \<inter> A) x * indicator (Q i) x 
38656  766 
= (f x * indicator (Q i) x) * indicator A x" 
767 
unfolding indicator_def by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

768 
have fm: "finite_measure (restricted_space (Q i))" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

769 
(is "finite_measure ?R") by (rule restricted_finite_measure[OF Q_sets[of i]]) 
38656  770 
then interpret R: finite_measure ?R . 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

771 
have fmv: "finite_measure (restricted_space (Q i) \<lparr> measure := \<nu>\<rparr>)" (is "finite_measure ?Q") 
38656  772 
unfolding finite_measure_def finite_measure_axioms_def 
773 
proof 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

774 
show "measure_space ?Q" 
38656  775 
using v.restricted_measure_space Q_sets[of i] by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

776 
show "measure ?Q (space ?Q) \<noteq> \<infinity>" using Q_fin by simp 
38656  777 
qed 
778 
have "R.absolutely_continuous \<nu>" 

779 
using `absolutely_continuous \<nu>` `Q i \<in> sets M` 

780 
by (auto simp: R.absolutely_continuous_def absolutely_continuous_def) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

781 
from R.Radon_Nikodym_finite_measure[OF fmv this] 
38656  782 
obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

783 
and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. (f x * indicator (Q i) x) * indicator A x \<partial>M)" 
38656  784 
unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`] 
785 
positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

786 
then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>x. 0 \<le> f x) \<and> (\<forall>A\<in>sets M. 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

787 
\<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x \<partial>M))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

788 
by (auto intro!: exI[of _ "\<lambda>x. max 0 (f x * indicator (Q i) x)"] positive_integral_cong_pos 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

789 
split: split_indicator split_if_asm simp: max_def) 
38656  790 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

791 
from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x" 
38656  792 
and f: "\<And>A i. A \<in> sets M \<Longrightarrow> 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

793 
\<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)" 
38656  794 
by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

795 
let "?f x" = "(\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x" 
38656  796 
show ?thesis 
797 
proof (safe intro!: bexI[of _ ?f]) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

798 
show "?f \<in> borel_measurable M" using Q0 borel Q_sets 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

799 
by (auto intro!: measurable_If) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

800 
show "\<And>x. 0 \<le> ?f x" using borel by (auto intro!: suminf_0_le simp: indicator_def) 
38656  801 
fix A assume "A \<in> sets M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

802 
have Qi: "\<And>i. Q i \<in> sets M" using Q by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

803 
have [intro,simp]: "\<And>i. (\<lambda>x. f i x * indicator (Q i \<inter> A) x) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

804 
"\<And>i. AE x. 0 \<le> f i x * indicator (Q i \<inter> A) x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

805 
using borel Qi Q0(1) `A \<in> sets M` by (auto intro!: borel_measurable_extreal_times) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

806 
have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) + \<infinity> * indicator (Q0 \<inter> A) x \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

807 
using borel by (intro positive_integral_cong) (auto simp: indicator_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

808 
also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * \<mu> (Q0 \<inter> A)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

809 
using borel Qi Q0(1) `A \<in> sets M` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

810 
by (subst positive_integral_add) (auto simp del: extreal_infty_mult 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

811 
simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

812 
also have "\<dots> = (\<Sum>i. \<nu> (Q i \<inter> A)) + \<infinity> * \<mu> (Q0 \<inter> A)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

813 
by (subst f[OF `A \<in> sets M`], subst positive_integral_suminf) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

814 
finally have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. \<nu> (Q i \<inter> A)) + \<infinity> * \<mu> (Q0 \<inter> A)" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

815 
moreover have "(\<Sum>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)" 
40859  816 
using Q Q_sets `A \<in> sets M` 
817 
by (intro v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified]) 

818 
(auto simp: disjoint_family_on_def) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

819 
moreover have "\<infinity> * \<mu> (Q0 \<inter> A) = \<nu> (Q0 \<inter> A)" 
40859  820 
proof  
821 
have "Q0 \<inter> A \<in> sets M" using Q0(1) `A \<in> sets M` by blast 

822 
from in_Q0[OF this] show ?thesis by auto 

38656  823 
qed 
40859  824 
moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M" 
825 
using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN) 

826 
moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}" 

827 
using `A \<in> sets M` sets_into_space Q0 by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

828 
ultimately show "\<nu> A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)" 
40859  829 
using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"] 
830 
by simp 

38656  831 
qed 
832 
qed 

833 

834 
lemma (in sigma_finite_measure) Radon_Nikodym: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

835 
assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?N") 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

836 
assumes ac: "absolutely_continuous \<nu>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

837 
shows "\<exists>f \<in> borel_measurable M. (\<forall>x. 0 \<le> f x) \<and> (\<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M))" 
38656  838 
proof  
839 
from Ex_finite_integrable_function 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

840 
obtain h where finite: "integral\<^isup>P M h \<noteq> \<infinity>" and 
38656  841 
borel: "h \<in> borel_measurable M" and 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

842 
nn: "\<And>x. 0 \<le> h x" and 
38656  843 
pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

844 
"\<And>x. x \<in> space M \<Longrightarrow> h x < \<infinity>" by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

845 
let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

846 
let ?MT = "M\<lparr> measure := ?T \<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

847 
interpret T: finite_measure ?MT 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

848 
where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

849 
unfolding finite_measure_def finite_measure_axioms_def using borel finite nn 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

850 
by (auto intro!: measure_space_density cong: positive_integral_cong) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

851 
have "T.absolutely_continuous \<nu>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

852 
proof (unfold T.absolutely_continuous_def, safe) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

853 
fix N assume "N \<in> sets M" "(\<integral>\<^isup>+x. h x * indicator N x \<partial>M) = 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

854 
with borel ac pos have "AE x. x \<notin> N" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

855 
by (subst (asm) positive_integral_0_iff_AE) (auto split: split_indicator simp: not_le) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

856 
then have "N \<in> null_sets" using `N \<in> sets M` sets_into_space 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

857 
by (subst (asm) AE_iff_measurable[OF `N \<in> sets M`]) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

858 
then show "\<nu> N = 0" using ac by (auto simp: absolutely_continuous_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

859 
qed 
38656  860 
from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

861 
obtain f where f_borel: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

862 
fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>?MT)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

863 
by (auto simp: measurable_def) 
38656  864 
show ?thesis 
865 
proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"]) 

866 
show "(\<lambda>x. h x * f x) \<in> borel_measurable M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

867 
using borel f_borel by (auto intro: borel_measurable_extreal_times) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

868 
show "\<And>x. 0 \<le> h x * f x" using nn f_borel by auto 
38656  869 
fix A assume "A \<in> sets M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

870 
then show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

871 
unfolding fT[OF `A \<in> sets M`] mult_assoc using nn borel f_borel 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

872 
by (intro positive_integral_translated_density) auto 
38656  873 
qed 
874 
qed 

875 

40859  876 
section "Uniqueness of densities" 
877 

878 
lemma (in measure_space) finite_density_unique: 

879 
assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

880 
assumes pos: "AE x. 0 \<le> f x" "AE x. 0 \<le> g x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

881 
and fin: "integral\<^isup>P M f \<noteq> \<infinity>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

882 
shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. g x * indicator A x \<partial>M)) 
40859  883 
\<longleftrightarrow> (AE x. f x = g x)" 
884 
(is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _") 

885 
proof (intro iffI ballI) 

886 
fix A assume eq: "AE x. f x = g x" 

41705  887 
then show "?P f A = ?P g A" 
888 
by (auto intro: positive_integral_cong_AE) 

40859  889 
next 
890 
assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A" 

891 
from this[THEN bspec, OF top] fin 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

892 
have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong) 
40859  893 
{ fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

894 
and pos: "AE x. 0 \<le> f x" "AE x. 0 \<le> g x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

895 
and g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A" 
40859  896 
let ?N = "{x\<in>space M. g x < f x}" 
897 
have N: "?N \<in> sets M" using borel by simp 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

898 
have "?P g ?N \<le> integral\<^isup>P M g" using pos 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

899 
by (intro positive_integral_mono_AE) (auto split: split_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

900 
then have Pg_fin: "?P g ?N \<noteq> \<infinity>" using g_fin by auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

901 
have "?P (\<lambda>x. (f x  g x)) ?N = (\<integral>\<^isup>+x. f x * indicator ?N x  g x * indicator ?N x \<partial>M)" 
40859  902 
by (auto intro!: positive_integral_cong simp: indicator_def) 
903 
also have "\<dots> = ?P f ?N  ?P g ?N" 

904 
proof (rule positive_integral_diff) 

905 
show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M" 

906 
using borel N by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

907 
show "AE x. g x * indicator ?N x \<le> f x * indicator ?N x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

908 
"AE x. 0 \<le> g x * indicator ?N x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

909 
using pos by (auto split: split_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

910 
qed fact 
40859  911 
also have "\<dots> = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

912 
unfolding eq[THEN bspec, OF N] using positive_integral_positive Pg_fin by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

913 
finally have "AE x. f x \<le> g x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

914 
using pos borel positive_integral_PInf_AE[OF borel(2) g_fin] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

915 
by (subst (asm) positive_integral_0_iff_AE) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

916 
(auto split: split_indicator simp: not_less extreal_minus_le_iff) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

917 
from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

918 
show "AE x. f x = g x" by auto 
40859  919 
qed 
920 

921 
lemma (in finite_measure) density_unique_finite_measure: 

922 
assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

923 
assumes pos: "AE x. 0 \<le> f x" "AE x. 0 \<le> f' x" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

924 
assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. f' x * indicator A x \<partial>M)" 
40859  925 
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A") 
926 
shows "AE x. f x = f' x" 

927 
proof  

928 
let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A" 

929 
let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

930 
interpret M: measure_space "M\<lparr> measure := ?\<nu>\<rparr>" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

931 
using borel(1) pos(1) by (rule measure_space_density) simp 
40859  932 
have ac: "absolutely_continuous ?\<nu>" 
933 
using f by (rule density_is_absolutely_continuous) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

934 
from split_space_into_finite_sets_and_rest[OF `measure_space (M\<lparr> measure := ?\<nu>\<rparr>)` ac] 
40859  935 
obtain Q0 and Q :: "nat \<Rightarrow> 'a set" 
936 
where Q: "disjoint_family Q" "range Q \<subseteq> sets M" 

937 
and Q0: "Q0 \<in> sets M" "Q0 = space M  (\<Union>i. Q i)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

938 
and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> ?\<nu> A = 0 \<or> 0 < \<mu> A \<and> ?\<nu> A = \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

939 
and Q_fin: "\<And>i. ?\<nu> (Q i) \<noteq> \<infinity>" by force 
40859  940 
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto 
941 
let ?N = "{x\<in>space M. f x \<noteq> f' x}" 

942 
have "?N \<in> sets M" using borel by auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

943 
have *: "\<And>i x A. \<And>y::extreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x" 
40859  944 
unfolding indicator_def by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

945 
have "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos 
40859  946 
by (intro finite_density_unique[THEN iffD1] allI) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

947 
(auto intro!: borel_measurable_extreal_times f Int simp: *) 
41705  948 
moreover have "AE x. ?f Q0 x = ?f' Q0 x" 
40859  949 
proof (rule AE_I') 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

950 
{ fix f :: "'a \<Rightarrow> extreal" assume borel: "f \<in> borel_measurable M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

951 
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)" 
40859  952 
let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}" 
953 
have "(\<Union>i. ?A i) \<in> null_sets" 

954 
proof (rule null_sets_UN) 

955 
fix i have "?A i \<in> sets M" 

956 
using borel Q0(1) by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

957 
have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x \<partial>M)" 
40859  958 
unfolding eq[OF `?A i \<in> sets M`] 
959 
by (auto intro!: positive_integral_mono simp: indicator_def) 

960 
also have "\<dots> = of_nat i * \<mu> (?A i)" 

961 
using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

962 
also have "\<dots> < \<infinity>" 
40859  963 
using `?A i \<in> sets M`[THEN finite_measure] by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

964 
finally have "?\<nu> (?A i) \<noteq> \<infinity>" by simp 
40859  965 
then show "?A i \<in> null_sets" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto 
966 
qed 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

967 
also have "(\<Union>i. ?A i) = Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

968 
by (auto simp: less_PInf_Ex_of_nat real_eq_of_nat) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

969 
finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" by simp } 
40859  970 
from this[OF borel(1) refl] this[OF borel(2) f] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

971 
have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>} \<in> null_sets" by simp_all 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

972 
then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>}) \<in> null_sets" by (rule null_sets_Un) 
40859  973 
show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq> 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

974 
(Q0 \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<infinity>})" by (auto simp: indicator_def) 
40859  975 
qed 
41705  976 
moreover have "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow> 
40859  977 
?f (space M) x = ?f' (space M) x" 
978 
by (auto simp: indicator_def Q0) 

41705  979 
ultimately have "AE x. ?f (space M) x = ?f' (space M) x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

980 
by (auto simp: AE_all_countable[symmetric]) 
41705  981 
then show "AE x. f x = f' x" by auto 
40859  982 
qed 
983 

984 
lemma (in sigma_finite_measure) density_unique: 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

985 
assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

986 
assumes f': "f' \<in> borel_measurable M" "AE x. 0 \<le> f' x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

987 
assumes eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. f' x * indicator A x \<partial>M)" 
40859  988 
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A") 
989 
shows "AE x. f x = f' x" 

990 
proof  

991 
obtain h where h_borel: "h \<in> borel_measurable M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

992 
and fin: "integral\<^isup>P M h \<noteq> \<infinity>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<infinity>" "\<And>x. 0 \<le> h x" 
40859  993 
using Ex_finite_integrable_function by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

994 
then have h_nn: "AE x. 0 \<le> h x" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

995 
let ?H = "M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M) \<rparr>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

996 
have H: "measure_space ?H" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

997 
using h_borel h_nn by (rule measure_space_density) simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

998 
then interpret h: measure_space ?H . 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

999 
interpret h: finite_measure "M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M) \<rparr>" 
40859  1000 
by default (simp cong: positive_integral_cong add: fin) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1001 
let ?fM = "M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)\<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1002 
interpret f: measure_space ?fM 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1003 
using f by (rule measure_space_density) simp 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1004 
let ?f'M = "M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+x. f' x * indicator A x \<partial>M)\<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1005 
interpret f': measure_space ?f'M 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1006 
using f' by (rule measure_space_density) simp 
40859  1007 
{ fix A assume "A \<in> sets M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1008 
then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1009 
using pos(1) sets_into_space by (force simp: indicator_def) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1010 
then have "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1011 
using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto } 
40859  1012 
note h_null_sets = this 
1013 
{ fix A assume "A \<in> sets M" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1014 
have "(\<integral>\<^isup>+x. f x * (h x * indicator A x) \<partial>M) = (\<integral>\<^isup>+x. h x * indicator A x \<partial>?fM)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1015 
using `A \<in> sets M` h_borel h_nn f f' 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1016 
by (intro positive_integral_translated_density[symmetric]) auto 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1017 
also have "\<dots> = (\<integral>\<^isup>+x. h x * indicator A x \<partial>?f'M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1018 
by (rule f'.positive_integral_cong_measure) (simp_all add: eq) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1019 
also have "\<dots> = (\<integral>\<^isup>+x. f' x * (h x * indicator A x) \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1020 
using `A \<in> sets M` h_borel h_nn f f' 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1021 
by (intro positive_integral_translated_density) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1022 
finally have "(\<integral>\<^isup>+x. h x * (f x * indicator A x) \<partial>M) = (\<integral>\<^isup>+x. h x * (f' x * indicator A x) \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1023 
by (simp add: ac_simps) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1024 
then have "(\<integral>\<^isup>+x. (f x * indicator A x) \<partial>?H) = (\<integral>\<^isup>+x. (f' x * indicator A x) \<partial>?H)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1025 
using `A \<in> sets M` h_borel h_nn f f' 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1026 
by (subst (asm) (1 2) positive_integral_translated_density[symmetric]) auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1027 
then have "AE x in ?H. f x = f' x" using h_borel h_nn f f' 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1028 
by (intro h.density_unique_finite_measure absolutely_continuous_AE[OF H] density_is_absolutely_continuous) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1029 
simp_all 
40859  1030 
then show "AE x. f x = f' x" 
1031 
unfolding h.almost_everywhere_def almost_everywhere_def 

1032 
by (auto simp add: h_null_sets) 

1033 
qed 

1034 

1035 
lemma (in sigma_finite_measure) sigma_finite_iff_density_finite: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1036 
assumes \<nu>: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?N") 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1037 
and f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1038 
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1039 
shows "sigma_finite_measure (M\<lparr>measure := \<nu>\<rparr>) \<longleftrightarrow> (AE x. f x \<noteq> \<infinity>)" 
40859  1040 
proof 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1041 
assume "sigma_finite_measure ?N" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1042 
then interpret \<nu>: sigma_finite_measure ?N 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1043 
where "borel_measurable ?N = borel_measurable M" and "measure ?N = \<nu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1044 
and "sets ?N = sets M" and "space ?N = space M" by (auto simp: measurable_def) 
40859  1045 
from \<nu>.Ex_finite_integrable_function obtain h where 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1046 
h: "h \<in> borel_measurable M" "integral\<^isup>P ?N h \<noteq> \<infinity>" and 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1047 
h_nn: "\<And>x. 0 \<le> h x" and 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1048 
fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1049 
have "AE x. f x * h x \<noteq> \<infinity>" 
40859  1050 
proof (rule AE_I') 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1051 
have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)" using f h h_nn 
41705  1052 
by (subst \<nu>.positive_integral_cong_measure[symmetric, 
1053 
of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"]) 

1054 
(auto intro!: positive_integral_translated_density simp: eq) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1055 
then have "(\<integral>\<^isup>+x. f x * h x \<partial>M) \<noteq> \<infinity>" 
40859  1056 
using h(2) by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1057 
then show "(\<lambda>x. f x * h x) ` {\<infinity>} \<inter> space M \<in> null_sets" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1058 
using f h(1) by (auto intro!: positive_integral_PInf borel_measurable_vimage) 
40859  1059 
qed auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1060 
then show "AE x. f x \<noteq> \<infinity>" 
41705  1061 
using fin by (auto elim!: AE_Ball_mp) 
40859  1062 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1063 
assume AE: "AE x. f x \<noteq> \<infinity>" 
40859  1064 
from sigma_finite guess Q .. note Q = this 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1065 
interpret \<nu>: measure_space ?N 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1066 
where "borel_measurable ?N = borel_measurable M" and "measure ?N = \<nu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1067 
and "sets ?N = sets M" and "space ?N = space M" using \<nu> by (auto simp: measurable_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1068 
def A \<equiv> "\<lambda>i. f ` (case i of 0 \<Rightarrow> {\<infinity>}  Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M" 
40859  1069 
{ fix i j have "A i \<inter> Q j \<in> sets M" 
1070 
unfolding A_def using f Q 

1071 
apply (rule_tac Int) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1072 
by (cases i) (auto intro: measurable_sets[OF f(1)]) } 
40859  1073 
note A_in_sets = this 
1074 
let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j" 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1075 
show "sigma_finite_measure ?N" 
40859  1076 
proof (default, intro exI conjI subsetI allI) 
1077 
fix x assume "x \<in> range ?A" 

1078 
then obtain n where n: "x = ?A n" by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1079 
then show "x \<in> sets ?N" using A_in_sets by (cases "prod_decode n") auto 
40859  1080 
next 
1081 
have "(\<Union>i. ?A i) = (\<Union>i j. A i \<inter> Q j)" 

1082 
proof safe 

1083 
fix x i j assume "x \<in> A i" "x \<in> Q j" 

1084 
then show "x \<in> (\<Union>i. case prod_decode i of (i, j) \<Rightarrow> A i \<inter> Q j)" 

1085 
by (intro UN_I[of "prod_encode (i,j)"]) auto 

1086 
qed auto 

1087 
also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto 

1088 
also have "(\<Union>i. A i) = space M" 

1089 
proof safe 

1090 
fix x assume x: "x \<in> space M" 

1091 
show "x \<in> (\<Union>i. A i)" 

1092 
proof (cases "f x") 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1093 
case PInf with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0]) 
40859  1094 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1095 
case (real r) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1096 
with less_PInf_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by (auto simp: real_eq_of_nat) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1097 
then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1098 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1099 
case MInf with x show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1100 
unfolding A_def by (auto intro!: exI[of _ "Suc 0"]) 
40859  1101 
qed 
1102 
qed (auto simp: A_def) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1103 
finally show "(\<Union>i. ?A i) = space ?N" by simp 
40859  1104 
next 
1105 
fix n obtain i j where 

1106 
[simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1107 
have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<noteq> \<infinity>" 
40859  1108 
proof (cases i) 
1109 
case 0 

1110 
have "AE x. f x * indicator (A i \<inter> Q j) x = 0" 

41705  1111 
using AE by (auto simp: A_def `i = 0`) 
1112 
from positive_integral_cong_AE[OF this] show ?thesis by simp 

40859  1113 
next 
1114 
case (Suc n) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1115 
then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le> 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1116 
(\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x \<partial>M)" 
40859  1117 
by (auto intro!: positive_integral_mono simp: indicator_def A_def) 
1118 
also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)" 

1119 
using Q by (auto intro!: positive_integral_cmult_indicator) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1120 
also have "\<dots> < \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1121 
using Q by (auto simp: real_eq_of_nat[symmetric]) 
40859  1122 
finally show ?thesis by simp 
1123 
qed 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1124 
then show "measure ?N (?A n) \<noteq> \<infinity>" 
40859  1125 
using A_in_sets Q eq by auto 
1126 
qed 

1127 
qed 

1128 

40871  1129 
section "RadonNikodym derivative" 
38656  1130 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1131 
definition 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1132 
"RN_deriv M \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and> (\<forall>x. 0 \<le> f x) \<and> 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1133 
(\<forall>A \<in> sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M))" 
38656  1134 

40859  1135 
lemma (in sigma_finite_measure) RN_deriv_cong: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1136 
assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> measure M' A = \<mu> A" "sets M' = sets M" "space M' = space M" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1137 
and \<nu>: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1138 
shows "RN_deriv M' \<nu>' x = RN_deriv M \<nu> x" 
40859  1139 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1140 
interpret \<mu>': sigma_finite_measure M' 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1141 
using cong by (rule sigma_finite_measure_cong) 
40859  1142 
show ?thesis 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1143 
unfolding RN_deriv_def 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1144 
by (simp add: cong \<nu> positive_integral_cong_measure[OF cong] measurable_def) 
40859  1145 
qed 
1146 

38656  1147 
lemma (in sigma_finite_measure) RN_deriv: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1148 
assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" 
38656  1149 
assumes "absolutely_continuous \<nu>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1150 
shows "RN_deriv M \<nu> \<in> borel_measurable M" (is ?borel) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1151 
and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. RN_deriv M \<nu> x * indicator A x \<partial>M)" 
38656  1152 
(is "\<And>A. _ \<Longrightarrow> ?int A") 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1153 
and "0 \<le> RN_deriv M \<nu> x" 
38656  1154 
proof  
1155 
note Ex = Radon_Nikodym[OF assms, unfolded Bex_def] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1156 
then show ?borel unfolding RN_deriv_def by (rule someI2_ex) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1157 
from Ex show "0 \<le> RN_deriv M \<nu> x" unfolding RN_deriv_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1158 
by (rule someI2_ex) simp 
38656  1159 
fix A assume "A \<in> sets M" 
1160 
from Ex show "?int A" unfolding RN_deriv_def 

1161 
by (rule someI2_ex) (simp add: `A \<in> sets M`) 

1162 
qed 

1163 

40859  1164 
lemma (in sigma_finite_measure) RN_deriv_positive_integral: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1165 
assumes \<nu>: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" "absolutely_continuous \<nu>" 
40859  1166 
and f: "f \<in> borel_measurable M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1167 
shows "integral\<^isup>P (M\<lparr>measure := \<nu>\<rparr>) f = (\<integral>\<^isup>+x. RN_deriv M \<nu> x * f x \<partial>M)" 
40859  1168 
proof  
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1169 
interpret \<nu>: measure_space "M\<lparr>measure := \<nu>\<rparr>" by fact 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1170 
note RN = RN_deriv[OF \<nu>] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1171 
have "integral\<^isup>P (M\<lparr>measure := \<nu>\<rparr>) f = (\<integral>\<^isup>+x. max 0 (f x) \<partial>M\<lparr>measure := \<nu>\<rparr>)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1172 
unfolding positive_integral_max_0 .. 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1173 
also have "(\<integral>\<^isup>+x. max 0 (f x) \<partial>M\<lparr>measure := \<nu>\<rparr>) = 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1174 
(\<integral>\<^isup>+x. max 0 (f x) \<partial>M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+x. RN_deriv M \<nu> x * indicator A x \<partial>M)\<rparr>)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1175 
by (intro \<nu>.positive_integral_cong_measure[symmetric]) (simp_all add: RN(2)) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1176 
also have "\<dots> = (\<integral>\<^isup>+x. RN_deriv M \<nu> x * max 0 (f x) \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1177 
by (intro positive_integral_translated_density) (auto simp add: RN f) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1178 
also have "\<dots> = (\<integral>\<^isup>+x. RN_deriv M \<nu> x * f x \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1179 
using RN_deriv(3)[OF \<nu>] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1180 
by (auto intro!: positive_integral_cong_pos split: split_if_asm 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41832
diff
changeset

1181 
simp: max_def extreal_mult_le_0_iff) 
40859  1182 
finally show ?thesis . 
1183 
qed 

1184 

1185 
lemma (in sigma_finite_measure) RN_deriv_unique: 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1186 
assumes \<nu>: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" "absolutely_continuous \<nu>" 