|
1 |
|
2 header {* Lebsegue measure *} |
|
3 (* Author: Robert Himmelmann, TU Muenchen *) |
|
4 |
|
5 theory Lebesgue_Measure |
|
6 imports Gauge_Measure Measure Lebesgue_Integration |
|
7 begin |
|
8 |
|
9 subsection {* Various *} |
|
10 |
|
11 lemma seq_offset_iff:"f ----> l \<longleftrightarrow> (\<lambda>i. f (i + k)) ----> l" |
|
12 using seq_offset_rev seq_offset[of f l k] by auto |
|
13 |
|
14 lemma has_integral_disjoint_union: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach" |
|
15 assumes "(f has_integral i) s" "(f has_integral j) t" "s \<inter> t = {}" |
|
16 shows "(f has_integral (i + j)) (s \<union> t)" |
|
17 apply(rule has_integral_union[OF assms(1-2)]) unfolding assms by auto |
|
18 |
|
19 lemma lim_eq: assumes "\<forall>n>N. f n = g n" shows "(f ----> l) \<longleftrightarrow> (g ----> l)" using assms |
|
20 proof(induct N arbitrary: f g) case 0 |
|
21 hence *:"\<And>n. f (Suc n) = g (Suc n)" by auto |
|
22 show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym]) |
|
23 unfolding * .. |
|
24 next case (Suc n) |
|
25 show ?case apply(subst LIMSEQ_Suc_iff[THEN sym]) apply(subst(2) LIMSEQ_Suc_iff[THEN sym]) |
|
26 apply(rule Suc(1)) using Suc(2) by auto |
|
27 qed |
|
28 |
|
29 subsection {* Standard Cubes *} |
|
30 |
|
31 definition cube where |
|
32 "cube (n::nat) \<equiv> {\<chi>\<chi> i. - real n .. (\<chi>\<chi> i. real n)::_::ordered_euclidean_space}" |
|
33 |
|
34 lemma cube_subset[intro]:"n\<le>N \<Longrightarrow> cube n \<subseteq> (cube N::'a::ordered_euclidean_space set)" |
|
35 apply(auto simp: eucl_le[where 'a='a] cube_def) apply(erule_tac[!] x=i in allE)+ by auto |
|
36 |
|
37 lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n" |
|
38 unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta' |
|
39 proof- fix x::'a and i assume as:"x\<in>ball 0 (real n)" "i<DIM('a)" |
|
40 thus "- real n \<le> x $$ i" "real n \<ge> x $$ i" |
|
41 using component_le_norm[of x i] by(auto simp: dist_norm) |
|
42 qed |
|
43 |
|
44 lemma mem_big_cube: obtains n where "x \<in> cube n" |
|
45 proof- from real_arch_lt[of "norm x"] guess n .. |
|
46 thus ?thesis apply-apply(rule that[where n=n]) |
|
47 apply(rule ball_subset_cube[unfolded subset_eq,rule_format]) |
|
48 by (auto simp add:dist_norm) |
|
49 qed |
|
50 |
|
51 lemma Union_inter_cube:"\<Union>{s \<inter> cube n |n. n \<in> UNIV} = s" |
|
52 proof safe case goal1 |
|
53 from mem_big_cube[of x] guess n . note n=this |
|
54 show ?case unfolding Union_iff apply(rule_tac x="s \<inter> cube n" in bexI) |
|
55 using n goal1 by auto |
|
56 qed |
|
57 |
|
58 lemma gmeasurable_cube[intro]:"gmeasurable (cube n)" |
|
59 unfolding cube_def by auto |
|
60 |
|
61 lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set" |
|
62 assumes "gmeasurable (s \<inter> cube n)" shows "gmeasure (s \<inter> cube n) \<le> gmeasure (cube n::'a set)" |
|
63 apply(rule has_gmeasure_subset[of "s\<inter>cube n" _ "cube n"]) |
|
64 unfolding has_gmeasure_measure[THEN sym] using assms by auto |
|
65 |
|
66 |
|
67 subsection {* Measurability *} |
|
68 |
|
69 definition lmeasurable :: "('a::ordered_euclidean_space) set => bool" where |
|
70 "lmeasurable s \<equiv> (\<forall>n::nat. gmeasurable (s \<inter> cube n))" |
|
71 |
|
72 lemma lmeasurableD[dest]:assumes "lmeasurable s" |
|
73 shows "\<And>n. gmeasurable (s \<inter> cube n)" |
|
74 using assms unfolding lmeasurable_def by auto |
|
75 |
|
76 lemma measurable_imp_lmeasurable: assumes"gmeasurable s" |
|
77 shows "lmeasurable s" unfolding lmeasurable_def cube_def |
|
78 using assms gmeasurable_interval by auto |
|
79 |
|
80 lemma lmeasurable_empty[intro]: "lmeasurable {}" |
|
81 using gmeasurable_empty apply- apply(drule_tac measurable_imp_lmeasurable) . |
|
82 |
|
83 lemma lmeasurable_union[intro]: assumes "lmeasurable s" "lmeasurable t" |
|
84 shows "lmeasurable (s \<union> t)" |
|
85 using assms unfolding lmeasurable_def Int_Un_distrib2 |
|
86 by(auto intro:gmeasurable_union) |
|
87 |
|
88 lemma lmeasurable_countable_unions_strong: |
|
89 fixes s::"nat => 'a::ordered_euclidean_space set" |
|
90 assumes "\<And>n::nat. lmeasurable(s n)" |
|
91 shows "lmeasurable(\<Union>{ s(n) |n. n \<in> UNIV })" |
|
92 unfolding lmeasurable_def |
|
93 proof fix n::nat |
|
94 have *:"\<Union>{s n |n. n \<in> UNIV} \<inter> cube n = \<Union>{s k \<inter> cube n |k. k \<in> UNIV}" by auto |
|
95 show "gmeasurable (\<Union>{s n |n. n \<in> UNIV} \<inter> cube n)" unfolding * |
|
96 apply(rule gmeasurable_countable_unions_strong) |
|
97 apply(rule assms[unfolded lmeasurable_def,rule_format]) |
|
98 proof- fix k::nat |
|
99 show "gmeasure (\<Union>{s ka \<inter> cube n |ka. ka \<le> k}) \<le> gmeasure (cube n::'a set)" |
|
100 apply(rule measure_subset) apply(rule gmeasurable_finite_unions) |
|
101 using assms(1)[unfolded lmeasurable_def] by auto |
|
102 qed |
|
103 qed |
|
104 |
|
105 lemma lmeasurable_inter[intro]: fixes s::"'a :: ordered_euclidean_space set" |
|
106 assumes "lmeasurable s" "lmeasurable t" shows "lmeasurable (s \<inter> t)" |
|
107 unfolding lmeasurable_def |
|
108 proof fix n::nat |
|
109 have *:"s \<inter> t \<inter> cube n = (s \<inter> cube n) \<inter> (t \<inter> cube n)" by auto |
|
110 show "gmeasurable (s \<inter> t \<inter> cube n)" |
|
111 using assms unfolding lmeasurable_def * |
|
112 using gmeasurable_inter[of "s \<inter> cube n" "t \<inter> cube n"] by auto |
|
113 qed |
|
114 |
|
115 lemma lmeasurable_complement[intro]: assumes "lmeasurable s" |
|
116 shows "lmeasurable (UNIV - s)" |
|
117 unfolding lmeasurable_def |
|
118 proof fix n::nat |
|
119 have *:"(UNIV - s) \<inter> cube n = cube n - (s \<inter> cube n)" by auto |
|
120 show "gmeasurable ((UNIV - s) \<inter> cube n)" unfolding * |
|
121 apply(rule gmeasurable_diff) using assms unfolding lmeasurable_def by auto |
|
122 qed |
|
123 |
|
124 lemma lmeasurable_finite_unions: |
|
125 assumes "finite f" "\<And>s. s \<in> f \<Longrightarrow> lmeasurable s" |
|
126 shows "lmeasurable (\<Union> f)" unfolding lmeasurable_def |
|
127 proof fix n::nat have *:"(\<Union>f \<inter> cube n) = \<Union>{x \<inter> cube n | x . x\<in>f}" by auto |
|
128 show "gmeasurable (\<Union>f \<inter> cube n)" unfolding * |
|
129 apply(rule gmeasurable_finite_unions) unfolding simple_image |
|
130 using assms unfolding lmeasurable_def by auto |
|
131 qed |
|
132 |
|
133 lemma negligible_imp_lmeasurable[dest]: fixes s::"'a::ordered_euclidean_space set" |
|
134 assumes "negligible s" shows "lmeasurable s" |
|
135 unfolding lmeasurable_def |
|
136 proof case goal1 |
|
137 have *:"\<And>x. (if x \<in> cube n then indicator s x else 0) = (if x \<in> s \<inter> cube n then 1 else 0)" |
|
138 unfolding indicator_def_raw by auto |
|
139 note assms[unfolded negligible_def,rule_format,of "(\<chi>\<chi> i. - real n)::'a" "\<chi>\<chi> i. real n"] |
|
140 thus ?case apply-apply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def |
|
141 apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric] |
|
142 apply(subst has_integral_restrict_univ[THEN sym]) unfolding * . |
|
143 qed |
|
144 |
|
145 |
|
146 section {* The Lebesgue Measure *} |
|
147 |
|
148 definition has_lmeasure (infixr "has'_lmeasure" 80) where |
|
149 "s has_lmeasure m \<equiv> lmeasurable s \<and> ((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially" |
|
150 |
|
151 lemma has_lmeasureD: assumes "s has_lmeasure m" |
|
152 shows "lmeasurable s" "gmeasurable (s \<inter> cube n)" |
|
153 "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially" |
|
154 using assms unfolding has_lmeasure_def lmeasurable_def by auto |
|
155 |
|
156 lemma has_lmeasureI: assumes "lmeasurable s" "((\<lambda>n. Real (gmeasure (s \<inter> cube n))) ---> m) sequentially" |
|
157 shows "s has_lmeasure m" using assms unfolding has_lmeasure_def by auto |
|
158 |
|
159 definition lmeasure where |
|
160 "lmeasure s \<equiv> SOME m. s has_lmeasure m" |
|
161 |
|
162 lemma has_lmeasure_has_gmeasure: assumes "s has_lmeasure (Real m)" "m\<ge>0" |
|
163 shows "s has_gmeasure m" |
|
164 proof- note s = has_lmeasureD[OF assms(1)] |
|
165 have *:"(\<lambda>n. (gmeasure (s \<inter> cube n))) ----> m" |
|
166 using s(3) apply(subst (asm) lim_Real) using s(2) assms(2) by auto |
|
167 |
|
168 have "(\<lambda>x. if x \<in> s then 1 else (0::real)) integrable_on UNIV \<and> |
|
169 (\<lambda>k. integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real))) |
|
170 ----> integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" |
|
171 proof(rule monotone_convergence_increasing) |
|
172 have "\<forall>n. gmeasure (s \<inter> cube n) \<le> m" apply(rule ccontr) unfolding not_all not_le |
|
173 proof(erule exE) fix k assume k:"m < gmeasure (s \<inter> cube k)" |
|
174 hence "gmeasure (s \<inter> cube k) - m > 0" by auto |
|
175 from *[unfolded Lim_sequentially,rule_format,OF this] guess N .. |
|
176 note this[unfolded dist_real_def,rule_format,of "N + k"] |
|
177 moreover have "gmeasure (s \<inter> cube (N + k)) \<ge> gmeasure (s \<inter> cube k)" apply- |
|
178 apply(rule measure_subset) prefer 3 using s(2) |
|
179 using cube_subset[of k "N + k"] by auto |
|
180 ultimately show False by auto |
|
181 qed |
|
182 thus *:"bounded {integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)) |k. True}" |
|
183 unfolding integral_measure_univ[OF s(2)] bounded_def apply- |
|
184 apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def |
|
185 by (auto simp: measure_pos_le) |
|
186 |
|
187 show "\<forall>k. (\<lambda>x. if x \<in> s \<inter> cube k then (1::real) else 0) integrable_on UNIV" |
|
188 unfolding integrable_restrict_univ |
|
189 using s(2) unfolding gmeasurable_def has_gmeasure_def by auto |
|
190 have *:"\<And>n. n \<le> Suc n" by auto |
|
191 show "\<forall>k. \<forall>x\<in>UNIV. (if x \<in> s \<inter> cube k then 1 else 0) \<le> (if x \<in> s \<inter> cube (Suc k) then 1 else (0::real))" |
|
192 using cube_subset[OF *] by fastsimp |
|
193 show "\<forall>x\<in>UNIV. (\<lambda>k. if x \<in> s \<inter> cube k then 1 else 0) ----> (if x \<in> s then 1 else (0::real))" |
|
194 unfolding Lim_sequentially |
|
195 proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this |
|
196 show ?case apply(rule_tac x=N in exI) |
|
197 proof safe case goal1 |
|
198 have "x \<in> cube n" using cube_subset[OF goal1] N |
|
199 using ball_subset_cube[of N] by(auto simp: dist_norm) |
|
200 thus ?case using `e>0` by auto |
|
201 qed |
|
202 qed |
|
203 qed note ** = conjunctD2[OF this] |
|
204 hence *:"m = integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" apply- |
|
205 apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s(2)] using * . |
|
206 show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto |
|
207 qed |
|
208 |
|
209 lemma has_lmeasure_unique: "s has_lmeasure m1 \<Longrightarrow> s has_lmeasure m2 \<Longrightarrow> m1 = m2" |
|
210 unfolding has_lmeasure_def apply(rule Lim_unique) using trivial_limit_sequentially by auto |
|
211 |
|
212 lemma lmeasure_unique[intro]: assumes "A has_lmeasure m" shows "lmeasure A = m" |
|
213 using assms unfolding lmeasure_def lmeasurable_def apply- |
|
214 apply(rule some_equality) defer apply(rule has_lmeasure_unique) by auto |
|
215 |
|
216 lemma glmeasurable_finite: assumes "lmeasurable s" "lmeasure s \<noteq> \<omega>" |
|
217 shows "gmeasurable s" |
|
218 proof- have "\<exists>B. \<forall>n. gmeasure (s \<inter> cube n) \<le> B" |
|
219 proof(rule ccontr) case goal1 |
|
220 note as = this[unfolded not_ex not_all not_le] |
|
221 have "s has_lmeasure \<omega>" apply- apply(rule has_lmeasureI[OF assms(1)]) |
|
222 unfolding Lim_omega |
|
223 proof fix B::real |
|
224 from as[rule_format,of B] guess N .. note N = this |
|
225 have "\<And>n. N \<le> n \<Longrightarrow> B \<le> gmeasure (s \<inter> cube n)" |
|
226 apply(rule order_trans[where y="gmeasure (s \<inter> cube N)"]) defer |
|
227 apply(rule measure_subset) prefer 3 |
|
228 using cube_subset N assms(1)[unfolded lmeasurable_def] by auto |
|
229 thus "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (s \<inter> cube n))" apply- |
|
230 apply(subst Real_max') apply(rule_tac x=N in exI,safe) |
|
231 unfolding pinfreal_less_eq apply(subst if_P) by auto |
|
232 qed note lmeasure_unique[OF this] |
|
233 thus False using assms(2) by auto |
|
234 qed then guess B .. note B=this |
|
235 |
|
236 show ?thesis apply(rule gmeasurable_nested_unions[of "\<lambda>n. s \<inter> cube n", |
|
237 unfolded Union_inter_cube,THEN conjunct1, where B1=B]) |
|
238 proof- fix n::nat |
|
239 show " gmeasurable (s \<inter> cube n)" using assms by auto |
|
240 show "gmeasure (s \<inter> cube n) \<le> B" using B by auto |
|
241 show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" |
|
242 by (rule Int_mono) (simp_all add: cube_subset) |
|
243 qed |
|
244 qed |
|
245 |
|
246 lemma lmeasure_empty[intro]:"lmeasure {} = 0" |
|
247 apply(rule lmeasure_unique) |
|
248 unfolding has_lmeasure_def by auto |
|
249 |
|
250 lemma lmeasurableI[dest]:"s has_lmeasure m \<Longrightarrow> lmeasurable s" |
|
251 unfolding has_lmeasure_def by auto |
|
252 |
|
253 lemma has_gmeasure_has_lmeasure: assumes "s has_gmeasure m" |
|
254 shows "s has_lmeasure (Real m)" |
|
255 proof- have gmea:"gmeasurable s" using assms by auto |
|
256 have m:"m \<ge> 0" using assms by auto |
|
257 have *:"m = gmeasure (\<Union>{s \<inter> cube n |n. n \<in> UNIV})" unfolding Union_inter_cube |
|
258 using assms by(rule measure_unique[THEN sym]) |
|
259 show ?thesis unfolding has_lmeasure_def |
|
260 apply(rule,rule measurable_imp_lmeasurable[OF gmea]) |
|
261 apply(subst lim_Real) apply(rule,rule,rule m) unfolding * |
|
262 apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"]) |
|
263 proof- fix n::nat show *:"gmeasurable (s \<inter> cube n)" |
|
264 using gmeasurable_inter[OF gmea gmeasurable_cube] . |
|
265 show "gmeasure (s \<inter> cube n) \<le> gmeasure s" apply(rule measure_subset) |
|
266 apply(rule * gmea)+ by auto |
|
267 show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" using cube_subset[of n "Suc n"] by auto |
|
268 qed |
|
269 qed |
|
270 |
|
271 lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)" |
|
272 proof- note has_gmeasure_measureI[OF assms] |
|
273 note has_gmeasure_has_lmeasure[OF this] |
|
274 thus ?thesis by(rule lmeasure_unique) |
|
275 qed |
|
276 |
|
277 lemma has_lmeasure_lmeasure: "lmeasurable s \<longleftrightarrow> s has_lmeasure (lmeasure s)" (is "?l = ?r") |
|
278 proof assume ?l let ?f = "\<lambda>n. Real (gmeasure (s \<inter> cube n))" |
|
279 have "\<forall>n m. n\<ge>m \<longrightarrow> ?f n \<ge> ?f m" unfolding pinfreal_less_eq apply safe |
|
280 apply(subst if_P) defer apply(rule measure_subset) prefer 3 |
|
281 apply(drule cube_subset) using `?l` by auto |
|
282 from lim_pinfreal_increasing[OF this] guess l . note l=this |
|
283 hence "s has_lmeasure l" using `?l` apply-apply(rule has_lmeasureI) by auto |
|
284 thus ?r using lmeasure_unique by auto |
|
285 next assume ?r thus ?l unfolding has_lmeasure_def by auto |
|
286 qed |
|
287 |
|
288 lemma lmeasure_subset[dest]: assumes "lmeasurable s" "lmeasurable t" "s \<subseteq> t" |
|
289 shows "lmeasure s \<le> lmeasure t" |
|
290 proof(cases "lmeasure t = \<omega>") |
|
291 case False have som:"lmeasure s \<noteq> \<omega>" |
|
292 proof(rule ccontr,unfold not_not) assume as:"lmeasure s = \<omega>" |
|
293 have "t has_lmeasure \<omega>" using assms(2) apply(rule has_lmeasureI) |
|
294 unfolding Lim_omega |
|
295 proof case goal1 |
|
296 note assms(1)[unfolded has_lmeasure_lmeasure] |
|
297 note has_lmeasureD(3)[OF this,unfolded as Lim_omega,rule_format,of B] |
|
298 then guess N .. note N = this |
|
299 show ?case apply(rule_tac x=N in exI) apply safe |
|
300 apply(rule order_trans) apply(rule N[rule_format],assumption) |
|
301 unfolding pinfreal_less_eq apply(subst if_P)defer |
|
302 apply(rule measure_subset) using assms by auto |
|
303 qed |
|
304 thus False using lmeasure_unique False by auto |
|
305 qed |
|
306 |
|
307 note assms(1)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this] |
|
308 hence "(\<lambda>n. Real (gmeasure (s \<inter> cube n))) ----> Real (real (lmeasure s))" |
|
309 unfolding Real_real'[OF som] . |
|
310 hence l1:"(\<lambda>n. gmeasure (s \<inter> cube n)) ----> real (lmeasure s)" |
|
311 apply-apply(subst(asm) lim_Real) by auto |
|
312 |
|
313 note assms(2)[unfolded has_lmeasure_lmeasure] note has_lmeasureD(3)[OF this] |
|
314 hence "(\<lambda>n. Real (gmeasure (t \<inter> cube n))) ----> Real (real (lmeasure t))" |
|
315 unfolding Real_real'[OF False] . |
|
316 hence l2:"(\<lambda>n. gmeasure (t \<inter> cube n)) ----> real (lmeasure t)" |
|
317 apply-apply(subst(asm) lim_Real) by auto |
|
318 |
|
319 have "real (lmeasure s) \<le> real (lmeasure t)" apply(rule LIMSEQ_le[OF l1 l2]) |
|
320 apply(rule_tac x=0 in exI,safe) apply(rule measure_subset) using assms by auto |
|
321 hence "Real (real (lmeasure s)) \<le> Real (real (lmeasure t))" |
|
322 unfolding pinfreal_less_eq by auto |
|
323 thus ?thesis unfolding Real_real'[OF som] Real_real'[OF False] . |
|
324 qed auto |
|
325 |
|
326 lemma has_lmeasure_negligible_unions_image: |
|
327 assumes "finite s" "\<And>x. x \<in> s ==> lmeasurable(f x)" |
|
328 "\<And>x y. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x \<noteq> y \<Longrightarrow> negligible((f x) \<inter> (f y))" |
|
329 shows "(\<Union> (f ` s)) has_lmeasure (setsum (\<lambda>x. lmeasure(f x)) s)" |
|
330 unfolding has_lmeasure_def |
|
331 proof show lmeaf:"lmeasurable (\<Union>f ` s)" apply(rule lmeasurable_finite_unions) |
|
332 using assms(1-2) by auto |
|
333 show "(\<lambda>n. Real (gmeasure (\<Union>f ` s \<inter> cube n))) ----> (\<Sum>x\<in>s. lmeasure (f x))" (is ?l) |
|
334 proof(cases "\<exists>x\<in>s. lmeasure (f x) = \<omega>") |
|
335 case False hence *:"(\<Sum>x\<in>s. lmeasure (f x)) \<noteq> \<omega>" apply- |
|
336 apply(rule setsum_neq_omega) using assms(1) by auto |
|
337 have gmea:"\<And>x. x\<in>s \<Longrightarrow> gmeasurable (f x)" apply(rule glmeasurable_finite) using False assms(2) by auto |
|
338 have "(\<Sum>x\<in>s. lmeasure (f x)) = (\<Sum>x\<in>s. Real (gmeasure (f x)))" apply(rule setsum_cong2) |
|
339 apply(rule gmeasure_lmeasure) using False assms(2) gmea by auto |
|
340 also have "... = Real (\<Sum>x\<in>s. (gmeasure (f x)))" apply(rule setsum_Real) by auto |
|
341 finally have sum:"(\<Sum>x\<in>s. lmeasure (f x)) = Real (\<Sum>x\<in>s. gmeasure (f x))" . |
|
342 have sum_0:"(\<Sum>x\<in>s. gmeasure (f x)) \<ge> 0" apply(rule setsum_nonneg) by auto |
|
343 have int_un:"\<Union>f ` s has_gmeasure (\<Sum>x\<in>s. gmeasure (f x))" |
|
344 apply(rule has_gmeasure_negligible_unions_image) using assms gmea by auto |
|
345 |
|
346 have unun:"\<Union>{\<Union>f ` s \<inter> cube n |n. n \<in> UNIV} = \<Union>f ` s" unfolding simple_image |
|
347 proof safe fix x y assume as:"x \<in> f y" "y \<in> s" |
|
348 from mem_big_cube[of x] guess n . note n=this |
|
349 thus "x \<in> \<Union>range (\<lambda>n. \<Union>f ` s \<inter> cube n)" unfolding Union_iff |
|
350 apply-apply(rule_tac x="\<Union>f ` s \<inter> cube n" in bexI) using as by auto |
|
351 qed |
|
352 show ?l apply(subst Real_real'[OF *,THEN sym])apply(subst lim_Real) |
|
353 apply rule apply rule unfolding sum real_Real if_P[OF sum_0] apply(rule sum_0) |
|
354 unfolding measure_unique[OF int_un,THEN sym] apply(subst(2) unun[THEN sym]) |
|
355 apply(rule has_gmeasure_nested_unions[THEN conjunct2]) |
|
356 proof- fix n::nat |
|
357 show *:"gmeasurable (\<Union>f ` s \<inter> cube n)" using lmeaf unfolding lmeasurable_def by auto |
|
358 thus "gmeasure (\<Union>f ` s \<inter> cube n) \<le> gmeasure (\<Union>f ` s)" |
|
359 apply(rule measure_subset) using int_un by auto |
|
360 show "\<Union>f ` s \<inter> cube n \<subseteq> \<Union>f ` s \<inter> cube (Suc n)" |
|
361 using cube_subset[of n "Suc n"] by auto |
|
362 qed |
|
363 |
|
364 next case True then guess X .. note X=this |
|
365 hence sum:"(\<Sum>x\<in>s. lmeasure (f x)) = \<omega>" using setsum_\<omega>[THEN iffD2, of s] assms by fastsimp |
|
366 show ?l unfolding sum Lim_omega |
|
367 proof fix B::real |
|
368 have Xm:"(f X) has_lmeasure \<omega>" using X by (metis assms(2) has_lmeasure_lmeasure) |
|
369 note this[unfolded has_lmeasure_def,THEN conjunct2, unfolded Lim_omega] |
|
370 from this[rule_format,of B] guess N .. note N=this[rule_format] |
|
371 show "\<exists>N. \<forall>n\<ge>N. Real B \<le> Real (gmeasure (\<Union>f ` s \<inter> cube n))" |
|
372 apply(rule_tac x=N in exI) |
|
373 proof safe case goal1 show ?case apply(rule order_trans[OF N[OF goal1]]) |
|
374 unfolding pinfreal_less_eq apply(subst if_P) defer |
|
375 apply(rule measure_subset) using has_lmeasureD(2)[OF Xm] |
|
376 using lmeaf unfolding lmeasurable_def using X(1) by auto |
|
377 qed qed qed qed |
|
378 |
|
379 lemma has_lmeasure_negligible_unions: |
|
380 assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)" |
|
381 "\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> negligible (s\<inter>t)" |
|
382 shows "(\<Union> f) has_lmeasure (setsum m f)" |
|
383 proof- have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2) |
|
384 apply(subst lmeasure_unique[OF assms(2)]) by auto |
|
385 show ?thesis unfolding * |
|
386 apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply]) |
|
387 using assms by auto |
|
388 qed |
|
389 |
|
390 lemma has_lmeasure_disjoint_unions: |
|
391 assumes"finite f" "\<And>s. s \<in> f ==> s has_lmeasure (m s)" |
|
392 "\<And>s t. s \<in> f \<Longrightarrow> t \<in> f \<Longrightarrow> s \<noteq> t ==> s \<inter> t = {}" |
|
393 shows "(\<Union> f) has_lmeasure (setsum m f)" |
|
394 proof- have *:"setsum m f = setsum lmeasure f" apply(rule setsum_cong2) |
|
395 apply(subst lmeasure_unique[OF assms(2)]) by auto |
|
396 show ?thesis unfolding * |
|
397 apply(rule has_lmeasure_negligible_unions_image[where s=f and f=id,unfolded image_id id_apply]) |
|
398 using assms by auto |
|
399 qed |
|
400 |
|
401 lemma has_lmeasure_nested_unions: |
|
402 assumes "\<And>n. lmeasurable(s n)" "\<And>n. s(n) \<subseteq> s(Suc n)" |
|
403 shows "lmeasurable(\<Union> { s n | n. n \<in> UNIV }) \<and> |
|
404 (\<lambda>n. lmeasure(s n)) ----> lmeasure(\<Union> { s(n) | n. n \<in> UNIV })" (is "?mea \<and> ?lim") |
|
405 proof- have cube:"\<And>m. \<Union> { s(n) | n. n \<in> UNIV } \<inter> cube m = \<Union> { s(n) \<inter> cube m | n. n \<in> UNIV }" by blast |
|
406 have 3:"\<And>n. \<forall>m\<ge>n. s n \<subseteq> s m" apply(rule transitive_stepwise_le) using assms(2) by auto |
|
407 have mea:"?mea" unfolding lmeasurable_def cube apply rule |
|
408 apply(rule_tac B1="gmeasure (cube n)" in has_gmeasure_nested_unions[THEN conjunct1]) |
|
409 prefer 3 apply rule using assms(1) unfolding lmeasurable_def |
|
410 by(auto intro!:assms(2)[unfolded subset_eq,rule_format]) |
|
411 show ?thesis apply(rule,rule mea) |
|
412 proof(cases "lmeasure(\<Union> { s(n) | n. n \<in> UNIV }) = \<omega>") |
|
413 case True show ?lim unfolding True Lim_omega |
|
414 proof(rule ccontr) case goal1 note this[unfolded not_all not_ex] |
|
415 hence "\<exists>B. \<forall>n. \<exists>m\<ge>n. Real B > lmeasure (s m)" by(auto simp add:not_le) |
|
416 from this guess B .. note B=this[rule_format] |
|
417 |
|
418 have "\<forall>n. gmeasurable (s n) \<and> gmeasure (s n) \<le> max B 0" |
|
419 proof safe fix n::nat from B[of n] guess m .. note m=this |
|
420 hence *:"lmeasure (s n) < Real B" apply-apply(rule le_less_trans) |
|
421 apply(rule lmeasure_subset[OF assms(1,1)]) apply(rule 3[rule_format]) by auto |
|
422 thus **:"gmeasurable (s n)" apply-apply(rule glmeasurable_finite[OF assms(1)]) by auto |
|
423 thus "gmeasure (s n) \<le> max B 0" using * unfolding gmeasure_lmeasure[OF **] Real_max'[of B] |
|
424 unfolding pinfreal_less apply- apply(subst(asm) if_P) by auto |
|
425 qed |
|
426 hence "\<And>n. gmeasurable (s n)" "\<And>n. gmeasure (s n) \<le> max B 0" by auto |
|
427 note g = conjunctD2[OF has_gmeasure_nested_unions[of s, OF this assms(2)]] |
|
428 show False using True unfolding gmeasure_lmeasure[OF g(1)] by auto |
|
429 qed |
|
430 next let ?B = "lmeasure (\<Union>{s n |n. n \<in> UNIV})" |
|
431 case False note gmea_lim = glmeasurable_finite[OF mea this] |
|
432 have ls:"\<And>n. lmeasure (s n) \<le> lmeasure (\<Union>{s n |n. n \<in> UNIV})" |
|
433 apply(rule lmeasure_subset) using assms(1) mea by auto |
|
434 have "\<And>n. lmeasure (s n) \<noteq> \<omega>" |
|
435 proof(rule ccontr,safe) case goal1 |
|
436 show False using False ls[of n] unfolding goal1 by auto |
|
437 qed |
|
438 note gmea = glmeasurable_finite[OF assms(1) this] |
|
439 |
|
440 have "\<And>n. gmeasure (s n) \<le> real ?B" unfolding gmeasure_lmeasure[OF gmea_lim] |
|
441 unfolding real_Real apply(subst if_P,rule) apply(rule measure_subset) |
|
442 using gmea gmea_lim by auto |
|
443 note has_gmeasure_nested_unions[of s, OF gmea this assms(2)] |
|
444 thus ?lim unfolding gmeasure_lmeasure[OF gmea] gmeasure_lmeasure[OF gmea_lim] |
|
445 apply-apply(subst lim_Real) by auto |
|
446 qed |
|
447 qed |
|
448 |
|
449 lemma has_lmeasure_countable_negligible_unions: |
|
450 assumes "\<And>n. lmeasurable(s n)" "\<And>m n. m \<noteq> n \<Longrightarrow> negligible(s m \<inter> s n)" |
|
451 shows "(\<lambda>m. setsum (\<lambda>n. lmeasure(s n)) {..m}) ----> (lmeasure(\<Union> { s(n) |n. n \<in> UNIV }))" |
|
452 proof- have *:"\<And>n. (\<Union> (s ` {0..n})) has_lmeasure (setsum (\<lambda>k. lmeasure(s k)) {0..n})" |
|
453 apply(rule has_lmeasure_negligible_unions_image) using assms by auto |
|
454 have **:"(\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV}) = (\<Union>{s n |n. n \<in> UNIV})" unfolding simple_image by fastsimp |
|
455 have "lmeasurable (\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV}) \<and> |
|
456 (\<lambda>n. lmeasure (\<Union>(s ` {0..n}))) ----> lmeasure (\<Union>{\<Union>s ` {0..n} |n. n \<in> UNIV})" |
|
457 apply(rule has_lmeasure_nested_unions) apply(rule has_lmeasureD(1)[OF *]) |
|
458 apply(rule Union_mono,rule image_mono) by auto |
|
459 note lem = conjunctD2[OF this,unfolded **] |
|
460 show ?thesis using lem(2) unfolding lmeasure_unique[OF *] unfolding atLeast0AtMost . |
|
461 qed |
|
462 |
|
463 lemma lmeasure_eq_0: assumes "negligible s" shows "lmeasure s = 0" |
|
464 proof- note mea=negligible_imp_lmeasurable[OF assms] |
|
465 have *:"\<And>n. (gmeasure (s \<inter> cube n)) = 0" |
|
466 unfolding gmeasurable_measure_eq_0[OF mea[unfolded lmeasurable_def,rule_format]] |
|
467 using assms by auto |
|
468 show ?thesis |
|
469 apply(rule lmeasure_unique) unfolding has_lmeasure_def |
|
470 apply(rule,rule mea) unfolding * by auto |
|
471 qed |
|
472 |
|
473 lemma negligible_img_gmeasurable: fixes s::"'a::ordered_euclidean_space set" |
|
474 assumes "negligible s" shows "gmeasurable s" |
|
475 apply(rule glmeasurable_finite) |
|
476 using lmeasure_eq_0[OF assms] negligible_imp_lmeasurable[OF assms] by auto |
|
477 |
|
478 |
|
479 |
|
480 |
|
481 section {* Instantiation of _::euclidean_space as measure_space *} |
|
482 |
|
483 definition lebesgue_space :: "'a::ordered_euclidean_space algebra" where |
|
484 "lebesgue_space = \<lparr> space = UNIV, sets = lmeasurable \<rparr>" |
|
485 |
|
486 lemma lebesgue_measurable[simp]:"A \<in> sets lebesgue_space \<longleftrightarrow> lmeasurable A" |
|
487 unfolding lebesgue_space_def by(auto simp: mem_def) |
|
488 |
|
489 lemma mem_gmeasurable[simp]: "A \<in> gmeasurable \<longleftrightarrow> gmeasurable A" |
|
490 unfolding mem_def .. |
|
491 |
|
492 interpretation lebesgue: measure_space lebesgue_space lmeasure |
|
493 apply(intro_locales) unfolding measure_space_axioms_def countably_additive_def |
|
494 unfolding sigma_algebra_axioms_def algebra_def |
|
495 unfolding lebesgue_measurable |
|
496 proof safe |
|
497 fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space" "disjoint_family A" |
|
498 "lmeasurable (UNION UNIV A)" |
|
499 have *:"UNION UNIV A = \<Union>range A" by auto |
|
500 show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (UNION UNIV A)" |
|
501 unfolding psuminf_def apply(rule SUP_Lim_pinfreal) |
|
502 proof- fix n m::nat assume mn:"m\<le>n" |
|
503 have *:"\<And>m. (\<Sum>n<m. lmeasure (A n)) = lmeasure (\<Union>A ` {..<m})" |
|
504 apply(subst lmeasure_unique[OF has_lmeasure_negligible_unions[where m=lmeasure]]) |
|
505 apply(rule finite_imageI) apply rule apply(subst has_lmeasure_lmeasure[THEN sym]) |
|
506 proof- fix m::nat |
|
507 show "(\<Sum>n<m. lmeasure (A n)) = setsum lmeasure (A ` {..<m})" |
|
508 apply(subst setsum_reindex_nonzero) unfolding o_def apply rule |
|
509 apply(rule lmeasure_eq_0) using as(2) unfolding disjoint_family_on_def |
|
510 apply(erule_tac x=x in ballE,safe,erule_tac x=y in ballE) by auto |
|
511 next fix m s assume "s \<in> A ` {..<m}" |
|
512 hence "s \<in> range A" by auto thus "lmeasurable s" using as(1) by fastsimp |
|
513 next fix m s t assume st:"s \<in> A ` {..<m}" "t \<in> A ` {..<m}" "s \<noteq> t" |
|
514 from st(1-2) guess sa ta unfolding image_iff apply-by(erule bexE)+ note a=this |
|
515 from st(3) have "sa \<noteq> ta" unfolding a by auto |
|
516 thus "negligible (s \<inter> t)" |
|
517 using as(2) unfolding disjoint_family_on_def a |
|
518 apply(erule_tac x=sa in ballE,erule_tac x=ta in ballE) by auto |
|
519 qed |
|
520 |
|
521 have "\<And>m. lmeasurable (\<Union>A ` {..<m})" apply(rule lmeasurable_finite_unions) |
|
522 apply(rule finite_imageI,rule) using as(1) by fastsimp |
|
523 from this this show "(\<Sum>n<m. lmeasure (A n)) \<le> (\<Sum>n<n. lmeasure (A n))" unfolding * |
|
524 apply(rule lmeasure_subset) apply(rule Union_mono) apply(rule image_mono) using mn by auto |
|
525 |
|
526 next have *:"UNION UNIV A = \<Union>{A n |n. n \<in> UNIV}" by auto |
|
527 show "(\<lambda>n. \<Sum>n<n. lmeasure (A n)) ----> lmeasure (UNION UNIV A)" |
|
528 apply(rule LIMSEQ_imp_Suc) unfolding lessThan_Suc_atMost * |
|
529 apply(rule has_lmeasure_countable_negligible_unions) |
|
530 using as unfolding disjoint_family_on_def subset_eq by auto |
|
531 qed |
|
532 |
|
533 next show "lmeasure {} = 0" by auto |
|
534 next fix A::"nat => _" assume as:"range A \<subseteq> sets lebesgue_space" |
|
535 have *:"UNION UNIV A = (\<Union>{A n |n. n \<in> UNIV})" unfolding simple_image by auto |
|
536 show "lmeasurable (UNION UNIV A)" unfolding * using as unfolding subset_eq |
|
537 using lmeasurable_countable_unions_strong[of A] by auto |
|
538 qed(auto simp: lebesgue_space_def mem_def) |
|
539 |
|
540 |
|
541 |
|
542 lemma lmeasurbale_closed_interval[intro]: |
|
543 "lmeasurable {a..b::'a::ordered_euclidean_space}" |
|
544 unfolding lmeasurable_def cube_def inter_interval by auto |
|
545 |
|
546 lemma space_lebesgue_space[simp]:"space lebesgue_space = UNIV" |
|
547 unfolding lebesgue_space_def by auto |
|
548 |
|
549 abbreviation "gintegral \<equiv> Integration.integral" |
|
550 |
|
551 lemma lebesgue_simple_function_indicator: |
|
552 fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal" |
|
553 assumes f:"lebesgue.simple_function f" |
|
554 shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))" |
|
555 apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto |
|
556 |
|
557 lemma lmeasure_gmeasure: |
|
558 "gmeasurable s \<Longrightarrow> gmeasure s = real (lmeasure s)" |
|
559 apply(subst gmeasure_lmeasure) by auto |
|
560 |
|
561 lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \<noteq> \<omega>" |
|
562 using gmeasure_lmeasure[OF assms] by auto |
|
563 |
|
564 lemma negligible_lmeasure: assumes "lmeasurable s" |
|
565 shows "lmeasure s = 0 \<longleftrightarrow> negligible s" (is "?l = ?r") |
|
566 proof assume ?l |
|
567 hence *:"gmeasurable s" using glmeasurable_finite[of s] assms by auto |
|
568 show ?r unfolding gmeasurable_measure_eq_0[THEN sym,OF *] |
|
569 unfolding lmeasure_gmeasure[OF *] using `?l` by auto |
|
570 next assume ?r |
|
571 note g=negligible_img_gmeasurable[OF this] and measure_eq_0[OF this] |
|
572 hence "real (lmeasure s) = 0" using lmeasure_gmeasure[of s] by auto |
|
573 thus ?l using lmeasure_finite[OF g] apply- apply(rule real_0_imp_eq_0) by auto |
|
574 qed |
|
575 |
|
576 end |