src/HOL/Probability/Lebesgue_Integration.thy
 author hoelzl Tue Mar 22 18:53:05 2011 +0100 (2011-03-22) changeset 42066 6db76c88907a parent 41981 cdf7693bbe08 child 42067 66c8281349ec permissions -rw-r--r--
generalized Caratheodory from algebra to ring_of_sets
1 (* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)
3 header {*Lebesgue Integration*}
5 theory Lebesgue_Integration
6 imports Measure Borel_Space
7 begin
9 lemma extreal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::extreal)"
10   unfolding indicator_def by auto
12 lemma tendsto_real_max:
13   fixes x y :: real
14   assumes "(X ---> x) net"
15   assumes "(Y ---> y) net"
16   shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
17 proof -
18   have *: "\<And>x y :: real. max x y = y + ((x - y) + norm (x - y)) / 2"
19     by (auto split: split_max simp: field_simps)
20   show ?thesis
21     unfolding *
22     by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto
23 qed
25 lemma (in measure_space) measure_Union:
26   assumes "finite S" "S \<subseteq> sets M" "\<And>A B. A \<in> S \<Longrightarrow> B \<in> S \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}"
27   shows "setsum \<mu> S = \<mu> (\<Union>S)"
28 proof -
29   have "setsum \<mu> S = \<mu> (\<Union>i\<in>S. i)"
30     using assms by (intro measure_setsum[OF `finite S`]) (auto simp: disjoint_family_on_def)
31   also have "\<dots> = \<mu> (\<Union>S)" by (auto intro!: arg_cong[where f=\<mu>])
32   finally show ?thesis .
33 qed
35 lemma (in sigma_algebra) measurable_sets2[intro]:
36   assumes "f \<in> measurable M M'" "g \<in> measurable M M''"
37   and "A \<in> sets M'" "B \<in> sets M''"
38   shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
39 proof -
40   have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
41     by auto
42   then show ?thesis using assms by (auto intro: measurable_sets)
43 qed
45 lemma incseq_extreal: "incseq f \<Longrightarrow> incseq (\<lambda>x. extreal (f x))"
46   unfolding incseq_def by auto
48 lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
49 proof
50   assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
51 qed (auto simp: incseq_def)
53 lemma borel_measurable_real_floor:
54   "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
55   unfolding borel.borel_measurable_iff_ge
56 proof (intro allI)
57   fix a :: real
58   { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
59       using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
60       unfolding real_eq_of_int by simp }
61   then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
62   then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
63 qed
65 lemma measure_preservingD2:
66   "f \<in> measure_preserving A B \<Longrightarrow> f \<in> measurable A B"
67   unfolding measure_preserving_def by auto
69 lemma measure_preservingD3:
70   "f \<in> measure_preserving A B \<Longrightarrow> f \<in> space A \<rightarrow> space B"
71   unfolding measure_preserving_def measurable_def by auto
73 lemma measure_preservingD:
74   "T \<in> measure_preserving A B \<Longrightarrow> X \<in> sets B \<Longrightarrow> measure A (T -` X \<inter> space A) = measure B X"
75   unfolding measure_preserving_def by auto
77 lemma (in sigma_algebra) borel_measurable_real_natfloor[intro, simp]:
78   assumes "f \<in> borel_measurable M"
79   shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
80 proof -
81   have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
82     by (auto simp: max_def natfloor_def)
83   with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
84   show ?thesis by (simp add: comp_def)
85 qed
87 lemma (in measure_space) AE_not_in:
88   assumes N: "N \<in> null_sets" shows "AE x. x \<notin> N"
89   using N by (rule AE_I') auto
91 lemma sums_If_finite:
92   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
93   assumes finite: "finite {r. P r}"
94   shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")
95 proof cases
96   assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto
97   thus ?thesis by (simp add: sums_zero)
98 next
99   assume not_empty: "{r. P r} \<noteq> {}"
100   have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"
101     by (rule series_zero)
102        (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])
103   also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"
104     by (subst setsum_cases)
105        (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)
106   finally show ?thesis .
107 qed
109 lemma sums_single:
110   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
111   shows "(\<lambda>r. if r = i then f r else 0) sums f i"
112   using sums_If_finite[of "\<lambda>r. r = i" f] by simp
114 section "Simple function"
116 text {*
118 Our simple functions are not restricted to positive real numbers. Instead
119 they are just functions with a finite range and are measurable when singleton
120 sets are measurable.
122 *}
124 definition "simple_function M g \<longleftrightarrow>
125     finite (g ` space M) \<and>
126     (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)"
128 lemma (in sigma_algebra) simple_functionD:
129   assumes "simple_function M g"
130   shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M"
131 proof -
132   show "finite (g ` space M)"
133     using assms unfolding simple_function_def by auto
134   have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
135   also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
136   finally show "g -` X \<inter> space M \<in> sets M" using assms
137     by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def)
138 qed
140 lemma (in sigma_algebra) simple_function_measurable2[intro]:
141   assumes "simple_function M f" "simple_function M g"
142   shows "f -` A \<inter> g -` B \<inter> space M \<in> sets M"
143 proof -
144   have "f -` A \<inter> g -` B \<inter> space M = (f -` A \<inter> space M) \<inter> (g -` B \<inter> space M)"
145     by auto
146   then show ?thesis using assms[THEN simple_functionD(2)] by auto
147 qed
149 lemma (in sigma_algebra) simple_function_indicator_representation:
150   fixes f ::"'a \<Rightarrow> extreal"
151   assumes f: "simple_function M f" and x: "x \<in> space M"
152   shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)"
153   (is "?l = ?r")
154 proof -
155   have "?r = (\<Sum>y \<in> f ` space M.
156     (if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))"
157     by (auto intro!: setsum_cong2)
158   also have "... =  f x *  indicator (f -` {f x} \<inter> space M) x"
159     using assms by (auto dest: simple_functionD simp: setsum_delta)
160   also have "... = f x" using x by (auto simp: indicator_def)
161   finally show ?thesis by auto
162 qed
164 lemma (in measure_space) simple_function_notspace:
165   "simple_function M (\<lambda>x. h x * indicator (- space M) x::extreal)" (is "simple_function M ?h")
166 proof -
167   have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto
168   hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset)
169   have "?h -` {0} \<inter> space M = space M" by auto
170   thus ?thesis unfolding simple_function_def by auto
171 qed
173 lemma (in sigma_algebra) simple_function_cong:
174   assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
175   shows "simple_function M f \<longleftrightarrow> simple_function M g"
176 proof -
177   have "f ` space M = g ` space M"
178     "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
179     using assms by (auto intro!: image_eqI)
180   thus ?thesis unfolding simple_function_def using assms by simp
181 qed
183 lemma (in sigma_algebra) simple_function_cong_algebra:
184   assumes "sets N = sets M" "space N = space M"
185   shows "simple_function M f \<longleftrightarrow> simple_function N f"
186   unfolding simple_function_def assms ..
188 lemma (in sigma_algebra) borel_measurable_simple_function:
189   assumes "simple_function M f"
190   shows "f \<in> borel_measurable M"
191 proof (rule borel_measurableI)
192   fix S
193   let ?I = "f ` (f -` S \<inter> space M)"
194   have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto
195   have "finite ?I"
196     using assms unfolding simple_function_def
197     using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto
198   hence "?U \<in> sets M"
199     apply (rule finite_UN)
200     using assms unfolding simple_function_def by auto
201   thus "f -` S \<inter> space M \<in> sets M" unfolding * .
202 qed
204 lemma (in sigma_algebra) simple_function_borel_measurable:
205   fixes f :: "'a \<Rightarrow> 'x::{t2_space}"
206   assumes "f \<in> borel_measurable M" and "finite (f ` space M)"
207   shows "simple_function M f"
208   using assms unfolding simple_function_def
209   by (auto intro: borel_measurable_vimage)
211 lemma (in sigma_algebra) simple_function_eq_borel_measurable:
212   fixes f :: "'a \<Rightarrow> extreal"
213   shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M"
214   using simple_function_borel_measurable[of f]
215     borel_measurable_simple_function[of f]
216   by (fastsimp simp: simple_function_def)
218 lemma (in sigma_algebra) simple_function_const[intro, simp]:
219   "simple_function M (\<lambda>x. c)"
220   by (auto intro: finite_subset simp: simple_function_def)
221 lemma (in sigma_algebra) simple_function_compose[intro, simp]:
222   assumes "simple_function M f"
223   shows "simple_function M (g \<circ> f)"
224   unfolding simple_function_def
225 proof safe
226   show "finite ((g \<circ> f) ` space M)"
227     using assms unfolding simple_function_def by (auto simp: image_compose)
228 next
229   fix x assume "x \<in> space M"
230   let ?G = "g -` {g (f x)} \<inter> (f`space M)"
231   have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M =
232     (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
233   show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
234     using assms unfolding simple_function_def *
235     by (rule_tac finite_UN) (auto intro!: finite_UN)
236 qed
238 lemma (in sigma_algebra) simple_function_indicator[intro, simp]:
239   assumes "A \<in> sets M"
240   shows "simple_function M (indicator A)"
241 proof -
242   have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _")
243     by (auto simp: indicator_def)
244   hence "finite ?S" by (rule finite_subset) simp
245   moreover have "- A \<inter> space M = space M - A" by auto
246   ultimately show ?thesis unfolding simple_function_def
247     using assms by (auto simp: indicator_def_raw)
248 qed
250 lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
251   assumes "simple_function M f"
252   assumes "simple_function M g"
253   shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p")
254   unfolding simple_function_def
255 proof safe
256   show "finite (?p ` space M)"
257     using assms unfolding simple_function_def
258     by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto
259 next
260   fix x assume "x \<in> space M"
261   have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M =
262       (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)"
263     by auto
264   with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M"
265     using assms unfolding simple_function_def by auto
266 qed
268 lemma (in sigma_algebra) simple_function_compose1:
269   assumes "simple_function M f"
270   shows "simple_function M (\<lambda>x. g (f x))"
271   using simple_function_compose[OF assms, of g]
272   by (simp add: comp_def)
274 lemma (in sigma_algebra) simple_function_compose2:
275   assumes "simple_function M f" and "simple_function M g"
276   shows "simple_function M (\<lambda>x. h (f x) (g x))"
277 proof -
278   have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))"
279     using assms by auto
280   thus ?thesis by (simp_all add: comp_def)
281 qed
283 lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]
284   and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]
285   and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
286   and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]
287   and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]
288   and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
289   and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
291 lemma (in sigma_algebra) simple_function_setsum[intro, simp]:
292   assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"
293   shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)"
294 proof cases
295   assume "finite P" from this assms show ?thesis by induct auto
296 qed auto
298 lemma (in sigma_algebra)
299   fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"
300   shows simple_function_extreal[intro, simp]: "simple_function M (\<lambda>x. extreal (f x))"
301   by (auto intro!: simple_function_compose1[OF sf])
303 lemma (in sigma_algebra)
304   fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
305   shows simple_function_real_of_nat[intro, simp]: "simple_function M (\<lambda>x. real (f x))"
306   by (auto intro!: simple_function_compose1[OF sf])
308 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence:
309   fixes u :: "'a \<Rightarrow> extreal"
310   assumes u: "u \<in> borel_measurable M"
311   shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
312              (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
313 proof -
314   def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)"
315   { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
316     proof (split split_if, intro conjI impI)
317       assume "\<not> real j \<le> u x"
318       then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
319          by (cases "u x") (auto intro!: natfloor_mono simp: mult_nonneg_nonneg)
320       moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
321         by (intro real_natfloor_le) (auto simp: mult_nonneg_nonneg)
322       ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
323         unfolding real_of_nat_le_iff by auto
324     qed auto }
325   note f_upper = this
327   have real_f:
328     "\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))"
329     unfolding f_def by auto
331   let "?g j x" = "real (f x j) / 2^j :: extreal"
332   show ?thesis
333   proof (intro exI[of _ ?g] conjI allI ballI)
334     fix i
335     have "simple_function M (\<lambda>x. real (f x i))"
336     proof (intro simple_function_borel_measurable)
337       show "(\<lambda>x. real (f x i)) \<in> borel_measurable M"
338         using u by (auto intro!: measurable_If simp: real_f)
339       have "(\<lambda>x. real (f x i))`space M \<subseteq> real`{..i*2^i}"
340         using f_upper[of _ i] by auto
341       then show "finite ((\<lambda>x. real (f x i))`space M)"
342         by (rule finite_subset) auto
343     qed
344     then show "simple_function M (?g i)"
345       by (auto intro: simple_function_extreal simple_function_div)
346   next
347     show "incseq ?g"
348     proof (intro incseq_extreal incseq_SucI le_funI)
349       fix x and i :: nat
350       have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
351       proof ((split split_if)+, intro conjI impI)
352         assume "extreal (real i) \<le> u x" "\<not> extreal (real (Suc i)) \<le> u x"
353         then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)"
354           by (cases "u x") (auto intro!: le_natfloor)
355       next
356         assume "\<not> extreal (real i) \<le> u x" "extreal (real (Suc i)) \<le> u x"
357         then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i"
358           by (cases "u x") auto
359       next
360         assume "\<not> extreal (real i) \<le> u x" "\<not> extreal (real (Suc i)) \<le> u x"
361         have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2"
362           by simp
363         also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
364         proof cases
365           assume "0 \<le> u x" then show ?thesis
366             by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg)
367         next
368           assume "\<not> 0 \<le> u x" then show ?thesis
369             by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)
370         qed
371         also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)"
372           by (simp add: ac_simps)
373         finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" .
374       qed simp
375       then show "?g i x \<le> ?g (Suc i) x"
376         by (auto simp: field_simps)
377     qed
378   next
379     fix x show "(SUP i. ?g i x) = max 0 (u x)"
380     proof (rule extreal_SUPI)
381       fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
382         by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
383                                      mult_nonpos_nonneg mult_nonneg_nonneg)
384     next
385       fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
386       have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
387       from order_trans[OF this *] have "0 \<le> y" by simp
388       show "max 0 (u x) \<le> y"
389       proof (cases y)
390         case (real r)
391         with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq)
392         from real_arch_lt[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le)
393         then have "\<exists>p. max 0 (u x) = extreal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def)
394         then guess p .. note ux = this
395         obtain m :: nat where m: "p < real m" using real_arch_lt ..
396         have "p \<le> r"
397         proof (rule ccontr)
398           assume "\<not> p \<le> r"
399           with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"]
400           obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: inverse_eq_divide field_simps)
401           then have "r * 2^max N m < p * 2^max N m - 1" by simp
402           moreover
403           have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
404             using *[of "max N m"] m unfolding real_f using ux
405             by (cases "0 \<le> u x") (simp_all add: max_def mult_nonneg_nonneg split: split_if_asm)
406           then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
407             by (metis real_natfloor_gt_diff_one less_le_trans)
408           ultimately show False by auto
409         qed
410         then show "max 0 (u x) \<le> y" using real ux by simp
411       qed (insert `0 \<le> y`, auto)
412     qed
413   qed (auto simp: divide_nonneg_pos)
414 qed
416 lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence':
417   fixes u :: "'a \<Rightarrow> extreal"
418   assumes u: "u \<in> borel_measurable M"
419   obtains f where "\<And>i. simple_function M (f i)" "incseq f" "\<And>i. \<infinity> \<notin> range (f i)"
420     "\<And>x. (SUP i. f i x) = max 0 (u x)" "\<And>i x. 0 \<le> f i x"
421   using borel_measurable_implies_simple_function_sequence[OF u] by auto
423 lemma (in sigma_algebra) simple_function_If_set:
424   assumes sf: "simple_function M f" "simple_function M g" and A: "A \<inter> space M \<in> sets M"
425   shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF")
426 proof -
427   def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
428   show ?thesis unfolding simple_function_def
429   proof safe
430     have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
431     from finite_subset[OF this] assms
432     show "finite (?IF ` space M)" unfolding simple_function_def by auto
433   next
434     fix x assume "x \<in> space M"
435     then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
436       then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
437       else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
438       using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
439     have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
440       unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
441     show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
442   qed
443 qed
445 lemma (in sigma_algebra) simple_function_If:
446   assumes sf: "simple_function M f" "simple_function M g" and P: "{x\<in>space M. P x} \<in> sets M"
447   shows "simple_function M (\<lambda>x. if P x then f x else g x)"
448 proof -
449   have "{x\<in>space M. P x} = {x. P x} \<inter> space M" by auto
450   with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp
451 qed
453 lemma (in measure_space) simple_function_restricted:
454   fixes f :: "'a \<Rightarrow> extreal" assumes "A \<in> sets M"
455   shows "simple_function (restricted_space A) f \<longleftrightarrow> simple_function M (\<lambda>x. f x * indicator A x)"
456     (is "simple_function ?R f \<longleftrightarrow> simple_function M ?f")
457 proof -
458   interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
459   have f: "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
460   proof cases
461     assume "A = space M"
462     then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
463     then show ?thesis by simp
464   next
465     assume "A \<noteq> space M"
466     then obtain x where x: "x \<in> space M" "x \<notin> A"
467       using sets_into_space `A \<in> sets M` by auto
468     have *: "?f`space M = f`A \<union> {0}"
469     proof (auto simp add: image_iff)
470       show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0"
471         using x by (auto intro!: bexI[of _ x])
472     next
473       fix x assume "x \<in> A"
474       then show "\<exists>y\<in>space M. f x = f y * indicator A y"
475         using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x])
476     next
477       fix x
478       assume "indicator A x \<noteq> (0::extreal)"
479       then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm)
480       moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y"
481       ultimately show "f x = 0" by auto
482     qed
483     then show ?thesis by auto
484   qed
485   then show ?thesis
486     unfolding simple_function_eq_borel_measurable
487       R.simple_function_eq_borel_measurable
488     unfolding borel_measurable_restricted[OF `A \<in> sets M`]
489     using assms(1)[THEN sets_into_space]
490     by (auto simp: indicator_def)
491 qed
493 lemma (in sigma_algebra) simple_function_subalgebra:
494   assumes "simple_function N f"
495   and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M"
496   shows "simple_function M f"
497   using assms unfolding simple_function_def by auto
499 lemma (in measure_space) simple_function_vimage:
500   assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
501     and f: "simple_function M' f"
502   shows "simple_function M (\<lambda>x. f (T x))"
503 proof (intro simple_function_def[THEN iffD2] conjI ballI)
504   interpret T: sigma_algebra M' by fact
505   have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
506     using T unfolding measurable_def by auto
507   then show "finite ((\<lambda>x. f (T x)) ` space M)"
508     using f unfolding simple_function_def by (auto intro: finite_subset)
509   fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M"
510   then have "i \<in> f ` space M'"
511     using T unfolding measurable_def by auto
512   then have "f -` {i} \<inter> space M' \<in> sets M'"
513     using f unfolding simple_function_def by auto
514   then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M"
515     using T unfolding measurable_def by auto
516   also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
517     using T unfolding measurable_def by auto
518   finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
519 qed
521 section "Simple integral"
523 definition simple_integral_def:
524   "integral\<^isup>S M f = (\<Sum>x \<in> f ` space M. x * measure M (f -` {x} \<inter> space M))"
526 syntax
527   "_simple_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> extreal) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> extreal" ("\<integral>\<^isup>S _. _ \<partial>_" [60,61] 110)
529 translations
530   "\<integral>\<^isup>S x. f \<partial>M" == "CONST integral\<^isup>S M (%x. f)"
532 lemma (in measure_space) simple_integral_cong:
533   assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
534   shows "integral\<^isup>S M f = integral\<^isup>S M g"
535 proof -
536   have "f ` space M = g ` space M"
537     "\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M"
538     using assms by (auto intro!: image_eqI)
539   thus ?thesis unfolding simple_integral_def by simp
540 qed
542 lemma (in measure_space) simple_integral_cong_measure:
543   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
544     and "simple_function M f"
545   shows "integral\<^isup>S N f = integral\<^isup>S M f"
546 proof -
547   interpret v: measure_space N
548     by (rule measure_space_cong) fact+
549   from simple_functionD[OF `simple_function M f`] assms show ?thesis
550     by (auto intro!: setsum_cong simp: simple_integral_def)
551 qed
553 lemma (in measure_space) simple_integral_const[simp]:
554   "(\<integral>\<^isup>Sx. c \<partial>M) = c * \<mu> (space M)"
555 proof (cases "space M = {}")
556   case True thus ?thesis unfolding simple_integral_def by simp
557 next
558   case False hence "(\<lambda>x. c) ` space M = {c}" by auto
559   thus ?thesis unfolding simple_integral_def by simp
560 qed
562 lemma (in measure_space) simple_function_partition:
563   assumes f: "simple_function M f" and g: "simple_function M g"
564   shows "integral\<^isup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
565     (is "_ = setsum _ (?p ` space M)")
566 proof-
567   let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
568   let ?SIGMA = "Sigma (f`space M) ?sub"
570   have [intro]:
571     "finite (f ` space M)"
572     "finite (g ` space M)"
573     using assms unfolding simple_function_def by simp_all
575   { fix A
576     have "?p ` (A \<inter> space M) \<subseteq>
577       (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
578       by auto
579     hence "finite (?p ` (A \<inter> space M))"
580       by (rule finite_subset) auto }
581   note this[intro, simp]
582   note sets = simple_function_measurable2[OF f g]
584   { fix x assume "x \<in> space M"
585     have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
586     with sets have "\<mu> (f -` {f x} \<inter> space M) = setsum \<mu> (?sub (f x))"
587       by (subst measure_Union) auto }
588   hence "integral\<^isup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)"
589     unfolding simple_integral_def using f sets
590     by (subst setsum_Sigma[symmetric])
591        (auto intro!: setsum_cong setsum_extreal_right_distrib)
592   also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)"
593   proof -
594     have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
595     have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
596       = (\<lambda>x. (f x, ?p x)) ` space M"
597     proof safe
598       fix x assume "x \<in> space M"
599       thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
600         by (auto intro!: image_eqI[of _ _ "?p x"])
601     qed auto
602     thus ?thesis
603       apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
604       apply (rule_tac x="xa" in image_eqI)
605       by simp_all
606   qed
607   finally show ?thesis .
608 qed
610 lemma (in measure_space) simple_integral_add[simp]:
611   assumes f: "simple_function M f" and "\<And>x. 0 \<le> f x" and g: "simple_function M g" and "\<And>x. 0 \<le> g x"
612   shows "(\<integral>\<^isup>Sx. f x + g x \<partial>M) = integral\<^isup>S M f + integral\<^isup>S M g"
613 proof -
614   { fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
615     assume "x \<in> space M"
616     hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}"
617         "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S"
618       by auto }
619   with assms show ?thesis
620     unfolding
621       simple_function_partition[OF simple_function_add[OF f g] simple_function_Pair[OF f g]]
622       simple_function_partition[OF f g]
623       simple_function_partition[OF g f]
624     by (subst (3) Int_commute)
625        (auto simp add: extreal_left_distrib setsum_addf[symmetric] intro!: setsum_cong)
626 qed
628 lemma (in measure_space) simple_integral_setsum[simp]:
629   assumes "\<And>i x. i \<in> P \<Longrightarrow> 0 \<le> f i x"
630   assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)"
631   shows "(\<integral>\<^isup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>S M (f i))"
632 proof cases
633   assume "finite P"
634   from this assms show ?thesis
635     by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg)
636 qed auto
638 lemma (in measure_space) simple_integral_mult[simp]:
639   assumes f: "simple_function M f" "\<And>x. 0 \<le> f x"
640   shows "(\<integral>\<^isup>Sx. c * f x \<partial>M) = c * integral\<^isup>S M f"
641 proof -
642   note mult = simple_function_mult[OF simple_function_const[of c] f(1)]
643   { fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M"
644     assume "x \<in> space M"
645     hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}"
646       by auto }
647   with assms show ?thesis
648     unfolding simple_function_partition[OF mult f(1)]
649               simple_function_partition[OF f(1) mult]
650     by (subst setsum_extreal_right_distrib)
651        (auto intro!: extreal_0_le_mult setsum_cong simp: mult_assoc)
652 qed
654 lemma (in measure_space) simple_integral_mono_AE:
655   assumes f: "simple_function M f" and g: "simple_function M g"
656   and mono: "AE x. f x \<le> g x"
657   shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
658 proof -
659   let "?S x" = "(g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)"
660   have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x"
661     "\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto
662   show ?thesis
663     unfolding *
664       simple_function_partition[OF f g]
665       simple_function_partition[OF g f]
666   proof (safe intro!: setsum_mono)
667     fix x assume "x \<in> space M"
668     then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto
669     show "the_elem (f`?S x) * \<mu> (?S x) \<le> the_elem (g`?S x) * \<mu> (?S x)"
670     proof (cases "f x \<le> g x")
671       case True then show ?thesis
672         using * assms(1,2)[THEN simple_functionD(2)]
673         by (auto intro!: extreal_mult_right_mono)
674     next
675       case False
676       obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "\<mu> N = 0"
677         using mono by (auto elim!: AE_E)
678       have "?S x \<subseteq> N" using N `x \<in> space M` False by auto
679       moreover have "?S x \<in> sets M" using assms
680         by (rule_tac Int) (auto intro!: simple_functionD)
681       ultimately have "\<mu> (?S x) \<le> \<mu> N"
682         using `N \<in> sets M` by (auto intro!: measure_mono)
683       moreover have "0 \<le> \<mu> (?S x)"
684         using assms(1,2)[THEN simple_functionD(2)] by auto
685       ultimately have "\<mu> (?S x) = 0" using `\<mu> N = 0` by auto
686       then show ?thesis by simp
687     qed
688   qed
689 qed
691 lemma (in measure_space) simple_integral_mono:
692   assumes "simple_function M f" and "simple_function M g"
693   and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
694   shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
695   using assms by (intro simple_integral_mono_AE) auto
697 lemma (in measure_space) simple_integral_cong_AE:
698   assumes "simple_function M f" and "simple_function M g"
699   and "AE x. f x = g x"
700   shows "integral\<^isup>S M f = integral\<^isup>S M g"
701   using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE)
703 lemma (in measure_space) simple_integral_cong':
704   assumes sf: "simple_function M f" "simple_function M g"
705   and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0"
706   shows "integral\<^isup>S M f = integral\<^isup>S M g"
707 proof (intro simple_integral_cong_AE sf AE_I)
708   show "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" by fact
709   show "{x \<in> space M. f x \<noteq> g x} \<in> sets M"
710     using sf[THEN borel_measurable_simple_function] by auto
711 qed simp
713 lemma (in measure_space) simple_integral_indicator:
714   assumes "A \<in> sets M"
715   assumes "simple_function M f"
716   shows "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) =
717     (\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
718 proof cases
719   assume "A = space M"
720   moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = integral\<^isup>S M f"
721     by (auto intro!: simple_integral_cong)
722   moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
723   ultimately show ?thesis by (simp add: simple_integral_def)
724 next
725   assume "A \<noteq> space M"
726   then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto
727   have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _")
728   proof safe
729     fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto
730   next
731     fix y assume "y \<in> A" thus "f y \<in> ?I ` space M"
732       using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y])
733   next
734     show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x])
735   qed
736   have *: "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) =
737     (\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))"
738     unfolding simple_integral_def I
739   proof (rule setsum_mono_zero_cong_left)
740     show "finite (f ` space M \<union> {0})"
741       using assms(2) unfolding simple_function_def by auto
742     show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}"
743       using sets_into_space[OF assms(1)] by auto
744     have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
745       by (auto simp: image_iff)
746     thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}).
747       i * \<mu> (f -` {i} \<inter> space M \<inter> A) = 0" by auto
748   next
749     fix x assume "x \<in> f`A \<union> {0}"
750     hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A"
751       by (auto simp: indicator_def split: split_if_asm)
752     thus "x * \<mu> (?I -` {x} \<inter> space M) =
753       x * \<mu> (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all
754   qed
755   show ?thesis unfolding *
756     using assms(2) unfolding simple_function_def
757     by (auto intro!: setsum_mono_zero_cong_right)
758 qed
760 lemma (in measure_space) simple_integral_indicator_only[simp]:
761   assumes "A \<in> sets M"
762   shows "integral\<^isup>S M (indicator A) = \<mu> A"
763 proof cases
764   assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto
765   thus ?thesis unfolding simple_integral_def using `space M = {}` by auto
766 next
767   assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::extreal}" by auto
768   thus ?thesis
769     using simple_integral_indicator[OF assms simple_function_const[of 1]]
770     using sets_into_space[OF assms]
771     by (auto intro!: arg_cong[where f="\<mu>"])
772 qed
774 lemma (in measure_space) simple_integral_null_set:
775   assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets"
776   shows "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = 0"
777 proof -
778   have "AE x. indicator N x = (0 :: extreal)"
779     using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
780   then have "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^isup>Sx. 0 \<partial>M)"
781     using assms apply (intro simple_integral_cong_AE) by auto
782   then show ?thesis by simp
783 qed
785 lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
786   assumes sf: "simple_function M f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
787   shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)"
788   using assms by (intro simple_integral_cong_AE) auto
790 lemma (in measure_space) simple_integral_restricted:
791   assumes "A \<in> sets M"
792   assumes sf: "simple_function M (\<lambda>x. f x * indicator A x)"
793   shows "integral\<^isup>S (restricted_space A) f = (\<integral>\<^isup>Sx. f x * indicator A x \<partial>M)"
794     (is "_ = integral\<^isup>S M ?f")
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)"
815     unfolding extreal_mult_cancel_left by auto
816 qed
818 lemma (in measure_space) simple_integral_subalgebra:
819   assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M"
820   shows "integral\<^isup>S N = integral\<^isup>S M"
821   unfolding simple_integral_def_raw by simp
823 lemma (in measure_space) simple_integral_vimage:
824   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
825     and f: "simple_function M' f"
826   shows "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
827 proof -
828   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
829   show "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
830     unfolding simple_integral_def
831   proof (intro setsum_mono_zero_cong_right ballI)
832     show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'"
833       using T unfolding measurable_def measure_preserving_def by auto
834     show "finite (f ` space M')"
835       using f unfolding simple_function_def by auto
836   next
837     fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M"
838     then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff)
839     with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
840     show "i * T.\<mu> (f -` {i} \<inter> space M') = 0" by simp
841   next
842     fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
843     then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
844       using T unfolding measurable_def measure_preserving_def by auto
845     with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"]
846     show "i * T.\<mu> (f -` {i} \<inter> space M') = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
847       by auto
848   qed
849 qed
851 lemma (in measure_space) simple_integral_cmult_indicator:
852   assumes A: "A \<in> sets M"
853   shows "(\<integral>\<^isup>Sx. c * indicator A x \<partial>M) = c * \<mu> A"
854   using simple_integral_mult[OF simple_function_indicator[OF A]]
855   unfolding simple_integral_indicator_only[OF A] by simp
857 lemma (in measure_space) simple_integral_positive:
858   assumes f: "simple_function M f" and ae: "AE x. 0 \<le> f x"
859   shows "0 \<le> integral\<^isup>S M f"
860 proof -
861   have "integral\<^isup>S M (\<lambda>x. 0) \<le> integral\<^isup>S M f"
862     using simple_integral_mono_AE[OF _ f ae] by auto
863   then show ?thesis by simp
864 qed
866 section "Continuous positive integration"
868 definition positive_integral_def:
869   "integral\<^isup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^isup>S M g)"
871 syntax
872   "_positive_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> extreal) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> extreal" ("\<integral>\<^isup>+ _. _ \<partial>_" [60,61] 110)
874 translations
875   "\<integral>\<^isup>+ x. f \<partial>M" == "CONST integral\<^isup>P M (%x. f)"
877 lemma (in measure_space) positive_integral_cong_measure:
878   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
879   shows "integral\<^isup>P N f = integral\<^isup>P M f"
880   unfolding positive_integral_def
881   unfolding simple_function_cong_algebra[OF assms(2,3), symmetric]
882   using AE_cong_measure[OF assms]
883   using simple_integral_cong_measure[OF assms]
884   by (auto intro!: SUP_cong)
886 lemma (in measure_space) positive_integral_positive:
887   "0 \<le> integral\<^isup>P M f"
888   by (auto intro!: le_SUPI2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
890 lemma (in measure_space) positive_integral_def_finite:
891   "integral\<^isup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^isup>S M g)"
892     (is "_ = SUPR ?A ?f")
893   unfolding positive_integral_def
894 proof (safe intro!: antisym SUP_leI)
895   fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
896   let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
897   note gM = g(1)[THEN borel_measurable_simple_function]
898   have \<mu>G_pos: "0 \<le> \<mu> ?G" using gM by auto
899   let "?g y x" = "if g x = \<infinity> then y else max 0 (g x)"
900   from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
901     apply (safe intro!: simple_function_max simple_function_If)
902     apply (force simp: max_def le_fun_def split: split_if_asm)+
903     done
904   show "integral\<^isup>S M g \<le> SUPR ?A ?f"
905   proof cases
906     have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto
907     assume "\<mu> ?G = 0"
908     with gM have "AE x. x \<notin> ?G" by (simp add: AE_iff_null_set)
909     with gM g show ?thesis
910       by (intro le_SUPI2[OF g0] simple_integral_mono_AE)
911          (auto simp: max_def intro!: simple_function_If)
912   next
913     assume \<mu>G: "\<mu> ?G \<noteq> 0"
914     have "SUPR ?A (integral\<^isup>S M) = \<infinity>"
915     proof (intro SUP_PInfty)
916       fix n :: nat
917       let ?y = "extreal (real n) / (if \<mu> ?G = \<infinity> then 1 else \<mu> ?G)"
918       have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>G \<mu>G_pos by (auto simp: extreal_divide_eq)
919       then have "?g ?y \<in> ?A" by (rule g_in_A)
920       have "real n \<le> ?y * \<mu> ?G"
921         using \<mu>G \<mu>G_pos by (cases "\<mu> ?G") (auto simp: field_simps)
922       also have "\<dots> = (\<integral>\<^isup>Sx. ?y * indicator ?G x \<partial>M)"
923         using `0 \<le> ?y` `?g ?y \<in> ?A` gM
924         by (subst simple_integral_cmult_indicator) auto
925       also have "\<dots> \<le> integral\<^isup>S M (?g ?y)" using `?g ?y \<in> ?A` gM
926         by (intro simple_integral_mono) auto
927       finally show "\<exists>i\<in>?A. real n \<le> integral\<^isup>S M i"
928         using `?g ?y \<in> ?A` by blast
929     qed
930     then show ?thesis by simp
931   qed
932 qed (auto intro: le_SUPI)
934 lemma (in measure_space) positive_integral_mono_AE:
935   assumes ae: "AE x. u x \<le> v x" shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
936   unfolding positive_integral_def
937 proof (safe intro!: SUP_mono)
938   fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u"
939   from ae[THEN AE_E] guess N . note N = this
940   then have ae_N: "AE x. x \<notin> N" by (auto intro: AE_not_in)
941   let "?n x" = "n x * indicator (space M - N) x"
942   have "AE x. n x \<le> ?n x" "simple_function M ?n"
943     using n N ae_N by auto
944   moreover
945   { fix x have "?n x \<le> max 0 (v x)"
946     proof cases
947       assume x: "x \<in> space M - N"
948       with N have "u x \<le> v x" by auto
949       with n(2)[THEN le_funD, of x] x show ?thesis
950         by (auto simp: max_def split: split_if_asm)
951     qed simp }
952   then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI)
953   moreover have "integral\<^isup>S M n \<le> integral\<^isup>S M ?n"
954     using ae_N N n by (auto intro!: simple_integral_mono_AE)
955   ultimately show "\<exists>m\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> v}. integral\<^isup>S M n \<le> integral\<^isup>S M m"
956     by force
957 qed
959 lemma (in measure_space) positive_integral_mono:
960   "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^isup>P M u \<le> integral\<^isup>P M v"
961   by (auto intro: positive_integral_mono_AE)
963 lemma (in measure_space) positive_integral_cong_AE:
964   "AE x. u x = v x \<Longrightarrow> integral\<^isup>P M u = integral\<^isup>P M v"
965   by (auto simp: eq_iff intro!: positive_integral_mono_AE)
967 lemma (in measure_space) positive_integral_cong:
968   "(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^isup>P M u = integral\<^isup>P M v"
969   by (auto intro: positive_integral_cong_AE)
971 lemma (in measure_space) positive_integral_eq_simple_integral:
972   assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
973 proof -
974   let "?f x" = "f x * indicator (space M) x"
975   have f': "simple_function M ?f" using f by auto
976   with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
977     by (auto simp: fun_eq_iff max_def split: split_indicator)
978   have "integral\<^isup>P M ?f \<le> integral\<^isup>S M ?f" using f'
979     by (force intro!: SUP_leI simple_integral_mono simp: le_fun_def positive_integral_def)
980   moreover have "integral\<^isup>S M ?f \<le> integral\<^isup>P M ?f"
981     unfolding positive_integral_def
982     using f' by (auto intro!: le_SUPI)
983   ultimately show ?thesis
984     by (simp cong: positive_integral_cong simple_integral_cong)
985 qed
987 lemma (in measure_space) positive_integral_eq_simple_integral_AE:
988   assumes f: "simple_function M f" "AE x. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f"
989 proof -
990   have "AE x. f x = max 0 (f x)" using f by (auto split: split_max)
991   with f have "integral\<^isup>P M f = integral\<^isup>S M (\<lambda>x. max 0 (f x))"
992     by (simp cong: positive_integral_cong_AE simple_integral_cong_AE
994   with assms show ?thesis
995     by (auto intro!: simple_integral_cong_AE split: split_max)
996 qed
998 lemma (in measure_space) positive_integral_SUP_approx:
999   assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
1000   and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}"
1001   shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S")
1002 proof (rule extreal_le_mult_one_interval)
1003   have "0 \<le> (SUP i. integral\<^isup>P M (f i))"
1004     using f(3) by (auto intro!: le_SUPI2 positive_integral_positive)
1005   then show "(SUP i. integral\<^isup>P M (f i)) \<noteq> -\<infinity>" by auto
1006   have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
1007     using u(3) by auto
1008   fix a :: extreal assume "0 < a" "a < 1"
1009   hence "a \<noteq> 0" by auto
1010   let "?B i" = "{x \<in> space M. a * u x \<le> f i x}"
1011   have B: "\<And>i. ?B i \<in> sets M"
1012     using f `simple_function M u` by (auto simp: borel_measurable_simple_function)
1014   let "?uB i x" = "u x * indicator (?B i) x"
1016   { fix i have "?B i \<subseteq> ?B (Suc i)"
1017     proof safe
1018       fix i x assume "a * u x \<le> f i x"
1019       also have "\<dots> \<le> f (Suc i) x"
1020         using `incseq f`[THEN incseq_SucD] unfolding le_fun_def by auto
1021       finally show "a * u x \<le> f (Suc i) x" .
1022     qed }
1023   note B_mono = this
1025   note B_u = Int[OF u(1)[THEN simple_functionD(2)] B]
1027   let "?B' i n" = "(u -` {i} \<inter> space M) \<inter> ?B n"
1028   have measure_conv: "\<And>i. \<mu> (u -` {i} \<inter> space M) = (SUP n. \<mu> (?B' i n))"
1029   proof -
1030     fix i
1031     have 1: "range (?B' i) \<subseteq> sets M" using B_u by auto
1032     have 2: "incseq (?B' i)" using B_mono by (auto intro!: incseq_SucI)
1033     have "(\<Union>n. ?B' i n) = u -` {i} \<inter> space M"
1034     proof safe
1035       fix x i assume x: "x \<in> space M"
1036       show "x \<in> (\<Union>i. ?B' (u x) i)"
1037       proof cases
1038         assume "u x = 0" thus ?thesis using `x \<in> space M` f(3) by simp
1039       next
1040         assume "u x \<noteq> 0"
1041         with `a < 1` u_range[OF `x \<in> space M`]
1042         have "a * u x < 1 * u x"
1043           by (intro extreal_mult_strict_right_mono) (auto simp: image_iff)
1044         also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUPR_apply)
1045         finally obtain i where "a * u x < f i x" unfolding SUPR_def
1046           by (auto simp add: less_Sup_iff)
1047         hence "a * u x \<le> f i x" by auto
1048         thus ?thesis using `x \<in> space M` by auto
1049       qed
1050     qed
1051     then show "?thesis i" using continuity_from_below[OF 1 2] by simp
1052   qed
1054   have "integral\<^isup>S M u = (SUP i. integral\<^isup>S M (?uB i))"
1055     unfolding simple_integral_indicator[OF B `simple_function M u`]
1056   proof (subst SUPR_extreal_setsum, safe)
1057     fix x n assume "x \<in> space M"
1058     with u_range show "incseq (\<lambda>i. u x * \<mu> (?B' (u x) i))" "\<And>i. 0 \<le> u x * \<mu> (?B' (u x) i)"
1059       using B_mono B_u by (auto intro!: measure_mono extreal_mult_left_mono incseq_SucI simp: extreal_zero_le_0_iff)
1060   next
1061     show "integral\<^isup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (?B' i n))"
1062       using measure_conv u_range B_u unfolding simple_integral_def
1063       by (auto intro!: setsum_cong SUPR_extreal_cmult[symmetric])
1064   qed
1065   moreover
1066   have "a * (SUP i. integral\<^isup>S M (?uB i)) \<le> ?S"
1067     apply (subst SUPR_extreal_cmult[symmetric])
1068   proof (safe intro!: SUP_mono bexI)
1069     fix i
1070     have "a * integral\<^isup>S M (?uB i) = (\<integral>\<^isup>Sx. a * ?uB i x \<partial>M)"
1071       using B `simple_function M u` u_range
1072       by (subst simple_integral_mult) (auto split: split_indicator)
1073     also have "\<dots> \<le> integral\<^isup>P M (f i)"
1074     proof -
1075       have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto
1076       show ?thesis using f(3) * u_range `0 < a`
1077         by (subst positive_integral_eq_simple_integral[symmetric])
1078            (auto intro!: positive_integral_mono split: split_indicator)
1079     qed
1080     finally show "a * integral\<^isup>S M (?uB i) \<le> integral\<^isup>P M (f i)"
1081       by auto
1082   next
1083     fix i show "0 \<le> \<integral>\<^isup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range
1084       by (intro simple_integral_positive) (auto split: split_indicator)
1085   qed (insert `0 < a`, auto)
1086   ultimately show "a * integral\<^isup>S M u \<le> ?S" by simp
1087 qed
1089 lemma (in measure_space) incseq_positive_integral:
1090   assumes "incseq f" shows "incseq (\<lambda>i. integral\<^isup>P M (f i))"
1091 proof -
1092   have "\<And>i x. f i x \<le> f (Suc i) x"
1093     using assms by (auto dest!: incseq_SucD simp: le_fun_def)
1094   then show ?thesis
1095     by (auto intro!: incseq_SucI positive_integral_mono)
1096 qed
1098 text {* Beppo-Levi monotone convergence theorem *}
1099 lemma (in measure_space) positive_integral_monotone_convergence_SUP:
1100   assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
1101   shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
1102 proof (rule antisym)
1103   show "(SUP j. integral\<^isup>P M (f j)) \<le> (\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M)"
1104     by (auto intro!: SUP_leI le_SUPI positive_integral_mono)
1105 next
1106   show "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^isup>P M (f j))"
1107     unfolding positive_integral_def_finite[of "\<lambda>x. SUP i. f i x"]
1108   proof (safe intro!: SUP_leI)
1109     fix g assume g: "simple_function M g"
1110       and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
1111     moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
1112       using f by (auto intro!: le_SUPI2)
1113     ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
1114       by (intro  positive_integral_SUP_approx[OF f g _ g'])
1115          (auto simp: le_fun_def max_def SUPR_apply)
1116   qed
1117 qed
1119 lemma (in measure_space) positive_integral_monotone_convergence_SUP_AE:
1120   assumes f: "\<And>i. AE x. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M"
1121   shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
1122 proof -
1123   from f have "AE x. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x"
1124     by (simp add: AE_all_countable)
1125   from this[THEN AE_E] guess N . note N = this
1126   let "?f i x" = "if x \<in> space M - N then f i x else 0"
1127   have f_eq: "AE x. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ N])
1128   then have "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^isup>+ x. (SUP i. ?f i x) \<partial>M)"
1129     by (auto intro!: positive_integral_cong_AE)
1130   also have "\<dots> = (SUP i. (\<integral>\<^isup>+ x. ?f i x \<partial>M))"
1131   proof (rule positive_integral_monotone_convergence_SUP)
1132     show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI)
1133     { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M"
1134         using f N(3) by (intro measurable_If_set) auto
1135       fix x show "0 \<le> ?f i x"
1136         using N(1) by auto }
1137   qed
1138   also have "\<dots> = (SUP i. (\<integral>\<^isup>+ x. f i x \<partial>M))"
1139     using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext)
1140   finally show ?thesis .
1141 qed
1143 lemma (in measure_space) positive_integral_monotone_convergence_SUP_AE_incseq:
1144   assumes f: "incseq f" "\<And>i. AE x. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M"
1145   shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
1146   using f[unfolded incseq_Suc_iff le_fun_def]
1147   by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel])
1148      auto
1150 lemma (in measure_space) positive_integral_monotone_convergence_simple:
1151   assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
1152   shows "(SUP i. integral\<^isup>S M (f i)) = (\<integral>\<^isup>+x. (SUP i. f i x) \<partial>M)"
1153   using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
1154     f(3)[THEN borel_measurable_simple_function] f(2)]
1155   by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext)
1157 lemma positive_integral_max_0:
1158   "(\<integral>\<^isup>+x. max 0 (f x) \<partial>M) = integral\<^isup>P M f"
1159   by (simp add: le_fun_def positive_integral_def)
1161 lemma (in measure_space) positive_integral_cong_pos:
1162   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x"
1163   shows "integral\<^isup>P M f = integral\<^isup>P M g"
1164 proof -
1165   have "integral\<^isup>P M (\<lambda>x. max 0 (f x)) = integral\<^isup>P M (\<lambda>x. max 0 (g x))"
1166   proof (intro positive_integral_cong)
1167     fix x assume "x \<in> space M"
1168     from assms[OF this] show "max 0 (f x) = max 0 (g x)"
1169       by (auto split: split_max)
1170   qed
1171   then show ?thesis by (simp add: positive_integral_max_0)
1172 qed
1174 lemma (in measure_space) SUP_simple_integral_sequences:
1175   assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)"
1176   and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)"
1177   and eq: "AE x. (SUP i. f i x) = (SUP i. g i x)"
1178   shows "(SUP i. integral\<^isup>S M (f i)) = (SUP i. integral\<^isup>S M (g i))"
1179     (is "SUPR _ ?F = SUPR _ ?G")
1180 proof -
1181   have "(SUP i. integral\<^isup>S M (f i)) = (\<integral>\<^isup>+x. (SUP i. f i x) \<partial>M)"
1182     using f by (rule positive_integral_monotone_convergence_simple)
1183   also have "\<dots> = (\<integral>\<^isup>+x. (SUP i. g i x) \<partial>M)"
1184     unfolding eq[THEN positive_integral_cong_AE] ..
1185   also have "\<dots> = (SUP i. ?G i)"
1186     using g by (rule positive_integral_monotone_convergence_simple[symmetric])
1187   finally show ?thesis by simp
1188 qed
1190 lemma (in measure_space) positive_integral_const[simp]:
1191   "0 \<le> c \<Longrightarrow> (\<integral>\<^isup>+ x. c \<partial>M) = c * \<mu> (space M)"
1192   by (subst positive_integral_eq_simple_integral) auto
1194 lemma (in measure_space) positive_integral_vimage:
1195   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
1196   and f: "f \<in> borel_measurable M'"
1197   shows "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
1198 proof -
1199   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
1200   from T.borel_measurable_implies_simple_function_sequence'[OF f]
1201   guess f' . note f' = this
1202   let "?f i x" = "f' i (T x)"
1203   have inc: "incseq ?f" using f' by (force simp: le_fun_def incseq_def)
1204   have sup: "\<And>x. (SUP i. ?f i x) = max 0 (f (T x))"
1205     using f'(4) .
1206   have sf: "\<And>i. simple_function M (\<lambda>x. f' i (T x))"
1207     using simple_function_vimage[OF T(1) measure_preservingD2[OF T(2)] f'(1)] .
1208   show "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
1209     using
1210       T.positive_integral_monotone_convergence_simple[OF f'(2,5,1)]
1211       positive_integral_monotone_convergence_simple[OF inc f'(5) sf]
1212     by (simp add: positive_integral_max_0 simple_integral_vimage[OF T f'(1)] f')
1213 qed
1215 lemma (in measure_space) positive_integral_linear:
1216   assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
1217   and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
1218   shows "(\<integral>\<^isup>+ x. a * f x + g x \<partial>M) = a * integral\<^isup>P M f + integral\<^isup>P M g"
1219     (is "integral\<^isup>P M ?L = _")
1220 proof -
1221   from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
1222   note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
1223   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
1224   note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
1225   let "?L' i x" = "a * u i x + v i x"
1227   have "?L \<in> borel_measurable M" using assms by auto
1228   from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
1229   note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this
1231   have inc: "incseq (\<lambda>i. a * integral\<^isup>S M (u i))" "incseq (\<lambda>i. integral\<^isup>S M (v i))"
1232     using u v `0 \<le> a`
1233     by (auto simp: incseq_Suc_iff le_fun_def
1234              intro!: add_mono extreal_mult_left_mono simple_integral_mono)
1235   have pos: "\<And>i. 0 \<le> integral\<^isup>S M (u i)" "\<And>i. 0 \<le> integral\<^isup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^isup>S M (u i)"
1236     using u v `0 \<le> a` by (auto simp: simple_integral_positive)
1237   { fix i from pos[of i] have "a * integral\<^isup>S M (u i) \<noteq> -\<infinity>" "integral\<^isup>S M (v i) \<noteq> -\<infinity>"
1238       by (auto split: split_if_asm) }
1239   note not_MInf = this
1241   have l': "(SUP i. integral\<^isup>S M (l i)) = (SUP i. integral\<^isup>S M (?L' i))"
1242   proof (rule SUP_simple_integral_sequences[OF l(3,6,2)])
1243     show "incseq ?L'" "\<And>i x. 0 \<le> ?L' i x" "\<And>i. simple_function M (?L' i)"
1244       using u v  `0 \<le> a` unfolding incseq_Suc_iff le_fun_def
1245       by (auto intro!: add_mono extreal_mult_left_mono extreal_add_nonneg_nonneg)
1246     { fix x
1247       { fix i have "a * u i x \<noteq> -\<infinity>" "v i x \<noteq> -\<infinity>" "u i x \<noteq> -\<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x]
1248           by auto }
1249       then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
1250         using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
1251         by (subst SUPR_extreal_cmult[symmetric, OF u(6) `0 \<le> a`])
1252            (auto intro!: SUPR_extreal_add
1253                  simp: incseq_Suc_iff le_fun_def add_mono extreal_mult_left_mono extreal_add_nonneg_nonneg) }
1254     then show "AE x. (SUP i. l i x) = (SUP i. ?L' i x)"
1255       unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
1256       by (intro AE_I2) (auto split: split_max simp add: extreal_add_nonneg_nonneg)
1257   qed
1258   also have "\<dots> = (SUP i. a * integral\<^isup>S M (u i) + integral\<^isup>S M (v i))"
1259     using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPR UNIV"] ext)
1260   finally have "(\<integral>\<^isup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^isup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^isup>+x. max 0 (g x) \<partial>M)"
1261     unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
1262     unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
1263     apply (subst SUPR_extreal_cmult[symmetric, OF pos(1) `0 \<le> a`])
1264     apply (subst SUPR_extreal_add[symmetric, OF inc not_MInf]) .
1265   then show ?thesis by (simp add: positive_integral_max_0)
1266 qed
1268 lemma (in measure_space) positive_integral_cmult:
1269   assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x" "0 \<le> c"
1270   shows "(\<integral>\<^isup>+ x. c * f x \<partial>M) = c * integral\<^isup>P M f"
1271 proof -
1272   have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c`
1273     by (auto split: split_max simp: extreal_zero_le_0_iff)
1274   have "(\<integral>\<^isup>+ x. c * f x \<partial>M) = (\<integral>\<^isup>+ x. c * max 0 (f x) \<partial>M)"
1275     by (simp add: positive_integral_max_0)
1276   then show ?thesis
1277     using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" "\<lambda>x. 0"] f
1278     by (auto simp: positive_integral_max_0)
1279 qed
1281 lemma (in measure_space) positive_integral_multc:
1282   assumes "f \<in> borel_measurable M" "AE x. 0 \<le> f x" "0 \<le> c"
1283   shows "(\<integral>\<^isup>+ x. f x * c \<partial>M) = integral\<^isup>P M f * c"
1284   unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
1286 lemma (in measure_space) positive_integral_indicator[simp]:
1287   "A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x\<partial>M) = \<mu> A"
1288   by (subst positive_integral_eq_simple_integral)
1289      (auto simp: simple_function_indicator simple_integral_indicator)
1291 lemma (in measure_space) positive_integral_cmult_indicator:
1292   "0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x \<partial>M) = c * \<mu> A"
1293   by (subst positive_integral_eq_simple_integral)
1294      (auto simp: simple_function_indicator simple_integral_indicator)
1296 lemma (in measure_space) positive_integral_add:
1297   assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x"
1298   and g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
1299   shows "(\<integral>\<^isup>+ x. f x + g x \<partial>M) = integral\<^isup>P M f + integral\<^isup>P M g"
1300 proof -
1301   have ae: "AE x. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)"
1302     using assms by (auto split: split_max simp: extreal_add_nonneg_nonneg)
1303   have "(\<integral>\<^isup>+ x. f x + g x \<partial>M) = (\<integral>\<^isup>+ x. max 0 (f x + g x) \<partial>M)"
1304     by (simp add: positive_integral_max_0)
1305   also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (f x) + max 0 (g x) \<partial>M)"
1306     unfolding ae[THEN positive_integral_cong_AE] ..
1307   also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (f x) \<partial>M) + (\<integral>\<^isup>+ x. max 0 (g x) \<partial>M)"
1308     using positive_integral_linear[of "\<lambda>x. max 0 (f x)" 1 "\<lambda>x. max 0 (g x)"] f g
1309     by auto
1310   finally show ?thesis
1311     by (simp add: positive_integral_max_0)
1312 qed
1314 lemma (in measure_space) positive_integral_setsum:
1315   assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" "\<And>i. i\<in>P \<Longrightarrow> AE x. 0 \<le> f i x"
1316   shows "(\<integral>\<^isup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>P M (f i))"
1317 proof cases
1318   assume f: "finite P"
1319   from assms have "AE x. \<forall>i\<in>P. 0 \<le> f i x" unfolding AE_finite_all[OF f] by auto
1320   from f this assms(1) show ?thesis
1321   proof induct
1322     case (insert i P)
1323     then have "f i \<in> borel_measurable M" "AE x. 0 \<le> f i x"
1324       "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x. 0 \<le> (\<Sum>i\<in>P. f i x)"
1325       by (auto intro!: borel_measurable_extreal_setsum setsum_nonneg)
1326     from positive_integral_add[OF this]
1327     show ?case using insert by auto
1328   qed simp
1329 qed simp
1331 lemma (in measure_space) positive_integral_Markov_inequality:
1332   assumes u: "u \<in> borel_measurable M" "AE x. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c" "c \<noteq> \<infinity>"
1333   shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
1334     (is "\<mu> ?A \<le> _ * ?PI")
1335 proof -
1336   have "?A \<in> sets M"
1337     using `A \<in> sets M` u by auto
1338   hence "\<mu> ?A = (\<integral>\<^isup>+ x. indicator ?A x \<partial>M)"
1339     using positive_integral_indicator by simp
1340   also have "\<dots> \<le> (\<integral>\<^isup>+ x. c * (u x * indicator A x) \<partial>M)" using u c
1341     by (auto intro!: positive_integral_mono_AE
1342       simp: indicator_def extreal_zero_le_0_iff)
1343   also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
1344     using assms
1345     by (auto intro!: positive_integral_cmult borel_measurable_indicator simp: extreal_zero_le_0_iff)
1346   finally show ?thesis .
1347 qed
1349 lemma (in measure_space) positive_integral_noteq_infinite:
1350   assumes g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
1351   and "integral\<^isup>P M g \<noteq> \<infinity>"
1352   shows "AE x. g x \<noteq> \<infinity>"
1353 proof (rule ccontr)
1354   assume c: "\<not> (AE x. g x \<noteq> \<infinity>)"
1355   have "\<mu> {x\<in>space M. g x = \<infinity>} \<noteq> 0"
1356     using c g by (simp add: AE_iff_null_set)
1357   moreover have "0 \<le> \<mu> {x\<in>space M. g x = \<infinity>}" using g by (auto intro: measurable_sets)
1358   ultimately have "0 < \<mu> {x\<in>space M. g x = \<infinity>}" by auto
1359   then have "\<infinity> = \<infinity> * \<mu> {x\<in>space M. g x = \<infinity>}" by auto
1360   also have "\<dots> \<le> (\<integral>\<^isup>+x. \<infinity> * indicator {x\<in>space M. g x = \<infinity>} x \<partial>M)"
1361     using g by (subst positive_integral_cmult_indicator) auto
1362   also have "\<dots> \<le> integral\<^isup>P M g"
1363     using assms by (auto intro!: positive_integral_mono_AE simp: indicator_def)
1364   finally show False using `integral\<^isup>P M g \<noteq> \<infinity>` by auto
1365 qed
1367 lemma (in measure_space) positive_integral_diff:
1368   assumes f: "f \<in> borel_measurable M"
1369   and g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
1370   and fin: "integral\<^isup>P M g \<noteq> \<infinity>"
1371   and mono: "AE x. g x \<le> f x"
1372   shows "(\<integral>\<^isup>+ x. f x - g x \<partial>M) = integral\<^isup>P M f - integral\<^isup>P M g"
1373 proof -
1374   have diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M" "AE x. 0 \<le> f x - g x"
1375     using assms by (auto intro: extreal_diff_positive)
1376   have pos_f: "AE x. 0 \<le> f x" using mono g by auto
1377   { fix a b :: extreal assume "0 \<le> a" "a \<noteq> \<infinity>" "0 \<le> b" "a \<le> b" then have "b - a + a = b"
1378       by (cases rule: extreal2_cases[of a b]) auto }
1379   note * = this
1380   then have "AE x. f x = f x - g x + g x"
1381     using mono positive_integral_noteq_infinite[OF g fin] assms by auto
1382   then have **: "integral\<^isup>P M f = (\<integral>\<^isup>+x. f x - g x \<partial>M) + integral\<^isup>P M g"
1383     unfolding positive_integral_add[OF diff g, symmetric]
1384     by (rule positive_integral_cong_AE)
1385   show ?thesis unfolding **
1386     using fin positive_integral_positive[of g]
1387     by (cases rule: extreal2_cases[of "\<integral>\<^isup>+ x. f x - g x \<partial>M" "integral\<^isup>P M g"]) auto
1388 qed
1390 lemma (in measure_space) positive_integral_suminf:
1391   assumes f: "\<And>i. f i \<in> borel_measurable M" "\<And>i. AE x. 0 \<le> f i x"
1392   shows "(\<integral>\<^isup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^isup>P M (f i))"
1393 proof -
1394   have all_pos: "AE x. \<forall>i. 0 \<le> f i x"
1395     using assms by (auto simp: AE_all_countable)
1396   have "(\<Sum>i. integral\<^isup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^isup>P M (f i))"
1397     using positive_integral_positive by (rule suminf_extreal_eq_SUPR)
1398   also have "\<dots> = (SUP n. \<integral>\<^isup>+x. (\<Sum>i<n. f i x) \<partial>M)"
1399     unfolding positive_integral_setsum[OF f] ..
1400   also have "\<dots> = \<integral>\<^isup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
1401     by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
1402        (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
1403   also have "\<dots> = \<integral>\<^isup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
1404     by (intro positive_integral_cong_AE) (auto simp: suminf_extreal_eq_SUPR)
1405   finally show ?thesis by simp
1406 qed
1408 text {* Fatou's lemma: convergence theorem on limes inferior *}
1409 lemma (in measure_space) positive_integral_lim_INF:
1410   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> extreal"
1411   assumes u: "\<And>i. u i \<in> borel_measurable M" "\<And>i. AE x. 0 \<le> u i x"
1412   shows "(\<integral>\<^isup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
1413 proof -
1414   have pos: "AE x. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
1415   have "(\<integral>\<^isup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
1416     (SUP n. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>M)"
1417     unfolding liminf_SUPR_INFI using pos u
1418     by (intro positive_integral_monotone_convergence_SUP_AE)
1419        (elim AE_mp, auto intro!: AE_I2 intro: le_INFI INF_subset)
1420   also have "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
1421     unfolding liminf_SUPR_INFI
1422     by (auto intro!: SUP_mono exI le_INFI positive_integral_mono INF_leI)
1423   finally show ?thesis .
1424 qed
1426 lemma (in measure_space) measure_space_density:
1427   assumes u: "u \<in> borel_measurable M" "AE x. 0 \<le> u x"
1428     and M'[simp]: "M' = (M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)\<rparr>)"
1429   shows "measure_space M'"
1430 proof -
1431   interpret M': sigma_algebra M' by (intro sigma_algebra_cong) auto
1432   show ?thesis
1433   proof
1434     have pos: "\<And>A. AE x. 0 \<le> u x * indicator A x"
1435       using u by (auto simp: extreal_zero_le_0_iff)
1436     then show "positive M' (measure M')" unfolding M'
1437       using u(1) by (auto simp: positive_def intro!: positive_integral_positive)
1438     show "countably_additive M' (measure M')"
1439     proof (intro countably_additiveI)
1440       fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M'"
1441       then have *: "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M"
1442         using u by (auto intro: borel_measurable_indicator)
1443       assume disj: "disjoint_family A"
1444       have "(\<Sum>n. measure M' (A n)) = (\<integral>\<^isup>+ x. (\<Sum>n. u x * indicator (A n) x) \<partial>M)"
1445         unfolding M' using u(1) *
1446         by (simp add: positive_integral_suminf[OF _ pos, symmetric])
1447       also have "\<dots> = (\<integral>\<^isup>+ x. u x * (\<Sum>n. indicator (A n) x) \<partial>M)" using u
1448         by (intro positive_integral_cong_AE)
1449            (elim AE_mp, auto intro!: AE_I2 suminf_cmult_extreal)
1450       also have "\<dots> = (\<integral>\<^isup>+ x. u x * indicator (\<Union>n. A n) x \<partial>M)"
1451         unfolding suminf_indicator[OF disj] ..
1452       finally show "(\<Sum>n. measure M' (A n)) = measure M' (\<Union>x. A x)"
1453         unfolding M' by simp
1454     qed
1455   qed
1456 qed
1458 lemma (in measure_space) positive_integral_null_set:
1459   assumes "N \<in> null_sets" shows "(\<integral>\<^isup>+ x. u x * indicator N x \<partial>M) = 0"
1460 proof -
1461   have "(\<integral>\<^isup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)"
1462   proof (intro positive_integral_cong_AE AE_I)
1463     show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N"
1464       by (auto simp: indicator_def)
1465     show "\<mu> N = 0" "N \<in> sets M"
1466       using assms by auto
1467   qed
1468   then show ?thesis by simp
1469 qed
1471 lemma (in measure_space) positive_integral_translated_density:
1472   assumes f: "f \<in> borel_measurable M" "AE x. 0 \<le> f x"
1473   assumes g: "g \<in> borel_measurable M" "AE x. 0 \<le> g x"
1474     and M': "M' = (M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)\<rparr>)"
1475   shows "integral\<^isup>P M' g = (\<integral>\<^isup>+ x. f x * g x \<partial>M)"
1476 proof -
1477   from measure_space_density[OF f M']
1478   interpret T: measure_space M' .
1479   have borel[simp]:
1480     "borel_measurable M' = borel_measurable M"
1481     "simple_function M' = simple_function M"
1482     unfolding measurable_def simple_function_def_raw by (auto simp: M')
1483   from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
1484   note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
1485   note G'(2)[simp]
1486   { fix P have "AE x. P x \<Longrightarrow> AE x in M'. P x"
1487       using positive_integral_null_set[of _ f]
1488       unfolding T.almost_everywhere_def almost_everywhere_def
1489       by (auto simp: M') }
1490   note ac = this
1491   from G(4) g(2) have G_M': "AE x in M'. (SUP i. G i x) = g x"
1492     by (auto intro!: ac split: split_max)
1493   { fix i
1494     let "?I y x" = "indicator (G i -` {y} \<inter> space M) x"
1495     { fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"
1496       then have [simp]: "G i ` space M \<inter> {y. G i x = y \<and> x \<in> space M} = {G i x}" by auto
1497       from * G' G have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * (\<Sum>y\<in>G i`space M. (y * ?I y x))"
1498         by (subst setsum_extreal_right_distrib) (auto simp: ac_simps)
1499       also have "\<dots> = f x * G i x"
1500         by (simp add: indicator_def if_distrib setsum_cases)
1501       finally have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * G i x" . }
1502     note to_singleton = this
1503     have "integral\<^isup>P M' (G i) = integral\<^isup>S M' (G i)"
1504       using G T.positive_integral_eq_simple_integral by simp
1505     also have "\<dots> = (\<Sum>y\<in>G i`space M. y * (\<integral>\<^isup>+x. f x * ?I y x \<partial>M))"
1506       unfolding simple_integral_def M' by simp
1507     also have "\<dots> = (\<Sum>y\<in>G i`space M. (\<integral>\<^isup>+x. y * (f x * ?I y x) \<partial>M))"
1508       using f G' G by (auto intro!: setsum_cong positive_integral_cmult[symmetric])
1509     also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) \<partial>M)"
1510       using f G' G by (auto intro!: positive_integral_setsum[symmetric])
1511     finally have "integral\<^isup>P M' (G i) = (\<integral>\<^isup>+x. f x * G i x \<partial>M)"
1512       using f g G' to_singleton by (auto intro!: positive_integral_cong_AE) }
1513   note [simp] = this
1514   have "integral\<^isup>P M' g = (SUP i. integral\<^isup>P M' (G i))" using G'(1) G_M'(1) G
1515     using T.positive_integral_monotone_convergence_SUP[symmetric, OF `incseq G`]
1516     by (simp cong: T.positive_integral_cong_AE)
1517   also have "\<dots> = (SUP i. (\<integral>\<^isup>+x. f x * G i x \<partial>M))" by simp
1518   also have "\<dots> = (\<integral>\<^isup>+x. (SUP i. f x * G i x) \<partial>M)"
1519     using f G' G(2)[THEN incseq_SucD] G
1520     by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
1521        (auto simp: extreal_mult_left_mono le_fun_def extreal_zero_le_0_iff)
1522   also have "\<dots> = (\<integral>\<^isup>+x. f x * g x \<partial>M)" using f G' G g
1523     by (intro positive_integral_cong_AE)
1524        (auto simp add: SUPR_extreal_cmult split: split_max)
1525   finally show "integral\<^isup>P M' g = (\<integral>\<^isup>+x. f x * g x \<partial>M)" .
1526 qed
1528 lemma (in measure_space) positive_integral_0_iff:
1529   assumes u: "u \<in> borel_measurable M" and pos: "AE x. 0 \<le> u x"
1530   shows "integral\<^isup>P M u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0"
1531     (is "_ \<longleftrightarrow> \<mu> ?A = 0")
1532 proof -
1533   have u_eq: "(\<integral>\<^isup>+ x. u x * indicator ?A x \<partial>M) = integral\<^isup>P M u"
1534     by (auto intro!: positive_integral_cong simp: indicator_def)
1535   show ?thesis
1536   proof
1537     assume "\<mu> ?A = 0"
1538     with positive_integral_null_set[of ?A u] u
1539     show "integral\<^isup>P M u = 0" by (simp add: u_eq)
1540   next
1541     { fix r :: extreal and n :: nat assume gt_1: "1 \<le> real n * r"
1542       then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_extreal_def)
1543       then have "0 \<le> r" by (auto simp add: extreal_zero_less_0_iff) }
1544     note gt_1 = this
1545     assume *: "integral\<^isup>P M u = 0"
1546     let "?M n" = "{x \<in> space M. 1 \<le> real (n::nat) * u x}"
1547     have "0 = (SUP n. \<mu> (?M n \<inter> ?A))"
1548     proof -
1549       { fix n :: nat
1550         from positive_integral_Markov_inequality[OF u pos, of ?A "extreal (real n)"]
1551         have "\<mu> (?M n \<inter> ?A) \<le> 0" unfolding u_eq * using u by simp
1552         moreover have "0 \<le> \<mu> (?M n \<inter> ?A)" using u by auto
1553         ultimately have "\<mu> (?M n \<inter> ?A) = 0" by auto }
1554       thus ?thesis by simp
1555     qed
1556     also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)"
1557     proof (safe intro!: continuity_from_below)
1558       fix n show "?M n \<inter> ?A \<in> sets M"
1559         using u by (auto intro!: Int)
1560     next
1561       show "incseq (\<lambda>n. {x \<in> space M. 1 \<le> real n * u x} \<inter> {x \<in> space M. u x \<noteq> 0})"
1562       proof (safe intro!: incseq_SucI)
1563         fix n :: nat and x
1564         assume *: "1 \<le> real n * u x"
1565         also from gt_1[OF this] have "real n * u x \<le> real (Suc n) * u x"
1566           using `0 \<le> u x` by (auto intro!: extreal_mult_right_mono)
1567         finally show "1 \<le> real (Suc n) * u x" by auto
1568       qed
1569     qed
1570     also have "\<dots> = \<mu> {x\<in>space M. 0 < u x}"
1571     proof (safe intro!: arg_cong[where f="\<mu>"] dest!: gt_1)
1572       fix x assume "0 < u x" and [simp, intro]: "x \<in> space M"
1573       show "x \<in> (\<Union>n. ?M n \<inter> ?A)"
1574       proof (cases "u x")
1575         case (real r) with `0 < u x` have "0 < r" by auto
1576         obtain j :: nat where "1 / r \<le> real j" using real_arch_simple ..
1577         hence "1 / r * r \<le> real j * r" unfolding mult_le_cancel_right using `0 < r` by auto
1578         hence "1 \<le> real j * r" using real `0 < r` by auto
1579         thus ?thesis using `0 < r` real by (auto simp: one_extreal_def)
1580       qed (insert `0 < u x`, auto)
1581     qed auto
1582     finally have "\<mu> {x\<in>space M. 0 < u x} = 0" by simp
1583     moreover
1584     from pos have "AE x. \<not> (u x < 0)" by auto
1585     then have "\<mu> {x\<in>space M. u x < 0} = 0"
1586       using AE_iff_null_set u by auto
1587     moreover have "\<mu> {x\<in>space M. u x \<noteq> 0} = \<mu> {x\<in>space M. u x < 0} + \<mu> {x\<in>space M. 0 < u x}"
1588       using u by (subst measure_additive) (auto intro!: arg_cong[where f=\<mu>])
1589     ultimately show "\<mu> ?A = 0" by simp
1590   qed
1591 qed
1593 lemma (in measure_space) positive_integral_0_iff_AE:
1594   assumes u: "u \<in> borel_measurable M"
1595   shows "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. u x \<le> 0)"
1596 proof -
1597   have sets: "{x\<in>space M. max 0 (u x) \<noteq> 0} \<in> sets M"
1598     using u by auto
1599   from positive_integral_0_iff[of "\<lambda>x. max 0 (u x)"]
1600   have "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. max 0 (u x) = 0)"
1601     unfolding positive_integral_max_0
1602     using AE_iff_null_set[OF sets] u by auto
1603   also have "\<dots> \<longleftrightarrow> (AE x. u x \<le> 0)" by (auto split: split_max)
1604   finally show ?thesis .
1605 qed
1607 lemma (in measure_space) positive_integral_restricted:
1608   assumes A: "A \<in> sets M"
1609   shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
1610     (is "integral\<^isup>P ?R f = integral\<^isup>P M ?f")
1611 proof -
1612   interpret R: measure_space ?R
1613     by (rule restricted_measure_space) fact
1614   let "?I g x" = "g x * indicator A x :: extreal"
1615   show ?thesis
1616     unfolding positive_integral_def
1617     unfolding simple_function_restricted[OF A]
1618     unfolding AE_restricted[OF A]
1619   proof (safe intro!: SUPR_eq)
1620     fix g assume g: "simple_function M (?I g)" and le: "g \<le> max 0 \<circ> f"
1621     show "\<exists>j\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> ?I f}.
1622       integral\<^isup>S (restricted_space A) g \<le> integral\<^isup>S M j"
1623     proof (safe intro!: bexI[of _ "?I g"])
1624       show "integral\<^isup>S (restricted_space A) g \<le> integral\<^isup>S M (?I g)"
1625         using g A by (simp add: simple_integral_restricted)
1626       show "?I g \<le> max 0 \<circ> ?I f"
1627         using le by (auto simp: le_fun_def max_def indicator_def split: split_if_asm)
1628     qed fact
1629   next
1630     fix g assume g: "simple_function M g" and le: "g \<le> max 0 \<circ> ?I f"
1631     show "\<exists>i\<in>{g. simple_function M (?I g) \<and> g \<le> max 0 \<circ> f}.
1632       integral\<^isup>S M g \<le> integral\<^isup>S (restricted_space A) i"
1633     proof (safe intro!: bexI[of _ "?I g"])
1634       show "?I g \<le> max 0 \<circ> f"
1635         using le by (auto simp: le_fun_def max_def indicator_def split: split_if_asm)
1636       from le have "\<And>x. g x \<le> ?I (?I g) x"
1637         by (auto simp: le_fun_def max_def indicator_def split: split_if_asm)
1638       then show "integral\<^isup>S M g \<le> integral\<^isup>S (restricted_space A) (?I g)"
1639         using A g by (auto intro!: simple_integral_mono simp: simple_integral_restricted)
1640       show "simple_function M (?I (?I g))" using g A by auto
1641     qed
1642   qed
1643 qed
1645 lemma (in measure_space) positive_integral_subalgebra:
1646   assumes f: "f \<in> borel_measurable N" "AE x in N. 0 \<le> f x"
1647   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A"
1648   and sa: "sigma_algebra N"
1649   shows "integral\<^isup>P N f = integral\<^isup>P M f"
1650 proof -
1651   interpret N: measure_space N using measure_space_subalgebra[OF sa N] .
1652   from N.borel_measurable_implies_simple_function_sequence'[OF f(1)] guess fs . note fs = this
1653   note sf = simple_function_subalgebra[OF fs(1) N(1,2)]
1654   from N.positive_integral_monotone_convergence_simple[OF fs(2,5,1), symmetric]
1655   have "integral\<^isup>P N f = (SUP i. \<Sum>x\<in>fs i ` space M. x * N.\<mu> (fs i -` {x} \<inter> space M))"
1656     unfolding fs(4) positive_integral_max_0
1657     unfolding simple_integral_def `space N = space M` by simp
1658   also have "\<dots> = (SUP i. \<Sum>x\<in>fs i ` space M. x * \<mu> (fs i -` {x} \<inter> space M))"
1659     using N N.simple_functionD(2)[OF fs(1)] unfolding `space N = space M` by auto
1660   also have "\<dots> = integral\<^isup>P M f"
1661     using positive_integral_monotone_convergence_simple[OF fs(2,5) sf, symmetric]
1662     unfolding fs(4) positive_integral_max_0
1663     unfolding simple_integral_def `space N = space M` by simp
1664   finally show ?thesis .
1665 qed
1667 section "Lebesgue Integral"
1669 definition integrable where
1670   "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
1671     (\<integral>\<^isup>+ x. extreal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^isup>+ x. extreal (- f x) \<partial>M) \<noteq> \<infinity>"
1673 lemma integrableD[dest]:
1674   assumes "integrable M f"
1675   shows "f \<in> borel_measurable M" "(\<integral>\<^isup>+ x. extreal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^isup>+ x. extreal (- f x) \<partial>M) \<noteq> \<infinity>"
1676   using assms unfolding integrable_def by auto
1678 definition lebesgue_integral_def:
1679   "integral\<^isup>L M f = real ((\<integral>\<^isup>+ x. extreal (f x) \<partial>M)) - real ((\<integral>\<^isup>+ x. extreal (- f x) \<partial>M))"
1681 syntax
1682   "_lebesgue_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110)
1684 translations
1685   "\<integral> x. f \<partial>M" == "CONST integral\<^isup>L M (%x. f)"
1687 lemma (in measure_space) integrableE:
1688   assumes "integrable M f"
1689   obtains r q where
1690     "(\<integral>\<^isup>+x. extreal (f x)\<partial>M) = extreal r"
1691     "(\<integral>\<^isup>+x. extreal (-f x)\<partial>M) = extreal q"
1692     "f \<in> borel_measurable M" "integral\<^isup>L M f = r - q"
1693   using assms unfolding integrable_def lebesgue_integral_def
1694   using positive_integral_positive[of "\<lambda>x. extreal (f x)"]
1695   using positive_integral_positive[of "\<lambda>x. extreal (-f x)"]
1696   by (cases rule: extreal2_cases[of "(\<integral>\<^isup>+x. extreal (-f x)\<partial>M)" "(\<integral>\<^isup>+x. extreal (f x)\<partial>M)"]) auto
1698 lemma (in measure_space) integral_cong:
1699   assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
1700   shows "integral\<^isup>L M f = integral\<^isup>L M g"
1701   using assms by (simp cong: positive_integral_cong add: lebesgue_integral_def)
1703 lemma (in measure_space) integral_cong_measure:
1704   assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M"
1705   shows "integral\<^isup>L N f = integral\<^isup>L M f"
1706   by (simp add: positive_integral_cong_measure[OF assms] lebesgue_integral_def)
1708 lemma (in measure_space) integral_cong_AE:
1709   assumes cong: "AE x. f x = g x"
1710   shows "integral\<^isup>L M f = integral\<^isup>L M g"
1711 proof -
1712   have *: "AE x. extreal (f x) = extreal (g x)"
1713     "AE x. extreal (- f x) = extreal (- g x)" using cong by auto
1714   show ?thesis
1715     unfolding *[THEN positive_integral_cong_AE] lebesgue_integral_def ..
1716 qed
1718 lemma (in measure_space) integrable_cong:
1719   "(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable M g"
1720   by (simp cong: positive_integral_cong measurable_cong add: integrable_def)
1722 lemma (in measure_space) integral_eq_positive_integral:
1723   assumes f: "\<And>x. 0 \<le> f x"
1724   shows "integral\<^isup>L M f = real (\<integral>\<^isup>+ x. extreal (f x) \<partial>M)"
1725 proof -
1726   { fix x have "max 0 (extreal (- f x)) = 0" using f[of x] by (simp split: split_max) }
1727   then have "0 = (\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>M)" by simp
1728   also have "\<dots> = (\<integral>\<^isup>+ x. extreal (- f x) \<partial>M)" unfolding positive_integral_max_0 ..
1729   finally show ?thesis
1730     unfolding lebesgue_integral_def by simp
1731 qed
1733 lemma (in measure_space) integral_vimage:
1734   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
1735   assumes f: "f \<in> borel_measurable M'"
1736   shows "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)"
1737 proof -
1738   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
1739   from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
1740   have borel: "(\<lambda>x. extreal (f x)) \<in> borel_measurable M'" "(\<lambda>x. extreal (- f x)) \<in> borel_measurable M'"
1741     and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
1742     using f by (auto simp: comp_def)
1743   then show ?thesis
1744     using f unfolding lebesgue_integral_def integrable_def
1745     by (auto simp: borel[THEN positive_integral_vimage[OF T]])
1746 qed
1748 lemma (in measure_space) integrable_vimage:
1749   assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
1750   assumes f: "integrable M' f"
1751   shows "integrable M (\<lambda>x. f (T x))"
1752 proof -
1753   interpret T: measure_space M' by (rule measure_space_vimage[OF T])
1754   from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel]
1755   have borel: "(\<lambda>x. extreal (f x)) \<in> borel_measurable M'" "(\<lambda>x. extreal (- f x)) \<in> borel_measurable M'"
1756     and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
1757     using f by (auto simp: comp_def)
1758   then show ?thesis
1759     using f unfolding lebesgue_integral_def integrable_def
1760     by (auto simp: borel[THEN positive_integral_vimage[OF T]])
1761 qed
1763 lemma (in measure_space) integral_minus[intro, simp]:
1764   assumes "integrable M f"
1765   shows "integrable M (\<lambda>x. - f x)" "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
1766   using assms by (auto simp: integrable_def lebesgue_integral_def)
1768 lemma (in measure_space) integral_of_positive_diff:
1769   assumes integrable: "integrable M u" "integrable M v"
1770   and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x"
1771   shows "integrable M f" and "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
1772 proof -
1773   let "?f x" = "max 0 (extreal (f x))"
1774   let "?mf x" = "max 0 (extreal (- f x))"
1775   let "?u x" = "max 0 (extreal (u x))"
1776   let "?v x" = "max 0 (extreal (v x))"
1778   from borel_measurable_diff[of u v] integrable
1779   have f_borel: "?f \<in> borel_measurable M" and
1780     mf_borel: "?mf \<in> borel_measurable M" and
1781     v_borel: "?v \<in> borel_measurable M" and
1782     u_borel: "?u \<in> borel_measurable M" and
1783     "f \<in> borel_measurable M"
1784     by (auto simp: f_def[symmetric] integrable_def)
1786   have "(\<integral>\<^isup>+ x. extreal (u x - v x) \<partial>M) \<le> integral\<^isup>P M ?u"
1787     using pos by (auto intro!: positive_integral_mono simp: positive_integral_max_0)
1788   moreover have "(\<integral>\<^isup>+ x. extreal (v x - u x) \<partial>M) \<le> integral\<^isup>P M ?v"
1789     using pos by (auto intro!: positive_integral_mono simp: positive_integral_max_0)
1790   ultimately show f: "integrable M f"
1791     using `integrable M u` `integrable M v` `f \<in> borel_measurable M`
1792     by (auto simp: integrable_def f_def positive_integral_max_0)
1794   have "\<And>x. ?u x + ?mf x = ?v x + ?f x"
1795     unfolding f_def using pos by (simp split: split_max)
1796   then have "(\<integral>\<^isup>+ x. ?u x + ?mf x \<partial>M) = (\<integral>\<^isup>+ x. ?v x + ?f x \<partial>M)" by simp
1797   then have "real (integral\<^isup>P M ?u + integral\<^isup>P M ?mf) =
1798       real (integral\<^isup>P M ?v + integral\<^isup>P M ?f)"
1799     using positive_integral_add[OF u_borel _ mf_borel]
1800     using positive_integral_add[OF v_borel _ f_borel]
1801     by auto
1802   then show "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v"
1803     unfolding positive_integral_max_0
1804     unfolding pos[THEN integral_eq_positive_integral]
1805     using integrable f by (auto elim!: integrableE)
1806 qed
1808 lemma (in measure_space) integral_linear:
1809   assumes "integrable M f" "integrable M g" and "0 \<le> a"
1810   shows "integrable M (\<lambda>t. a * f t + g t)"
1811   and "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" (is ?EQ)
1812 proof -
1813   let "?f x" = "max 0 (extreal (f x))"
1814   let "?g x" = "max 0 (extreal (g x))"
1815   let "?mf x" = "max 0 (extreal (- f x))"
1816   let "?mg x" = "max 0 (extreal (- g x))"
1817   let "?p t" = "max 0 (a * f t) + max 0 (g t)"
1818   let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)"
1820   from assms have linear:
1821     "(\<integral>\<^isup>+ x. extreal a * ?f x + ?g x \<partial>M) = extreal a * integral\<^isup>P M ?f + integral\<^isup>P M ?g"
1822     "(\<integral>\<^isup>+ x. extreal a * ?mf x + ?mg x \<partial>M) = extreal a * integral\<^isup>P M ?mf + integral\<^isup>P M ?mg"
1823     by (auto intro!: positive_integral_linear simp: integrable_def)
1825   have *: "(\<integral>\<^isup>+x. extreal (- ?p x) \<partial>M) = 0" "(\<integral>\<^isup>+x. extreal (- ?n x) \<partial>M) = 0"
1826     using `0 \<le> a` assms by (auto simp: positive_integral_0_iff_AE integrable_def)
1827   have **: "\<And>x. extreal a * ?f x + ?g x = max 0 (extreal (?p x))"
1828            "\<And>x. extreal a * ?mf x + ?mg x = max 0 (extreal (?n x))"
1829     using `0 \<le> a` by (auto split: split_max simp: zero_le_mult_iff mult_le_0_iff)
1831   have "integrable M ?p" "integrable M ?n"
1832       "\<And>t. a * f t + g t = ?p t - ?n t" "\<And>t. 0 \<le> ?p t" "\<And>t. 0 \<le> ?n t"
1833     using linear assms unfolding integrable_def ** *
1834     by (auto simp: positive_integral_max_0)
1835   note diff = integral_of_positive_diff[OF this]
1837   show "integrable M (\<lambda>t. a * f t + g t)" by (rule diff)
1838   from assms linear show ?EQ
1839     unfolding diff(2) ** positive_integral_max_0
1840     unfolding lebesgue_integral_def *
1841     by (auto elim!: integrableE simp: field_simps)
1842 qed
1844 lemma (in measure_space) integral_add[simp, intro]:
1845   assumes "integrable M f" "integrable M g"
1846   shows "integrable M (\<lambda>t. f t + g t)"
1847   and "(\<integral> t. f t + g t \<partial>M) = integral\<^isup>L M f + integral\<^isup>L M g"
1848   using assms integral_linear[where a=1] by auto
1850 lemma (in measure_space) integral_zero[simp, intro]:
1851   shows "integrable M (\<lambda>x. 0)" "(\<integral> x.0 \<partial>M) = 0"
1852   unfolding integrable_def lebesgue_integral_def
1853   by (auto simp add: borel_measurable_const)
1855 lemma (in measure_space) integral_cmult[simp, intro]:
1856   assumes "integrable M f"
1857   shows "integrable M (\<lambda>t. a * f t)" (is ?P)
1858   and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I)
1859 proof -
1860   have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f"
1861   proof (cases rule: le_cases)
1862     assume "0 \<le> a" show ?thesis
1863       using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
1864       by (simp add: integral_zero)
1865   next
1866     assume "a \<le> 0" hence "0 \<le> - a" by auto
1867     have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
1868     show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
1869         integral_minus(1)[of "\<lambda>t. - a * f t"]
1870       unfolding * integral_zero by simp
1871   qed
1872   thus ?P ?I by auto
1873 qed
1875 lemma (in measure_space) integral_multc:
1876   assumes "integrable M f"
1877   shows "(\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
1878   unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
1880 lemma (in measure_space) integral_mono_AE:
1881   assumes fg: "integrable M f" "integrable M g"
1882   and mono: "AE t. f t \<le> g t"
1883   shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
1884 proof -
1885   have "AE x. extreal (f x) \<le> extreal (g x)"
1886     using mono by auto
1887   moreover have "AE x. extreal (- g x) \<le> extreal (- f x)"
1888     using mono by auto
1889   ultimately show ?thesis using fg
1890     by (auto intro!: add_mono positive_integral_mono_AE real_of_extreal_positive_mono
1891              simp: positive_integral_positive lebesgue_integral_def diff_minus)
1892 qed
1894 lemma (in measure_space) integral_mono:
1895   assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
1896   shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
1897   using assms by (auto intro: integral_mono_AE)
1899 lemma (in measure_space) integral_diff[simp, intro]:
1900   assumes f: "integrable M f" and g: "integrable M g"
1901   shows "integrable M (\<lambda>t. f t - g t)"
1902   and "(\<integral> t. f t - g t \<partial>M) = integral\<^isup>L M f - integral\<^isup>L M g"
1903   using integral_add[OF f integral_minus(1)[OF g]]
1904   unfolding diff_minus integral_minus(2)[OF g]
1905   by auto
1907 lemma (in measure_space) integral_indicator[simp, intro]:
1908   assumes "A \<in> sets M" and "\<mu> A \<noteq> \<infinity>"
1909   shows "integral\<^isup>L M (indicator A) = real (\<mu> A)" (is ?int)
1910   and "integrable M (indicator A)" (is ?able)
1911 proof -
1912   from `A \<in> sets M` have *:
1913     "\<And>x. extreal (indicator A x) = indicator A x"
1914     "(\<integral>\<^isup>+x. extreal (- indicator A x) \<partial>M) = 0"
1915     by (auto split: split_indicator simp: positive_integral_0_iff_AE one_extreal_def)
1916   show ?int ?able
1917     using assms unfolding lebesgue_integral_def integrable_def
1918     by (auto simp: * positive_integral_indicator borel_measurable_indicator)
1919 qed
1921 lemma (in measure_space) integral_cmul_indicator:
1922   assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<infinity>"
1923   shows "integrable M (\<lambda>x. c * indicator A x)" (is ?P)
1924   and "(\<integral>x. c * indicator A x \<partial>M) = c * real (\<mu> A)" (is ?I)
1925 proof -
1926   show ?P
1927   proof (cases "c = 0")
1928     case False with assms show ?thesis by simp
1929   qed simp
1931   show ?I
1932   proof (cases "c = 0")
1933     case False with assms show ?thesis by simp
1934   qed simp
1935 qed
1937 lemma (in measure_space) integral_setsum[simp, intro]:
1938   assumes "\<And>n. n \<in> S \<Longrightarrow> integrable M (f n)"
1939   shows "(\<integral>x. (\<Sum> i \<in> S. f i x) \<partial>M) = (\<Sum> i \<in> S. integral\<^isup>L M (f i))" (is "?int S")
1940     and "integrable M (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S")
1941 proof -
1942   have "?int S \<and> ?I S"
1943   proof (cases "finite S")
1944     assume "finite S"
1945     from this assms show ?thesis by (induct S) simp_all
1946   qed simp
1947   thus "?int S" and "?I S" by auto
1948 qed
1950 lemma (in measure_space) integrable_abs:
1951   assumes "integrable M f"
1952   shows "integrable M (\<lambda> x. \<bar>f x\<bar>)"
1953 proof -
1954   from assms have *: "(\<integral>\<^isup>+x. extreal (- \<bar>f x\<bar>)\<partial>M) = 0"
1955     "\<And>x. extreal \<bar>f x\<bar> = max 0 (extreal (f x)) + max 0 (extreal (- f x))"
1956     by (auto simp: integrable_def positive_integral_0_iff_AE split: split_max)
1957   with assms show ?thesis
1958     by (simp add: positive_integral_add positive_integral_max_0 integrable_def)
1959 qed
1961 lemma (in measure_space) integral_subalgebra:
1962   assumes borel: "f \<in> borel_measurable N"
1963   and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A" and sa: "sigma_algebra N"
1964   shows "integrable N f \<longleftrightarrow> integrable M f" (is ?P)
1965     and "integral\<^isup>L N f = integral\<^isup>L M f" (is ?I)
1966 proof -
1967   interpret N: measure_space N using measure_space_subalgebra[OF sa N] .
1968   have "(\<integral>\<^isup>+ x. max 0 (extreal (f x)) \<partial>N) = (\<integral>\<^isup>+ x. max 0 (extreal (f x)) \<partial>M)"
1969        "(\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>N) = (\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>M)"
1970     using borel by (auto intro!: positive_integral_subalgebra N sa)
1971   moreover have "f \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable N"
1972     using assms unfolding measurable_def by auto
1973   ultimately show ?P ?I
1974     by (auto simp: integrable_def lebesgue_integral_def positive_integral_max_0)
1975 qed
1977 lemma (in measure_space) integrable_bound:
1978   assumes "integrable M f"
1979   and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
1980     "\<And>x. x \<in> space M \<Longrightarrow> \<bar>g x\<bar> \<le> f x"
1981   assumes borel: "g \<in> borel_measurable M"
1982   shows "integrable M g"
1983 proof -
1984   have "(\<integral>\<^isup>+ x. extreal (g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. extreal \<bar>g x\<bar> \<partial>M)"
1985     by (auto intro!: positive_integral_mono)
1986   also have "\<dots> \<le> (\<integral>\<^isup>+ x. extreal (f x) \<partial>M)"
1987     using f by (auto intro!: positive_integral_mono)
1988   also have "\<dots> < \<infinity>"
1989     using `integrable M f` unfolding integrable_def by auto
1990   finally have pos: "(\<integral>\<^isup>+ x. extreal (g x) \<partial>M) < \<infinity>" .
1992   have "(\<integral>\<^isup>+ x. extreal (- g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. extreal (\<bar>g x\<bar>) \<partial>M)"
1993     by (auto intro!: positive_integral_mono)
1994   also have "\<dots> \<le> (\<integral>\<^isup>+ x. extreal (f x) \<partial>M)"
1995     using f by (auto intro!: positive_integral_mono)
1996   also have "\<dots> < \<infinity>"
1997     using `integrable M f` unfolding integrable_def by auto
1998   finally have neg: "(\<integral>\<^isup>+ x. extreal (- g x) \<partial>M) < \<infinity>" .
2000   from neg pos borel show ?thesis
2001     unfolding integrable_def by auto
2002 qed
2004 lemma (in measure_space) integrable_abs_iff:
2005   "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda> x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
2006   by (auto intro!: integrable_bound[where g=f] integrable_abs)
2008 lemma (in measure_space) integrable_max:
2009   assumes int: "integrable M f" "integrable M g"
2010   shows "integrable M (\<lambda> x. max (f x) (g x))"
2011 proof (rule integrable_bound)
2012   show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
2013     using int by (simp add: integrable_abs)
2014   show "(\<lambda>x. max (f x) (g x)) \<in> borel_measurable M"
2015     using int unfolding integrable_def by auto
2016 next
2017   fix x assume "x \<in> space M"
2018   show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>max (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
2019     by auto
2020 qed
2022 lemma (in measure_space) integrable_min:
2023   assumes int: "integrable M f" "integrable M g"
2024   shows "integrable M (\<lambda> x. min (f x) (g x))"
2025 proof (rule integrable_bound)
2026   show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)"
2027     using int by (simp add: integrable_abs)
2028   show "(\<lambda>x. min (f x) (g x)) \<in> borel_measurable M"
2029     using int unfolding integrable_def by auto
2030 next
2031   fix x assume "x \<in> space M"
2032   show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>min (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>"
2033     by auto
2034 qed
2036 lemma (in measure_space) integral_triangle_inequality:
2037   assumes "integrable M f"
2038   shows "\<bar>integral\<^isup>L M f\<bar> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
2039 proof -
2040   have "\<bar>integral\<^isup>L M f\<bar> = max (integral\<^isup>L M f) (- integral\<^isup>L M f)" by auto
2041   also have "\<dots> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
2042       using assms integral_minus(2)[of f, symmetric]
2043       by (auto intro!: integral_mono integrable_abs simp del: integral_minus)
2044   finally show ?thesis .
2045 qed
2047 lemma (in measure_space) integral_positive:
2048   assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
2049   shows "0 \<le> integral\<^isup>L M f"
2050 proof -
2051   have "0 = (\<integral>x. 0 \<partial>M)" by (auto simp: integral_zero)
2052   also have "\<dots> \<le> integral\<^isup>L M f"
2053     using assms by (rule integral_mono[OF integral_zero(1)])
2054   finally show ?thesis .
2055 qed
2057 lemma (in measure_space) integral_monotone_convergence_pos:
2058   assumes i: "\<And>i. integrable M (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
2059   and pos: "\<And>x i. 0 \<le> f i x"
2060   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
2061   and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
2062   shows "integrable M u"
2063   and "integral\<^isup>L M u = x"
2064 proof -
2065   { fix x have "0 \<le> u x"
2066       using mono pos[of 0 x] incseq_le[OF _ lim, of x 0]
2067       by (simp add: mono_def incseq_def) }
2068   note pos_u = this
2070   have SUP_F: "\<And>x. (SUP n. extreal (f n x)) = extreal (u x)"
2071     unfolding SUP_eq_LIMSEQ[OF mono] by (rule lim)
2073   have borel_f: "\<And>i. (\<lambda>x. extreal (f i x)) \<in> borel_measurable M"
2074     using i unfolding integrable_def by auto
2075   hence "(\<lambda>x. SUP i. extreal (f i x)) \<in> borel_measurable M"
2076     by auto
2077   hence borel_u: "u \<in> borel_measurable M"
2078     by (auto simp: borel_measurable_extreal_iff SUP_F)
2080   hence [simp]: "\<And>i. (\<integral>\<^isup>+x. extreal (- f i x) \<partial>M) = 0" "(\<integral>\<^isup>+x. extreal (- u x) \<partial>M) = 0"
2081     using i borel_u pos pos_u by (auto simp: positive_integral_0_iff_AE integrable_def)
2083   have integral_eq: "\<And>n. (\<integral>\<^isup>+ x. extreal (f n x) \<partial>M) = extreal (integral\<^isup>L M (f n))"
2084     using i positive_integral_positive by (auto simp: extreal_real lebesgue_integral_def integrable_def)
2086   have pos_integral: "\<And>n. 0 \<le> integral\<^isup>L M (f n)"
2087     using pos i by (auto simp: integral_positive)
2088   hence "0 \<le> x"
2089     using LIMSEQ_le_const[OF ilim, of 0] by auto
2091   from mono pos i have pI: "(\<integral>\<^isup>+ x. extreal (u x) \<partial>M) = (SUP n. (\<integral>\<^isup>+ x. extreal (f n x) \<partial>M))"
2092     by (auto intro!: positive_integral_monotone_convergence_SUP
2093       simp: integrable_def incseq_mono incseq_Suc_iff le_fun_def SUP_F[symmetric])
2094   also have "\<dots> = extreal x" unfolding integral_eq
2095   proof (rule SUP_eq_LIMSEQ[THEN iffD2])
2096     show "mono (\<lambda>n. integral\<^isup>L M (f n))"
2097       using mono i by (auto simp: mono_def intro!: integral_mono)
2098     show "(\<lambda>n. integral\<^isup>L M (f n)) ----> x" using ilim .
2099   qed
2100   finally show  "integrable M u" "integral\<^isup>L M u = x" using borel_u `0 \<le> x`
2101     unfolding integrable_def lebesgue_integral_def by auto
2102 qed
2104 lemma (in measure_space) integral_monotone_convergence:
2105   assumes f: "\<And>i. integrable M (f i)" and "mono f"
2106   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
2107   and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
2108   shows "integrable M u"
2109   and "integral\<^isup>L M u = x"
2110 proof -
2111   have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)"
2112       using f by (auto intro!: integral_diff)
2113   have 2: "\<And>x. mono (\<lambda>n. f n x - f 0 x)" using `mono f`
2114       unfolding mono_def le_fun_def by auto
2115   have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f`
2116       unfolding mono_def le_fun_def by (auto simp: field_simps)
2117   have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x"
2118     using lim by (auto intro!: LIMSEQ_diff)
2119   have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)"
2120     using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff)
2121   note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5]
2122   have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)"
2123     using diff(1) f by (rule integral_add(1))
2124   with diff(2) f show "integrable M u" "integral\<^isup>L M u = x"
2125     by (auto simp: integral_diff)
2126 qed
2128 lemma (in measure_space) integral_0_iff:
2129   assumes "integrable M f"
2130   shows "(\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0"
2131 proof -
2132   have *: "(\<integral>\<^isup>+x. extreal (- \<bar>f x\<bar>) \<partial>M) = 0"
2133     using assms by (auto simp: positive_integral_0_iff_AE integrable_def)
2134   have "integrable M (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs)
2135   hence "(\<lambda>x. extreal (\<bar>f x\<bar>)) \<in> borel_measurable M"
2136     "(\<integral>\<^isup>+ x. extreal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" unfolding integrable_def by auto
2137   from positive_integral_0_iff[OF this(1)] this(2)
2138   show ?thesis unfolding lebesgue_integral_def *
2139     using positive_integral_positive[of "\<lambda>x. extreal \<bar>f x\<bar>"]
2140     by (auto simp add: real_of_extreal_eq_0)
2141 qed
2143 lemma (in measure_space) positive_integral_PInf:
2144   assumes f: "f \<in> borel_measurable M"
2145   and not_Inf: "integral\<^isup>P M f \<noteq> \<infinity>"
2146   shows "\<mu> (f -` {\<infinity>} \<inter> space M) = 0"
2147 proof -
2148   have "\<infinity> * \<mu> (f -` {\<infinity>} \<inter> space M) = (\<integral>\<^isup>+ x. \<infinity> * indicator (f -` {\<infinity>} \<inter> space M) x \<partial>M)"
2149     using f by (subst positive_integral_cmult_indicator) (auto simp: measurable_sets)
2150   also have "\<dots> \<le> integral\<^isup>P M (\<lambda>x. max 0 (f x))"
2151     by (auto intro!: positive_integral_mono simp: indicator_def max_def)
2152   finally have "\<infinity> * \<mu> (f -` {\<infinity>} \<inter> space M) \<le> integral\<^isup>P M f"
2153     by (simp add: positive_integral_max_0)
2154   moreover have "0 \<le> \<mu> (f -` {\<infinity>} \<inter> space M)"
2155     using f by (simp add: measurable_sets)
2156   ultimately show ?thesis
2157     using assms by (auto split: split_if_asm)
2158 qed
2160 lemma (in measure_space) positive_integral_PInf_AE:
2161   assumes "f \<in> borel_measurable M" "integral\<^isup>P M f \<noteq> \<infinity>" shows "AE x. f x \<noteq> \<infinity>"
2162 proof (rule AE_I)
2163   show "\<mu> (f -` {\<infinity>} \<inter> space M) = 0"
2164     by (rule positive_integral_PInf[OF assms])
2165   show "f -` {\<infinity>} \<inter> space M \<in> sets M"
2166     using assms by (auto intro: borel_measurable_vimage)
2167 qed auto
2169 lemma (in measure_space) simple_integral_PInf:
2170   assumes "simple_function M f" "\<And>x. 0 \<le> f x"
2171   and "integral\<^isup>S M f \<noteq> \<infinity>"
2172   shows "\<mu> (f -` {\<infinity>} \<inter> space M) = 0"
2173 proof (rule positive_integral_PInf)
2174   show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function)
2175   show "integral\<^isup>P M f \<noteq> \<infinity>"
2176     using assms by (simp add: positive_integral_eq_simple_integral)
2177 qed
2179 lemma (in measure_space) integral_real:
2180   "AE x. \<bar>f x\<bar> \<noteq> \<infinity> \<Longrightarrow> (\<integral>x. real (f x) \<partial>M) = real (integral\<^isup>P M f) - real (integral\<^isup>P M (\<lambda>x. - f x))"
2181   using assms unfolding lebesgue_integral_def
2182   by (subst (1 2) positive_integral_cong_AE) (auto simp add: extreal_real)
2184 lemma liminf_extreal_cminus:
2185   fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
2186   shows "liminf (\<lambda>x. c - f x) = c - limsup f"
2187 proof (cases c)
2188   case PInf then show ?thesis by (simp add: Liminf_const)
2189 next
2190   case (real r) then show ?thesis
2191     unfolding liminf_SUPR_INFI limsup_INFI_SUPR
2192     apply (subst INFI_extreal_cminus)
2193     apply auto
2194     apply (subst SUPR_extreal_cminus)
2195     apply auto
2196     done
2197 qed (insert `c \<noteq> -\<infinity>`, simp)
2199 lemma (in measure_space) integral_dominated_convergence:
2200   assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
2201   and w: "integrable M w"
2202   and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
2203   shows "integrable M u'"
2204   and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
2205   and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim)
2206 proof -
2207   { fix x j assume x: "x \<in> space M"
2208     from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs)
2209     from LIMSEQ_le_const2[OF this]
2210     have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto }
2211   note u'_bound = this
2213   from u[unfolded integrable_def]
2214   have u'_borel: "u' \<in> borel_measurable M"
2215     using u' by (blast intro: borel_measurable_LIMSEQ[of u])
2217   { fix x assume x: "x \<in> space M"
2218     then have "0 \<le> \<bar>u 0 x\<bar>" by auto
2219     also have "\<dots> \<le> w x" using bound[OF x] by auto
2220     finally have "0 \<le> w x" . }
2221   note w_pos = this
2223   show "integrable M u'"
2224   proof (rule integrable_bound)
2225     show "integrable M w" by fact
2226     show "u' \<in> borel_measurable M" by fact
2227   next
2228     fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact
2229     show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
2230   qed
2232   let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>"
2233   have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)"
2234     using w u `integrable M u'`
2235     by (auto intro!: integral_add integral_diff integral_cmult integrable_abs)
2237   { fix j x assume x: "x \<in> space M"
2238     have "\<bar>u j x - u' x\<bar> \<le> \<bar>u j x\<bar> + \<bar>u' x\<bar>" by auto
2239     also have "\<dots> \<le> w x + w x"
2240       by (rule add_mono[OF bound[OF x] u'_bound[OF x]])
2241     finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp }
2242   note diff_less_2w = this
2244   have PI_diff: "\<And>n. (\<integral>\<^isup>+ x. extreal (?diff n x) \<partial>M) =
2245     (\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"
2246     using diff w diff_less_2w w_pos
2247     by (subst positive_integral_diff[symmetric])
2248        (auto simp: integrable_def intro!: positive_integral_cong)
2250   have "integrable M (\<lambda>x. 2 * w x)"
2251     using w by (auto intro: integral_cmult)
2252   hence I2w_fin: "(\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M) \<noteq> \<infinity>" and
2253     borel_2w: "(\<lambda>x. extreal (2 * w x)) \<in> borel_measurable M"
2254     unfolding integrable_def by auto
2256   have "limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M) = 0" (is "limsup ?f = 0")
2257   proof cases
2258     assume eq_0: "(\<integral>\<^isup>+ x. max 0 (extreal (2 * w x)) \<partial>M) = 0" (is "?wx = 0")
2259     { fix n
2260       have "?f n \<le> ?wx" (is "integral\<^isup>P M ?f' \<le> _")
2261         using diff_less_2w[of _ n] unfolding positive_integral_max_0
2262         by (intro positive_integral_mono) auto
2263       then have "?f n = 0"
2264         using positive_integral_positive[of ?f'] eq_0 by auto }
2265     then show ?thesis by (simp add: Limsup_const)
2266   next
2267     assume neq_0: "(\<integral>\<^isup>+ x. max 0 (extreal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
2268     have "0 = limsup (\<lambda>n. 0 :: extreal)" by (simp add: Limsup_const)
2269     also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"
2270       by (intro limsup_mono positive_integral_positive)
2271     finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)" .
2272     have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (extreal (?diff n x))) \<partial>M)"
2273     proof (rule positive_integral_cong)
2274       fix x assume x: "x \<in> space M"
2275       show "max 0 (extreal (2 * w x)) = liminf (\<lambda>n. max 0 (extreal (?diff n x)))"
2276         unfolding extreal_max_0
2277       proof (rule lim_imp_Liminf[symmetric], unfold lim_extreal)
2278         have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>"
2279           using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs)
2280         then show "(\<lambda>i. max 0 (?diff i x)) ----> max 0 (2 * w x)"
2281           by (auto intro!: tendsto_real_max simp add: lim_extreal)
2282       qed (rule trivial_limit_sequentially)
2283     qed
2284     also have "\<dots> \<le> liminf (\<lambda>n. \<integral>\<^isup>+ x. max 0 (extreal (?diff n x)) \<partial>M)"
2285       using u'_borel w u unfolding integrable_def
2286       by (intro positive_integral_lim_INF) (auto intro!: positive_integral_lim_INF)
2287     also have "\<dots> = (\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M) -
2288         limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"
2289       unfolding PI_diff positive_integral_max_0
2290       using positive_integral_positive[of "\<lambda>x. extreal (2 * w x)"]
2291       by (subst liminf_extreal_cminus) auto
2292     finally show ?thesis
2293       using neq_0 I2w_fin positive_integral_positive[of "\<lambda>x. extreal (2 * w x)"] pos
2294       unfolding positive_integral_max_0
2295       by (cases rule: extreal2_cases[of "\<integral>\<^isup>+ x. extreal (2 * w x) \<partial>M" "limsup (\<lambda>n. \<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M)"])
2296          auto
2297   qed
2299   have "liminf ?f \<le> limsup ?f"
2300     by (intro extreal_Liminf_le_Limsup trivial_limit_sequentially)
2301   moreover
2302   { have "0 = liminf (\<lambda>n. 0 :: extreal)" by (simp add: Liminf_const)
2303     also have "\<dots> \<le> liminf ?f"
2304       by (intro liminf_mono positive_integral_positive)
2305     finally have "0 \<le> liminf ?f" . }
2306   ultimately have liminf_limsup_eq: "liminf ?f = extreal 0" "limsup ?f = extreal 0"
2307     using `limsup ?f = 0` by auto
2308   have "\<And>n. (\<integral>\<^isup>+ x. extreal \<bar>u n x - u' x\<bar> \<partial>M) = extreal (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)"
2309     using diff positive_integral_positive
2310     by (subst integral_eq_positive_integral) (auto simp: extreal_real integrable_def)
2311   then show ?lim_diff
2312     using extreal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
2313     by (simp add: lim_extreal)
2315   show ?lim
2316   proof (rule LIMSEQ_I)
2317     fix r :: real assume "0 < r"
2318     from LIMSEQ_D[OF `?lim_diff` this]
2319     obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M) < r"
2320       using diff by (auto simp: integral_positive)
2322     show "\<exists>N. \<forall>n\<ge>N. norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r"
2323     proof (safe intro!: exI[of _ N])
2324       fix n assume "N \<le> n"
2325       have "\<bar>integral\<^isup>L M (u n) - integral\<^isup>L M u'\<bar> = \<bar>(\<integral>x. u n x - u' x \<partial>M)\<bar>"
2326         using u `integrable M u'` by (auto simp: integral_diff)
2327       also have "\<dots> \<le> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)" using u `integrable M u'`
2328         by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff)
2329       also note N[OF `N \<le> n`]
2330       finally show "norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r" by simp
2331     qed
2332   qed
2333 qed
2335 lemma (in measure_space) integral_sums:
2336   assumes borel: "\<And>i. integrable M (f i)"
2337   and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
2338   and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
2339   shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
2340   and "(\<lambda>i. integral\<^isup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is ?integral)
2341 proof -
2342   have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
2343     using summable unfolding summable_def by auto
2344   from bchoice[OF this]
2345   obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
2347   let "?w y" = "if y \<in> space M then w y else 0"
2349   obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
2350     using sums unfolding summable_def ..
2352   have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)"
2353     using borel by (auto intro!: integral_setsum)
2355   { fix j x assume [simp]: "x \<in> space M"
2356     have "\<bar>\<Sum>i = 0..< j. f i x\<bar> \<le> (\<Sum>i = 0..< j. \<bar>f i x\<bar>)" by (rule setsum_abs)
2357     also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
2358     finally have "\<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x" by simp }
2359   note 2 = this
2361   have 3: "integrable M ?w"
2362   proof (rule integral_monotone_convergence(1))
2363     let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
2364     let "?w' n y" = "if y \<in> space M then ?F n y else 0"
2365     have "\<And>n. integrable M (?F n)"
2366       using borel by (auto intro!: integral_setsum integrable_abs)
2367     thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
2368     show "mono ?w'"
2369       by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
2370     { fix x show "(\<lambda>n. ?w' n x) ----> ?w x"
2371         using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) }
2372     have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
2373       using borel by (simp add: integral_setsum integrable_abs cong: integral_cong)
2374     from abs_sum
2375     show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
2376   qed
2378   from summable[THEN summable_rabs_cancel]
2379   have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
2380     by (auto intro: summable_sumr_LIMSEQ_suminf)
2382   note int = integral_dominated_convergence(1,3)[OF 1 2 3 4]
2384   from int show "integrable M ?S" by simp
2386   show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel]
2387     using int(2) by simp
2388 qed
2390 section "Lebesgue integration on countable spaces"
2392 lemma (in measure_space) integral_on_countable:
2393   assumes f: "f \<in> borel_measurable M"
2394   and bij: "bij_betw enum S (f ` space M)"
2395   and enum_zero: "enum ` (-S) \<subseteq> {0}"
2396   and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<infinity>"
2397   and abs_summable: "summable (\<lambda>r. \<bar>enum r * real (\<mu> (f -` {enum r} \<inter> space M))\<bar>)"
2398   shows "integrable M f"
2399   and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral\<^isup>L M f" (is ?sums)
2400 proof -
2401   let "?A r" = "f -` {enum r} \<inter> space M"
2402   let "?F r x" = "enum r * indicator (?A r) x"
2403   have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral\<^isup>L M (?F r)"
2404     using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
2406   { fix x assume "x \<in> space M"
2407     hence "f x \<in> enum ` S" using bij unfolding bij_betw_def by auto
2408     then obtain i where "i\<in>S" "enum i = f x" by auto
2409     have F: "\<And>j. ?F j x = (if j = i then f x else 0)"
2410     proof cases
2411       fix j assume "j = i"
2412       thus "?thesis j" using `x \<in> space M` `enum i = f x` by (simp add: indicator_def)
2413     next
2414       fix j assume "j \<noteq> i"
2415       show "?thesis j" using bij `i \<in> S` `j \<noteq> i` `enum i = f x` enum_zero
2416         by (cases "j \<in> S") (auto simp add: indicator_def bij_betw_def inj_on_def)
2417     qed
2418     hence F_abs: "\<And>j. \<bar>if j = i then f x else 0\<bar> = (if j = i then \<bar>f x\<bar> else 0)" by auto
2419     have "(\<lambda>i. ?F i x) sums f x"
2420          "(\<lambda>i. \<bar>?F i x\<bar>) sums \<bar>f x\<bar>"
2421       by (auto intro!: sums_single simp: F F_abs) }
2422   note F_sums_f = this(1) and F_abs_sums_f = this(2)
2424   have int_f: "integral\<^isup>L M f = (\<integral>x. (\<Sum>r. ?F r x) \<partial>M)" "integrable M f = integrable M (\<lambda>x. \<Sum>r. ?F r x)"
2425     using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff)
2427   { fix r
2428     have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x \<partial>M)"
2429       by (auto simp: indicator_def intro!: integral_cong)
2430     also have "\<dots> = \<bar>enum r\<bar> * real (\<mu> (?A r))"
2431       using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
2432     finally have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = \<bar>enum r * real (\<mu> (?A r))\<bar>"
2433       using f by (subst (2) abs_mult_pos[symmetric]) (auto intro!: real_of_extreal_pos measurable_sets) }
2434   note int_abs_F = this
2436   have 1: "\<And>i. integrable M (\<lambda>x. ?F i x)"
2437     using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator)
2439   have 2: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>?F i x\<bar>)"
2440     using F_abs_sums_f unfolding sums_iff by auto
2442   from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
2443   show ?sums unfolding enum_eq int_f by simp
2445   from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
2446   show "integrable M f" unfolding int_f by simp
2447 qed
2449 section "Lebesgue integration on finite space"
2451 lemma (in measure_space) integral_on_finite:
2452   assumes f: "f \<in> borel_measurable M" and finite: "finite (f`space M)"
2453   and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<infinity>"
2454   shows "integrable M f"
2455   and "(\<integral>x. f x \<partial>M) =
2456     (\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral")
2457 proof -
2458   let "?A r" = "f -` {r} \<inter> space M"
2459   let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x"
2461   { fix x assume "x \<in> space M"
2462     have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)"
2463       using finite `x \<in> space M` by (simp add: setsum_cases)
2464     also have "\<dots> = ?S x"
2465       by (auto intro!: setsum_cong)
2466     finally have "f x = ?S x" . }
2467   note f_eq = this
2469   have f_eq_S: "integrable M f \<longleftrightarrow> integrable M ?S" "integral\<^isup>L M f = integral\<^isup>L M ?S"
2470     by (auto intro!: integrable_cong integral_cong simp only: f_eq)
2472   show "integrable M f" ?integral using fin f f_eq_S
2473     by (simp_all add: integral_cmul_indicator borel_measurable_vimage)
2474 qed
2476 lemma (in finite_measure_space) simple_function_finite[simp, intro]: "simple_function M f"
2477   unfolding simple_function_def using finite_space by auto
2479 lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
2480   by (auto intro: borel_measurable_simple_function)
2482 lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
2483   assumes pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
2484   shows "integral\<^isup>P M f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
2485 proof -
2486   have *: "integral\<^isup>P M f = (\<integral>\<^isup>+ x. (\<Sum>y\<in>space M. f y * indicator {y} x) \<partial>M)"
2487     by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
2488   show ?thesis unfolding * using borel_measurable_finite[of f] pos
2489     by (simp add: positive_integral_setsum positive_integral_cmult_indicator)
2490 qed
2492 lemma (in finite_measure_space) integral_finite_singleton:
2493   shows "integrable M f"
2494   and "integral\<^isup>L M f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I)
2495 proof -
2496   have *:
2497     "(\<integral>\<^isup>+ x. max 0 (extreal (f x)) \<partial>M) = (\<Sum>x \<in> space M. max 0 (extreal (f x)) * \<mu> {x})"
2498     "(\<integral>\<^isup>+ x. max 0 (extreal (- f x)) \<partial>M) = (\<Sum>x \<in> space M. max 0 (extreal (- f x)) * \<mu> {x})"
2499     by (simp_all add: positive_integral_finite_eq_setsum)
2500   then show "integrable M f" using finite_space finite_measure
2501     by (simp add: setsum_Pinfty integrable_def positive_integral_max_0
2502              split: split_max)
2503   show ?I using finite_measure *
2504     apply (simp add: positive_integral_max_0 lebesgue_integral_def)
2505     apply (subst (1 2) setsum_real_of_extreal[symmetric])
2506     apply (simp_all split: split_max add: setsum_subtractf[symmetric])
2507     apply (intro setsum_cong[OF refl])
2508     apply (simp split: split_max)
2509     done
2510 qed
2512 end