author  hoelzl 
Wed, 08 Dec 2010 19:32:11 +0100  
changeset 41097  a1abfa4e2b44 
parent 41095  c335d880ff82 
child 41544  c3b977fee8a3 
permissions  rwrr 
38656  1 
theory Radon_Nikodym 
2 
imports Lebesgue_Integration 

3 
begin 

4 

40859  5 
lemma less_\<omega>_Ex_of_nat: "x < \<omega> \<longleftrightarrow> (\<exists>n. x < of_nat n)" 
6 
proof safe 

7 
assume "x < \<omega>" 

8 
then obtain r where "0 \<le> r" "x = Real r" by (cases x) auto 

9 
moreover obtain n where "r < of_nat n" using ex_less_of_nat by auto 

10 
ultimately show "\<exists>n. x < of_nat n" by (auto simp: real_eq_of_nat) 

11 
qed auto 

12 

38656  13 
lemma (in sigma_finite_measure) Ex_finite_integrable_function: 
14 
shows "\<exists>h\<in>borel_measurable M. positive_integral h \<noteq> \<omega> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>)" 

15 
proof  

16 
obtain A :: "nat \<Rightarrow> 'a set" where 

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

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

19 
measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and 

20 
disjoint: "disjoint_family A" 

21 
using disjoint_sigma_finite by auto 

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

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

24 
proof 

25 
fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)" 

26 
proof cases 

27 
assume "\<mu> (A i) = 0" 

28 
then show ?thesis by (auto intro!: exI[of _ 1]) 

29 
next 

30 
assume not_0: "\<mu> (A i) \<noteq> 0" 

31 
then have "?B i \<noteq> \<omega>" using measure[of i] by auto 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

32 
then have "inverse (?B i) \<noteq> 0" unfolding pextreal_inverse_eq_0 by simp 
38656  33 
then show ?thesis using measure[of i] not_0 
34 
by (auto intro!: exI[of _ "inverse (?B i) / 2"] 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

35 
simp: pextreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq) 
38656  36 
qed 
37 
qed 

38 
from choice[OF this] obtain n where n: "\<And>i. 0 < n i" 

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

40 
let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x" 

41 
show ?thesis 

42 
proof (safe intro!: bexI[of _ ?h] del: notI) 

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

45 
then have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))" 

46 
by (simp add: positive_integral_psuminf positive_integral_cmult_indicator) 

38656  47 
also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))" 
48 
proof (rule psuminf_le) 

49 
fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)" 

50 
using measure[of N] n[of N] 

39092  51 
by (cases "n N") 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

52 
(auto simp: pextreal_noteq_omega_Ex field_simps zero_le_mult_iff 
39092  53 
mult_le_0_iff mult_less_0_iff power_less_zero_eq 
54 
power_le_zero_eq inverse_eq_divide less_divide_eq 

55 
power_divide split: split_if_asm) 

38656  56 
qed 
57 
also have "\<dots> = Real 1" 

58 
by (rule suminf_imp_psuminf, rule power_half_series, auto) 

59 
finally show "positive_integral ?h \<noteq> \<omega>" by auto 

60 
next 

61 
fix x assume "x \<in> space M" 

62 
then obtain i where "x \<in> A i" using space[symmetric] by auto 

63 
from psuminf_cmult_indicator[OF disjoint, OF this] 

64 
have "?h x = n i" by simp 

65 
then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto 

66 
next 

67 
show "?h \<in> borel_measurable M" using range 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

68 
by (auto intro!: borel_measurable_psuminf borel_measurable_pextreal_times) 
38656  69 
qed 
70 
qed 

71 

40871  72 
subsection "Absolutely continuous" 
73 

38656  74 
definition (in measure_space) 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

75 
"absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pextreal))" 
38656  76 

40859  77 
lemma (in sigma_finite_measure) absolutely_continuous_AE: 
78 
assumes "measure_space M \<nu>" "absolutely_continuous \<nu>" "AE x. P x" 

79 
shows "measure_space.almost_everywhere M \<nu> P" 

80 
proof  

81 
interpret \<nu>: measure_space M \<nu> by fact 

82 
from `AE x. P x` obtain N where N: "N \<in> null_sets" and "{x\<in>space M. \<not> P x} \<subseteq> N" 

83 
unfolding almost_everywhere_def by auto 

84 
show "\<nu>.almost_everywhere P" 

85 
proof (rule \<nu>.AE_I') 

86 
show "{x\<in>space M. \<not> P x} \<subseteq> N" by fact 

87 
from `absolutely_continuous \<nu>` show "N \<in> \<nu>.null_sets" 

88 
using N unfolding absolutely_continuous_def by auto 

89 
qed 

90 
qed 

91 

39097  92 
lemma (in finite_measure_space) absolutely_continuousI: 
93 
assumes "finite_measure_space M \<nu>" 

94 
assumes v: "\<And>x. \<lbrakk> x \<in> space M ; \<mu> {x} = 0 \<rbrakk> \<Longrightarrow> \<nu> {x} = 0" 

95 
shows "absolutely_continuous \<nu>" 

96 
proof (unfold absolutely_continuous_def sets_eq_Pow, safe) 

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

98 
interpret v: finite_measure_space M \<nu> by fact 

99 
have "\<nu> N = \<nu> (\<Union>x\<in>N. {x})" by simp 

100 
also have "\<dots> = (\<Sum>x\<in>N. \<nu> {x})" 

101 
proof (rule v.measure_finitely_additive''[symmetric]) 

102 
show "finite N" using `N \<subseteq> space M` finite_space by (auto intro: finite_subset) 

103 
show "disjoint_family_on (\<lambda>i. {i}) N" unfolding disjoint_family_on_def by auto 

104 
fix x assume "x \<in> N" thus "{x} \<in> sets M" using `N \<subseteq> space M` sets_eq_Pow by auto 

105 
qed 

106 
also have "\<dots> = 0" 

107 
proof (safe intro!: setsum_0') 

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

109 
hence "\<mu> {x} \<le> \<mu> N" using sets_eq_Pow `N \<subseteq> space M` by (auto intro!: measure_mono) 

110 
hence "\<mu> {x} = 0" using `\<mu> N = 0` by simp 

111 
thus "\<nu> {x} = 0" using v[of x] `x \<in> N` `N \<subseteq> space M` by auto 

112 
qed 

113 
finally show "\<nu> N = 0" . 

114 
qed 

115 

40871  116 
lemma (in measure_space) density_is_absolutely_continuous: 
117 
assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

118 
shows "absolutely_continuous \<nu>" 

119 
using assms unfolding absolutely_continuous_def 

120 
by (simp add: positive_integral_null_set) 

121 

122 
subsection "Existence of the RadonNikodym derivative" 

123 

38656  124 
lemma (in finite_measure) Radon_Nikodym_aux_epsilon: 
125 
fixes e :: real assumes "0 < e" 

126 
assumes "finite_measure M s" 

127 
shows "\<exists>A\<in>sets M. real (\<mu> (space M))  real (s (space M)) \<le> 

128 
real (\<mu> A)  real (s A) \<and> 

129 
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow>  e < real (\<mu> B)  real (s B))" 

130 
proof  

131 
let "?d A" = "real (\<mu> A)  real (s A)" 

132 
interpret M': finite_measure M s by fact 

133 
let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M  A \<longrightarrow> e < ?d B) 

134 
then {} 

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

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

137 
have A_simps[simp]: 

138 
"A 0 = {}" 

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

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

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

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

143 
note A'_in_sets = this 

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

145 
proof (induct n) 

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

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

148 
qed (simp add: A_def) } 

149 
note A_in_sets = this 

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

151 
{ fix n B 

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

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

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

155 
proof (rule someI2_ex[OF Ex]) 

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

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

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

159 
using `A n \<in> sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp 

160 
also have "\<dots> \<le> ?d (A n)  e" using dB by simp 

161 
finally show "?d (A n \<union> B) \<le> ?d (A n)  e" . 

162 
qed } 

163 
note dA_epsilon = this 

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

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

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

167 
next 

168 
case False 

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

170 
thus ?thesis by simp 

171 
qed } 

172 
note dA_mono = this 

173 
show ?thesis 

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

175 
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 

176 
show ?thesis 

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

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

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

180 
next 

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

182 
next 

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

184 
proof (induct n) 

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

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

187 
using A_in_sets sets_into_space dA_mono[of n] 

188 
real_finite_measure_Diff[of "space M"] 

189 
real_finite_measure_Diff[of "space M"] 

190 
M'.real_finite_measure_Diff[of "space M"] 

191 
M'.real_finite_measure_Diff[of "space M"] 

192 
by (simp del: A_simps) 

193 
finally show "?d (space M) \<le> ?d (space M  A (Suc n))" . 

194 
qed simp 

195 
qed 

196 
next 

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

198 
by (auto simp add: not_less) 

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

200 
proof (induct n) 

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

202 
qed simp } note dA_less = this 

203 
have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq 

204 
proof (rule incseq_SucI) 

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

206 
qed 

207 
from real_finite_continuity_from_below[of A] `range A \<subseteq> sets M` 

208 
M'.real_finite_continuity_from_below[of A] 

209 
have convergent: "(\<lambda>i. ?d (A i)) > ?d (\<Union>i. A i)" 

210 
by (auto intro!: LIMSEQ_diff) 

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

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

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

214 
ultimately show ?thesis by auto 

215 
qed 

216 
qed 

217 

218 
lemma (in finite_measure) Radon_Nikodym_aux: 

219 
assumes "finite_measure M s" 

220 
shows "\<exists>A\<in>sets M. real (\<mu> (space M))  real (s (space M)) \<le> 

221 
real (\<mu> A)  real (s A) \<and> 

222 
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> real (\<mu> B)  real (s B))" 

223 
proof  

224 
let "?d A" = "real (\<mu> A)  real (s A)" 

225 
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)" 

226 
interpret M': finite_measure M s by fact 

39092  227 
let "?r S" = "restricted_space S" 
38656  228 
{ fix S n 
229 
assume S: "S \<in> sets M" 

230 
hence **: "\<And>X. X \<in> op \<inter> S ` sets M \<longleftrightarrow> X \<in> sets M \<and> X \<subseteq> S" by auto 

231 
from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S 

232 
have "finite_measure (?r S) \<mu>" "0 < 1 / real (Suc n)" 

233 
"finite_measure (?r S) s" by auto 

234 
from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. 

235 
hence "?P X S n" 

236 
proof (simp add: **, safe) 

237 
fix C assume C: "C \<in> sets M" "C \<subseteq> X" "X \<subseteq> S" and 

238 
*: "\<forall>B\<in>sets M. S \<inter> B \<subseteq> X \<longrightarrow>  (1 / real (Suc n)) < ?d (S \<inter> B)" 

239 
hence "C \<subseteq> S" "C \<subseteq> X" "S \<inter> C = C" by auto 

240 
with *[THEN bspec, OF `C \<in> sets M`] 

241 
show " (1 / real (Suc n)) < ?d C" by auto 

242 
qed 

243 
hence "\<exists>A. ?P A S n" by auto } 

244 
note Ex_P = this 

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

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

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

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

249 
proof (induct i) 

250 
case (Suc i) 

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

252 
by (rule someI2_ex) simp 

253 
qed simp } 

254 
note A_in_sets = this 

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

256 
using Ex_P[OF A_in_sets] unfolding A_Suc 

257 
by (rule someI2_ex) simp } 

258 
note P_A = this 

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

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

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

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

263 
using P_A by auto 

264 
show ?thesis 

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

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

267 
from `range A \<subseteq> sets M` A_mono 

268 
real_finite_continuity_from_above[of A] 

269 
M'.real_finite_continuity_from_above[of A] 

270 
have "(\<lambda>i. ?d (A i)) > ?d (\<Inter>i. A i)" by (auto intro!: LIMSEQ_diff) 

271 
thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _] 

272 
by (rule_tac LIMSEQ_le_const) (auto intro!: exI) 

273 
next 

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

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

276 
proof (rule ccontr) 

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

278 
hence "0 <  ?d B" by auto 

279 
from ex_inverse_of_nat_Suc_less[OF this] 

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

281 
by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) 

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

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

284 
show False by auto 

285 
qed 

286 
qed 

287 
qed 

288 

289 
lemma (in finite_measure) Radon_Nikodym_finite_measure: 

290 
assumes "finite_measure M \<nu>" 

291 
assumes "absolutely_continuous \<nu>" 

292 
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

293 
proof  

294 
interpret M': finite_measure M \<nu> using assms(1) . 

295 
def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}" 

296 
have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto 

297 
hence "G \<noteq> {}" by auto 

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

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

300 
proof safe 

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

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

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

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

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

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

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

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

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

310 
by (auto simp: indicator_def max_def) 

311 
hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) = 

312 
positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) + 

313 
positive_integral (\<lambda>x. f x * indicator ((space M  ?A) \<inter> A) x)" 

314 
using f g sets unfolding G_def 

315 
by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator) 

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

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

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

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

320 
finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" . 

321 
qed } 

322 
note max_in_G = this 

323 
{ fix f g assume "f \<up> g" and f: "\<And>i. f i \<in> G" 

324 
have "g \<in> G" unfolding G_def 

325 
proof safe 

41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41095
diff
changeset

326 
from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)" 
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41095
diff
changeset

327 
unfolding isoton_def fun_eq_iff SUPR_apply by simp 
38656  328 
have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp 
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41095
diff
changeset

329 
thus "g \<in> borel_measurable M" by auto 
38656  330 
fix A assume "A \<in> sets M" 
331 
hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M" 

332 
using f_borel by (auto intro!: borel_measurable_indicator) 

333 
from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this] 

334 
have SUP: "positive_integral (\<lambda>x. g x * indicator A x) = 

335 
(SUP i. positive_integral (\<lambda>x. f i x * indicator A x))" 

336 
unfolding isoton_def by simp 

337 
show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP 

338 
using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI) 

339 
qed } 

340 
note SUP_in_G = this 

341 
let ?y = "SUP g : G. positive_integral g" 

342 
have "?y \<le> \<nu> (space M)" unfolding G_def 

343 
proof (safe intro!: SUP_leI) 

344 
fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" 

345 
from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)" 

346 
by (simp cong: positive_integral_cong) 

347 
qed 

348 
hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto 

349 
from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this 

350 
hence "\<forall>n. \<exists>g. g\<in>G \<and> positive_integral g = ys n" 

351 
proof safe 

352 
fix n assume "range ys \<subseteq> positive_integral ` G" 

353 
hence "ys n \<in> positive_integral ` G" by auto 

354 
thus "\<exists>g. g\<in>G \<and> positive_integral g = ys n" by auto 

355 
qed 

356 
from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. positive_integral (gs n) = ys n" by auto 

357 
hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto 

358 
let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})" 

359 
def f \<equiv> "SUP i. ?g i" 

360 
have gs_not_empty: "\<And>i. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto 

361 
{ fix i have "?g i \<in> G" 

362 
proof (induct i) 

363 
case 0 thus ?case by simp fact 

364 
next 

365 
case (Suc i) 

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

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

368 
qed } 

369 
note g_in_G = this 

370 
have "\<And>x. \<forall>i. ?g i x \<le> ?g (Suc i) x" 

371 
using gs_not_empty by (simp add: atMost_Suc) 

372 
hence isoton_g: "?g \<up> f" by (simp add: isoton_def le_fun_def f_def) 

373 
from SUP_in_G[OF this g_in_G] have "f \<in> G" . 

374 
hence [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto 

375 
have "(\<lambda>i. positive_integral (?g i)) \<up> positive_integral f" 

376 
using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def) 

377 
hence "positive_integral f = (SUP i. positive_integral (?g i))" 

378 
unfolding isoton_def by simp 

379 
also have "\<dots> = ?y" 

380 
proof (rule antisym) 

381 
show "(SUP i. positive_integral (?g i)) \<le> ?y" 

382 
using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def) 

383 
show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq 

384 
by (auto intro!: SUP_mono positive_integral_mono Max_ge) 

385 
qed 

386 
finally have int_f_eq_y: "positive_integral f = ?y" . 

387 
let "?t A" = "\<nu> A  positive_integral (\<lambda>x. f x * indicator A x)" 

388 
have "finite_measure M ?t" 

389 
proof 

390 
show "?t {} = 0" by simp 

391 
show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp 

392 
show "countably_additive M ?t" unfolding countably_additive_def 

393 
proof safe 

394 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" 

395 
have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x)) 

396 
= positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))" 

397 
using `range A \<subseteq> sets M` 

398 
by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator) 

399 
also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" 

400 
apply (rule positive_integral_cong) 

401 
apply (subst psuminf_cmult_right) 

402 
unfolding psuminf_indicator[OF `disjoint_family A`] .. 

403 
finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x)) 

404 
= positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" . 

405 
moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)" 

406 
using M'.measure_countably_additive A by (simp add: comp_def) 

407 
moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)" 

408 
using A `f \<in> G` unfolding G_def by auto 

409 
moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN) 

410 
moreover { 

411 
have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)" 

412 
using A `f \<in> G` unfolding G_def by (auto simp: countable_UN) 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

413 
also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>) 
38656  414 
finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>" 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

415 
by (simp add: pextreal_less_\<omega>) } 
38656  416 
ultimately 
417 
show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)" 

418 
apply (subst psuminf_minus) by simp_all 

419 
qed 

420 
qed 

421 
then interpret M: finite_measure M ?t . 

422 
have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto 

423 
have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0" 

424 
proof (rule ccontr) 

425 
assume "\<not> ?thesis" 

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

427 
by (auto simp: not_le) 

428 
note pos 

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

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

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

432 
moreover 

433 
hence pos_M: "0 < \<mu> (space M)" 

434 
using ac top unfolding absolutely_continuous_def by auto 

435 
moreover 

436 
have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)" 

437 
using `f \<in> G` unfolding G_def by auto 

438 
hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>" 

439 
using M'.finite_measure_of_space by auto 

440 
moreover 

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

442 
ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>" 

443 
using M'.finite_measure_of_space 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

444 
by (auto simp: pextreal_inverse_eq_0 finite_measure_of_space) 
38656  445 
have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b") 
446 
proof 

447 
show "?b {} = 0" by simp 

448 
show "?b (space M) \<noteq> \<omega>" using finite_measure_of_space b by auto 

449 
show "countably_additive M ?b" 

450 
unfolding countably_additive_def psuminf_cmult_right 

451 
using measure_countably_additive by auto 

452 
qed 

453 
from M.Radon_Nikodym_aux[OF this] 

454 
obtain A0 where "A0 \<in> sets M" and 

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

456 
*: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B)  real (b * \<mu> B)" by auto 

457 
{ fix B assume "B \<in> sets M" "B \<subseteq> A0" 

458 
with *[OF this] have "b * \<mu> B \<le> ?t B" 

459 
using M'.finite_measure b finite_measure 

460 
by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) } 

461 
note bM_le_t = this 

462 
let "?f0 x" = "f x + b * indicator A0 x" 

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

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

465 
have "positive_integral (\<lambda>x. ?f0 x * indicator A x) = 

466 
positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)" 

467 
by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith) 

468 
hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) = 

469 
positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)" 

470 
using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A 

471 
by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) } 

472 
note f0_eq = this 

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

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

475 
have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A" 

476 
using `f \<in> G` A unfolding G_def by auto 

477 
note f0_eq[OF A] 

478 
also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le> 

479 
positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)" 

480 
using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M` 

481 
by (auto intro!: add_left_mono) 

482 
also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A" 

483 
using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`] 

484 
by (auto intro!: add_left_mono) 

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

486 
using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`] 

487 
by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto) 

488 
finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . } 

489 
hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

490 
by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times) 
38656  491 
have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>" 
492 
"b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>" 

493 
using `A0 \<in> sets M` b 

494 
finite_measure[of A0] M.finite_measure[of A0] 

495 
finite_measure_of_space M.finite_measure_of_space 

496 
by auto 

497 
have int_f_finite: "positive_integral f \<noteq> \<omega>" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

498 
using M'.finite_measure_of_space pos_t unfolding pextreal_zero_less_diff_iff 
38656  499 
by (auto cong: positive_integral_cong) 
500 
have "?t (space M) > b * \<mu> (space M)" unfolding b_def 

501 
apply (simp add: field_simps) 

502 
apply (subst mult_assoc[symmetric]) 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

503 
apply (subst pextreal_mult_inverse) 
38656  504 
using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

505 
using pextreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"] 
38656  506 
by simp_all 
507 
hence "0 < ?t (space M)  b * \<mu> (space M)" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

508 
by (simp add: pextreal_zero_less_diff_iff) 
38656  509 
also have "\<dots> \<le> ?t A0  b * \<mu> A0" 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

510 
using space_less_A0 pos_M pos_t b real[unfolded pextreal_noteq_omega_Ex] by auto 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

511 
finally have "b * \<mu> A0 < ?t A0" unfolding pextreal_zero_less_diff_iff . 
38656  512 
hence "0 < ?t A0" by auto 
513 
hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def 

514 
using `A0 \<in> sets M` by auto 

515 
hence "0 < b * \<mu> A0" using b by auto 

516 
from int_f_finite this 

517 
have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

518 
by (rule pextreal_less_add) 
38656  519 
also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space 
520 
by (simp cong: positive_integral_cong) 

521 
finally have "?y < positive_integral ?f0" by simp 

522 
moreover from `?f0 \<in> G` have "positive_integral ?f0 \<le> ?y" by (auto intro!: le_SUPI) 

523 
ultimately show False by auto 

524 
qed 

525 
show ?thesis 

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

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

528 
show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

529 
proof (rule antisym) 

530 
show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A" 

531 
using `f \<in> G` `A \<in> sets M` unfolding G_def by auto 

532 
show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)" 

533 
using upper_bound[THEN bspec, OF `A \<in> sets M`] 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

534 
by (simp add: pextreal_zero_le_diff) 
38656  535 
qed 
536 
qed simp 

537 
qed 

538 

40859  539 
lemma (in finite_measure) split_space_into_finite_sets_and_rest: 
38656  540 
assumes "measure_space M \<nu>" 
40859  541 
assumes ac: "absolutely_continuous \<nu>" 
542 
shows "\<exists>\<Omega>0\<in>sets M. \<exists>\<Omega>::nat\<Rightarrow>'a set. disjoint_family \<Omega> \<and> range \<Omega> \<subseteq> sets M \<and> \<Omega>0 = space M  (\<Union>i. \<Omega> i) \<and> 

543 
(\<forall>A\<in>sets M. A \<subseteq> \<Omega>0 \<longrightarrow> (\<mu> A = 0 \<and> \<nu> A = 0) \<or> (\<mu> A > 0 \<and> \<nu> A = \<omega>)) \<and> 

544 
(\<forall>i. \<nu> (\<Omega> i) \<noteq> \<omega>)" 

38656  545 
proof  
546 
interpret v: measure_space M \<nu> by fact 

547 
let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<omega>}" 

548 
let ?a = "SUP Q:?Q. \<mu> Q" 

549 
have "{} \<in> ?Q" using v.empty_measure by auto 

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

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

552 
by (auto intro!: SUP_leI measure_mono top) 

553 
then have "?a \<noteq> \<omega>" using finite_measure_of_space 

554 
by auto 

555 
from SUPR_countable_SUPR[OF this Q_not_empty] 

556 
obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)" 

557 
by auto 

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

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

560 
by auto 

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

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

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

564 
proof (rule continuity_from_below[of ?O]) 

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

566 
show "\<And>i. ?O i \<subseteq> ?O (Suc i)" by fastsimp 

567 
qed 

568 
have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto 

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

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

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

572 
proof (safe del: notI) 

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

574 
using Q' by (auto intro: finite_UN) 

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

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

577 
also have "\<dots> < \<omega>" unfolding setsum_\<omega> pextreal_less_\<omega> using Q' by auto 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

578 
finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pextreal_less_\<omega> by auto 
38656  579 
qed auto 
580 
have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp 

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

582 
proof (rule antisym) 

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

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

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

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

587 
fix i 

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

589 
then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<omega>) \<and> 

590 
\<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x" 

591 
using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) 

592 
qed 

593 
qed 

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

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

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

40859  599 
show ?thesis 
600 
proof (intro bexI exI conjI ballI impI allI) 

601 
show "disjoint_family Q" 

602 
by (fastsimp simp: disjoint_family_on_def Q_def 

603 
split: nat.split_asm) 

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

605 
using Q_sets by auto 

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

607 
show "\<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>" 

608 
proof (rule disjCI, simp) 

609 
assume *: "0 < \<mu> A \<longrightarrow> \<nu> A \<noteq> \<omega>" 

610 
show "\<mu> A = 0 \<and> \<nu> A = 0" 

611 
proof cases 

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

613 
unfolding absolutely_continuous_def by auto 

614 
ultimately show ?thesis by simp 

615 
next 

616 
assume "\<mu> A \<noteq> 0" with * have "\<nu> A \<noteq> \<omega>" by auto 

617 
with A have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)" 

618 
using Q' by (auto intro!: measure_additive countable_UN) 

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

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

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

622 
using `\<nu> A \<noteq> \<omega>` O_sets A by auto 

623 
qed fastsimp 

624 
also have "\<dots> \<le> ?a" 

625 
proof (safe intro!: SUPR_bound) 

626 
fix i have "?O i \<union> A \<in> ?Q" 

627 
proof (safe del: notI) 

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

629 
from O_in_G[of i] 

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

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

632 
ultimately show "\<nu> (?O i \<union> A) \<noteq> \<omega>" 

633 
using `\<nu> A \<noteq> \<omega>` by auto 

634 
qed 

635 
then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI) 

636 
qed 

637 
finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`] 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

638 
by (cases "\<mu> A") (auto simp: pextreal_noteq_omega_Ex) 
40859  639 
with `\<mu> A \<noteq> 0` show ?thesis by auto 
640 
qed 

641 
qed } 

642 
{ fix i show "\<nu> (Q i) \<noteq> \<omega>" 

643 
proof (cases i) 

644 
case 0 then show ?thesis 

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

646 
next 

647 
case (Suc n) 

648 
then show ?thesis unfolding Q_def 

649 
using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` O_mono 

650 
using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto 

651 
qed } 

652 
show "space M  ?O_0 \<in> sets M" using Q'_sets by auto 

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

654 
proof (induct j) 

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

656 
next 

657 
case (Suc j) 

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

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

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

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

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

663 
qed } 

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

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

666 
qed 

667 
qed 

668 

669 
lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: 

670 
assumes "measure_space M \<nu>" 

671 
assumes "absolutely_continuous \<nu>" 

672 
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

673 
proof  

674 
interpret v: measure_space M \<nu> by fact 

675 
from split_space_into_finite_sets_and_rest[OF assms] 

676 
obtain Q0 and Q :: "nat \<Rightarrow> 'a set" 

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

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

679 
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 = \<omega>" 

680 
and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force 

681 
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto 

38656  682 
have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M. 
683 
\<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))" 

684 
proof 

685 
fix i 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

686 
have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x 
38656  687 
= (f x * indicator (Q i) x) * indicator A x" 
688 
unfolding indicator_def by auto 

39092  689 
have fm: "finite_measure (restricted_space (Q i)) \<mu>" 
38656  690 
(is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]]) 
691 
then interpret R: finite_measure ?R . 

692 
have fmv: "finite_measure ?R \<nu>" 

693 
unfolding finite_measure_def finite_measure_axioms_def 

694 
proof 

695 
show "measure_space ?R \<nu>" 

696 
using v.restricted_measure_space Q_sets[of i] by auto 

697 
show "\<nu> (space ?R) \<noteq> \<omega>" 

40859  698 
using Q_fin by simp 
38656  699 
qed 
700 
have "R.absolutely_continuous \<nu>" 

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

702 
by (auto simp: R.absolutely_continuous_def absolutely_continuous_def) 

703 
from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this] 

704 
obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M" 

705 
and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)" 

706 
unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`] 

707 
positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq) 

708 
then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M. 

709 
\<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))" 

710 
by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong 

711 
simp: indicator_def) 

712 
qed 

713 
from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M" 

714 
and f: "\<And>A i. A \<in> sets M \<Longrightarrow> 

715 
\<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)" 

716 
by auto 

717 
let "?f x" = 

40859  718 
"(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x" 
38656  719 
show ?thesis 
720 
proof (safe intro!: bexI[of _ ?f]) 

721 
show "?f \<in> borel_measurable M" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

722 
by (safe intro!: borel_measurable_psuminf borel_measurable_pextreal_times 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

723 
borel_measurable_pextreal_add borel_measurable_indicator 
40859  724 
borel_measurable_const borel Q_sets Q0 Diff countable_UN) 
38656  725 
fix A assume "A \<in> sets M" 
40859  726 
have *: 
38656  727 
"\<And>x i. indicator A x * (f i x * indicator (Q i) x) = 
728 
f i x * indicator (Q i \<inter> A) x" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

729 
"\<And>x i. (indicator A x * indicator Q0 x :: pextreal) = 
40859  730 
indicator (Q0 \<inter> A) x" by (auto simp: indicator_def) 
38656  731 
have "positive_integral (\<lambda>x. ?f x * indicator A x) = 
40859  732 
(\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)" 
38656  733 
unfolding f[OF `A \<in> sets M`] 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

734 
apply (simp del: pextreal_times(2) add: field_simps *) 
38656  735 
apply (subst positive_integral_add) 
40859  736 
apply (fastsimp intro: Q0 `A \<in> sets M`) 
737 
apply (fastsimp intro: Q_sets `A \<in> sets M` borel_measurable_psuminf borel) 

738 
apply (subst positive_integral_cmult_indicator) 

739 
apply (fastsimp intro: Q0 `A \<in> sets M`) 

38656  740 
unfolding psuminf_cmult_right[symmetric] 
741 
apply (subst positive_integral_psuminf) 

40859  742 
apply (fastsimp intro: `A \<in> sets M` Q_sets borel) 
743 
apply (simp add: *) 

744 
done 

38656  745 
moreover have "(\<Sum>\<^isub>\<infinity>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)" 
40859  746 
using Q Q_sets `A \<in> sets M` 
747 
by (intro v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified]) 

748 
(auto simp: disjoint_family_on_def) 

749 
moreover have "\<omega> * \<mu> (Q0 \<inter> A) = \<nu> (Q0 \<inter> A)" 

750 
proof  

751 
have "Q0 \<inter> A \<in> sets M" using Q0(1) `A \<in> sets M` by blast 

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

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

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

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

38656  758 
ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)" 
40859  759 
using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"] 
760 
by simp 

38656  761 
qed 
762 
qed 

763 

764 
lemma (in sigma_finite_measure) Radon_Nikodym: 

765 
assumes "measure_space M \<nu>" 

766 
assumes "absolutely_continuous \<nu>" 

767 
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

768 
proof  

769 
from Ex_finite_integrable_function 

770 
obtain h where finite: "positive_integral h \<noteq> \<omega>" and 

771 
borel: "h \<in> borel_measurable M" and 

772 
pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and 

773 
"\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto 

774 
let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)" 

775 
from measure_space_density[OF borel] finite 

776 
interpret T: finite_measure M ?T 

777 
unfolding finite_measure_def finite_measure_axioms_def 

778 
by (simp cong: positive_integral_cong) 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

779 
have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pextreal)} = N" 
38656  780 
using sets_into_space pos by (force simp: indicator_def) 
781 
then have "T.absolutely_continuous \<nu>" using assms(2) borel 

782 
unfolding T.absolutely_continuous_def absolutely_continuous_def 

783 
by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff) 

784 
from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this] 

785 
obtain f where f_borel: "f \<in> borel_measurable M" and 

786 
fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = T.positive_integral (\<lambda>x. f x * indicator A x)" by auto 

787 
show ?thesis 

788 
proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"]) 

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

790 
using borel f_borel by (auto intro: borel_measurable_pextreal_times) 
38656  791 
fix A assume "A \<in> sets M" 
792 
then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

793 
using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator) 
38656  794 
from positive_integral_translated_density[OF borel this] 
795 
show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)" 

796 
unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps) 

797 
qed 

798 
qed 

799 

40859  800 
section "Uniqueness of densities" 
801 

802 
lemma (in measure_space) finite_density_unique: 

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

804 
and fin: "positive_integral f < \<omega>" 

805 
shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x)) 

806 
\<longleftrightarrow> (AE x. f x = g x)" 

807 
(is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _") 

808 
proof (intro iffI ballI) 

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

810 
show "?P f A = ?P g A" 

811 
by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp 

812 
next 

813 
assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A" 

814 
from this[THEN bspec, OF top] fin 

815 
have g_fin: "positive_integral g < \<omega>" by (simp cong: positive_integral_cong) 

816 
{ fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 

817 
and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A" 

818 
let ?N = "{x\<in>space M. g x < f x}" 

819 
have N: "?N \<in> sets M" using borel by simp 

820 
have "?P (\<lambda>x. (f x  g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x  g x * indicator ?N x)" 

821 
by (auto intro!: positive_integral_cong simp: indicator_def) 

822 
also have "\<dots> = ?P f ?N  ?P g ?N" 

823 
proof (rule positive_integral_diff) 

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

825 
using borel N by auto 

826 
have "?P g ?N \<le> positive_integral g" 

827 
by (auto intro!: positive_integral_mono simp: indicator_def) 

828 
then show "?P g ?N \<noteq> \<omega>" using g_fin by auto 

829 
fix x assume "x \<in> space M" 

830 
show "g x * indicator ?N x \<le> f x * indicator ?N x" 

831 
by (auto simp: indicator_def) 

832 
qed 

833 
also have "\<dots> = 0" 

834 
using eq[THEN bspec, OF N] by simp 

835 
finally have "\<mu> {x\<in>space M. (f x  g x) * indicator ?N x \<noteq> 0} = 0" 

836 
using borel N by (subst (asm) positive_integral_0_iff) auto 

837 
moreover have "{x\<in>space M. (f x  g x) * indicator ?N x \<noteq> 0} = ?N" 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

838 
by (auto simp: pextreal_zero_le_diff) 
40859  839 
ultimately have "?N \<in> null_sets" using N by simp } 
840 
from this[OF borel g_fin eq] this[OF borel(2,1) fin] 

841 
have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} \<in> null_sets" 

842 
using eq by (intro null_sets_Un) auto 

843 
also have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} = {x\<in>space M. f x \<noteq> g x}" 

844 
by auto 

845 
finally show "AE x. f x = g x" 

846 
unfolding almost_everywhere_def by auto 

847 
qed 

848 

849 
lemma (in finite_measure) density_unique_finite_measure: 

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

851 
assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)" 

852 
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A") 

853 
shows "AE x. f x = f' x" 

854 
proof  

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

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

857 
interpret M: measure_space M ?\<nu> 

858 
using borel(1) by (rule measure_space_density) 

859 
have ac: "absolutely_continuous ?\<nu>" 

860 
using f by (rule density_is_absolutely_continuous) 

861 
from split_space_into_finite_sets_and_rest[OF `measure_space M ?\<nu>` ac] 

862 
obtain Q0 and Q :: "nat \<Rightarrow> 'a set" 

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

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

865 
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 = \<omega>" 

866 
and Q_fin: "\<And>i. ?\<nu> (Q i) \<noteq> \<omega>" by force 

867 
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto 

868 
let ?N = "{x\<in>space M. f x \<noteq> f' x}" 

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

870 
have *: "\<And>i x A. \<And>y::pextreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x" 
40859  871 
unfolding indicator_def by auto 
872 
have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x" 

873 
using borel Q_fin Q 

874 
by (intro finite_density_unique[THEN iffD1] allI) 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

875 
(auto intro!: borel_measurable_pextreal_times f Int simp: *) 
40859  876 
have 2: "AE x. ?f Q0 x = ?f' Q0 x" 
877 
proof (rule AE_I') 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

878 
{ fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M" 
40859  879 
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 
880 
let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}" 

881 
have "(\<Union>i. ?A i) \<in> null_sets" 

882 
proof (rule null_sets_UN) 

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

884 
using borel Q0(1) by auto 

885 
have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)" 

886 
unfolding eq[OF `?A i \<in> sets M`] 

887 
by (auto intro!: positive_integral_mono simp: indicator_def) 

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

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

890 
also have "\<dots> < \<omega>" 

891 
using `?A i \<in> sets M`[THEN finite_measure] by auto 

892 
finally have "?\<nu> (?A i) \<noteq> \<omega>" by simp 

893 
then show "?A i \<in> null_sets" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto 

894 
qed 

895 
also have "(\<Union>i. ?A i) = Q0 \<inter> {x\<in>space M. f x < \<omega>}" 

896 
by (auto simp: less_\<omega>_Ex_of_nat) 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

897 
finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" by (simp add: pextreal_less_\<omega>) } 
40859  898 
from this[OF borel(1) refl] this[OF borel(2) f] 
899 
have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>} \<in> null_sets" by simp_all 

900 
then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>}) \<in> null_sets" by (rule null_sets_Un) 

901 
show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq> 

902 
(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def) 

903 
qed 

904 
have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow> 

905 
?f (space M) x = ?f' (space M) x" 

906 
by (auto simp: indicator_def Q0) 

907 
have 3: "AE x. ?f (space M) x = ?f' (space M) x" 

908 
by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **) 

909 
then show "AE x. f x = f' x" 

910 
by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def) 

911 
qed 

912 

913 
lemma (in sigma_finite_measure) density_unique: 

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

915 
assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)" 

916 
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A") 

917 
shows "AE x. f x = f' x" 

918 
proof  

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

920 
and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" 

921 
using Ex_finite_integrable_function by auto 

922 
interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)" 

923 
using h_borel by (rule measure_space_density) 

924 
interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)" 

925 
by default (simp cong: positive_integral_cong add: fin) 

926 
interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)" 

927 
using borel(1) by (rule measure_space_density) 

928 
interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)" 

929 
using borel(2) by (rule measure_space_density) 

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

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

931 
then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A" 
40859  932 
using pos sets_into_space by (force simp: indicator_def) 
933 
then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets" 

934 
using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) } 

935 
note h_null_sets = this 

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

937 
have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = 

938 
f.positive_integral (\<lambda>x. h x * indicator A x)" 

939 
using `A \<in> sets M` h_borel borel 

940 
by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong) 

941 
also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)" 

942 
by (rule f'.positive_integral_cong_measure) (rule f) 

943 
also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" 

944 
using `A \<in> sets M` h_borel borel 

945 
by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong) 

946 
finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . } 

947 
then have "h.almost_everywhere (\<lambda>x. f x = f' x)" 

948 
using h_borel borel 

949 
by (intro h.density_unique_finite_measure[OF borel]) 

950 
(simp add: positive_integral_translated_density) 

951 
then show "AE x. f x = f' x" 

952 
unfolding h.almost_everywhere_def almost_everywhere_def 

953 
by (auto simp add: h_null_sets) 

954 
qed 

955 

956 
lemma (in sigma_finite_measure) sigma_finite_iff_density_finite: 

957 
assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M" 

958 
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

959 
shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)" 

960 
proof 

961 
assume "sigma_finite_measure M \<nu>" 

962 
then interpret \<nu>: sigma_finite_measure M \<nu> . 

963 
from \<nu>.Ex_finite_integrable_function obtain h where 

964 
h: "h \<in> borel_measurable M" "\<nu>.positive_integral h \<noteq> \<omega>" 

965 
and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto 

966 
have "AE x. f x * h x \<noteq> \<omega>" 

967 
proof (rule AE_I') 

968 
have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)" 

969 
by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]]) 

970 
(intro positive_integral_translated_density f h) 

971 
then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>" 

972 
using h(2) by simp 

973 
then show "(\<lambda>x. f x * h x) ` {\<omega>} \<inter> space M \<in> null_sets" 

974 
using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage) 

975 
qed auto 

976 
then show "AE x. f x \<noteq> \<omega>" 

977 
proof (rule AE_mp, intro AE_cong) 

978 
fix x assume "x \<in> space M" from this[THEN fin] 

979 
show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto 

980 
qed 

981 
next 

982 
assume AE: "AE x. f x \<noteq> \<omega>" 

983 
from sigma_finite guess Q .. note Q = this 

984 
interpret \<nu>: measure_space M \<nu> by fact 

985 
def A \<equiv> "\<lambda>i. f ` (case i of 0 \<Rightarrow> {\<omega>}  Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M" 

986 
{ fix i j have "A i \<inter> Q j \<in> sets M" 

987 
unfolding A_def using f Q 

988 
apply (rule_tac Int) 

989 
by (cases i) (auto intro: measurable_sets[OF f]) } 

990 
note A_in_sets = this 

991 
let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j" 

992 
show "sigma_finite_measure M \<nu>" 

993 
proof (default, intro exI conjI subsetI allI) 

994 
fix x assume "x \<in> range ?A" 

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

996 
then show "x \<in> sets M" using A_in_sets by (cases "prod_decode n") auto 

997 
next 

998 
have "(\<Union>i. ?A i) = (\<Union>i j. A i \<inter> Q j)" 

999 
proof safe 

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

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

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

1003 
qed auto 

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

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

1006 
proof safe 

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

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

1009 
proof (cases "f x") 

1010 
case infinite then show ?thesis using x unfolding A_def by (auto intro: exI[of _ 0]) 

1011 
next 

1012 
case (preal r) 

1013 
with less_\<omega>_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by auto 

1014 
then show ?thesis using x preal unfolding A_def by (auto intro!: exI[of _ "Suc n"]) 

1015 
qed 

1016 
qed (auto simp: A_def) 

1017 
finally show "(\<Union>i. ?A i) = space M" by simp 

1018 
next 

1019 
fix n obtain i j where 

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

1021 
have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>" 

1022 
proof (cases i) 

1023 
case 0 

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

1025 
using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`) 

1026 
then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0" 

1027 
using A_in_sets f 

1028 
apply (subst positive_integral_0_iff) 

1029 
apply fast 

1030 
apply (subst (asm) AE_iff_null_set) 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

1031 
apply (intro borel_measurable_pextreal_neq_const) 
40859  1032 
apply fast 
1033 
by simp 

1034 
then show ?thesis by simp 

1035 
next 

1036 
case (Suc n) 

1037 
then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le> 

1038 
positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)" 

1039 
by (auto intro!: positive_integral_mono simp: indicator_def A_def) 

1040 
also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)" 

1041 
using Q by (auto intro!: positive_integral_cmult_indicator) 

1042 
also have "\<dots> < \<omega>" 

1043 
using Q by auto 

1044 
finally show ?thesis by simp 

1045 
qed 

1046 
then show "\<nu> (?A n) \<noteq> \<omega>" 

1047 
using A_in_sets Q eq by auto 

1048 
qed 

1049 
qed 

1050 

40871  1051 
section "RadonNikodym derivative" 
38656  1052 

1053 
definition (in sigma_finite_measure) 

1054 
"RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and> 

1055 
(\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))" 

1056 

40859  1057 
lemma (in sigma_finite_measure) RN_deriv_cong: 
1058 
assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A" 

1059 
shows "sigma_finite_measure.RN_deriv M \<mu>' \<nu>' x = RN_deriv \<nu> x" 

1060 
proof  

1061 
interpret \<mu>': sigma_finite_measure M \<mu>' 

1062 
using cong(1) by (rule sigma_finite_measure_cong) 

1063 
show ?thesis 

1064 
unfolding RN_deriv_def \<mu>'.RN_deriv_def 

1065 
by (simp add: cong positive_integral_cong_measure[OF cong(1)]) 

1066 
qed 

1067 

38656  1068 
lemma (in sigma_finite_measure) RN_deriv: 
1069 
assumes "measure_space M \<nu>" 

1070 
assumes "absolutely_continuous \<nu>" 

1071 
shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel) 

1072 
and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)" 

1073 
(is "\<And>A. _ \<Longrightarrow> ?int A") 

1074 
proof  

1075 
note Ex = Radon_Nikodym[OF assms, unfolded Bex_def] 

1076 
thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto 

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

1078 
from Ex show "?int A" unfolding RN_deriv_def 

1079 
by (rule someI2_ex) (simp add: `A \<in> sets M`) 

1080 
qed 

1081 

40859  1082 
lemma (in sigma_finite_measure) RN_deriv_positive_integral: 
1083 
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>" 

1084 
and f: "f \<in> borel_measurable M" 

1085 
shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)" 

1086 
proof  

1087 
interpret \<nu>: measure_space M \<nu> by fact 

1088 
have "\<nu>.positive_integral f = 

1089 
measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f" 

1090 
by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric]) 

1091 
also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)" 

1092 
by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f) 

1093 
finally show ?thesis . 

1094 
qed 

1095 

1096 
lemma (in sigma_finite_measure) RN_deriv_unique: 

1097 
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>" 

1098 
and f: "f \<in> borel_measurable M" 

1099 
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)" 

1100 
shows "AE x. f x = RN_deriv \<nu> x" 

1101 
proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]]) 

1102 
fix A assume A: "A \<in> sets M" 

1103 
show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)" 

1104 
unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] .. 

1105 
qed 

1106 

1107 
lemma (in sigma_finite_measure) RN_deriv_vimage: 

1108 
fixes f :: "'b \<Rightarrow> 'a" 

41095  1109 
assumes f: "bij_inv S (space M) f g" 
40859  1110 
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>" 
1111 
shows "AE x. 

41095  1112 
sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x" 
40859  1113 
proof (rule RN_deriv_unique[OF \<nu>]) 
1114 
interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)" 

41095  1115 
using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)]) 
40859  1116 
interpret \<nu>: measure_space M \<nu> using \<nu>(1) . 
1117 
have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))" 

41095  1118 
using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)]) 
40859  1119 
{ fix A assume "A \<in> sets M" then have "f ` (f ` A \<inter> S) = A" 
41095  1120 
using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def] 
40859  1121 
by (intro image_vimage_inter_eq[where T="space M"]) auto } 
1122 
note A_f = this 

1123 
then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))" 

1124 
using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def) 

41095  1125 
show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M" 
40859  1126 
using sf.RN_deriv(1)[OF \<nu>' ac] 
1127 
unfolding measurable_vimage_iff_inv[OF f] comp_def . 

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

41095  1129 
then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f ` A \<inter> S) (g x) = (indicator A x :: pextreal)" 
1130 
using f by (auto simp: bij_inv_def indicator_def) 

40859  1131 
have "\<nu> (f ` (f ` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f ` A \<inter> S) x)" 
1132 
using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac]) 

41095  1133 
also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)" 
40859  1134 
unfolding positive_integral_vimage_inv[OF f] 
1135 
by (simp add: * cong: positive_integral_cong) 

41095  1136 
finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)" 
40859  1137 
unfolding A_f[OF `A \<in> sets M`] . 
1138 
qed 

1139 

1140 
lemma (in sigma_finite_measure) RN_deriv_finite: 

1141 
assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>" 

1142 
shows "AE x. RN_deriv \<nu> x \<noteq> \<omega>" 

1143 
proof  

1144 
interpret \<nu>: sigma_finite_measure M \<nu> by fact 

1145 
have \<nu>: "measure_space M \<nu>" by default 

1146 
from sfm show ?thesis 

1147 
using sigma_finite_iff_density_finite[OF \<nu> RN_deriv[OF \<nu> ac]] by simp 

1148 
qed 

1149 

1150 
lemma (in sigma_finite_measure) 

1151 
assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>" 

1152 
and f: "f \<in> borel_measurable M" 

1153 
shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral) 

1154 
and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable) 

1155 
proof  

1156 
interpret \<nu>: sigma_finite_measure M \<nu> by fact 

1157 
have ms: "measure_space M \<nu>" by default 

41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset

1158 
have minus_cong: "\<And>A B A' B'::pextreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A  real B = real A'  real B'" by simp 
40859  1159 
have f': "(\<lambda>x.  f x) \<in> borel_measurable M" using f by auto 
1160 
{ fix f :: "'a \<Rightarrow> real" assume "f \<in> borel_measurable M" 

1161 
{ fix x assume *: "RN_deriv \<nu> x \<noteq> \<omega>" 

1162 
have "Real (real (RN_deriv \<nu> x)) * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)" 

1163 
by (simp add: mult_le_0_iff) 

1164 
then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)" 

1165 
using * by (simp add: Real_real) } 

1166 
note * = this 

1167 
have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))" 

1168 
apply (rule positive_integral_cong_AE) 

1169 
apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]]) 

1170 
by (auto intro!: AE_cong simp: *) } 

1171 
with this[OF f] this[OF f'] f f' 

1172 
show ?integral ?integrable 

1173 
unfolding \<nu>.integral_def integral_def \<nu>.integrable_def integrable_def 

1174 
by (auto intro!: RN_deriv(1)[OF ms \<nu>(2)] minus_cong simp: RN_deriv_positive_integral[OF ms \<nu>(2)]) 

1175 
qed 

1176 

38656  1177 
lemma (in sigma_finite_measure) RN_deriv_singleton: 
1178 
assumes "measure_space M \<nu>" 

1179 
and ac: "absolutely_continuous \<nu>" 

1180 
and "{x} \<in> sets M" 

1181 
shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}" 

1182 
proof  

1183 
note deriv = RN_deriv[OF assms(1, 2)] 

1184 
from deriv(2)[OF `{x} \<in> sets M`] 

1185 
have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)" 

1186 
by (auto simp: indicator_def intro!: positive_integral_cong) 

1187 
thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`] 

1188 
by auto 

1189 
qed 

1190 

1191 
theorem (in finite_measure_space) RN_deriv_finite_measure: 

1192 
assumes "measure_space M \<nu>" 

1193 
and ac: "absolutely_continuous \<nu>" 

1194 
and "x \<in> space M" 

1195 
shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}" 

1196 
proof  

1197 
have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto 

1198 
from RN_deriv_singleton[OF assms(1,2) this] show ?thesis . 

1199 
qed 

1200 

1201 
end 