author  hoelzl 
Wed, 10 Oct 2012 12:12:17 +0200  
changeset 49775  970964690b3d 
parent 47761  dfe747e72fa8 
child 49795  9f2fb9b25a77 
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 

47694  12 
lemma ereal_minus_eq_PInfty_iff: 
13 
fixes x y :: ereal shows "x  y = \<infinity> \<longleftrightarrow> y = \<infinity> \<or> x = \<infinity>" 

14 
by (cases x y rule: ereal2_cases) simp_all 

15 

43920  16 
lemma real_ereal_1[simp]: "real (1::ereal) = 1" 
17 
unfolding one_ereal_def by simp 

42991
3fa22920bf86
integral strong monotone; finite subadditivity for measure
hoelzl
parents:
42950
diff
changeset

18 

43920  19 
lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

21 

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

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

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

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

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

26 
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

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

28 
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

29 
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

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

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

32 
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

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

34 

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

36 
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

37 
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

38 
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

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

40 
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

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

42 
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

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

44 

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

45 
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

47 
assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

49 

38656  50 
section "Simple function" 
35582  51 

38656  52 
text {* 
53 

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

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

56 
sets are measurable. 

35582  57 

38656  58 
*} 
59 

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

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

36624  63 

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

65 
assumes "simple_function M g" 
40875  66 
shows "finite (g ` space M)" and "g ` X \<inter> space M \<in> sets M" 
40871  67 
proof  
68 
show "finite (g ` space M)" 

69 
using assms unfolding simple_function_def by auto 

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

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

73 
by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def) 

40871  74 
qed 
36624  75 

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

77 
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

78 
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

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

80 
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

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

82 
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

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

84 

47694  85 
lemma simple_function_indicator_representation: 
43920  86 
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

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

90 
proof  

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

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

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

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

97 
finally show ?thesis by auto 

98 
qed 

36624  99 

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

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

106 
thus ?thesis unfolding simple_function_def by auto 

107 
qed 

108 

47694  109 
lemma simple_function_cong: 
38656  110 
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

111 
shows "simple_function M f \<longleftrightarrow> simple_function M g" 
38656  112 
proof  
113 
have "f ` space M = g ` space M" 

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

115 
using assms by (auto intro!: image_eqI) 

116 
thus ?thesis unfolding simple_function_def using assms by simp 

117 
qed 

118 

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

120 
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

121 
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

122 
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

123 

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

125 
assumes "simple_function M f" 
38656  126 
shows "f \<in> borel_measurable M" 
127 
proof (rule borel_measurableI) 

128 
fix S 

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

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

131 
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

132 
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

133 
using finite_subset[of "f ` (f ` S \<inter> space M)" "f ` space M"] by auto 
38656  134 
hence "?U \<in> sets M" 
135 
apply (rule finite_UN) 

136 
using assms unfolding simple_function_def by auto 

137 
thus "f ` S \<inter> space M \<in> sets M" unfolding * . 

35692  138 
qed 
139 

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

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

143 
shows "simple_function M f" 
38656  144 
using assms unfolding simple_function_def 
145 
by (auto intro: borel_measurable_vimage) 

146 

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

149 
shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M" 
47694  150 
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

151 
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

152 

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

154 
"simple_function M (\<lambda>x. c)" 
38656  155 
by (auto intro: finite_subset simp: simple_function_def) 
47694  156 
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

157 
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

158 
shows "simple_function M (g \<circ> f)" 
38656  159 
unfolding simple_function_def 
160 
proof safe 

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

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

163 
next 

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

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

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

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

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

169 
using assms unfolding simple_function_def * 

170 
by (rule_tac finite_UN) (auto intro!: finite_UN) 

171 
qed 

172 

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

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

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

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

181 
ultimately show ?thesis unfolding simple_function_def 

46905  182 
using assms by (auto simp: indicator_def [abs_def]) 
35692  183 
qed 
184 

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

186 
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

187 
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

188 
shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p") 
38656  189 
unfolding simple_function_def 
190 
proof safe 

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

192 
using assms unfolding simple_function_def 

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

194 
next 

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

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

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

198 
by auto 

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

200 
using assms unfolding simple_function_def by auto 

201 
qed 

35692  202 

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

204 
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

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

35582  208 

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

210 
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

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

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

216 
qed 

35582  217 

47694  218 
lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] 
38656  219 
and simple_function_diff[intro, simp] = simple_function_compose2[where h="op "] 
220 
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] 

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

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

223 
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

224 
and simple_function_max[intro, simp] = simple_function_compose2[where h=max] 
38656  225 

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

227 
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

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

231 
qed auto 

35582  232 

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

234 
fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f" 
43920  235 
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

236 
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

237 

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

239 
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

240 
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

241 
by (auto intro!: simple_function_compose1[OF sf]) 
35582  242 

47694  243 
lemma borel_measurable_implies_simple_function_sequence: 
43920  244 
fixes u :: "'a \<Rightarrow> ereal" 
38656  245 
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

246 
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

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

249 
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

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

251 
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

252 
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

253 
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

254 
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

255 
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

256 
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

257 
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

258 
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

259 
qed auto } 
38656  260 
note f_upper = this 
35582  261 

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

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

263 
"\<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

264 
unfolding f_def by auto 
35582  265 

46731  266 
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

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

268 
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

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

270 
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

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

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

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

274 
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

275 
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

276 
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

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

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

279 
then show "simple_function M (?g i)" 
43920  280 
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

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

282 
show "incseq ?g" 
43920  283 
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

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

285 
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

286 
proof ((split split_if)+, intro conjI impI) 
43920  287 
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

288 
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

289 
by (cases "u x") (auto intro!: le_natfloor) 
38656  290 
next 
43920  291 
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

292 
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

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

294 
next 
43920  295 
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

296 
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

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

298 
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

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

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

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

303 
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

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

306 
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

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

308 
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

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

310 
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

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

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

316 
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

317 
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

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

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

320 
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

321 
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

322 
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

323 
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

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

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

326 
with * have *: "\<And>i. f x i \<le> r * 2^i" by (auto simp: divide_le_eq) 
44666  327 
from reals_Archimedean2[of r] * have "u x \<noteq> \<infinity>" by (auto simp: f_def) (metis less_le_not_le) 
43920  328 
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

329 
then guess p .. note ux = this 
44666  330 
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

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

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

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

334 
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

335 
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

336 
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

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

338 
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

339 
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

340 
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

341 
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

342 
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

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

345 
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

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

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

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

349 
qed 
35582  350 

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

353 
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

354 
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

355 
"\<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

356 
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

357 

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

359 
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

360 
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

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

362 
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

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

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

365 
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

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

367 
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

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

369 
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

370 
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

371 
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

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

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

374 
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

375 
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

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

379 

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

381 
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

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

384 
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

385 
with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp 
38656  386 
qed 
387 

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

389 
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

390 
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

391 
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

392 
using assms unfolding simple_function_def by auto 
39092  393 

47694  394 
lemma simple_function_comp: 
395 
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

396 
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

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

400 
using T unfolding measurable_def by auto 

401 
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

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

405 
using T unfolding measurable_def by auto 

406 
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

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

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

411 
using T unfolding measurable_def by auto 

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

40859  413 
qed 
414 

38656  415 
section "Simple integral" 
416 

47694  417 
definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^isup>S") where 
418 
"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

419 

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

420 
syntax 
47694  421 
"_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

422 

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

423 
translations 
47694  424 
"\<integral>\<^isup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)" 
35582  425 

47694  426 
lemma simple_integral_cong: 
38656  427 
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

428 
shows "integral\<^isup>S M f = integral\<^isup>S M g" 
38656  429 
proof  
430 
have "f ` space M = g ` space M" 

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

432 
using assms by (auto intro!: image_eqI) 

433 
thus ?thesis unfolding simple_integral_def by simp 

434 
qed 

435 

47694  436 
lemma simple_integral_const[simp]: 
437 
"(\<integral>\<^isup>Sx. c \<partial>M) = c * (emeasure M) (space M)" 

38656  438 
proof (cases "space M = {}") 
439 
case True thus ?thesis unfolding simple_integral_def by simp 

440 
next 

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

442 
thus ?thesis unfolding simple_integral_def by simp 

35582  443 
qed 
444 

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

446 
assumes f: "simple_function M f" and g: "simple_function M g" 
47694  447 
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  448 
(is "_ = setsum _ (?p ` space M)") 
449 
proof 

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

38656  453 
have [intro]: 
454 
"finite (f ` space M)" 

455 
"finite (g ` space M)" 

456 
using assms unfolding simple_function_def by simp_all 

457 

458 
{ fix A 

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

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

461 
by auto 

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

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

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

465 
note sets = simple_function_measurable2[OF f g] 
35582  466 

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

47694  469 
with sets have "(emeasure M) (f ` {f x} \<inter> space M) = setsum (emeasure M) (?sub (f x))" 
47761  470 
by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) } 
47694  471 
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

472 
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

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

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

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

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

485 
thus ?thesis 

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

489 
qed 

490 
finally show ?thesis . 

35582  491 
qed 
492 

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

494 
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

495 
shows "(\<integral>\<^isup>Sx. f x + g x \<partial>M) = integral\<^isup>S M f + integral\<^isup>S M g" 
35582  496 
proof  
38656  497 
{ fix x let ?S = "g ` {g x} \<inter> f ` {f x} \<inter> space M" 
498 
assume "x \<in> space M" 

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

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

501 
by auto } 

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

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

504 
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

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

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

507 
by (subst (3) Int_commute) 
43920  508 
(auto simp add: ereal_left_distrib setsum_addf[symmetric] intro!: setsum_cong) 
35582  509 
qed 
510 

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

512 
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

513 
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

514 
shows "(\<integral>\<^isup>Sx. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>S M (f i))" 
38656  515 
proof cases 
516 
assume "finite P" 

517 
from this assms show ?thesis 

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

518 
by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg) 
38656  519 
qed auto 
520 

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

522 
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

523 
shows "(\<integral>\<^isup>Sx. c * f x \<partial>M) = c * integral\<^isup>S M f" 
38656  524 
proof  
47694  525 
note mult = simple_function_mult[OF simple_function_const[of _ c] f(1)] 
38656  526 
{ fix x let ?S = "f ` {f x} \<inter> (\<lambda>x. c * f x) ` {c * f x} \<inter> space M" 
527 
assume "x \<in> space M" 

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

529 
by auto } 

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

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

531 
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

532 
simple_function_partition[OF f(1) mult] 
43920  533 
by (subst setsum_ereal_right_distrib) 
534 
(auto intro!: ereal_0_le_mult setsum_cong simp: mult_assoc) 

40871  535 
qed 
536 

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

538 
assumes f: "simple_function M f" and g: "simple_function M g" 
47694  539 
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

540 
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g" 
40859  541 
proof  
46731  542 
let ?S = "\<lambda>x. (g ` {g x} \<inter> space M) \<inter> (f ` {f x} \<inter> space M)" 
40859  543 
have *: "\<And>x. g ` {g x} \<inter> f ` {f x} \<inter> space M = ?S x" 
544 
"\<And>x. f ` {f x} \<inter> g ` {g x} \<inter> space M = ?S x" by auto 

545 
show ?thesis 

546 
unfolding * 

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

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

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

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

47694  552 
show "the_elem (f`?S x) * (emeasure M) (?S x) \<le> the_elem (g`?S x) * (emeasure M) (?S x)" 
40859  553 
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

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

555 
using * assms(1,2)[THEN simple_functionD(2)] 
43920  556 
by (auto intro!: ereal_mult_right_mono) 
40859  557 
next 
558 
case False 

47694  559 
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  560 
using mono by (auto elim!: AE_E) 
561 
have "?S x \<subseteq> N" using N `x \<in> space M` False by auto 

40871  562 
moreover have "?S x \<in> sets M" using assms 
563 
by (rule_tac Int) (auto intro!: simple_functionD) 

47694  564 
ultimately have "(emeasure M) (?S x) \<le> (emeasure M) N" 
565 
using `N \<in> sets M` by (auto intro!: emeasure_mono) 

566 
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

567 
using assms(1,2)[THEN simple_functionD(2)] by auto 
47694  568 
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

569 
then show ?thesis by simp 
40859  570 
qed 
571 
qed 

572 
qed 

573 

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

575 
assumes "simple_function M f" and "simple_function M g" 
38656  576 
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

577 
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g" 
41705  578 
using assms by (intro simple_integral_mono_AE) auto 
35582  579 

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

581 
assumes "simple_function M f" and "simple_function M g" 
47694  582 
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

583 
shows "integral\<^isup>S M f = integral\<^isup>S M g" 
40859  584 
using assms by (auto simp: eq_iff intro!: simple_integral_mono_AE) 
585 

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

587 
assumes sf: "simple_function M f" "simple_function M g" 
47694  588 
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

589 
shows "integral\<^isup>S M f = integral\<^isup>S M g" 
40859  590 
proof (intro simple_integral_cong_AE sf AE_I) 
47694  591 
show "(emeasure M) {x\<in>space M. f x \<noteq> g x} = 0" by fact 
40859  592 
show "{x \<in> space M. f x \<noteq> g x} \<in> sets M" 
593 
using sf[THEN borel_measurable_simple_function] by auto 

594 
qed simp 

595 

47694  596 
lemma simple_integral_indicator: 
38656  597 
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

598 
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

599 
shows "(\<integral>\<^isup>Sx. f x * indicator A x \<partial>M) = 
47694  600 
(\<Sum>x \<in> f ` space M. x * (emeasure M) (f ` {x} \<inter> space M \<inter> A))" 
38656  601 
proof cases 
602 
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

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

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

607 
next 

608 
assume "A \<noteq> space M" 

609 
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets_into_space[OF assms(1)] by auto 

610 
have I: "(\<lambda>x. f x * indicator A x) ` space M = f ` A \<union> {0}" (is "?I ` _ = _") 

35582  611 
proof safe 
38656  612 
fix y assume "?I y \<notin> f ` A" hence "y \<notin> A" by auto thus "?I y = 0" by auto 
613 
next 

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

615 
using sets_into_space[OF assms(1)] by (auto intro!: image_eqI[of _ _ y]) 

616 
next 

617 
show "0 \<in> ?I ` space M" using x by (auto intro!: image_eqI[of _ _ x]) 

35582  618 
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

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

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

624 
using assms(2) unfolding simple_function_def by auto 

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

626 
using sets_into_space[OF assms(1)] by auto 

40859  627 
have "\<And>x. f x \<notin> f ` A \<Longrightarrow> f ` {f x} \<inter> space M \<inter> A = {}" 
628 
by (auto simp: image_iff) 

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

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

634 
by (auto simp: indicator_def split: split_if_asm) 

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

38656  637 
qed 
638 
show ?thesis unfolding * 

639 
using assms(2) unfolding simple_function_def 

640 
by (auto intro!: setsum_mono_zero_cong_right) 

641 
qed 

35582  642 

47694  643 
lemma simple_integral_indicator_only[simp]: 
38656  644 
assumes "A \<in> sets M" 
47694  645 
shows "integral\<^isup>S M (indicator A) = emeasure M A" 
38656  646 
proof cases 
647 
assume "space M = {}" hence "A = {}" using sets_into_space[OF assms] by auto 

648 
thus ?thesis unfolding simple_integral_def using `space M = {}` by auto 

649 
next 

43920  650 
assume "space M \<noteq> {}" hence "(\<lambda>x. 1) ` space M = {1::ereal}" by auto 
38656  651 
thus ?thesis 
47694  652 
using simple_integral_indicator[OF assms simple_function_const[of _ 1]] 
38656  653 
using sets_into_space[OF assms] 
47694  654 
by (auto intro!: arg_cong[where f="(emeasure M)"]) 
38656  655 
qed 
35582  656 

47694  657 
lemma simple_integral_null_set: 
658 
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

659 
shows "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = 0" 
38656  660 
proof  
47694  661 
have "AE x in M. indicator N x = (0 :: ereal)" 
662 
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

663 
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

664 
using assms apply (intro simple_integral_cong_AE) by auto 
40859  665 
then show ?thesis by simp 
38656  666 
qed 
35582  667 

47694  668 
lemma simple_integral_cong_AE_mult_indicator: 
669 
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

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

47694  673 
lemma simple_integral_distr: 
674 
assumes T: "T \<in> measurable M M'" 

675 
and f: "simple_function M' f" 

676 
shows "integral\<^isup>S (distr M M' T) f = (\<integral>\<^isup>S x. f (T x) \<partial>M)" 

39092  677 
unfolding simple_integral_def 
47694  678 
proof (intro setsum_mono_zero_cong_right ballI) 
679 
show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space (distr M M' T)" 

680 
using T unfolding measurable_def by auto 

681 
show "finite (f ` space (distr M M' T))" 

682 
using f unfolding simple_function_def by auto 

39092  683 
next 
47694  684 
fix i assume "i \<in> f ` space (distr M M' T)  (\<lambda>x. f (T x)) ` space M" 
685 
then have "T ` (f ` {i} \<inter> space (distr M M' T)) \<inter> space M = {}" by (auto simp: image_iff) 

686 
with f[THEN simple_functionD(2), of "{i}"] 

687 
show "i * emeasure (distr M M' T) (f ` {i} \<inter> space (distr M M' T)) = 0" 

688 
using T by (simp add: emeasure_distr) 

39092  689 
next 
47694  690 
fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M" 
691 
then have "T ` (f ` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) ` {i} \<inter> space M" 

692 
using T unfolding measurable_def by auto 

693 
with f[THEN simple_functionD(2), of "{i}"] T 

694 
show "i * emeasure (distr M M' T) (f ` {i} \<inter> space (distr M M' T)) = 

695 
i * (emeasure M) ((\<lambda>x. f (T x)) ` {i} \<inter> space M)" 

696 
by (auto simp add: emeasure_distr) 

39092  697 
qed 
698 

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

700 
assumes A: "A \<in> sets M" 
47694  701 
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

702 
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

703 
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

704 

47694  705 
lemma simple_integral_positive: 
706 
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

707 
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

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

709 
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

710 
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

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

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

713 

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

714 
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

715 

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

717 
"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  718 

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

719 
syntax 
47694  720 
"_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

721 

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

722 
translations 
47694  723 
"\<integral>\<^isup>+ x. f \<partial>M" == "CONST positive_integral M (%x. f)" 
40872  724 

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

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

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

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

731 

732 
lemma positive_integral_def_finite: 

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

733 
"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

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

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

736 
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

737 
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

738 
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

739 
note gM = g(1)[THEN borel_measurable_simple_function] 
47694  740 
have \<mu>G_pos: "0 \<le> (emeasure M) ?G" using gM by auto 
46731  741 
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

742 
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

743 
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

744 
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

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

746 
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

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

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

751 
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

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

753 
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

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

755 
next 
47694  756 
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

757 
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

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

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

762 
then have "?g ?y \<in> ?A" by (rule g_in_A) 
47694  763 
have "real n \<le> ?y * (emeasure M) ?G" 
764 
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

765 
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

766 
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

767 
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

768 
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

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

770 
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

771 
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

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

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

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

775 
qed (auto intro: SUP_upper) 
40873  776 

47694  777 
lemma positive_integral_mono_AE: 
778 
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

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

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

781 
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

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

786 
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

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

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

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

790 
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

791 
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

792 
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

793 
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

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

795 
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

796 
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

797 
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

798 
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

799 
by force 
38656  800 
qed 
801 

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

803 
"(\<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

804 
by (auto intro: positive_integral_mono_AE) 
40859  805 

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

40859  808 
by (auto simp: eq_iff intro!: positive_integral_mono_AE) 
809 

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

811 
"(\<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

812 
by (auto intro: positive_integral_cong_AE) 
40859  813 

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

815 
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

816 
proof  
46731  817 
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

818 
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

819 
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

820 
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

821 
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

822 
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

823 
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

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

825 
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

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

827 
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

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

829 

47694  830 
lemma positive_integral_eq_simple_integral_AE: 
831 
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

832 
proof  
47694  833 
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

834 
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

835 
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

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

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

838 
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

839 
qed 
40873  840 

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

842 
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

843 
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

844 
shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S") 
43920  845 
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

846 
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

847 
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

848 
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

849 
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

850 
using u(3) by auto 
43920  851 
fix a :: ereal assume "0 < a" "a < 1" 
38656  852 
hence "a \<noteq> 0" by auto 
46731  853 
let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}" 
38656  854 
have B: "\<And>i. ?B i \<in> sets M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

855 
using f `simple_function M u` by (auto simp: borel_measurable_simple_function) 
38656  856 

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

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

860 
proof safe 

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

862 
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

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

866 
note B_mono = this 

35582  867 

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

868 
note B_u = Int[OF u(1)[THEN simple_functionD(2)] B] 
38656  869 

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

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

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

874 
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

875 
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

876 
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

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

878 
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

879 
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

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

881 
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

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

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

884 
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

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

888 
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

889 
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

890 
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

891 
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

892 
qed 
40859  893 
qed 
47694  894 
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

895 
qed 
38656  896 

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

897 
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

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

38656  903 
next 
47694  904 
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

905 
using measure_conv u_range B_u unfolding simple_integral_def 
43920  906 
by (auto intro!: setsum_cong SUPR_ereal_cmult[symmetric]) 
38656  907 
qed 
908 
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

909 
have "a * (SUP i. integral\<^isup>S M (?uB i)) \<le> ?S" 
43920  910 
apply (subst SUPR_ereal_cmult[symmetric]) 
38705  911 
proof (safe intro!: SUP_mono bexI) 
38656  912 
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

913 
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

914 
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

915 
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

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

918 
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

919 
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

920 
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

921 
(auto intro!: positive_integral_mono split: split_indicator) 
38656  922 
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

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

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

926 
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

927 
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

928 
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

929 
ultimately show "a * integral\<^isup>S M u \<le> ?S" by simp 
35582  930 
qed 
931 

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

933 
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

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

935 
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

936 
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

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

938 
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

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

940 

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

943 
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

944 
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

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

946 
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

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

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

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

952 
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

953 
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

954 
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

955 
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

956 
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

957 
by (intro positive_integral_SUP_approx[OF f g _ g']) 
46884  958 
(auto simp: le_fun_def max_def) 
35582  959 
qed 
960 
qed 

961 

47694  962 
lemma positive_integral_monotone_convergence_SUP_AE: 
963 
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

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

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

968 
from this[THEN AE_E] guess N . note N = this 
46731  969 
let ?f = "\<lambda>i x. if x \<in> space M  N then f i x else 0" 
47694  970 
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

971 
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

972 
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

973 
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

974 
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

975 
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

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

977 
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

978 
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

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

981 
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

982 
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

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

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

985 

47694  986 
lemma positive_integral_monotone_convergence_SUP_AE_incseq: 
987 
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

988 
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

989 
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

990 
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

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

992 

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

994 
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

995 
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

996 
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

997 
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

998 
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

999 

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

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

1001 
"(\<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

1002 
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

1003 

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

1005 
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

1006 
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

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

1008 
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

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

1010 
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

1011 
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

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

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

1014 
then show ?thesis by (simp add: positive_integral_max_0) 
40859  1015 
qed 
1016 

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

1018 
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

1019 
and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)" 
47694  1020 
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

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

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

1024 
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

1025 
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

1026 
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

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

1029 
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

1030 
finally show ?thesis by simp 
38656  1031 
qed 
1032 

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

38656  1035 
by (subst positive_integral_eq_simple_integral) auto 
1036 

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

1038 
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

1039 
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

1040 
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

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

1043 
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

1044 
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

1045 
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

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

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

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

1051 
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

1052 

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

1053 
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

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

1055 
by (auto simp: incseq_Suc_iff le_fun_def 
43920  1056 
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

1057 
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

1058 
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

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

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

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

1062 

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

1063 
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

1064 
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

1065 
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

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

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

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

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

1071 
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

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

1075 
simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) } 

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

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

1080 
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

1081 
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

1082 
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

1083 
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:
41831
diff
changeset

1084 
unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric] 
43920  1085 
apply (subst SUPR_ereal_cmult[symmetric, OF pos(1) `0 \<le> a`]) 
1086 
apply (subst SUPR_ereal_add[symmetric, OF inc not_MInf]) . 

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

1087 
then show ?thesis by (simp add: positive_integral_max_0) 
38656  1088 
qed 
1089 

47694  1090 
lemma positive_integral_cmult: 
49775
970964690b3d
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
hoelzl
parents:
47761
diff
changeset

1091 
assumes f: "f \<in> borel_measurable M" "0 \<le> c" 
41689
3e39b0e730d6
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 
shows "(\<integral>\<^isup>+ x. c * f x \<partial>M) = c * integral\<^isup>P M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1094 
have [simp]: "\<And>x. c * max 0 (f x) = max 0 (c * f x)" using `0 \<le> c` 
43920  1095 
by (auto split: split_max simp: ereal_zero_le_0_iff) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

1098 
then show ?thesis 
47694  1099 
using positive_integral_linear[OF _ _ `0 \<le> c`, of "\<lambda>x. max 0 (f x)" _ "\<lambda>x. 0"] f 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1101 
qed 
38656  1102 

47694  1103 
lemma positive_integral_multc: 
49775
970964690b3d
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
hoelzl
parents:
47761
diff
changeset

1104 
assumes "f \<in> borel_measurable M" "0 \<le> c" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

1105 
shows "(\<integral>\<^isup>+ x. f x * c \<partial>M) = integral\<^isup>P M f * c" 
41096  1106 
unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp 
1107 

47694  1108 
lemma positive_integral_indicator[simp]: 
1109 
"A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. indicator A x\<partial>M) = (emeasure M) A" 

41544  1110 
by (subst positive_integral_eq_simple_integral) 
49775
970964690b3d
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
hoelzl
parents:
47761
diff
changeset

1111 
(auto simp: simple_integral_indicator) 
38656  1112 

47694  1113 
lemma positive_integral_cmult_indicator: 
1114 
"0 \<le> c \<Longrightarrow> A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+ x. c * indicator A x \<partial>M) = c * (emeasure M) A" 

41544  1115 
by (subst positive_integral_eq_simple_integral) 
1116 
(auto simp: simple_function_indicator simple_integral_indicator) 

38656  1117 

47694  1118 
lemma positive_integral_add: 
1119 
assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" 

1120 
and g: "g \<in> borel_measurable M" "AE x in M. 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

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

1122 
proof  
47694  1123 
have ae: "AE x in M. max 0 (f x) + max 0 (g x) = max 0 (f x + g x)" 
43920  1124 
using assms by (auto split: split_max simp: ereal_add_nonneg_nonneg) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

1127 
also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (f 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

1128 
unfolding ae[THEN positive_integral_cong_AE] .. 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1129 
also have "\<dots> = (\<integral>\<^isup>+ x. max 0 (f x) \<partial>M) + (\<integral>\<^isup>+ x. max 0 (g x) \<partial>M)" 
47694  1130 
using positive_integral_linear[of "\<lambda>x. max 0 (f x)" _ 1 "\<lambda>x. max 0 (g x)"] f g 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

1134 
qed 
38656  1135 

47694  1136 
lemma positive_integral_setsum: 
1137 
assumes "\<And>i. i\<in>P \<Longrightarrow> f i \<in> borel_measurable M" "\<And>i. i\<in>P \<Longrightarrow> AE x in M. 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

1138 
shows "(\<integral>\<^isup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^isup>P M (f i))" 
38656  1139 
proof cases 