author  hoelzl 
Tue, 12 Nov 2013 19:28:56 +0100  
changeset 54418  3b8e33d1a39a 
parent 54417  dbb8ecfe1337 
child 54611  31afce809794 
permissions  rwrr 
42067  1 
(* Title: HOL/Probability/Lebesgue_Integration.thy 
2 
Author: Johannes Hölzl, TU München 

3 
Author: Armin Heller, TU München 

4 
*) 

38656  5 

35582  6 
header {*Lebesgue Integration*} 
7 

38656  8 
theory Lebesgue_Integration 
47694  9 
imports Measure_Space Borel_Space 
35582  10 
begin 
11 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

12 
lemma tendsto_real_max: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

13 
fixes x y :: real 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

14 
assumes "(X > x) net" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

15 
assumes "(Y > y) net" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

16 
shows "((\<lambda>x. max (X x) (Y x)) > max x y) net" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

17 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

18 
have *: "\<And>x y :: real. max x y = y + ((x  y) + norm (x  y)) / 2" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

19 
by (auto split: split_max simp: field_simps) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

20 
show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

21 
unfolding * 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

22 
by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

23 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

24 

47694  25 
lemma measurable_sets2[intro]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

26 
assumes "f \<in> measurable M M'" "g \<in> measurable M M''" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

27 
and "A \<in> sets M'" "B \<in> sets M''" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

28 
shows "f ` A \<inter> g ` B \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

29 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

30 
have "f ` A \<inter> g ` B \<inter> space M = (f ` A \<inter> space M) \<inter> (g ` B \<inter> space M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

31 
by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

32 
then show ?thesis using assms by (auto intro: measurable_sets) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

33 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

34 

38656  35 
section "Simple function" 
35582  36 

38656  37 
text {* 
38 

39 
Our simple functions are not restricted to positive real numbers. Instead 

40 
they are just functions with a finite range and are measurable when singleton 

41 
sets are measurable. 

35582  42 

38656  43 
*} 
44 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

45 
definition "simple_function M g \<longleftrightarrow> 
38656  46 
finite (g ` space M) \<and> 
47 
(\<forall>x \<in> g ` space M. g ` {x} \<inter> space M \<in> sets M)" 

36624  48 

47694  49 
lemma 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

50 
assumes "simple_function M g" 
40875  51 
shows "finite (g ` space M)" and "g ` X \<inter> space M \<in> sets M" 
40871  52 
proof  
53 
show "finite (g ` space M)" 

54 
using assms unfolding simple_function_def by auto 

40875  55 
have "g ` X \<inter> space M = g ` (X \<inter> g`space M) \<inter> space M" by auto 
56 
also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g`{x} \<inter> space M)" by auto 

57 
finally show "g ` X \<inter> space M \<in> sets M" using assms 

50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

58 
by (auto simp del: UN_simps simp: simple_function_def) 
40871  59 
qed 
36624  60 

47694  61 
lemma simple_function_measurable2[intro]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

62 
assumes "simple_function M f" "simple_function M g" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

63 
shows "f ` A \<inter> g ` B \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

64 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

65 
have "f ` A \<inter> g ` B \<inter> space M = (f ` A \<inter> space M) \<inter> (g ` B \<inter> space M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

66 
by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

67 
then show ?thesis using assms[THEN simple_functionD(2)] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

68 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

69 

47694  70 
lemma simple_function_indicator_representation: 
43920  71 
fixes f ::"'a \<Rightarrow> ereal" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

72 
assumes f: "simple_function M f" and x: "x \<in> space M" 
38656  73 
shows "f x = (\<Sum>y \<in> f ` space M. y * indicator (f ` {y} \<inter> space M) x)" 
74 
(is "?l = ?r") 

75 
proof  

38705  76 
have "?r = (\<Sum>y \<in> f ` space M. 
38656  77 
(if y = f x then y * indicator (f ` {y} \<inter> space M) x else 0))" 
78 
by (auto intro!: setsum_cong2) 

79 
also have "... = f x * indicator (f ` {f x} \<inter> space M) x" 

80 
using assms by (auto dest: simple_functionD simp: setsum_delta) 

81 
also have "... = f x" using x by (auto simp: indicator_def) 

82 
finally show ?thesis by auto 

83 
qed 

36624  84 

47694  85 
lemma simple_function_notspace: 
43920  86 
"simple_function M (\<lambda>x. h x * indicator ( space M) x::ereal)" (is "simple_function M ?h") 
35692  87 
proof  
38656  88 
have "?h ` space M \<subseteq> {0}" unfolding indicator_def by auto 
89 
hence [simp, intro]: "finite (?h ` space M)" by (auto intro: finite_subset) 

90 
have "?h ` {0} \<inter> space M = space M" by auto 

91 
thus ?thesis unfolding simple_function_def by auto 

92 
qed 

93 

47694  94 
lemma simple_function_cong: 
38656  95 
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

96 
shows "simple_function M f \<longleftrightarrow> simple_function M g" 
38656  97 
proof  
98 
have "f ` space M = g ` space M" 

99 
"\<And>x. f ` {x} \<inter> space M = g ` {x} \<inter> space M" 

100 
using assms by (auto intro!: image_eqI) 

101 
thus ?thesis unfolding simple_function_def using assms by simp 

102 
qed 

103 

47694  104 
lemma simple_function_cong_algebra: 
41689
3e39b0e730d6
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 
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

106 
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

107 
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

108 

50003  109 
lemma borel_measurable_simple_function[measurable_dest]: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

110 
assumes "simple_function M f" 
38656  111 
shows "f \<in> borel_measurable M" 
112 
proof (rule borel_measurableI) 

113 
fix S 

114 
let ?I = "f ` (f ` S \<inter> space M)" 

115 
have *: "(\<Union>x\<in>?I. f ` {x} \<inter> space M) = f ` S \<inter> space M" (is "?U = _") by auto 

116 
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

117 
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

118 
using finite_subset[of "f ` (f ` S \<inter> space M)" "f ` space M"] by auto 
38656  119 
hence "?U \<in> sets M" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

120 
apply (rule sets.finite_UN) 
38656  121 
using assms unfolding simple_function_def by auto 
122 
thus "f ` S \<inter> space M \<in> sets M" unfolding * . 

35692  123 
qed 
124 

47694  125 
lemma simple_function_borel_measurable: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

126 
fixes f :: "'a \<Rightarrow> 'x::{t2_space}" 
38656  127 
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

128 
shows "simple_function M f" 
38656  129 
using assms unfolding simple_function_def 
130 
by (auto intro: borel_measurable_vimage) 

131 

47694  132 
lemma simple_function_eq_borel_measurable: 
43920  133 
fixes f :: "'a \<Rightarrow> ereal" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

134 
shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M" 
47694  135 
using simple_function_borel_measurable[of f] borel_measurable_simple_function[of M f] 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44666
diff
changeset

136 
by (fastforce simp: simple_function_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

137 

47694  138 
lemma 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

139 
"simple_function M (\<lambda>x. c)" 
38656  140 
by (auto intro: finite_subset simp: simple_function_def) 
47694  141 
lemma 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

142 
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

143 
shows "simple_function M (g \<circ> f)" 
38656  144 
unfolding simple_function_def 
145 
proof safe 

146 
show "finite ((g \<circ> f) ` space M)" 

147 
using assms unfolding simple_function_def by (auto simp: image_compose) 

148 
next 

149 
fix x assume "x \<in> space M" 

150 
let ?G = "g ` {g (f x)} \<inter> (f`space M)" 

151 
have *: "(g \<circ> f) ` {(g \<circ> f) x} \<inter> space M = 

152 
(\<Union>x\<in>?G. f ` {x} \<inter> space M)" by auto 

153 
show "(g \<circ> f) ` {(g \<circ> f) x} \<inter> space M \<in> sets M" 

154 
using assms unfolding simple_function_def * 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

155 
by (rule_tac sets.finite_UN) auto 
38656  156 
qed 
157 

47694  158 
lemma simple_function_indicator[intro, simp]: 
38656  159 
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

160 
shows "simple_function M (indicator A)" 
35692  161 
proof  
38656  162 
have "indicator A ` space M \<subseteq> {0, 1}" (is "?S \<subseteq> _") 
163 
by (auto simp: indicator_def) 

164 
hence "finite ?S" by (rule finite_subset) simp 

165 
moreover have " A \<inter> space M = space M  A" by auto 

166 
ultimately show ?thesis unfolding simple_function_def 

46905  167 
using assms by (auto simp: indicator_def [abs_def]) 
35692  168 
qed 
169 

47694  170 
lemma 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

171 
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

172 
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

173 
shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p") 
38656  174 
unfolding simple_function_def 
175 
proof safe 

176 
show "finite (?p ` space M)" 

177 
using assms unfolding simple_function_def 

178 
by (rule_tac finite_subset[of _ "f`space M \<times> g`space M"]) auto 

179 
next 

180 
fix x assume "x \<in> space M" 

181 
have "(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M = 

182 
(f ` {f x} \<inter> space M) \<inter> (g ` {g x} \<inter> space M)" 

183 
by auto 

184 
with `x \<in> space M` show "(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M \<in> sets M" 

185 
using assms unfolding simple_function_def by auto 

186 
qed 

35692  187 

47694  188 
lemma 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

189 
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

190 
shows "simple_function M (\<lambda>x. g (f x))" 
38656  191 
using simple_function_compose[OF assms, of g] 
192 
by (simp add: comp_def) 

35582  193 

47694  194 
lemma 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

195 
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

196 
shows "simple_function M (\<lambda>x. h (f x) (g x))" 
38656  197 
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

198 
have "simple_function M ((\<lambda>(x, y). h x y) \<circ> (\<lambda>x. (f x, g x)))" 
38656  199 
using assms by auto 
200 
thus ?thesis by (simp_all add: comp_def) 

201 
qed 

35582  202 

47694  203 
lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] 
38656  204 
and simple_function_diff[intro, simp] = simple_function_compose2[where h="op "] 
205 
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] 

206 
and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"] 

207 
and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"] 

208 
and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"] 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

209 
and simple_function_max[intro, simp] = simple_function_compose2[where h=max] 
38656  210 

47694  211 
lemma 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

212 
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

213 
shows "simple_function M (\<lambda>x. \<Sum>i\<in>P. f i x)" 
38656  214 
proof cases 
215 
assume "finite P" from this assms show ?thesis by induct auto 

216 
qed auto 

35582  217 

47694  218 
lemma 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

219 
fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f" 
43920  220 
shows simple_function_ereal[intro, simp]: "simple_function M (\<lambda>x. ereal (f x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

221 
by (auto intro!: simple_function_compose1[OF sf]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

222 

47694  223 
lemma 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

224 
fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

225 
shows simple_function_real_of_nat[intro, simp]: "simple_function M (\<lambda>x. real (f x))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

226 
by (auto intro!: simple_function_compose1[OF sf]) 
35582  227 

47694  228 
lemma borel_measurable_implies_simple_function_sequence: 
43920  229 
fixes u :: "'a \<Rightarrow> ereal" 
38656  230 
assumes u: "u \<in> borel_measurable M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

231 
shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

232 
(\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)" 
35582  233 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

234 
def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

235 
{ fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

236 
proof (split split_if, intro conjI impI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

237 
assume "\<not> real j \<le> u x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

238 
then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

239 
by (cases "u x") (auto intro!: natfloor_mono simp: mult_nonneg_nonneg) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

240 
moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

241 
by (intro real_natfloor_le) (auto simp: mult_nonneg_nonneg) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

242 
ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

243 
unfolding real_of_nat_le_iff by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

244 
qed auto } 
38656  245 
note f_upper = this 
35582  246 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

247 
have real_f: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

248 
"\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

249 
unfolding f_def by auto 
35582  250 

46731  251 
let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

252 
show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

253 
proof (intro exI[of _ ?g] conjI allI ballI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

254 
fix i 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

255 
have "simple_function M (\<lambda>x. real (f x i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

256 
proof (intro simple_function_borel_measurable) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

257 
show "(\<lambda>x. real (f x i)) \<in> borel_measurable M" 
50021
d96a3f468203
add support for function application to measurability prover
hoelzl
parents:
50003
diff
changeset

258 
using u by (auto simp: real_f) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

259 
have "(\<lambda>x. real (f x i))`space M \<subseteq> real`{..i*2^i}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

260 
using f_upper[of _ i] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

261 
then show "finite ((\<lambda>x. real (f x i))`space M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

262 
by (rule finite_subset) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

263 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

264 
then show "simple_function M (?g i)" 
43920  265 
by (auto intro: simple_function_ereal simple_function_div) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

266 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

267 
show "incseq ?g" 
43920  268 
proof (intro incseq_ereal incseq_SucI le_funI) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

269 
fix x and i :: nat 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

270 
have "f x i * 2 \<le> f x (Suc i)" unfolding f_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

271 
proof ((split split_if)+, intro conjI impI) 
43920  272 
assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

273 
then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

274 
by (cases "u x") (auto intro!: le_natfloor) 
38656  275 
next 
43920  276 
assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

277 
then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

278 
by (cases "u x") auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

279 
next 
43920  280 
assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

281 
have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

282 
by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

283 
also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

284 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

285 
assume "0 \<le> u x" then show ?thesis 
46671  286 
by (intro le_mult_natfloor) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

287 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

288 
assume "\<not> 0 \<le> u x" then show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

289 
by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg) 
38656  290 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

291 
also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

292 
by (simp add: ac_simps) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

293 
finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

294 
qed simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

295 
then show "?g i x \<le> ?g (Suc i) x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

296 
by (auto simp: field_simps) 
35582  297 
qed 
38656  298 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

299 
fix x show "(SUP i. ?g i x) = max 0 (u x)" 
51000  300 
proof (rule SUP_eqI) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

301 
fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

302 
by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

303 
mult_nonpos_nonneg mult_nonneg_nonneg) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

304 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

305 
fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

306 
have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

307 
from order_trans[OF this *] have "0 \<le> y" by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

308 
show "max 0 (u x) \<le> y" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

309 
proof (cases y) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

310 
case (real r) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

311 
with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq) 
44666  312 
from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le) 
43920  313 
then have "\<exists>p. max 0 (u x) = ereal p \<and> 0 \<le> p" by (cases "u x") (auto simp: max_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

314 
then guess p .. note ux = this 
44666  315 
obtain m :: nat where m: "p < real m" using reals_Archimedean2 .. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

316 
have "p \<le> r" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

317 
proof (rule ccontr) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

318 
assume "\<not> p \<le> r" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

319 
with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p  r"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

320 
obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n  1" by (auto simp: inverse_eq_divide field_simps) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

321 
then have "r * 2^max N m < p * 2^max N m  1" by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

322 
moreover 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

323 
have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

324 
using *[of "max N m"] m unfolding real_f using ux 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

325 
by (cases "0 \<le> u x") (simp_all add: max_def mult_nonneg_nonneg split: split_if_asm) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

326 
then have "p * 2 ^ max N m  1 < r * 2 ^ max N m" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

327 
by (metis real_natfloor_gt_diff_one less_le_trans) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

328 
ultimately show False by auto 
38656  329 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

330 
then show "max 0 (u x) \<le> y" using real ux by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

331 
qed (insert `0 \<le> y`, auto) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

332 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

333 
qed (auto simp: divide_nonneg_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

334 
qed 
35582  335 

47694  336 
lemma borel_measurable_implies_simple_function_sequence': 
43920  337 
fixes u :: "'a \<Rightarrow> ereal" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

338 
assumes u: "u \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

339 
obtains f where "\<And>i. simple_function M (f i)" "incseq f" "\<And>i. \<infinity> \<notin> range (f i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

340 
"\<And>x. (SUP i. f i x) = max 0 (u x)" "\<And>i x. 0 \<le> f i x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

341 
using borel_measurable_implies_simple_function_sequence[OF u] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

342 

49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

343 
lemma simple_function_induct[consumes 1, case_names cong set mult add, induct set: simple_function]: 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

344 
fixes u :: "'a \<Rightarrow> ereal" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

345 
assumes u: "simple_function M u" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

346 
assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

347 
assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

348 
assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

349 
assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

350 
shows "P u" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

351 
proof (rule cong) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

352 
from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x) = u x" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

353 
proof eventually_elim 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

354 
fix x assume x: "x \<in> space M" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

355 
from simple_function_indicator_representation[OF u x] 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

356 
show "(\<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x) = u x" .. 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

357 
qed 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

358 
next 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

359 
from u have "finite (u ` space M)" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

360 
unfolding simple_function_def by auto 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

361 
then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x)" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

362 
proof induct 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

363 
case empty show ?case 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

364 
using set[of "{}"] by (simp add: indicator_def[abs_def]) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

365 
qed (auto intro!: add mult set simple_functionD u) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

366 
next 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

367 
show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x))" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

368 
apply (subst simple_function_cong) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

369 
apply (rule simple_function_indicator_representation[symmetric]) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

370 
apply (auto intro: u) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

371 
done 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

372 
qed fact 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

373 

182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

374 
lemma simple_function_induct_nn[consumes 2, case_names cong set mult add]: 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

375 
fixes u :: "'a \<Rightarrow> ereal" 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

376 
assumes u: "simple_function M u" and nn: "\<And>x. 0 \<le> u x" 
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

377 
assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

378 
assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" 
49797
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

379 
assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" 
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

380 
assumes add: "\<And>u v. simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> simple_function M v \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

381 
shows "P u" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

382 
proof  
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

383 
show ?thesis 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

384 
proof (rule cong) 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

385 
fix x assume x: "x \<in> space M" 
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

386 
from simple_function_indicator_representation[OF u x] 
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

387 
show "(\<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x) = u x" .. 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

388 
next 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

389 
show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x))" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

390 
apply (subst simple_function_cong) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

391 
apply (rule simple_function_indicator_representation[symmetric]) 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

392 
apply (auto intro: u) 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

393 
done 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

394 
next 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

395 
from u nn have "finite (u ` space M)" "\<And>x. x \<in> u ` space M \<Longrightarrow> 0 \<le> x" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

396 
unfolding simple_function_def by auto 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

397 
then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u ` {y} \<inter> space M) x)" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

398 
proof induct 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

399 
case empty show ?case 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

400 
using set[of "{}"] by (simp add: indicator_def[abs_def]) 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

401 
qed (auto intro!: add mult set simple_functionD u setsum_nonneg 
49797
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

402 
simple_function_setsum) 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

403 
qed fact 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

404 
qed 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

405 

182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

406 
lemma borel_measurable_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]: 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

407 
fixes u :: "'a \<Rightarrow> ereal" 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

408 
assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x" 
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

409 
assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

410 
assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" 
49797
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

411 
assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" 
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

412 
assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" 
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

413 
assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P (SUP i. U i)" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

414 
shows "P u" 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

415 
using u 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

416 
proof (induct rule: borel_measurable_implies_simple_function_sequence') 
49797
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

417 
fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

418 
sup: "\<And>x. (SUP i. U i x) = max 0 (u x)" and nn: "\<And>i x. 0 \<le> U i x" 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

419 
have u_eq: "u = (SUP i. U i)" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

420 
using nn u sup by (auto simp: max_def) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

421 

49797
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

422 
from U have "\<And>i. U i \<in> borel_measurable M" 
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

423 
by (simp add: borel_measurable_simple_function) 
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

424 

49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

425 
show "P u" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

426 
unfolding u_eq 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

427 
proof (rule seq) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

428 
fix i show "P (U i)" 
49799
15ea98537c76
strong nonnegativ (instead of ae nn) for induction rule
hoelzl
parents:
49798
diff
changeset

429 
using `simple_function M (U i)` nn 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

430 
by (induct rule: simple_function_induct_nn) 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

431 
(auto intro: set mult add cong dest!: borel_measurable_simple_function) 
49797
28066863284c
add induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49796
diff
changeset

432 
qed fact+ 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

433 
qed 
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

434 

47694  435 
lemma simple_function_If_set: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

436 
assumes sf: "simple_function M f" "simple_function M g" and A: "A \<inter> space M \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

437 
shows "simple_function M (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function M ?IF") 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

438 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

439 
def F \<equiv> "\<lambda>x. f ` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g ` {x} \<inter> space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

440 
show ?thesis unfolding simple_function_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

441 
proof safe 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

442 
have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

443 
from finite_subset[OF this] assms 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

444 
show "finite (?IF ` space M)" unfolding simple_function_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

445 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

446 
fix x assume "x \<in> space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

447 
then have *: "?IF ` {?IF x} \<inter> space M = (if x \<in> A 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

448 
then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x)  (G (f x) \<inter> (A \<inter> space M)))) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

449 
else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x)  (G (g x) \<inter> (A \<inter> space M)))))" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

450 
using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

451 
have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

452 
unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

453 
show "?IF ` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto 
35582  454 
qed 
455 
qed 

456 

47694  457 
lemma simple_function_If: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

458 
assumes sf: "simple_function M f" "simple_function M g" and P: "{x\<in>space M. P x} \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

459 
shows "simple_function M (\<lambda>x. if P x then f x else g x)" 
35582  460 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

461 
have "{x\<in>space M. P x} = {x. P x} \<inter> space M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

462 
with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp 
38656  463 
qed 
464 

47694  465 
lemma 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

466 
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

467 
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

468 
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

469 
using assms unfolding simple_function_def by auto 
39092  470 

47694  471 
lemma simple_function_comp: 
472 
assumes T: "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

473 
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

474 
shows "simple_function M (\<lambda>x. f (T x))" 
41661  475 
proof (intro simple_function_def[THEN iffD2] conjI ballI) 
476 
have "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space M'" 

477 
using T unfolding measurable_def by auto 

478 
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

479 
using f unfolding simple_function_def by (auto intro: finite_subset) 
41661  480 
fix i assume i: "i \<in> (\<lambda>x. f (T x)) ` space M" 
481 
then have "i \<in> f ` space M'" 

482 
using T unfolding measurable_def by auto 

483 
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

484 
using f unfolding simple_function_def by auto 
41661  485 
then have "T ` (f ` {i} \<inter> space M') \<inter> space M \<in> sets M" 
486 
using T unfolding measurable_def by auto 

487 
also have "T ` (f ` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) ` {i} \<inter> space M" 

488 
using T unfolding measurable_def by auto 

489 
finally show "(\<lambda>x. f (T x)) ` {i} \<inter> space M \<in> sets M" . 

40859  490 
qed 
491 

38656  492 
section "Simple integral" 
493 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

494 
definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>S") where 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

495 
"integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f ` {x} \<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

496 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

497 
syntax 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

498 
"_simple_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

499 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

500 
translations 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

501 
"\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)" 
35582  502 

47694  503 
lemma simple_integral_cong: 
38656  504 
assumes "\<And>t. t \<in> space M \<Longrightarrow> f t = g t" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

505 
shows "integral\<^sup>S M f = integral\<^sup>S M g" 
38656  506 
proof  
507 
have "f ` space M = g ` space M" 

508 
"\<And>x. f ` {x} \<inter> space M = g ` {x} \<inter> space M" 

509 
using assms by (auto intro!: image_eqI) 

510 
thus ?thesis unfolding simple_integral_def by simp 

511 
qed 

512 

47694  513 
lemma simple_integral_const[simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

514 
"(\<integral>\<^sup>Sx. c \<partial>M) = c * (emeasure M) (space M)" 
38656  515 
proof (cases "space M = {}") 
516 
case True thus ?thesis unfolding simple_integral_def by simp 

517 
next 

518 
case False hence "(\<lambda>x. c) ` space M = {c}" by auto 

519 
thus ?thesis unfolding simple_integral_def by simp 

35582  520 
qed 
521 

47694  522 
lemma simple_function_partition: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

523 
assumes f: "simple_function M f" and g: "simple_function M g" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

524 
shows "integral\<^sup>S M f = (\<Sum>A\<in>(\<lambda>x. f ` {f x} \<inter> g ` {g x} \<inter> space M) ` space M. the_elem (f`A) * (emeasure M) A)" 
38656  525 
(is "_ = setsum _ (?p ` space M)") 
526 
proof 

46731  527 
let ?sub = "\<lambda>x. ?p ` (f ` {x} \<inter> space M)" 
38656  528 
let ?SIGMA = "Sigma (f`space M) ?sub" 
35582  529 

38656  530 
have [intro]: 
531 
"finite (f ` space M)" 

532 
"finite (g ` space M)" 

533 
using assms unfolding simple_function_def by simp_all 

534 

535 
{ fix A 

536 
have "?p ` (A \<inter> space M) \<subseteq> 

537 
(\<lambda>(x,y). f ` {x} \<inter> g ` {y} \<inter> space M) ` (f`space M \<times> g`space M)" 

538 
by auto 

539 
hence "finite (?p ` (A \<inter> space M))" 

40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
39910
diff
changeset

540 
by (rule finite_subset) auto } 
38656  541 
note this[intro, simp] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

542 
note sets = simple_function_measurable2[OF f g] 
35582  543 

38656  544 
{ fix x assume "x \<in> space M" 
545 
have "\<Union>(?sub (f x)) = (f ` {f x} \<inter> space M)" by auto 

47694  546 
with sets have "(emeasure M) (f ` {f x} \<inter> space M) = setsum (emeasure M) (?sub (f x))" 
47761  547 
by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) } 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

548 
hence "integral\<^sup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * (emeasure M) A)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

549 
unfolding simple_integral_def using f sets 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

550 
by (subst setsum_Sigma[symmetric]) 
43920  551 
(auto intro!: setsum_cong setsum_ereal_right_distrib) 
47694  552 
also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * (emeasure M) A)" 
38656  553 
proof  
554 
have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI) 

39910  555 
have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M 
38656  556 
= (\<lambda>x. (f x, ?p x)) ` space M" 
557 
proof safe 

558 
fix x assume "x \<in> space M" 

39910  559 
thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M" 
38656  560 
by (auto intro!: image_eqI[of _ _ "?p x"]) 
561 
qed auto 

562 
thus ?thesis 

39910  563 
apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI) 
38656  564 
apply (rule_tac x="xa" in image_eqI) 
565 
by simp_all 

566 
qed 

567 
finally show ?thesis . 

35582  568 
qed 
569 

47694  570 
lemma simple_integral_add[simp]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

571 
assumes f: "simple_function M f" and "\<And>x. 0 \<le> f x" and g: "simple_function M g" and "\<And>x. 0 \<le> g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

572 
shows "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = integral\<^sup>S M f + integral\<^sup>S M g" 
35582  573 
proof  
38656  574 
{ fix x let ?S = "g ` {g x} \<inter> f ` {f x} \<inter> space M" 
575 
assume "x \<in> space M" 

576 
hence "(\<lambda>a. f a + g a) ` ?S = {f x + g x}" "f ` ?S = {f x}" "g ` ?S = {g x}" 

577 
"(\<lambda>x. (f x, g x)) ` {(f x, g x)} \<inter> space M = ?S" 

578 
by auto } 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

579 
with assms show ?thesis 
38656  580 
unfolding 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

581 
simple_function_partition[OF simple_function_add[OF f g] simple_function_Pair[OF f g]] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

582 
simple_function_partition[OF f g] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

583 
simple_function_partition[OF g f] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

584 
by (subst (3) Int_commute) 
43920  585 
(auto simp add: ereal_left_distrib setsum_addf[symmetric] intro!: setsum_cong) 
35582  586 
qed 
587 

47694  588 
lemma simple_integral_setsum[simp]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

589 
assumes "\<And>i x. i \<in> P \<Longrightarrow> 0 \<le> f i 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

590 
assumes "\<And>i. i \<in> P \<Longrightarrow> simple_function M (f i)" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

591 
shows "(\<integral>\<^sup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>S M (f i))" 
38656  592 
proof cases 
593 
assume "finite P" 

594 
from this assms show ?thesis 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

595 
by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg) 
38656  596 
qed auto 
597 

47694  598 
lemma simple_integral_mult[simp]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

599 
assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

600 
shows "(\<integral>\<^sup>Sx. c * f x \<partial>M) = c * integral\<^sup>S M f" 
38656  601 
proof  
47694  602 
note mult = simple_function_mult[OF simple_function_const[of _ c] f(1)] 
38656  603 
{ fix x let ?S = "f ` {f x} \<inter> (\<lambda>x. c * f x) ` {c * f x} \<inter> space M" 
604 
assume "x \<in> space M" 

605 
hence "(\<lambda>x. c * f x) ` ?S = {c * f x}" "f ` ?S = {f x}" 

606 
by auto } 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

607 
with assms show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

608 
unfolding simple_function_partition[OF mult f(1)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

609 
simple_function_partition[OF f(1) mult] 
43920  610 
by (subst setsum_ereal_right_distrib) 
611 
(auto intro!: ereal_0_le_mult setsum_cong simp: mult_assoc) 

40871  612 
qed 
613 

47694  614 
lemma simple_integral_mono_AE: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

615 
assumes f: "simple_function M f" and g: "simple_function M g" 
47694  616 
and mono: "AE x in M. f x \<le> g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

617 
shows "integral\<^sup>S M f \<le> integral\<^sup>S M g" 
40859  618 
proof  
46731  619 
let ?S = "\<lambda>x. (g ` {g x} \<inter> space M) \<inter> (f ` {f x} \<inter> space M)" 
40859  620 
have *: "\<And>x. g ` {g x} \<inter> f ` {f x} \<inter> space M = ?S x" 
621 
"\<And>x. f ` {f x} \<inter> g ` {g x} \<inter> space M = ?S x" by auto 

622 
show ?thesis 

623 
unfolding * 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

624 
simple_function_partition[OF f g] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

625 
simple_function_partition[OF g f] 
40859  626 
proof (safe intro!: setsum_mono) 
627 
fix x assume "x \<in> space M" 

628 
then have *: "f ` ?S x = {f x}" "g ` ?S x = {g x}" by auto 

47694  629 
show "the_elem (f`?S x) * (emeasure M) (?S x) \<le> the_elem (g`?S x) * (emeasure M) (?S x)" 
40859  630 
proof (cases "f x \<le> g x") 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

631 
case True then show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

632 
using * assms(1,2)[THEN simple_functionD(2)] 
43920  633 
by (auto intro!: ereal_mult_right_mono) 
40859  634 
next 
635 
case False 

47694  636 
obtain N where N: "{x\<in>space M. \<not> f x \<le> g x} \<subseteq> N" "N \<in> sets M" "(emeasure M) N = 0" 
40859  637 
using mono by (auto elim!: AE_E) 
638 
have "?S x \<subseteq> N" using N `x \<in> space M` False by auto 

40871  639 
moreover have "?S x \<in> sets M" using assms 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

640 
by (rule_tac sets.Int) (auto intro!: simple_functionD) 
47694  641 
ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N" 
642 
using `N \<in> sets M` by (auto intro!: emeasure_mono) 

643 
moreover have "0 \<le> (emeasure M) (?S x)" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

644 
using assms(1,2)[THEN simple_functionD(2)] by auto 
47694  645 
ultimately have "(emeasure M) (?S x) = 0" using `(emeasure M) N = 0` by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

646 
then show ?thesis by simp 
40859  647 
qed 
648 
qed 

649 
qed 

650 

47694  651 
lemma 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

652 
assumes "simple_function M f" and "simple_function M g" 
38656  653 
and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

654 
shows "integral\<^sup>S M f \<le> integral\<^sup>S M g" 
41705  655 
using assms by (intro simple_integral_mono_AE) auto 
35582  656 

47694  657 
lemma simple_integral_cong_AE: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

658 
assumes "simple_function M f" and "simple_function M g" 
47694  659 
and "AE x in M. f x = g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

660 
shows "integral\<^sup>S M f = integral\<^sup>S M g" 
40859  661 
using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) 
662 

47694  663 
lemma 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

664 
assumes sf: "simple_function M f" "simple_function M g" 
47694  665 
and mea: "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

666 
shows "integral\<^sup>S M f = integral\<^sup>S M g" 
40859  667 
proof (intro simple_integral_cong_AE sf AE_I) 
47694  668 
show "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" by fact 
40859  669 
show "{x \<in> space M. f x \<noteq> g x} \<in> sets M" 
670 
using sf[THEN borel_measurable_simple_function] by auto 

671 
qed simp 

672 

47694  673 
lemma simple_integral_indicator: 
38656  674 
assumes "A \<in> sets M" 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

675 
assumes f: "simple_function M f" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

676 
shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = 
47694  677 
(\<Sum>x \<in> f ` space M. x * (emeasure M) (f ` {x} \<inter> space M \<inter> A))" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

678 
proof (cases "A = space M") 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

679 
case True 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

680 
then have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f" 
38656  681 
by (auto intro!: simple_integral_cong) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

682 
with True show ?thesis by (simp add: simple_integral_def) 
38656  683 
next 
684 
assume "A \<noteq> space M" 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

685 
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto 
38656  686 
have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _") 
35582  687 
proof safe 
38656  688 
fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto 
689 
next 

690 
fix y assume "y \<in> A" thus "f y \<in> ?I ` space M" 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

691 
using sets.sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) 
38656  692 
next 
693 
show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) 

35582  694 
qed 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

695 
have *: "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = 
47694  696 
(\<Sum>x \<in> f ` space M \<union> {0}. x * (emeasure M) (f ` {x} \<inter> space M \<inter> A))" 
38656  697 
unfolding simple_integral_def I 
698 
proof (rule setsum_mono_zero_cong_left) 

699 
show "finite (f ` space M \<union> {0})" 

700 
using assms(2) unfolding simple_function_def by auto 

701 
show "f ` A \<union> {0} \<subseteq> f`space M \<union> {0}" 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

702 
using sets.sets_into_space[OF assms(1)] by auto 
40859  703 
have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f ` {f x} \<inter> space M \<inter> A = {}" 
704 
by (auto simp: image_iff) 

38656  705 
thus "\<forall>i\<in>f ` space M \<union> {0}  (f ` A \<union> {0}). 
47694  706 
i * (emeasure M) (f ` {i} \<inter> space M \<inter> A) = 0" by auto 
38656  707 
next 
708 
fix x assume "x \<in> f`A \<union> {0}" 

709 
hence "x \<noteq> 0 \<Longrightarrow> ?I ` {x} \<inter> space M = f ` {x} \<inter> space M \<inter> A" 

710 
by (auto simp: indicator_def split: split_if_asm) 

47694  711 
thus "x * (emeasure M) (?I ` {x} \<inter> space M) = 
712 
x * (emeasure M) (f ` {x} \<inter> space M \<inter> A)" by (cases "x = 0") simp_all 

38656  713 
qed 
714 
show ?thesis unfolding * 

715 
using assms(2) unfolding simple_function_def 

716 
by (auto intro!: setsum_mono_zero_cong_right) 

717 
qed 

35582  718 

47694  719 
lemma simple_integral_indicator_only[simp]: 
38656  720 
assumes "A \<in> sets M" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

721 
shows "integral\<^sup>S M (indicator A) = emeasure M A" 
38656  722 
proof cases 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

723 
assume "space M = {}" hence "A = {}" using sets.sets_into_space[OF assms] by auto 
38656  724 
thus ?thesis unfolding simple_integral_def using `space M = {}` by auto 
725 
next 

43920  726 
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto 
38656  727 
thus ?thesis 
47694  728 
using simple_integral_indicator[OF assms simple_function_const[of _ 1]] 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

729 
using sets.sets_into_space[OF assms] 
47694  730 
by (auto intro!: arg_cong[where f="(emeasure M)"]) 
38656  731 
qed 
35582  732 

47694  733 
lemma simple_integral_null_set: 
734 
assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets M" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

735 
shows "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = 0" 
38656  736 
proof  
47694  737 
have "AE x in M. indicator N x = (0 :: ereal)" 
738 
using `N \<in> null_sets M` by (auto simp: indicator_def intro!: AE_I[of _ _ N]) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

739 
then have "(\<integral>\<^sup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^sup>Sx. 0 \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

740 
using assms apply (intro simple_integral_cong_AE) by auto 
40859  741 
then show ?thesis by simp 
38656  742 
qed 
35582  743 

47694  744 
lemma simple_integral_cong_AE_mult_indicator: 
745 
assumes sf: "simple_function M f" and eq: "AE x in M. x \<in> S" and "S \<in> sets M" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

746 
shows "integral\<^sup>S M f = (\<integral>\<^sup>Sx. f x * indicator S x \<partial>M)" 
41705  747 
using assms by (intro simple_integral_cong_AE) auto 
35582  748 

47694  749 
lemma simple_integral_cmult_indicator: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

750 
assumes A: "A \<in> sets M" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

751 
shows "(\<integral>\<^sup>Sx. c * indicator A x \<partial>M) = c * (emeasure M) A" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

752 
using simple_integral_mult[OF simple_function_indicator[OF A]] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

753 
unfolding simple_integral_indicator_only[OF A] by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

754 

47694  755 
lemma simple_integral_positive: 
756 
assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

757 
shows "0 \<le> integral\<^sup>S M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

758 
proof  
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

759 
have "integral\<^sup>S M (\<lambda>x. 0) \<le> integral\<^sup>S M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

760 
using simple_integral_mono_AE[OF _ f ae] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

761 
then show ?thesis by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

762 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

763 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

764 
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

765 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

766 
definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

767 
"integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)" 
35692  768 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

769 
syntax 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

770 
"_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^sup>+ _. _ \<partial>_" [60,61] 110) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

771 

3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

772 
translations 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

773 
"\<integral>\<^sup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)" 
40872  774 

47694  775 
lemma positive_integral_positive: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

776 
"0 \<le> integral\<^sup>P M f" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

777 
by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def) 
40873  778 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

779 
lemma positive_integral_not_MInfty[simp]: "integral\<^sup>P M f \<noteq> \<infinity>" 
47694  780 
using positive_integral_positive[of M f] by auto 
781 

782 
lemma positive_integral_def_finite: 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

783 
"integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

784 
(is "_ = SUPR ?A ?f") 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

785 
unfolding positive_integral_def 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

786 
proof (safe intro!: antisym SUP_least) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

787 
fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

788 
let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

789 
note gM = g(1)[THEN borel_measurable_simple_function] 
50252  790 
have \<mu>_G_pos: "0 \<le> (emeasure M) ?G" using gM by auto 
46731  791 
let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

792 
from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

793 
apply (safe intro!: simple_function_max simple_function_If) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

794 
apply (force simp: max_def le_fun_def split: split_if_asm)+ 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

795 
done 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

796 
show "integral\<^sup>S M g \<le> SUPR ?A ?f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

797 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

798 
have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto 
47694  799 
assume "(emeasure M) ?G = 0" 
800 
with gM have "AE x in M. x \<notin> ?G" 

801 
by (auto simp add: AE_iff_null intro!: null_setsI) 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

802 
with gM g show ?thesis 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

803 
by (intro SUP_upper2[OF g0] simple_integral_mono_AE) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

804 
(auto simp: max_def intro!: simple_function_If) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

805 
next 
50252  806 
assume \<mu>_G: "(emeasure M) ?G \<noteq> 0" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

807 
have "SUPR ?A (integral\<^sup>S M) = \<infinity>" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

808 
proof (intro SUP_PInfty) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

809 
fix n :: nat 
47694  810 
let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)" 
50252  811 
have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>_G \<mu>_G_pos by (auto simp: ereal_divide_eq) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

812 
then have "?g ?y \<in> ?A" by (rule g_in_A) 
47694  813 
have "real n \<le> ?y * (emeasure M) ?G" 
50252  814 
using \<mu>_G \<mu>_G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

815 
also have "\<dots> = (\<integral>\<^sup>Sx. ?y * indicator ?G x \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

816 
using `0 \<le> ?y` `?g ?y \<in> ?A` gM 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

817 
by (subst simple_integral_cmult_indicator) auto 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

818 
also have "\<dots> \<le> integral\<^sup>S M (?g ?y)" using `?g ?y \<in> ?A` gM 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

819 
by (intro simple_integral_mono) auto 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

820 
finally show "\<exists>i\<in>?A. real n \<le> integral\<^sup>S M i" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

821 
using `?g ?y \<in> ?A` by blast 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

822 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

823 
then show ?thesis by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

824 
qed 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

825 
qed (auto intro: SUP_upper) 
40873  826 

47694  827 
lemma positive_integral_mono_AE: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

828 
assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>P M u \<le> integral\<^sup>P M v" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

829 
unfolding positive_integral_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

830 
proof (safe intro!: SUP_mono) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

831 
fix n assume n: "simple_function M n" "n \<le> max 0 \<circ> u" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

832 
from ae[THEN AE_E] guess N . note N = this 
47694  833 
then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in) 
46731  834 
let ?n = "\<lambda>x. n x * indicator (space M  N) x" 
47694  835 
have "AE x in M. n x \<le> ?n x" "simple_function M ?n" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

836 
using n N ae_N by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

837 
moreover 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

838 
{ fix x have "?n x \<le> max 0 (v x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

839 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

840 
assume x: "x \<in> space M  N" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

841 
with N have "u x \<le> v x" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

842 
with n(2)[THEN le_funD, of x] x show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

843 
by (auto simp: max_def split: split_if_asm) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

844 
qed simp } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

845 
then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

846 
moreover have "integral\<^sup>S M n \<le> integral\<^sup>S M ?n" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

847 
using ae_N N n by (auto intro!: simple_integral_mono_AE) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

848 
ultimately show "\<exists>m\<in>{g. simple_function M g \<and> g \<le> max 0 \<circ> v}. integral\<^sup>S M n \<le> integral\<^sup>S M m" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

849 
by force 
38656  850 
qed 
851 

47694  852 
lemma positive_integral_mono: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

853 
"(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>P M u \<le> integral\<^sup>P M v" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

854 
by (auto intro: positive_integral_mono_AE) 
40859  855 

47694  856 
lemma positive_integral_cong_AE: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

857 
"AE x in M. u x = v x \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v" 
40859  858 
by (auto simp: eq_iff intro!: positive_integral_mono_AE) 
859 

47694  860 
lemma positive_integral_cong: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

861 
"(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>P M u = integral\<^sup>P M v" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

862 
by (auto intro: positive_integral_cong_AE) 
40859  863 

47694  864 
lemma positive_integral_eq_simple_integral: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

865 
assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

866 
proof  
46731  867 
let ?f = "\<lambda>x. f x * indicator (space M) x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

868 
have f': "simple_function M ?f" using f by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

869 
with f(2) have [simp]: "max 0 \<circ> ?f = ?f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

870 
by (auto simp: fun_eq_iff max_def split: split_indicator) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

871 
have "integral\<^sup>P M ?f \<le> integral\<^sup>S M ?f" using f' 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

872 
by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

873 
moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>P M ?f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

874 
unfolding positive_integral_def 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

875 
using f' by (auto intro!: SUP_upper) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

876 
ultimately show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

877 
by (simp cong: positive_integral_cong simple_integral_cong) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

878 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

879 

47694  880 
lemma positive_integral_eq_simple_integral_AE: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

881 
assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>P M f = integral\<^sup>S M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

882 
proof  
47694  883 
have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

884 
with f have "integral\<^sup>P M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

885 
by (simp cong: positive_integral_cong_AE simple_integral_cong_AE 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

886 
add: positive_integral_eq_simple_integral) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

887 
with assms show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

888 
by (auto intro!: simple_integral_cong_AE split: split_max) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

889 
qed 
40873  890 

47694  891 
lemma positive_integral_SUP_approx: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

892 
assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

893 
and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

894 
shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>P M (f i))" (is "_ \<le> ?S") 
43920  895 
proof (rule ereal_le_mult_one_interval) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

896 
have "0 \<le> (SUP i. integral\<^sup>P M (f i))" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

897 
using f(3) by (auto intro!: SUP_upper2 positive_integral_positive) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

898 
then show "(SUP i. integral\<^sup>P M (f i)) \<noteq> \<infinity>" by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

899 
have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

900 
using u(3) by auto 
43920  901 
fix a :: ereal assume "0 < a" "a < 1" 
38656  902 
hence "a \<noteq> 0" by auto 
46731  903 
let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}" 
38656  904 
have B: "\<And>i. ?B i \<in> sets M" 
50003  905 
using f `simple_function M u` by auto 
38656  906 

46731  907 
let ?uB = "\<lambda>i x. u x * indicator (?B i) x" 
38656  908 

909 
{ fix i have "?B i \<subseteq> ?B (Suc i)" 

910 
proof safe 

911 
fix i x assume "a * u x \<le> f i x" 

912 
also have "\<dots> \<le> f (Suc i) x" 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

913 
using `incseq f`[THEN incseq_SucD] unfolding le_fun_def by auto 
38656  914 
finally show "a * u x \<le> f (Suc i) x" . 
915 
qed } 

916 
note B_mono = this 

35582  917 

50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

918 
note B_u = sets.Int[OF u(1)[THEN simple_functionD(2)] B] 
38656  919 

46731  920 
let ?B' = "\<lambda>i n. (u ` {i} \<inter> space M) \<inter> ?B n" 
47694  921 
have measure_conv: "\<And>i. (emeasure M) (u ` {i} \<inter> space M) = (SUP n. (emeasure M) (?B' i n))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

922 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

923 
fix i 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

924 
have 1: "range (?B' i) \<subseteq> sets M" using B_u by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

925 
have 2: "incseq (?B' i)" using B_mono by (auto intro!: incseq_SucI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

926 
have "(\<Union>n. ?B' i n) = u ` {i} \<inter> space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

927 
proof safe 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

928 
fix x i assume x: "x \<in> space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

929 
show "x \<in> (\<Union>i. ?B' (u x) i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

930 
proof cases 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

931 
assume "u x = 0" thus ?thesis using `x \<in> space M` f(3) by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

932 
next 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

933 
assume "u x \<noteq> 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

934 
with `a < 1` u_range[OF `x \<in> space M`] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

935 
have "a * u x < 1 * u x" 
43920  936 
by (intro ereal_mult_strict_right_mono) (auto simp: image_iff) 
46884  937 
also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def) 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

938 
finally obtain i where "a * u x < f i x" unfolding SUP_def 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

939 
by (auto simp add: less_Sup_iff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

940 
hence "a * u x \<le> f i x" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

941 
thus ?thesis using `x \<in> space M` by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

942 
qed 
40859  943 
qed 
47694  944 
then show "?thesis i" using SUP_emeasure_incseq[OF 1 2] by simp 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

945 
qed 
38656  946 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

947 
have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB 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

948 
unfolding simple_integral_indicator[OF B `simple_function M u`] 
43920  949 
proof (subst SUPR_ereal_setsum, safe) 
38656  950 
fix x n assume "x \<in> space M" 
47694  951 
with u_range show "incseq (\<lambda>i. u x * (emeasure M) (?B' (u x) i))" "\<And>i. 0 \<le> u x * (emeasure M) (?B' (u x) i)" 
952 
using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff) 

38656  953 
next 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

954 
show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

955 
using measure_conv u_range B_u unfolding simple_integral_def 
43920  956 
by (auto intro!: setsum_cong SUPR_ereal_cmult[symmetric]) 
38656  957 
qed 
958 
moreover 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

959 
have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S" 
43920  960 
apply (subst SUPR_ereal_cmult[symmetric]) 
38705  961 
proof (safe intro!: SUP_mono bexI) 
38656  962 
fix i 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

963 
have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

964 
using B `simple_function M u` u_range 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

965 
by (subst simple_integral_mult) (auto split: split_indicator) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

966 
also have "\<dots> \<le> integral\<^sup>P M (f i)" 
38656  967 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

968 
have *: "simple_function M (\<lambda>x. a * ?uB i x)" using B `0 < a` u(1) by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

969 
show ?thesis using f(3) * u_range `0 < a` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

970 
by (subst positive_integral_eq_simple_integral[symmetric]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

971 
(auto intro!: positive_integral_mono split: split_indicator) 
38656  972 
qed 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

973 
finally show "a * integral\<^sup>S M (?uB i) \<le> integral\<^sup>P M (f i)" 
38656  974 
by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

975 
next 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

976 
fix i show "0 \<le> \<integral>\<^sup>S x. ?uB i x \<partial>M" using B `0 < a` u(1) u_range 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

977 
by (intro simple_integral_positive) (auto split: split_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

978 
qed (insert `0 < a`, auto) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

979 
ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp 
35582  980 
qed 
981 

47694  982 
lemma incseq_positive_integral: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

983 
assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>P M (f i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

984 
proof  
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

985 
have "\<And>i x. f i x \<le> f (Suc i) x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

986 
using assms by (auto dest!: incseq_SucD simp: le_fun_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

987 
then show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

988 
by (auto intro!: incseq_SucI positive_integral_mono) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

989 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

990 

35582  991 
text {* BeppoLevi monotone convergence theorem *} 
47694  992 
lemma positive_integral_monotone_convergence_SUP: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

993 
assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

994 
shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

995 
proof (rule antisym) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

996 
show "(SUP j. integral\<^sup>P M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

997 
by (auto intro!: SUP_least SUP_upper positive_integral_mono) 
38656  998 
next 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

999 
show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>P M (f j))" 
47694  1000 
unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"] 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

1001 
proof (safe intro!: SUP_least) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1002 
fix g assume g: "simple_function M g" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

1003 
and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}" 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

1004 
then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}" 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

1005 
using f by (auto intro!: SUP_upper2) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

1006 
with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1007 
by (intro positive_integral_SUP_approx[OF f g _ g']) 
46884  1008 
(auto simp: le_fun_def max_def) 
35582  1009 
qed 
1010 
qed 

1011 

47694  1012 
lemma positive_integral_monotone_convergence_SUP_AE: 
1013 
assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" "\<And>i. f i \<in> borel_measurable M" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1014 
shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))" 
40859  1015 
proof  
47694  1016 
from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x \<and> 0 \<le> f i x" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1017 
by (simp add: AE_all_countable) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1018 
from this[THEN AE_E] guess N . note N = this 
46731  1019 
let ?f = "\<lambda>i x. if x \<in> space M  N then f i x else 0" 
47694  1020 
have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N]) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1021 
then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1022 
by (auto intro!: positive_integral_cong_AE) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1023 
also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>M))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1024 
proof (rule positive_integral_monotone_convergence_SUP) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1025 
show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1026 
{ fix i show "(\<lambda>x. if x \<in> space M  N then f i x else 0) \<in> borel_measurable M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1027 
using f N(3) by (intro measurable_If_set) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1028 
fix x show "0 \<le> ?f i x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1029 
using N(1) by auto } 
40859  1030 
qed 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1031 
also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1032 
using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1033 
finally show ?thesis . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1034 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1035 

47694  1036 
lemma positive_integral_monotone_convergence_SUP_AE_incseq: 
1037 
assumes f: "incseq f" "\<And>i. AE x in M. 0 \<le> f i x" and borel: "\<And>i. f i \<in> borel_measurable M" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1038 
shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>P M (f i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1039 
using f[unfolded incseq_Suc_iff le_fun_def] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1040 
by (intro positive_integral_monotone_convergence_SUP_AE[OF _ borel]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1041 
auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1042 

47694  1043 
lemma positive_integral_monotone_convergence_simple: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1044 
assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1045 
shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1046 
using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1047 
f(3)[THEN borel_measurable_simple_function] f(2)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1048 
by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1049 

cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1050 
lemma positive_integral_max_0: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1051 
"(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1052 
by (simp add: le_fun_def positive_integral_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1053 

47694  1054 
lemma positive_integral_cong_pos: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1055 
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1056 
shows "integral\<^sup>P M f = integral\<^sup>P M g" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1057 
proof  
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1058 
have "integral\<^sup>P M (\<lambda>x. max 0 (f x)) = integral\<^sup>P M (\<lambda>x. max 0 (g x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1059 
proof (intro positive_integral_cong) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1060 
fix x assume "x \<in> space M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1061 
from assms[OF this] show "max 0 (f x) = max 0 (g x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1062 
by (auto split: split_max) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1063 
qed 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1064 
then show ?thesis by (simp add: positive_integral_max_0) 
40859  1065 
qed 
1066 

47694  1067 
lemma SUP_simple_integral_sequences: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1068 
assumes f: "incseq f" "\<And>i x. 0 \<le> f i x" "\<And>i. simple_function M (f i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1069 
and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)" 
47694  1070 
and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1071 
shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" 
38656  1072 
(is "SUPR _ ?F = SUPR _ ?G") 
1073 
proof  

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1074 
have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1075 
using f by (rule positive_integral_monotone_convergence_simple) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1076 
also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1077 
unfolding eq[THEN positive_integral_cong_AE] .. 
38656  1078 
also have "\<dots> = (SUP i. ?G i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1079 
using g by (rule positive_integral_monotone_convergence_simple[symmetric]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1080 
finally show ?thesis by simp 
38656  1081 
qed 
1082 

47694  1083 
lemma positive_integral_const[simp]: 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1084 
"0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)" 
38656  1085 
by (subst positive_integral_eq_simple_integral) auto 
1086 

47694  1087 
lemma positive_integral_linear: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1088 
assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1089 
and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1090 
shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>P M f + integral\<^sup>P M g" 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1091 
(is "integral\<^sup>P M ?L = _") 
35582  1092 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1093 
from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1094 
note u = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1095 
from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1096 
note v = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this 
46731  1097 
let ?L' = "\<lambda>i x. a * u i x + v i x" 
38656  1098 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1099 
have "?L \<in> borel_measurable M" using assms by auto 
38656  1100 
from borel_measurable_implies_simple_function_sequence'[OF this] guess l . 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1101 
note l = positive_integral_monotone_convergence_simple[OF this(2,5,1)] this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1102 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1103 
have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1104 
using u v `0 \<le> a` 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1105 
by (auto simp: incseq_Suc_iff le_fun_def 
43920  1106 
intro!: add_mono ereal_mult_left_mono simple_integral_mono) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1107 
have pos: "\<And>i. 0 \<le> integral\<^sup>S M (u i)" "\<And>i. 0 \<le> integral\<^sup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^sup>S M (u i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1108 
using u v `0 \<le> a` by (auto simp: simple_integral_positive) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1109 
{ fix i from pos[of i] have "a * integral\<^sup>S M (u i) \<noteq> \<infinity>" "integral\<^sup>S M (v i) \<noteq> \<infinity>" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1110 
by (auto split: split_if_asm) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1111 
note not_MInf = this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1112 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1113 
have l': "(SUP i. integral\<^sup>S M (l i)) = (SUP i. integral\<^sup>S M (?L' i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1114 
proof (rule SUP_simple_integral_sequences[OF l(3,6,2)]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1115 
show "incseq ?L'" "\<And>i x. 0 \<le> ?L' i x" "\<And>i. simple_function M (?L' i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1116 
using u v `0 \<le> a` unfolding incseq_Suc_iff le_fun_def 
43920  1117 
by (auto intro!: add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1118 
{ fix x 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1119 
{ fix i have "a * u i x \<noteq> \<infinity>" "v i x \<noteq> \<infinity>" "u i x \<noteq> \<infinity>" using `0 \<le> a` u(6)[of i x] v(6)[of i x] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1120 
by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1121 
then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1122 
using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x] 
43920  1123 
by (subst SUPR_ereal_cmult[symmetric, OF u(6) `0 \<le> a`]) 
1124 
(auto intro!: SUPR_ereal_add 

1125 
simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) } 

47694 