author | hoelzl |
Wed, 23 Feb 2011 11:40:12 +0100 | |
changeset 41831 | 91a2b435dd7a |
parent 41705 | 1100512e16d8 |
child 41981 | cdf7693bbe08 |
permissions | -rw-r--r-- |
38656 | 1 |
(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) |
2 |
||
35582 | 3 |
header {*Lebesgue Integration*} |
4 |
||
38656 | 5 |
theory Lebesgue_Integration |
40859 | 6 |
imports Measure Borel_Space |
35582 | 7 |
begin |
8 |
||
38656 | 9 |
lemma sums_If_finite: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
10 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
38656 | 11 |
assumes finite: "finite {r. P r}" |
12 |
shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _") |
|
13 |
proof cases |
|
14 |
assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto |
|
15 |
thus ?thesis by (simp add: sums_zero) |
|
16 |
next |
|
17 |
assume not_empty: "{r. P r} \<noteq> {}" |
|
18 |
have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)" |
|
19 |
by (rule series_zero) |
|
20 |
(auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric]) |
|
21 |
also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)" |
|
22 |
by (subst setsum_cases) |
|
23 |
(auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le) |
|
24 |
finally show ?thesis . |
|
25 |
qed |
|
35582 | 26 |
|
38656 | 27 |
lemma sums_single: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
28 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
29 |
shows "(\<lambda>r. if r = i then f r else 0) sums f i" |
38656 | 30 |
using sums_If_finite[of "\<lambda>r. r = i" f] by simp |
31 |
||
32 |
section "Simple function" |
|
35582 | 33 |
|
38656 | 34 |
text {* |
35 |
||
36 |
Our simple functions are not restricted to positive real numbers. Instead |
|
37 |
they are just functions with a finite range and are measurable when singleton |
|
38 |
sets are measurable. |
|
35582 | 39 |
|
38656 | 40 |
*} |
41 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
42 |
definition "simple_function M g \<longleftrightarrow> |
38656 | 43 |
finite (g ` space M) \<and> |
44 |
(\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)" |
|
36624 | 45 |
|
38656 | 46 |
lemma (in sigma_algebra) simple_functionD: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
47 |
assumes "simple_function M g" |
40875 | 48 |
shows "finite (g ` space M)" and "g -` X \<inter> space M \<in> sets M" |
40871 | 49 |
proof - |
50 |
show "finite (g ` space M)" |
|
51 |
using assms unfolding simple_function_def by auto |
|
40875 | 52 |
have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto |
53 |
also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto |
|
54 |
finally show "g -` X \<inter> space M \<in> sets M" using assms |
|
55 |
by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def) |
|
40871 | 56 |
qed |
36624 | 57 |
|
38656 | 58 |
lemma (in sigma_algebra) simple_function_indicator_representation: |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
59 |
fixes f ::"'a \<Rightarrow> pextreal" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
60 |
assumes f: "simple_function M f" and x: "x \<in> space M" |
38656 | 61 |
shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f -` {y} \<inter> space M) x)" |
62 |
(is "?l = ?r") |
|
63 |
proof - |
|
38705 | 64 |
have "?r = (\<Sum>y \<in> f ` space M. |
38656 | 65 |
(if y = f x then y * indicator (f -` {y} \<inter> space M) x else 0))" |
66 |
by (auto intro!: setsum_cong2) |
|
67 |
also have "... = f x * indicator (f -` {f x} \<inter> space M) x" |
|
68 |
using assms by (auto dest: simple_functionD simp: setsum_delta) |
|
69 |
also have "... = f x" using x by (auto simp: indicator_def) |
|
70 |
finally show ?thesis by auto |
|
71 |
qed |
|
36624 | 72 |
|
38656 | 73 |
lemma (in measure_space) simple_function_notspace: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
74 |
"simple_function M (\<lambda>x. h x * indicator (- space M) x::pextreal)" (is "simple_function M ?h") |
35692 | 75 |
proof - |
38656 | 76 |
have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto |
77 |
hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) |
|
78 |
have "?h -` {0} \<inter> space M = space M" by auto |
|
79 |
thus ?thesis unfolding simple_function_def by auto |
|
80 |
qed |
|
81 |
||
82 |
lemma (in sigma_algebra) simple_function_cong: |
|
83 |
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
84 |
shows "simple_function M f \<longleftrightarrow> simple_function M g" |
38656 | 85 |
proof - |
86 |
have "f ` space M = g ` space M" |
|
87 |
"\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M" |
|
88 |
using assms by (auto intro!: image_eqI) |
|
89 |
thus ?thesis unfolding simple_function_def using assms by simp |
|
90 |
qed |
|
91 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
92 |
lemma (in sigma_algebra) simple_function_cong_algebra: |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
93 |
assumes "sets N = sets M" "space N = space M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
94 |
shows "simple_function M f \<longleftrightarrow> simple_function N f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
95 |
unfolding simple_function_def assms .. |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
96 |
|
38656 | 97 |
lemma (in sigma_algebra) borel_measurable_simple_function: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
98 |
assumes "simple_function M f" |
38656 | 99 |
shows "f \<in> borel_measurable M" |
100 |
proof (rule borel_measurableI) |
|
101 |
fix S |
|
102 |
let ?I = "f ` (f -` S \<inter> space M)" |
|
103 |
have *: "(\<Union>x\<in>?I. f -` {x} \<inter> space M) = f -` S \<inter> space M" (is "?U = _") by auto |
|
104 |
have "finite ?I" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
105 |
using assms unfolding simple_function_def |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
106 |
using finite_subset[of "f ` (f -` S \<inter> space M)" "f ` space M"] by auto |
38656 | 107 |
hence "?U \<in> sets M" |
108 |
apply (rule finite_UN) |
|
109 |
using assms unfolding simple_function_def by auto |
|
110 |
thus "f -` S \<inter> space M \<in> sets M" unfolding * . |
|
35692 | 111 |
qed |
112 |
||
38656 | 113 |
lemma (in sigma_algebra) simple_function_borel_measurable: |
114 |
fixes f :: "'a \<Rightarrow> 'x::t2_space" |
|
115 |
assumes "f \<in> borel_measurable M" and "finite (f ` space M)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
116 |
shows "simple_function M f" |
38656 | 117 |
using assms unfolding simple_function_def |
118 |
by (auto intro: borel_measurable_vimage) |
|
119 |
||
120 |
lemma (in sigma_algebra) simple_function_const[intro, simp]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
121 |
"simple_function M (\<lambda>x. c)" |
38656 | 122 |
by (auto intro: finite_subset simp: simple_function_def) |
123 |
||
124 |
lemma (in sigma_algebra) simple_function_compose[intro, simp]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
125 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
126 |
shows "simple_function M (g \<circ> f)" |
38656 | 127 |
unfolding simple_function_def |
128 |
proof safe |
|
129 |
show "finite ((g \<circ> f) ` space M)" |
|
130 |
using assms unfolding simple_function_def by (auto simp: image_compose) |
|
131 |
next |
|
132 |
fix x assume "x \<in> space M" |
|
133 |
let ?G = "g -` {g (f x)} \<inter> (f`space M)" |
|
134 |
have *: "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M = |
|
135 |
(\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto |
|
136 |
show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M" |
|
137 |
using assms unfolding simple_function_def * |
|
138 |
by (rule_tac finite_UN) (auto intro!: finite_UN) |
|
139 |
qed |
|
140 |
||
141 |
lemma (in sigma_algebra) simple_function_indicator[intro, simp]: |
|
142 |
assumes "A \<in> 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:
41661
diff
changeset
|
143 |
shows "simple_function M (indicator A)" |
35692 | 144 |
proof - |
38656 | 145 |
have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _") |
146 |
by (auto simp: indicator_def) |
|
147 |
hence "finite ?S" by (rule finite_subset) simp |
|
148 |
moreover have "- A \<inter> space M = space M - A" by auto |
|
149 |
ultimately show ?thesis unfolding simple_function_def |
|
150 |
using assms by (auto simp: indicator_def_raw) |
|
35692 | 151 |
qed |
152 |
||
38656 | 153 |
lemma (in sigma_algebra) simple_function_Pair[intro, simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
154 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
155 |
assumes "simple_function M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
156 |
shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p") |
38656 | 157 |
unfolding simple_function_def |
158 |
proof safe |
|
159 |
show "finite (?p ` space M)" |
|
160 |
using assms unfolding simple_function_def |
|
161 |
by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto |
|
162 |
next |
|
163 |
fix x assume "x \<in> space M" |
|
164 |
have "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = |
|
165 |
(f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" |
|
166 |
by auto |
|
167 |
with `x \<in> space M` show "(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M \<in> sets M" |
|
168 |
using assms unfolding simple_function_def by auto |
|
169 |
qed |
|
35692 | 170 |
|
38656 | 171 |
lemma (in sigma_algebra) simple_function_compose1: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
172 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
173 |
shows "simple_function M (\<lambda>x. g (f x))" |
38656 | 174 |
using simple_function_compose[OF assms, of g] |
175 |
by (simp add: comp_def) |
|
35582 | 176 |
|
38656 | 177 |
lemma (in sigma_algebra) simple_function_compose2: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
178 |
assumes "simple_function M f" and "simple_function M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
179 |
shows "simple_function M (\<lambda>x. h (f x) (g x))" |
38656 | 180 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
181 |
have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))" |
38656 | 182 |
using assms by auto |
183 |
thus ?thesis by (simp_all add: comp_def) |
|
184 |
qed |
|
35582 | 185 |
|
38656 | 186 |
lemmas (in sigma_algebra) simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] |
187 |
and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"] |
|
188 |
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] |
|
189 |
and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] |
|
190 |
and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] |
|
191 |
and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] |
|
192 |
||
193 |
lemma (in sigma_algebra) simple_function_setsum[intro, simp]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
194 |
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
195 |
shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)" |
38656 | 196 |
proof cases |
197 |
assume "finite P" from this assms show ?thesis by induct auto |
|
198 |
qed auto |
|
35582 | 199 |
|
38656 | 200 |
lemma (in sigma_algebra) simple_function_le_measurable: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
201 |
assumes "simple_function M f" "simple_function M g" |
38656 | 202 |
shows "{x \<in> space M. f x \<le> g x} \<in> sets M" |
203 |
proof - |
|
204 |
have *: "{x \<in> space M. f x \<le> g x} = |
|
205 |
(\<Union>(F, G)\<in>f`space M \<times> g`space M. |
|
206 |
if F \<le> G then (f -` {F} \<inter> space M) \<inter> (g -` {G} \<inter> space M) else {})" |
|
207 |
apply (auto split: split_if_asm) |
|
208 |
apply (rule_tac x=x in bexI) |
|
209 |
apply (rule_tac x=x in bexI) |
|
210 |
by simp_all |
|
211 |
have **: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> |
|
212 |
(f -` {f x} \<inter> space M) \<inter> (g -` {g y} \<inter> space M) \<in> sets M" |
|
213 |
using assms unfolding simple_function_def by auto |
|
214 |
have "finite (f`space M \<times> g`space M)" |
|
215 |
using assms unfolding simple_function_def by auto |
|
216 |
thus ?thesis unfolding * |
|
217 |
apply (rule finite_UN) |
|
218 |
using assms unfolding simple_function_def |
|
219 |
by (auto intro!: **) |
|
35582 | 220 |
qed |
221 |
||
38656 | 222 |
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence: |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
223 |
fixes u :: "'a \<Rightarrow> pextreal" |
38656 | 224 |
assumes u: "u \<in> borel_measurable M" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
225 |
shows "\<exists>f. (\<forall>i. simple_function M (f i) \<and> (\<forall>x\<in>space M. f i x \<noteq> \<omega>)) \<and> f \<up> u" |
35582 | 226 |
proof - |
38656 | 227 |
have "\<exists>f. \<forall>x j. (of_nat j \<le> u x \<longrightarrow> f x j = j*2^j) \<and> |
228 |
(u x < of_nat j \<longrightarrow> of_nat (f x j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f x j)))" |
|
229 |
(is "\<exists>f. \<forall>x j. ?P x j (f x j)") |
|
230 |
proof(rule choice, rule, rule choice, rule) |
|
231 |
fix x j show "\<exists>n. ?P x j n" |
|
232 |
proof cases |
|
233 |
assume *: "u x < of_nat j" |
|
234 |
then obtain r where r: "u x = Real r" "0 \<le> r" by (cases "u x") auto |
|
235 |
from reals_Archimedean6a[of "r * 2^j"] |
|
236 |
obtain n :: nat where "real n \<le> r * 2 ^ j" "r * 2 ^ j < real (Suc n)" |
|
237 |
using `0 \<le> r` by (auto simp: zero_le_power zero_le_mult_iff) |
|
238 |
thus ?thesis using r * by (auto intro!: exI[of _ n]) |
|
239 |
qed auto |
|
35582 | 240 |
qed |
38656 | 241 |
then obtain f where top: "\<And>j x. of_nat j \<le> u x \<Longrightarrow> f x j = j*2^j" and |
242 |
upper: "\<And>j x. u x < of_nat j \<Longrightarrow> of_nat (f x j) \<le> u x * 2^j" and |
|
243 |
lower: "\<And>j x. u x < of_nat j \<Longrightarrow> u x * 2^j < of_nat (Suc (f x j))" by blast |
|
35582 | 244 |
|
38656 | 245 |
{ fix j x P |
246 |
assume 1: "of_nat j \<le> u x \<Longrightarrow> P (j * 2^j)" |
|
247 |
assume 2: "\<And>k. \<lbrakk> u x < of_nat j ; of_nat k \<le> u x * 2^j ; u x * 2^j < of_nat (Suc k) \<rbrakk> \<Longrightarrow> P k" |
|
248 |
have "P (f x j)" |
|
249 |
proof cases |
|
250 |
assume "of_nat j \<le> u x" thus "P (f x j)" |
|
251 |
using top[of j x] 1 by auto |
|
252 |
next |
|
253 |
assume "\<not> of_nat j \<le> u x" |
|
254 |
hence "u x < of_nat j" "of_nat (f x j) \<le> u x * 2^j" "u x * 2^j < of_nat (Suc (f x j))" |
|
255 |
using upper lower by auto |
|
256 |
from 2[OF this] show "P (f x j)" . |
|
257 |
qed } |
|
258 |
note fI = this |
|
259 |
||
260 |
{ fix j x |
|
261 |
have "f x j = j * 2 ^ j \<longleftrightarrow> of_nat j \<le> u x" |
|
262 |
by (rule fI, simp, cases "u x") (auto split: split_if_asm) } |
|
263 |
note f_eq = this |
|
35582 | 264 |
|
38656 | 265 |
{ fix j x |
266 |
have "f x j \<le> j * 2 ^ j" |
|
267 |
proof (rule fI) |
|
268 |
fix k assume *: "u x < of_nat j" |
|
269 |
assume "of_nat k \<le> u x * 2 ^ j" |
|
270 |
also have "\<dots> \<le> of_nat (j * 2^j)" |
|
271 |
using * by (cases "u x") (auto simp: zero_le_mult_iff) |
|
272 |
finally show "k \<le> j*2^j" by (auto simp del: real_of_nat_mult) |
|
273 |
qed simp } |
|
274 |
note f_upper = this |
|
35582 | 275 |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
276 |
let "?g j x" = "of_nat (f x j) / 2^j :: pextreal" |
38656 | 277 |
show ?thesis unfolding simple_function_def isoton_fun_expand unfolding isoton_def |
278 |
proof (safe intro!: exI[of _ ?g]) |
|
279 |
fix j |
|
280 |
have *: "?g j ` space M \<subseteq> (\<lambda>x. of_nat x / 2^j) ` {..j * 2^j}" |
|
281 |
using f_upper by auto |
|
282 |
thus "finite (?g j ` space M)" by (rule finite_subset) auto |
|
283 |
next |
|
284 |
fix j t assume "t \<in> space M" |
|
285 |
have **: "?g j -` {?g j t} \<inter> space M = {x \<in> space M. f t j = f x j}" |
|
286 |
by (auto simp: power_le_zero_eq Real_eq_Real mult_le_0_iff) |
|
35582 | 287 |
|
38656 | 288 |
show "?g j -` {?g j t} \<inter> space M \<in> sets M" |
289 |
proof cases |
|
290 |
assume "of_nat j \<le> u t" |
|
291 |
hence "?g j -` {?g j t} \<inter> space M = {x\<in>space M. of_nat j \<le> u x}" |
|
292 |
unfolding ** f_eq[symmetric] by auto |
|
293 |
thus "?g j -` {?g j t} \<inter> space M \<in> sets M" |
|
294 |
using u by auto |
|
35582 | 295 |
next |
38656 | 296 |
assume not_t: "\<not> of_nat j \<le> u t" |
297 |
hence less: "f t j < j*2^j" using f_eq[symmetric] `f t j \<le> j*2^j` by auto |
|
298 |
have split_vimage: "?g j -` {?g j t} \<inter> space M = |
|
299 |
{x\<in>space M. of_nat (f t j)/2^j \<le> u x} \<inter> {x\<in>space M. u x < of_nat (Suc (f t j))/2^j}" |
|
300 |
unfolding ** |
|
301 |
proof safe |
|
302 |
fix x assume [simp]: "f t j = f x j" |
|
303 |
have *: "\<not> of_nat j \<le> u x" using not_t f_eq[symmetric] by simp |
|
304 |
hence "of_nat (f t j) \<le> u x * 2^j \<and> u x * 2^j < of_nat (Suc (f t j))" |
|
305 |
using upper lower by auto |
|
306 |
hence "of_nat (f t j) / 2^j \<le> u x \<and> u x < of_nat (Suc (f t j))/2^j" using * |
|
307 |
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) |
|
308 |
thus "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" by auto |
|
309 |
next |
|
310 |
fix x |
|
311 |
assume "of_nat (f t j) / 2^j \<le> u x" "u x < of_nat (Suc (f t j))/2^j" |
|
312 |
hence "of_nat (f t j) \<le> u x * 2 ^ j \<and> u x * 2 ^ j < of_nat (Suc (f t j))" |
|
313 |
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) |
|
314 |
hence 1: "of_nat (f t j) \<le> u x * 2 ^ j" and 2: "u x * 2 ^ j < of_nat (Suc (f t j))" by auto |
|
315 |
note 2 |
|
316 |
also have "\<dots> \<le> of_nat (j*2^j)" |
|
317 |
using less by (auto simp: zero_le_mult_iff simp del: real_of_nat_mult) |
|
318 |
finally have bound_ux: "u x < of_nat j" |
|
319 |
by (cases "u x") (auto simp: zero_le_mult_iff power_le_zero_eq) |
|
320 |
show "f t j = f x j" |
|
321 |
proof (rule antisym) |
|
322 |
from 1 lower[OF bound_ux] |
|
323 |
show "f t j \<le> f x j" by (cases "u x") (auto split: split_if_asm) |
|
324 |
from upper[OF bound_ux] 2 |
|
325 |
show "f x j \<le> f t j" by (cases "u x") (auto split: split_if_asm) |
|
326 |
qed |
|
327 |
qed |
|
328 |
show ?thesis unfolding split_vimage using u by auto |
|
35582 | 329 |
qed |
38656 | 330 |
next |
331 |
fix j t assume "?g j t = \<omega>" thus False by (auto simp: power_le_zero_eq) |
|
332 |
next |
|
333 |
fix t |
|
334 |
{ fix i |
|
335 |
have "f t i * 2 \<le> f t (Suc i)" |
|
336 |
proof (rule fI) |
|
337 |
assume "of_nat (Suc i) \<le> u t" |
|
338 |
hence "of_nat i \<le> u t" by (cases "u t") auto |
|
339 |
thus "f t i * 2 \<le> Suc i * 2 ^ Suc i" unfolding f_eq[symmetric] by simp |
|
340 |
next |
|
341 |
fix k |
|
342 |
assume *: "u t * 2 ^ Suc i < of_nat (Suc k)" |
|
343 |
show "f t i * 2 \<le> k" |
|
344 |
proof (rule fI) |
|
345 |
assume "of_nat i \<le> u t" |
|
346 |
hence "of_nat (i * 2^Suc i) \<le> u t * 2^Suc i" |
|
347 |
by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) |
|
348 |
also have "\<dots> < of_nat (Suc k)" using * by auto |
|
349 |
finally show "i * 2 ^ i * 2 \<le> k" |
|
350 |
by (auto simp del: real_of_nat_mult) |
|
351 |
next |
|
352 |
fix j assume "of_nat j \<le> u t * 2 ^ i" |
|
353 |
with * show "j * 2 \<le> k" by (cases "u t") (auto simp: zero_le_mult_iff power_le_zero_eq) |
|
354 |
qed |
|
355 |
qed |
|
356 |
thus "?g i t \<le> ?g (Suc i) t" |
|
357 |
by (auto simp: zero_le_mult_iff power_le_zero_eq divide_real_def[symmetric] field_simps) } |
|
358 |
hence mono: "mono (\<lambda>i. ?g i t)" unfolding mono_iff_le_Suc by auto |
|
35582 | 359 |
|
38656 | 360 |
show "(SUP j. of_nat (f t j) / 2 ^ j) = u t" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
361 |
proof (rule pextreal_SUPI) |
38656 | 362 |
fix j show "of_nat (f t j) / 2 ^ j \<le> u t" |
363 |
proof (rule fI) |
|
364 |
assume "of_nat j \<le> u t" thus "of_nat (j * 2 ^ j) / 2 ^ j \<le> u t" |
|
365 |
by (cases "u t") (auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps) |
|
366 |
next |
|
367 |
fix k assume "of_nat k \<le> u t * 2 ^ j" |
|
368 |
thus "of_nat k / 2 ^ j \<le> u t" |
|
369 |
by (cases "u t") |
|
370 |
(auto simp: power_le_zero_eq divide_real_def[symmetric] field_simps zero_le_mult_iff) |
|
371 |
qed |
|
372 |
next |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
373 |
fix y :: pextreal assume *: "\<And>j. j \<in> UNIV \<Longrightarrow> of_nat (f t j) / 2 ^ j \<le> y" |
38656 | 374 |
show "u t \<le> y" |
375 |
proof (cases "u t") |
|
376 |
case (preal r) |
|
377 |
show ?thesis |
|
378 |
proof (rule ccontr) |
|
379 |
assume "\<not> u t \<le> y" |
|
380 |
then obtain p where p: "y = Real p" "0 \<le> p" "p < r" using preal by (cases y) auto |
|
381 |
with LIMSEQ_inverse_realpow_zero[of 2, unfolded LIMSEQ_iff, rule_format, of "r - p"] |
|
382 |
obtain n where n: "\<And>N. n \<le> N \<Longrightarrow> inverse (2^N) < r - p" by auto |
|
383 |
let ?N = "max n (natfloor r + 1)" |
|
384 |
have "u t < of_nat ?N" "n \<le> ?N" |
|
385 |
using ge_natfloor_plus_one_imp_gt[of r n] preal |
|
38705 | 386 |
using real_natfloor_add_one_gt |
387 |
by (auto simp: max_def real_of_nat_Suc) |
|
38656 | 388 |
from lower[OF this(1)] |
389 |
have "r < (real (f t ?N) + 1) / 2 ^ ?N" unfolding less_divide_eq |
|
390 |
using preal by (auto simp add: power_le_zero_eq zero_le_mult_iff real_of_nat_Suc split: split_if_asm) |
|
391 |
hence "u t < of_nat (f t ?N) / 2 ^ ?N + 1 / 2 ^ ?N" |
|
392 |
using preal by (auto simp: field_simps divide_real_def[symmetric]) |
|
393 |
with n[OF `n \<le> ?N`] p preal *[of ?N] |
|
394 |
show False |
|
395 |
by (cases "f t ?N") (auto simp: power_le_zero_eq split: split_if_asm) |
|
396 |
qed |
|
397 |
next |
|
398 |
case infinite |
|
399 |
{ fix j have "f t j = j*2^j" using top[of j t] infinite by simp |
|
400 |
hence "of_nat j \<le> y" using *[of j] |
|
401 |
by (cases y) (auto simp: power_le_zero_eq zero_le_mult_iff field_simps) } |
|
402 |
note all_less_y = this |
|
403 |
show ?thesis unfolding infinite |
|
404 |
proof (rule ccontr) |
|
405 |
assume "\<not> \<omega> \<le> y" then obtain r where r: "y = Real r" "0 \<le> r" by (cases y) auto |
|
406 |
moreover obtain n ::nat where "r < real n" using ex_less_of_nat by (auto simp: real_eq_of_nat) |
|
407 |
with all_less_y[of n] r show False by auto |
|
408 |
qed |
|
409 |
qed |
|
410 |
qed |
|
35582 | 411 |
qed |
412 |
qed |
|
413 |
||
38656 | 414 |
lemma (in sigma_algebra) borel_measurable_implies_simple_function_sequence': |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
415 |
fixes u :: "'a \<Rightarrow> pextreal" |
38656 | 416 |
assumes "u \<in> borel_measurable M" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
417 |
obtains (x) f where "f \<up> u" "\<And>i. simple_function M (f i)" "\<And>i. \<omega>\<notin>f i`space M" |
35582 | 418 |
proof - |
38656 | 419 |
from borel_measurable_implies_simple_function_sequence[OF assms] |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
420 |
obtain f where x: "\<And>i. simple_function M (f i)" "f \<up> u" |
38656 | 421 |
and fin: "\<And>i. \<And>x. x\<in>space M \<Longrightarrow> f i x \<noteq> \<omega>" by auto |
422 |
{ fix i from fin[of _ i] have "\<omega> \<notin> f i`space M" by fastsimp } |
|
423 |
with x show thesis by (auto intro!: that[of f]) |
|
424 |
qed |
|
425 |
||
39092 | 426 |
lemma (in sigma_algebra) simple_function_eq_borel_measurable: |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
427 |
fixes f :: "'a \<Rightarrow> pextreal" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
428 |
shows "simple_function M f \<longleftrightarrow> |
39092 | 429 |
finite (f`space M) \<and> f \<in> borel_measurable M" |
430 |
using simple_function_borel_measurable[of f] |
|
431 |
borel_measurable_simple_function[of f] |
|
432 |
by (fastsimp simp: simple_function_def) |
|
433 |
||
434 |
lemma (in measure_space) simple_function_restricted: |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
435 |
fixes f :: "'a \<Rightarrow> pextreal" assumes "A \<in> 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:
41661
diff
changeset
|
436 |
shows "simple_function (restricted_space A) f \<longleftrightarrow> simple_function M (\<lambda>x. f x * indicator A x)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
437 |
(is "simple_function ?R f \<longleftrightarrow> simple_function M ?f") |
39092 | 438 |
proof - |
439 |
interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`]) |
|
440 |
have "finite (f`A) \<longleftrightarrow> finite (?f`space M)" |
|
441 |
proof cases |
|
442 |
assume "A = space M" |
|
443 |
then have "f`A = ?f`space M" by (fastsimp simp: image_iff) |
|
444 |
then show ?thesis by simp |
|
445 |
next |
|
446 |
assume "A \<noteq> space M" |
|
447 |
then obtain x where x: "x \<in> space M" "x \<notin> A" |
|
448 |
using sets_into_space `A \<in> sets M` by auto |
|
449 |
have *: "?f`space M = f`A \<union> {0}" |
|
450 |
proof (auto simp add: image_iff) |
|
451 |
show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0" |
|
452 |
using x by (auto intro!: bexI[of _ x]) |
|
453 |
next |
|
454 |
fix x assume "x \<in> A" |
|
455 |
then show "\<exists>y\<in>space M. f x = f y * indicator A y" |
|
456 |
using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x]) |
|
457 |
next |
|
458 |
fix x |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
459 |
assume "indicator A x \<noteq> (0::pextreal)" |
39092 | 460 |
then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm) |
461 |
moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y" |
|
462 |
ultimately show "f x = 0" by auto |
|
463 |
qed |
|
464 |
then show ?thesis by auto |
|
465 |
qed |
|
466 |
then show ?thesis |
|
467 |
unfolding simple_function_eq_borel_measurable |
|
468 |
R.simple_function_eq_borel_measurable |
|
469 |
unfolding borel_measurable_restricted[OF `A \<in> sets M`] |
|
470 |
by auto |
|
471 |
qed |
|
472 |
||
473 |
lemma (in sigma_algebra) simple_function_subalgebra: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
474 |
assumes "simple_function N f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
475 |
and N_subalgebra: "sets N \<subseteq> sets M" "space N = space M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
476 |
shows "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
477 |
using assms unfolding simple_function_def by auto |
39092 | 478 |
|
41661 | 479 |
lemma (in measure_space) simple_function_vimage: |
480 |
assumes T: "sigma_algebra M'" "T \<in> measurable M M'" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
481 |
and f: "simple_function M' f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
482 |
shows "simple_function M (\<lambda>x. f (T x))" |
41661 | 483 |
proof (intro simple_function_def[THEN iffD2] conjI ballI) |
484 |
interpret T: sigma_algebra M' by fact |
|
485 |
have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'" |
|
486 |
using T unfolding measurable_def by auto |
|
487 |
then show "finite ((\<lambda>x. f (T x)) ` space M)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
488 |
using f unfolding simple_function_def by (auto intro: finite_subset) |
41661 | 489 |
fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M" |
490 |
then have "i \<in> f ` space M'" |
|
491 |
using T unfolding measurable_def by auto |
|
492 |
then have "f -` {i} \<inter> space M' \<in> 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:
41661
diff
changeset
|
493 |
using f unfolding simple_function_def by auto |
41661 | 494 |
then have "T -` (f -` {i} \<inter> space M') \<inter> space M \<in> sets M" |
495 |
using T unfolding measurable_def by auto |
|
496 |
also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M" |
|
497 |
using T unfolding measurable_def by auto |
|
498 |
finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" . |
|
40859 | 499 |
qed |
500 |
||
38656 | 501 |
section "Simple integral" |
502 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
503 |
definition simple_integral_def: |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
504 |
"integral\<^isup>S M f = (\<Sum>x \<in> f ` space M. x * measure M (f -` {x} \<inter> space M))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
505 |
|
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
506 |
syntax |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
507 |
"_simple_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> pextreal) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> pextreal" ("\<integral>\<^isup>S _. _ \<partial>_" [60,61] 110) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
508 |
|
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
509 |
translations |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
510 |
"\<integral>\<^isup>S x. f \<partial>M" == "CONST integral\<^isup>S M (%x. f)" |
35582 | 511 |
|
38656 | 512 |
lemma (in measure_space) simple_integral_cong: |
513 |
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
514 |
shows "integral\<^isup>S M f = integral\<^isup>S M g" |
38656 | 515 |
proof - |
516 |
have "f ` space M = g ` space M" |
|
517 |
"\<And>x. f -` {x} \<inter> space M = g -` {x} \<inter> space M" |
|
518 |
using assms by (auto intro!: image_eqI) |
|
519 |
thus ?thesis unfolding simple_integral_def by simp |
|
520 |
qed |
|
521 |
||
40859 | 522 |
lemma (in measure_space) simple_integral_cong_measure: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
523 |
assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
524 |
and "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
525 |
shows "integral\<^isup>S N f = integral\<^isup>S M f" |
40859 | 526 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
527 |
interpret v: measure_space N |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
528 |
by (rule measure_space_cong) fact+ |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
529 |
from simple_functionD[OF `simple_function M f`] assms show ?thesis |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
530 |
by (auto intro!: setsum_cong simp: simple_integral_def) |
40859 | 531 |
qed |
532 |
||
38656 | 533 |
lemma (in measure_space) simple_integral_const[simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
534 |
"(\<integral>\<^isup>Sx. c \<partial>M) = c * \<mu> (space M)" |
38656 | 535 |
proof (cases "space M = {}") |
536 |
case True thus ?thesis unfolding simple_integral_def by simp |
|
537 |
next |
|
538 |
case False hence "(\<lambda>x. c) ` space M = {c}" by auto |
|
539 |
thus ?thesis unfolding simple_integral_def by simp |
|
35582 | 540 |
qed |
541 |
||
38656 | 542 |
lemma (in measure_space) simple_function_partition: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
543 |
assumes "simple_function M f" and "simple_function M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
544 |
shows "integral\<^isup>S M f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)" |
38656 | 545 |
(is "_ = setsum _ (?p ` space M)") |
546 |
proof- |
|
547 |
let "?sub x" = "?p ` (f -` {x} \<inter> space M)" |
|
548 |
let ?SIGMA = "Sigma (f`space M) ?sub" |
|
35582 | 549 |
|
38656 | 550 |
have [intro]: |
551 |
"finite (f ` space M)" |
|
552 |
"finite (g ` space M)" |
|
553 |
using assms unfolding simple_function_def by simp_all |
|
554 |
||
555 |
{ fix A |
|
556 |
have "?p ` (A \<inter> space M) \<subseteq> |
|
557 |
(\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)" |
|
558 |
by auto |
|
559 |
hence "finite (?p ` (A \<inter> space M))" |
|
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
39910
diff
changeset
|
560 |
by (rule finite_subset) auto } |
38656 | 561 |
note this[intro, simp] |
35582 | 562 |
|
38656 | 563 |
{ fix x assume "x \<in> space M" |
564 |
have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto |
|
565 |
moreover { |
|
566 |
fix x y |
|
567 |
have *: "f -` {f x} \<inter> g -` {g x} \<inter> space M |
|
568 |
= (f -` {f x} \<inter> space M) \<inter> (g -` {g x} \<inter> space M)" by auto |
|
569 |
assume "x \<in> space M" "y \<in> space M" |
|
570 |
hence "f -` {f x} \<inter> g -` {g x} \<inter> space M \<in> sets M" |
|
571 |
using assms unfolding simple_function_def * by auto } |
|
572 |
ultimately |
|
573 |
have "\<mu> (f -` {f x} \<inter> space M) = setsum (\<mu>) (?sub (f x))" |
|
574 |
by (subst measure_finitely_additive) auto } |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
575 |
hence "integral\<^isup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * \<mu> A)" |
38656 | 576 |
unfolding simple_integral_def |
577 |
by (subst setsum_Sigma[symmetric], |
|
578 |
auto intro!: setsum_cong simp: setsum_right_distrib[symmetric]) |
|
39910 | 579 |
also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)" |
38656 | 580 |
proof - |
581 |
have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI) |
|
39910 | 582 |
have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M |
38656 | 583 |
= (\<lambda>x. (f x, ?p x)) ` space M" |
584 |
proof safe |
|
585 |
fix x assume "x \<in> space M" |
|
39910 | 586 |
thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M" |
38656 | 587 |
by (auto intro!: image_eqI[of _ _ "?p x"]) |
588 |
qed auto |
|
589 |
thus ?thesis |
|
39910 | 590 |
apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI) |
38656 | 591 |
apply (rule_tac x="xa" in image_eqI) |
592 |
by simp_all |
|
593 |
qed |
|
594 |
finally show ?thesis . |
|
35582 | 595 |
qed |
596 |
||
38656 | 597 |
lemma (in measure_space) simple_integral_add[simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
598 |
assumes "simple_function M f" and "simple_function M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
599 |
shows "(\<integral>\<^isup>Sx. f x + g x \<partial>M) = integral\<^isup>S M f + integral\<^isup>S M g" |
35582 | 600 |
proof - |
38656 | 601 |
{ fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M" |
602 |
assume "x \<in> space M" |
|
603 |
hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" |
|
604 |
"(\<lambda>x. (f x, g x)) -` {(f x, g x)} \<inter> space M = ?S" |
|
605 |
by auto } |
|
606 |
thus ?thesis |
|
607 |
unfolding |
|
608 |
simple_function_partition[OF simple_function_add[OF assms] simple_function_Pair[OF assms]] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
609 |
simple_function_partition[OF `simple_function M f` `simple_function M g`] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
610 |
simple_function_partition[OF `simple_function M g` `simple_function M f`] |
38656 | 611 |
apply (subst (3) Int_commute) |
612 |
by (auto simp add: field_simps setsum_addf[symmetric] intro!: setsum_cong) |
|
35582 | 613 |
qed |
614 |
||
38656 | 615 |
lemma (in measure_space) simple_integral_setsum[simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
616 |
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
617 |
shows "(\<integral>\<^isup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>S M (f i))" |
38656 | 618 |
proof cases |
619 |
assume "finite P" |
|
620 |
from this assms show ?thesis |
|
621 |
by induct (auto simp: simple_function_setsum simple_integral_add) |
|
622 |
qed auto |
|
623 |
||
624 |
lemma (in measure_space) simple_integral_mult[simp]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
625 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
626 |
shows "(\<integral>\<^isup>Sx. c * f x \<partial>M) = c * integral\<^isup>S M f" |
38656 | 627 |
proof - |
628 |
note mult = simple_function_mult[OF simple_function_const[of c] assms] |
|
629 |
{ fix x let ?S = "f -` {f x} \<inter> (\<lambda>x. c * f x) -` {c * f x} \<inter> space M" |
|
630 |
assume "x \<in> space M" |
|
631 |
hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" |
|
632 |
by auto } |
|
633 |
thus ?thesis |
|
634 |
unfolding simple_function_partition[OF mult assms] |
|
635 |
simple_function_partition[OF assms mult] |
|
636 |
by (auto simp: setsum_right_distrib field_simps intro!: setsum_cong) |
|
35582 | 637 |
qed |
638 |
||
40871 | 639 |
lemma (in sigma_algebra) simple_function_If: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
640 |
assumes sf: "simple_function M f" "simple_function M g" and A: "A \<in> sets M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
641 |
shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF") |
40871 | 642 |
proof - |
643 |
def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M" |
|
644 |
show ?thesis unfolding simple_function_def |
|
645 |
proof safe |
|
646 |
have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto |
|
647 |
from finite_subset[OF this] assms |
|
648 |
show "finite (?IF ` space M)" unfolding simple_function_def by auto |
|
649 |
next |
|
650 |
fix x assume "x \<in> space M" |
|
651 |
then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A |
|
652 |
then ((F (f x) \<inter> A) \<union> (G (f x) - (G (f x) \<inter> A))) |
|
653 |
else ((F (g x) \<inter> A) \<union> (G (g x) - (G (g x) \<inter> A))))" |
|
654 |
using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) |
|
655 |
have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M" |
|
656 |
unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto |
|
657 |
show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto |
|
658 |
qed |
|
659 |
qed |
|
660 |
||
40859 | 661 |
lemma (in measure_space) simple_integral_mono_AE: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
662 |
assumes "simple_function M f" and "simple_function M g" |
40859 | 663 |
and mono: "AE x. f x \<le> g x" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
664 |
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g" |
40859 | 665 |
proof - |
666 |
let "?S x" = "(g -` {g x} \<inter> space M) \<inter> (f -` {f x} \<inter> space M)" |
|
667 |
have *: "\<And>x. g -` {g x} \<inter> f -` {f x} \<inter> space M = ?S x" |
|
668 |
"\<And>x. f -` {f x} \<inter> g -` {g x} \<inter> space M = ?S x" by auto |
|
669 |
show ?thesis |
|
670 |
unfolding * |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
671 |
simple_function_partition[OF `simple_function M f` `simple_function M g`] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
672 |
simple_function_partition[OF `simple_function M g` `simple_function M f`] |
40859 | 673 |
proof (safe intro!: setsum_mono) |
674 |
fix x assume "x \<in> space M" |
|
675 |
then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto |
|
676 |
show "the_elem (f`?S x) * \<mu> (?S x) \<le> the_elem (g`?S x) * \<mu> (?S x)" |
|
677 |
proof (cases "f x \<le> g x") |
|
678 |
case True then show ?thesis using * by (auto intro!: mult_right_mono) |
|
679 |
next |
|
680 |
case False |
|
681 |
obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "\<mu> N = 0" |
|
682 |
using mono by (auto elim!: AE_E) |
|
683 |
have "?S x \<subseteq> N" using N `x \<in> space M` False by auto |
|
40871 | 684 |
moreover have "?S x \<in> sets M" using assms |
685 |
by (rule_tac Int) (auto intro!: simple_functionD) |
|
40859 | 686 |
ultimately have "\<mu> (?S x) \<le> \<mu> N" |
687 |
using `N \<in> sets M` by (auto intro!: measure_mono) |
|
688 |
then show ?thesis using `\<mu> N = 0` by auto |
|
689 |
qed |
|
690 |
qed |
|
691 |
qed |
|
692 |
||
38656 | 693 |
lemma (in measure_space) simple_integral_mono: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
694 |
assumes "simple_function M f" and "simple_function M g" |
38656 | 695 |
and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
696 |
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g" |
41705 | 697 |
using assms by (intro simple_integral_mono_AE) auto |
35582 | 698 |
|
40859 | 699 |
lemma (in measure_space) simple_integral_cong_AE: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
700 |
assumes "simple_function M f" "simple_function M g" and "AE x. f x = g x" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
701 |
shows "integral\<^isup>S M f = integral\<^isup>S M g" |
40859 | 702 |
using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) |
703 |
||
704 |
lemma (in measure_space) simple_integral_cong': |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
705 |
assumes sf: "simple_function M f" "simple_function M g" |
40859 | 706 |
and mea: "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
707 |
shows "integral\<^isup>S M f = integral\<^isup>S M g" |
40859 | 708 |
proof (intro simple_integral_cong_AE sf AE_I) |
709 |
show "\<mu> {x\<in>space M. f x \<noteq> g x} = 0" by fact |
|
710 |
show "{x \<in> space M. f x \<noteq> g x} \<in> sets M" |
|
711 |
using sf[THEN borel_measurable_simple_function] by auto |
|
712 |
qed simp |
|
713 |
||
38656 | 714 |
lemma (in measure_space) simple_integral_indicator: |
715 |
assumes "A \<in> 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:
41661
diff
changeset
|
716 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
717 |
shows "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = |
38656 | 718 |
(\<Sum>x \<in> f ` space M. x * \<mu> (f -` {x} \<inter> space M \<inter> A))" |
719 |
proof cases |
|
720 |
assume "A = space M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
721 |
moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = integral\<^isup>S M f" |
38656 | 722 |
by (auto intro!: simple_integral_cong) |
723 |
moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto |
|
724 |
ultimately show ?thesis by (simp add: simple_integral_def) |
|
725 |
next |
|
726 |
assume "A \<noteq> space M" |
|
727 |
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto |
|
728 |
have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _") |
|
35582 | 729 |
proof safe |
38656 | 730 |
fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto |
731 |
next |
|
732 |
fix y assume "y \<in> A" thus "f y \<in> ?I ` space M" |
|
733 |
using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) |
|
734 |
next |
|
735 |
show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) |
|
35582 | 736 |
qed |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
737 |
have *: "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = |
38656 | 738 |
(\<Sum>x \<in> f ` space M \<union> {0}. x * \<mu> (f -` {x} \<inter> space M \<inter> A))" |
739 |
unfolding simple_integral_def I |
|
740 |
proof (rule setsum_mono_zero_cong_left) |
|
741 |
show "finite (f ` space M \<union> {0})" |
|
742 |
using assms(2) unfolding simple_function_def by auto |
|
743 |
show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}" |
|
744 |
using sets_into_space[OF assms(1)] by auto |
|
40859 | 745 |
have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}" |
746 |
by (auto simp: image_iff) |
|
38656 | 747 |
thus "\<forall>i\<in>f ` space M \<union> {0} - (f ` A \<union> {0}). |
748 |
i * \<mu> (f -` {i} \<inter> space M \<inter> A) = 0" by auto |
|
749 |
next |
|
750 |
fix x assume "x \<in> f`A \<union> {0}" |
|
751 |
hence "x \<noteq> 0 \<Longrightarrow> ?I -` {x} \<inter> space M = f -` {x} \<inter> space M \<inter> A" |
|
752 |
by (auto simp: indicator_def split: split_if_asm) |
|
753 |
thus "x * \<mu> (?I -` {x} \<inter> space M) = |
|
754 |
x * \<mu> (f -` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all |
|
755 |
qed |
|
756 |
show ?thesis unfolding * |
|
757 |
using assms(2) unfolding simple_function_def |
|
758 |
by (auto intro!: setsum_mono_zero_cong_right) |
|
759 |
qed |
|
35582 | 760 |
|
38656 | 761 |
lemma (in measure_space) simple_integral_indicator_only[simp]: |
762 |
assumes "A \<in> 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:
41661
diff
changeset
|
763 |
shows "integral\<^isup>S M (indicator A) = \<mu> A" |
38656 | 764 |
proof cases |
765 |
assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto |
|
766 |
thus ?thesis unfolding simple_integral_def using `space M = {}` by auto |
|
767 |
next |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
768 |
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::pextreal}" by auto |
38656 | 769 |
thus ?thesis |
770 |
using simple_integral_indicator[OF assms simple_function_const[of 1]] |
|
771 |
using sets_into_space[OF assms] |
|
772 |
by (auto intro!: arg_cong[where f="\<mu>"]) |
|
773 |
qed |
|
35582 | 774 |
|
38656 | 775 |
lemma (in measure_space) simple_integral_null_set: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
776 |
assumes "simple_function M u" "N \<in> null_sets" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
777 |
shows "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = 0" |
38656 | 778 |
proof - |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
779 |
have "AE x. indicator N x = (0 :: pextreal)" |
40859 | 780 |
using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
781 |
then have "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^isup>Sx. 0 \<partial>M)" |
41705 | 782 |
using assms by (intro simple_integral_cong_AE) auto |
40859 | 783 |
then show ?thesis by simp |
38656 | 784 |
qed |
35582 | 785 |
|
40859 | 786 |
lemma (in measure_space) simple_integral_cong_AE_mult_indicator: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
787 |
assumes sf: "simple_function M f" and eq: "AE x. x \<in> S" and "S \<in> sets M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
788 |
shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)" |
41705 | 789 |
using assms by (intro simple_integral_cong_AE) auto |
35582 | 790 |
|
39092 | 791 |
lemma (in measure_space) simple_integral_restricted: |
792 |
assumes "A \<in> 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:
41661
diff
changeset
|
793 |
assumes sf: "simple_function M (\<lambda>x. f x * indicator A x)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
794 |
shows "integral\<^isup>S (restricted_space A) f = (\<integral>\<^isup>Sx. f x * indicator A x \<partial>M)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
795 |
(is "_ = integral\<^isup>S M ?f") |
39092 | 796 |
unfolding simple_integral_def |
797 |
proof (simp, safe intro!: setsum_mono_zero_cong_left) |
|
798 |
from sf show "finite (?f ` space M)" |
|
799 |
unfolding simple_function_def by auto |
|
800 |
next |
|
801 |
fix x assume "x \<in> A" |
|
802 |
then show "f x \<in> ?f ` space M" |
|
803 |
using sets_into_space `A \<in> sets M` by (auto intro!: image_eqI[of _ _ x]) |
|
804 |
next |
|
805 |
fix x assume "x \<in> space M" "?f x \<notin> f`A" |
|
806 |
then have "x \<notin> A" by (auto simp: image_iff) |
|
807 |
then show "?f x * \<mu> (?f -` {?f x} \<inter> space M) = 0" by simp |
|
808 |
next |
|
809 |
fix x assume "x \<in> A" |
|
810 |
then have "f x \<noteq> 0 \<Longrightarrow> |
|
811 |
f -` {f x} \<inter> A = ?f -` {f x} \<inter> space M" |
|
812 |
using `A \<in> sets M` sets_into_space |
|
813 |
by (auto simp: indicator_def split: split_if_asm) |
|
814 |
then show "f x * \<mu> (f -` {f x} \<inter> A) = |
|
815 |
f x * \<mu> (?f -` {f x} \<inter> space M)" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
816 |
unfolding pextreal_mult_cancel_left by auto |
39092 | 817 |
qed |
818 |
||
41545 | 819 |
lemma (in measure_space) simple_integral_subalgebra: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
820 |
assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
821 |
shows "integral\<^isup>S N = integral\<^isup>S M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
822 |
unfolding simple_integral_def_raw by simp |
39092 | 823 |
|
41831 | 824 |
lemma measure_preservingD: |
825 |
"T \<in> measure_preserving A B \<Longrightarrow> X \<in> sets B \<Longrightarrow> measure A (T -` X \<inter> space A) = measure B X" |
|
826 |
unfolding measure_preserving_def by auto |
|
827 |
||
40859 | 828 |
lemma (in measure_space) simple_integral_vimage: |
41831 | 829 |
assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
830 |
and f: "simple_function M' f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
831 |
shows "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)" |
40859 | 832 |
proof - |
41831 | 833 |
interpret T: measure_space M' by (rule measure_space_vimage[OF T]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
834 |
show "integral\<^isup>S M' f = (\<integral>\<^isup>S x. f (T x) \<partial>M)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
835 |
unfolding simple_integral_def |
41661 | 836 |
proof (intro setsum_mono_zero_cong_right ballI) |
837 |
show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'" |
|
41831 | 838 |
using T unfolding measurable_def measure_preserving_def by auto |
41661 | 839 |
show "finite (f ` space M')" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
840 |
using f unfolding simple_function_def by auto |
41661 | 841 |
next |
842 |
fix i assume "i \<in> f ` space M' - (\<lambda>x. f (T x)) ` space M" |
|
843 |
then have "T -` (f -` {i} \<inter> space M') \<inter> space M = {}" by (auto simp: image_iff) |
|
41831 | 844 |
with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"] |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
845 |
show "i * T.\<mu> (f -` {i} \<inter> space M') = 0" by simp |
41661 | 846 |
next |
847 |
fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M" |
|
848 |
then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M" |
|
41831 | 849 |
using T unfolding measurable_def measure_preserving_def by auto |
850 |
with f[THEN T.simple_functionD(2), THEN measure_preservingD[OF T(2)], of "{i}"] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
851 |
show "i * T.\<mu> (f -` {i} \<inter> space M') = i * \<mu> ((\<lambda>x. f (T x)) -` {i} \<inter> space M)" |
41661 | 852 |
by auto |
853 |
qed |
|
40859 | 854 |
qed |
855 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
856 |
section "Continuous positive integration" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
857 |
|
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
858 |
definition positive_integral_def: |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
859 |
"integral\<^isup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> f}. integral\<^isup>S M g)" |
35692 | 860 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
861 |
syntax |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
862 |
"_positive_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> pextreal) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> pextreal" ("\<integral>\<^isup>+ _. _ \<partial>_" [60,61] 110) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
863 |
|
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
864 |
translations |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
865 |
"\<integral>\<^isup>+ x. f \<partial>M" == "CONST integral\<^isup>P M (%x. f)" |
40872 | 866 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
867 |
lemma (in measure_space) positive_integral_alt: "integral\<^isup>P M f = |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
868 |
(SUP g : {g. simple_function M g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}. integral\<^isup>S M g)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
869 |
(is "_ = ?alt") |
40872 | 870 |
proof (rule antisym SUP_leI) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
871 |
show "integral\<^isup>P M f \<le> ?alt" unfolding positive_integral_def |
40872 | 872 |
proof (safe intro!: SUP_leI) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
873 |
fix g assume g: "simple_function M g" "g \<le> f" |
40872 | 874 |
let ?G = "g -` {\<omega>} \<inter> space M" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
875 |
show "integral\<^isup>S M g \<le> |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
876 |
(SUP h : {i. simple_function M i \<and> i \<le> f \<and> \<omega> \<notin> i ` space M}. integral\<^isup>S M h)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
877 |
(is "integral\<^isup>S M g \<le> SUPR ?A _") |
40872 | 878 |
proof cases |
879 |
let ?g = "\<lambda>x. indicator (space M - ?G) x * g x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
880 |
have g': "simple_function M ?g" |
40872 | 881 |
using g by (auto intro: simple_functionD) |
882 |
moreover |
|
883 |
assume "\<mu> ?G = 0" |
|
884 |
then have "AE x. g x = ?g x" using g |
|
885 |
by (intro AE_I[where N="?G"]) |
|
886 |
(auto intro: simple_functionD simp: indicator_def) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
887 |
with g(1) g' have "integral\<^isup>S M g = integral\<^isup>S M ?g" |
40872 | 888 |
by (rule simple_integral_cong_AE) |
889 |
moreover have "?g \<le> g" by (auto simp: le_fun_def indicator_def) |
|
890 |
from this `g \<le> f` have "?g \<le> f" by (rule order_trans) |
|
891 |
moreover have "\<omega> \<notin> ?g ` space M" |
|
892 |
by (auto simp: indicator_def split: split_if_asm) |
|
893 |
ultimately show ?thesis by (auto intro!: le_SUPI) |
|
894 |
next |
|
895 |
assume "\<mu> ?G \<noteq> 0" |
|
896 |
then have "?G \<noteq> {}" by auto |
|
897 |
then have "\<omega> \<in> g`space M" by force |
|
898 |
then have "space M \<noteq> {}" by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
899 |
have "SUPR ?A (integral\<^isup>S M) = \<omega>" |
40872 | 900 |
proof (intro SUP_\<omega>[THEN iffD2] allI impI) |
901 |
fix x assume "x < \<omega>" |
|
902 |
then guess n unfolding less_\<omega>_Ex_of_nat .. note n = this |
|
903 |
then have "0 < n" by (intro neq0_conv[THEN iffD1] notI) simp |
|
904 |
let ?g = "\<lambda>x. (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * indicator ?G x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
905 |
show "\<exists>i\<in>?A. x < integral\<^isup>S M i" |
40872 | 906 |
proof (intro bexI impI CollectI conjI) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
907 |
show "simple_function M ?g" using g |
40872 | 908 |
by (auto intro!: simple_functionD simple_function_add) |
909 |
have "?g \<le> g" by (auto simp: le_fun_def indicator_def) |
|
910 |
from this g(2) show "?g \<le> f" by (rule order_trans) |
|
911 |
show "\<omega> \<notin> ?g ` space M" |
|
912 |
using `\<mu> ?G \<noteq> 0` by (auto simp: indicator_def split: split_if_asm) |
|
913 |
have "x < (of_nat n / (if \<mu> ?G = \<omega> then 1 else \<mu> ?G)) * \<mu> ?G" |
|
914 |
using n `\<mu> ?G \<noteq> 0` `0 < n` |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
915 |
by (auto simp: pextreal_noteq_omega_Ex field_simps) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
916 |
also have "\<dots> = integral\<^isup>S M ?g" using g `space M \<noteq> {}` |
40872 | 917 |
by (subst simple_integral_indicator) |
918 |
(auto simp: image_constant ac_simps dest: simple_functionD) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
919 |
finally show "x < integral\<^isup>S M ?g" . |
40872 | 920 |
qed |
921 |
qed |
|
922 |
then show ?thesis by simp |
|
923 |
qed |
|
35582 | 924 |
qed |
40872 | 925 |
qed (auto intro!: SUP_subset simp: positive_integral_def) |
35582 | 926 |
|
40873 | 927 |
lemma (in measure_space) positive_integral_cong_measure: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
928 |
assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
929 |
shows "integral\<^isup>P N f = integral\<^isup>P M f" |
40873 | 930 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
931 |
interpret v: measure_space N |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
932 |
by (rule measure_space_cong) fact+ |
40873 | 933 |
with assms show ?thesis |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
934 |
unfolding positive_integral_def SUPR_def |
40873 | 935 |
by (auto intro!: arg_cong[where f=Sup] image_cong |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
936 |
simp: simple_integral_cong_measure[OF assms] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
937 |
simple_function_cong_algebra[OF assms(2,3)]) |
40873 | 938 |
qed |
939 |
||
940 |
lemma (in measure_space) positive_integral_alt1: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
941 |
"integral\<^isup>P M f = |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
942 |
(SUP g : {g. simple_function M g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}. integral\<^isup>S M g)" |
40873 | 943 |
unfolding positive_integral_alt SUPR_def |
944 |
proof (safe intro!: arg_cong[where f=Sup]) |
|
945 |
fix g let ?g = "\<lambda>x. if x \<in> space M then g x else f x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
946 |
assume "simple_function M g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
947 |
hence "?g \<le> f" "simple_function M ?g" "integral\<^isup>S M g = integral\<^isup>S M ?g" |
40873 | 948 |
"\<omega> \<notin> g`space M" |
949 |
unfolding le_fun_def by (auto cong: simple_function_cong simple_integral_cong) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
950 |
thus "integral\<^isup>S M g \<in> integral\<^isup>S M ` {g. simple_function M g \<and> g \<le> f \<and> \<omega> \<notin> g`space M}" |
40873 | 951 |
by auto |
952 |
next |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
953 |
fix g assume "simple_function M g" "g \<le> f" "\<omega> \<notin> g`space M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
954 |
hence "simple_function M g" "\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>" |
40873 | 955 |
by (auto simp add: le_fun_def image_iff) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
956 |
thus "integral\<^isup>S M g \<in> integral\<^isup>S M ` {g. simple_function M g \<and> (\<forall>x\<in>space M. g x \<le> f x \<and> g x \<noteq> \<omega>)}" |
40873 | 957 |
by auto |
958 |
qed |
|
959 |
||
38656 | 960 |
lemma (in measure_space) positive_integral_cong: |
961 |
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
962 |
shows "integral\<^isup>P M f = integral\<^isup>P M g" |
38656 | 963 |
proof - |
964 |
have "\<And>h. (\<forall>x\<in>space M. h x \<le> f x \<and> h x \<noteq> \<omega>) = (\<forall>x\<in>space M. h x \<le> g x \<and> h x \<noteq> \<omega>)" |
|
965 |
using assms by auto |
|
966 |
thus ?thesis unfolding positive_integral_alt1 by auto |
|
967 |
qed |
|
968 |
||
969 |
lemma (in measure_space) positive_integral_eq_simple_integral: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
970 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
971 |
shows "integral\<^isup>P M f = integral\<^isup>S M f" |
40873 | 972 |
unfolding positive_integral_def |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
973 |
proof (safe intro!: pextreal_SUPI) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
974 |
fix g assume "simple_function M g" "g \<le> f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
975 |
with assms show "integral\<^isup>S M g \<le> integral\<^isup>S M f" |
38656 | 976 |
by (auto intro!: simple_integral_mono simp: le_fun_def) |
977 |
next |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
978 |
fix y assume "\<forall>x. x\<in>{g. simple_function M g \<and> g \<le> f} \<longrightarrow> integral\<^isup>S M x \<le> y" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
979 |
with assms show "integral\<^isup>S M f \<le> y" by auto |
38656 | 980 |
qed |
35582 | 981 |
|
40859 | 982 |
lemma (in measure_space) positive_integral_mono_AE: |
983 |
assumes ae: "AE x. u x \<le> v x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
984 |
shows "integral\<^isup>P M u \<le> integral\<^isup>P M v" |
38656 | 985 |
unfolding positive_integral_alt1 |
986 |
proof (safe intro!: SUPR_mono) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
987 |
fix a assume a: "simple_function M a" and mono: "\<forall>x\<in>space M. a x \<le> u x \<and> a x \<noteq> \<omega>" |
40859 | 988 |
from ae obtain N where N: "{x\<in>space M. \<not> u x \<le> v x} \<subseteq> N" "N \<in> sets M" "\<mu> N = 0" |
989 |
by (auto elim!: AE_E) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
990 |
have "simple_function M (\<lambda>x. a x * indicator (space M - N) x)" |
40859 | 991 |
using `N \<in> sets M` a by auto |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
992 |
with a show "\<exists>b\<in>{g. simple_function M g \<and> (\<forall>x\<in>space M. g x \<le> v x \<and> g x \<noteq> \<omega>)}. |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
993 |
integral\<^isup>S M a \<le> integral\<^isup>S M b" |
40859 | 994 |
proof (safe intro!: bexI[of _ "\<lambda>x. a x * indicator (space M - N) x"] |
995 |
simple_integral_mono_AE) |
|
996 |
show "AE x. a x \<le> a x * indicator (space M - N) x" |
|
997 |
proof (rule AE_I, rule subset_refl) |
|
998 |
have *: "{x \<in> space M. \<not> a x \<le> a x * indicator (space M - N) x} = |
|
999 |
N \<inter> {x \<in> space M. a x \<noteq> 0}" (is "?N = _") |
|
1000 |
using `N \<in> sets M`[THEN sets_into_space] by (auto simp: indicator_def) |
|
41705 | 1001 |
then show "?N \<in> 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:
41661
diff
changeset
|
1002 |
using `N \<in> sets M` `simple_function M a`[THEN borel_measurable_simple_function] |
40859 | 1003 |
by (auto intro!: measure_mono Int) |
1004 |
then have "\<mu> ?N \<le> \<mu> N" |
|
1005 |
unfolding * using `N \<in> sets M` by (auto intro!: measure_mono) |
|
1006 |
then show "\<mu> ?N = 0" using `\<mu> N = 0` by auto |
|
1007 |
qed |
|
1008 |
next |
|
1009 |
fix x assume "x \<in> space M" |
|
1010 |
show "a x * indicator (space M - N) x \<le> v x" |
|
1011 |
proof (cases "x \<in> N") |
|
1012 |
case True then show ?thesis by simp |
|
1013 |
next |
|
1014 |
case False |
|
1015 |
with N mono have "a x \<le> u x" "u x \<le> v x" using `x \<in> space M` by auto |
|
1016 |
with False `x \<in> space M` show "a x * indicator (space M - N) x \<le> v x" by auto |
|
1017 |
qed |
|
1018 |
assume "a x * indicator (space M - N) x = \<omega>" |
|
1019 |
with mono `x \<in> space M` show False |
|
1020 |
by (simp split: split_if_asm add: indicator_def) |
|
1021 |
qed |
|
1022 |
qed |
|
1023 |
||
1024 |
lemma (in measure_space) positive_integral_cong_AE: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1025 |
"AE x. u x = v x \<Longrightarrow> integral\<^isup>P M u = integral\<^isup>P M v" |
40859 | 1026 |
by (auto simp: eq_iff intro!: positive_integral_mono_AE) |
1027 |
||
1028 |
lemma (in measure_space) positive_integral_mono: |
|
41705 | 1029 |
"(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^isup>P M u \<le> integral\<^isup>P M v" |
1030 |
by (auto intro: positive_integral_mono_AE) |
|
40859 | 1031 |
|
40873 | 1032 |
lemma image_set_cong: |
1033 |
assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y" |
|
1034 |
assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. g y = f x" |
|
1035 |
shows "f ` A = g ` B" |
|
1036 |
using assms by blast |
|
1037 |
||
38656 | 1038 |
lemma (in measure_space) positive_integral_SUP_approx: |
1039 |
assumes "f \<up> s" |
|
1040 |
and f: "\<And>i. f i \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1041 |
and "simple_function M u" |
38656 | 1042 |
and le: "u \<le> s" and real: "\<omega> \<notin> u`space M" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1043 |
shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S") |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1044 |
proof (rule pextreal_le_mult_one_interval) |
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1045 |
fix a :: pextreal assume "0 < a" "a < 1" |
38656 | 1046 |
hence "a \<noteq> 0" by auto |
1047 |
let "?B i" = "{x \<in> space M. a * u x \<le> f i x}" |
|
1048 |
have B: "\<And>i. ?B i \<in> 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:
41661
diff
changeset
|
1049 |
using f `simple_function M u` by (auto simp: borel_measurable_simple_function) |
38656 | 1050 |
|
1051 |
let "?uB i x" = "u x * indicator (?B i) x" |
|
1052 |
||
1053 |
{ fix i have "?B i \<subseteq> ?B (Suc i)" |
|
1054 |
proof safe |
|
1055 |
fix i x assume "a * u x \<le> f i x" |
|
1056 |
also have "\<dots> \<le> f (Suc i) x" |
|
1057 |
using `f \<up> s` unfolding isoton_def le_fun_def by auto |
|
1058 |
finally show "a * u x \<le> f (Suc i) x" . |
|
1059 |
qed } |
|
1060 |
note B_mono = this |
|
35582 | 1061 |
|
38656 | 1062 |
have u: "\<And>x. x \<in> space M \<Longrightarrow> u -` {u x} \<inter> space M \<in> 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:
41661
diff
changeset
|
1063 |
using `simple_function M u` by (auto simp add: simple_function_def) |
38656 | 1064 |
|
40859 | 1065 |
have "\<And>i. (\<lambda>n. (u -` {i} \<inter> space M) \<inter> ?B n) \<up> (u -` {i} \<inter> space M)" using B_mono unfolding isoton_def |
1066 |
proof safe |
|
1067 |
fix x i assume "x \<in> space M" |
|
1068 |
show "x \<in> (\<Union>i. (u -` {u x} \<inter> space M) \<inter> ?B i)" |
|
1069 |
proof cases |
|
1070 |
assume "u x = 0" thus ?thesis using `x \<in> space M` by simp |
|
1071 |
next |
|
1072 |
assume "u x \<noteq> 0" |
|
1073 |
with `a < 1` real `x \<in> space M` |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1074 |
have "a * u x < 1 * u x" by (rule_tac pextreal_mult_strict_right_mono) (auto simp: image_iff) |
40859 | 1075 |
also have "\<dots> \<le> (SUP i. f i x)" using le `f \<up> s` |
1076 |
unfolding isoton_fun_expand by (auto simp: isoton_def le_fun_def) |
|
1077 |
finally obtain i where "a * u x < f i x" unfolding SUPR_def |
|
1078 |
by (auto simp add: less_Sup_iff) |
|
1079 |
hence "a * u x \<le> f i x" by auto |
|
1080 |
thus ?thesis using `x \<in> space M` by auto |
|
1081 |
qed |
|
1082 |
qed auto |
|
1083 |
note measure_conv = measure_up[OF Int[OF u B] this] |
|
38656 | 1084 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1085 |
have "integral\<^isup>S M u = (SUP i. integral\<^isup>S M (?uB i))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1086 |
unfolding simple_integral_indicator[OF B `simple_function M u`] |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1087 |
proof (subst SUPR_pextreal_setsum, safe) |
38656 | 1088 |
fix x n assume "x \<in> space M" |
1089 |
have "\<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f n x}) |
|
1090 |
\<le> \<mu> (u -` {u x} \<inter> space M \<inter> {x \<in> space M. a * u x \<le> f (Suc n) x})" |
|
1091 |
using B_mono Int[OF u[OF `x \<in> space M`] B] by (auto intro!: measure_mono) |
|
1092 |
thus "u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B n) |
|
1093 |
\<le> u x * \<mu> (u -` {u x} \<inter> space M \<inter> ?B (Suc n))" |
|
1094 |
by (auto intro: mult_left_mono) |
|
1095 |
next |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1096 |
show "integral\<^isup>S M u = |
38656 | 1097 |
(\<Sum>i\<in>u ` space M. SUP n. i * \<mu> (u -` {i} \<inter> space M \<inter> ?B n))" |
1098 |
using measure_conv unfolding simple_integral_def isoton_def |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1099 |
by (auto intro!: setsum_cong simp: pextreal_SUP_cmult) |
38656 | 1100 |
qed |
1101 |
moreover |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1102 |
have "a * (SUP i. integral\<^isup>S M (?uB i)) \<le> ?S" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1103 |
unfolding pextreal_SUP_cmult[symmetric] |
38705 | 1104 |
proof (safe intro!: SUP_mono bexI) |
38656 | 1105 |
fix i |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1106 |
have "a * integral\<^isup>S M (?uB i) = (\<integral>\<^isup>Sx. a * ?uB i x \<partial>M)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1107 |
using B `simple_function M u` |
38656 | 1108 |
by (subst simple_integral_mult[symmetric]) (auto simp: field_simps) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1109 |
also have "\<dots> \<le> integral\<^isup>P M (f i)" |
38656 | 1110 |
proof - |
1111 |
have "\<And>x. a * ?uB i x \<le> f i x" unfolding indicator_def by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1112 |
hence *: "simple_function M (\<lambda>x. a * ?uB i x)" using B assms(3) |
38656 | 1113 |
by (auto intro!: simple_integral_mono) |
1114 |
show ?thesis unfolding positive_integral_eq_simple_integral[OF *, symmetric] |
|
1115 |
by (auto intro!: positive_integral_mono simp: indicator_def) |
|
1116 |
qed |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1117 |
finally show "a * integral\<^isup>S M (?uB i) \<le> integral\<^isup>P M (f i)" |
38656 | 1118 |
by auto |
38705 | 1119 |
qed simp |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1120 |
ultimately show "a * integral\<^isup>S M u \<le> ?S" by simp |
35582 | 1121 |
qed |
1122 |
||
1123 |
text {* Beppo-Levi monotone convergence theorem *} |
|
38656 | 1124 |
lemma (in measure_space) positive_integral_isoton: |
1125 |
assumes "f \<up> u" "\<And>i. f i \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1126 |
shows "(\<lambda>i. integral\<^isup>P M (f i)) \<up> integral\<^isup>P M u" |
38656 | 1127 |
unfolding isoton_def |
1128 |
proof safe |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1129 |
fix i show "integral\<^isup>P M (f i) \<le> integral\<^isup>P M (f (Suc i))" |
38656 | 1130 |
apply (rule positive_integral_mono) |
1131 |
using `f \<up> u` unfolding isoton_def le_fun_def by auto |
|
1132 |
next |
|
1133 |
have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1134 |
show "(SUP i. integral\<^isup>P M (f i)) = integral\<^isup>P M u" |
38656 | 1135 |
proof (rule antisym) |
1136 |
from `f \<up> u`[THEN isoton_Sup, unfolded le_fun_def] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1137 |
show "(SUP j. integral\<^isup>P M (f j)) \<le> integral\<^isup>P M u" |
38656 | 1138 |
by (auto intro!: SUP_leI positive_integral_mono) |
1139 |
next |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1140 |
show "integral\<^isup>P M u \<le> (SUP i. integral\<^isup>P M (f i))" |
40873 | 1141 |
unfolding positive_integral_alt[of u] |
38656 | 1142 |
by (auto intro!: SUP_leI positive_integral_SUP_approx[OF assms]) |
35582 | 1143 |
qed |
1144 |
qed |
|
1145 |
||
40859 | 1146 |
lemma (in measure_space) positive_integral_monotone_convergence_SUP: |
1147 |
assumes "\<And>i x. x \<in> space M \<Longrightarrow> f i x \<le> f (Suc i) x" |
|
1148 |
assumes "\<And>i. f i \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1149 |
shows "(SUP i. integral\<^isup>P M (f i)) = (\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1150 |
(is "_ = integral\<^isup>P M ?u") |
40859 | 1151 |
proof - |
1152 |
show ?thesis |
|
1153 |
proof (rule antisym) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1154 |
show "(SUP j. integral\<^isup>P M (f j)) \<le> integral\<^isup>P M ?u" |
40859 | 1155 |
by (auto intro!: SUP_leI positive_integral_mono le_SUPI) |
1156 |
next |
|
1157 |
def rf \<equiv> "\<lambda>i. \<lambda>x\<in>space M. f i x" and ru \<equiv> "\<lambda>x\<in>space M. ?u x" |
|
1158 |
have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def |
|
1159 |
using assms by (simp cong: measurable_cong) |
|
1160 |
moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def |
|
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1161 |
unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply |
40872 | 1162 |
using SUP_const[OF UNIV_not_empty] |
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1163 |
by (auto simp: restrict_def le_fun_def fun_eq_iff) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1164 |
ultimately have "integral\<^isup>P M ru \<le> (SUP i. integral\<^isup>P M (rf i))" |
40873 | 1165 |
unfolding positive_integral_alt[of ru] |
40859 | 1166 |
by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1167 |
then show "integral\<^isup>P M ?u \<le> (SUP i. integral\<^isup>P M (f i))" |
40859 | 1168 |
unfolding ru_def rf_def by (simp cong: positive_integral_cong) |
1169 |
qed |
|
1170 |
qed |
|
1171 |
||
38656 | 1172 |
lemma (in measure_space) SUP_simple_integral_sequences: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1173 |
assumes f: "f \<up> u" "\<And>i. simple_function M (f i)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1174 |
and g: "g \<up> u" "\<And>i. simple_function M (g i)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1175 |
shows "(SUP i. integral\<^isup>S M (f i)) = (SUP i. integral\<^isup>S M (g i))" |
38656 | 1176 |
(is "SUPR _ ?F = SUPR _ ?G") |
1177 |
proof - |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1178 |
have "(SUP i. ?F i) = (SUP i. integral\<^isup>P M (f i))" |
38656 | 1179 |
using assms by (simp add: positive_integral_eq_simple_integral) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1180 |
also have "\<dots> = integral\<^isup>P M u" |
38656 | 1181 |
using positive_integral_isoton[OF f(1) borel_measurable_simple_function[OF f(2)]] |
1182 |
unfolding isoton_def by simp |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1183 |
also have "\<dots> = (SUP i. integral\<^isup>P M (g i))" |
38656 | 1184 |
using positive_integral_isoton[OF g(1) borel_measurable_simple_function[OF g(2)]] |
1185 |
unfolding isoton_def by simp |
|
1186 |
also have "\<dots> = (SUP i. ?G i)" |
|
1187 |
using assms by (simp add: positive_integral_eq_simple_integral) |
|
1188 |
finally show ?thesis . |
|
1189 |
qed |
|
1190 |
||
1191 |
lemma (in measure_space) positive_integral_const[simp]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1192 |
"(\<integral>\<^isup>+ x. c \<partial>M) = c * \<mu> (space M)" |
38656 | 1193 |
by (subst positive_integral_eq_simple_integral) auto |
1194 |
||
1195 |
lemma (in measure_space) positive_integral_isoton_simple: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1196 |
assumes "f \<up> u" and e: "\<And>i. simple_function M (f i)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1197 |
shows "(\<lambda>i. integral\<^isup>S M (f i)) \<up> integral\<^isup>P M u" |
38656 | 1198 |
using positive_integral_isoton[OF `f \<up> u` e(1)[THEN borel_measurable_simple_function]] |
1199 |
unfolding positive_integral_eq_simple_integral[OF e] . |
|
1200 |
||
41831 | 1201 |
lemma measure_preservingD2: |
1202 |
"f \<in> measure_preserving A B \<Longrightarrow> f \<in> measurable A B" |
|
1203 |
unfolding measure_preserving_def by auto |
|
1204 |
||
41661 | 1205 |
lemma (in measure_space) positive_integral_vimage: |
41831 | 1206 |
assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'" and f: "f \<in> borel_measurable M'" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1207 |
shows "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)" |
41661 | 1208 |
proof - |
41831 | 1209 |
interpret T: measure_space M' by (rule measure_space_vimage[OF T]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1210 |
obtain f' where f': "f' \<up> f" "\<And>i. simple_function M' (f' i)" |
41661 | 1211 |
using T.borel_measurable_implies_simple_function_sequence[OF f] by blast |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1212 |
then have f: "(\<lambda>i x. f' i (T x)) \<up> (\<lambda>x. f (T x))" "\<And>i. simple_function M (\<lambda>x. f' i (T x))" |
41831 | 1213 |
using simple_function_vimage[OF T(1) measure_preservingD2[OF T(2)]] unfolding isoton_fun_expand by auto |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1214 |
show "integral\<^isup>P M' f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)" |
41661 | 1215 |
using positive_integral_isoton_simple[OF f] |
1216 |
using T.positive_integral_isoton_simple[OF f'] |
|
41831 | 1217 |
by (simp add: simple_integral_vimage[OF T f'(2)] isoton_def) |
41661 | 1218 |
qed |
1219 |
||
38656 | 1220 |
lemma (in measure_space) positive_integral_linear: |
1221 |
assumes f: "f \<in> borel_measurable M" |
|
1222 |
and g: "g \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1223 |
shows "(\<integral>\<^isup>+ x. a * f x + g x \<partial>M) = a * integral\<^isup>P M f + integral\<^isup>P M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1224 |
(is "integral\<^isup>P M ?L = _") |
35582 | 1225 |
proof - |
38656 | 1226 |
from borel_measurable_implies_simple_function_sequence'[OF f] guess u . |
1227 |
note u = this positive_integral_isoton_simple[OF this(1-2)] |
|
1228 |
from borel_measurable_implies_simple_function_sequence'[OF g] guess v . |
|
1229 |
note v = this positive_integral_isoton_simple[OF this(1-2)] |
|
1230 |
let "?L' i x" = "a * u i x + v i x" |
|
1231 |
||
1232 |
have "?L \<in> borel_measurable M" |
|
1233 |
using assms by simp |
|
1234 |
from borel_measurable_implies_simple_function_sequence'[OF this] guess l . |
|
1235 |
note positive_integral_isoton_simple[OF this(1-2)] and l = this |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1236 |
moreover have "(SUP i. integral\<^isup>S M (l i)) = (SUP i. integral\<^isup>S M (?L' i))" |
38656 | 1237 |
proof (rule SUP_simple_integral_sequences[OF l(1-2)]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1238 |
show "?L' \<up> ?L" "\<And>i. simple_function M (?L' i)" |
38656 | 1239 |
using u v by (auto simp: isoton_fun_expand isoton_add isoton_cmult_right) |
1240 |
qed |
|
1241 |
moreover from u v have L'_isoton: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1242 |
"(\<lambda>i. integral\<^isup>S M (?L' i)) \<up> a * integral\<^isup>P M f + integral\<^isup>P M g" |
38656 | 1243 |
by (simp add: isoton_add isoton_cmult_right) |
1244 |
ultimately show ?thesis by (simp add: isoton_def) |
|
1245 |
qed |
|
1246 |
||
1247 |
lemma (in measure_space) positive_integral_cmult: |
|
1248 |
assumes "f \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1249 |
shows "(\<integral>\<^isup>+ x. c * f x \<partial>M) = c * integral\<^isup>P M f" |
38656 | 1250 |
using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto |
1251 |
||
41096 | 1252 |
lemma (in measure_space) positive_integral_multc: |
1253 |
assumes "f \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1254 |
shows "(\<integral>\<^isup>+ x. f x * c \<partial>M) = integral\<^isup>P M f * c" |
41096 | 1255 |
unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp |
1256 |
||
38656 | 1257 |
lemma (in measure_space) positive_integral_indicator[simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1258 |
"A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x\<partial>M) = \<mu> A" |
41544 | 1259 |
by (subst positive_integral_eq_simple_integral) |
1260 |
(auto simp: simple_function_indicator simple_integral_indicator) |
|
38656 | 1261 |
|
1262 |
lemma (in measure_space) positive_integral_cmult_indicator: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1263 |
"A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x \<partial>M) = c * \<mu> A" |
41544 | 1264 |
by (subst positive_integral_eq_simple_integral) |
1265 |
(auto simp: simple_function_indicator simple_integral_indicator) |
|
38656 | 1266 |
|
1267 |
lemma (in measure_space) positive_integral_add: |
|
1268 |
assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1269 |
shows "(\<integral>\<^isup>+ x. f x + g x \<partial>M) = integral\<^isup>P M f + integral\<^isup>P M g" |
38656 | 1270 |
using positive_integral_linear[OF assms, of 1] by simp |
1271 |
||
1272 |
lemma (in measure_space) positive_integral_setsum: |
|
1273 |
assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1274 |
shows "(\<integral>\<^isup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>P M (f i))" |
38656 | 1275 |
proof cases |
1276 |
assume "finite P" |
|
1277 |
from this assms show ?thesis |
|
1278 |
proof induct |
|
1279 |
case (insert i P) |
|
1280 |
have "f i \<in> borel_measurable M" |
|
1281 |
"(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1282 |
using insert by (auto intro!: borel_measurable_pextreal_setsum) |
38656 | 1283 |
from positive_integral_add[OF this] |
1284 |
show ?case using insert by auto |
|
1285 |
qed simp |
|
1286 |
qed simp |
|
1287 |
||
1288 |
lemma (in measure_space) positive_integral_diff: |
|
1289 |
assumes f: "f \<in> borel_measurable M" and g: "g \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1290 |
and fin: "integral\<^isup>P M g \<noteq> \<omega>" |
38656 | 1291 |
and mono: "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1292 |
shows "(\<integral>\<^isup>+ x. f x - g x \<partial>M) = integral\<^isup>P M f - integral\<^isup>P M g" |
38656 | 1293 |
proof - |
1294 |
have borel: "(\<lambda>x. f x - g x) \<in> borel_measurable M" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1295 |
using f g by (rule borel_measurable_pextreal_diff) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1296 |
have "(\<integral>\<^isup>+x. f x - g x \<partial>M) + integral\<^isup>P M g = integral\<^isup>P M f" |
38656 | 1297 |
unfolding positive_integral_add[OF borel g, symmetric] |
1298 |
proof (rule positive_integral_cong) |
|
1299 |
fix x assume "x \<in> space M" |
|
1300 |
from mono[OF this] show "f x - g x + g x = f x" |
|
1301 |
by (cases "f x", cases "g x", simp, simp, cases "g x", auto) |
|
1302 |
qed |
|
1303 |
with mono show ?thesis |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1304 |
by (subst minus_pextreal_eq2[OF _ fin]) (auto intro!: positive_integral_mono) |
38656 | 1305 |
qed |
1306 |
||
1307 |
lemma (in measure_space) positive_integral_psuminf: |
|
1308 |
assumes "\<And>i. f i \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1309 |
shows "(\<integral>\<^isup>+ x. (\<Sum>\<^isub>\<infinity> i. f i x) \<partial>M) = (\<Sum>\<^isub>\<infinity> i. integral\<^isup>P M (f i))" |
38656 | 1310 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1311 |
have "(\<lambda>i. (\<integral>\<^isup>+x. (\<Sum>i<i. f i x) \<partial>M)) \<up> (\<integral>\<^isup>+x. (\<Sum>\<^isub>\<infinity>i. f i x) \<partial>M)" |
38656 | 1312 |
by (rule positive_integral_isoton) |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1313 |
(auto intro!: borel_measurable_pextreal_setsum assms positive_integral_mono |
38656 | 1314 |
arg_cong[where f=Sup] |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
1315 |
simp: isoton_def le_fun_def psuminf_def fun_eq_iff SUPR_def Sup_fun_def) |
38656 | 1316 |
thus ?thesis |
1317 |
by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms]) |
|
1318 |
qed |
|
1319 |
||
1320 |
text {* Fatou's lemma: convergence theorem on limes inferior *} |
|
1321 |
lemma (in measure_space) positive_integral_lim_INF: |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1322 |
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal" |
38656 | 1323 |
assumes "\<And>i. u i \<in> borel_measurable M" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1324 |
shows "(\<integral>\<^isup>+ x. (SUP n. INF m. u (m + n) x) \<partial>M) \<le> |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1325 |
(SUP n. INF m. integral\<^isup>P M (u (m + n)))" |
38656 | 1326 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1327 |
have "(\<integral>\<^isup>+x. (SUP n. INF m. u (m + n) x) \<partial>M) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1328 |
= (SUP n. (\<integral>\<^isup>+x. (INF m. u (m + n) x) \<partial>M))" |
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1329 |
using assms |
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1330 |
by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono) |
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1331 |
(auto simp del: add_Suc simp add: add_Suc[symmetric]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1332 |
also have "\<dots> \<le> (SUP n. INF m. integral\<^isup>P M (u (m + n)))" |
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1333 |
by (auto intro!: SUP_mono bexI le_INFI positive_integral_mono INF_leI) |
38656 | 1334 |
finally show ?thesis . |
35582 | 1335 |
qed |
1336 |
||
38656 | 1337 |
lemma (in measure_space) measure_space_density: |
1338 |
assumes borel: "u \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1339 |
and M'[simp]: "M' = (M\<lparr>measure := \<lambda>A. (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)\<rparr>)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1340 |
shows "measure_space M'" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1341 |
proof - |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1342 |
interpret M': sigma_algebra M' by (intro sigma_algebra_cong) auto |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1343 |
show ?thesis |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1344 |
proof |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1345 |
show "measure M' {} = 0" unfolding M' by simp |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1346 |
show "countably_additive M' (measure M')" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1347 |
proof (intro countably_additiveI) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1348 |
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M'" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1349 |
then have "\<And>i. (\<lambda>x. u x * indicator (A i) x) \<in> borel_measurable M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1350 |
using borel by (auto intro: borel_measurable_indicator) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1351 |
moreover assume "disjoint_family A" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1352 |
note psuminf_indicator[OF this] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1353 |
ultimately show "(\<Sum>\<^isub>\<infinity>n. measure M' (A n)) = measure M' (\<Union>x. A x)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1354 |
by (simp add: positive_integral_psuminf[symmetric]) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1355 |
qed |
38656 | 1356 |
qed |
1357 |
qed |
|
35582 | 1358 |
|
39092 | 1359 |
lemma (in measure_space) positive_integral_translated_density: |
1360 |
assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1361 |
and M': "M' = (M\<lparr> measure := \<lambda>A. (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)\<rparr>)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1362 |
shows "integral\<^isup>P M' g = (\<integral>\<^isup>+ x. f x * g x \<partial>M)" |
39092 | 1363 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1364 |
from measure_space_density[OF assms(1) M'] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1365 |
interpret T: measure_space M' . |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1366 |
have borel[simp]: |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1367 |
"borel_measurable M' = borel_measurable M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1368 |
"simple_function M' = simple_function M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1369 |
unfolding measurable_def simple_function_def_raw by (auto simp: M') |
39092 | 1370 |
from borel_measurable_implies_simple_function_sequence[OF assms(2)] |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1371 |
obtain G where G: "\<And>i. simple_function M (G i)" "G \<up> g" by blast |
39092 | 1372 |
note G_borel = borel_measurable_simple_function[OF this(1)] |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1373 |
from T.positive_integral_isoton[unfolded borel, OF `G \<up> g` G_borel] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1374 |
have *: "(\<lambda>i. integral\<^isup>P M' (G i)) \<up> integral\<^isup>P M' g" . |
39092 | 1375 |
{ fix i |
1376 |
have [simp]: "finite (G i ` space M)" |
|
1377 |
using G(1) unfolding simple_function_def by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1378 |
have "integral\<^isup>P M' (G i) = integral\<^isup>S M' (G i)" |
39092 | 1379 |
using G T.positive_integral_eq_simple_integral by simp |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1380 |
also have "\<dots> = (\<integral>\<^isup>+x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x) \<partial>M)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1381 |
apply (simp add: simple_integral_def M') |
39092 | 1382 |
apply (subst positive_integral_cmult[symmetric]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1383 |
using G_borel assms(1) apply (fastsimp intro: borel_measurable_vimage) |
39092 | 1384 |
apply (subst positive_integral_setsum[symmetric]) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1385 |
using G_borel assms(1) apply (fastsimp intro: borel_measurable_vimage) |
39092 | 1386 |
by (simp add: setsum_right_distrib field_simps) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1387 |
also have "\<dots> = (\<integral>\<^isup>+x. f x * G i x \<partial>M)" |
39092 | 1388 |
by (auto intro!: positive_integral_cong |
1389 |
simp: indicator_def if_distrib setsum_cases) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1390 |
finally have "integral\<^isup>P M' (G i) = (\<integral>\<^isup>+x. f x * G i x \<partial>M)" . } |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1391 |
with * have eq_Tg: "(\<lambda>i. (\<integral>\<^isup>+x. f x * G i x \<partial>M)) \<up> integral\<^isup>P M' g" by simp |
39092 | 1392 |
from G(2) have "(\<lambda>i x. f x * G i x) \<up> (\<lambda>x. f x * g x)" |
1393 |
unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1394 |
then have "(\<lambda>i. (\<integral>\<^isup>+x. f x * G i x \<partial>M)) \<up> (\<integral>\<^isup>+x. f x * g x \<partial>M)" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1395 |
using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pextreal_times) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1396 |
with eq_Tg show "integral\<^isup>P M' g = (\<integral>\<^isup>+x. f x * g x \<partial>M)" |
39092 | 1397 |
unfolding isoton_def by simp |
1398 |
qed |
|
1399 |
||
38656 | 1400 |
lemma (in measure_space) positive_integral_null_set: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1401 |
assumes "N \<in> null_sets" shows "(\<integral>\<^isup>+ x. u x * indicator N x \<partial>M) = 0" |
38656 | 1402 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1403 |
have "(\<integral>\<^isup>+ x. u x * indicator N x \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)" |
40859 | 1404 |
proof (intro positive_integral_cong_AE AE_I) |
1405 |
show "{x \<in> space M. u x * indicator N x \<noteq> 0} \<subseteq> N" |
|
1406 |
by (auto simp: indicator_def) |
|
1407 |
show "\<mu> N = 0" "N \<in> sets M" |
|
1408 |
using assms by auto |
|
35582 | 1409 |
qed |
40859 | 1410 |
then show ?thesis by simp |
38656 | 1411 |
qed |
35582 | 1412 |
|
38656 | 1413 |
lemma (in measure_space) positive_integral_Markov_inequality: |
1414 |
assumes borel: "u \<in> borel_measurable M" and "A \<in> sets M" and c: "c \<noteq> \<omega>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1415 |
shows "\<mu> ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)" |
38656 | 1416 |
(is "\<mu> ?A \<le> _ * ?PI") |
1417 |
proof - |
|
1418 |
have "?A \<in> sets M" |
|
1419 |
using `A \<in> sets M` borel by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1420 |
hence "\<mu> ?A = (\<integral>\<^isup>+ x. indicator ?A x \<partial>M)" |
38656 | 1421 |
using positive_integral_indicator by simp |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1422 |
also have "\<dots> \<le> (\<integral>\<^isup>+ x. c * (u x * indicator A x) \<partial>M)" |
38656 | 1423 |
proof (rule positive_integral_mono) |
1424 |
fix x assume "x \<in> space M" |
|
1425 |
show "indicator ?A x \<le> c * (u x * indicator A x)" |
|
1426 |
by (cases "x \<in> ?A") auto |
|
1427 |
qed |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1428 |
also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)" |
38656 | 1429 |
using assms |
1430 |
by (auto intro!: positive_integral_cmult borel_measurable_indicator) |
|
1431 |
finally show ?thesis . |
|
35582 | 1432 |
qed |
1433 |
||
38656 | 1434 |
lemma (in measure_space) positive_integral_0_iff: |
1435 |
assumes borel: "u \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1436 |
shows "integral\<^isup>P M u = 0 \<longleftrightarrow> \<mu> {x\<in>space M. u x \<noteq> 0} = 0" |
38656 | 1437 |
(is "_ \<longleftrightarrow> \<mu> ?A = 0") |
35582 | 1438 |
proof - |
38656 | 1439 |
have A: "?A \<in> sets M" using borel by auto |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1440 |
have u: "(\<integral>\<^isup>+ x. u x * indicator ?A x \<partial>M) = integral\<^isup>P M u" |
38656 | 1441 |
by (auto intro!: positive_integral_cong simp: indicator_def) |
35582 | 1442 |
|
38656 | 1443 |
show ?thesis |
1444 |
proof |
|
1445 |
assume "\<mu> ?A = 0" |
|
1446 |
hence "?A \<in> null_sets" using `?A \<in> sets M` by auto |
|
40859 | 1447 |
from positive_integral_null_set[OF this] |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1448 |
have "0 = (\<integral>\<^isup>+ x. u x * indicator ?A x \<partial>M)" by simp |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1449 |
thus "integral\<^isup>P M u = 0" unfolding u by simp |
38656 | 1450 |
next |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1451 |
assume *: "integral\<^isup>P M u = 0" |
38656 | 1452 |
let "?M n" = "{x \<in> space M. 1 \<le> of_nat n * u x}" |
1453 |
have "0 = (SUP n. \<mu> (?M n \<inter> ?A))" |
|
1454 |
proof - |
|
1455 |
{ fix n |
|
1456 |
from positive_integral_Markov_inequality[OF borel `?A \<in> sets M`, of "of_nat n"] |
|
1457 |
have "\<mu> (?M n \<inter> ?A) = 0" unfolding * u by simp } |
|
1458 |
thus ?thesis by simp |
|
35582 | 1459 |
qed |
38656 | 1460 |
also have "\<dots> = \<mu> (\<Union>n. ?M n \<inter> ?A)" |
1461 |
proof (safe intro!: continuity_from_below) |
|
1462 |
fix n show "?M n \<inter> ?A \<in> sets M" |
|
1463 |
using borel by (auto intro!: Int) |
|
1464 |
next |
|
1465 |
fix n x assume "1 \<le> of_nat n * u x" |
|
1466 |
also have "\<dots> \<le> of_nat (Suc n) * u x" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1467 |
by (subst (1 2) mult_commute) (auto intro!: pextreal_mult_cancel) |
38656 | 1468 |
finally show "1 \<le> of_nat (Suc n) * u x" . |
1469 |
qed |
|
1470 |
also have "\<dots> = \<mu> ?A" |
|
1471 |
proof (safe intro!: arg_cong[where f="\<mu>"]) |
|
1472 |
fix x assume "u x \<noteq> 0" and [simp, intro]: "x \<in> space M" |
|
1473 |
show "x \<in> (\<Union>n. ?M n \<inter> ?A)" |
|
1474 |
proof (cases "u x") |
|
1475 |
case (preal r) |
|
1476 |
obtain j where "1 / r \<le> of_nat j" using ex_le_of_nat .. |
|
1477 |
hence "1 / r * r \<le> of_nat j * r" using preal unfolding mult_le_cancel_right by auto |
|
1478 |
hence "1 \<le> of_nat j * r" using preal `u x \<noteq> 0` by auto |
|
1479 |
thus ?thesis using `u x \<noteq> 0` preal by (auto simp: real_of_nat_def[symmetric]) |
|
1480 |
qed auto |
|
1481 |
qed |
|
1482 |
finally show "\<mu> ?A = 0" by simp |
|
35582 | 1483 |
qed |
1484 |
qed |
|
1485 |
||
41705 | 1486 |
lemma (in measure_space) positive_integral_0_iff_AE: |
1487 |
assumes u: "u \<in> borel_measurable M" |
|
1488 |
shows "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. u x = 0)" |
|
1489 |
proof - |
|
1490 |
have sets: "{x\<in>space M. u x \<noteq> 0} \<in> sets M" |
|
1491 |
using u by auto |
|
1492 |
then show ?thesis |
|
1493 |
using positive_integral_0_iff[OF u] AE_iff_null_set[OF sets] by auto |
|
1494 |
qed |
|
1495 |
||
39092 | 1496 |
lemma (in measure_space) positive_integral_restricted: |
1497 |
assumes "A \<in> 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:
41661
diff
changeset
|
1498 |
shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1499 |
(is "integral\<^isup>P ?R f = integral\<^isup>P M ?f") |
39092 | 1500 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1501 |
have msR: "measure_space ?R" by (rule restricted_measure_space[OF `A \<in> sets M`]) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1502 |
then interpret R: measure_space ?R . |
39092 | 1503 |
have saR: "sigma_algebra ?R" by fact |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1504 |
have *: "integral\<^isup>P ?R f = integral\<^isup>P ?R ?f" |
40859 | 1505 |
by (intro R.positive_integral_cong) auto |
39092 | 1506 |
show ?thesis |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1507 |
unfolding * positive_integral_def |
39092 | 1508 |
unfolding simple_function_restricted[OF `A \<in> sets M`] |
1509 |
apply (simp add: SUPR_def) |
|
1510 |
apply (rule arg_cong[where f=Sup]) |
|
40859 | 1511 |
proof (auto simp add: image_iff simple_integral_restricted[OF `A \<in> 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:
41661
diff
changeset
|
1512 |
fix g assume "simple_function M (\<lambda>x. g x * indicator A x)" |
40873 | 1513 |
"g \<le> f" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1514 |
then show "\<exists>x. simple_function M x \<and> x \<le> (\<lambda>x. f x * indicator A x) \<and> |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1515 |
(\<integral>\<^isup>Sx. g x * indicator A x \<partial>M) = integral\<^isup>S M x" |
39092 | 1516 |
apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"]) |
1517 |
by (auto simp: indicator_def le_fun_def) |
|
1518 |
next |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1519 |
fix g assume g: "simple_function M g" "g \<le> (\<lambda>x. f x * indicator A x)" |
39092 | 1520 |
then have *: "(\<lambda>x. g x * indicator A x) = g" |
1521 |
"\<And>x. g x * indicator A x = g x" |
|
1522 |
"\<And>x. g x \<le> f x" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
1523 |
by (auto simp: le_fun_def fun_eq_iff indicator_def split: split_if_asm) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1524 |
from g show "\<exists>x. simple_function M (\<lambda>xa. x xa * indicator A xa) \<and> x \<le> f \<and> |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1525 |
integral\<^isup>S M g = integral\<^isup>S M (\<lambda>xa. x xa * indicator A xa)" |
39092 | 1526 |
using `A \<in> sets M`[THEN sets_into_space] |
1527 |
apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"]) |
|
1528 |
by (fastsimp simp: le_fun_def *) |
|
1529 |
qed |
|
1530 |
qed |
|
1531 |
||
41545 | 1532 |
lemma (in measure_space) positive_integral_subalgebra: |
1533 |
assumes borel: "f \<in> borel_measurable N" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1534 |
and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1535 |
and sa: "sigma_algebra N" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1536 |
shows "integral\<^isup>P N f = integral\<^isup>P M f" |
39092 | 1537 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1538 |
interpret N: measure_space N using measure_space_subalgebra[OF sa N] . |
39092 | 1539 |
from N.borel_measurable_implies_simple_function_sequence[OF borel] |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1540 |
obtain fs where Nsf: "\<And>i. simple_function N (fs i)" and "fs \<up> f" by blast |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1541 |
then have sf: "\<And>i. simple_function M (fs i)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1542 |
using simple_function_subalgebra[OF _ N(1,2)] by blast |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1543 |
from N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1544 |
have "integral\<^isup>P N f = (SUP i. \<Sum>x\<in>fs i ` space M. x * N.\<mu> (fs i -` {x} \<inter> space M))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1545 |
unfolding isoton_def simple_integral_def `space N = space M` by simp |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1546 |
also have "\<dots> = (SUP i. \<Sum>x\<in>fs i ` space M. x * \<mu> (fs i -` {x} \<inter> space M))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1547 |
using N N.simple_functionD(2)[OF Nsf] unfolding `space N = space M` by auto |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1548 |
also have "\<dots> = integral\<^isup>P M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1549 |
using positive_integral_isoton_simple[OF `fs \<up> f` sf] |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1550 |
unfolding isoton_def simple_integral_def `space N = space M` by simp |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1551 |
finally show ?thesis . |
39092 | 1552 |
qed |
1553 |
||
35692 | 1554 |
section "Lebesgue Integral" |
1555 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1556 |
definition integrable where |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1557 |
"integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1558 |
(\<integral>\<^isup>+ x. Real (f x) \<partial>M) \<noteq> \<omega> \<and> |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1559 |
(\<integral>\<^isup>+ x. Real (- f x) \<partial>M) \<noteq> \<omega>" |
35692 | 1560 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1561 |
lemma integrableD[dest]: |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1562 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1563 |
shows "f \<in> borel_measurable M" "(\<integral>\<^isup>+ x. Real (f x) \<partial>M) \<noteq> \<omega>" "(\<integral>\<^isup>+ x. Real (- f x) \<partial>M) \<noteq> \<omega>" |
38656 | 1564 |
using assms unfolding integrable_def by auto |
35692 | 1565 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1566 |
definition lebesgue_integral_def: |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1567 |
"integral\<^isup>L M f = real ((\<integral>\<^isup>+ x. Real (f x) \<partial>M)) - real ((\<integral>\<^isup>+ x. Real (- f x) \<partial>M))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1568 |
|
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1569 |
syntax |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1570 |
"_lebesgue_integral" :: "'a \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a, 'b) measure_space_scheme \<Rightarrow> real" ("\<integral> _. _ \<partial>_" [60,61] 110) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1571 |
|
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1572 |
translations |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1573 |
"\<integral> x. f \<partial>M" == "CONST integral\<^isup>L M (%x. f)" |
38656 | 1574 |
|
1575 |
lemma (in measure_space) integral_cong: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1576 |
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x = g x" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1577 |
shows "integral\<^isup>L M f = integral\<^isup>L M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1578 |
using assms by (simp cong: positive_integral_cong add: lebesgue_integral_def) |
35582 | 1579 |
|
40859 | 1580 |
lemma (in measure_space) integral_cong_measure: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1581 |
assumes "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A" "sets N = sets M" "space N = space M" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1582 |
shows "integral\<^isup>L N f = integral\<^isup>L M f" |
40859 | 1583 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1584 |
interpret v: measure_space N |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1585 |
by (rule measure_space_cong) fact+ |
40859 | 1586 |
show ?thesis |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1587 |
by (simp add: positive_integral_cong_measure[OF assms] lebesgue_integral_def) |
40859 | 1588 |
qed |
1589 |
||
1590 |
lemma (in measure_space) integral_cong_AE: |
|
1591 |
assumes cong: "AE x. f x = g x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1592 |
shows "integral\<^isup>L M f = integral\<^isup>L M g" |
40859 | 1593 |
proof - |
41705 | 1594 |
have "AE x. Real (f x) = Real (g x)" using cong by auto |
1595 |
moreover have "AE x. Real (- f x) = Real (- g x)" using cong by auto |
|
40859 | 1596 |
ultimately show ?thesis |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1597 |
by (simp cong: positive_integral_cong_AE add: lebesgue_integral_def) |
40859 | 1598 |
qed |
1599 |
||
38656 | 1600 |
lemma (in measure_space) integrable_cong: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1601 |
"(\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable M g" |
38656 | 1602 |
by (simp cong: positive_integral_cong measurable_cong add: integrable_def) |
1603 |
||
1604 |
lemma (in measure_space) integral_eq_positive_integral: |
|
1605 |
assumes "\<And>x. 0 \<le> f x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1606 |
shows "integral\<^isup>L M f = real (\<integral>\<^isup>+ x. Real (f x) \<partial>M)" |
35582 | 1607 |
proof - |
38656 | 1608 |
have "\<And>x. Real (- f x) = 0" using assms by simp |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1609 |
thus ?thesis by (simp del: Real_eq_0 add: lebesgue_integral_def) |
35582 | 1610 |
qed |
1611 |
||
41661 | 1612 |
lemma (in measure_space) integral_vimage: |
41831 | 1613 |
assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'" |
1614 |
assumes f: "f \<in> borel_measurable M'" |
|
1615 |
shows "integral\<^isup>L M' f = (\<integral>x. f (T x) \<partial>M)" |
|
40859 | 1616 |
proof - |
41831 | 1617 |
interpret T: measure_space M' by (rule measure_space_vimage[OF T]) |
1618 |
from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel] |
|
41661 | 1619 |
have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'" |
1620 |
and "(\<lambda>x. f (T x)) \<in> borel_measurable M" |
|
41831 | 1621 |
using f by (auto simp: comp_def) |
1622 |
then show ?thesis |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1623 |
using f unfolding lebesgue_integral_def integrable_def |
41831 | 1624 |
by (auto simp: borel[THEN positive_integral_vimage[OF T]]) |
1625 |
qed |
|
1626 |
||
1627 |
lemma (in measure_space) integrable_vimage: |
|
1628 |
assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'" |
|
1629 |
assumes f: "integrable M' f" |
|
1630 |
shows "integrable M (\<lambda>x. f (T x))" |
|
1631 |
proof - |
|
1632 |
interpret T: measure_space M' by (rule measure_space_vimage[OF T]) |
|
1633 |
from measurable_comp[OF measure_preservingD2[OF T(2)], of f borel] |
|
1634 |
have borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable M'" "(\<lambda>x. Real (- f x)) \<in> borel_measurable M'" |
|
1635 |
and "(\<lambda>x. f (T x)) \<in> borel_measurable M" |
|
1636 |
using f by (auto simp: comp_def) |
|
1637 |
then show ?thesis |
|
1638 |
using f unfolding lebesgue_integral_def integrable_def |
|
1639 |
by (auto simp: borel[THEN positive_integral_vimage[OF T]]) |
|
40859 | 1640 |
qed |
1641 |
||
38656 | 1642 |
lemma (in measure_space) integral_minus[intro, simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1643 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1644 |
shows "integrable M (\<lambda>x. - f x)" "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1645 |
using assms by (auto simp: integrable_def lebesgue_integral_def) |
38656 | 1646 |
|
1647 |
lemma (in measure_space) integral_of_positive_diff: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1648 |
assumes integrable: "integrable M u" "integrable M v" |
38656 | 1649 |
and f_def: "\<And>x. f x = u x - v x" and pos: "\<And>x. 0 \<le> u x" "\<And>x. 0 \<le> v x" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1650 |
shows "integrable M f" and "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v" |
35582 | 1651 |
proof - |
38656 | 1652 |
let "?f x" = "Real (f x)" |
1653 |
let "?mf x" = "Real (- f x)" |
|
1654 |
let "?u x" = "Real (u x)" |
|
1655 |
let "?v x" = "Real (v x)" |
|
1656 |
||
1657 |
from borel_measurable_diff[of u v] integrable |
|
1658 |
have f_borel: "?f \<in> borel_measurable M" and |
|
1659 |
mf_borel: "?mf \<in> borel_measurable M" and |
|
1660 |
v_borel: "?v \<in> borel_measurable M" and |
|
1661 |
u_borel: "?u \<in> borel_measurable M" and |
|
1662 |
"f \<in> borel_measurable M" |
|
1663 |
by (auto simp: f_def[symmetric] integrable_def) |
|
35582 | 1664 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1665 |
have "(\<integral>\<^isup>+ x. Real (u x - v x) \<partial>M) \<le> integral\<^isup>P M ?u" |
38656 | 1666 |
using pos by (auto intro!: positive_integral_mono) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1667 |
moreover have "(\<integral>\<^isup>+ x. Real (v x - u x) \<partial>M) \<le> integral\<^isup>P M ?v" |
38656 | 1668 |
using pos by (auto intro!: positive_integral_mono) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1669 |
ultimately show f: "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1670 |
using `integrable M u` `integrable M v` `f \<in> borel_measurable M` |
38656 | 1671 |
by (auto simp: integrable_def f_def) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1672 |
hence mf: "integrable M (\<lambda>x. - f x)" .. |
38656 | 1673 |
|
1674 |
have *: "\<And>x. Real (- v x) = 0" "\<And>x. Real (- u x) = 0" |
|
1675 |
using pos by auto |
|
35582 | 1676 |
|
38656 | 1677 |
have "\<And>x. ?u x + ?mf x = ?v x + ?f x" |
1678 |
unfolding f_def using pos by simp |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1679 |
hence "(\<integral>\<^isup>+ x. ?u x + ?mf x \<partial>M) = (\<integral>\<^isup>+ x. ?v x + ?f x \<partial>M)" by simp |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1680 |
hence "real (integral\<^isup>P M ?u + integral\<^isup>P M ?mf) = |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1681 |
real (integral\<^isup>P M ?v + integral\<^isup>P M ?f)" |
38656 | 1682 |
using positive_integral_add[OF u_borel mf_borel] |
1683 |
using positive_integral_add[OF v_borel f_borel] |
|
1684 |
by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1685 |
then show "integral\<^isup>L M f = integral\<^isup>L M u - integral\<^isup>L M v" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1686 |
using f mf `integrable M u` `integrable M v` |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1687 |
unfolding lebesgue_integral_def integrable_def * |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1688 |
by (cases "integral\<^isup>P M ?f", cases "integral\<^isup>P M ?mf", cases "integral\<^isup>P M ?v", cases "integral\<^isup>P M ?u") |
38656 | 1689 |
(auto simp add: field_simps) |
35582 | 1690 |
qed |
1691 |
||
38656 | 1692 |
lemma (in measure_space) integral_linear: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1693 |
assumes "integrable M f" "integrable M g" and "0 \<le> a" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1694 |
shows "integrable M (\<lambda>t. a * f t + g t)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1695 |
and "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" |
38656 | 1696 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1697 |
let ?PI = "integral\<^isup>P M" |
38656 | 1698 |
let "?f x" = "Real (f x)" |
1699 |
let "?g x" = "Real (g x)" |
|
1700 |
let "?mf x" = "Real (- f x)" |
|
1701 |
let "?mg x" = "Real (- g x)" |
|
1702 |
let "?p t" = "max 0 (a * f t) + max 0 (g t)" |
|
1703 |
let "?n t" = "max 0 (- (a * f t)) + max 0 (- g t)" |
|
1704 |
||
1705 |
have pos: "?f \<in> borel_measurable M" "?g \<in> borel_measurable M" |
|
1706 |
and neg: "?mf \<in> borel_measurable M" "?mg \<in> borel_measurable M" |
|
1707 |
and p: "?p \<in> borel_measurable M" |
|
1708 |
and n: "?n \<in> borel_measurable M" |
|
1709 |
using assms by (simp_all add: integrable_def) |
|
35582 | 1710 |
|
38656 | 1711 |
have *: "\<And>x. Real (?p x) = Real a * ?f x + ?g x" |
1712 |
"\<And>x. Real (?n x) = Real a * ?mf x + ?mg x" |
|
1713 |
"\<And>x. Real (- ?p x) = 0" |
|
1714 |
"\<And>x. Real (- ?n x) = 0" |
|
1715 |
using `0 \<le> a` by (auto simp: max_def min_def zero_le_mult_iff mult_le_0_iff add_nonpos_nonpos) |
|
1716 |
||
1717 |
note linear = |
|
1718 |
positive_integral_linear[OF pos] |
|
1719 |
positive_integral_linear[OF neg] |
|
35582 | 1720 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1721 |
have "integrable M ?p" "integrable M ?n" |
38656 | 1722 |
"\<And>t. a * f t + g t = ?p t - ?n t" "\<And>t. 0 \<le> ?p t" "\<And>t. 0 \<le> ?n t" |
1723 |
using assms p n unfolding integrable_def * linear by auto |
|
1724 |
note diff = integral_of_positive_diff[OF this] |
|
1725 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1726 |
show "integrable M (\<lambda>t. a * f t + g t)" by (rule diff) |
38656 | 1727 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1728 |
from assms show "(\<integral> t. a * f t + g t \<partial>M) = a * integral\<^isup>L M f + integral\<^isup>L M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1729 |
unfolding diff(2) unfolding lebesgue_integral_def * linear integrable_def |
38656 | 1730 |
by (cases "?PI ?f", cases "?PI ?mf", cases "?PI ?g", cases "?PI ?mg") |
1731 |
(auto simp add: field_simps zero_le_mult_iff) |
|
1732 |
qed |
|
1733 |
||
1734 |
lemma (in measure_space) integral_add[simp, intro]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1735 |
assumes "integrable M f" "integrable M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1736 |
shows "integrable M (\<lambda>t. f t + g t)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1737 |
and "(\<integral> t. f t + g t \<partial>M) = integral\<^isup>L M f + integral\<^isup>L M g" |
38656 | 1738 |
using assms integral_linear[where a=1] by auto |
1739 |
||
1740 |
lemma (in measure_space) integral_zero[simp, intro]: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1741 |
shows "integrable M (\<lambda>x. 0)" "(\<integral> x.0 \<partial>M) = 0" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1742 |
unfolding integrable_def lebesgue_integral_def |
38656 | 1743 |
by (auto simp add: borel_measurable_const) |
35582 | 1744 |
|
38656 | 1745 |
lemma (in measure_space) integral_cmult[simp, intro]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1746 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1747 |
shows "integrable M (\<lambda>t. a * f t)" (is ?P) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1748 |
and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I) |
38656 | 1749 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1750 |
have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" |
38656 | 1751 |
proof (cases rule: le_cases) |
1752 |
assume "0 \<le> a" show ?thesis |
|
1753 |
using integral_linear[OF assms integral_zero(1) `0 \<le> a`] |
|
1754 |
by (simp add: integral_zero) |
|
1755 |
next |
|
1756 |
assume "a \<le> 0" hence "0 \<le> - a" by auto |
|
1757 |
have *: "\<And>t. - a * t + 0 = (-a) * t" by simp |
|
1758 |
show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`] |
|
1759 |
integral_minus(1)[of "\<lambda>t. - a * f t"] |
|
1760 |
unfolding * integral_zero by simp |
|
1761 |
qed |
|
1762 |
thus ?P ?I by auto |
|
35582 | 1763 |
qed |
1764 |
||
41096 | 1765 |
lemma (in measure_space) integral_multc: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1766 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1767 |
shows "(\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c" |
41096 | 1768 |
unfolding mult_commute[of _ c] integral_cmult[OF assms] .. |
1769 |
||
40859 | 1770 |
lemma (in measure_space) integral_mono_AE: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1771 |
assumes fg: "integrable M f" "integrable M g" |
40859 | 1772 |
and mono: "AE t. f t \<le> g t" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1773 |
shows "integral\<^isup>L M f \<le> integral\<^isup>L M g" |
40859 | 1774 |
proof - |
1775 |
have "AE x. Real (f x) \<le> Real (g x)" |
|
41705 | 1776 |
using mono by auto |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1777 |
moreover have "AE x. Real (- g x) \<le> Real (- f x)" |
41705 | 1778 |
using mono by auto |
40859 | 1779 |
ultimately show ?thesis using fg |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1780 |
by (auto simp: lebesgue_integral_def integrable_def diff_minus |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
1781 |
intro!: add_mono real_of_pextreal_mono positive_integral_mono_AE) |
40859 | 1782 |
qed |
1783 |
||
38656 | 1784 |
lemma (in measure_space) integral_mono: |
41705 | 1785 |
assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1786 |
shows "integral\<^isup>L M f \<le> integral\<^isup>L M g" |
41705 | 1787 |
using assms by (auto intro: integral_mono_AE) |
35582 | 1788 |
|
38656 | 1789 |
lemma (in measure_space) integral_diff[simp, intro]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1790 |
assumes f: "integrable M f" and g: "integrable M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1791 |
shows "integrable M (\<lambda>t. f t - g t)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1792 |
and "(\<integral> t. f t - g t \<partial>M) = integral\<^isup>L M f - integral\<^isup>L M g" |
38656 | 1793 |
using integral_add[OF f integral_minus(1)[OF g]] |
1794 |
unfolding diff_minus integral_minus(2)[OF g] |
|
1795 |
by auto |
|
1796 |
||
1797 |
lemma (in measure_space) integral_indicator[simp, intro]: |
|
1798 |
assumes "a \<in> sets M" and "\<mu> a \<noteq> \<omega>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1799 |
shows "integral\<^isup>L M (indicator a) = real (\<mu> a)" (is ?int) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1800 |
and "integrable M (indicator a)" (is ?able) |
35582 | 1801 |
proof - |
38656 | 1802 |
have *: |
1803 |
"\<And>A x. Real (indicator A x) = indicator A x" |
|
1804 |
"\<And>A x. Real (- indicator A x) = 0" unfolding indicator_def by auto |
|
1805 |
show ?int ?able |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1806 |
using assms unfolding lebesgue_integral_def integrable_def |
38656 | 1807 |
by (auto simp: * positive_integral_indicator borel_measurable_indicator) |
35582 | 1808 |
qed |
1809 |
||
38656 | 1810 |
lemma (in measure_space) integral_cmul_indicator: |
1811 |
assumes "A \<in> sets M" and "c \<noteq> 0 \<Longrightarrow> \<mu> A \<noteq> \<omega>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1812 |
shows "integrable M (\<lambda>x. c * indicator A x)" (is ?P) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1813 |
and "(\<integral>x. c * indicator A x \<partial>M) = c * real (\<mu> A)" (is ?I) |
38656 | 1814 |
proof - |
1815 |
show ?P |
|
1816 |
proof (cases "c = 0") |
|
1817 |
case False with assms show ?thesis by simp |
|
1818 |
qed simp |
|
35582 | 1819 |
|
38656 | 1820 |
show ?I |
1821 |
proof (cases "c = 0") |
|
1822 |
case False with assms show ?thesis by simp |
|
1823 |
qed simp |
|
1824 |
qed |
|
35582 | 1825 |
|
38656 | 1826 |
lemma (in measure_space) integral_setsum[simp, intro]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1827 |
assumes "\<And>n. n \<in> S \<Longrightarrow> integrable M (f n)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1828 |
shows "(\<integral>x. (\<Sum> i \<in> S. f i x) \<partial>M) = (\<Sum> i \<in> S. integral\<^isup>L M (f i))" (is "?int S") |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1829 |
and "integrable M (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I S") |
35582 | 1830 |
proof - |
38656 | 1831 |
have "?int S \<and> ?I S" |
1832 |
proof (cases "finite S") |
|
1833 |
assume "finite S" |
|
1834 |
from this assms show ?thesis by (induct S) simp_all |
|
1835 |
qed simp |
|
35582 | 1836 |
thus "?int S" and "?I S" by auto |
1837 |
qed |
|
1838 |
||
36624 | 1839 |
lemma (in measure_space) integrable_abs: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1840 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1841 |
shows "integrable M (\<lambda> x. \<bar>f x\<bar>)" |
36624 | 1842 |
proof - |
38656 | 1843 |
have *: |
1844 |
"\<And>x. Real \<bar>f x\<bar> = Real (f x) + Real (- f x)" |
|
1845 |
"\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto |
|
1846 |
have abs: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M" and |
|
1847 |
f: "(\<lambda>x. Real (f x)) \<in> borel_measurable M" |
|
1848 |
"(\<lambda>x. Real (- f x)) \<in> borel_measurable M" |
|
1849 |
using assms unfolding integrable_def by auto |
|
1850 |
from abs assms show ?thesis unfolding integrable_def * |
|
1851 |
using positive_integral_linear[OF f, of 1] by simp |
|
1852 |
qed |
|
1853 |
||
41545 | 1854 |
lemma (in measure_space) integral_subalgebra: |
1855 |
assumes borel: "f \<in> borel_measurable N" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1856 |
and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> measure N A = \<mu> A" and sa: "sigma_algebra N" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1857 |
shows "integrable N f \<longleftrightarrow> integrable M f" (is ?P) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1858 |
and "integral\<^isup>L N f = integral\<^isup>L M f" (is ?I) |
41545 | 1859 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1860 |
interpret N: measure_space N using measure_space_subalgebra[OF sa N] . |
41545 | 1861 |
have "(\<lambda>x. Real (f x)) \<in> borel_measurable N" "(\<lambda>x. Real (- f x)) \<in> borel_measurable N" |
1862 |
using borel by auto |
|
1863 |
note * = this[THEN positive_integral_subalgebra[OF _ N sa]] |
|
1864 |
have "f \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable N" |
|
1865 |
using assms unfolding measurable_def by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1866 |
then show ?P ?I by (auto simp: * integrable_def lebesgue_integral_def) |
41545 | 1867 |
qed |
1868 |
||
38656 | 1869 |
lemma (in measure_space) integrable_bound: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1870 |
assumes "integrable M f" |
38656 | 1871 |
and f: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" |
1872 |
"\<And>x. x \<in> space M \<Longrightarrow> \<bar>g x\<bar> \<le> f x" |
|
1873 |
assumes borel: "g \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1874 |
shows "integrable M g" |
38656 | 1875 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1876 |
have "(\<integral>\<^isup>+ x. Real (g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. Real \<bar>g x\<bar> \<partial>M)" |
38656 | 1877 |
by (auto intro!: positive_integral_mono) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1878 |
also have "\<dots> \<le> (\<integral>\<^isup>+ x. Real (f x) \<partial>M)" |
38656 | 1879 |
using f by (auto intro!: positive_integral_mono) |
1880 |
also have "\<dots> < \<omega>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1881 |
using `integrable M f` unfolding integrable_def by (auto simp: pextreal_less_\<omega>) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1882 |
finally have pos: "(\<integral>\<^isup>+ x. Real (g x) \<partial>M) < \<omega>" . |
38656 | 1883 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1884 |
have "(\<integral>\<^isup>+ x. Real (- g x) \<partial>M) \<le> (\<integral>\<^isup>+ x. Real (\<bar>g x\<bar>) \<partial>M)" |
38656 | 1885 |
by (auto intro!: positive_integral_mono) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1886 |
also have "\<dots> \<le> (\<integral>\<^isup>+ x. Real (f x) \<partial>M)" |
38656 | 1887 |
using f by (auto intro!: positive_integral_mono) |
1888 |
also have "\<dots> < \<omega>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1889 |
using `integrable M f` unfolding integrable_def by (auto simp: pextreal_less_\<omega>) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1890 |
finally have neg: "(\<integral>\<^isup>+ x. Real (- g x) \<partial>M) < \<omega>" . |
38656 | 1891 |
|
1892 |
from neg pos borel show ?thesis |
|
36624 | 1893 |
unfolding integrable_def by auto |
38656 | 1894 |
qed |
1895 |
||
1896 |
lemma (in measure_space) integrable_abs_iff: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1897 |
"f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda> x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f" |
38656 | 1898 |
by (auto intro!: integrable_bound[where g=f] integrable_abs) |
1899 |
||
1900 |
lemma (in measure_space) integrable_max: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1901 |
assumes int: "integrable M f" "integrable M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1902 |
shows "integrable M (\<lambda> x. max (f x) (g x))" |
38656 | 1903 |
proof (rule integrable_bound) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1904 |
show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)" |
38656 | 1905 |
using int by (simp add: integrable_abs) |
1906 |
show "(\<lambda>x. max (f x) (g x)) \<in> borel_measurable M" |
|
1907 |
using int unfolding integrable_def by auto |
|
1908 |
next |
|
1909 |
fix x assume "x \<in> space M" |
|
1910 |
show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>max (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" |
|
1911 |
by auto |
|
1912 |
qed |
|
1913 |
||
1914 |
lemma (in measure_space) integrable_min: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1915 |
assumes int: "integrable M f" "integrable M g" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1916 |
shows "integrable M (\<lambda> x. min (f x) (g x))" |
38656 | 1917 |
proof (rule integrable_bound) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1918 |
show "integrable M (\<lambda>x. \<bar>f x\<bar> + \<bar>g x\<bar>)" |
38656 | 1919 |
using int by (simp add: integrable_abs) |
1920 |
show "(\<lambda>x. min (f x) (g x)) \<in> borel_measurable M" |
|
1921 |
using int unfolding integrable_def by auto |
|
1922 |
next |
|
1923 |
fix x assume "x \<in> space M" |
|
1924 |
show "0 \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" "\<bar>min (f x) (g x)\<bar> \<le> \<bar>f x\<bar> + \<bar>g x\<bar>" |
|
1925 |
by auto |
|
1926 |
qed |
|
1927 |
||
1928 |
lemma (in measure_space) integral_triangle_inequality: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1929 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1930 |
shows "\<bar>integral\<^isup>L M f\<bar> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)" |
38656 | 1931 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1932 |
have "\<bar>integral\<^isup>L M f\<bar> = max (integral\<^isup>L M f) (- integral\<^isup>L M f)" by auto |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1933 |
also have "\<dots> \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)" |
38656 | 1934 |
using assms integral_minus(2)[of f, symmetric] |
1935 |
by (auto intro!: integral_mono integrable_abs simp del: integral_minus) |
|
1936 |
finally show ?thesis . |
|
36624 | 1937 |
qed |
1938 |
||
38656 | 1939 |
lemma (in measure_space) integral_positive: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1940 |
assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1941 |
shows "0 \<le> integral\<^isup>L M f" |
38656 | 1942 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1943 |
have "0 = (\<integral>x. 0 \<partial>M)" by (auto simp: integral_zero) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1944 |
also have "\<dots> \<le> integral\<^isup>L M f" |
38656 | 1945 |
using assms by (rule integral_mono[OF integral_zero(1)]) |
1946 |
finally show ?thesis . |
|
1947 |
qed |
|
1948 |
||
1949 |
lemma (in measure_space) integral_monotone_convergence_pos: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1950 |
assumes i: "\<And>i. integrable M (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)" |
38656 | 1951 |
and pos: "\<And>x i. 0 \<le> f i x" |
1952 |
and lim: "\<And>x. (\<lambda>i. f i x) ----> u x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1953 |
and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1954 |
shows "integrable M u" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1955 |
and "integral\<^isup>L M u = x" |
35582 | 1956 |
proof - |
38656 | 1957 |
{ fix x have "0 \<le> u x" |
1958 |
using mono pos[of 0 x] incseq_le[OF _ lim, of x 0] |
|
1959 |
by (simp add: mono_def incseq_def) } |
|
1960 |
note pos_u = this |
|
1961 |
||
1962 |
hence [simp]: "\<And>i x. Real (- f i x) = 0" "\<And>x. Real (- u x) = 0" |
|
1963 |
using pos by auto |
|
1964 |
||
1965 |
have SUP_F: "\<And>x. (SUP n. Real (f n x)) = Real (u x)" |
|
1966 |
using mono pos pos_u lim by (rule SUP_eq_LIMSEQ[THEN iffD2]) |
|
1967 |
||
1968 |
have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M" |
|
1969 |
using i unfolding integrable_def by auto |
|
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1970 |
hence "(\<lambda>x. SUP i. Real (f i x)) \<in> borel_measurable M" |
35582 | 1971 |
by auto |
38656 | 1972 |
hence borel_u: "u \<in> borel_measurable M" |
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
1973 |
using pos_u by (auto simp: borel_measurable_Real_eq SUP_F) |
38656 | 1974 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1975 |
have integral_eq: "\<And>n. (\<integral>\<^isup>+ x. Real (f n x) \<partial>M) = Real (integral\<^isup>L M (f n))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1976 |
using i unfolding lebesgue_integral_def integrable_def by (auto simp: Real_real) |
38656 | 1977 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1978 |
have pos_integral: "\<And>n. 0 \<le> integral\<^isup>L M (f n)" |
38656 | 1979 |
using pos i by (auto simp: integral_positive) |
1980 |
hence "0 \<le> x" |
|
1981 |
using LIMSEQ_le_const[OF ilim, of 0] by auto |
|
1982 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1983 |
have "(\<lambda>i. (\<integral>\<^isup>+ x. Real (f i x) \<partial>M)) \<up> (\<integral>\<^isup>+ x. Real (u x) \<partial>M)" |
38656 | 1984 |
proof (rule positive_integral_isoton) |
1985 |
from SUP_F mono pos |
|
1986 |
show "(\<lambda>i x. Real (f i x)) \<up> (\<lambda>x. Real (u x))" |
|
1987 |
unfolding isoton_fun_expand by (auto simp: isoton_def mono_def) |
|
1988 |
qed (rule borel_f) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1989 |
hence pI: "(\<integral>\<^isup>+ x. Real (u x) \<partial>M) = (SUP n. (\<integral>\<^isup>+ x. Real (f n x) \<partial>M))" |
38656 | 1990 |
unfolding isoton_def by simp |
1991 |
also have "\<dots> = Real x" unfolding integral_eq |
|
1992 |
proof (rule SUP_eq_LIMSEQ[THEN iffD2]) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1993 |
show "mono (\<lambda>n. integral\<^isup>L M (f n))" |
38656 | 1994 |
using mono i by (auto simp: mono_def intro!: integral_mono) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1995 |
show "\<And>n. 0 \<le> integral\<^isup>L M (f n)" using pos_integral . |
38656 | 1996 |
show "0 \<le> x" using `0 \<le> x` . |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1997 |
show "(\<lambda>n. integral\<^isup>L M (f n)) ----> x" using ilim . |
38656 | 1998 |
qed |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
1999 |
finally show "integrable M u" "integral\<^isup>L M u = x" using borel_u `0 \<le> x` |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2000 |
unfolding integrable_def lebesgue_integral_def by auto |
38656 | 2001 |
qed |
2002 |
||
2003 |
lemma (in measure_space) integral_monotone_convergence: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2004 |
assumes f: "\<And>i. integrable M (f i)" and "mono f" |
38656 | 2005 |
and lim: "\<And>x. (\<lambda>i. f i x) ----> u x" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2006 |
and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2007 |
shows "integrable M u" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2008 |
and "integral\<^isup>L M u = x" |
38656 | 2009 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2010 |
have 1: "\<And>i. integrable M (\<lambda>x. f i x - f 0 x)" |
38656 | 2011 |
using f by (auto intro!: integral_diff) |
2012 |
have 2: "\<And>x. mono (\<lambda>n. f n x - f 0 x)" using `mono f` |
|
2013 |
unfolding mono_def le_fun_def by auto |
|
2014 |
have 3: "\<And>x n. 0 \<le> f n x - f 0 x" using `mono f` |
|
2015 |
unfolding mono_def le_fun_def by (auto simp: field_simps) |
|
2016 |
have 4: "\<And>x. (\<lambda>i. f i x - f 0 x) ----> u x - f 0 x" |
|
2017 |
using lim by (auto intro!: LIMSEQ_diff) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2018 |
have 5: "(\<lambda>i. (\<integral>x. f i x - f 0 x \<partial>M)) ----> x - integral\<^isup>L M (f 0)" |
38656 | 2019 |
using f ilim by (auto intro!: LIMSEQ_diff simp: integral_diff) |
2020 |
note diff = integral_monotone_convergence_pos[OF 1 2 3 4 5] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2021 |
have "integrable M (\<lambda>x. (u x - f 0 x) + f 0 x)" |
38656 | 2022 |
using diff(1) f by (rule integral_add(1)) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2023 |
with diff(2) f show "integrable M u" "integral\<^isup>L M u = x" |
38656 | 2024 |
by (auto simp: integral_diff) |
2025 |
qed |
|
2026 |
||
2027 |
lemma (in measure_space) integral_0_iff: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2028 |
assumes "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2029 |
shows "(\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> \<mu> {x\<in>space M. f x \<noteq> 0} = 0" |
38656 | 2030 |
proof - |
2031 |
have *: "\<And>x. Real (- \<bar>f x\<bar>) = 0" by auto |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2032 |
have "integrable M (\<lambda>x. \<bar>f x\<bar>)" using assms by (rule integrable_abs) |
38656 | 2033 |
hence "(\<lambda>x. Real (\<bar>f x\<bar>)) \<in> borel_measurable M" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2034 |
"(\<integral>\<^isup>+ x. Real \<bar>f x\<bar> \<partial>M) \<noteq> \<omega>" unfolding integrable_def by auto |
38656 | 2035 |
from positive_integral_0_iff[OF this(1)] this(2) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2036 |
show ?thesis unfolding lebesgue_integral_def * |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
2037 |
by (simp add: real_of_pextreal_eq_0) |
35582 | 2038 |
qed |
2039 |
||
40859 | 2040 |
lemma (in measure_space) positive_integral_omega: |
2041 |
assumes "f \<in> borel_measurable M" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2042 |
and "integral\<^isup>P M f \<noteq> \<omega>" |
40859 | 2043 |
shows "\<mu> (f -` {\<omega>} \<inter> space M) = 0" |
2044 |
proof - |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2045 |
have "\<omega> * \<mu> (f -` {\<omega>} \<inter> space M) = (\<integral>\<^isup>+ x. \<omega> * indicator (f -` {\<omega>} \<inter> space M) x \<partial>M)" |
40859 | 2046 |
using positive_integral_cmult_indicator[OF borel_measurable_vimage, OF assms(1), of \<omega> \<omega>] by simp |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2047 |
also have "\<dots> \<le> integral\<^isup>P M f" |
40859 | 2048 |
by (auto intro!: positive_integral_mono simp: indicator_def) |
2049 |
finally show ?thesis |
|
2050 |
using assms(2) by (cases ?thesis) auto |
|
2051 |
qed |
|
2052 |
||
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2053 |
lemma (in measure_space) positive_integral_omega_AE: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2054 |
assumes "f \<in> borel_measurable M" "integral\<^isup>P M f \<noteq> \<omega>" shows "AE x. f x \<noteq> \<omega>" |
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2055 |
proof (rule AE_I) |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2056 |
show "\<mu> (f -` {\<omega>} \<inter> space M) = 0" |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2057 |
by (rule positive_integral_omega[OF assms]) |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2058 |
show "f -` {\<omega>} \<inter> space M \<in> sets M" |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2059 |
using assms by (auto intro: borel_measurable_vimage) |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2060 |
qed auto |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2061 |
|
40859 | 2062 |
lemma (in measure_space) simple_integral_omega: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2063 |
assumes "simple_function M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2064 |
and "integral\<^isup>S M f \<noteq> \<omega>" |
40859 | 2065 |
shows "\<mu> (f -` {\<omega>} \<inter> space M) = 0" |
2066 |
proof (rule positive_integral_omega) |
|
2067 |
show "f \<in> borel_measurable M" using assms by (auto intro: borel_measurable_simple_function) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2068 |
show "integral\<^isup>P M f \<noteq> \<omega>" |
40859 | 2069 |
using assms by (simp add: positive_integral_eq_simple_integral) |
2070 |
qed |
|
2071 |
||
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2072 |
lemma (in measure_space) integral_real: |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2073 |
fixes f :: "'a \<Rightarrow> pextreal" |
41705 | 2074 |
assumes [simp]: "AE x. f x \<noteq> \<omega>" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2075 |
shows "(\<integral>x. real (f x) \<partial>M) = real (integral\<^isup>P M f)" (is ?plus) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2076 |
and "(\<integral>x. - real (f x) \<partial>M) = - real (integral\<^isup>P M f)" (is ?minus) |
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2077 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2078 |
have "(\<integral>\<^isup>+ x. Real (real (f x)) \<partial>M) = integral\<^isup>P M f" |
41705 | 2079 |
by (auto intro!: positive_integral_cong_AE simp: Real_real) |
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2080 |
moreover |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2081 |
have "(\<integral>\<^isup>+ x. Real (- real (f x)) \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)" |
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2082 |
by (intro positive_integral_cong) auto |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2083 |
ultimately show ?plus ?minus |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2084 |
by (auto simp: lebesgue_integral_def integrable_def) |
41026
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2085 |
qed |
bea75746dc9d
folding on arbitrary Lebesgue integrable functions
hoelzl
parents:
41023
diff
changeset
|
2086 |
|
38656 | 2087 |
lemma (in measure_space) integral_dominated_convergence: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2088 |
assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x" |
41705 | 2089 |
and w: "integrable M w" |
38656 | 2090 |
and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2091 |
shows "integrable M u'" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2092 |
and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff") |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2093 |
and "(\<lambda>i. integral\<^isup>L M (u i)) ----> integral\<^isup>L M u'" (is ?lim) |
36624 | 2094 |
proof - |
38656 | 2095 |
{ fix x j assume x: "x \<in> space M" |
2096 |
from u'[OF x] have "(\<lambda>i. \<bar>u i x\<bar>) ----> \<bar>u' x\<bar>" by (rule LIMSEQ_imp_rabs) |
|
2097 |
from LIMSEQ_le_const2[OF this] |
|
2098 |
have "\<bar>u' x\<bar> \<le> w x" using bound[OF x] by auto } |
|
2099 |
note u'_bound = this |
|
2100 |
||
2101 |
from u[unfolded integrable_def] |
|
2102 |
have u'_borel: "u' \<in> borel_measurable M" |
|
2103 |
using u' by (blast intro: borel_measurable_LIMSEQ[of u]) |
|
2104 |
||
41705 | 2105 |
{ fix x assume x: "x \<in> space M" |
2106 |
then have "0 \<le> \<bar>u 0 x\<bar>" by auto |
|
2107 |
also have "\<dots> \<le> w x" using bound[OF x] by auto |
|
2108 |
finally have "0 \<le> w x" . } |
|
2109 |
note w_pos = this |
|
2110 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2111 |
show "integrable M u'" |
38656 | 2112 |
proof (rule integrable_bound) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2113 |
show "integrable M w" by fact |
38656 | 2114 |
show "u' \<in> borel_measurable M" by fact |
2115 |
next |
|
41705 | 2116 |
fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact |
38656 | 2117 |
show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] . |
2118 |
qed |
|
2119 |
||
2120 |
let "?diff n x" = "2 * w x - \<bar>u n x - u' x\<bar>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2121 |
have diff: "\<And>n. integrable M (\<lambda>x. \<bar>u n x - u' x\<bar>)" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2122 |
using w u `integrable M u'` |
38656 | 2123 |
by (auto intro!: integral_add integral_diff integral_cmult integrable_abs) |
2124 |
||
2125 |
{ fix j x assume x: "x \<in> space M" |
|
2126 |
have "\<bar>u j x - u' x\<bar> \<le> \<bar>u j x\<bar> + \<bar>u' x\<bar>" by auto |
|
2127 |
also have "\<dots> \<le> w x + w x" |
|
2128 |
by (rule add_mono[OF bound[OF x] u'_bound[OF x]]) |
|
2129 |
finally have "\<bar>u j x - u' x\<bar> \<le> 2 * w x" by simp } |
|
2130 |
note diff_less_2w = this |
|
2131 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2132 |
have PI_diff: "\<And>m n. (\<integral>\<^isup>+ x. Real (?diff (m + n) x) \<partial>M) = |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2133 |
(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)" |
41705 | 2134 |
using diff w diff_less_2w w_pos |
38656 | 2135 |
by (subst positive_integral_diff[symmetric]) |
2136 |
(auto simp: integrable_def intro!: positive_integral_cong) |
|
2137 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2138 |
have "integrable M (\<lambda>x. 2 * w x)" |
38656 | 2139 |
using w by (auto intro: integral_cmult) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2140 |
hence I2w_fin: "(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) \<noteq> \<omega>" and |
38656 | 2141 |
borel_2w: "(\<lambda>x. Real (2 * w x)) \<in> borel_measurable M" |
2142 |
unfolding integrable_def by auto |
|
2143 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2144 |
have "(INF n. SUP m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)) = 0" (is "?lim_SUP = 0") |
38656 | 2145 |
proof cases |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2146 |
assume eq_0: "(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) = 0" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2147 |
have "\<And>i. (\<integral>\<^isup>+ x. Real \<bar>u i x - u' x\<bar> \<partial>M) \<le> (\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M)" |
38656 | 2148 |
proof (rule positive_integral_mono) |
2149 |
fix i x assume "x \<in> space M" from diff_less_2w[OF this, of i] |
|
2150 |
show "Real \<bar>u i x - u' x\<bar> \<le> Real (2 * w x)" by auto |
|
2151 |
qed |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2152 |
hence "\<And>i. (\<integral>\<^isup>+ x. Real \<bar>u i x - u' x\<bar> \<partial>M) = 0" using eq_0 by auto |
38656 | 2153 |
thus ?thesis by simp |
2154 |
next |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2155 |
assume neq_0: "(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) \<noteq> 0" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2156 |
have "(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) = (\<integral>\<^isup>+ x. (SUP n. INF m. Real (?diff (m + n) x)) \<partial>M)" |
41097
a1abfa4e2b44
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
hoelzl
parents:
41096
diff
changeset
|
2157 |
proof (rule positive_integral_cong, subst add_commute) |
38656 | 2158 |
fix x assume x: "x \<in> space M" |
2159 |
show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))" |
|
2160 |
proof (rule LIMSEQ_imp_lim_INF[symmetric]) |
|
2161 |
fix j show "0 \<le> ?diff j x" using diff_less_2w[OF x, of j] by simp |
|
2162 |
next |
|
2163 |
have "(\<lambda>i. ?diff i x) ----> 2 * w x - \<bar>u' x - u' x\<bar>" |
|
2164 |
using u'[OF x] by (safe intro!: LIMSEQ_diff LIMSEQ_const LIMSEQ_imp_rabs) |
|
2165 |
thus "(\<lambda>i. ?diff i x) ----> 2 * w x" by simp |
|
2166 |
qed |
|
2167 |
qed |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2168 |
also have "\<dots> \<le> (SUP n. INF m. (\<integral>\<^isup>+ x. Real (?diff (m + n) x) \<partial>M))" |
38656 | 2169 |
using u'_borel w u unfolding integrable_def |
2170 |
by (auto intro!: positive_integral_lim_INF) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2171 |
also have "\<dots> = (\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) - |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2172 |
(INF n. SUP m. \<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
2173 |
unfolding PI_diff pextreal_INF_minus[OF I2w_fin] pextreal_SUP_minus .. |
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
2174 |
finally show ?thesis using neq_0 I2w_fin by (rule pextreal_le_minus_imp_0) |
38656 | 2175 |
qed |
41705 | 2176 |
|
38656 | 2177 |
have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto |
2178 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2179 |
have [simp]: "\<And>n m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M) = |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2180 |
Real ((\<integral>x. \<bar>u (n + m) x - u' x\<bar> \<partial>M))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2181 |
using diff by (subst add_commute) (simp add: lebesgue_integral_def integrable_def Real_real) |
38656 | 2182 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2183 |
have "(SUP n. INF m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)) \<le> ?lim_SUP" |
38656 | 2184 |
(is "?lim_INF \<le> _") by (subst (1 2) add_commute) (rule lim_INF_le_lim_SUP) |
2185 |
hence "?lim_INF = Real 0" "?lim_SUP = Real 0" using `?lim_SUP = 0` by auto |
|
2186 |
thus ?lim_diff using diff by (auto intro!: integral_positive lim_INF_eq_lim_SUP) |
|
2187 |
||
2188 |
show ?lim |
|
2189 |
proof (rule LIMSEQ_I) |
|
2190 |
fix r :: real assume "0 < r" |
|
2191 |
from LIMSEQ_D[OF `?lim_diff` this] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2192 |
obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M) < r" |
38656 | 2193 |
using diff by (auto simp: integral_positive) |
2194 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2195 |
show "\<exists>N. \<forall>n\<ge>N. norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r" |
38656 | 2196 |
proof (safe intro!: exI[of _ N]) |
2197 |
fix n assume "N \<le> n" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2198 |
have "\<bar>integral\<^isup>L M (u n) - integral\<^isup>L M u'\<bar> = \<bar>(\<integral>x. u n x - u' x \<partial>M)\<bar>" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2199 |
using u `integrable M u'` by (auto simp: integral_diff) |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2200 |
also have "\<dots> \<le> (\<integral>x. \<bar>u n x - u' x\<bar> \<partial>M)" using u `integrable M u'` |
38656 | 2201 |
by (rule_tac integral_triangle_inequality) (auto intro!: integral_diff) |
2202 |
also note N[OF `N \<le> n`] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2203 |
finally show "norm (integral\<^isup>L M (u n) - integral\<^isup>L M u') < r" by simp |
38656 | 2204 |
qed |
2205 |
qed |
|
2206 |
qed |
|
2207 |
||
2208 |
lemma (in measure_space) integral_sums: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2209 |
assumes borel: "\<And>i. integrable M (f i)" |
38656 | 2210 |
and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)" |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2211 |
and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2212 |
shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S") |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2213 |
and "(\<lambda>i. integral\<^isup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is ?integral) |
38656 | 2214 |
proof - |
2215 |
have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w" |
|
2216 |
using summable unfolding summable_def by auto |
|
2217 |
from bchoice[OF this] |
|
2218 |
obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto |
|
2219 |
||
2220 |
let "?w y" = "if y \<in> space M then w y else 0" |
|
2221 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2222 |
obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x" |
38656 | 2223 |
using sums unfolding summable_def .. |
2224 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2225 |
have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i = 0..<n. f i x)" |
38656 | 2226 |
using borel by (auto intro!: integral_setsum) |
2227 |
||
2228 |
{ fix j x assume [simp]: "x \<in> space M" |
|
2229 |
have "\<bar>\<Sum>i = 0..< j. f i x\<bar> \<le> (\<Sum>i = 0..< j. \<bar>f i x\<bar>)" by (rule setsum_abs) |
|
2230 |
also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto |
|
2231 |
finally have "\<bar>\<Sum>i = 0..<j. f i x\<bar> \<le> ?w x" by simp } |
|
2232 |
note 2 = this |
|
2233 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2234 |
have 3: "integrable M ?w" |
38656 | 2235 |
proof (rule integral_monotone_convergence(1)) |
2236 |
let "?F n y" = "(\<Sum>i = 0..<n. \<bar>f i y\<bar>)" |
|
2237 |
let "?w' n y" = "if y \<in> space M then ?F n y else 0" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2238 |
have "\<And>n. integrable M (?F n)" |
38656 | 2239 |
using borel by (auto intro!: integral_setsum integrable_abs) |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2240 |
thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong) |
38656 | 2241 |
show "mono ?w'" |
2242 |
by (auto simp: mono_def le_fun_def intro!: setsum_mono2) |
|
2243 |
{ fix x show "(\<lambda>n. ?w' n x) ----> ?w x" |
|
2244 |
using w by (cases "x \<in> space M") (simp_all add: LIMSEQ_const sums_def) } |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2245 |
have *: "\<And>n. integral\<^isup>L M (?w' n) = (\<Sum>i = 0..< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))" |
38656 | 2246 |
using borel by (simp add: integral_setsum integrable_abs cong: integral_cong) |
2247 |
from abs_sum |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2248 |
show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def . |
38656 | 2249 |
qed |
2250 |
||
2251 |
from summable[THEN summable_rabs_cancel] |
|
41705 | 2252 |
have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)" |
38656 | 2253 |
by (auto intro: summable_sumr_LIMSEQ_suminf) |
2254 |
||
41705 | 2255 |
note int = integral_dominated_convergence(1,3)[OF 1 2 3 4] |
38656 | 2256 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2257 |
from int show "integrable M ?S" by simp |
38656 | 2258 |
|
2259 |
show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF borel] |
|
2260 |
using int(2) by simp |
|
36624 | 2261 |
qed |
2262 |
||
35748 | 2263 |
section "Lebesgue integration on countable spaces" |
2264 |
||
38656 | 2265 |
lemma (in measure_space) integral_on_countable: |
2266 |
assumes f: "f \<in> borel_measurable M" |
|
35748 | 2267 |
and bij: "bij_betw enum S (f ` space M)" |
2268 |
and enum_zero: "enum ` (-S) \<subseteq> {0}" |
|
38656 | 2269 |
and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>" |
2270 |
and abs_summable: "summable (\<lambda>r. \<bar>enum r * real (\<mu> (f -` {enum r} \<inter> space M))\<bar>)" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2271 |
shows "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2272 |
and "(\<lambda>r. enum r * real (\<mu> (f -` {enum r} \<inter> space M))) sums integral\<^isup>L M f" (is ?sums) |
35748 | 2273 |
proof - |
38656 | 2274 |
let "?A r" = "f -` {enum r} \<inter> space M" |
2275 |
let "?F r x" = "enum r * indicator (?A r) x" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2276 |
have enum_eq: "\<And>r. enum r * real (\<mu> (?A r)) = integral\<^isup>L M (?F r)" |
38656 | 2277 |
using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) |
35748 | 2278 |
|
38656 | 2279 |
{ fix x assume "x \<in> space M" |
2280 |
hence "f x \<in> enum ` S" using bij unfolding bij_betw_def by auto |
|
2281 |
then obtain i where "i\<in>S" "enum i = f x" by auto |
|
2282 |
have F: "\<And>j. ?F j x = (if j = i then f x else 0)" |
|
2283 |
proof cases |
|
2284 |
fix j assume "j = i" |
|
2285 |
thus "?thesis j" using `x \<in> space M` `enum i = f x` by (simp add: indicator_def) |
|
2286 |
next |
|
2287 |
fix j assume "j \<noteq> i" |
|
2288 |
show "?thesis j" using bij `i \<in> S` `j \<noteq> i` `enum i = f x` enum_zero |
|
2289 |
by (cases "j \<in> S") (auto simp add: indicator_def bij_betw_def inj_on_def) |
|
2290 |
qed |
|
2291 |
hence F_abs: "\<And>j. \<bar>if j = i then f x else 0\<bar> = (if j = i then \<bar>f x\<bar> else 0)" by auto |
|
2292 |
have "(\<lambda>i. ?F i x) sums f x" |
|
2293 |
"(\<lambda>i. \<bar>?F i x\<bar>) sums \<bar>f x\<bar>" |
|
2294 |
by (auto intro!: sums_single simp: F F_abs) } |
|
2295 |
note F_sums_f = this(1) and F_abs_sums_f = this(2) |
|
35748 | 2296 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2297 |
have int_f: "integral\<^isup>L M f = (\<integral>x. (\<Sum>r. ?F r x) \<partial>M)" "integrable M f = integrable M (\<lambda>x. \<Sum>r. ?F r x)" |
38656 | 2298 |
using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff) |
35748 | 2299 |
|
2300 |
{ fix r |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2301 |
have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x \<partial>M)" |
38656 | 2302 |
by (auto simp: indicator_def intro!: integral_cong) |
2303 |
also have "\<dots> = \<bar>enum r\<bar> * real (\<mu> (?A r))" |
|
2304 |
using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2305 |
finally have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = \<bar>enum r * real (\<mu> (?A r))\<bar>" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
2306 |
by (simp add: abs_mult_pos real_pextreal_pos) } |
38656 | 2307 |
note int_abs_F = this |
35748 | 2308 |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2309 |
have 1: "\<And>i. integrable M (\<lambda>x. ?F i x)" |
38656 | 2310 |
using f fin by (simp add: borel_measurable_vimage integral_cmul_indicator) |
2311 |
||
2312 |
have 2: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>?F i x\<bar>)" |
|
2313 |
using F_abs_sums_f unfolding sums_iff by auto |
|
2314 |
||
2315 |
from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable] |
|
2316 |
show ?sums unfolding enum_eq int_f by simp |
|
2317 |
||
2318 |
from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable] |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2319 |
show "integrable M f" unfolding int_f by simp |
35748 | 2320 |
qed |
2321 |
||
35692 | 2322 |
section "Lebesgue integration on finite space" |
2323 |
||
38656 | 2324 |
lemma (in measure_space) integral_on_finite: |
2325 |
assumes f: "f \<in> borel_measurable M" and finite: "finite (f`space M)" |
|
2326 |
and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> \<mu> (f -` {x} \<inter> space M) \<noteq> \<omega>" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2327 |
shows "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2328 |
and "(\<integral>x. f x \<partial>M) = |
38656 | 2329 |
(\<Sum> r \<in> f`space M. r * real (\<mu> (f -` {r} \<inter> space M)))" (is "?integral") |
35582 | 2330 |
proof - |
38656 | 2331 |
let "?A r" = "f -` {r} \<inter> space M" |
2332 |
let "?S x" = "\<Sum>r\<in>f`space M. r * indicator (?A r) x" |
|
35582 | 2333 |
|
38656 | 2334 |
{ fix x assume "x \<in> space M" |
2335 |
have "f x = (\<Sum>r\<in>f`space M. if x \<in> ?A r then r else 0)" |
|
2336 |
using finite `x \<in> space M` by (simp add: setsum_cases) |
|
2337 |
also have "\<dots> = ?S x" |
|
2338 |
by (auto intro!: setsum_cong) |
|
2339 |
finally have "f x = ?S x" . } |
|
2340 |
note f_eq = this |
|
2341 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2342 |
have f_eq_S: "integrable M f \<longleftrightarrow> integrable M ?S" "integral\<^isup>L M f = integral\<^isup>L M ?S" |
38656 | 2343 |
by (auto intro!: integrable_cong integral_cong simp only: f_eq) |
2344 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2345 |
show "integrable M f" ?integral using fin f f_eq_S |
38656 | 2346 |
by (simp_all add: integral_cmul_indicator borel_measurable_vimage) |
35582 | 2347 |
qed |
2348 |
||
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2349 |
lemma (in finite_measure_space) simple_function_finite[simp, intro]: "simple_function M f" |
40875 | 2350 |
unfolding simple_function_def using finite_space by auto |
35977 | 2351 |
|
38705 | 2352 |
lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M" |
39092 | 2353 |
by (auto intro: borel_measurable_simple_function) |
38705 | 2354 |
|
2355 |
lemma (in finite_measure_space) positive_integral_finite_eq_setsum: |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2356 |
"integral\<^isup>P M f = (\<Sum>x \<in> space M. f x * \<mu> {x})" |
38705 | 2357 |
proof - |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2358 |
have *: "integral\<^isup>P M f = (\<integral>\<^isup>+ x. (\<Sum>y\<in>space M. f y * indicator {y} x) \<partial>M)" |
38705 | 2359 |
by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space]) |
2360 |
show ?thesis unfolding * using borel_measurable_finite[of f] |
|
40875 | 2361 |
by (simp add: positive_integral_setsum positive_integral_cmult_indicator) |
38705 | 2362 |
qed |
2363 |
||
35977 | 2364 |
lemma (in finite_measure_space) integral_finite_singleton: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2365 |
shows "integrable M f" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2366 |
and "integral\<^isup>L M f = (\<Sum>x \<in> space M. f x * real (\<mu> {x}))" (is ?I) |
35977 | 2367 |
proof - |
38705 | 2368 |
have [simp]: |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2369 |
"(\<integral>\<^isup>+ x. Real (f x) \<partial>M) = (\<Sum>x \<in> space M. Real (f x) * \<mu> {x})" |
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2370 |
"(\<integral>\<^isup>+ x. Real (- f x) \<partial>M) = (\<Sum>x \<in> space M. Real (- f x) * \<mu> {x})" |
38705 | 2371 |
unfolding positive_integral_finite_eq_setsum by auto |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2372 |
show "integrable M f" using finite_space finite_measure |
40875 | 2373 |
by (simp add: setsum_\<omega> integrable_def) |
38705 | 2374 |
show ?I using finite_measure |
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset
|
2375 |
apply (simp add: lebesgue_integral_def real_of_pextreal_setsum[symmetric] |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40875
diff
changeset
|
2376 |
real_of_pextreal_mult[symmetric] setsum_subtractf[symmetric]) |
38705 | 2377 |
by (rule setsum_cong) (simp_all split: split_if) |
35977 | 2378 |
qed |
2379 |
||
35748 | 2380 |
end |