author  hoelzl 
Mon, 24 Jan 2011 22:29:50 +0100  
changeset 41661  baf1964bc468 
parent 41545  9c869baf1c66 
child 41689  3e39b0e730d6 
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: 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

57 
fixes f ::"'a \<Rightarrow> pextreal" 
38656  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: 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

72 
"simple_function (\<lambda>x. h x * indicator ( space M) x::pextreal)" (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: 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

215 
fixes u :: "'a \<Rightarrow> pextreal" 
38656  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 

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

268 
let "?g j x" = "of_nat (f x j) / 2^j :: pextreal" 
38656  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" 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

353 
proof (rule pextreal_SUPI) 
38656  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 

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

365 
fix y :: pextreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y" 
38656  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': 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

407 
fixes u :: "'a \<Rightarrow> pextreal" 
38656  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: 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

419 
fixes f :: "'a \<Rightarrow> pextreal" 
39092  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: 

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

427 
fixes f :: "'a \<Rightarrow> pextreal" assumes "A \<in> sets M" 
39092  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 

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

451 
assume "indicator A x \<noteq> (0::pextreal)" 
39092  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: 

41545  466 
assumes "sigma_algebra.simple_function N f" 
467 
and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M" "sigma_algebra N" 

39092  468 
shows "simple_function f" 
469 
using assms 

470 
unfolding simple_function_def 

41545  471 
unfolding sigma_algebra.simple_function_def[OF N_subalgebra(3)] 
39092  472 
by auto 
473 

41661  474 
lemma (in measure_space) simple_function_vimage: 
475 
assumes T: "sigma_algebra M'" "T \<in> measurable M M'" 

476 
and f: "sigma_algebra.simple_function M' f" 

477 
shows "simple_function (\<lambda>x. f (T x))" 

478 
proof (intro simple_function_def[THEN iffD2] conjI ballI) 

479 
interpret T: sigma_algebra M' by fact 

480 
have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'" 

481 
using T unfolding measurable_def by auto 

482 
then show "finite ((\<lambda>x. f (T x)) ` space M)" 

483 
using f unfolding T.simple_function_def by (auto intro: finite_subset) 

484 
fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M" 

485 
then have "i \<in> f ` space M'" 

486 
using T unfolding measurable_def by auto 

487 
then have "f ` {i} \<inter> space M' \<in> sets M'" 

488 
using f unfolding T.simple_function_def by auto 

489 
then have "T ` (f ` {i} \<inter> space M') \<inter> space M \<in> sets M" 

490 
using T unfolding measurable_def by auto 

491 
also have "T ` (f ` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) ` {i} \<inter> space M" 

492 
using T unfolding measurable_def by auto 

493 
finally show "(\<lambda>x. f (T x)) ` {i} \<inter> space M \<in> sets M" . 

40859  494 
qed 
495 

38656  496 
section "Simple integral" 
497 

41544  498 
definition (in measure_space) simple_integral (binder "\<integral>\<^isup>S " 10) where 
38656  499 
"simple_integral f = (\<Sum>x \<in> f ` space M. x * \<mu> (f ` {x} \<inter> space M))" 
35582  500 

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

503 
shows "simple_integral f = simple_integral g" 

504 
proof  

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

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

507 
using assms by (auto intro!: image_eqI) 

508 
thus ?thesis unfolding simple_integral_def by simp 

509 
qed 

510 

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

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

514 
proof  

515 
interpret v: measure_space M \<nu> 

516 
by (rule measure_space_cong) fact 

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

520 
qed 

521 

38656  522 
lemma (in measure_space) simple_integral_const[simp]: 
41544  523 
"(\<integral>\<^isup>Sx. c) = c * \<mu> (space M)" 
38656  524 
proof (cases "space M = {}") 
525 
case True thus ?thesis unfolding simple_integral_def by simp 

526 
next 

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

528 
thus ?thesis unfolding simple_integral_def by simp 

35582  529 
qed 
530 

38656  531 
lemma (in measure_space) simple_function_partition: 
532 
assumes "simple_function f" and "simple_function g" 

39910  533 
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  534 
(is "_ = setsum _ (?p ` space M)") 
535 
proof 

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

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

35582  538 

38656  539 
have [intro]: 
540 
"finite (f ` space M)" 

541 
"finite (g ` space M)" 

542 
using assms unfolding simple_function_def by simp_all 

543 

544 
{ fix A 

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

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

547 
by auto 

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

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

549 
by (rule finite_subset) auto } 
38656  550 
note this[intro, simp] 
35582  551 

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

554 
moreover { 

555 
fix x y 

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

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

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

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

560 
using assms unfolding simple_function_def * by auto } 

561 
ultimately 

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

563 
by (subst measure_finitely_additive) auto } 

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

565 
unfolding simple_integral_def 

566 
by (subst setsum_Sigma[symmetric], 

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

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

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

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

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

578 
thus ?thesis 

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

582 
qed 

583 
finally show ?thesis . 

35582  584 
qed 
585 

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

41544  588 
shows "(\<integral>\<^isup>Sx. f x + g x) = simple_integral f + simple_integral g" 
35582  589 
proof  
38656  590 
{ fix x let ?S = "g ` {g x} \<inter> f ` {f x} \<inter> space M" 
591 
assume "x \<in> space M" 

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

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

594 
by auto } 

595 
thus ?thesis 

596 
unfolding 

597 
simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]] 

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

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

600 
apply (subst (3) Int_commute) 

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

35582  602 
qed 
603 

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

41544  606 
shows "(\<integral>\<^isup>Sx. \<Sum>i\<in>P. f i x) = (\<Sum>i\<in>P. simple_integral (f i))" 
38656  607 
proof cases 
608 
assume "finite P" 

609 
from this assms show ?thesis 

610 
by induct (auto simp: simple_function_setsum simple_integral_add) 

611 
qed auto 

612 

613 
lemma (in measure_space) simple_integral_mult[simp]: 

614 
assumes "simple_function f" 

41544  615 
shows "(\<integral>\<^isup>Sx. c * f x) = c * simple_integral f" 
38656  616 
proof  
617 
note mult = simple_function_mult[OF simple_function_const[of c] assms] 

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

619 
assume "x \<in> space M" 

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

621 
by auto } 

622 
thus ?thesis 

623 
unfolding simple_function_partition[OF mult assms] 

624 
simple_function_partition[OF assms mult] 

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

35582  626 
qed 
627 

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

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

631 
proof  

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

633 
show ?thesis unfolding simple_function_def 

634 
proof safe 

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

636 
from finite_subset[OF this] assms 

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

638 
next 

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

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

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

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

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

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

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

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

647 
qed 

648 
qed 

649 

40859  650 
lemma (in measure_space) simple_integral_mono_AE: 
651 
assumes "simple_function f" and "simple_function g" 

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

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

654 
proof  

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

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

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

658 
show ?thesis 

659 
unfolding * 

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

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

662 
proof (safe intro!: setsum_mono) 

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

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

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

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

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

668 
next 

669 
case False 

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

671 
using mono by (auto elim!: AE_E) 

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

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

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

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

678 
qed 

679 
qed 

680 
qed 

681 

38656  682 
lemma (in measure_space) simple_integral_mono: 
683 
assumes "simple_function f" and "simple_function g" 

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

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

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

688 
using mono by (rule AE_cong) auto 

35582  689 
qed 
690 

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

693 
shows "simple_integral f = simple_integral g" 

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

695 

696 
lemma (in measure_space) simple_integral_cong': 

697 
assumes sf: "simple_function f" "simple_function g" 

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

699 
shows "simple_integral f = simple_integral g" 

700 
proof (intro simple_integral_cong_AE sf AE_I) 

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

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

703 
using sf[THEN borel_measurable_simple_function] by auto 

704 
qed simp 

705 

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

708 
assumes "simple_function f" 

41544  709 
shows "(\<integral>\<^isup>Sx. f x * indicator A x) = 
38656  710 
(\<Sum>x \<in> f ` space M. x * \<mu> (f ` {x} \<inter> space M \<inter> A))" 
711 
proof cases 

712 
assume "A = space M" 

41544  713 
moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x) = simple_integral f" 
38656  714 
by (auto intro!: simple_integral_cong) 
715 
moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto 

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

717 
next 

718 
assume "A \<noteq> space M" 

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

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

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

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

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

726 
next 

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

35582  728 
qed 
41544  729 
have *: "(\<integral>\<^isup>Sx. f x * indicator A x) = 
38656  730 
(\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f ` {x} \<inter> space M \<inter> A))" 
731 
unfolding simple_integral_def I 

732 
proof (rule setsum_mono_zero_cong_left) 

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

734 
using assms(2) unfolding simple_function_def by auto 

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

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

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

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

741 
next 

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

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

744 
by (auto simp: indicator_def split: split_if_asm) 

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

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

747 
qed 

748 
show ?thesis unfolding * 

749 
using assms(2) unfolding simple_function_def 

750 
by (auto intro!: setsum_mono_zero_cong_right) 

751 
qed 

35582  752 

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

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

756 
proof cases 

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

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

759 
next 

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

760 
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pextreal}" by auto 
38656  761 
thus ?thesis 
762 
using simple_integral_indicator[OF assms simple_function_const[of 1]] 

763 
using sets_into_space[OF assms] 

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

765 
qed 

35582  766 

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

41544  769 
shows "(\<integral>\<^isup>Sx. u x * indicator N x) = 0" 
38656  770 
proof  
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

771 
have "AE x. indicator N x = (0 :: pextreal)" 
40859  772 
using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N]) 
41544  773 
then have "(\<integral>\<^isup>Sx. u x * indicator N x) = (\<integral>\<^isup>Sx. 0)" 
40859  774 
using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2) 
775 
then show ?thesis by simp 

38656  776 
qed 
35582  777 

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

41544  780 
shows "simple_integral f = (\<integral>\<^isup>Sx. f x * indicator S x)" 
40859  781 
proof (rule simple_integral_cong_AE) 
782 
show "simple_function f" by fact 

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

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

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

786 
by (rule AE_mp) simp 

35582  787 
qed 
788 

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

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

41544  792 
shows "measure_space.simple_integral (restricted_space A) \<mu> f = (\<integral>\<^isup>Sx. f x * indicator A x)" 
39092  793 
(is "_ = simple_integral ?f") 
794 
unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]] 

795 
unfolding simple_integral_def 

796 
proof (simp, safe intro!: setsum_mono_zero_cong_left) 

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

798 
unfolding simple_function_def by auto 

799 
next 

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

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

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

803 
next 

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

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

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

807 
next 

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

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

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

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

812 
by (auto simp: indicator_def split: split_if_asm) 

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

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

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

815 
unfolding pextreal_mult_cancel_left by auto 
39092  816 
qed 
817 

41545  818 
lemma (in measure_space) simple_integral_subalgebra: 
819 
assumes N: "measure_space N \<mu>" and [simp]: "space N = space M" 

820 
shows "measure_space.simple_integral N \<mu> = simple_integral" 

39092  821 
unfolding simple_integral_def_raw 
41545  822 
unfolding measure_space.simple_integral_def_raw[OF N] by simp 
39092  823 

40859  824 
lemma (in measure_space) simple_integral_vimage: 
41661  825 
assumes T: "sigma_algebra M'" "T \<in> measurable M M'" 
826 
and f: "sigma_algebra.simple_function M' f" 

827 
shows "measure_space.simple_integral M' (\<lambda>A. \<mu> (T ` A \<inter> space M)) f = (\<integral>\<^isup>S x. f (T x))" 

828 
(is "measure_space.simple_integral M' ?nu f = _") 

40859  829 
proof  
41661  830 
interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto 
831 
show "T.simple_integral f = (\<integral>\<^isup>S x. f (T x))" 

832 
unfolding simple_integral_def T.simple_integral_def 

833 
proof (intro setsum_mono_zero_cong_right ballI) 

834 
show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'" 

835 
using T unfolding measurable_def by auto 

836 
show "finite (f ` space M')" 

837 
using f unfolding T.simple_function_def by auto 

838 
next 

839 
fix i assume "i \<in> f ` space M'  (\<lambda>x. f (T x)) ` space M" 

840 
then have "T ` (f ` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff) 

841 
then show "i * \<mu> (T ` (f ` {i} \<inter> space M') \<inter> space M) = 0" by simp 

842 
next 

843 
fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M" 

844 
then have "T ` (f ` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) ` {i} \<inter> space M" 

845 
using T unfolding measurable_def by auto 

846 
then show "i * \<mu> (T ` (f ` {i} \<inter> space M') \<inter> space M) = i * \<mu> ((\<lambda>x. f (T x)) ` {i} \<inter> space M)" 

847 
by auto 

848 
qed 

40859  849 
qed 
850 

35692  851 
section "Continuous posititve integration" 
852 

41544  853 
definition (in measure_space) positive_integral (binder "\<integral>\<^isup>+ " 10) where 
40873  854 
"positive_integral f = SUPR {g. simple_function g \<and> g \<le> f} simple_integral" 
40872  855 

38656  856 
lemma (in measure_space) positive_integral_alt: 
857 
"positive_integral f = 

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

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

864 
show "simple_integral g \<le> 

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

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

867 
proof cases 

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

869 
have g': "simple_function ?g" 

870 
using g by (auto intro: simple_functionD) 

871 
moreover 

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

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

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

875 
(auto intro: simple_functionD simp: indicator_def) 

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

877 
by (rule simple_integral_cong_AE) 

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

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

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

881 
by (auto simp: indicator_def split: split_if_asm) 

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

883 
next 

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

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

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

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

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

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

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

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

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

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

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

895 
proof (intro bexI impI CollectI conjI) 

896 
show "simple_function ?g" using g 

897 
by (auto intro!: simple_functionD simple_function_add) 

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

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

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

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

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

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

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

904 
by (auto simp: pextreal_noteq_omega_Ex field_simps) 
40872  905 
also have "\<dots> = simple_integral ?g" using g `space M \<noteq> {}` 
906 
by (subst simple_integral_indicator) 

907 
(auto simp: image_constant ac_simps dest: simple_functionD) 

908 
finally show "x < simple_integral ?g" . 

909 
qed 

910 
qed 

911 
then show ?thesis by simp 

912 
qed 

35582  913 
qed 
40872  914 
qed (auto intro!: SUP_subset simp: positive_integral_def) 
35582  915 

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

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

919 
proof  

920 
interpret v: measure_space M \<nu> 

921 
by (rule measure_space_cong) fact 

922 
with assms show ?thesis 

923 
unfolding positive_integral_def v.positive_integral_def SUPR_def 

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

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

926 
qed 

927 

928 
lemma (in measure_space) positive_integral_alt1: 

929 
"positive_integral f = 

930 
(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)" 

931 
unfolding positive_integral_alt SUPR_def 

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

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

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

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

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

937 
unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) 

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

939 
by auto 

940 
next 

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

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

943 
by (auto simp add: le_fun_def image_iff) 

944 
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>)}" 

945 
by auto 

946 
qed 

947 

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

950 
shows "positive_integral f = positive_integral g" 

951 
proof  

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

953 
using assms by auto 

954 
thus ?thesis unfolding positive_integral_alt1 by auto 

955 
qed 

956 

957 
lemma (in measure_space) positive_integral_eq_simple_integral: 

958 
assumes "simple_function f" 

959 
shows "positive_integral f = simple_integral f" 

40873  960 
unfolding positive_integral_def 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

961 
proof (safe intro!: pextreal_SUPI) 
38656  962 
fix g assume "simple_function g" "g \<le> f" 
963 
with assms show "simple_integral g \<le> simple_integral f" 

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

965 
next 

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

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

968 
qed 

35582  969 

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

38656  972 
shows "positive_integral u \<le> positive_integral v" 
973 
unfolding positive_integral_alt1 

974 
proof (safe intro!: SUPR_mono) 

40859  975 
fix a assume a: "simple_function a" and mono: "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>" 
976 
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" 

977 
by (auto elim!: AE_E) 

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

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

980 
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>)}. 

981 
simple_integral a \<le> simple_integral b" 

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

983 
simple_integral_mono_AE) 

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

985 
proof (rule AE_I, rule subset_refl) 

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

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

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

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

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

991 
by (auto intro!: measure_mono Int) 

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

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

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

995 
qed 

996 
next 

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

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

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

1000 
case True then show ?thesis by simp 

1001 
next 

1002 
case False 

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

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

1005 
qed 

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

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

1008 
by (simp split: split_if_asm add: indicator_def) 

1009 
qed 

1010 
qed 

1011 

1012 
lemma (in measure_space) positive_integral_cong_AE: 

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

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

1015 

1016 
lemma (in measure_space) positive_integral_mono: 

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

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

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

1020 

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

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

1024 
shows "f ` A = g ` B" 

1025 
using assms by blast 

1026 

38656  1027 
lemma (in measure_space) positive_integral_SUP_approx: 
1028 
assumes "f \<up> s" 

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

1030 
and "simple_function u" 

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

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

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

1033 
proof (rule pextreal_le_mult_one_interval) 
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset

1034 
fix a :: pextreal assume "0 < a" "a < 1" 
38656  1035 
hence "a \<noteq> 0" by auto 
1036 
let "?B i" = "{x \<in> space M. a * u x \<le> f i x}" 

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

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

1039 

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

1041 

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

1043 
proof safe 

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

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

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

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

1048 
qed } 

1049 
note B_mono = this 

35582  1050 

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

1053 

40859  1054 
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 
1055 
proof safe 

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

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

1058 
proof cases 

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

1060 
next 

1061 
assume "u x \<noteq> 0" 

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

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

1063 
have "a * u x < 1 * u x" by (rule_tac pextreal_mult_strict_right_mono) (auto simp: image_iff) 
40859  1064 
also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s` 
1065 
unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def) 

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

1067 
by (auto simp add: less_Sup_iff) 

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

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

1070 
qed 

1071 
qed auto 

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

38656  1073 

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

1075 
unfolding simple_integral_indicator[OF B `simple_function u`] 

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

1076 
proof (subst SUPR_pextreal_setsum, safe) 
38656  1077 
fix x n assume "x \<in> space M" 
1078 
have "\<mu> (u ` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x}) 

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

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

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

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

1083 
by (auto intro: mult_left_mono) 

1084 
next 

1085 
show "simple_integral u = 

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

1087 
using measure_conv unfolding simple_integral_def isoton_def 

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

1088 
by (auto intro!: setsum_cong simp: pextreal_SUP_cmult) 
38656  1089 
qed 
1090 
moreover 

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

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

1092 
unfolding pextreal_SUP_cmult[symmetric] 
38705  1093 
proof (safe intro!: SUP_mono bexI) 
38656  1094 
fix i 
41544  1095 
have "a * simple_integral (?uB i) = (\<integral>\<^isup>Sx. a * ?uB i x)" 
38656  1096 
using B `simple_function u` 
1097 
by (subst simple_integral_mult[symmetric]) (auto simp: field_simps) 

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

1099 
proof  

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

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

1102 
by (auto intro!: simple_integral_mono) 

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

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

1105 
qed 

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

1107 
by auto 

38705  1108 
qed simp 
38656  1109 
ultimately show "a * simple_integral u \<le> ?S" by simp 
35582  1110 
qed 
1111 

1112 
text {* BeppoLevi monotone convergence theorem *} 

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

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

1116 
unfolding isoton_def 

1117 
proof safe 

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

1119 
apply (rule positive_integral_mono) 

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

1121 
next 

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

35582  1123 

38656  1124 
show "(SUP i. positive_integral (f i)) = positive_integral u" 
1125 
proof (rule antisym) 

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

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

1128 
by (auto intro!: SUP_leI positive_integral_mono) 

1129 
next 

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

40873  1131 
unfolding positive_integral_alt[of u] 
38656  1132 
by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) 
35582  1133 
qed 
1134 
qed 

1135 

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

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

41544  1139 
shows "(SUP i. positive_integral (f i)) = (\<integral>\<^isup>+ x. SUP i. f i x)" 
40859  1140 
(is "_ = positive_integral ?u") 
1141 
proof  

1142 
show ?thesis 

1143 
proof (rule antisym) 

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

1145 
by (auto intro!: SUP_leI positive_integral_mono le_SUPI) 

1146 
next 

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

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

1149 
using assms by (simp cong: measurable_cong) 

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

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

1151 
unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply 
40872  1152 
using SUP_const[OF UNIV_not_empty] 
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset

1153 
by (auto simp: restrict_def le_fun_def fun_eq_iff) 
40859  1154 
ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))" 
40873  1155 
unfolding positive_integral_alt[of ru] 
40859  1156 
by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx) 
1157 
then show "positive_integral ?u \<le> (SUP i. positive_integral (f i))" 

1158 
unfolding ru_def rf_def by (simp cong: positive_integral_cong) 

1159 
qed 

1160 
qed 

1161 

38656  1162 
lemma (in measure_space) SUP_simple_integral_sequences: 
1163 
assumes f: "f \<up> u" "\<And>i. simple_function (f i)" 

1164 
and g: "g \<up> u" "\<And>i. simple_function (g i)" 

1165 
shows "(SUP i. simple_integral (f i)) = (SUP i. simple_integral (g i))" 

1166 
(is "SUPR _ ?F = SUPR _ ?G") 

1167 
proof  

1168 
have "(SUP i. ?F i) = (SUP i. positive_integral (f i))" 

1169 
using assms by (simp add: positive_integral_eq_simple_integral) 

1170 
also have "\<dots> = positive_integral u" 

1171 
using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]] 

1172 
unfolding isoton_def by simp 

1173 
also have "\<dots> = (SUP i. positive_integral (g i))" 

1174 
using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]] 

1175 
unfolding isoton_def by simp 

1176 
also have "\<dots> = (SUP i. ?G i)" 

1177 
using assms by (simp add: positive_integral_eq_simple_integral) 

1178 
finally show ?thesis . 

1179 
qed 

1180 

1181 
lemma (in measure_space) positive_integral_const[simp]: 

41544  1182 
"(\<integral>\<^isup>+ x. c) = c * \<mu> (space M)" 
38656  1183 
by (subst positive_integral_eq_simple_integral) auto 
1184 

1185 
lemma (in measure_space) positive_integral_isoton_simple: 

1186 
assumes "f \<up> u" and e: "\<And>i. simple_function (f i)" 

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

1188 
using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]] 

1189 
unfolding positive_integral_eq_simple_integral[OF e] . 

1190 

41661  1191 
lemma (in measure_space) positive_integral_vimage: 
1192 
assumes T: "sigma_algebra M'" "T \<in> measurable M M'" and f: "f \<in> borel_measurable M'" 

1193 
shows "measure_space.positive_integral M' (\<lambda>A. \<mu> (T ` A \<inter> space M)) f = (\<integral>\<^isup>+ x. f (T x))" 

1194 
(is "measure_space.positive_integral M' ?nu f = _") 

1195 
proof  

1196 
interpret T: measure_space M' ?nu using T by (rule measure_space_vimage) auto 

1197 
obtain f' where f': "f' \<up> f" "\<And>i. T.simple_function (f' i)" 

1198 
using T.borel_measurable_implies_simple_function_sequence[OF f] by blast 

1199 
then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function (\<lambda>x. f' i (T x))" 

1200 
using simple_function_vimage[OF T] unfolding isoton_fun_expand by auto 

1201 
show "T.positive_integral f = (\<integral>\<^isup>+ x. f (T x))" 

1202 
using positive_integral_isoton_simple[OF f] 

1203 
using T.positive_integral_isoton_simple[OF f'] 

1204 
unfolding simple_integral_vimage[OF T f'(2)] isoton_def 

1205 
by simp 

1206 
qed 

1207 

38656  1208 
lemma (in measure_space) positive_integral_linear: 
1209 
assumes f: "f \<in> borel_measurable M" 

1210 
and g: "g \<in> borel_measurable M" 

41544  1211 
shows "(\<integral>\<^isup>+ x. a * f x + g x) = 
38656  1212 