author  hoelzl 
Thu, 02 Dec 2010 15:09:02 +0100  
changeset 40875  9a9d33f6fb46 
parent 40873  1ef85f4e7097 
child 41023  9118eb4eb8dc 
permissions  rwrr 
38656  1 
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) 
2 

35582  3 
header {*Lebesgue Integration*} 
4 

38656  5 
theory Lebesgue_Integration 
40859  6 
imports Measure Borel_Space 
35582  7 
begin 
8 

38656  9 
lemma sums_If_finite: 
10 
assumes finite: "finite {r. P r}" 

11 
shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _") 

12 
proof cases 

13 
assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto 

14 
thus ?thesis by (simp add: sums_zero) 

15 
next 

16 
assume not_empty: "{r. P r} \<noteq> {}" 

17 
have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)" 

18 
by (rule series_zero) 

19 
(auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric]) 

20 
also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)" 

21 
by (subst setsum_cases) 

22 
(auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le) 

23 
finally show ?thesis . 

24 
qed 

35582  25 

38656  26 
lemma sums_single: 
27 
"(\<lambda>r. if r = i then f r else 0) sums f i" 

28 
using sums_If_finite[of "\<lambda>r. r = i" f] by simp 

29 

30 
section "Simple function" 

35582  31 

38656  32 
text {* 
33 

34 
Our simple functions are not restricted to positive real numbers. Instead 

35 
they are just functions with a finite range and are measurable when singleton 

36 
sets are measurable. 

35582  37 

38656  38 
*} 
39 

40 
definition (in sigma_algebra) "simple_function g \<longleftrightarrow> 

41 
finite (g ` space M) \<and> 

42 
(\<forall>x \<in> g ` space M. g ` {x} \<inter> space M \<in> sets M)" 

36624  43 

38656  44 
lemma (in sigma_algebra) simple_functionD: 
45 
assumes "simple_function g" 

40875  46 
shows "finite (g ` space M)" and "g ` X \<inter> space M \<in> sets M" 
40871  47 
proof  
48 
show "finite (g ` space M)" 

49 
using assms unfolding simple_function_def by auto 

40875  50 
have "g ` X \<inter> space M = g ` (X \<inter> g`space M) \<inter> space M" by auto 
51 
also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g`{x} \<inter> space M)" by auto 

52 
finally show "g ` X \<inter> space M \<in> sets M" using assms 

53 
by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def) 

40871  54 
qed 
36624  55 

38656  56 
lemma (in sigma_algebra) simple_function_indicator_representation: 
57 
fixes f ::"'a \<Rightarrow> pinfreal" 

58 
assumes f: "simple_function f" and x: "x \<in> space M" 

59 
shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f ` {y} \<inter> space M) x)" 

60 
(is "?l = ?r") 

61 
proof  

38705  62 
have "?r = (\<Sum>y \<in> f ` space M. 
38656  63 
(if y = f x then y * indicator (f ` {y} \<inter> space M) x else 0))" 
64 
by (auto intro!: setsum_cong2) 

65 
also have "... = f x * indicator (f ` {f x} \<inter> space M) x" 

66 
using assms by (auto dest: simple_functionD simp: setsum_delta) 

67 
also have "... = f x" using x by (auto simp: indicator_def) 

68 
finally show ?thesis by auto 

69 
qed 

36624  70 

38656  71 
lemma (in measure_space) simple_function_notspace: 
72 
"simple_function (\<lambda>x. h x * indicator ( space M) x::pinfreal)" (is "simple_function ?h") 

35692  73 
proof  
38656  74 
have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto 
75 
hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) 

76 
have "?h ` {0} \<inter> space M = space M" by auto 

77 
thus ?thesis unfolding simple_function_def by auto 

78 
qed 

79 

80 
lemma (in sigma_algebra) simple_function_cong: 

81 
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" 

82 
shows "simple_function f \<longleftrightarrow> simple_function g" 

83 
proof  

84 
have "f ` space M = g ` space M" 

85 
"\<And>x. f ` {x} \<inter> space M = g ` {x} \<inter> space M" 

86 
using assms by (auto intro!: image_eqI) 

87 
thus ?thesis unfolding simple_function_def using assms by simp 

88 
qed 

89 

90 
lemma (in sigma_algebra) borel_measurable_simple_function: 

91 
assumes "simple_function f" 

92 
shows "f \<in> borel_measurable M" 

93 
proof (rule borel_measurableI) 

94 
fix S 

95 
let ?I = "f ` (f ` S \<inter> space M)" 

96 
have *: "(\<Union>x\<in>?I. f ` {x} \<inter> space M) = f ` S \<inter> space M" (is "?U = _") by auto 

97 
have "finite ?I" 

98 
using assms unfolding simple_function_def by (auto intro: finite_subset) 

99 
hence "?U \<in> sets M" 

100 
apply (rule finite_UN) 

101 
using assms unfolding simple_function_def by auto 

102 
thus "f ` S \<inter> space M \<in> sets M" unfolding * . 

35692  103 
qed 
104 

38656  105 
lemma (in sigma_algebra) simple_function_borel_measurable: 
106 
fixes f :: "'a \<Rightarrow> 'x::t2_space" 

107 
assumes "f \<in> borel_measurable M" and "finite (f ` space M)" 

108 
shows "simple_function f" 

109 
using assms unfolding simple_function_def 

110 
by (auto intro: borel_measurable_vimage) 

111 

112 
lemma (in sigma_algebra) simple_function_const[intro, simp]: 

113 
"simple_function (\<lambda>x. c)" 

114 
by (auto intro: finite_subset simp: simple_function_def) 

115 

116 
lemma (in sigma_algebra) simple_function_compose[intro, simp]: 

117 
assumes "simple_function f" 

118 
shows "simple_function (g \<circ> f)" 

119 
unfolding simple_function_def 

120 
proof safe 

121 
show "finite ((g \<circ> f) ` space M)" 

122 
using assms unfolding simple_function_def by (auto simp: image_compose) 

123 
next 

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

125 
let ?G = "g ` {g (f x)} \<inter> (f`space M)" 

126 
have *: "(g \<circ> f) ` {(g \<circ> f) x} \<inter> space M = 

127 
(\<Union>x\<in>?G. f ` {x} \<inter> space M)" by auto 

128 
show "(g \<circ> f) ` {(g \<circ> f) x} \<inter> space M \<in> sets M" 

129 
using assms unfolding simple_function_def * 

130 
by (rule_tac finite_UN) (auto intro!: finite_UN) 

131 
qed 

132 

133 
lemma (in sigma_algebra) simple_function_indicator[intro, simp]: 

134 
assumes "A \<in> sets M" 

135 
shows "simple_function (indicator A)" 

35692  136 
proof  
38656  137 
have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _") 
138 
by (auto simp: indicator_def) 

139 
hence "finite ?S" by (rule finite_subset) simp 

140 
moreover have " A \<inter> space M = space M  A" by auto 

141 
ultimately show ?thesis unfolding simple_function_def 

142 
using assms by (auto simp: indicator_def_raw) 

35692  143 
qed 
144 

38656  145 
lemma (in sigma_algebra) simple_function_Pair[intro, simp]: 
146 
assumes "simple_function f" 

147 
assumes "simple_function g" 

148 
shows "simple_function (\<lambda>x. (f x, g x))" (is "simple_function ?p") 

149 
unfolding simple_function_def 

150 
proof safe 

151 
show "finite (?p ` space M)" 

152 
using assms unfolding simple_function_def 

153 
by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto 

154 
next 

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

156 
have "(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M = 

157 
(f ` {f x} \<inter> space M) \<inter> (g ` {g x} \<inter> space M)" 

158 
by auto 

159 
with `x \<in> space M` show "(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M \<in> sets M" 

160 
using assms unfolding simple_function_def by auto 

161 
qed 

35692  162 

38656  163 
lemma (in sigma_algebra) simple_function_compose1: 
164 
assumes "simple_function f" 

165 
shows "simple_function (\<lambda>x. g (f x))" 

166 
using simple_function_compose[OF assms, of g] 

167 
by (simp add: comp_def) 

35582  168 

38656  169 
lemma (in sigma_algebra) simple_function_compose2: 
170 
assumes "simple_function f" and "simple_function g" 

171 
shows "simple_function (\<lambda>x. h (f x) (g x))" 

172 
proof  

173 
have "simple_function ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))" 

174 
using assms by auto 

175 
thus ?thesis by (simp_all add: comp_def) 

176 
qed 

35582  177 

38656  178 
lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] 
179 
and simple_function_diff[intro, simp] = simple_function_compose2[where h="op "] 

180 
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] 

181 
and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] 

182 
and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] 

183 
and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] 

184 

185 
lemma (in sigma_algebra) simple_function_setsum[intro, simp]: 

186 
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)" 

187 
shows "simple_function (\<lambda>x. \<Sum>i\<in>P. f i x)" 

188 
proof cases 

189 
assume "finite P" from this assms show ?thesis by induct auto 

190 
qed auto 

35582  191 

38656  192 
lemma (in sigma_algebra) simple_function_le_measurable: 
193 
assumes "simple_function f" "simple_function g" 

194 
shows "{x \<in> space M. f x \<le> g x} \<in> sets M" 

195 
proof  

196 
have *: "{x \<in> space M. f x \<le> g x} = 

197 
(\<Union>(F, G)\<in>f`space M \<times> g`space M. 

198 
if F \<le> G then (f ` {F} \<inter> space M) \<inter> (g ` {G} \<inter> space M) else {})" 

199 
apply (auto split: split_if_asm) 

200 
apply (rule_tac x=x in bexI) 

201 
apply (rule_tac x=x in bexI) 

202 
by simp_all 

203 
have **: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> 

204 
(f ` {f x} \<inter> space M) \<inter> (g ` {g y} \<inter> space M) \<in> sets M" 

205 
using assms unfolding simple_function_def by auto 

206 
have "finite (f`space M \<times> g`space M)" 

207 
using assms unfolding simple_function_def by auto 

208 
thus ?thesis unfolding * 

209 
apply (rule finite_UN) 

210 
using assms unfolding simple_function_def 

211 
by (auto intro!: **) 

35582  212 
qed 
213 

38656  214 
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence: 
215 
fixes u :: "'a \<Rightarrow> pinfreal" 

216 
assumes u: "u \<in> borel_measurable M" 

217 
shows "\<exists>f. (\<forall>i. simple_function (f i) \<and> (\<forall>x\<in>space M. f i x \<noteq> \<omega>)) \<and> f \<up> u" 

35582  218 
proof  
38656  219 
have "\<exists>f. \<forall>x j. (of_nat j \<le> u x \<longrightarrow> f x j = j*2^j) \<and> 
220 
(u x < of_nat j \<longrightarrow> of_nat (f x j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f x j)))" 

221 
(is "\<exists>f. \<forall>x j. ?P x j (f x j)") 

222 
proof(rule choice, rule, rule choice, rule) 

223 
fix x j show "\<exists>n. ?P x j n" 

224 
proof cases 

225 
assume *: "u x < of_nat j" 

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

227 
from reals_Archimedean6a[of "r * 2^j"] 

228 
obtain n :: nat where "real n \<le> r * 2 ^ j" "r * 2 ^ j < real (Suc n)" 

229 
using `0 \<le> r` by (auto simp: zero_le_power zero_le_mult_iff) 

230 
thus ?thesis using r * by (auto intro!: exI[of _ n]) 

231 
qed auto 

35582  232 
qed 
38656  233 
then obtain f where top: "\<And>j x. of_nat j \<le> u x \<Longrightarrow> f x j = j*2^j" and 
234 
upper: "\<And>j x. u x < of_nat j \<Longrightarrow> of_nat (f x j) \<le> u x * 2^j" and 

235 
lower: "\<And>j x. u x < of_nat j \<Longrightarrow> u x * 2^j < of_nat (Suc (f x j))" by blast 

35582  236 

38656  237 
{ fix j x P 
238 
assume 1: "of_nat j \<le> u x \<Longrightarrow> P (j * 2^j)" 

239 
assume 2: "\<And>k. \<lbrakk> u x < of_nat j ; of_nat k \<le> u x * 2^j ; u x * 2^j < of_nat (Suc k) \<rbrakk> \<Longrightarrow> P k" 

240 
have "P (f x j)" 

241 
proof cases 

242 
assume "of_nat j \<le> u x" thus "P (f x j)" 

243 
using top[of j x] 1 by auto 

244 
next 

245 
assume "\<not> of_nat j \<le> u x" 

246 
hence "u x < of_nat j" "of_nat (f x j) \<le> u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))" 

247 
using upper lower by auto 

248 
from 2[OF this] show "P (f x j)" . 

249 
qed } 

250 
note fI = this 

251 

252 
{ fix j x 

253 
have "f x j = j * 2 ^ j \<longleftrightarrow> of_nat j \<le> u x" 

254 
by (rule fI, simp, cases "u x") (auto split: split_if_asm) } 

255 
note f_eq = this 

35582  256 

38656  257 
{ fix j x 
258 
have "f x j \<le> j * 2 ^ j" 

259 
proof (rule fI) 

260 
fix k assume *: "u x < of_nat j" 

261 
assume "of_nat k \<le> u x * 2 ^ j" 

262 
also have "\<dots> \<le> of_nat (j * 2^j)" 

263 
using * by (cases "u x") (auto simp: zero_le_mult_iff) 

264 
finally show "k \<le> j*2^j" by (auto simp del: real_of_nat_mult) 

265 
qed simp } 

266 
note f_upper = this 

35582  267 

38656  268 
let "?g j x" = "of_nat (f x j) / 2^j :: pinfreal" 
269 
show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def 

270 
proof (safe intro!: exI[of _ ?g]) 

271 
fix j 

272 
have *: "?g j ` space M \<subseteq> (\<lambda>x. of_nat x / 2^j) ` {..j * 2^j}" 

273 
using f_upper by auto 

274 
thus "finite (?g j ` space M)" by (rule finite_subset) auto 

275 
next 

276 
fix j t assume "t \<in> space M" 

277 
have **: "?g j ` {?g j t} \<inter> space M = {x \<in> space M. f t j = f x j}" 

278 
by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff) 

35582  279 

38656  280 
show "?g j ` {?g j t} \<inter> space M \<in> sets M" 
281 
proof cases 

282 
assume "of_nat j \<le> u t" 

283 
hence "?g j ` {?g j t} \<inter> space M = {x\<in>space M. of_nat j \<le> u x}" 

284 
unfolding ** f_eq[symmetric] by auto 

285 
thus "?g j ` {?g j t} \<inter> space M \<in> sets M" 

286 
using u by auto 

35582  287 
next 
38656  288 
assume not_t: "\<not> of_nat j \<le> u t" 
289 
hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \<le> j*2^j` by auto 

290 
have split_vimage: "?g j ` {?g j t} \<inter> space M = 

291 
{x\<in>space M. of_nat (f t j)/2^j \<le> u x} \<inter> {x\<in>space M. u x < of_nat (Suc (f t j))/2^j}" 

292 
unfolding ** 

293 
proof safe 

294 
fix x assume [simp]: "f t j = f x j" 

295 
have *: "\<not> of_nat j \<le> u x" using not_t f_eq[symmetric] by simp 

296 
hence "of_nat (f t j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f t j))" 

297 
using upper lower by auto 

298 
hence "of_nat (f t j) / 2^j \<le> u x \<and> u x < of_nat (Suc (f t j))/2^j" using * 

299 
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) 

300 
thus "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" by auto 

301 
next 

302 
fix x 

303 
assume "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" 

304 
hence "of_nat (f t j) \<le> u x * 2 ^ j \<and> u x * 2 ^ j < of_nat (Suc (f t j))" 

305 
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) 

306 
hence 1: "of_nat (f t j) \<le> u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto 

307 
note 2 

308 
also have "\<dots> \<le> of_nat (j*2^j)" 

309 
using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult) 

310 
finally have bound_ux: "u x < of_nat j" 

311 
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq) 

312 
show "f t j = f x j" 

313 
proof (rule antisym) 

314 
from 1 lower[OF bound_ux] 

315 
show "f t j \<le> f x j" by (cases "u x") (auto split: split_if_asm) 

316 
from upper[OF bound_ux] 2 

317 
show "f x j \<le> f t j" by (cases "u x") (auto split: split_if_asm) 

318 
qed 

319 
qed 

320 
show ?thesis unfolding split_vimage using u by auto 

35582  321 
qed 
38656  322 
next 
323 
fix j t assume "?g j t = \<omega>" thus False by (auto simp: power_le_zero_eq) 

324 
next 

325 
fix t 

326 
{ fix i 

327 
have "f t i * 2 \<le> f t (Suc i)" 

328 
proof (rule fI) 

329 
assume "of_nat (Suc i) \<le> u t" 

330 
hence "of_nat i \<le> u t" by (cases "u t") auto 

331 
thus "f t i * 2 \<le> Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp 

332 
next 

333 
fix k 

334 
assume *: "u t * 2 ^ Suc i < of_nat (Suc k)" 

335 
show "f t i * 2 \<le> k" 

336 
proof (rule fI) 

337 
assume "of_nat i \<le> u t" 

338 
hence "of_nat (i * 2^Suc i) \<le> u t * 2^Suc i" 

339 
by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) 

340 
also have "\<dots> < of_nat (Suc k)" using * by auto 

341 
finally show "i * 2 ^ i * 2 \<le> k" 

342 
by (auto simp del: real_of_nat_mult) 

343 
next 

344 
fix j assume "of_nat j \<le> u t * 2 ^ i" 

345 
with * show "j * 2 \<le> k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) 

346 
qed 

347 
qed 

348 
thus "?g i t \<le> ?g (Suc i) t" 

349 
by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) } 

350 
hence mono: "mono (\<lambda>i. ?g i t)" unfolding mono_iff_le_Suc by auto 

35582  351 

38656  352 
show "(SUP j. of_nat (f t j) / 2 ^ j) = u t" 
353 
proof (rule pinfreal_SUPI) 

354 
fix j show "of_nat (f t j) / 2 ^ j \<le> u t" 

355 
proof (rule fI) 

356 
assume "of_nat j \<le> u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \<le> u t" 

357 
by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps) 

358 
next 

359 
fix k assume "of_nat k \<le> u t * 2 ^ j" 

360 
thus "of_nat k / 2 ^ j \<le> u t" 

361 
by (cases "u t") 

362 
(auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff) 

363 
qed 

364 
next 

365 
fix y :: pinfreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y" 

366 
show "u t \<le> y" 

367 
proof (cases "u t") 

368 
case (preal r) 

369 
show ?thesis 

370 
proof (rule ccontr) 

371 
assume "\<not> u t \<le> y" 

372 
then obtain p where p: "y = Real p" "0 \<le> p" "p < r" using preal by (cases y) auto 

373 
with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r  p"] 

374 
obtain n where n: "\<And>N. n \<le> N \<Longrightarrow> inverse (2^N) < r  p" by auto 

375 
let ?N = "max n (natfloor r + 1)" 

376 
have "u t < of_nat ?N" "n \<le> ?N" 

377 
using ge_natfloor_plus_one_imp_gt[of r n] preal 

38705  378 
using real_natfloor_add_one_gt 
379 
by (auto simp: max_def real_of_nat_Suc) 

38656  380 
from lower[OF this(1)] 
381 
have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq 

382 
using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm) 

383 
hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N" 

384 
using preal by (auto simp: field_simps divide_real_def[symmetric]) 

385 
with n[OF `n \<le> ?N`] p preal *[of ?N] 

386 
show False 

387 
by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm) 

388 
qed 

389 
next 

390 
case infinite 

391 
{ fix j have "f t j = j*2^j" using top[of j t] infinite by simp 

392 
hence "of_nat j \<le> y" using *[of j] 

393 
by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) } 

394 
note all_less_y = this 

395 
show ?thesis unfolding infinite 

396 
proof (rule ccontr) 

397 
assume "\<not> \<omega> \<le> y" then obtain r where r: "y = Real r" "0 \<le> r" by (cases y) auto 

398 
moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat) 

399 
with all_less_y[of n] r show False by auto 

400 
qed 

401 
qed 

402 
qed 

35582  403 
qed 
404 
qed 

405 

38656  406 
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence': 
407 
fixes u :: "'a \<Rightarrow> pinfreal" 

408 
assumes "u \<in> borel_measurable M" 

409 
obtains (x) f where "f \<up> u" "\<And>i. simple_function (f i)" "\<And>i. \<omega>\<notin>f i`space M" 

35582  410 
proof  
38656  411 
from borel_measurable_implies_simple_function_sequence[OF assms] 
412 
obtain f where x: "\<And>i. simple_function (f i)" "f \<up> u" 

413 
and fin: "\<And>i. \<And>x. x\<in>space M \<Longrightarrow> f i x \<noteq> \<omega>" by auto 

414 
{ fix i from fin[of _ i] have "\<omega> \<notin> f i`space M" by fastsimp } 

415 
with x show thesis by (auto intro!: that[of f]) 

416 
qed 

417 

39092  418 
lemma (in sigma_algebra) simple_function_eq_borel_measurable: 
419 
fixes f :: "'a \<Rightarrow> pinfreal" 

420 
shows "simple_function f \<longleftrightarrow> 

421 
finite (f`space M) \<and> f \<in> borel_measurable M" 

422 
using simple_function_borel_measurable[of f] 

423 
borel_measurable_simple_function[of f] 

424 
by (fastsimp simp: simple_function_def) 

425 

426 
lemma (in measure_space) simple_function_restricted: 

427 
fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M" 

428 
shows "sigma_algebra.simple_function (restricted_space A) f \<longleftrightarrow> simple_function (\<lambda>x. f x * indicator A x)" 

429 
(is "sigma_algebra.simple_function ?R f \<longleftrightarrow> simple_function ?f") 

430 
proof  

431 
interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`]) 

432 
have "finite (f`A) \<longleftrightarrow> finite (?f`space M)" 

433 
proof cases 

434 
assume "A = space M" 

435 
then have "f`A = ?f`space M" by (fastsimp simp: image_iff) 

436 
then show ?thesis by simp 

437 
next 

438 
assume "A \<noteq> space M" 

439 
then obtain x where x: "x \<in> space M" "x \<notin> A" 

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

441 
have *: "?f`space M = f`A \<union> {0}" 

442 
proof (auto simp add: image_iff) 

443 
show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0" 

444 
using x by (auto intro!: bexI[of _ x]) 

445 
next 

446 
fix x assume "x \<in> A" 

447 
then show "\<exists>y\<in>space M. f x = f y * indicator A y" 

448 
using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x]) 

449 
next 

450 
fix x 

451 
assume "indicator A x \<noteq> (0::pinfreal)" 

452 
then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm) 

453 
moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y" 

454 
ultimately show "f x = 0" by auto 

455 
qed 

456 
then show ?thesis by auto 

457 
qed 

458 
then show ?thesis 

459 
unfolding simple_function_eq_borel_measurable 

460 
R.simple_function_eq_borel_measurable 

461 
unfolding borel_measurable_restricted[OF `A \<in> sets M`] 

462 
by auto 

463 
qed 

464 

465 
lemma (in sigma_algebra) simple_function_subalgebra: 

466 
assumes "sigma_algebra.simple_function (M\<lparr>sets:=N\<rparr>) f" 

467 
and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr>sets:=N\<rparr>)" 

468 
shows "simple_function f" 

469 
using assms 

470 
unfolding simple_function_def 

471 
unfolding sigma_algebra.simple_function_def[OF N_subalgebra(2)] 

472 
by auto 

473 

40859  474 
lemma (in sigma_algebra) simple_function_vimage: 
475 
fixes g :: "'a \<Rightarrow> pinfreal" and f :: "'d \<Rightarrow> 'a" 

476 
assumes g: "simple_function g" and f: "f \<in> S \<rightarrow> space M" 

477 
shows "sigma_algebra.simple_function (vimage_algebra S f) (\<lambda>x. g (f x))" 

478 
proof  

479 
have subset: "(\<lambda>x. g (f x)) ` S \<subseteq> g ` space M" 

480 
using f by auto 

481 
interpret V: sigma_algebra "vimage_algebra S f" 

482 
using f by (rule sigma_algebra_vimage) 

483 
show ?thesis using g 

484 
unfolding simple_function_eq_borel_measurable 

485 
unfolding V.simple_function_eq_borel_measurable 

486 
using measurable_vimage[OF _ f, of g borel] 

487 
using finite_subset[OF subset] by auto 

488 
qed 

489 

38656  490 
section "Simple integral" 
491 

492 
definition (in measure_space) 

493 
"simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f ` {x} \<inter> space M))" 

35582  494 

38656  495 
lemma (in measure_space) simple_integral_cong: 
496 
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" 

497 
shows "simple_integral f = simple_integral g" 

498 
proof  

499 
have "f ` space M = g ` space M" 

500 
"\<And>x. f ` {x} \<inter> space M = g ` {x} \<inter> space M" 

501 
using assms by (auto intro!: image_eqI) 

502 
thus ?thesis unfolding simple_integral_def by simp 

503 
qed 

504 

40859  505 
lemma (in measure_space) simple_integral_cong_measure: 
506 
assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A" and "simple_function f" 

507 
shows "measure_space.simple_integral M \<nu> f = simple_integral f" 

508 
proof  

509 
interpret v: measure_space M \<nu> 

510 
by (rule measure_space_cong) fact 

40871  511 
from simple_functionD[OF `simple_function f`] assms show ?thesis 
40859  512 
unfolding simple_integral_def v.simple_integral_def 
513 
by (auto intro!: setsum_cong) 

514 
qed 

515 

38656  516 
lemma (in measure_space) simple_integral_const[simp]: 
517 
"simple_integral (\<lambda>x. c) = c * \<mu> (space M)" 

518 
proof (cases "space M = {}") 

519 
case True thus ?thesis unfolding simple_integral_def by simp 

520 
next 

521 
case False hence "(\<lambda>x. c) ` space M = {c}" by auto 

522 
thus ?thesis unfolding simple_integral_def by simp 

35582  523 
qed 
524 

38656  525 
lemma (in measure_space) simple_function_partition: 
526 
assumes "simple_function f" and "simple_function g" 

39910  527 
shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f ` {f x} \<inter> g ` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)" 
38656  528 
(is "_ = setsum _ (?p ` space M)") 
529 
proof 

530 
let "?sub x" = "?p ` (f ` {x} \<inter> space M)" 

531 
let ?SIGMA = "Sigma (f`space M) ?sub" 

35582  532 

38656  533 
have [intro]: 
534 
"finite (f ` space M)" 

535 
"finite (g ` space M)" 

536 
using assms unfolding simple_function_def by simp_all 

537 

538 
{ fix A 

539 
have "?p ` (A \<inter> space M) \<subseteq> 

540 
(\<lambda>(x,y). f ` {x} \<inter> g ` {y} \<inter> space M) ` (f`space M \<times> g`space M)" 

541 
by auto 

542 
hence "finite (?p ` (A \<inter> space M))" 

40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
39910
diff
changeset

543 
by (rule finite_subset) auto } 
38656  544 
note this[intro, simp] 
35582  545 

38656  546 
{ fix x assume "x \<in> space M" 
547 
have "\<Union>(?sub (f x)) = (f ` {f x} \<inter> space M)" by auto 

548 
moreover { 

549 
fix x y 

550 
have *: "f ` {f x} \<inter> g ` {g x} \<inter> space M 

551 
= (f ` {f x} \<inter> space M) \<inter> (g ` {g x} \<inter> space M)" by auto 

552 
assume "x \<in> space M" "y \<in> space M" 

553 
hence "f ` {f x} \<inter> g ` {g x} \<inter> space M \<in> sets M" 

554 
using assms unfolding simple_function_def * by auto } 

555 
ultimately 

556 
have "\<mu> (f ` {f x} \<inter> space M) = setsum (\<mu>) (?sub (f x))" 

557 
by (subst measure_finitely_additive) auto } 

558 
hence "simple_integral f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)" 

559 
unfolding simple_integral_def 

560 
by (subst setsum_Sigma[symmetric], 

561 
auto intro!: setsum_cong simp: setsum_right_distrib[symmetric]) 

39910  562 
also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)" 
38656  563 
proof  
564 
have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI) 

39910  565 
have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M 
38656  566 
= (\<lambda>x. (f x, ?p x)) ` space M" 
567 
proof safe 

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

39910  569 
thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M" 
38656  570 
by (auto intro!: image_eqI[of _ _ "?p x"]) 
571 
qed auto 

572 
thus ?thesis 

39910  573 
apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI) 
38656  574 
apply (rule_tac x="xa" in image_eqI) 
575 
by simp_all 

576 
qed 

577 
finally show ?thesis . 

35582  578 
qed 
579 

38656  580 
lemma (in measure_space) simple_integral_add[simp]: 
581 
assumes "simple_function f" and "simple_function g" 

582 
shows "simple_integral (\<lambda>x. f x + g x) = simple_integral f + simple_integral g" 

35582  583 
proof  
38656  584 
{ fix x let ?S = "g ` {g x} \<inter> f ` {f x} \<inter> space M" 
585 
assume "x \<in> space M" 

586 
hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" 

587 
"(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M = ?S" 

588 
by auto } 

589 
thus ?thesis 

590 
unfolding 

591 
simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]] 

592 
simple_function_partition[OF `simple_function f` `simple_function g`] 

593 
simple_function_partition[OF `simple_function g` `simple_function f`] 

594 
apply (subst (3) Int_commute) 

595 
by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong) 

35582  596 
qed 
597 

38656  598 
lemma (in measure_space) simple_integral_setsum[simp]: 
599 
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function (f i)" 

600 
shows "simple_integral (\<lambda>x. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))" 

601 
proof cases 

602 
assume "finite P" 

603 
from this assms show ?thesis 

604 
by induct (auto simp: simple_function_setsum simple_integral_add) 

605 
qed auto 

606 

607 
lemma (in measure_space) simple_integral_mult[simp]: 

608 
assumes "simple_function f" 

609 
shows "simple_integral (\<lambda>x. c * f x) = c * simple_integral f" 

610 
proof  

611 
note mult = simple_function_mult[OF simple_function_const[of c] assms] 

612 
{ fix x let ?S = "f ` {f x} \<inter> (\<lambda>x. c * f x) ` {c * f x} \<inter> space M" 

613 
assume "x \<in> space M" 

614 
hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" 

615 
by auto } 

616 
thus ?thesis 

617 
unfolding simple_function_partition[OF mult assms] 

618 
simple_function_partition[OF assms mult] 

619 
by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong) 

35582  620 
qed 
621 

40871  622 
lemma (in sigma_algebra) simple_function_If: 
623 
assumes sf: "simple_function f" "simple_function g" and A: "A \<in> sets M" 

624 
shows "simple_function (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function ?IF") 

625 
proof  

626 
def F \<equiv> "\<lambda>x. f ` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g ` {x} \<inter> space M" 

627 
show ?thesis unfolding simple_function_def 

628 
proof safe 

629 
have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto 

630 
from finite_subset[OF this] assms 

631 
show "finite (?IF ` space M)" unfolding simple_function_def by auto 

632 
next 

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

634 
then have *: "?IF ` {?IF x} \<inter> space M = (if x \<in> A 

635 
then ((F (f x) \<inter> A) \<union> (G (f x)  (G (f x) \<inter> A))) 

636 
else ((F (g x) \<inter> A) \<union> (G (g x)  (G (g x) \<inter> A))))" 

637 
using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) 

638 
have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M" 

639 
unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto 

640 
show "?IF ` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto 

641 
qed 

642 
qed 

643 

40859  644 
lemma (in measure_space) simple_integral_mono_AE: 
645 
assumes "simple_function f" and "simple_function g" 

646 
and mono: "AE x. f x \<le> g x" 

647 
shows "simple_integral f \<le> simple_integral g" 

648 
proof  

649 
let "?S x" = "(g ` {g x} \<inter> space M) \<inter> (f ` {f x} \<inter> space M)" 

650 
have *: "\<And>x. g ` {g x} \<inter> f ` {f x} \<inter> space M = ?S x" 

651 
"\<And>x. f ` {f x} \<inter> g ` {g x} \<inter> space M = ?S x" by auto 

652 
show ?thesis 

653 
unfolding * 

654 
simple_function_partition[OF `simple_function f` `simple_function g`] 

655 
simple_function_partition[OF `simple_function g` `simple_function f`] 

656 
proof (safe intro!: setsum_mono) 

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

658 
then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto 

659 
show "the_elem (f`?S x) * \<mu> (?S x) \<le> the_elem (g`?S x) * \<mu> (?S x)" 

660 
proof (cases "f x \<le> g x") 

661 
case True then show ?thesis using * by (auto intro!: mult_right_mono) 

662 
next 

663 
case False 

664 
obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "\<mu> N = 0" 

665 
using mono by (auto elim!: AE_E) 

666 
have "?S x \<subseteq> N" using N `x \<in> space M` False by auto 

40871  667 
moreover have "?S x \<in> sets M" using assms 
668 
by (rule_tac Int) (auto intro!: simple_functionD) 

40859  669 
ultimately have "\<mu> (?S x) \<le> \<mu> N" 
670 
using `N \<in> sets M` by (auto intro!: measure_mono) 

671 
then show ?thesis using `\<mu> N = 0` by auto 

672 
qed 

673 
qed 

674 
qed 

675 

38656  676 
lemma (in measure_space) simple_integral_mono: 
677 
assumes "simple_function f" and "simple_function g" 

678 
and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x" 

679 
shows "simple_integral f \<le> simple_integral g" 

40859  680 
proof (rule simple_integral_mono_AE[OF assms(1, 2)]) 
681 
show "AE x. f x \<le> g x" 

682 
using mono by (rule AE_cong) auto 

35582  683 
qed 
684 

40859  685 
lemma (in measure_space) simple_integral_cong_AE: 
686 
assumes "simple_function f" "simple_function g" and "AE x. f x = g x" 

687 
shows "simple_integral f = simple_integral g" 

688 
using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) 

689 

690 
lemma (in measure_space) simple_integral_cong': 

691 
assumes sf: "simple_function f" "simple_function g" 

692 
and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" 

693 
shows "simple_integral f = simple_integral g" 

694 
proof (intro simple_integral_cong_AE sf AE_I) 

695 
show "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" by fact 

696 
show "{x \<in> space M. f x \<noteq> g x} \<in> sets M" 

697 
using sf[THEN borel_measurable_simple_function] by auto 

698 
qed simp 

699 

38656  700 
lemma (in measure_space) simple_integral_indicator: 
701 
assumes "A \<in> sets M" 

702 
assumes "simple_function f" 

703 
shows "simple_integral (\<lambda>x. f x * indicator A x) = 

704 
(\<Sum>x \<in> f ` space M. x * \<mu> (f ` {x} \<inter> space M \<inter> A))" 

705 
proof cases 

706 
assume "A = space M" 

707 
moreover hence "simple_integral (\<lambda>x. f x * indicator A x) = simple_integral f" 

708 
by (auto intro!: simple_integral_cong) 

709 
moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto 

710 
ultimately show ?thesis by (simp add: simple_integral_def) 

711 
next 

712 
assume "A \<noteq> space M" 

713 
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto 

714 
have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _") 

35582  715 
proof safe 
38656  716 
fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto 
717 
next 

718 
fix y assume "y \<in> A" thus "f y \<in> ?I ` space M" 

719 
using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) 

720 
next 

721 
show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) 

35582  722 
qed 
38656  723 
have *: "simple_integral (\<lambda>x. f x * indicator A x) = 
724 
(\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f ` {x} \<inter> space M \<inter> A))" 

725 
unfolding simple_integral_def I 

726 
proof (rule setsum_mono_zero_cong_left) 

727 
show "finite (f ` space M \<union> {0})" 

728 
using assms(2) unfolding simple_function_def by auto 

729 
show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}" 

730 
using sets_into_space[OF assms(1)] by auto 

40859  731 
have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f ` {f x} \<inter> space M \<inter> A = {}" 
732 
by (auto simp: image_iff) 

38656  733 
thus "\<forall>i\<in>f ` space M \<union> {0}  (f ` A \<union> {0}). 
734 
i * \<mu> (f ` {i} \<inter> space M \<inter> A) = 0" by auto 

735 
next 

736 
fix x assume "x \<in> f`A \<union> {0}" 

737 
hence "x \<noteq> 0 \<Longrightarrow> ?I ` {x} \<inter> space M = f ` {x} \<inter> space M \<inter> A" 

738 
by (auto simp: indicator_def split: split_if_asm) 

739 
thus "x * \<mu> (?I ` {x} \<inter> space M) = 

740 
x * \<mu> (f ` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all 

741 
qed 

742 
show ?thesis unfolding * 

743 
using assms(2) unfolding simple_function_def 

744 
by (auto intro!: setsum_mono_zero_cong_right) 

745 
qed 

35582  746 

38656  747 
lemma (in measure_space) simple_integral_indicator_only[simp]: 
748 
assumes "A \<in> sets M" 

749 
shows "simple_integral (indicator A) = \<mu> A" 

750 
proof cases 

751 
assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto 

752 
thus ?thesis unfolding simple_integral_def using `space M = {}` by auto 

753 
next 

754 
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pinfreal}" by auto 

755 
thus ?thesis 

756 
using simple_integral_indicator[OF assms simple_function_const[of 1]] 

757 
using sets_into_space[OF assms] 

758 
by (auto intro!: arg_cong[where f="\<mu>"]) 

759 
qed 

35582  760 

38656  761 
lemma (in measure_space) simple_integral_null_set: 
762 
assumes "simple_function u" "N \<in> null_sets" 

763 
shows "simple_integral (\<lambda>x. u x * indicator N x) = 0" 

764 
proof  

40859  765 
have "AE x. indicator N x = (0 :: pinfreal)" 
766 
using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N]) 

767 
then have "simple_integral (\<lambda>x. u x * indicator N x) = simple_integral (\<lambda>x. 0)" 

768 
using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2) 

769 
then show ?thesis by simp 

38656  770 
qed 
35582  771 

40859  772 
lemma (in measure_space) simple_integral_cong_AE_mult_indicator: 
773 
assumes sf: "simple_function f" and eq: "AE x. x \<in> S" and "S \<in> sets M" 

774 
shows "simple_integral f = simple_integral (\<lambda>x. f x * indicator S x)" 

775 
proof (rule simple_integral_cong_AE) 

776 
show "simple_function f" by fact 

777 
show "simple_function (\<lambda>x. f x * indicator S x)" 

778 
using sf `S \<in> sets M` by auto 

779 
from eq show "AE x. f x = f x * indicator S x" 

780 
by (rule AE_mp) simp 

35582  781 
qed 
782 

39092  783 
lemma (in measure_space) simple_integral_restricted: 
784 
assumes "A \<in> sets M" 

785 
assumes sf: "simple_function (\<lambda>x. f x * indicator A x)" 

786 
shows "measure_space.simple_integral (restricted_space A) \<mu> f = simple_integral (\<lambda>x. f x * indicator A x)" 

787 
(is "_ = simple_integral ?f") 

788 
unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]] 

789 
unfolding simple_integral_def 

790 
proof (simp, safe intro!: setsum_mono_zero_cong_left) 

791 
from sf show "finite (?f ` space M)" 

792 
unfolding simple_function_def by auto 

793 
next 

794 
fix x assume "x \<in> A" 

795 
then show "f x \<in> ?f ` space M" 

796 
using sets_into_space `A \<in> sets M` by (auto intro!: image_eqI[of _ _ x]) 

797 
next 

798 
fix x assume "x \<in> space M" "?f x \<notin> f`A" 

799 
then have "x \<notin> A" by (auto simp: image_iff) 

800 
then show "?f x * \<mu> (?f ` {?f x} \<inter> space M) = 0" by simp 

801 
next 

802 
fix x assume "x \<in> A" 

803 
then have "f x \<noteq> 0 \<Longrightarrow> 

804 
f ` {f x} \<inter> A = ?f ` {f x} \<inter> space M" 

805 
using `A \<in> sets M` sets_into_space 

806 
by (auto simp: indicator_def split: split_if_asm) 

807 
then show "f x * \<mu> (f ` {f x} \<inter> A) = 

808 
f x * \<mu> (?f ` {f x} \<inter> space M)" 

809 
unfolding pinfreal_mult_cancel_left by auto 

810 
qed 

811 

812 
lemma (in measure_space) simple_integral_subalgebra[simp]: 

813 
assumes "measure_space (M\<lparr>sets := N\<rparr>) \<mu>" 

814 
shows "measure_space.simple_integral (M\<lparr>sets := N\<rparr>) \<mu> = simple_integral" 

815 
unfolding simple_integral_def_raw 

816 
unfolding measure_space.simple_integral_def_raw[OF assms] by simp 

817 

40859  818 
lemma (in measure_space) simple_integral_vimage: 
819 
fixes g :: "'a \<Rightarrow> pinfreal" and f :: "'d \<Rightarrow> 'a" 

820 
assumes f: "bij_betw f S (space M)" 

821 
shows "simple_integral g = 

822 
measure_space.simple_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))" 

823 
(is "_ = measure_space.simple_integral ?T ?\<mu> _") 

824 
proof  

825 
from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic) 

826 
have surj: "f`S = space M" 

827 
using f unfolding bij_betw_def by simp 

828 
have *: "(\<lambda>x. g (f x)) ` S = g ` f ` S" by auto 

829 
have **: "f`S = space M" using f unfolding bij_betw_def by auto 

830 
{ fix x assume "x \<in> space M" 

831 
have "(f ` ((\<lambda>x. g (f x)) ` {g x} \<inter> S)) = 

832 
(f ` (f ` (g ` {g x}) \<inter> S))" by auto 

833 
also have "f ` (g ` {g x}) \<inter> S = f ` (g ` {g x} \<inter> space M) \<inter> S" 

834 
using f unfolding bij_betw_def by auto 

835 
also have "(f ` (f ` (g ` {g x} \<inter> space M) \<inter> S)) = g ` {g x} \<inter> space M" 

836 
using ** by (intro image_vimage_inter_eq) auto 

837 
finally have "(f ` ((\<lambda>x. g (f x)) ` {g x} \<inter> S)) = g ` {g x} \<inter> space M" by auto } 

838 
then show ?thesis using assms 

839 
unfolding simple_integral_def T.simple_integral_def bij_betw_def 

840 
by (auto simp add: * intro!: setsum_cong) 

841 
qed 

842 

35692  843 
section "Continuous posititve integration" 
844 

38656  845 
definition (in measure_space) 
40873  846 
"positive_integral f = SUPR {g. simple_function g \<and> g \<le> f} simple_integral" 
40872  847 

38656  848 
lemma (in measure_space) positive_integral_alt: 
849 
"positive_integral f = 

40873  850 
(SUPR {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M} simple_integral)" (is "_ = ?alt") 
40872  851 
proof (rule antisym SUP_leI) 
40873  852 
show "positive_integral f \<le> ?alt" unfolding positive_integral_def 
40872  853 
proof (safe intro!: SUP_leI) 
854 
fix g assume g: "simple_function g" "g \<le> f" 

855 
let ?G = "g ` {\<omega>} \<inter> space M" 

856 
show "simple_integral g \<le> 

857 
SUPR {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g ` space M} simple_integral" 

858 
(is "simple_integral g \<le> SUPR ?A simple_integral") 

859 
proof cases 

860 
let ?g = "\<lambda>x. indicator (space M  ?G) x * g x" 

861 
have g': "simple_function ?g" 

862 
using g by (auto intro: simple_functionD) 

863 
moreover 

864 
assume "\<mu> ?G = 0" 

865 
then have "AE x. g x = ?g x" using g 

866 
by (intro AE_I[where N="?G"]) 

867 
(auto intro: simple_functionD simp: indicator_def) 

868 
with g(1) g' have "simple_integral g = simple_integral ?g" 

869 
by (rule simple_integral_cong_AE) 

870 
moreover have "?g \<le> g" by (auto simp: le_fun_def indicator_def) 

871 
from this `g \<le> f` have "?g \<le> f" by (rule order_trans) 

872 
moreover have "\<omega> \<notin> ?g ` space M" 

873 
by (auto simp: indicator_def split: split_if_asm) 

874 
ultimately show ?thesis by (auto intro!: le_SUPI) 

875 
next 

876 
assume "\<mu> ?G \<noteq> 0" 

877 
then have "?G \<noteq> {}" by auto 

878 
then have "\<omega> \<in> g`space M" by force 

879 
then have "space M \<noteq> {}" by auto 

880 
have "SUPR ?A simple_integral = \<omega>" 

881 
proof (intro SUP_\<omega>[THEN iffD2] allI impI) 

882 
fix x assume "x < \<omega>" 

883 
then guess n unfolding less_\<omega>_Ex_of_nat .. note n = this 

884 
then have "0 < n" by (intro neq0_conv[THEN iffD1] notI) simp 

885 
let ?g = "\<lambda>x. (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * indicator ?G x" 

886 
show "\<exists>i\<in>?A. x < simple_integral i" 

887 
proof (intro bexI impI CollectI conjI) 

888 
show "simple_function ?g" using g 

889 
by (auto intro!: simple_functionD simple_function_add) 

890 
have "?g \<le> g" by (auto simp: le_fun_def indicator_def) 

891 
from this g(2) show "?g \<le> f" by (rule order_trans) 

892 
show "\<omega> \<notin> ?g ` space M" 

893 
using `\<mu> ?G \<noteq> 0` by (auto simp: indicator_def split: split_if_asm) 

894 
have "x < (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * \<mu> ?G" 

895 
using n `\<mu> ?G \<noteq> 0` `0 < n` 

896 
by (auto simp: pinfreal_noteq_omega_Ex field_simps) 

897 
also have "\<dots> = simple_integral ?g" using g `space M \<noteq> {}` 

898 
by (subst simple_integral_indicator) 

899 
(auto simp: image_constant ac_simps dest: simple_functionD) 

900 
finally show "x < simple_integral ?g" . 

901 
qed 

902 
qed 

903 
then show ?thesis by simp 

904 
qed 

35582  905 
qed 
40872  906 
qed (auto intro!: SUP_subset simp: positive_integral_def) 
35582  907 

40873  908 
lemma (in measure_space) positive_integral_cong_measure: 
909 
assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A" 

910 
shows "measure_space.positive_integral M \<nu> f = positive_integral f" 

911 
proof  

912 
interpret v: measure_space M \<nu> 

913 
by (rule measure_space_cong) fact 

914 
with assms show ?thesis 

915 
unfolding positive_integral_def v.positive_integral_def SUPR_def 

916 
by (auto intro!: arg_cong[where f=Sup] image_cong 

917 
simp: simple_integral_cong_measure[of \<nu>]) 

918 
qed 

919 

920 
lemma (in measure_space) positive_integral_alt1: 

921 
"positive_integral f = 

922 
(SUP g : {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}. simple_integral g)" 

923 
unfolding positive_integral_alt SUPR_def 

924 
proof (safe intro!: arg_cong[where f=Sup]) 

925 
fix g let ?g = "\<lambda>x. if x \<in> space M then g x else f x" 

926 
assume "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>" 

927 
hence "?g \<le> f" "simple_function ?g" "simple_integral g = simple_integral ?g" 

928 
"\<omega> \<notin> g`space M" 

929 
unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) 

930 
thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}" 

931 
by auto 

932 
next 

933 
fix g assume "simple_function g" "g \<le> f" "\<omega> \<notin> g`space M" 

934 
hence "simple_function g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>" 

935 
by (auto simp add: le_fun_def image_iff) 

936 
thus "simple_integral g \<in> simple_integral ` {g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}" 

937 
by auto 

938 
qed 

939 

38656  940 
lemma (in measure_space) positive_integral_cong: 
941 
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x" 

942 
shows "positive_integral f = positive_integral g" 

943 
proof  

944 
have "\<And>h. (\<forall>x\<in>space M. h x \<le> f x \<and> h x \<noteq> \<omega>) = (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>)" 

945 
using assms by auto 

946 
thus ?thesis unfolding positive_integral_alt1 by auto 

947 
qed 

948 

949 
lemma (in measure_space) positive_integral_eq_simple_integral: 

950 
assumes "simple_function f" 

951 
shows "positive_integral f = simple_integral f" 

40873  952 
unfolding positive_integral_def 
38656  953 
proof (safe intro!: pinfreal_SUPI) 
954 
fix g assume "simple_function g" "g \<le> f" 

955 
with assms show "simple_integral g \<le> simple_integral f" 

956 
by (auto intro!: simple_integral_mono simp: le_fun_def) 

957 
next 

958 
fix y assume "\<forall>x. x\<in>{g. simple_function g \<and> g \<le> f} \<longrightarrow> simple_integral x \<le> y" 

959 
with assms show "simple_integral f \<le> y" by auto 

960 
qed 

35582  961 

40859  962 
lemma (in measure_space) positive_integral_mono_AE: 
963 
assumes ae: "AE x. u x \<le> v x" 

38656  964 
shows "positive_integral u \<le> positive_integral v" 
965 
unfolding positive_integral_alt1 

966 
proof (safe intro!: SUPR_mono) 

40859  967 
fix a assume a: "simple_function a" and mono: "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>" 
968 
from ae obtain N where N: "{x\<in>space M. \<not> u x \<le> v x} \<subseteq> N" "N \<in> sets M" "\<mu> N = 0" 

969 
by (auto elim!: AE_E) 

970 
have "simple_function (\<lambda>x. a x * indicator (space M  N) x)" 

971 
using `N \<in> sets M` a by auto 

972 
with a show "\<exists>b\<in>{g. simple_function g \<and> (\<forall>x\<in>space M. g x \<le> v x \<and> g x \<noteq> \<omega>)}. 

973 
simple_integral a \<le> simple_integral b" 

974 
proof (safe intro!: bexI[of _ "\<lambda>x. a x * indicator (space M  N) x"] 

975 
simple_integral_mono_AE) 

976 
show "AE x. a x \<le> a x * indicator (space M  N) x" 

977 
proof (rule AE_I, rule subset_refl) 

978 
have *: "{x \<in> space M. \<not> a x \<le> a x * indicator (space M  N) x} = 

979 
N \<inter> {x \<in> space M. a x \<noteq> 0}" (is "?N = _") 

980 
using `N \<in> sets M`[THEN sets_into_space] by (auto simp: indicator_def) 

981 
then show "?N \<in> sets M" 

982 
using `N \<in> sets M` `simple_function a`[THEN borel_measurable_simple_function] 

983 
by (auto intro!: measure_mono Int) 

984 
then have "\<mu> ?N \<le> \<mu> N" 

985 
unfolding * using `N \<in> sets M` by (auto intro!: measure_mono) 

986 
then show "\<mu> ?N = 0" using `\<mu> N = 0` by auto 

987 
qed 

988 
next 

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

990 
show "a x * indicator (space M  N) x \<le> v x" 

991 
proof (cases "x \<in> N") 

992 
case True then show ?thesis by simp 

993 
next 

994 
case False 

995 
with N mono have "a x \<le> u x" "u x \<le> v x" using `x \<in> space M` by auto 

996 
with False `x \<in> space M` show "a x * indicator (space M  N) x \<le> v x" by auto 

997 
qed 

998 
assume "a x * indicator (space M  N) x = \<omega>" 

999 
with mono `x \<in> space M` show False 

1000 
by (simp split: split_if_asm add: indicator_def) 

1001 
qed 

1002 
qed 

1003 

1004 
lemma (in measure_space) positive_integral_cong_AE: 

1005 
"AE x. u x = v x \<Longrightarrow> positive_integral u = positive_integral v" 

1006 
by (auto simp: eq_iff intro!: positive_integral_mono_AE) 

1007 

1008 
lemma (in measure_space) positive_integral_mono: 

1009 
assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x" 

1010 
shows "positive_integral u \<le> positive_integral v" 

1011 
using mono by (auto intro!: AE_cong positive_integral_mono_AE) 

1012 

40873  1013 
lemma image_set_cong: 
1014 
assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y" 

1015 
assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. g y = f x" 

1016 
shows "f ` A = g ` B" 

1017 
using assms by blast 

1018 

40859  1019 
lemma (in measure_space) positive_integral_vimage: 
1020 
fixes g :: "'a \<Rightarrow> pinfreal" and f :: "'d \<Rightarrow> 'a" 

1021 
assumes f: "bij_betw f S (space M)" 

1022 
shows "positive_integral g = 

1023 
measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>x. g (f x))" 

1024 
(is "_ = measure_space.positive_integral ?T ?\<mu> _") 

1025 
proof  

1026 
from f interpret T: measure_space ?T ?\<mu> by (rule measure_space_isomorphic) 

1027 
have f_fun: "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto 

1028 
from assms have inv: "bij_betw (the_inv_into S f) (space M) S" 

1029 
by (rule bij_betw_the_inv_into) 

1030 
then have inv_fun: "the_inv_into S f \<in> space M \<rightarrow> S" unfolding bij_betw_def by auto 

1031 
have surj: "f`S = space M" 

1032 
using f unfolding bij_betw_def by simp 

1033 
have inj: "inj_on f S" 

1034 
using f unfolding bij_betw_def by simp 

1035 
have inv_f: "\<And>x. x \<in> space M \<Longrightarrow> f (the_inv_into S f x) = x" 

1036 
using f_the_inv_into_f[of f S] f unfolding bij_betw_def by auto 

1037 
from simple_integral_vimage[OF assms, symmetric] 

1038 
have *: "simple_integral = T.simple_integral \<circ> (\<lambda>g. g \<circ> f)" by (simp add: comp_def) 

1039 
show ?thesis 

1040 
unfolding positive_integral_alt1 T.positive_integral_alt1 SUPR_def * image_compose 

1041 
proof (safe intro!: arg_cong[where f=Sup] image_set_cong, simp_all add: comp_def) 

1042 
fix g' :: "'a \<Rightarrow> pinfreal" assume "simple_function g'" "\<forall>x\<in>space M. g' x \<le> g x \<and> g' x \<noteq> \<omega>" 

1043 
then show "\<exists>h. T.simple_function h \<and> (\<forall>x\<in>S. h x \<le> g (f x) \<and> h x \<noteq> \<omega>) \<and> 

1044 
T.simple_integral (\<lambda>x. g' (f x)) = T.simple_integral h" 

1045 
using f unfolding bij_betw_def 

1046 
by (auto intro!: exI[of _ "\<lambda>x. g' (f x)"] 

1047 
simp add: le_fun_def simple_function_vimage[OF _ f_fun]) 

1048 
next 

1049 
fix g' :: "'d \<Rightarrow> pinfreal" assume g': "T.simple_function g'" "\<forall>x\<in>S. g' x \<le> g (f x) \<and> g' x \<noteq> \<omega>" 

1050 
let ?g = "\<lambda>x. g' (the_inv_into S f x)" 

1051 
show "\<exists>h. simple_function h \<and> (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>) \<and> 

1052 
T.simple_integral g' = T.simple_integral (\<lambda>x. h (f x))" 

1053 
proof (intro exI[of _ ?g] conjI ballI) 

1054 
{ fix x assume x: "x \<in> space M" 

1055 
then have "the_inv_into S f x \<in> S" using inv_fun by auto 

1056 
with g' have "g' (the_inv_into S f x) \<le> g (f (the_inv_into S f x)) \<and> g' (the_inv_into S f x) \<noteq> \<omega>" 

1057 
by auto 

1058 
then show "g' (the_inv_into S f x) \<le> g x" "g' (the_inv_into S f x) \<noteq> \<omega>" 

1059 
using f_the_inv_into_f[of f S x] x f unfolding bij_betw_def by auto } 

1060 
note vimage_vimage_inv[OF f inv_f inv_fun, simp] 

1061 
from T.simple_function_vimage[OF g'(1), unfolded space_vimage_algebra, OF inv_fun] 

1062 
show "simple_function (\<lambda>x. g' (the_inv_into S f x))" 

1063 
unfolding simple_function_def by (simp add: simple_function_def) 

1064 
show "T.simple_integral g' = T.simple_integral (\<lambda>x. ?g (f x))" 

1065 
using the_inv_into_f_f[OF inj] by (auto intro!: T.simple_integral_cong) 

1066 
qed 

1067 
qed 

1068 
qed 

1069 

1070 
lemma (in measure_space) positive_integral_vimage_inv: 

1071 
fixes g :: "'d \<Rightarrow> pinfreal" and f :: "'d \<Rightarrow> 'a" 

1072 
assumes f: "bij_betw f S (space M)" 

1073 
shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g = 

1074 
positive_integral (\<lambda>x. g (the_inv_into S f x))" 

1075 
proof  

1076 
interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)" 

1077 
using f by (rule measure_space_isomorphic) 

1078 
show ?thesis 

1079 
unfolding positive_integral_vimage[OF f, of "\<lambda>x. g (the_inv_into S f x)"] 

1080 
using f[unfolded bij_betw_def] 

1081 
by (auto intro!: v.positive_integral_cong simp: the_inv_into_f_f) 

38656  1082 
qed 
1083 

1084 
lemma (in measure_space) positive_integral_SUP_approx: 

1085 
assumes "f \<up> s" 

1086 
and f: "\<And>i. f i \<in> borel_measurable M" 

1087 
and "simple_function u" 

1088 
and le: "u \<le> s" and real: "\<omega> \<notin> u`space M" 

1089 
shows "simple_integral u \<le> (SUP i. positive_integral (f i))" (is "_ \<le> ?S") 

1090 
proof (rule pinfreal_le_mult_one_interval) 

1091 
fix a :: pinfreal assume "0 < a" "a < 1" 

1092 
hence "a \<noteq> 0" by auto 

1093 
let "?B i" = "{x \<in> space M. a * u x \<le> f i x}" 

1094 
have B: "\<And>i. ?B i \<in> sets M" 

1095 
using f `simple_function u` by (auto simp: borel_measurable_simple_function) 

1096 

1097 
let "?uB i x" = "u x * indicator (?B i) x" 

1098 

1099 
{ fix i have "?B i \<subseteq> ?B (Suc i)" 

1100 
proof safe 

1101 
fix i x assume "a * u x \<le> f i x" 

1102 
also have "\<dots> \<le> f (Suc i) x" 

1103 
using `f \<up> s` unfolding isoton_def le_fun_def by auto 

1104 
finally show "a * u x \<le> f (Suc i) x" . 

1105 
qed } 

1106 
note B_mono = this 

35582  1107 

38656  1108 
have u: "\<And>x. x \<in> space M \<Longrightarrow> u ` {u x} \<inter> space M \<in> sets M" 
1109 
using `simple_function u` by (auto simp add: simple_function_def) 

1110 

40859  1111 
have "\<And>i. (\<lambda>n. (u ` {i} \<inter> space M) \<inter> ?B n) \<up> (u ` {i} \<inter> space M)" using B_mono unfolding isoton_def 
1112 
proof safe 

1113 
fix x i assume "x \<in> space M" 

1114 
show "x \<in> (\<Union>i. (u ` {u x} \<inter> space M) \<inter> ?B i)" 

1115 
proof cases 

1116 
assume "u x = 0" thus ?thesis using `x \<in> space M` by simp 

1117 
next 

1118 
assume "u x \<noteq> 0" 

1119 
with `a < 1` real `x \<in> space M` 

1120 
have "a * u x < 1 * u x" by (rule_tac pinfreal_mult_strict_right_mono) (auto simp: image_iff) 

1121 
also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s` 

1122 
unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def) 

1123 
finally obtain i where "a * u x < f i x" unfolding SUPR_def 

1124 
by (auto simp add: less_Sup_iff) 

1125 
hence "a * u x \<le> f i x" by auto 

1126 
thus ?thesis using `x \<in> space M` by auto 

1127 
qed 

1128 
qed auto 

1129 
note measure_conv = measure_up[OF Int[OF u B] this] 

38656  1130 

1131 
have "simple_integral u = (SUP i. simple_integral (?uB i))" 

1132 
unfolding simple_integral_indicator[OF B `simple_function u`] 

1133 
proof (subst SUPR_pinfreal_setsum, safe) 

1134 
fix x n assume "x \<in> space M" 

1135 
have "\<mu> (u ` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x}) 

1136 
\<le> \<mu> (u ` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f (Suc n) x})" 

1137 
using B_mono Int[OF u[OF `x \<in> space M`] B] by (auto intro!: measure_mono) 

1138 
thus "u x * \<mu> (u ` {u x} \<inter> space M \<inter> ?B n) 

1139 
\<le> u x * \<mu> (u ` {u x} \<inter> space M \<inter> ?B (Suc n))" 

1140 
by (auto intro: mult_left_mono) 

1141 
next 

1142 
show "simple_integral u = 

1143 
(\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (u ` {i} \<inter> space M \<inter> ?B n))" 

1144 
using measure_conv unfolding simple_integral_def isoton_def 

1145 
by (auto intro!: setsum_cong simp: pinfreal_SUP_cmult) 

1146 
qed 

1147 
moreover 

1148 
have "a * (SUP i. simple_integral (?uB i)) \<le> ?S" 

1149 
unfolding pinfreal_SUP_cmult[symmetric] 

38705  1150 
proof (safe intro!: SUP_mono bexI) 
38656  1151 
fix i 
1152 
have "a * simple_integral (?uB i) = simple_integral (\<lambda>x. a * ?uB i x)" 

1153 
using B `simple_function u` 

1154 
by (subst simple_integral_mult[symmetric]) (auto simp: field_simps) 

1155 
also have "\<dots> \<le> positive_integral (f i)" 

1156 
proof  

1157 
have "\<And>x. a * ?uB i x \<le> f i x" unfolding indicator_def by auto 

1158 
hence *: "simple_function (\<lambda>x. a * ?uB i x)" using B assms(3) 

1159 
by (auto intro!: simple_integral_mono) 

1160 
show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric] 

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

1162 
qed 

1163 
finally show "a * simple_integral (?uB i) \<le> positive_integral (f i)" 

1164 
by auto 

38705  1165 
qed simp 
38656  1166 
ultimately show "a * simple_integral u \<le> ?S" by simp 
35582  1167 
qed 
1168 

1169 
text {* BeppoLevi monotone convergence theorem *} 

38656  1170 
lemma (in measure_space) positive_integral_isoton: 
1171 
assumes "f \<up> u" "\<And>i. f i \<in> borel_measurable M" 

1172 
shows "(\<lambda>i. positive_integral (f i)) \<up> positive_integral u" 

1173 
unfolding isoton_def 

1174 
proof safe 

1175 
fix i show "positive_integral (f i) \<le> positive_integral (f (Suc i))" 

1176 
apply (rule positive_integral_mono) 

1177 
using `f \<up> u` unfolding isoton_def le_fun_def by auto 

1178 
next 

1179 
have "u \<in> borel_measurable M" 

1180 
using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def) 

1181 
have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto 

35582  1182 

38656  1183 
show "(SUP i. positive_integral (f i)) = positive_integral u" 
1184 
proof (rule antisym) 

1185 
from `f \<up> u`[THEN isoton_Sup, unfolded le_fun_def] 

1186 
show "(SUP j. positive_integral (f j)) \<le> positive_integral u" 

1187 
by (auto intro!: SUP_leI positive_integral_mono) 

1188 
next 

1189 
show "positive_integral u \<le> (SUP i. positive_integral (f i))" 

40873  1190 
unfolding positive_integral_alt[of u] 
38656  1191 
by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) 
35582  1192 
qed 
1193 
qed 

1194 

40859  1195 
lemma (in measure_space) positive_integral_monotone_convergence_SUP: 
1196 
assumes "\<And>i x. x \<in> space M \<Longrightarrow> f i x \<le> f (Suc i) x" 

1197 
assumes "\<And>i. f i \<in> borel_measurable M" 

1198 
shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)" 

1199 
(is "_ = positive_integral ?u") 

1200 
proof  

1201 
have "?u \<in> borel_measurable M" 

1202 
using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand) 

1203 
show ?thesis 

1204 
proof (rule antisym) 

1205 
show "(SUP j. positive_integral (f j)) \<le> positive_integral ?u" 

1206 
by (auto intro!: SUP_leI positive_integral_mono le_SUPI) 

1207 
next 

1208 
def rf \<equiv> "\<lambda>i. \<lambda>x\<in>space M. f i x" and ru \<equiv> "\<lambda>x\<in>space M. ?u x" 

1209 
have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def 

1210 
using assms by (simp cong: measurable_cong) 

1211 
moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def 

1212 
unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff 

40872  1213 
using SUP_const[OF UNIV_not_empty] 
40859  1214 
by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff) 
1215 
ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))" 

40873  1216 
unfolding positive_integral_alt[of ru] 
40859  1217 
by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx) 
1218 
then show "positive_integral ?u \<le> (SUP i. positive_integral (f i))" 

1219 
unfolding ru_def rf_def by (simp cong: positive_integral_cong) 

1220 
qed 

1221 
qed 

de0b30e6c2d2
Support product spaces on sigma finite measures.
hoe 