|
1 (* Title: HOL/Analysis/Lebesgue_Measure.thy |
|
2 Author: Johannes Hölzl, TU München |
|
3 Author: Robert Himmelmann, TU München |
|
4 Author: Jeremy Avigad |
|
5 Author: Luke Serafin |
|
6 *) |
|
7 |
|
8 section \<open>Lebesgue measure\<close> |
|
9 |
|
10 theory Lebesgue_Measure |
|
11 imports Finite_Product_Measure Bochner_Integration Caratheodory |
|
12 begin |
|
13 |
|
14 subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close> |
|
15 |
|
16 definition interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where |
|
17 "interval_measure F = extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a <.. b}) (\<lambda>(a, b). ennreal (F b - F a))" |
|
18 |
|
19 lemma emeasure_interval_measure_Ioc: |
|
20 assumes "a \<le> b" |
|
21 assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
|
22 assumes right_cont_F : "\<And>a. continuous (at_right a) F" |
|
23 shows "emeasure (interval_measure F) {a <.. b} = F b - F a" |
|
24 proof (rule extend_measure_caratheodory_pair[OF interval_measure_def \<open>a \<le> b\<close>]) |
|
25 show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \<le> b}" |
|
26 proof (unfold_locales, safe) |
|
27 fix a b c d :: real assume *: "a \<le> b" "c \<le> d" |
|
28 then show "\<exists>C\<subseteq>{{a<..b} |a b. a \<le> b}. finite C \<and> disjoint C \<and> {a<..b} - {c<..d} = \<Union>C" |
|
29 proof cases |
|
30 let ?C = "{{a<..b}}" |
|
31 assume "b < c \<or> d \<le> a \<or> d \<le> c" |
|
32 with * have "?C \<subseteq> {{a<..b} |a b. a \<le> b} \<and> finite ?C \<and> disjoint ?C \<and> {a<..b} - {c<..d} = \<Union>?C" |
|
33 by (auto simp add: disjoint_def) |
|
34 thus ?thesis .. |
|
35 next |
|
36 let ?C = "{{a<..c}, {d<..b}}" |
|
37 assume "\<not> (b < c \<or> d \<le> a \<or> d \<le> c)" |
|
38 with * have "?C \<subseteq> {{a<..b} |a b. a \<le> b} \<and> finite ?C \<and> disjoint ?C \<and> {a<..b} - {c<..d} = \<Union>?C" |
|
39 by (auto simp add: disjoint_def Ioc_inj) (metis linear)+ |
|
40 thus ?thesis .. |
|
41 qed |
|
42 qed (auto simp: Ioc_inj, metis linear) |
|
43 next |
|
44 fix l r :: "nat \<Rightarrow> real" and a b :: real |
|
45 assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})" |
|
46 assume lr_eq_ab: "(\<Union>i. {l i<..r i}) = {a<..b}" |
|
47 |
|
48 have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> F a \<le> F b" |
|
49 by (auto intro!: l_r mono_F) |
|
50 |
|
51 { fix S :: "nat set" assume "finite S" |
|
52 moreover note \<open>a \<le> b\<close> |
|
53 moreover have "\<And>i. i \<in> S \<Longrightarrow> {l i <.. r i} \<subseteq> {a <.. b}" |
|
54 unfolding lr_eq_ab[symmetric] by auto |
|
55 ultimately have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<le> F b - F a" |
|
56 proof (induction S arbitrary: a rule: finite_psubset_induct) |
|
57 case (psubset S) |
|
58 show ?case |
|
59 proof cases |
|
60 assume "\<exists>i\<in>S. l i < r i" |
|
61 with \<open>finite S\<close> have "Min (l ` {i\<in>S. l i < r i}) \<in> l ` {i\<in>S. l i < r i}" |
|
62 by (intro Min_in) auto |
|
63 then obtain m where m: "m \<in> S" "l m < r m" "l m = Min (l ` {i\<in>S. l i < r i})" |
|
64 by fastforce |
|
65 |
|
66 have "(\<Sum>i\<in>S. F (r i) - F (l i)) = (F (r m) - F (l m)) + (\<Sum>i\<in>S - {m}. F (r i) - F (l i))" |
|
67 using m psubset by (intro setsum.remove) auto |
|
68 also have "(\<Sum>i\<in>S - {m}. F (r i) - F (l i)) \<le> F b - F (r m)" |
|
69 proof (intro psubset.IH) |
|
70 show "S - {m} \<subset> S" |
|
71 using \<open>m\<in>S\<close> by auto |
|
72 show "r m \<le> b" |
|
73 using psubset.prems(2)[OF \<open>m\<in>S\<close>] \<open>l m < r m\<close> by auto |
|
74 next |
|
75 fix i assume "i \<in> S - {m}" |
|
76 then have i: "i \<in> S" "i \<noteq> m" by auto |
|
77 { assume i': "l i < r i" "l i < r m" |
|
78 with \<open>finite S\<close> i m have "l m \<le> l i" |
|
79 by auto |
|
80 with i' have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}" |
|
81 by auto |
|
82 then have False |
|
83 using disjoint_family_onD[OF disj, of i m] i by auto } |
|
84 then have "l i \<noteq> r i \<Longrightarrow> r m \<le> l i" |
|
85 unfolding not_less[symmetric] using l_r[of i] by auto |
|
86 then show "{l i <.. r i} \<subseteq> {r m <.. b}" |
|
87 using psubset.prems(2)[OF \<open>i\<in>S\<close>] by auto |
|
88 qed |
|
89 also have "F (r m) - F (l m) \<le> F (r m) - F a" |
|
90 using psubset.prems(2)[OF \<open>m \<in> S\<close>] \<open>l m < r m\<close> |
|
91 by (auto simp add: Ioc_subset_iff intro!: mono_F) |
|
92 finally show ?case |
|
93 by (auto intro: add_mono) |
|
94 qed (auto simp add: \<open>a \<le> b\<close> less_le) |
|
95 qed } |
|
96 note claim1 = this |
|
97 |
|
98 (* second key induction: a lower bound on the measures of any finite collection of Ai's |
|
99 that cover an interval {u..v} *) |
|
100 |
|
101 { fix S u v and l r :: "nat \<Rightarrow> real" |
|
102 assume "finite S" "\<And>i. i\<in>S \<Longrightarrow> l i < r i" "{u..v} \<subseteq> (\<Union>i\<in>S. {l i<..< r i})" |
|
103 then have "F v - F u \<le> (\<Sum>i\<in>S. F (r i) - F (l i))" |
|
104 proof (induction arbitrary: v u rule: finite_psubset_induct) |
|
105 case (psubset S) |
|
106 show ?case |
|
107 proof cases |
|
108 assume "S = {}" then show ?case |
|
109 using psubset by (simp add: mono_F) |
|
110 next |
|
111 assume "S \<noteq> {}" |
|
112 then obtain j where "j \<in> S" |
|
113 by auto |
|
114 |
|
115 let ?R = "r j < u \<or> l j > v \<or> (\<exists>i\<in>S-{j}. l i \<le> l j \<and> r j \<le> r i)" |
|
116 show ?case |
|
117 proof cases |
|
118 assume "?R" |
|
119 with \<open>j \<in> S\<close> psubset.prems have "{u..v} \<subseteq> (\<Union>i\<in>S-{j}. {l i<..< r i})" |
|
120 apply (auto simp: subset_eq Ball_def) |
|
121 apply (metis Diff_iff less_le_trans leD linear singletonD) |
|
122 apply (metis Diff_iff less_le_trans leD linear singletonD) |
|
123 apply (metis order_trans less_le_not_le linear) |
|
124 done |
|
125 with \<open>j \<in> S\<close> have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))" |
|
126 by (intro psubset) auto |
|
127 also have "\<dots> \<le> (\<Sum>i\<in>S. F (r i) - F (l i))" |
|
128 using psubset.prems |
|
129 by (intro setsum_mono2 psubset) (auto intro: less_imp_le) |
|
130 finally show ?thesis . |
|
131 next |
|
132 assume "\<not> ?R" |
|
133 then have j: "u \<le> r j" "l j \<le> v" "\<And>i. i \<in> S - {j} \<Longrightarrow> r i < r j \<or> l i > l j" |
|
134 by (auto simp: not_less) |
|
135 let ?S1 = "{i \<in> S. l i < l j}" |
|
136 let ?S2 = "{i \<in> S. r i > r j}" |
|
137 |
|
138 have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<ge> (\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i))" |
|
139 using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j |
|
140 by (intro setsum_mono2) (auto intro: less_imp_le) |
|
141 also have "(\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i)) = |
|
142 (\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))" |
|
143 using psubset(1) psubset.prems(1) j |
|
144 apply (subst setsum.union_disjoint) |
|
145 apply simp_all |
|
146 apply (subst setsum.union_disjoint) |
|
147 apply auto |
|
148 apply (metis less_le_not_le) |
|
149 done |
|
150 also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u" |
|
151 using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j |
|
152 apply (intro psubset.IH psubset) |
|
153 apply (auto simp: subset_eq Ball_def) |
|
154 apply (metis less_le_trans not_le) |
|
155 done |
|
156 also (xtrans) have "(\<Sum>i\<in>?S2. F (r i) - F (l i)) \<ge> F v - F (r j)" |
|
157 using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j |
|
158 apply (intro psubset.IH psubset) |
|
159 apply (auto simp: subset_eq Ball_def) |
|
160 apply (metis le_less_trans not_le) |
|
161 done |
|
162 finally (xtrans) show ?case |
|
163 by (auto simp: add_mono) |
|
164 qed |
|
165 qed |
|
166 qed } |
|
167 note claim2 = this |
|
168 |
|
169 (* now prove the inequality going the other way *) |
|
170 have "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i)))" |
|
171 proof (rule ennreal_le_epsilon) |
|
172 fix epsilon :: real assume egt0: "epsilon > 0" |
|
173 have "\<forall>i. \<exists>d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)" |
|
174 proof |
|
175 fix i |
|
176 note right_cont_F [of "r i"] |
|
177 thus "\<exists>d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)" |
|
178 apply - |
|
179 apply (subst (asm) continuous_at_right_real_increasing) |
|
180 apply (rule mono_F, assumption) |
|
181 apply (drule_tac x = "epsilon / 2 ^ (i + 2)" in spec) |
|
182 apply (erule impE) |
|
183 using egt0 by (auto simp add: field_simps) |
|
184 qed |
|
185 then obtain delta where |
|
186 deltai_gt0: "\<And>i. delta i > 0" and |
|
187 deltai_prop: "\<And>i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)" |
|
188 by metis |
|
189 have "\<exists>a' > a. F a' - F a < epsilon / 2" |
|
190 apply (insert right_cont_F [of a]) |
|
191 apply (subst (asm) continuous_at_right_real_increasing) |
|
192 using mono_F apply force |
|
193 apply (drule_tac x = "epsilon / 2" in spec) |
|
194 using egt0 unfolding mult.commute [of 2] by force |
|
195 then obtain a' where a'lea [arith]: "a' > a" and |
|
196 a_prop: "F a' - F a < epsilon / 2" |
|
197 by auto |
|
198 define S' where "S' = {i. l i < r i}" |
|
199 obtain S :: "nat set" where |
|
200 "S \<subseteq> S'" and finS: "finite S" and |
|
201 Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})" |
|
202 proof (rule compactE_image) |
|
203 show "compact {a'..b}" |
|
204 by (rule compact_Icc) |
|
205 show "\<forall>i \<in> S'. open ({l i<..<r i + delta i})" by auto |
|
206 have "{a'..b} \<subseteq> {a <.. b}" |
|
207 by auto |
|
208 also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})" |
|
209 unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans) |
|
210 also have "\<dots> \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" |
|
211 apply (intro UN_mono) |
|
212 apply (auto simp: S'_def) |
|
213 apply (cut_tac i=i in deltai_gt0) |
|
214 apply simp |
|
215 done |
|
216 finally show "{a'..b} \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" . |
|
217 qed |
|
218 with S'_def have Sprop2: "\<And>i. i \<in> S \<Longrightarrow> l i < r i" by auto |
|
219 from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n" |
|
220 by (subst finite_nat_set_iff_bounded_le [symmetric]) |
|
221 then obtain n where Sbound [rule_format]: "\<forall>i \<in> S. i \<le> n" .. |
|
222 have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))" |
|
223 apply (rule claim2 [rule_format]) |
|
224 using finS Sprop apply auto |
|
225 apply (frule Sprop2) |
|
226 apply (subgoal_tac "delta i > 0") |
|
227 apply arith |
|
228 by (rule deltai_gt0) |
|
229 also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))" |
|
230 apply (rule setsum_mono) |
|
231 apply simp |
|
232 apply (rule order_trans) |
|
233 apply (rule less_imp_le) |
|
234 apply (rule deltai_prop) |
|
235 by auto |
|
236 also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) + |
|
237 (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _") |
|
238 by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib) |
|
239 also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)" |
|
240 apply (rule add_left_mono) |
|
241 apply (rule mult_left_mono) |
|
242 apply (rule setsum_mono2) |
|
243 using egt0 apply auto |
|
244 by (frule Sbound, auto) |
|
245 also have "... \<le> ?t + (epsilon / 2)" |
|
246 apply (rule add_left_mono) |
|
247 apply (subst geometric_sum) |
|
248 apply auto |
|
249 apply (rule mult_left_mono) |
|
250 using egt0 apply auto |
|
251 done |
|
252 finally have aux2: "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2" |
|
253 by simp |
|
254 |
|
255 have "F b - F a = (F b - F a') + (F a' - F a)" |
|
256 by auto |
|
257 also have "... \<le> (F b - F a') + epsilon / 2" |
|
258 using a_prop by (intro add_left_mono) simp |
|
259 also have "... \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2" |
|
260 apply (intro add_right_mono) |
|
261 apply (rule aux2) |
|
262 done |
|
263 also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon" |
|
264 by auto |
|
265 also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon" |
|
266 using finS Sbound Sprop by (auto intro!: add_right_mono setsum_mono3) |
|
267 finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon" |
|
268 using egt0 by (simp add: ennreal_plus[symmetric] setsum_nonneg del: ennreal_plus) |
|
269 then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)" |
|
270 by (rule order_trans) (auto intro!: add_mono setsum_le_suminf simp del: setsum_ennreal) |
|
271 qed |
|
272 moreover have "(\<Sum>i. ennreal (F (r i) - F (l i))) \<le> ennreal (F b - F a)" |
|
273 using \<open>a \<le> b\<close> by (auto intro!: suminf_le_const ennreal_le_iff[THEN iffD2] claim1) |
|
274 ultimately show "(\<Sum>n. ennreal (F (r n) - F (l n))) = ennreal (F b - F a)" |
|
275 by (rule antisym[rotated]) |
|
276 qed (auto simp: Ioc_inj mono_F) |
|
277 |
|
278 lemma measure_interval_measure_Ioc: |
|
279 assumes "a \<le> b" |
|
280 assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
|
281 assumes right_cont_F : "\<And>a. continuous (at_right a) F" |
|
282 shows "measure (interval_measure F) {a <.. b} = F b - F a" |
|
283 unfolding measure_def |
|
284 apply (subst emeasure_interval_measure_Ioc) |
|
285 apply fact+ |
|
286 apply (simp add: assms) |
|
287 done |
|
288 |
|
289 lemma emeasure_interval_measure_Ioc_eq: |
|
290 "(\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow> |
|
291 emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)" |
|
292 using emeasure_interval_measure_Ioc[of a b F] by auto |
|
293 |
|
294 lemma sets_interval_measure [simp, measurable_cong]: "sets (interval_measure F) = sets borel" |
|
295 apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc) |
|
296 apply (rule sigma_sets_eqI) |
|
297 apply auto |
|
298 apply (case_tac "a \<le> ba") |
|
299 apply (auto intro: sigma_sets.Empty) |
|
300 done |
|
301 |
|
302 lemma space_interval_measure [simp]: "space (interval_measure F) = UNIV" |
|
303 by (simp add: interval_measure_def space_extend_measure) |
|
304 |
|
305 lemma emeasure_interval_measure_Icc: |
|
306 assumes "a \<le> b" |
|
307 assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
|
308 assumes cont_F : "continuous_on UNIV F" |
|
309 shows "emeasure (interval_measure F) {a .. b} = F b - F a" |
|
310 proof (rule tendsto_unique) |
|
311 { fix a b :: real assume "a \<le> b" then have "emeasure (interval_measure F) {a <.. b} = F b - F a" |
|
312 using cont_F |
|
313 by (subst emeasure_interval_measure_Ioc) |
|
314 (auto intro: mono_F continuous_within_subset simp: continuous_on_eq_continuous_within) } |
|
315 note * = this |
|
316 |
|
317 let ?F = "interval_measure F" |
|
318 show "((\<lambda>a. F b - F a) \<longlongrightarrow> emeasure ?F {a..b}) (at_left a)" |
|
319 proof (rule tendsto_at_left_sequentially) |
|
320 show "a - 1 < a" by simp |
|
321 fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a" |
|
322 with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})" |
|
323 apply (intro Lim_emeasure_decseq) |
|
324 apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *) |
|
325 apply force |
|
326 apply (subst (asm ) *) |
|
327 apply (auto intro: less_le_trans less_imp_le) |
|
328 done |
|
329 also have "(\<Inter>n. {X n <..b}) = {a..b}" |
|
330 using \<open>\<And>n. X n < a\<close> |
|
331 apply auto |
|
332 apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>]) |
|
333 apply (auto intro: less_imp_le) |
|
334 apply (auto intro: less_le_trans) |
|
335 done |
|
336 also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))" |
|
337 using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans) |
|
338 finally show "(\<lambda>n. F b - F (X n)) \<longlonglongrightarrow> emeasure ?F {a..b}" . |
|
339 qed |
|
340 show "((\<lambda>a. ennreal (F b - F a)) \<longlongrightarrow> F b - F a) (at_left a)" |
|
341 by (rule continuous_on_tendsto_compose[where g="\<lambda>x. x" and s=UNIV]) |
|
342 (auto simp: continuous_on_ennreal continuous_on_diff cont_F continuous_on_const) |
|
343 qed (rule trivial_limit_at_left_real) |
|
344 |
|
345 lemma sigma_finite_interval_measure: |
|
346 assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" |
|
347 assumes right_cont_F : "\<And>a. continuous (at_right a) F" |
|
348 shows "sigma_finite_measure (interval_measure F)" |
|
349 apply unfold_locales |
|
350 apply (intro exI[of _ "(\<lambda>(a, b). {a <.. b}) ` (\<rat> \<times> \<rat>)"]) |
|
351 apply (auto intro!: Rats_no_top_le Rats_no_bot_less countable_rat simp: emeasure_interval_measure_Ioc_eq[OF assms]) |
|
352 done |
|
353 |
|
354 subsection \<open>Lebesgue-Borel measure\<close> |
|
355 |
|
356 definition lborel :: "('a :: euclidean_space) measure" where |
|
357 "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)" |
|
358 |
|
359 lemma |
|
360 shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel" |
|
361 and space_lborel[simp]: "space lborel = space borel" |
|
362 and measurable_lborel1[simp]: "measurable M lborel = measurable M borel" |
|
363 and measurable_lborel2[simp]: "measurable lborel M = measurable borel M" |
|
364 by (simp_all add: lborel_def) |
|
365 |
|
366 context |
|
367 begin |
|
368 |
|
369 interpretation sigma_finite_measure "interval_measure (\<lambda>x. x)" |
|
370 by (rule sigma_finite_interval_measure) auto |
|
371 interpretation finite_product_sigma_finite "\<lambda>_. interval_measure (\<lambda>x. x)" Basis |
|
372 proof qed simp |
|
373 |
|
374 lemma lborel_eq_real: "lborel = interval_measure (\<lambda>x. x)" |
|
375 unfolding lborel_def Basis_real_def |
|
376 using distr_id[of "interval_measure (\<lambda>x. x)"] |
|
377 by (subst distr_component[symmetric]) |
|
378 (simp_all add: distr_distr comp_def del: distr_id cong: distr_cong) |
|
379 |
|
380 lemma lborel_eq: "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. lborel) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)" |
|
381 by (subst lborel_def) (simp add: lborel_eq_real) |
|
382 |
|
383 lemma nn_integral_lborel_setprod: |
|
384 assumes [measurable]: "\<And>b. b \<in> Basis \<Longrightarrow> f b \<in> borel_measurable borel" |
|
385 assumes nn[simp]: "\<And>b x. b \<in> Basis \<Longrightarrow> 0 \<le> f b x" |
|
386 shows "(\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. f b (x \<bullet> b)) \<partial>lborel) = (\<Prod>b\<in>Basis. (\<integral>\<^sup>+x. f b x \<partial>lborel))" |
|
387 by (simp add: lborel_def nn_integral_distr product_nn_integral_setprod |
|
388 product_nn_integral_singleton) |
|
389 |
|
390 lemma emeasure_lborel_Icc[simp]: |
|
391 fixes l u :: real |
|
392 assumes [simp]: "l \<le> u" |
|
393 shows "emeasure lborel {l .. u} = u - l" |
|
394 proof - |
|
395 have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^sub>E {l..u}" |
|
396 by (auto simp: space_PiM) |
|
397 then show ?thesis |
|
398 by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc continuous_on_id) |
|
399 qed |
|
400 |
|
401 lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \<le> u then u - l else 0)" |
|
402 by simp |
|
403 |
|
404 lemma emeasure_lborel_cbox[simp]: |
|
405 assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
|
406 shows "emeasure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
407 proof - |
|
408 have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b) :: ennreal) = indicator (cbox l u)" |
|
409 by (auto simp: fun_eq_iff cbox_def split: split_indicator) |
|
410 then have "emeasure lborel (cbox l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b)) \<partial>lborel)" |
|
411 by simp |
|
412 also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
413 by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left) |
|
414 finally show ?thesis . |
|
415 qed |
|
416 |
|
417 lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c" |
|
418 using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c] |
|
419 by (auto simp add: cbox_sing setprod_constant power_0_left) |
|
420 |
|
421 lemma emeasure_lborel_Ioo[simp]: |
|
422 assumes [simp]: "l \<le> u" |
|
423 shows "emeasure lborel {l <..< u} = ennreal (u - l)" |
|
424 proof - |
|
425 have "emeasure lborel {l <..< u} = emeasure lborel {l .. u}" |
|
426 using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
|
427 then show ?thesis |
|
428 by simp |
|
429 qed |
|
430 |
|
431 lemma emeasure_lborel_Ioc[simp]: |
|
432 assumes [simp]: "l \<le> u" |
|
433 shows "emeasure lborel {l <.. u} = ennreal (u - l)" |
|
434 proof - |
|
435 have "emeasure lborel {l <.. u} = emeasure lborel {l .. u}" |
|
436 using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
|
437 then show ?thesis |
|
438 by simp |
|
439 qed |
|
440 |
|
441 lemma emeasure_lborel_Ico[simp]: |
|
442 assumes [simp]: "l \<le> u" |
|
443 shows "emeasure lborel {l ..< u} = ennreal (u - l)" |
|
444 proof - |
|
445 have "emeasure lborel {l ..< u} = emeasure lborel {l .. u}" |
|
446 using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto |
|
447 then show ?thesis |
|
448 by simp |
|
449 qed |
|
450 |
|
451 lemma emeasure_lborel_box[simp]: |
|
452 assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
|
453 shows "emeasure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
454 proof - |
|
455 have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b) :: ennreal) = indicator (box l u)" |
|
456 by (auto simp: fun_eq_iff box_def split: split_indicator) |
|
457 then have "emeasure lborel (box l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b)) \<partial>lborel)" |
|
458 by simp |
|
459 also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
460 by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left) |
|
461 finally show ?thesis . |
|
462 qed |
|
463 |
|
464 lemma emeasure_lborel_cbox_eq: |
|
465 "emeasure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)" |
|
466 using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le) |
|
467 |
|
468 lemma emeasure_lborel_box_eq: |
|
469 "emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)" |
|
470 using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force |
|
471 |
|
472 lemma |
|
473 fixes l u :: real |
|
474 assumes [simp]: "l \<le> u" |
|
475 shows measure_lborel_Icc[simp]: "measure lborel {l .. u} = u - l" |
|
476 and measure_lborel_Ico[simp]: "measure lborel {l ..< u} = u - l" |
|
477 and measure_lborel_Ioc[simp]: "measure lborel {l <.. u} = u - l" |
|
478 and measure_lborel_Ioo[simp]: "measure lborel {l <..< u} = u - l" |
|
479 by (simp_all add: measure_def) |
|
480 |
|
481 lemma |
|
482 assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
|
483 shows measure_lborel_box[simp]: "measure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
484 and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
485 by (simp_all add: measure_def inner_diff_left setprod_nonneg) |
|
486 |
|
487 lemma sigma_finite_lborel: "sigma_finite_measure lborel" |
|
488 proof |
|
489 show "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets lborel \<and> \<Union>A = space lborel \<and> (\<forall>a\<in>A. emeasure lborel a \<noteq> \<infinity>)" |
|
490 by (intro exI[of _ "range (\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One))"]) |
|
491 (auto simp: emeasure_lborel_cbox_eq UN_box_eq_UNIV) |
|
492 qed |
|
493 |
|
494 end |
|
495 |
|
496 lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>" |
|
497 proof - |
|
498 { fix n::nat |
|
499 let ?Ba = "Basis :: 'a set" |
|
500 have "real n \<le> (2::real) ^ card ?Ba * real n" |
|
501 by (simp add: mult_le_cancel_right1) |
|
502 also |
|
503 have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" |
|
504 apply (rule mult_left_mono) |
|
505 apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le of_nat_le_iff of_nat_power self_le_power zero_less_Suc) |
|
506 apply (simp add: DIM_positive) |
|
507 done |
|
508 finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" . |
|
509 } note [intro!] = this |
|
510 show ?thesis |
|
511 unfolding UN_box_eq_UNIV[symmetric] |
|
512 apply (subst SUP_emeasure_incseq[symmetric]) |
|
513 apply (auto simp: incseq_def subset_box inner_add_left setprod_constant |
|
514 simp del: Sup_eq_top_iff SUP_eq_top_iff |
|
515 intro!: ennreal_SUP_eq_top) |
|
516 done |
|
517 qed |
|
518 |
|
519 lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0" |
|
520 using emeasure_lborel_cbox[of x x] nonempty_Basis |
|
521 by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant) |
|
522 |
|
523 lemma emeasure_lborel_countable: |
|
524 fixes A :: "'a::euclidean_space set" |
|
525 assumes "countable A" |
|
526 shows "emeasure lborel A = 0" |
|
527 proof - |
|
528 have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force |
|
529 then have "emeasure lborel A \<le> emeasure lborel (\<Union>i. {from_nat_into A i})" |
|
530 by (intro emeasure_mono) auto |
|
531 also have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0" |
|
532 by (rule emeasure_UN_eq_0) auto |
|
533 finally show ?thesis |
|
534 by (auto simp add: ) |
|
535 qed |
|
536 |
|
537 lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel" |
|
538 by (simp add: null_sets_def emeasure_lborel_countable sets.countable) |
|
539 |
|
540 lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel" |
|
541 by (intro countable_imp_null_set_lborel countable_finite) |
|
542 |
|
543 lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)" |
|
544 proof |
|
545 assume asm: "lborel = count_space A" |
|
546 have "space lborel = UNIV" by simp |
|
547 hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space) |
|
548 have "emeasure lborel {undefined::'a} = 1" |
|
549 by (subst asm, subst emeasure_count_space_finite) auto |
|
550 moreover have "emeasure lborel {undefined} \<noteq> 1" by simp |
|
551 ultimately show False by contradiction |
|
552 qed |
|
553 |
|
554 subsection \<open>Affine transformation on the Lebesgue-Borel\<close> |
|
555 |
|
556 lemma lborel_eqI: |
|
557 fixes M :: "'a::euclidean_space measure" |
|
558 assumes emeasure_eq: "\<And>l u. (\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b) \<Longrightarrow> emeasure M (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)" |
|
559 assumes sets_eq: "sets M = sets borel" |
|
560 shows "lborel = M" |
|
561 proof (rule measure_eqI_generator_eq) |
|
562 let ?E = "range (\<lambda>(a, b). box a b::'a set)" |
|
563 show "Int_stable ?E" |
|
564 by (auto simp: Int_stable_def box_Int_box) |
|
565 |
|
566 show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E" |
|
567 by (simp_all add: borel_eq_box sets_eq) |
|
568 |
|
569 let ?A = "\<lambda>n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set" |
|
570 show "range ?A \<subseteq> ?E" "(\<Union>i. ?A i) = UNIV" |
|
571 unfolding UN_box_eq_UNIV by auto |
|
572 |
|
573 { fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto } |
|
574 { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X" |
|
575 apply (auto simp: emeasure_eq emeasure_lborel_box_eq ) |
|
576 apply (subst box_eq_empty(1)[THEN iffD2]) |
|
577 apply (auto intro: less_imp_le simp: not_le) |
|
578 done } |
|
579 qed |
|
580 |
|
581 lemma lborel_affine: |
|
582 fixes t :: "'a::euclidean_space" assumes "c \<noteq> 0" |
|
583 shows "lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" (is "_ = ?D") |
|
584 proof (rule lborel_eqI) |
|
585 let ?B = "Basis :: 'a set" |
|
586 fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b" |
|
587 show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)" |
|
588 proof cases |
|
589 assume "0 < c" |
|
590 then have "(\<lambda>x. t + c *\<^sub>R x) -` box l u = box ((l - t) /\<^sub>R c) ((u - t) /\<^sub>R c)" |
|
591 by (auto simp: field_simps box_def inner_simps) |
|
592 with \<open>0 < c\<close> show ?thesis |
|
593 using le |
|
594 by (auto simp: field_simps inner_simps setprod_dividef setprod_constant setprod_nonneg |
|
595 ennreal_mult[symmetric] emeasure_density nn_integral_distr emeasure_distr |
|
596 nn_integral_cmult emeasure_lborel_box_eq borel_measurable_indicator') |
|
597 next |
|
598 assume "\<not> 0 < c" with \<open>c \<noteq> 0\<close> have "c < 0" by auto |
|
599 then have "box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c) = (\<lambda>x. t + c *\<^sub>R x) -` box l u" |
|
600 by (auto simp: field_simps box_def inner_simps) |
|
601 then have *: "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ennreal)" |
|
602 by (auto split: split_indicator) |
|
603 have **: "(\<Prod>x\<in>Basis. (l \<bullet> x - u \<bullet> x) / c) = (\<Prod>x\<in>Basis. u \<bullet> x - l \<bullet> x) / (-c) ^ card (Basis::'a set)" |
|
604 using \<open>c < 0\<close> |
|
605 by (auto simp add: field_simps setprod_dividef[symmetric] setprod_constant[symmetric] |
|
606 intro!: setprod.cong) |
|
607 show ?thesis |
|
608 using \<open>c < 0\<close> le |
|
609 by (auto simp: * ** field_simps emeasure_density nn_integral_distr nn_integral_cmult |
|
610 emeasure_lborel_box_eq inner_simps setprod_nonneg ennreal_mult[symmetric] |
|
611 borel_measurable_indicator') |
|
612 qed |
|
613 qed simp |
|
614 |
|
615 lemma lborel_real_affine: |
|
616 "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))" |
|
617 using lborel_affine[of c t] by simp |
|
618 |
|
619 lemma AE_borel_affine: |
|
620 fixes P :: "real \<Rightarrow> bool" |
|
621 shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)" |
|
622 by (subst lborel_real_affine[where t="- t / c" and c="1 / c"]) |
|
623 (simp_all add: AE_density AE_distr_iff field_simps) |
|
624 |
|
625 lemma nn_integral_real_affine: |
|
626 fixes c :: real assumes [measurable]: "f \<in> borel_measurable borel" and c: "c \<noteq> 0" |
|
627 shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = \<bar>c\<bar> * (\<integral>\<^sup>+x. f (t + c * x) \<partial>lborel)" |
|
628 by (subst lborel_real_affine[OF c, of t]) |
|
629 (simp add: nn_integral_density nn_integral_distr nn_integral_cmult) |
|
630 |
|
631 lemma lborel_integrable_real_affine: |
|
632 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
633 assumes f: "integrable lborel f" |
|
634 shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x))" |
|
635 using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded |
|
636 by (subst (asm) nn_integral_real_affine[where c=c and t=t]) (auto simp: ennreal_mult_less_top) |
|
637 |
|
638 lemma lborel_integrable_real_affine_iff: |
|
639 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
640 shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x)) \<longleftrightarrow> integrable lborel f" |
|
641 using |
|
642 lborel_integrable_real_affine[of f c t] |
|
643 lborel_integrable_real_affine[of "\<lambda>x. f (t + c * x)" "1/c" "-t/c"] |
|
644 by (auto simp add: field_simps) |
|
645 |
|
646 lemma lborel_integral_real_affine: |
|
647 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" and c :: real |
|
648 assumes c: "c \<noteq> 0" shows "(\<integral>x. f x \<partial> lborel) = \<bar>c\<bar> *\<^sub>R (\<integral>x. f (t + c * x) \<partial>lborel)" |
|
649 proof cases |
|
650 assume f[measurable]: "integrable lborel f" then show ?thesis |
|
651 using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t] |
|
652 by (subst lborel_real_affine[OF c, of t]) |
|
653 (simp add: integral_density integral_distr) |
|
654 next |
|
655 assume "\<not> integrable lborel f" with c show ?thesis |
|
656 by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq) |
|
657 qed |
|
658 |
|
659 lemma divideR_right: |
|
660 fixes x y :: "'a::real_normed_vector" |
|
661 shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x" |
|
662 using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp |
|
663 |
|
664 lemma lborel_has_bochner_integral_real_affine_iff: |
|
665 fixes x :: "'a :: {banach, second_countable_topology}" |
|
666 shows "c \<noteq> 0 \<Longrightarrow> |
|
667 has_bochner_integral lborel f x \<longleftrightarrow> |
|
668 has_bochner_integral lborel (\<lambda>x. f (t + c * x)) (x /\<^sub>R \<bar>c\<bar>)" |
|
669 unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff |
|
670 by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong) |
|
671 |
|
672 lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)" |
|
673 by (subst lborel_real_affine[of "-1" 0]) |
|
674 (auto simp: density_1 one_ennreal_def[symmetric]) |
|
675 |
|
676 lemma lborel_distr_mult: |
|
677 assumes "(c::real) \<noteq> 0" |
|
678 shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)" |
|
679 proof- |
|
680 have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong) |
|
681 also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)" |
|
682 by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr) |
|
683 finally show ?thesis . |
|
684 qed |
|
685 |
|
686 lemma lborel_distr_mult': |
|
687 assumes "(c::real) \<noteq> 0" |
|
688 shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. \<bar>c\<bar>)" |
|
689 proof- |
|
690 have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric]) |
|
691 also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp |
|
692 also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)" |
|
693 by (subst density_density_eq) (auto simp: ennreal_mult) |
|
694 also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (op * c)" |
|
695 by (rule lborel_distr_mult[symmetric]) |
|
696 finally show ?thesis . |
|
697 qed |
|
698 |
|
699 lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)" |
|
700 by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric]) |
|
701 |
|
702 interpretation lborel: sigma_finite_measure lborel |
|
703 by (rule sigma_finite_lborel) |
|
704 |
|
705 interpretation lborel_pair: pair_sigma_finite lborel lborel .. |
|
706 |
|
707 lemma lborel_prod: |
|
708 "lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)" |
|
709 proof (rule lborel_eqI[symmetric], clarify) |
|
710 fix la ua :: 'a and lb ub :: 'b |
|
711 assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)" |
|
712 have [simp]: |
|
713 "\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b" |
|
714 "\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b" |
|
715 "inj_on (\<lambda>u. (u, 0)) Basis" "inj_on (\<lambda>u. (0, u)) Basis" |
|
716 "(\<lambda>u. (u, 0)) ` Basis \<inter> (\<lambda>u. (0, u)) ` Basis = {}" |
|
717 "box (la, lb) (ua, ub) = box la ua \<times> box lb ub" |
|
718 using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def) |
|
719 show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) = |
|
720 ennreal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)" |
|
721 by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint |
|
722 setprod.reindex ennreal_mult inner_diff_left setprod_nonneg) |
|
723 qed (simp add: borel_prod[symmetric]) |
|
724 |
|
725 (* FIXME: conversion in measurable prover *) |
|
726 lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp |
|
727 lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp |
|
728 |
|
729 subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close> |
|
730 |
|
731 lemma has_integral_measure_lborel: |
|
732 fixes A :: "'a::euclidean_space set" |
|
733 assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>" |
|
734 shows "((\<lambda>x. 1) has_integral measure lborel A) A" |
|
735 proof - |
|
736 { fix l u :: 'a |
|
737 have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)" |
|
738 proof cases |
|
739 assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b" |
|
740 then show ?thesis |
|
741 apply simp |
|
742 apply (subst has_integral_restrict[symmetric, OF box_subset_cbox]) |
|
743 apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"]) |
|
744 using has_integral_const[of "1::real" l u] |
|
745 apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases) |
|
746 done |
|
747 next |
|
748 assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)" |
|
749 then have "box l u = {}" |
|
750 unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le) |
|
751 then show ?thesis |
|
752 by simp |
|
753 qed } |
|
754 note has_integral_box = this |
|
755 |
|
756 { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)" |
|
757 have "Int_stable (range (\<lambda>(a, b). box a b))" |
|
758 by (auto simp: Int_stable_def box_Int_box) |
|
759 moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV" |
|
760 by auto |
|
761 moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))" |
|
762 using A unfolding borel_eq_box by simp |
|
763 ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)" |
|
764 proof (induction rule: sigma_sets_induct_disjoint) |
|
765 case (basic A) then show ?case |
|
766 by (auto simp: box_Int_box has_integral_box) |
|
767 next |
|
768 case empty then show ?case |
|
769 by simp |
|
770 next |
|
771 case (compl A) |
|
772 then have [measurable]: "A \<in> sets borel" |
|
773 by (simp add: borel_eq_box) |
|
774 |
|
775 have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)" |
|
776 by (simp add: has_integral_box) |
|
777 moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)" |
|
778 by (subst has_integral_restrict) (auto intro: compl) |
|
779 ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)" |
|
780 by (rule has_integral_sub) |
|
781 then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)" |
|
782 by (rule has_integral_cong[THEN iffD1, rotated 1]) auto |
|
783 then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)" |
|
784 by (subst (asm) has_integral_restrict) auto |
|
785 also have "?M (box a b) - ?M A = ?M (UNIV - A)" |
|
786 by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2) |
|
787 finally show ?case . |
|
788 next |
|
789 case (union F) |
|
790 then have [measurable]: "\<And>i. F i \<in> sets borel" |
|
791 by (simp add: borel_eq_box subset_eq) |
|
792 have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)" |
|
793 proof (rule has_integral_monotone_convergence_increasing) |
|
794 let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real" |
|
795 show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)" |
|
796 using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff) |
|
797 show "\<And>k x. ?f k x \<le> ?f (Suc k) x" |
|
798 by (intro setsum_mono2) auto |
|
799 from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i" |
|
800 by (auto simp add: disjoint_family_on_def) |
|
801 show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)" |
|
802 apply (auto simp: * setsum.If_cases Iio_Int_singleton) |
|
803 apply (rule_tac k="Suc xa" in LIMSEQ_offset) |
|
804 apply simp |
|
805 done |
|
806 have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)" |
|
807 by (intro emeasure_mono) auto |
|
808 |
|
809 with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)" |
|
810 unfolding sums_def[symmetric] UN_extend_simps |
|
811 by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique) |
|
812 qed |
|
813 then show ?case |
|
814 by (subst (asm) has_integral_restrict) auto |
|
815 qed } |
|
816 note * = this |
|
817 |
|
818 show ?thesis |
|
819 proof (rule has_integral_monotone_convergence_increasing) |
|
820 let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set" |
|
821 let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real" |
|
822 let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)" |
|
823 |
|
824 show "\<And>n::nat. (?f n has_integral ?M n) A" |
|
825 using * by (subst has_integral_restrict) simp_all |
|
826 show "\<And>k x. ?f k x \<le> ?f (Suc k) x" |
|
827 by (auto simp: box_def) |
|
828 { fix x assume "x \<in> A" |
|
829 moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x" |
|
830 by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def) |
|
831 ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1" |
|
832 by (simp add: indicator_def UN_box_eq_UNIV) } |
|
833 |
|
834 have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)" |
|
835 by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def) |
|
836 also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))" |
|
837 proof (intro ext emeasure_eq_ennreal_measure) |
|
838 fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)" |
|
839 by (intro emeasure_mono) auto |
|
840 then show "emeasure lborel (A \<inter> ?B n) \<noteq> top" |
|
841 by (auto simp: top_unique) |
|
842 qed |
|
843 finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A" |
|
844 using emeasure_eq_ennreal_measure[of lborel A] finite |
|
845 by (simp add: UN_box_eq_UNIV less_top) |
|
846 qed |
|
847 qed |
|
848 |
|
849 lemma nn_integral_has_integral: |
|
850 fixes f::"'a::euclidean_space \<Rightarrow> real" |
|
851 assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r" |
|
852 shows "(f has_integral r) UNIV" |
|
853 using f proof (induct f arbitrary: r rule: borel_measurable_induct_real) |
|
854 case (set A) |
|
855 then have "((\<lambda>x. 1) has_integral measure lborel A) A" |
|
856 by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator) |
|
857 with set show ?case |
|
858 by (simp add: ennreal_indicator measure_def) (simp add: indicator_def) |
|
859 next |
|
860 case (mult g c) |
|
861 then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r" |
|
862 by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult) |
|
863 with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close> |
|
864 obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')" |
|
865 by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases) |
|
866 (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric]) |
|
867 with mult show ?case |
|
868 by (auto intro!: has_integral_cmult_real) |
|
869 next |
|
870 case (add g h) |
|
871 then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)" |
|
872 by (simp add: nn_integral_add) |
|
873 with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b" |
|
874 by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases) |
|
875 (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus) |
|
876 with add show ?case |
|
877 by (auto intro!: has_integral_add) |
|
878 next |
|
879 case (seq U) |
|
880 note seq(1)[measurable] and f[measurable] |
|
881 |
|
882 { fix i x |
|
883 have "U i x \<le> f x" |
|
884 using seq(5) |
|
885 apply (rule LIMSEQ_le_const) |
|
886 using seq(4) |
|
887 apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def) |
|
888 done } |
|
889 note U_le_f = this |
|
890 |
|
891 { fix i |
|
892 have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)" |
|
893 using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp |
|
894 then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p" |
|
895 using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique) |
|
896 moreover note seq |
|
897 ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV" |
|
898 by auto } |
|
899 then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)" |
|
900 and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i" |
|
901 and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis |
|
902 |
|
903 have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique) |
|
904 |
|
905 have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f" |
|
906 proof (rule monotone_convergence_increasing) |
|
907 show "\<forall>k. U k integrable_on UNIV" using U_int by auto |
|
908 show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def) |
|
909 then show "bounded {integral UNIV (U k) |k. True}" |
|
910 using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r]) |
|
911 show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x" |
|
912 using seq by auto |
|
913 qed |
|
914 moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)" |
|
915 using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto |
|
916 ultimately have "integral UNIV f = r" |
|
917 by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique) |
|
918 with * show ?case |
|
919 by (simp add: has_integral_integral) |
|
920 qed |
|
921 |
|
922 lemma nn_integral_lborel_eq_integral: |
|
923 fixes f::"'a::euclidean_space \<Rightarrow> real" |
|
924 assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>" |
|
925 shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f" |
|
926 proof - |
|
927 from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r" |
|
928 by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto |
|
929 then show ?thesis |
|
930 using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique) |
|
931 qed |
|
932 |
|
933 lemma nn_integral_integrable_on: |
|
934 fixes f::"'a::euclidean_space \<Rightarrow> real" |
|
935 assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>" |
|
936 shows "f integrable_on UNIV" |
|
937 proof - |
|
938 from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r" |
|
939 by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto |
|
940 then show ?thesis |
|
941 by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f) |
|
942 qed |
|
943 |
|
944 lemma nn_integral_has_integral_lborel: |
|
945 fixes f :: "'a::euclidean_space \<Rightarrow> real" |
|
946 assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x" |
|
947 assumes I: "(f has_integral I) UNIV" |
|
948 shows "integral\<^sup>N lborel f = I" |
|
949 proof - |
|
950 from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto |
|
951 from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this |
|
952 let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set" |
|
953 |
|
954 note F(1)[THEN borel_measurable_simple_function, measurable] |
|
955 |
|
956 have "0 \<le> I" |
|
957 using I by (rule has_integral_nonneg) (simp add: nonneg) |
|
958 |
|
959 have F_le_f: "enn2real (F i x) \<le> f x" for i x |
|
960 using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"] |
|
961 by (cases "F i x" rule: ennreal_cases) auto |
|
962 let ?F = "\<lambda>i x. F i x * indicator (?B i) x" |
|
963 have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))" |
|
964 proof (subst nn_integral_monotone_convergence_SUP[symmetric]) |
|
965 { fix x |
|
966 obtain j where j: "x \<in> ?B j" |
|
967 using UN_box_eq_UNIV by auto |
|
968 |
|
969 have "ennreal (f x) = (SUP i. F i x)" |
|
970 using F(4)[of x] nonneg[of x] by (simp add: max_def) |
|
971 also have "\<dots> = (SUP i. ?F i x)" |
|
972 proof (rule SUP_eq) |
|
973 fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x" |
|
974 using j F(2) |
|
975 by (intro bexI[of _ "max i j"]) |
|
976 (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def) |
|
977 qed (auto intro!: F split: split_indicator) |
|
978 finally have "ennreal (f x) = (SUP i. ?F i x)" . } |
|
979 then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)" |
|
980 by simp |
|
981 qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator) |
|
982 also have "\<dots> \<le> ennreal I" |
|
983 proof (rule SUP_least) |
|
984 fix i :: nat |
|
985 have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>" |
|
986 proof (rule nn_integral_bound_simple_function) |
|
987 have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le> |
|
988 emeasure lborel (?B i)" |
|
989 by (intro emeasure_mono) (auto split: split_indicator) |
|
990 then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>" |
|
991 by (auto simp: less_top[symmetric] top_unique) |
|
992 qed (auto split: split_indicator |
|
993 intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal) |
|
994 |
|
995 have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV" |
|
996 using F(4) finite_F |
|
997 by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg) |
|
998 |
|
999 have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) = |
|
1000 (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)" |
|
1001 using F(3,4) |
|
1002 by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator) |
|
1003 also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))" |
|
1004 using F |
|
1005 by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F]) |
|
1006 (auto split: split_indicator intro: enn2real_nonneg) |
|
1007 also have "\<dots> \<le> ennreal I" |
|
1008 by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f |
|
1009 simp: \<open>0 \<le> I\<close> split: split_indicator ) |
|
1010 finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" . |
|
1011 qed |
|
1012 finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>" |
|
1013 by (auto simp: less_top[symmetric] top_unique) |
|
1014 from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis |
|
1015 by (simp add: integral_unique) |
|
1016 qed |
|
1017 |
|
1018 lemma has_integral_iff_emeasure_lborel: |
|
1019 fixes A :: "'a::euclidean_space set" |
|
1020 assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r" |
|
1021 shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r" |
|
1022 proof (cases "emeasure lborel A = \<infinity>") |
|
1023 case emeasure_A: True |
|
1024 have "\<not> (\<lambda>x. 1::real) integrable_on A" |
|
1025 proof |
|
1026 assume int: "(\<lambda>x. 1::real) integrable_on A" |
|
1027 then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV" |
|
1028 unfolding indicator_def[abs_def] integrable_restrict_univ . |
|
1029 then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV" |
|
1030 by auto |
|
1031 from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False |
|
1032 by (simp add: ennreal_indicator) |
|
1033 qed |
|
1034 with emeasure_A show ?thesis |
|
1035 by auto |
|
1036 next |
|
1037 case False |
|
1038 then have "((\<lambda>x. 1) has_integral measure lborel A) A" |
|
1039 by (simp add: has_integral_measure_lborel less_top) |
|
1040 with False show ?thesis |
|
1041 by (auto simp: emeasure_eq_ennreal_measure has_integral_unique) |
|
1042 qed |
|
1043 |
|
1044 lemma has_integral_integral_real: |
|
1045 fixes f::"'a::euclidean_space \<Rightarrow> real" |
|
1046 assumes f: "integrable lborel f" |
|
1047 shows "(f has_integral (integral\<^sup>L lborel f)) UNIV" |
|
1048 using f proof induct |
|
1049 case (base A c) then show ?case |
|
1050 by (auto intro!: has_integral_mult_left simp: ) |
|
1051 (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel) |
|
1052 next |
|
1053 case (add f g) then show ?case |
|
1054 by (auto intro!: has_integral_add) |
|
1055 next |
|
1056 case (lim f s) |
|
1057 show ?case |
|
1058 proof (rule has_integral_dominated_convergence) |
|
1059 show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact |
|
1060 show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV" |
|
1061 using \<open>integrable lborel f\<close> |
|
1062 by (intro nn_integral_integrable_on) |
|
1063 (auto simp: integrable_iff_bounded abs_mult nn_integral_cmult ennreal_mult ennreal_mult_less_top) |
|
1064 show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)" |
|
1065 using lim by (auto simp add: abs_mult) |
|
1066 show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x" |
|
1067 using lim by auto |
|
1068 show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f" |
|
1069 using lim lim(1)[THEN borel_measurable_integrable] |
|
1070 by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto |
|
1071 qed |
|
1072 qed |
|
1073 |
|
1074 context |
|
1075 fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
1076 begin |
|
1077 |
|
1078 lemma has_integral_integral_lborel: |
|
1079 assumes f: "integrable lborel f" |
|
1080 shows "(f has_integral (integral\<^sup>L lborel f)) UNIV" |
|
1081 proof - |
|
1082 have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV" |
|
1083 using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto |
|
1084 also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f" |
|
1085 by (simp add: fun_eq_iff euclidean_representation) |
|
1086 also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f" |
|
1087 using f by (subst (2) eq_f[symmetric]) simp |
|
1088 finally show ?thesis . |
|
1089 qed |
|
1090 |
|
1091 lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV" |
|
1092 using has_integral_integral_lborel by auto |
|
1093 |
|
1094 lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)" |
|
1095 using has_integral_integral_lborel by auto |
|
1096 |
|
1097 end |
|
1098 |
|
1099 subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close> |
|
1100 |
|
1101 lemma emeasure_bounded_finite: |
|
1102 assumes "bounded A" shows "emeasure lborel A < \<infinity>" |
|
1103 proof - |
|
1104 from bounded_subset_cbox[OF \<open>bounded A\<close>] obtain a b where "A \<subseteq> cbox a b" |
|
1105 by auto |
|
1106 then have "emeasure lborel A \<le> emeasure lborel (cbox a b)" |
|
1107 by (intro emeasure_mono) auto |
|
1108 then show ?thesis |
|
1109 by (auto simp: emeasure_lborel_cbox_eq setprod_nonneg less_top[symmetric] top_unique split: if_split_asm) |
|
1110 qed |
|
1111 |
|
1112 lemma emeasure_compact_finite: "compact A \<Longrightarrow> emeasure lborel A < \<infinity>" |
|
1113 using emeasure_bounded_finite[of A] by (auto intro: compact_imp_bounded) |
|
1114 |
|
1115 lemma borel_integrable_compact: |
|
1116 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}" |
|
1117 assumes "compact S" "continuous_on S f" |
|
1118 shows "integrable lborel (\<lambda>x. indicator S x *\<^sub>R f x)" |
|
1119 proof cases |
|
1120 assume "S \<noteq> {}" |
|
1121 have "continuous_on S (\<lambda>x. norm (f x))" |
|
1122 using assms by (intro continuous_intros) |
|
1123 from continuous_attains_sup[OF \<open>compact S\<close> \<open>S \<noteq> {}\<close> this] |
|
1124 obtain M where M: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> M" |
|
1125 by auto |
|
1126 |
|
1127 show ?thesis |
|
1128 proof (rule integrable_bound) |
|
1129 show "integrable lborel (\<lambda>x. indicator S x * M)" |
|
1130 using assms by (auto intro!: emeasure_compact_finite borel_compact integrable_mult_left) |
|
1131 show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lborel" |
|
1132 using assms by (auto intro!: borel_measurable_continuous_on_indicator borel_compact) |
|
1133 show "AE x in lborel. norm (indicator S x *\<^sub>R f x) \<le> norm (indicator S x * M)" |
|
1134 by (auto split: split_indicator simp: abs_real_def dest!: M) |
|
1135 qed |
|
1136 qed simp |
|
1137 |
|
1138 lemma borel_integrable_atLeastAtMost: |
|
1139 fixes f :: "real \<Rightarrow> real" |
|
1140 assumes f: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" |
|
1141 shows "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is "integrable _ ?f") |
|
1142 proof - |
|
1143 have "integrable lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x)" |
|
1144 proof (rule borel_integrable_compact) |
|
1145 from f show "continuous_on {a..b} f" |
|
1146 by (auto intro: continuous_at_imp_continuous_on) |
|
1147 qed simp |
|
1148 then show ?thesis |
|
1149 by (auto simp: mult.commute) |
|
1150 qed |
|
1151 |
|
1152 text \<open> |
|
1153 |
|
1154 For the positive integral we replace continuity with Borel-measurability. |
|
1155 |
|
1156 \<close> |
|
1157 |
|
1158 lemma |
|
1159 fixes f :: "real \<Rightarrow> real" |
|
1160 assumes [measurable]: "f \<in> borel_measurable borel" |
|
1161 assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b" |
|
1162 shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn) |
|
1163 and has_bochner_integral_FTC_Icc_nonneg: |
|
1164 "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has) |
|
1165 and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq) |
|
1166 and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int) |
|
1167 proof - |
|
1168 have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x" |
|
1169 using f(2) by (auto split: split_indicator) |
|
1170 |
|
1171 have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y |
|
1172 using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans) |
|
1173 |
|
1174 have "(f has_integral F b - F a) {a..b}" |
|
1175 by (intro fundamental_theorem_of_calculus) |
|
1176 (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] |
|
1177 intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>) |
|
1178 then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV" |
|
1179 unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a] |
|
1180 by (simp cong del: if_weak_cong del: atLeastAtMost_iff) |
|
1181 then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" |
|
1182 by (rule nn_integral_has_integral_lborel[OF *]) |
|
1183 then show ?has |
|
1184 by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>) |
|
1185 then show ?eq ?int |
|
1186 unfolding has_bochner_integral_iff by auto |
|
1187 show ?nn |
|
1188 by (subst nn[symmetric]) |
|
1189 (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator) |
|
1190 qed |
|
1191 |
|
1192 lemma |
|
1193 fixes f :: "real \<Rightarrow> 'a :: euclidean_space" |
|
1194 assumes "a \<le> b" |
|
1195 assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})" |
|
1196 assumes cont: "continuous_on {a .. b} f" |
|
1197 shows has_bochner_integral_FTC_Icc: |
|
1198 "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has) |
|
1199 and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq) |
|
1200 proof - |
|
1201 let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x" |
|
1202 have int: "integrable lborel ?f" |
|
1203 using borel_integrable_compact[OF _ cont] by auto |
|
1204 have "(f has_integral F b - F a) {a..b}" |
|
1205 using assms(1,2) by (intro fundamental_theorem_of_calculus) auto |
|
1206 moreover |
|
1207 have "(f has_integral integral\<^sup>L lborel ?f) {a..b}" |
|
1208 using has_integral_integral_lborel[OF int] |
|
1209 unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] |
|
1210 by (simp cong del: if_weak_cong del: atLeastAtMost_iff) |
|
1211 ultimately show ?eq |
|
1212 by (auto dest: has_integral_unique) |
|
1213 then show ?has |
|
1214 using int by (auto simp: has_bochner_integral_iff) |
|
1215 qed |
|
1216 |
|
1217 lemma |
|
1218 fixes f :: "real \<Rightarrow> real" |
|
1219 assumes "a \<le> b" |
|
1220 assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x" |
|
1221 assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x" |
|
1222 shows has_bochner_integral_FTC_Icc_real: |
|
1223 "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has) |
|
1224 and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq) |
|
1225 proof - |
|
1226 have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})" |
|
1227 unfolding has_field_derivative_iff_has_vector_derivative[symmetric] |
|
1228 using deriv by (auto intro: DERIV_subset) |
|
1229 have 2: "continuous_on {a .. b} f" |
|
1230 using cont by (intro continuous_at_imp_continuous_on) auto |
|
1231 show ?has ?eq |
|
1232 using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] |
|
1233 by (auto simp: mult.commute) |
|
1234 qed |
|
1235 |
|
1236 lemma nn_integral_FTC_atLeast: |
|
1237 fixes f :: "real \<Rightarrow> real" |
|
1238 assumes f_borel: "f \<in> borel_measurable borel" |
|
1239 assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x" |
|
1240 assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x" |
|
1241 assumes lim: "(F \<longlongrightarrow> T) at_top" |
|
1242 shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a" |
|
1243 proof - |
|
1244 let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x" |
|
1245 let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x" |
|
1246 |
|
1247 have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y |
|
1248 using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans) |
|
1249 then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x |
|
1250 by (intro tendsto_le_const[OF _ lim]) |
|
1251 (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder) |
|
1252 |
|
1253 have "(SUP i::nat. ?f i x) = ?fR x" for x |
|
1254 proof (rule LIMSEQ_unique[OF LIMSEQ_SUP]) |
|
1255 from reals_Archimedean2[of "x - a"] guess n .. |
|
1256 then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially" |
|
1257 by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator) |
|
1258 then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x" |
|
1259 by (rule Lim_eventually) |
|
1260 qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator) |
|
1261 then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)" |
|
1262 by simp |
|
1263 also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))" |
|
1264 proof (rule nn_integral_monotone_convergence_SUP) |
|
1265 show "incseq ?f" |
|
1266 using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator) |
|
1267 show "\<And>i. (?f i) \<in> borel_measurable lborel" |
|
1268 using f_borel by auto |
|
1269 qed |
|
1270 also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))" |
|
1271 by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto |
|
1272 also have "\<dots> = T - F a" |
|
1273 proof (rule LIMSEQ_unique[OF LIMSEQ_SUP]) |
|
1274 have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T" |
|
1275 apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top]) |
|
1276 apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl]) |
|
1277 apply (rule filterlim_real_sequentially) |
|
1278 done |
|
1279 then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)" |
|
1280 by (simp add: F_mono F_le_T tendsto_diff) |
|
1281 qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono) |
|
1282 finally show ?thesis . |
|
1283 qed |
|
1284 |
|
1285 lemma integral_power: |
|
1286 "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k" |
|
1287 proof (subst integral_FTC_Icc_real) |
|
1288 fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k" |
|
1289 by (intro derivative_eq_intros) auto |
|
1290 qed (auto simp: field_simps simp del: of_nat_Suc) |
|
1291 |
|
1292 subsection \<open>Integration by parts\<close> |
|
1293 |
|
1294 lemma integral_by_parts_integrable: |
|
1295 fixes f g F G::"real \<Rightarrow> real" |
|
1296 assumes "a \<le> b" |
|
1297 assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x" |
|
1298 assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x" |
|
1299 assumes [intro]: "!!x. DERIV F x :> f x" |
|
1300 assumes [intro]: "!!x. DERIV G x :> g x" |
|
1301 shows "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)" |
|
1302 by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont) |
|
1303 |
|
1304 lemma integral_by_parts: |
|
1305 fixes f g F G::"real \<Rightarrow> real" |
|
1306 assumes [arith]: "a \<le> b" |
|
1307 assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x" |
|
1308 assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x" |
|
1309 assumes [intro]: "!!x. DERIV F x :> f x" |
|
1310 assumes [intro]: "!!x. DERIV G x :> g x" |
|
1311 shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) |
|
1312 = F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" |
|
1313 proof- |
|
1314 have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a" |
|
1315 by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros) |
|
1316 (auto intro!: DERIV_isCont) |
|
1317 |
|
1318 have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = |
|
1319 (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" |
|
1320 apply (subst integral_add[symmetric]) |
|
1321 apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros) |
|
1322 by (auto intro!: DERIV_isCont integral_cong split:split_indicator) |
|
1323 |
|
1324 thus ?thesis using 0 by auto |
|
1325 qed |
|
1326 |
|
1327 lemma integral_by_parts': |
|
1328 fixes f g F G::"real \<Rightarrow> real" |
|
1329 assumes "a \<le> b" |
|
1330 assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x" |
|
1331 assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x" |
|
1332 assumes "!!x. DERIV F x :> f x" |
|
1333 assumes "!!x. DERIV G x :> g x" |
|
1334 shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel) |
|
1335 = F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" |
|
1336 using integral_by_parts[OF assms] by (simp add: ac_simps) |
|
1337 |
|
1338 lemma has_bochner_integral_even_function: |
|
1339 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
1340 assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x" |
|
1341 assumes even: "\<And>x. f (- x) = f x" |
|
1342 shows "has_bochner_integral lborel f (2 *\<^sub>R x)" |
|
1343 proof - |
|
1344 have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x" |
|
1345 by (auto split: split_indicator) |
|
1346 have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x" |
|
1347 by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0]) |
|
1348 (auto simp: indicator even f) |
|
1349 with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)" |
|
1350 by (rule has_bochner_integral_add) |
|
1351 then have "has_bochner_integral lborel f (x + x)" |
|
1352 by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4]) |
|
1353 (auto split: split_indicator) |
|
1354 then show ?thesis |
|
1355 by (simp add: scaleR_2) |
|
1356 qed |
|
1357 |
|
1358 lemma has_bochner_integral_odd_function: |
|
1359 fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}" |
|
1360 assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x" |
|
1361 assumes odd: "\<And>x. f (- x) = - f x" |
|
1362 shows "has_bochner_integral lborel f 0" |
|
1363 proof - |
|
1364 have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x" |
|
1365 by (auto split: split_indicator) |
|
1366 have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x" |
|
1367 by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0]) |
|
1368 (auto simp: indicator odd f) |
|
1369 from has_bochner_integral_minus[OF this] |
|
1370 have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)" |
|
1371 by simp |
|
1372 with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)" |
|
1373 by (rule has_bochner_integral_add) |
|
1374 then have "has_bochner_integral lborel f (x + - x)" |
|
1375 by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4]) |
|
1376 (auto split: split_indicator) |
|
1377 then show ?thesis |
|
1378 by simp |
|
1379 qed |
|
1380 |
|
1381 end |