1 (* Title: HOL/Probability/Set_Integral.thy |
|
2 Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) |
|
3 |
|
4 Notation and useful facts for working with integrals over a set. |
|
5 |
|
6 TODO: keep all these? Need unicode translations as well. |
|
7 *) |
|
8 |
|
9 theory Set_Integral |
|
10 imports Bochner_Integration Lebesgue_Measure |
|
11 begin |
|
12 |
|
13 (* |
|
14 Notation |
|
15 *) |
|
16 |
|
17 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M" |
|
18 |
|
19 abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)" |
|
20 |
|
21 abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)" |
|
22 |
|
23 syntax |
|
24 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
|
25 ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60) |
|
26 |
|
27 translations |
|
28 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)" |
|
29 |
|
30 abbreviation |
|
31 "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x" |
|
32 |
|
33 syntax |
|
34 "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" |
|
35 ("AE _\<in>_ in _./ _" [0,0,0,10] 10) |
|
36 |
|
37 translations |
|
38 "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)" |
|
39 |
|
40 (* |
|
41 Notation for integration wrt lebesgue measure on the reals: |
|
42 |
|
43 LBINT x. f |
|
44 LBINT x : A. f |
|
45 |
|
46 TODO: keep all these? Need unicode. |
|
47 *) |
|
48 |
|
49 syntax |
|
50 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real" |
|
51 ("(2LBINT _./ _)" [0,60] 60) |
|
52 |
|
53 translations |
|
54 "LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)" |
|
55 |
|
56 syntax |
|
57 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real" |
|
58 ("(3LBINT _:_./ _)" [0,60,61] 60) |
|
59 |
|
60 translations |
|
61 "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)" |
|
62 |
|
63 (* |
|
64 Basic properties |
|
65 *) |
|
66 |
|
67 (* |
|
68 lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)" |
|
69 by (auto simp add: indicator_def) |
|
70 *) |
|
71 |
|
72 lemma set_borel_measurable_sets: |
|
73 fixes f :: "_ \<Rightarrow> _::real_normed_vector" |
|
74 assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M" |
|
75 shows "f -` B \<inter> X \<in> sets M" |
|
76 proof - |
|
77 have "f \<in> borel_measurable (restrict_space M X)" |
|
78 using assms by (subst borel_measurable_restrict_space_iff) auto |
|
79 then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)" |
|
80 by (rule measurable_sets) fact |
|
81 with \<open>X \<in> sets M\<close> show ?thesis |
|
82 by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space) |
|
83 qed |
|
84 |
|
85 lemma set_lebesgue_integral_cong: |
|
86 assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x" |
|
87 shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)" |
|
88 using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space) |
|
89 |
|
90 lemma set_lebesgue_integral_cong_AE: |
|
91 assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
|
92 assumes "AE x \<in> A in M. f x = g x" |
|
93 shows "LINT x:A|M. f x = LINT x:A|M. g x" |
|
94 proof- |
|
95 have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x" |
|
96 using assms by auto |
|
97 thus ?thesis by (intro integral_cong_AE) auto |
|
98 qed |
|
99 |
|
100 lemma set_integrable_cong_AE: |
|
101 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> |
|
102 AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow> |
|
103 set_integrable M A f = set_integrable M A g" |
|
104 by (rule integrable_cong_AE) auto |
|
105 |
|
106 lemma set_integrable_subset: |
|
107 fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
108 assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A" |
|
109 shows "set_integrable M B f" |
|
110 proof - |
|
111 have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)" |
|
112 by (rule integrable_mult_indicator) fact+ |
|
113 with \<open>B \<subseteq> A\<close> show ?thesis |
|
114 by (simp add: indicator_inter_arith[symmetric] Int_absorb2) |
|
115 qed |
|
116 |
|
117 (* TODO: integral_cmul_indicator should be named set_integral_const *) |
|
118 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *) |
|
119 |
|
120 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)" |
|
121 by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong) |
|
122 |
|
123 lemma set_integral_mult_right [simp]: |
|
124 fixes a :: "'a::{real_normed_field, second_countable_topology}" |
|
125 shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)" |
|
126 by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong) |
|
127 |
|
128 lemma set_integral_mult_left [simp]: |
|
129 fixes a :: "'a::{real_normed_field, second_countable_topology}" |
|
130 shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a" |
|
131 by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong) |
|
132 |
|
133 lemma set_integral_divide_zero [simp]: |
|
134 fixes a :: "'a::{real_normed_field, field, second_countable_topology}" |
|
135 shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a" |
|
136 by (subst integral_divide_zero[symmetric], intro integral_cong) |
|
137 (auto split: split_indicator) |
|
138 |
|
139 lemma set_integrable_scaleR_right [simp, intro]: |
|
140 shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)" |
|
141 unfolding scaleR_left_commute by (rule integrable_scaleR_right) |
|
142 |
|
143 lemma set_integrable_scaleR_left [simp, intro]: |
|
144 fixes a :: "_ :: {banach, second_countable_topology}" |
|
145 shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)" |
|
146 using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp |
|
147 |
|
148 lemma set_integrable_mult_right [simp, intro]: |
|
149 fixes a :: "'a::{real_normed_field, second_countable_topology}" |
|
150 shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)" |
|
151 using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp |
|
152 |
|
153 lemma set_integrable_mult_left [simp, intro]: |
|
154 fixes a :: "'a::{real_normed_field, second_countable_topology}" |
|
155 shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)" |
|
156 using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp |
|
157 |
|
158 lemma set_integrable_divide [simp, intro]: |
|
159 fixes a :: "'a::{real_normed_field, field, second_countable_topology}" |
|
160 assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f" |
|
161 shows "set_integrable M A (\<lambda>t. f t / a)" |
|
162 proof - |
|
163 have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)" |
|
164 using assms by (rule integrable_divide_zero) |
|
165 also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))" |
|
166 by (auto split: split_indicator) |
|
167 finally show ?thesis . |
|
168 qed |
|
169 |
|
170 lemma set_integral_add [simp, intro]: |
|
171 fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
172 assumes "set_integrable M A f" "set_integrable M A g" |
|
173 shows "set_integrable M A (\<lambda>x. f x + g x)" |
|
174 and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)" |
|
175 using assms by (simp_all add: scaleR_add_right) |
|
176 |
|
177 lemma set_integral_diff [simp, intro]: |
|
178 assumes "set_integrable M A f" "set_integrable M A g" |
|
179 shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x = |
|
180 (LINT x:A|M. f x) - (LINT x:A|M. g x)" |
|
181 using assms by (simp_all add: scaleR_diff_right) |
|
182 |
|
183 lemma set_integral_reflect: |
|
184 fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
185 shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))" |
|
186 by (subst lborel_integral_real_affine[where c="-1" and t=0]) |
|
187 (auto intro!: integral_cong split: split_indicator) |
|
188 |
|
189 (* question: why do we have this for negation, but multiplication by a constant |
|
190 requires an integrability assumption? *) |
|
191 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)" |
|
192 by (subst integral_minus[symmetric]) simp_all |
|
193 |
|
194 lemma set_integral_complex_of_real: |
|
195 "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)" |
|
196 by (subst integral_complex_of_real[symmetric]) |
|
197 (auto intro!: integral_cong split: split_indicator) |
|
198 |
|
199 lemma set_integral_mono: |
|
200 fixes f g :: "_ \<Rightarrow> real" |
|
201 assumes "set_integrable M A f" "set_integrable M A g" |
|
202 "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x" |
|
203 shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)" |
|
204 using assms by (auto intro: integral_mono split: split_indicator) |
|
205 |
|
206 lemma set_integral_mono_AE: |
|
207 fixes f g :: "_ \<Rightarrow> real" |
|
208 assumes "set_integrable M A f" "set_integrable M A g" |
|
209 "AE x \<in> A in M. f x \<le> g x" |
|
210 shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)" |
|
211 using assms by (auto intro: integral_mono_AE split: split_indicator) |
|
212 |
|
213 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)" |
|
214 using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps) |
|
215 |
|
216 lemma set_integrable_abs_iff: |
|
217 fixes f :: "_ \<Rightarrow> real" |
|
218 shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f" |
|
219 by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps) |
|
220 |
|
221 lemma set_integrable_abs_iff': |
|
222 fixes f :: "_ \<Rightarrow> real" |
|
223 shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow> |
|
224 set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f" |
|
225 by (intro set_integrable_abs_iff) auto |
|
226 |
|
227 lemma set_integrable_discrete_difference: |
|
228 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" |
|
229 assumes "countable X" |
|
230 assumes diff: "(A - B) \<union> (B - A) \<subseteq> X" |
|
231 assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" |
|
232 shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f" |
|
233 proof (rule integrable_discrete_difference[where X=X]) |
|
234 show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x" |
|
235 using diff by (auto split: split_indicator) |
|
236 qed fact+ |
|
237 |
|
238 lemma set_integral_discrete_difference: |
|
239 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" |
|
240 assumes "countable X" |
|
241 assumes diff: "(A - B) \<union> (B - A) \<subseteq> X" |
|
242 assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M" |
|
243 shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f" |
|
244 proof (rule integral_discrete_difference[where X=X]) |
|
245 show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x" |
|
246 using diff by (auto split: split_indicator) |
|
247 qed fact+ |
|
248 |
|
249 lemma set_integrable_Un: |
|
250 fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
251 assumes f_A: "set_integrable M A f" and f_B: "set_integrable M B f" |
|
252 and [measurable]: "A \<in> sets M" "B \<in> sets M" |
|
253 shows "set_integrable M (A \<union> B) f" |
|
254 proof - |
|
255 have "set_integrable M (A - B) f" |
|
256 using f_A by (rule set_integrable_subset) auto |
|
257 from integrable_add[OF this f_B] show ?thesis |
|
258 by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator) |
|
259 qed |
|
260 |
|
261 lemma set_integrable_UN: |
|
262 fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
263 assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f" |
|
264 "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M" |
|
265 shows "set_integrable M (\<Union>i\<in>I. A i) f" |
|
266 using assms by (induct I) (auto intro!: set_integrable_Un) |
|
267 |
|
268 lemma set_integral_Un: |
|
269 fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
270 assumes "A \<inter> B = {}" |
|
271 and "set_integrable M A f" |
|
272 and "set_integrable M B f" |
|
273 shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)" |
|
274 by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] |
|
275 scaleR_add_left assms) |
|
276 |
|
277 lemma set_integral_cong_set: |
|
278 fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
279 assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f" |
|
280 and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B" |
|
281 shows "LINT x:B|M. f x = LINT x:A|M. f x" |
|
282 proof (rule integral_cong_AE) |
|
283 show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x" |
|
284 using ae by (auto simp: subset_eq split: split_indicator) |
|
285 qed fact+ |
|
286 |
|
287 lemma set_borel_measurable_subset: |
|
288 fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
289 assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A" |
|
290 shows "set_borel_measurable M B f" |
|
291 proof - |
|
292 have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)" |
|
293 by measurable |
|
294 also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)" |
|
295 using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator) |
|
296 finally show ?thesis . |
|
297 qed |
|
298 |
|
299 lemma set_integral_Un_AE: |
|
300 fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
301 assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M" |
|
302 and "set_integrable M A f" |
|
303 and "set_integrable M B f" |
|
304 shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)" |
|
305 proof - |
|
306 have f: "set_integrable M (A \<union> B) f" |
|
307 by (intro set_integrable_Un assms) |
|
308 then have f': "set_borel_measurable M (A \<union> B) f" |
|
309 by (rule borel_measurable_integrable) |
|
310 have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x" |
|
311 proof (rule set_integral_cong_set) |
|
312 show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)" |
|
313 using ae by auto |
|
314 show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f" |
|
315 using f' by (rule set_borel_measurable_subset) auto |
|
316 qed fact |
|
317 also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)" |
|
318 by (auto intro!: set_integral_Un set_integrable_subset[OF f]) |
|
319 also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)" |
|
320 using ae |
|
321 by (intro arg_cong2[where f="op+"] set_integral_cong_set) |
|
322 (auto intro!: set_borel_measurable_subset[OF f']) |
|
323 finally show ?thesis . |
|
324 qed |
|
325 |
|
326 lemma set_integral_finite_Union: |
|
327 fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}" |
|
328 assumes "finite I" "disjoint_family_on A I" |
|
329 and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M" |
|
330 shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)" |
|
331 using assms |
|
332 apply induct |
|
333 apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def) |
|
334 by (subst set_integral_Un, auto intro: set_integrable_UN) |
|
335 |
|
336 (* TODO: find a better name? *) |
|
337 lemma pos_integrable_to_top: |
|
338 fixes l::real |
|
339 assumes "\<And>i. A i \<in> sets M" "mono A" |
|
340 assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x" |
|
341 and intgbl: "\<And>i::nat. set_integrable M (A i) f" |
|
342 and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l" |
|
343 shows "set_integrable M (\<Union>i. A i) f" |
|
344 apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l]) |
|
345 apply (rule intgbl) |
|
346 prefer 3 apply (rule lim) |
|
347 apply (rule AE_I2) |
|
348 using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) [] |
|
349 proof (rule AE_I2) |
|
350 { fix x assume "x \<in> space M" |
|
351 show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x" |
|
352 proof cases |
|
353 assume "\<exists>i. x \<in> A i" |
|
354 then guess i .. |
|
355 then have *: "eventually (\<lambda>i. x \<in> A i) sequentially" |
|
356 using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def) |
|
357 show ?thesis |
|
358 apply (intro Lim_eventually) |
|
359 using * |
|
360 apply eventually_elim |
|
361 apply (auto split: split_indicator) |
|
362 done |
|
363 qed auto } |
|
364 then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M" |
|
365 apply (rule borel_measurable_LIMSEQ_real) |
|
366 apply assumption |
|
367 apply (intro borel_measurable_integrable intgbl) |
|
368 done |
|
369 qed |
|
370 |
|
371 (* Proof from Royden Real Analysis, p. 91. *) |
|
372 lemma lebesgue_integral_countable_add: |
|
373 fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
374 assumes meas[intro]: "\<And>i::nat. A i \<in> sets M" |
|
375 and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}" |
|
376 and intgbl: "set_integrable M (\<Union>i. A i) f" |
|
377 shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))" |
|
378 proof (subst integral_suminf[symmetric]) |
|
379 show int_A: "\<And>i. set_integrable M (A i) f" |
|
380 using intgbl by (rule set_integrable_subset) auto |
|
381 { fix x assume "x \<in> space M" |
|
382 have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)" |
|
383 by (intro sums_scaleR_left indicator_sums) fact } |
|
384 note sums = this |
|
385 |
|
386 have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))" |
|
387 using int_A[THEN integrable_norm] by auto |
|
388 |
|
389 show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))" |
|
390 using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums]) |
|
391 |
|
392 show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))" |
|
393 proof (rule summableI_nonneg_bounded) |
|
394 fix n |
|
395 show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)" |
|
396 using norm_f by (auto intro!: integral_nonneg_AE) |
|
397 |
|
398 have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) = |
|
399 (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))" |
|
400 by (simp add: abs_mult) |
|
401 also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))" |
|
402 using norm_f |
|
403 by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj) |
|
404 also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))" |
|
405 using intgbl[THEN integrable_norm] |
|
406 by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f) |
|
407 (auto split: split_indicator) |
|
408 finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le> |
|
409 set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))" |
|
410 by simp |
|
411 qed |
|
412 show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)" |
|
413 apply (rule integral_cong[OF refl]) |
|
414 apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric]) |
|
415 using sums_unique[OF indicator_sums[OF disj]] |
|
416 apply auto |
|
417 done |
|
418 qed |
|
419 |
|
420 lemma set_integral_cont_up: |
|
421 fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
422 assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A" |
|
423 and intgbl: "set_integrable M (\<Union>i. A i) f" |
|
424 shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x" |
|
425 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"]) |
|
426 have int_A: "\<And>i. set_integrable M (A i) f" |
|
427 using intgbl by (rule set_integrable_subset) auto |
|
428 then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f" |
|
429 "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))" |
|
430 using intgbl integrable_norm[OF intgbl] by auto |
|
431 |
|
432 { fix x i assume "x \<in> A i" |
|
433 with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1" |
|
434 by (intro filterlim_cong refl) |
|
435 (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) } |
|
436 then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x" |
|
437 by (intro AE_I2 tendsto_intros) (auto split: split_indicator) |
|
438 qed (auto split: split_indicator) |
|
439 |
|
440 (* Can the int0 hypothesis be dropped? *) |
|
441 lemma set_integral_cont_down: |
|
442 fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
443 assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A" |
|
444 and int0: "set_integrable M (A 0) f" |
|
445 shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x" |
|
446 proof (rule integral_dominated_convergence) |
|
447 have int_A: "\<And>i. set_integrable M (A i) f" |
|
448 using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def) |
|
449 show "set_integrable M (A 0) (\<lambda>x. norm (f x))" |
|
450 using int0[THEN integrable_norm] by simp |
|
451 have "set_integrable M (\<Inter>i. A i) f" |
|
452 using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def) |
|
453 with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f" |
|
454 by auto |
|
455 show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)" |
|
456 using A by (auto split: split_indicator simp: decseq_def) |
|
457 { fix x i assume "x \<in> space M" "x \<notin> A i" |
|
458 with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0" |
|
459 by (intro filterlim_cong refl) |
|
460 (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) } |
|
461 then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x *\<^sub>R f x" |
|
462 by (intro AE_I2 tendsto_intros) (auto split: split_indicator) |
|
463 qed |
|
464 |
|
465 lemma set_integral_at_point: |
|
466 fixes a :: real |
|
467 assumes "set_integrable M {a} f" |
|
468 and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>" |
|
469 shows "(LINT x:{a} | M. f x) = f a * measure M {a}" |
|
470 proof- |
|
471 have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)" |
|
472 by (intro set_lebesgue_integral_cong) simp_all |
|
473 then show ?thesis using assms by simp |
|
474 qed |
|
475 |
|
476 |
|
477 abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where |
|
478 "complex_integrable M f \<equiv> integrable M f" |
|
479 |
|
480 abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where |
|
481 "integral\<^sup>C M f == integral\<^sup>L M f" |
|
482 |
|
483 syntax |
|
484 "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex" |
|
485 ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110) |
|
486 |
|
487 translations |
|
488 "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)" |
|
489 |
|
490 syntax |
|
491 "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
|
492 ("(3CLINT _|_. _)" [0,110,60] 60) |
|
493 |
|
494 translations |
|
495 "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)" |
|
496 |
|
497 lemma complex_integrable_cnj [simp]: |
|
498 "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f" |
|
499 proof |
|
500 assume "complex_integrable M (\<lambda>x. cnj (f x))" |
|
501 then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))" |
|
502 by (rule integrable_cnj) |
|
503 then show "complex_integrable M f" |
|
504 by simp |
|
505 qed simp |
|
506 |
|
507 lemma complex_of_real_integrable_eq: |
|
508 "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f" |
|
509 proof |
|
510 assume "complex_integrable M (\<lambda>x. complex_of_real (f x))" |
|
511 then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))" |
|
512 by (rule integrable_Re) |
|
513 then show "integrable M f" |
|
514 by simp |
|
515 qed simp |
|
516 |
|
517 |
|
518 abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where |
|
519 "complex_set_integrable M A f \<equiv> set_integrable M A f" |
|
520 |
|
521 abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where |
|
522 "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f" |
|
523 |
|
524 syntax |
|
525 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" |
|
526 ("(4CLINT _:_|_. _)" [0,60,110,61] 60) |
|
527 |
|
528 translations |
|
529 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)" |
|
530 |
|
531 (* |
|
532 lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x" |
|
533 apply (simp add: norm_mult) |
|
534 by (subst norm_mult, auto) |
|
535 *) |
|
536 |
|
537 lemma borel_integrable_atLeastAtMost': |
|
538 fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" |
|
539 assumes f: "continuous_on {a..b} f" |
|
540 shows "set_integrable lborel {a..b} f" (is "integrable _ ?f") |
|
541 by (intro borel_integrable_compact compact_Icc f) |
|
542 |
|
543 lemma integral_FTC_atLeastAtMost: |
|
544 fixes f :: "real \<Rightarrow> 'a :: euclidean_space" |
|
545 assumes "a \<le> b" |
|
546 and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})" |
|
547 and f: "continuous_on {a .. b} f" |
|
548 shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a" |
|
549 proof - |
|
550 let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x" |
|
551 have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV" |
|
552 using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel) |
|
553 moreover |
|
554 have "(f has_integral F b - F a) {a .. b}" |
|
555 by (intro fundamental_theorem_of_calculus ballI assms) auto |
|
556 then have "(?f has_integral F b - F a) {a .. b}" |
|
557 by (subst has_integral_cong[where g=f]) auto |
|
558 then have "(?f has_integral F b - F a) UNIV" |
|
559 by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto |
|
560 ultimately show "integral\<^sup>L lborel ?f = F b - F a" |
|
561 by (rule has_integral_unique) |
|
562 qed |
|
563 |
|
564 lemma set_borel_integral_eq_integral: |
|
565 fixes f :: "real \<Rightarrow> 'a::euclidean_space" |
|
566 assumes "set_integrable lborel S f" |
|
567 shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f" |
|
568 proof - |
|
569 let ?f = "\<lambda>x. indicator S x *\<^sub>R f x" |
|
570 have "(?f has_integral LINT x : S | lborel. f x) UNIV" |
|
571 by (rule has_integral_integral_lborel) fact |
|
572 hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S" |
|
573 apply (subst has_integral_restrict_univ [symmetric]) |
|
574 apply (rule has_integral_eq) |
|
575 by auto |
|
576 thus "f integrable_on S" |
|
577 by (auto simp add: integrable_on_def) |
|
578 with 1 have "(f has_integral (integral S f)) S" |
|
579 by (intro integrable_integral, auto simp add: integrable_on_def) |
|
580 thus "LINT x : S | lborel. f x = integral S f" |
|
581 by (intro has_integral_unique [OF 1]) |
|
582 qed |
|
583 |
|
584 lemma set_borel_measurable_continuous: |
|
585 fixes f :: "_ \<Rightarrow> _::real_normed_vector" |
|
586 assumes "S \<in> sets borel" "continuous_on S f" |
|
587 shows "set_borel_measurable borel S f" |
|
588 proof - |
|
589 have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel" |
|
590 by (intro assms borel_measurable_continuous_on_if continuous_on_const) |
|
591 also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)" |
|
592 by auto |
|
593 finally show ?thesis . |
|
594 qed |
|
595 |
|
596 lemma set_measurable_continuous_on_ivl: |
|
597 assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)" |
|
598 shows "set_borel_measurable borel {a..b} f" |
|
599 by (rule set_borel_measurable_continuous[OF _ assms]) simp |
|
600 |
|
601 end |
|
602 |
|