author  wenzelm 
Thu, 18 Apr 2013 17:07:01 +0200  
changeset 51717  9e7d1c139569 
parent 51340  5e6296afe08d 
child 53015  a1119cf551e8 
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 

47694  494 
definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^isup>S") where 
495 
"integral\<^isup>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 
47694  498 
"_simple_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^isup>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 
47694  501 
"\<integral>\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

505 
shows "integral\<^isup>S M f = integral\<^isup>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]: 
514 
"(\<integral>\<^isup>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" 
47694  524 
shows "integral\<^isup>S M f = (\<Sum>A\<in>(\<lambda>x. f ` {f x} \<inter> g ` {g x} \<inter> space M) ` space M. the_elem (f`A) * (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) } 
47694  548 
hence "integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

572 
shows "(\<integral>\<^isup>Sx. f x + g x \<partial>M) = integral\<^isup>S M f + integral\<^isup>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)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

591 
shows "(\<integral>\<^isup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

600 
shows "(\<integral>\<^isup>Sx. c * f x \<partial>M) = c * integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

617 
shows "integral\<^isup>S M f \<le> integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

654 
shows "integral\<^isup>S M f \<le> integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

660 
shows "integral\<^isup>S M f = integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

666 
shows "integral\<^isup>S M f = integral\<^isup>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" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

676 
shows "(\<integral>\<^isup>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))" 
38656  678 
proof cases 
679 
assume "A = space M" 

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

680 
moreover hence "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = integral\<^isup>S M f" 
38656  681 
by (auto intro!: simple_integral_cong) 
682 
moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto 

683 
ultimately show ?thesis by (simp add: simple_integral_def) 

684 
next 

685 
assume "A \<noteq> space M" 

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

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

691 
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

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

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

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

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

701 
using assms(2) unfolding simple_function_def by auto 

702 
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

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

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

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

711 
by (auto simp: indicator_def split: split_if_asm) 

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

38656  714 
qed 
715 
show ?thesis unfolding * 

716 
using assms(2) unfolding simple_function_def 

717 
by (auto intro!: setsum_mono_zero_cong_right) 

718 
qed 

35582  719 

47694  720 
lemma simple_integral_indicator_only[simp]: 
38656  721 
assumes "A \<in> sets M" 
47694  722 
shows "integral\<^isup>S M (indicator A) = emeasure M A" 
38656  723 
proof cases 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

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

43920  727 
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto 
38656  728 
thus ?thesis 
47694  729 
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

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

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

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

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

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

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

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

47694  745 
lemma simple_integral_cong_AE_mult_indicator: 
746 
assumes sf: "simple_function M f" and eq: "AE x in M. x \<in> S" and "S \<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

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

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

751 
assumes A: "A \<in> sets M" 
47694  752 
shows "(\<integral>\<^isup>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

753 
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

754 
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

755 

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

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

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

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

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

761 
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

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

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

764 

41689
3e39b0e730d6
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 
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

766 

47694  767 
definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^isup>P") where 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

770 
syntax 
47694  771 
"_positive_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> 'a measure \<Rightarrow> ereal" ("\<integral>\<^isup>+ _. _ \<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

772 

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

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

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

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

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

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

782 

783 
lemma positive_integral_def_finite: 

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

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

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

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

787 
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

788 
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

789 
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

790 
note gM = g(1)[THEN borel_measurable_simple_function] 
50252  791 
have \<mu>_G_pos: "0 \<le> (emeasure M) ?G" using gM by auto 
46731  792 
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

793 
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

794 
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

795 
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

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

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

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

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

802 
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

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

804 
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

805 
(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

806 
next 
50252  807 
assume \<mu>_G: "(emeasure M) ?G \<noteq> 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

810 
fix n :: nat 
47694  811 
let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)" 
50252  812 
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

813 
then have "?g ?y \<in> ?A" by (rule g_in_A) 
47694  814 
have "real n \<le> ?y * (emeasure M) ?G" 
50252  815 
using \<mu>_G \<mu>_G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

817 
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

818 
by (subst simple_integral_cmult_indicator) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

822 
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

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

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

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

826 
qed (auto intro: SUP_upper) 
40873  827 

47694  828 
lemma positive_integral_mono_AE: 
829 
assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^isup>P M u \<le> integral\<^isup>P M v" 

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

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

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

832 
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

833 
from ae[THEN AE_E] guess N . note N = this 
47694  834 
then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in) 
46731  835 
let ?n = "\<lambda>x. n x * indicator (space M  N) x" 
47694  836 
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

837 
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

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

839 
{ 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

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

841 
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

842 
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

843 
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

844 
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

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

846 
then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

848 
using ae_N N n by (auto intro!: simple_integral_mono_AE) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

850 
by force 
38656  851 
qed 
852 

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

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

855 
by (auto intro: positive_integral_mono_AE) 
40859  856 

47694  857 
lemma positive_integral_cong_AE: 
858 
"AE x in M. u x = v x \<Longrightarrow> integral\<^isup>P M u = integral\<^isup>P M v" 

40859  859 
by (auto simp: eq_iff intro!: positive_integral_mono_AE) 
860 

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

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

863 
by (auto intro: positive_integral_cong_AE) 
40859  864 

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

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

867 
proof  
46731  868 
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

869 
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

870 
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

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

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

873 
by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

876 
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

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

878 
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

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

880 

47694  881 
lemma positive_integral_eq_simple_integral_AE: 
882 
assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^isup>P M f = integral\<^isup>S M f" 

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

883 
proof  
47694  884 
have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

886 
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

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

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

889 
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

890 
qed 
40873  891 

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

893 
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

894 
and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

895 
shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S") 
43920  896 
proof (rule ereal_le_mult_one_interval) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

900 
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

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

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

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

911 
proof safe 

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

913 
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

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

917 
note B_mono = this 

35582  918 

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

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

46731  921 
let ?B' = "\<lambda>i n. (u ` {i} \<inter> space M) \<inter> ?B n" 
47694  922 
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

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

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

925 
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

926 
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

927 
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

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

929 
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

930 
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

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

932 
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

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

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

935 
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

936 
have "a * u x < 1 * u x" 
43920  937 
by (intro ereal_mult_strict_right_mono) (auto simp: image_iff) 
46884  938 
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

939 
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

940 
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

941 
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

942 
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

943 
qed 
40859  944 
qed 
47694  945 
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

946 
qed 
38656  947 

41689
3e39b0e730d6
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 
have "integral\<^isup>S M u = (SUP i. integral\<^isup>S M (?uB i))" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

949 
unfolding simple_integral_indicator[OF B `simple_function M u`] 
43920  950 
proof (subst SUPR_ereal_setsum, safe) 
38656  951 
fix x n assume "x \<in> space M" 
47694  952 
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)" 
953 
using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff) 

38656  954 
next 
47694  955 
show "integral\<^isup>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

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

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

960 
have "a * (SUP i. integral\<^isup>S M (?uB i)) \<le> ?S" 
43920  961 
apply (subst SUPR_ereal_cmult[symmetric]) 
38705  962 
proof (safe intro!: SUP_mono bexI) 
38656  963 
fix i 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

964 
have "a * integral\<^isup>S M (?uB i) = (\<integral>\<^isup>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

965 
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

966 
by (subst simple_integral_mult) (auto split: split_indicator) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

969 
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

970 
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

971 
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

972 
(auto intro!: positive_integral_mono split: split_indicator) 
38656  973 
qed 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

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

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

978 
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

979 
qed (insert `0 < a`, auto) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

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

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

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

986 
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

987 
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

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

989 
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

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

991 

35582  992 
text {* BeppoLevi monotone convergence theorem *} 
47694  993 
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

994 
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

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

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

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

998 
by (auto intro!: SUP_least SUP_upper positive_integral_mono) 
38656  999 
next 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1000 
show "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^isup>P M (f j))" 
47694  1001 
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

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

1003 
fix g assume g: "simple_function M g" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1004 
and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1005 
moreover 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

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

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

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

1012 

47694  1013 
lemma positive_integral_monotone_convergence_SUP_AE: 
1014 
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" 

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

1015 
shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))" 
40859  1016 
proof  
47694  1017 
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

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

1019 
from this[THEN AE_E] guess N . note N = this 
46731  1020 
let ?f = "\<lambda>i x. if x \<in> space M  N then f i x else 0" 
47694  1021 
have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

1025 
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

1026 
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

1027 
{ 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

1028 
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

1029 
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

1030 
using N(1) by auto } 
40859  1031 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1033 
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

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

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

1036 

47694  1037 
lemma positive_integral_monotone_convergence_SUP_AE_incseq: 
1038 
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" 

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

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

1040 
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

1041 
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

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

1043 

47694  1044 
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

1045 
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

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

1047 
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

1048 
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

1049 
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

1050 

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

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

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

1053 
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

1054 

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

1056 
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

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

1061 
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

1062 
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

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

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

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

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

1069 
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

1070 
and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)" 
47694  1071 
and eq: "AE x in M. (SUP i. f i x) = (SUP i. g 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

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

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

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

1076 
using f by (rule positive_integral_monotone_convergence_simple) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1078 
unfolding eq[THEN positive_integral_cong_AE] .. 
38656  1079 
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

1080 
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

1081 
finally show ?thesis by simp 
38656  1082 
qed 
1083 

47694  1084 
lemma positive_integral_const[simp]: 
1085 
"0 \<le> c \<Longrightarrow> (\<integral>\<^isup>+ x. c \<partial>M) = c * (emeasure M) (space M)" 

38656  1086 
by (subst positive_integral_eq_simple_integral) auto 
1087 

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

1089 
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

1090 
and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1091 
shows "(\<integral>\<^isup>+ x. a * f x + g x \<partial>M) = a * integral\<^isup>P M f + integral\<^isup>P M g" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

1094 
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

1095 
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

1096 
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

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

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

1100 
have "?L \<in> borel_measurable M" using assms by auto 
38656  1101 
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

1102 
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

1103 

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

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

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

1106 
by (auto simp: incseq_Suc_iff le_fun_def 
43920  1107 
intro!: add_mono ereal_mult_left_mono simple_integral_mono) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1109 
using u v `0 \<le> a` by (auto simp: simple_integral_positive) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

1113 

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

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

1115 
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

1116 
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

1117 
using u v `0 \<le> a` unfolding incseq_Suc_iff le_fun_def 
43920  1118 
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

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

1120 
{ 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

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

1122 
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

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

1126 
simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) } 

47694  1127 
then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1128 
unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2) 
43920  1129 
by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg) 
38656  1130 
qed 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1131 
also have "\<dots> = (SUP i. a * integral\<^isup>S M (u i) + integral\<^isup>S M (v i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1132 
using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: 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

1133 
finally have "(\<integral>\<^isup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^isup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^isup>+x. max 0 (g x) \<partial>M)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1134 
unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
