author | hoelzl |
Fri, 23 Sep 2016 10:26:04 +0200 | |
changeset 63940 | 0d82c4c94014 |
parent 63627 | 6ddb43c6b711 |
child 63941 | f353674c2528 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Complete_Measure.thy |
40859 | 2 |
Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen |
3 |
*) |
|
41983 | 4 |
|
40859 | 5 |
theory Complete_Measure |
63626
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
62975
diff
changeset
|
6 |
imports Bochner_Integration |
40859 | 7 |
begin |
8 |
||
63940
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
9 |
locale complete_measure = |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
10 |
fixes M :: "'a measure" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
11 |
assumes complete: "\<And>A B. B \<subseteq> A \<Longrightarrow> A \<in> null_sets M \<Longrightarrow> B \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
12 |
|
47694 | 13 |
definition |
14 |
"split_completion M A p = (if A \<in> sets M then p = (A, {}) else |
|
15 |
\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and> fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets M)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41097
diff
changeset
|
16 |
|
47694 | 17 |
definition |
18 |
"main_part M A = fst (Eps (split_completion M A))" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41097
diff
changeset
|
19 |
|
47694 | 20 |
definition |
21 |
"null_part M A = snd (Eps (split_completion M A))" |
|
40859 | 22 |
|
47694 | 23 |
definition completion :: "'a measure \<Rightarrow> 'a measure" where |
24 |
"completion M = measure_of (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } |
|
25 |
(emeasure M \<circ> main_part M)" |
|
40859 | 26 |
|
47694 | 27 |
lemma completion_into_space: |
28 |
"{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)" |
|
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
47694
diff
changeset
|
29 |
using sets.sets_into_space by auto |
40859 | 30 |
|
47694 | 31 |
lemma space_completion[simp]: "space (completion M) = space M" |
32 |
unfolding completion_def using space_measure_of[OF completion_into_space] by simp |
|
40859 | 33 |
|
47694 | 34 |
lemma completionI: |
35 |
assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" |
|
36 |
shows "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" |
|
40859 | 37 |
using assms by auto |
38 |
||
47694 | 39 |
lemma completionE: |
40 |
assumes "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" |
|
41 |
obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" |
|
42 |
using assms by auto |
|
43 |
||
44 |
lemma sigma_algebra_completion: |
|
45 |
"sigma_algebra (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" |
|
46 |
(is "sigma_algebra _ ?A") |
|
47 |
unfolding sigma_algebra_iff2 |
|
48 |
proof (intro conjI ballI allI impI) |
|
49 |
show "?A \<subseteq> Pow (space M)" |
|
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
47694
diff
changeset
|
50 |
using sets.sets_into_space by auto |
40859 | 51 |
next |
47694 | 52 |
show "{} \<in> ?A" by auto |
40859 | 53 |
next |
47694 | 54 |
let ?C = "space M" |
55 |
fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' . |
|
56 |
then show "space M - A \<in> ?A" |
|
57 |
by (intro completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"]) auto |
|
58 |
next |
|
59 |
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A" |
|
60 |
then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'" |
|
61 |
by (auto simp: image_subset_iff) |
|
40859 | 62 |
from choice[OF this] guess S .. |
63 |
from choice[OF this] guess N .. |
|
64 |
from choice[OF this] guess N' .. |
|
47694 | 65 |
then show "UNION UNIV A \<in> ?A" |
40859 | 66 |
using null_sets_UN[of N'] |
47694 | 67 |
by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto |
68 |
qed |
|
69 |
||
70 |
lemma sets_completion: |
|
71 |
"sets (completion M) = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }" |
|
72 |
using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] by (simp add: completion_def) |
|
73 |
||
74 |
lemma sets_completionE: |
|
75 |
assumes "A \<in> sets (completion M)" |
|
76 |
obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" |
|
77 |
using assms unfolding sets_completion by auto |
|
78 |
||
79 |
lemma sets_completionI: |
|
80 |
assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M" |
|
81 |
shows "A \<in> sets (completion M)" |
|
82 |
using assms unfolding sets_completion by auto |
|
83 |
||
84 |
lemma sets_completionI_sets[intro, simp]: |
|
85 |
"A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)" |
|
86 |
unfolding sets_completion by force |
|
40859 | 87 |
|
47694 | 88 |
lemma null_sets_completion: |
89 |
assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)" |
|
90 |
using assms by (intro sets_completionI[of N "{}" N N']) auto |
|
91 |
||
92 |
lemma split_completion: |
|
93 |
assumes "A \<in> sets (completion M)" |
|
94 |
shows "split_completion M A (main_part M A, null_part M A)" |
|
95 |
proof cases |
|
96 |
assume "A \<in> sets M" then show ?thesis |
|
97 |
by (simp add: split_completion_def[abs_def] main_part_def null_part_def) |
|
98 |
next |
|
99 |
assume nA: "A \<notin> sets M" |
|
100 |
show ?thesis |
|
101 |
unfolding main_part_def null_part_def if_not_P[OF nA] |
|
102 |
proof (rule someI2_ex) |
|
103 |
from assms[THEN sets_completionE] guess S N N' . note A = this |
|
104 |
let ?P = "(S, N - S)" |
|
105 |
show "\<exists>p. split_completion M A p" |
|
106 |
unfolding split_completion_def if_not_P[OF nA] using A |
|
107 |
proof (intro exI conjI) |
|
108 |
show "A = fst ?P \<union> snd ?P" using A by auto |
|
109 |
show "snd ?P \<subseteq> N'" using A by auto |
|
110 |
qed auto |
|
40859 | 111 |
qed auto |
47694 | 112 |
qed |
40859 | 113 |
|
47694 | 114 |
lemma |
115 |
assumes "S \<in> sets (completion M)" |
|
116 |
shows main_part_sets[intro, simp]: "main_part M S \<in> sets M" |
|
117 |
and main_part_null_part_Un[simp]: "main_part M S \<union> null_part M S = S" |
|
118 |
and main_part_null_part_Int[simp]: "main_part M S \<inter> null_part M S = {}" |
|
119 |
using split_completion[OF assms] |
|
62390 | 120 |
by (auto simp: split_completion_def split: if_split_asm) |
40859 | 121 |
|
47694 | 122 |
lemma main_part[simp]: "S \<in> sets M \<Longrightarrow> main_part M S = S" |
123 |
using split_completion[of S M] |
|
62390 | 124 |
by (auto simp: split_completion_def split: if_split_asm) |
40859 | 125 |
|
47694 | 126 |
lemma null_part: |
127 |
assumes "S \<in> sets (completion M)" shows "\<exists>N. N\<in>null_sets M \<and> null_part M S \<subseteq> N" |
|
62390 | 128 |
using split_completion[OF assms] by (auto simp: split_completion_def split: if_split_asm) |
47694 | 129 |
|
130 |
lemma null_part_sets[intro, simp]: |
|
131 |
assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0" |
|
40859 | 132 |
proof - |
47694 | 133 |
have S: "S \<in> sets (completion M)" using assms by auto |
134 |
have "S - main_part M S \<in> sets M" using assms by auto |
|
40859 | 135 |
moreover |
136 |
from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S] |
|
47694 | 137 |
have "S - main_part M S = null_part M S" by auto |
138 |
ultimately show sets: "null_part M S \<in> sets M" by auto |
|
40859 | 139 |
from null_part[OF S] guess N .. |
47694 | 140 |
with emeasure_eq_0[of N _ "null_part M S"] sets |
141 |
show "emeasure M (null_part M S) = 0" by auto |
|
40859 | 142 |
qed |
143 |
||
47694 | 144 |
lemma emeasure_main_part_UN: |
40859 | 145 |
fixes S :: "nat \<Rightarrow> 'a set" |
47694 | 146 |
assumes "range S \<subseteq> sets (completion M)" |
147 |
shows "emeasure M (main_part M (\<Union>i. (S i))) = emeasure M (\<Union>i. main_part M (S i))" |
|
40859 | 148 |
proof - |
47694 | 149 |
have S: "\<And>i. S i \<in> sets (completion M)" using assms by auto |
150 |
then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto |
|
151 |
have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N" |
|
40859 | 152 |
using null_part[OF S] by auto |
153 |
from choice[OF this] guess N .. note N = this |
|
47694 | 154 |
then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto |
155 |
have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto |
|
40859 | 156 |
from null_part[OF this] guess N' .. note N' = this |
157 |
let ?N = "(\<Union>i. N i) \<union> N'" |
|
47694 | 158 |
have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto |
159 |
have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N" |
|
40859 | 160 |
using N' by auto |
47694 | 161 |
also have "\<dots> = (\<Union>i. main_part M (S i) \<union> null_part M (S i)) \<union> ?N" |
40859 | 162 |
unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto |
47694 | 163 |
also have "\<dots> = (\<Union>i. main_part M (S i)) \<union> ?N" |
40859 | 164 |
using N by auto |
47694 | 165 |
finally have *: "main_part M (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part M (S i)) \<union> ?N" . |
166 |
have "emeasure M (main_part M (\<Union>i. S i)) = emeasure M (main_part M (\<Union>i. S i) \<union> ?N)" |
|
167 |
using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto |
|
168 |
also have "\<dots> = emeasure M ((\<Union>i. main_part M (S i)) \<union> ?N)" |
|
40859 | 169 |
unfolding * .. |
47694 | 170 |
also have "\<dots> = emeasure M (\<Union>i. main_part M (S i))" |
171 |
using null_set S by (intro emeasure_Un_null_set) auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41097
diff
changeset
|
172 |
finally show ?thesis . |
40859 | 173 |
qed |
174 |
||
47694 | 175 |
lemma emeasure_completion[simp]: |
176 |
assumes S: "S \<in> sets (completion M)" shows "emeasure (completion M) S = emeasure M (main_part M S)" |
|
177 |
proof (subst emeasure_measure_of[OF completion_def completion_into_space]) |
|
178 |
let ?\<mu> = "emeasure M \<circ> main_part M" |
|
179 |
show "S \<in> sets (completion M)" "?\<mu> S = emeasure M (main_part M S) " using S by simp_all |
|
180 |
show "positive (sets (completion M)) ?\<mu>" |
|
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
181 |
by (simp add: positive_def) |
47694 | 182 |
show "countably_additive (sets (completion M)) ?\<mu>" |
183 |
proof (intro countably_additiveI) |
|
184 |
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (completion M)" "disjoint_family A" |
|
185 |
have "disjoint_family (\<lambda>i. main_part M (A i))" |
|
186 |
proof (intro disjoint_family_on_bisimulation[OF A(2)]) |
|
187 |
fix n m assume "A n \<inter> A m = {}" |
|
188 |
then have "(main_part M (A n) \<union> null_part M (A n)) \<inter> (main_part M (A m) \<union> null_part M (A m)) = {}" |
|
189 |
using A by (subst (1 2) main_part_null_part_Un) auto |
|
190 |
then show "main_part M (A n) \<inter> main_part M (A m) = {}" by auto |
|
191 |
qed |
|
192 |
then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))" |
|
193 |
using A by (auto intro!: suminf_emeasure) |
|
194 |
then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (UNION UNIV A)" |
|
195 |
by (simp add: completion_def emeasure_main_part_UN[OF A(1)]) |
|
196 |
qed |
|
40859 | 197 |
qed |
198 |
||
47694 | 199 |
lemma emeasure_completion_UN: |
200 |
"range S \<subseteq> sets (completion M) \<Longrightarrow> |
|
201 |
emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))" |
|
202 |
by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN) |
|
40859 | 203 |
|
47694 | 204 |
lemma emeasure_completion_Un: |
205 |
assumes S: "S \<in> sets (completion M)" and T: "T \<in> sets (completion M)" |
|
206 |
shows "emeasure (completion M) (S \<union> T) = emeasure M (main_part M S \<union> main_part M T)" |
|
207 |
proof (subst emeasure_completion) |
|
208 |
have UN: "(\<Union>i. binary (main_part M S) (main_part M T) i) = (\<Union>i. main_part M (binary S T i))" |
|
62390 | 209 |
unfolding binary_def by (auto split: if_split_asm) |
47694 | 210 |
show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)" |
211 |
using emeasure_main_part_UN[of "binary S T" M] assms |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61808
diff
changeset
|
212 |
by (simp add: range_binary_eq, simp add: Un_range_binary UN) |
47694 | 213 |
qed (auto intro: S T) |
214 |
||
215 |
lemma sets_completionI_sub: |
|
216 |
assumes N: "N' \<in> null_sets M" "N \<subseteq> N'" |
|
217 |
shows "N \<in> sets (completion M)" |
|
218 |
using assms by (intro sets_completionI[of _ "{}" N N']) auto |
|
219 |
||
220 |
lemma completion_ex_simple_function: |
|
221 |
assumes f: "simple_function (completion M) f" |
|
222 |
shows "\<exists>f'. simple_function M f' \<and> (AE x in M. f x = f' x)" |
|
40859 | 223 |
proof - |
46731 | 224 |
let ?F = "\<lambda>x. f -` {x} \<inter> space M" |
47694 | 225 |
have F: "\<And>x. ?F x \<in> sets (completion M)" and fin: "finite (f`space M)" |
226 |
using simple_functionD[OF f] simple_functionD[OF f] by simp_all |
|
227 |
have "\<forall>x. \<exists>N. N \<in> null_sets M \<and> null_part M (?F x) \<subseteq> N" |
|
40859 | 228 |
using F null_part by auto |
229 |
from choice[OF this] obtain N where |
|
47694 | 230 |
N: "\<And>x. null_part M (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets M" by auto |
46731 | 231 |
let ?N = "\<Union>x\<in>f`space M. N x" |
232 |
let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x" |
|
47694 | 233 |
have sets: "?N \<in> null_sets M" using N fin by (intro null_sets.finite_UN) auto |
40859 | 234 |
show ?thesis unfolding simple_function_def |
235 |
proof (safe intro!: exI[of _ ?f']) |
|
236 |
have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto |
|
47694 | 237 |
from finite_subset[OF this] simple_functionD(1)[OF f] |
40859 | 238 |
show "finite (?f' ` space M)" by auto |
239 |
next |
|
240 |
fix x assume "x \<in> space M" |
|
241 |
have "?f' -` {?f' x} \<inter> space M = |
|
242 |
(if x \<in> ?N then ?F undefined \<union> ?N |
|
243 |
else if f x = undefined then ?F (f x) \<union> ?N |
|
244 |
else ?F (f x) - ?N)" |
|
62390 | 245 |
using N(2) sets.sets_into_space by (auto split: if_split_asm simp: null_sets_def) |
40859 | 246 |
moreover { fix y have "?F y \<union> ?N \<in> sets M" |
247 |
proof cases |
|
248 |
assume y: "y \<in> f`space M" |
|
47694 | 249 |
have "?F y \<union> ?N = (main_part M (?F y) \<union> null_part M (?F y)) \<union> ?N" |
40859 | 250 |
using main_part_null_part_Un[OF F] by auto |
47694 | 251 |
also have "\<dots> = main_part M (?F y) \<union> ?N" |
40859 | 252 |
using y N by auto |
253 |
finally show ?thesis |
|
254 |
using F sets by auto |
|
255 |
next |
|
256 |
assume "y \<notin> f`space M" then have "?F y = {}" by auto |
|
257 |
then show ?thesis using sets by auto |
|
258 |
qed } |
|
259 |
moreover { |
|
47694 | 260 |
have "?F (f x) - ?N = main_part M (?F (f x)) \<union> null_part M (?F (f x)) - ?N" |
40859 | 261 |
using main_part_null_part_Un[OF F] by auto |
47694 | 262 |
also have "\<dots> = main_part M (?F (f x)) - ?N" |
61808 | 263 |
using N \<open>x \<in> space M\<close> by auto |
40859 | 264 |
finally have "?F (f x) - ?N \<in> sets M" |
265 |
using F sets by auto } |
|
266 |
ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto |
|
267 |
next |
|
47694 | 268 |
show "AE x in M. f x = ?f' x" |
40859 | 269 |
by (rule AE_I', rule sets) auto |
270 |
qed |
|
271 |
qed |
|
272 |
||
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
273 |
lemma completion_ex_borel_measurable: |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
274 |
fixes g :: "'a \<Rightarrow> ennreal" |
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
275 |
assumes g: "g \<in> borel_measurable (completion M)" |
47694 | 276 |
shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)" |
40859 | 277 |
proof - |
47694 | 278 |
from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset
|
279 |
from this(1)[THEN completion_ex_simple_function] |
47694 | 280 |
have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" .. |
40859 | 281 |
from this[THEN choice] obtain f' where |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41097
diff
changeset
|
282 |
sf: "\<And>i. simple_function M (f' i)" and |
47694 | 283 |
AE: "\<forall>i. AE x in M. f i x = f' i x" by auto |
40859 | 284 |
show ?thesis |
285 |
proof (intro bexI) |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset
|
286 |
from AE[unfolded AE_all_countable[symmetric]] |
47694 | 287 |
show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x") |
41705 | 288 |
proof (elim AE_mp, safe intro!: AE_I2) |
40859 | 289 |
fix x assume eq: "\<forall>i. f i x = f' i x" |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset
|
290 |
moreover have "g x = (SUP i. f i x)" |
62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62390
diff
changeset
|
291 |
unfolding f by (auto split: split_max) |
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset
|
292 |
ultimately show "g x = ?f x" by auto |
40859 | 293 |
qed |
294 |
show "?f \<in> borel_measurable M" |
|
56949 | 295 |
using sf[THEN borel_measurable_simple_function] by auto |
40859 | 296 |
qed |
297 |
qed |
|
298 |
||
58587
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
299 |
lemma null_sets_completionI: "N \<in> null_sets M \<Longrightarrow> N \<in> null_sets (completion M)" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
300 |
by (auto simp: null_sets_def) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
301 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
302 |
lemma AE_completion: "(AE x in M. P x) \<Longrightarrow> (AE x in completion M. P x)" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
303 |
unfolding eventually_ae_filter by (auto intro: null_sets_completionI) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
304 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
305 |
lemma null_sets_completion_iff: "N \<in> sets M \<Longrightarrow> N \<in> null_sets (completion M) \<longleftrightarrow> N \<in> null_sets M" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
306 |
by (auto simp: null_sets_def) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
307 |
|
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
308 |
lemma AE_completion_iff: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in completion M. P x)" |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
309 |
by (simp add: AE_iff_null null_sets_completion_iff) |
5484f6079bcd
add type for probability mass functions, i.e. discrete probability distribution
hoelzl
parents:
56993
diff
changeset
|
310 |
|
63940
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
311 |
lemma sets_completion_AE: "(AE x in M. \<not> P x) \<Longrightarrow> Measurable.pred (completion M) P" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
312 |
unfolding pred_def sets_completion eventually_ae_filter |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
313 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
314 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
315 |
lemma null_sets_completion_iff2: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
316 |
"A \<in> null_sets (completion M) \<longleftrightarrow> (\<exists>N'\<in>null_sets M. A \<subseteq> N')" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
317 |
proof safe |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
318 |
assume "A \<in> null_sets (completion M)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
319 |
then have A: "A \<in> sets (completion M)" and "main_part M A \<in> null_sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
320 |
by (auto simp: null_sets_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
321 |
moreover obtain N where "N \<in> null_sets M" "null_part M A \<subseteq> N" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
322 |
using null_part[OF A] by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
323 |
ultimately show "\<exists>N'\<in>null_sets M. A \<subseteq> N'" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
324 |
proof (intro bexI) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
325 |
show "A \<subseteq> N \<union> main_part M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
326 |
using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[OF A, symmetric]) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
327 |
qed auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
328 |
next |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
329 |
fix N assume "N \<in> null_sets M" "A \<subseteq> N" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
330 |
then have "A \<in> sets (completion M)" and N: "N \<in> sets M" "A \<subseteq> N" "emeasure M N = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
331 |
by (auto intro: null_sets_completion) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
332 |
moreover have "emeasure (completion M) A = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
333 |
using N by (intro emeasure_eq_0[of N _ A]) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
334 |
ultimately show "A \<in> null_sets (completion M)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
335 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
336 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
337 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
338 |
lemma null_sets_completion_subset: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
339 |
"B \<subseteq> A \<Longrightarrow> A \<in> null_sets (completion M) \<Longrightarrow> B \<in> null_sets (completion M)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
340 |
unfolding null_sets_completion_iff2 by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
341 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
342 |
lemma null_sets_restrict_space: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
343 |
"\<Omega> \<in> sets M \<Longrightarrow> A \<in> null_sets (restrict_space M \<Omega>) \<longleftrightarrow> A \<subseteq> \<Omega> \<and> A \<in> null_sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
344 |
by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
345 |
lemma completion_ex_borel_measurable_real: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
346 |
fixes g :: "'a \<Rightarrow> real" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
347 |
assumes g: "g \<in> borel_measurable (completion M)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
348 |
shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
349 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
350 |
have "(\<lambda>x. ennreal (g x)) \<in> completion M \<rightarrow>\<^sub>M borel" "(\<lambda>x. ennreal (- g x)) \<in> completion M \<rightarrow>\<^sub>M borel" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
351 |
using g by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
352 |
from this[THEN completion_ex_borel_measurable] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
353 |
obtain pf nf :: "'a \<Rightarrow> ennreal" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
354 |
where [measurable]: "nf \<in> M \<rightarrow>\<^sub>M borel" "pf \<in> M \<rightarrow>\<^sub>M borel" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
355 |
and ae: "AE x in M. pf x = ennreal (g x)" "AE x in M. nf x = ennreal (- g x)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
356 |
by (auto simp: eq_commute) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
357 |
then have "AE x in M. pf x = ennreal (g x) \<and> nf x = ennreal (- g x)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
358 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
359 |
then obtain N where "N \<in> null_sets M" "{x\<in>space M. pf x \<noteq> ennreal (g x) \<and> nf x \<noteq> ennreal (- g x)} \<subseteq> N" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
360 |
by (auto elim!: AE_E) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
361 |
show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
362 |
proof |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
363 |
let ?F = "\<lambda>x. indicator (space M - N) x * (enn2real (pf x) - enn2real (nf x))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
364 |
show "?F \<in> M \<rightarrow>\<^sub>M borel" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
365 |
using \<open>N \<in> null_sets M\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
366 |
show "AE x in M. g x = ?F x" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
367 |
using \<open>N \<in> null_sets M\<close>[THEN AE_not_in] ae AE_space |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
368 |
apply eventually_elim |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
369 |
subgoal for x |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
370 |
by (cases "0::real" "g x" rule: linorder_le_cases) (auto simp: ennreal_neg) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
371 |
done |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
372 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
373 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
374 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
375 |
lemma simple_function_completion: "simple_function M f \<Longrightarrow> simple_function (completion M) f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
376 |
by (simp add: simple_function_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
377 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
378 |
lemma simple_integral_completion: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
379 |
"simple_function M f \<Longrightarrow> simple_integral (completion M) f = simple_integral M f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
380 |
unfolding simple_integral_def by simp |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
381 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
382 |
lemma nn_integral_completion: "nn_integral (completion M) f = nn_integral M f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
383 |
unfolding nn_integral_def |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
384 |
proof (safe intro!: SUP_eq) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
385 |
fix s assume s: "simple_function (completion M) s" and "s \<le> f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
386 |
then obtain s' where s': "simple_function M s'" "AE x in M. s x = s' x" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
387 |
by (auto dest: completion_ex_simple_function) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
388 |
then obtain N where N: "N \<in> null_sets M" "{x\<in>space M. s x \<noteq> s' x} \<subseteq> N" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
389 |
by (auto elim!: AE_E) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
390 |
then have ae_N: "AE x in M. (s x \<noteq> s' x \<longrightarrow> x \<in> N) \<and> x \<notin> N" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
391 |
by (auto dest: AE_not_in) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
392 |
define s'' where "s'' x = (if x \<in> N then 0 else s x)" for x |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
393 |
then have ae_s_eq_s'': "AE x in completion M. s x = s'' x" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
394 |
using s' ae_N by (intro AE_completion) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
395 |
have s'': "simple_function M s''" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
396 |
proof (subst simple_function_cong) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
397 |
show "t \<in> space M \<Longrightarrow> s'' t = (if t \<in> N then 0 else s' t)" for t |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
398 |
using N by (auto simp: s''_def dest: sets.sets_into_space) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
399 |
show "simple_function M (\<lambda>t. if t \<in> N then 0 else s' t)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
400 |
unfolding s''_def[abs_def] using N by (auto intro!: simple_function_If s') |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
401 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
402 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
403 |
show "\<exists>j\<in>{g. simple_function M g \<and> g \<le> f}. integral\<^sup>S (completion M) s \<le> integral\<^sup>S M j" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
404 |
proof (safe intro!: bexI[of _ s'']) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
405 |
have "integral\<^sup>S (completion M) s = integral\<^sup>S (completion M) s''" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
406 |
by (intro simple_integral_cong_AE s simple_function_completion s'' ae_s_eq_s'') |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
407 |
then show "integral\<^sup>S (completion M) s \<le> integral\<^sup>S M s''" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
408 |
using s'' by (simp add: simple_integral_completion) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
409 |
from \<open>s \<le> f\<close> show "s'' \<le> f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
410 |
unfolding s''_def le_fun_def by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
411 |
qed fact |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
412 |
next |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
413 |
fix s assume "simple_function M s" "s \<le> f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
414 |
then show "\<exists>j\<in>{g. simple_function (completion M) g \<and> g \<le> f}. integral\<^sup>S M s \<le> integral\<^sup>S (completion M) j" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
415 |
by (intro bexI[of _ s]) (auto simp: simple_integral_completion simple_function_completion) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
416 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
417 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
418 |
locale semifinite_measure = |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
419 |
fixes M :: "'a measure" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
420 |
assumes semifinite: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
421 |
"\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A = \<infinity> \<Longrightarrow> \<exists>B\<in>sets M. B \<subseteq> A \<and> emeasure M B < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
422 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
423 |
locale locally_determined_measure = semifinite_measure + |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
424 |
assumes locally_determined: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
425 |
"\<And>A. A \<subseteq> space M \<Longrightarrow> (\<And>B. B \<in> sets M \<Longrightarrow> emeasure M B < \<infinity> \<Longrightarrow> A \<inter> B \<in> sets M) \<Longrightarrow> A \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
426 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
427 |
locale cld_measure = complete_measure M + locally_determined_measure M for M :: "'a measure" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
428 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
429 |
definition outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
430 |
where "outer_measure_of M A = (INF B : {B\<in>sets M. A \<subseteq> B}. emeasure M B)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
431 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
432 |
lemma outer_measure_of_eq[simp]: "A \<in> sets M \<Longrightarrow> outer_measure_of M A = emeasure M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
433 |
by (auto simp: outer_measure_of_def intro!: INF_eqI emeasure_mono) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
434 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
435 |
lemma outer_measure_of_mono: "A \<subseteq> B \<Longrightarrow> outer_measure_of M A \<le> outer_measure_of M B" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
436 |
unfolding outer_measure_of_def by (intro INF_superset_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
437 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
438 |
lemma outer_measure_of_attain: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
439 |
assumes "A \<subseteq> space M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
440 |
shows "\<exists>E\<in>sets M. A \<subseteq> E \<and> outer_measure_of M A = emeasure M E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
441 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
442 |
have "emeasure M ` {B \<in> sets M. A \<subseteq> B} \<noteq> {}" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
443 |
using \<open>A \<subseteq> space M\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
444 |
from ennreal_Inf_countable_INF[OF this] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
445 |
obtain f |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
446 |
where f: "range f \<subseteq> emeasure M ` {B \<in> sets M. A \<subseteq> B}" "decseq f" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
447 |
and "outer_measure_of M A = (INF i. f i)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
448 |
unfolding outer_measure_of_def by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
449 |
have "\<exists>E. \<forall>n. (E n \<in> sets M \<and> A \<subseteq> E n \<and> emeasure M (E n) \<le> f n) \<and> E (Suc n) \<subseteq> E n" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
450 |
proof (rule dependent_nat_choice) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
451 |
show "\<exists>x. x \<in> sets M \<and> A \<subseteq> x \<and> emeasure M x \<le> f 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
452 |
using f(1) by (fastforce simp: image_subset_iff image_iff intro: eq_refl[OF sym]) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
453 |
next |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
454 |
fix E n assume "E \<in> sets M \<and> A \<subseteq> E \<and> emeasure M E \<le> f n" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
455 |
moreover obtain F where "F \<in> sets M" "A \<subseteq> F" "f (Suc n) = emeasure M F" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
456 |
using f(1) by (auto simp: image_subset_iff image_iff) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
457 |
ultimately show "\<exists>y. (y \<in> sets M \<and> A \<subseteq> y \<and> emeasure M y \<le> f (Suc n)) \<and> y \<subseteq> E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
458 |
by (auto intro!: exI[of _ "F \<inter> E"] emeasure_mono) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
459 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
460 |
then obtain E |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
461 |
where [simp]: "\<And>n. E n \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
462 |
and "\<And>n. A \<subseteq> E n" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
463 |
and le_f: "\<And>n. emeasure M (E n) \<le> f n" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
464 |
and "decseq E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
465 |
by (auto simp: decseq_Suc_iff) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
466 |
show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
467 |
proof cases |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
468 |
assume fin: "\<exists>i. emeasure M (E i) < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
469 |
show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
470 |
proof (intro bexI[of _ "\<Inter>i. E i"] conjI) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
471 |
show "A \<subseteq> (\<Inter>i. E i)" "(\<Inter>i. E i) \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
472 |
using \<open>\<And>n. A \<subseteq> E n\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
473 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
474 |
have " (INF i. emeasure M (E i)) \<le> outer_measure_of M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
475 |
unfolding \<open>outer_measure_of M A = (INF n. f n)\<close> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
476 |
by (intro INF_superset_mono le_f) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
477 |
moreover have "outer_measure_of M A \<le> (INF i. outer_measure_of M (E i))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
478 |
by (intro INF_greatest outer_measure_of_mono \<open>\<And>n. A \<subseteq> E n\<close>) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
479 |
ultimately have "outer_measure_of M A = (INF i. emeasure M (E i))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
480 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
481 |
also have "\<dots> = emeasure M (\<Inter>i. E i)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
482 |
using fin by (intro INF_emeasure_decseq' \<open>decseq E\<close>) (auto simp: less_top) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
483 |
finally show "outer_measure_of M A = emeasure M (\<Inter>i. E i)" . |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
484 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
485 |
next |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
486 |
assume "\<nexists>i. emeasure M (E i) < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
487 |
then have "f n = \<infinity>" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
488 |
using le_f by (auto simp: not_less top_unique) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
489 |
moreover have "\<exists>E\<in>sets M. A \<subseteq> E \<and> f 0 = emeasure M E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
490 |
using f by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
491 |
ultimately show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
492 |
unfolding \<open>outer_measure_of M A = (INF n. f n)\<close> by simp |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
493 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
494 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
495 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
496 |
lemma SUP_outer_measure_of_incseq: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
497 |
assumes A: "\<And>n. A n \<subseteq> space M" and "incseq A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
498 |
shows "(SUP n. outer_measure_of M (A n)) = outer_measure_of M (\<Union>i. A i)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
499 |
proof (rule antisym) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
500 |
obtain E |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
501 |
where E: "\<And>n. E n \<in> sets M" "\<And>n. A n \<subseteq> E n" "\<And>n. outer_measure_of M (A n) = emeasure M (E n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
502 |
using outer_measure_of_attain[OF A] by metis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
503 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
504 |
define F where "F n = (\<Inter>i\<in>{n ..}. E i)" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
505 |
with E have F: "incseq F" "\<And>n. F n \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
506 |
by (auto simp: incseq_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
507 |
have "A n \<subseteq> F n" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
508 |
using incseqD[OF \<open>incseq A\<close>, of n] \<open>\<And>n. A n \<subseteq> E n\<close> by (auto simp: F_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
509 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
510 |
have eq: "outer_measure_of M (A n) = outer_measure_of M (F n)" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
511 |
proof (intro antisym) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
512 |
have "outer_measure_of M (F n) \<le> outer_measure_of M (E n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
513 |
by (intro outer_measure_of_mono) (auto simp add: F_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
514 |
with E show "outer_measure_of M (F n) \<le> outer_measure_of M (A n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
515 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
516 |
show "outer_measure_of M (A n) \<le> outer_measure_of M (F n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
517 |
by (intro outer_measure_of_mono \<open>A n \<subseteq> F n\<close>) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
518 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
519 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
520 |
have "outer_measure_of M (\<Union>n. A n) \<le> outer_measure_of M (\<Union>n. F n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
521 |
using \<open>\<And>n. A n \<subseteq> F n\<close> by (intro outer_measure_of_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
522 |
also have "\<dots> = (SUP n. emeasure M (F n))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
523 |
using F by (simp add: SUP_emeasure_incseq subset_eq) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
524 |
finally show "outer_measure_of M (\<Union>n. A n) \<le> (SUP n. outer_measure_of M (A n))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
525 |
by (simp add: eq F) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
526 |
qed (auto intro: SUP_least outer_measure_of_mono) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
527 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
528 |
definition measurable_envelope :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
529 |
where "measurable_envelope M A E \<longleftrightarrow> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
530 |
(A \<subseteq> E \<and> E \<in> sets M \<and> (\<forall>F\<in>sets M. emeasure M (F \<inter> E) = outer_measure_of M (F \<inter> A)))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
531 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
532 |
lemma measurable_envelopeD: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
533 |
assumes "measurable_envelope M A E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
534 |
shows "A \<subseteq> E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
535 |
and "E \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
536 |
and "\<And>F. F \<in> sets M \<Longrightarrow> emeasure M (F \<inter> E) = outer_measure_of M (F \<inter> A)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
537 |
and "A \<subseteq> space M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
538 |
using assms sets.sets_into_space[of E] by (auto simp: measurable_envelope_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
539 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
540 |
lemma measurable_envelopeD1: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
541 |
assumes E: "measurable_envelope M A E" and F: "F \<in> sets M" "F \<subseteq> E - A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
542 |
shows "emeasure M F = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
543 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
544 |
have "emeasure M F = emeasure M (F \<inter> E)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
545 |
using F by (intro arg_cong2[where f=emeasure]) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
546 |
also have "\<dots> = outer_measure_of M (F \<inter> A)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
547 |
using measurable_envelopeD[OF E] \<open>F \<in> sets M\<close> by (auto simp: measurable_envelope_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
548 |
also have "\<dots> = outer_measure_of M {}" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
549 |
using \<open>F \<subseteq> E - A\<close> by (intro arg_cong2[where f=outer_measure_of]) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
550 |
finally show "emeasure M F = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
551 |
by simp |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
552 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
553 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
554 |
lemma measurable_envelope_eq1: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
555 |
assumes "A \<subseteq> E" "E \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
556 |
shows "measurable_envelope M A E \<longleftrightarrow> (\<forall>F\<in>sets M. F \<subseteq> E - A \<longrightarrow> emeasure M F = 0)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
557 |
proof safe |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
558 |
assume *: "\<forall>F\<in>sets M. F \<subseteq> E - A \<longrightarrow> emeasure M F = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
559 |
show "measurable_envelope M A E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
560 |
unfolding measurable_envelope_def |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
561 |
proof (rule ccontr, auto simp add: \<open>E \<in> sets M\<close> \<open>A \<subseteq> E\<close>) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
562 |
fix F assume "F \<in> sets M" "emeasure M (F \<inter> E) \<noteq> outer_measure_of M (F \<inter> A)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
563 |
then have "outer_measure_of M (F \<inter> A) < emeasure M (F \<inter> E)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
564 |
using outer_measure_of_mono[of "F \<inter> A" "F \<inter> E" M] \<open>A \<subseteq> E\<close> \<open>E \<in> sets M\<close> by (auto simp: less_le) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
565 |
then obtain G where G: "G \<in> sets M" "F \<inter> A \<subseteq> G" and less: "emeasure M G < emeasure M (E \<inter> F)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
566 |
unfolding outer_measure_of_def INF_less_iff by (auto simp: ac_simps) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
567 |
have le: "emeasure M (G \<inter> E \<inter> F) \<le> emeasure M G" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
568 |
using \<open>E \<in> sets M\<close> \<open>G \<in> sets M\<close> \<open>F \<in> sets M\<close> by (auto intro!: emeasure_mono) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
569 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
570 |
from G have "E \<inter> F - G \<in> sets M" "E \<inter> F - G \<subseteq> E - A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
571 |
using \<open>F \<in> sets M\<close> \<open>E \<in> sets M\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
572 |
with * have "0 = emeasure M (E \<inter> F - G)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
573 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
574 |
also have "E \<inter> F - G = E \<inter> F - (G \<inter> E \<inter> F)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
575 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
576 |
also have "emeasure M (E \<inter> F - (G \<inter> E \<inter> F)) = emeasure M (E \<inter> F) - emeasure M (G \<inter> E \<inter> F)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
577 |
using \<open>E \<in> sets M\<close> \<open>F \<in> sets M\<close> le less G by (intro emeasure_Diff) (auto simp: top_unique) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
578 |
also have "\<dots> > 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
579 |
using le less by (intro diff_gr0_ennreal) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
580 |
finally show False by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
581 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
582 |
qed (rule measurable_envelopeD1) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
583 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
584 |
lemma measurable_envelopeD2: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
585 |
assumes E: "measurable_envelope M A E" shows "emeasure M E = outer_measure_of M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
586 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
587 |
from \<open>measurable_envelope M A E\<close> have "emeasure M (E \<inter> E) = outer_measure_of M (E \<inter> A)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
588 |
by (auto simp: measurable_envelope_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
589 |
with measurable_envelopeD[OF E] show "emeasure M E = outer_measure_of M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
590 |
by (auto simp: Int_absorb1) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
591 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
592 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
593 |
lemma measurable_envelope_eq2: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
594 |
assumes "A \<subseteq> E" "E \<in> sets M" "emeasure M E < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
595 |
shows "measurable_envelope M A E \<longleftrightarrow> (emeasure M E = outer_measure_of M A)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
596 |
proof safe |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
597 |
assume *: "emeasure M E = outer_measure_of M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
598 |
show "measurable_envelope M A E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
599 |
unfolding measurable_envelope_eq1[OF \<open>A \<subseteq> E\<close> \<open>E \<in> sets M\<close>] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
600 |
proof (intro conjI ballI impI assms) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
601 |
fix F assume F: "F \<in> sets M" "F \<subseteq> E - A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
602 |
with \<open>E \<in> sets M\<close> have le: "emeasure M F \<le> emeasure M E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
603 |
by (intro emeasure_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
604 |
from F \<open>A \<subseteq> E\<close> have "outer_measure_of M A \<le> outer_measure_of M (E - F)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
605 |
by (intro outer_measure_of_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
606 |
then have "emeasure M E - 0 \<le> emeasure M (E - F)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
607 |
using * \<open>E \<in> sets M\<close> \<open>F \<in> sets M\<close> by simp |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
608 |
also have "\<dots> = emeasure M E - emeasure M F" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
609 |
using \<open>E \<in> sets M\<close> \<open>emeasure M E < \<infinity>\<close> F le by (intro emeasure_Diff) (auto simp: top_unique) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
610 |
finally show "emeasure M F = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
611 |
using ennreal_mono_minus_cancel[of "emeasure M E" 0 "emeasure M F"] le assms by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
612 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
613 |
qed (auto intro: measurable_envelopeD2) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
614 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
615 |
lemma measurable_envelopeI_countable: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
616 |
fixes A :: "nat \<Rightarrow> 'a set" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
617 |
assumes E: "\<And>n. measurable_envelope M (A n) (E n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
618 |
shows "measurable_envelope M (\<Union>n. A n) (\<Union>n. E n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
619 |
proof (subst measurable_envelope_eq1) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
620 |
show "(\<Union>n. A n) \<subseteq> (\<Union>n. E n)" "(\<Union>n. E n) \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
621 |
using measurable_envelopeD(1,2)[OF E] by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
622 |
show "\<forall>F\<in>sets M. F \<subseteq> (\<Union>n. E n) - (\<Union>n. A n) \<longrightarrow> emeasure M F = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
623 |
proof safe |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
624 |
fix F assume F: "F \<in> sets M" "F \<subseteq> (\<Union>n. E n) - (\<Union>n. A n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
625 |
then have "F \<inter> E n \<in> sets M" "F \<inter> E n \<subseteq> E n - A n" "F \<subseteq> (\<Union>n. E n)" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
626 |
using measurable_envelopeD(1,2)[OF E] by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
627 |
then have "emeasure M (\<Union>n. F \<inter> E n) = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
628 |
by (intro emeasure_UN_eq_0 measurable_envelopeD1[OF E]) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
629 |
then show "emeasure M F = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
630 |
using \<open>F \<subseteq> (\<Union>n. E n)\<close> by (auto simp: Int_absorb2) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
631 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
632 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
633 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
634 |
lemma measurable_envelopeI_countable_cover: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
635 |
fixes A and C :: "nat \<Rightarrow> 'a set" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
636 |
assumes C: "A \<subseteq> (\<Union>n. C n)" "\<And>n. C n \<in> sets M" "\<And>n. emeasure M (C n) < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
637 |
shows "\<exists>E\<subseteq>(\<Union>n. C n). measurable_envelope M A E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
638 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
639 |
have "A \<inter> C n \<subseteq> space M" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
640 |
using \<open>C n \<in> sets M\<close> by (auto dest: sets.sets_into_space) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
641 |
then have "\<forall>n. \<exists>E\<in>sets M. A \<inter> C n \<subseteq> E \<and> outer_measure_of M (A \<inter> C n) = emeasure M E" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
642 |
using outer_measure_of_attain[of "A \<inter> C n" M for n] by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
643 |
then obtain E |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
644 |
where E: "\<And>n. E n \<in> sets M" "\<And>n. A \<inter> C n \<subseteq> E n" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
645 |
and eq: "\<And>n. outer_measure_of M (A \<inter> C n) = emeasure M (E n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
646 |
by metis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
647 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
648 |
have "outer_measure_of M (A \<inter> C n) \<le> outer_measure_of M (E n \<inter> C n)" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
649 |
using E by (intro outer_measure_of_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
650 |
moreover have "outer_measure_of M (E n \<inter> C n) \<le> outer_measure_of M (E n)" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
651 |
by (intro outer_measure_of_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
652 |
ultimately have eq: "outer_measure_of M (A \<inter> C n) = emeasure M (E n \<inter> C n)" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
653 |
using E C by (intro antisym) (auto simp: eq) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
654 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
655 |
{ fix n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
656 |
have "outer_measure_of M (A \<inter> C n) \<le> outer_measure_of M (C n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
657 |
by (intro outer_measure_of_mono) simp |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
658 |
also have "\<dots> < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
659 |
using assms by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
660 |
finally have "emeasure M (E n \<inter> C n) < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
661 |
using eq by simp } |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
662 |
then have "measurable_envelope M (\<Union>n. A \<inter> C n) (\<Union>n. E n \<inter> C n)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
663 |
using E C by (intro measurable_envelopeI_countable measurable_envelope_eq2[THEN iffD2]) (auto simp: eq) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
664 |
with \<open>A \<subseteq> (\<Union>n. C n)\<close> show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
665 |
by (intro exI[of _ "(\<Union>n. E n \<inter> C n)"]) (auto simp add: Int_absorb2) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
666 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
667 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
668 |
lemma (in complete_measure) complete_sets_sandwich: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
669 |
assumes [measurable]: "A \<in> sets M" "C \<in> sets M" and subset: "A \<subseteq> B" "B \<subseteq> C" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
670 |
and measure: "emeasure M A = emeasure M C" "emeasure M A < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
671 |
shows "B \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
672 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
673 |
have "B - A \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
674 |
proof (rule complete) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
675 |
show "B - A \<subseteq> C - A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
676 |
using subset by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
677 |
show "C - A \<in> null_sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
678 |
using measure subset by(simp add: emeasure_Diff null_setsI) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
679 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
680 |
then have "A \<union> (B - A) \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
681 |
by measurable |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
682 |
also have "A \<union> (B - A) = B" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
683 |
using \<open>A \<subseteq> B\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
684 |
finally show ?thesis . |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
685 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
686 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
687 |
lemma (in cld_measure) notin_sets_outer_measure_of_cover: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
688 |
assumes E: "E \<subseteq> space M" "E \<notin> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
689 |
shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
690 |
outer_measure_of M (B \<inter> E) = emeasure M B \<and> outer_measure_of M (B - E) = emeasure M B" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
691 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
692 |
from locally_determined[OF \<open>E \<subseteq> space M\<close>] \<open>E \<notin> sets M\<close> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
693 |
obtain F |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
694 |
where [measurable]: "F \<in> sets M" and "emeasure M F < \<infinity>" "E \<inter> F \<notin> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
695 |
by blast |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
696 |
then obtain H H' |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
697 |
where H: "measurable_envelope M (F \<inter> E) H" and H': "measurable_envelope M (F - E) H'" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
698 |
using measurable_envelopeI_countable_cover[of "F \<inter> E" "\<lambda>_. F" M] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
699 |
measurable_envelopeI_countable_cover[of "F - E" "\<lambda>_. F" M] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
700 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
701 |
note measurable_envelopeD(2)[OF H', measurable] measurable_envelopeD(2)[OF H, measurable] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
702 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
703 |
from measurable_envelopeD(1)[OF H'] measurable_envelopeD(1)[OF H] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
704 |
have subset: "F - H' \<subseteq> F \<inter> E" "F \<inter> E \<subseteq> F \<inter> H" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
705 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
706 |
moreover define G where "G = (F \<inter> H) - (F - H')" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
707 |
ultimately have G: "G = F \<inter> H \<inter> H'" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
708 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
709 |
have "emeasure M (F \<inter> H) \<noteq> 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
710 |
proof |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
711 |
assume "emeasure M (F \<inter> H) = 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
712 |
then have "F \<inter> H \<in> null_sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
713 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
714 |
with \<open>E \<inter> F \<notin> sets M\<close> show False |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
715 |
using complete[OF \<open>F \<inter> E \<subseteq> F \<inter> H\<close>] by (auto simp: Int_commute) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
716 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
717 |
moreover |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
718 |
have "emeasure M (F - H') \<noteq> emeasure M (F \<inter> H)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
719 |
proof |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
720 |
assume "emeasure M (F - H') = emeasure M (F \<inter> H)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
721 |
with \<open>E \<inter> F \<notin> sets M\<close> emeasure_mono[of "F \<inter> H" F M] \<open>emeasure M F < \<infinity>\<close> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
722 |
have "F \<inter> E \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
723 |
by (intro complete_sets_sandwich[OF _ _ subset]) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
724 |
with \<open>E \<inter> F \<notin> sets M\<close> show False |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
725 |
by (simp add: Int_commute) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
726 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
727 |
moreover have "emeasure M (F - H') \<le> emeasure M (F \<inter> H)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
728 |
using subset by (intro emeasure_mono) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
729 |
ultimately have "emeasure M G \<noteq> 0" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
730 |
unfolding G_def using subset |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
731 |
by (subst emeasure_Diff) (auto simp: top_unique diff_eq_0_iff_ennreal) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
732 |
show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
733 |
proof (intro bexI conjI) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
734 |
have "emeasure M G \<le> emeasure M F" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
735 |
unfolding G by (auto intro!: emeasure_mono) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
736 |
with \<open>emeasure M F < \<infinity>\<close> show "0 < emeasure M G" "emeasure M G < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
737 |
using \<open>emeasure M G \<noteq> 0\<close> by (auto simp: zero_less_iff_neq_zero) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
738 |
show [measurable]: "G \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
739 |
unfolding G by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
740 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
741 |
have "emeasure M G = outer_measure_of M (F \<inter> H' \<inter> (F \<inter> E))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
742 |
using measurable_envelopeD(3)[OF H, of "F \<inter> H'"] unfolding G by (simp add: ac_simps) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
743 |
also have "\<dots> \<le> outer_measure_of M (G \<inter> E)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
744 |
using measurable_envelopeD(1)[OF H] by (intro outer_measure_of_mono) (auto simp: G) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
745 |
finally show "outer_measure_of M (G \<inter> E) = emeasure M G" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
746 |
using outer_measure_of_mono[of "G \<inter> E" G M] by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
747 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
748 |
have "emeasure M G = outer_measure_of M (F \<inter> H \<inter> (F - E))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
749 |
using measurable_envelopeD(3)[OF H', of "F \<inter> H"] unfolding G by (simp add: ac_simps) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
750 |
also have "\<dots> \<le> outer_measure_of M (G - E)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
751 |
using measurable_envelopeD(1)[OF H'] by (intro outer_measure_of_mono) (auto simp: G) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
752 |
finally show "outer_measure_of M (G - E) = emeasure M G" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
753 |
using outer_measure_of_mono[of "G - E" G M] by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
754 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
755 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
756 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
757 |
text \<open>The following theorem is a specialization of D.H. Fremlin, Measure Theory vol 4I (413G). We |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
758 |
only show one direction and do not use a inner regular family $K$.\<close> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
759 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
760 |
lemma (in cld_measure) borel_measurable_cld: |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
761 |
fixes f :: "'a \<Rightarrow> real" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
762 |
assumes "\<And>A a b. A \<in> sets M \<Longrightarrow> 0 < emeasure M A \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> a < b \<Longrightarrow> |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
763 |
min (outer_measure_of M {x\<in>A. f x \<le> a}) (outer_measure_of M {x\<in>A. b \<le> f x}) < emeasure M A" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
764 |
shows "f \<in> M \<rightarrow>\<^sub>M borel" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
765 |
proof (rule ccontr) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
766 |
let ?E = "\<lambda>a. {x\<in>space M. f x \<le> a}" and ?F = "\<lambda>a. {x\<in>space M. a \<le> f x}" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
767 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
768 |
assume "f \<notin> M \<rightarrow>\<^sub>M borel" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
769 |
then obtain a where "?E a \<notin> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
770 |
unfolding borel_measurable_iff_le by blast |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
771 |
from notin_sets_outer_measure_of_cover[OF _ this] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
772 |
obtain K |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
773 |
where K: "K \<in> sets M" "0 < emeasure M K" "emeasure M K < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
774 |
and eq1: "outer_measure_of M (K \<inter> ?E a) = emeasure M K" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
775 |
and eq2: "outer_measure_of M (K - ?E a) = emeasure M K" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
776 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
777 |
then have me_K: "measurable_envelope M (K \<inter> ?E a) K" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
778 |
by (subst measurable_envelope_eq2) auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
779 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
780 |
define b where "b n = a + inverse (real (Suc n))" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
781 |
have "(SUP n. outer_measure_of M (K \<inter> ?F (b n))) = outer_measure_of M (\<Union>n. K \<inter> ?F (b n))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
782 |
proof (intro SUP_outer_measure_of_incseq) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
783 |
have "x \<le> y \<Longrightarrow> b y \<le> b x" for x y |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
784 |
by (auto simp: b_def field_simps) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
785 |
then show "incseq (\<lambda>n. K \<inter> {x \<in> space M. b n \<le> f x})" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
786 |
by (auto simp: incseq_def intro: order_trans) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
787 |
qed auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
788 |
also have "(\<Union>n. K \<inter> ?F (b n)) = K - ?E a" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
789 |
proof - |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
790 |
have "b \<longlonglongrightarrow> a" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
791 |
unfolding b_def by (rule LIMSEQ_inverse_real_of_nat_add) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
792 |
then have "\<forall>n. \<not> b n \<le> f x \<Longrightarrow> f x \<le> a" for x |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
793 |
by (rule LIMSEQ_le_const) (auto intro: less_imp_le simp: not_le) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
794 |
moreover have "\<not> b n \<le> a" for n |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
795 |
by (auto simp: b_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
796 |
ultimately show ?thesis |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
797 |
using \<open>K \<in> sets M\<close>[THEN sets.sets_into_space] by (auto simp: subset_eq intro: order_trans) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
798 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
799 |
finally have "0 < (SUP n. outer_measure_of M (K \<inter> ?F (b n)))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
800 |
using K by (simp add: eq2) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
801 |
then obtain n where pos_b: "0 < outer_measure_of M (K \<inter> ?F (b n))" and "a < b n" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
802 |
unfolding less_SUP_iff by (auto simp: b_def) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
803 |
from measurable_envelopeI_countable_cover[of "K \<inter> ?F (b n)" "\<lambda>_. K" M] K |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
804 |
obtain K' where "K' \<subseteq> K" and me_K': "measurable_envelope M (K \<inter> ?F (b n)) K'" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
805 |
by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
806 |
then have K'_le_K: "emeasure M K' \<le> emeasure M K" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
807 |
by (intro emeasure_mono K) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
808 |
have "K' \<in> sets M" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
809 |
using me_K' by (rule measurable_envelopeD) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
810 |
|
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
811 |
have "min (outer_measure_of M {x\<in>K'. f x \<le> a}) (outer_measure_of M {x\<in>K'. b n \<le> f x}) < emeasure M K'" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
812 |
proof (rule assms) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
813 |
show "0 < emeasure M K'" "emeasure M K' < \<infinity>" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
814 |
using measurable_envelopeD2[OF me_K'] pos_b K K'_le_K by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
815 |
qed fact+ |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
816 |
also have "{x\<in>K'. f x \<le> a} = K' \<inter> (K \<inter> ?E a)" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
817 |
using \<open>K' \<in> sets M\<close>[THEN sets.sets_into_space] \<open>K' \<subseteq> K\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
818 |
also have "{x\<in>K'. b n \<le> f x} = K' \<inter> (K \<inter> ?F (b n))" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
819 |
using \<open>K' \<in> sets M\<close>[THEN sets.sets_into_space] \<open>K' \<subseteq> K\<close> by auto |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
820 |
finally have "min (emeasure M K) (emeasure M K') < emeasure M K'" |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
821 |
unfolding |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
822 |
measurable_envelopeD(3)[OF me_K \<open>K' \<in> sets M\<close>, symmetric] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
823 |
measurable_envelopeD(3)[OF me_K' \<open>K' \<in> sets M\<close>, symmetric] |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
824 |
using \<open>K' \<subseteq> K\<close> by (simp add: Int_absorb1 Int_absorb2) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
825 |
with K'_le_K show False |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
826 |
by (auto simp: min_def split: if_split_asm) |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
827 |
qed |
0d82c4c94014
prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
hoelzl
parents:
63627
diff
changeset
|
828 |
|
40859 | 829 |
end |