author  hoelzl 
Fri, 30 May 2014 15:56:30 +0200  
changeset 57137  f174712d0a84 
parent 57025  e7fd64f82876 
child 57275  0ddb5b755cdc 
permissions  rwrr 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

1 
(* Title: HOL/Probability/Nonnegative_Lebesgue_Integration.thy 
42067  2 
Author: Johannes Hölzl, TU München 
3 
Author: Armin Heller, TU München 

4 
*) 

38656  5 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

6 
header {* Lebesgue Integration for Nonnegative Functions *} 
35582  7 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

8 
theory Nonnegative_Lebesgue_Integration 
47694  9 
imports Measure_Space Borel_Space 
35582  10 
begin 
11 

56949  12 
lemma indicator_less_ereal[simp]: 
13 
"indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)" 

14 
by (simp add: indicator_def not_le) 

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

15 

56994  16 
subsection "Simple function" 
35582  17 

38656  18 
text {* 
19 

56996  20 
Our simple functions are not restricted to nonnegative real numbers. Instead 
38656  21 
they are just functions with a finite range and are measurable when singleton 
22 
sets are measurable. 

35582  23 

38656  24 
*} 
25 

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

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

36624  29 

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

31 
assumes "simple_function M g" 
40875  32 
shows "finite (g ` space M)" and "g ` X \<inter> space M \<in> sets M" 
40871  33 
proof  
34 
show "finite (g ` space M)" 

35 
using assms unfolding simple_function_def by auto 

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

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

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

39 
by (auto simp del: UN_simps simp: simple_function_def) 
40871  40 
qed 
36624  41 

56949  42 
lemma measurable_simple_function[measurable_dest]: 
43 
"simple_function M f \<Longrightarrow> f \<in> measurable M (count_space UNIV)" 

44 
unfolding simple_function_def measurable_def 

45 
proof safe 

46 
fix A assume "finite (f ` space M)" "\<forall>x\<in>f ` space M. f ` {x} \<inter> space M \<in> sets M" 

47 
then have "(\<Union>x\<in>f ` space M. if x \<in> A then f ` {x} \<inter> space M else {}) \<in> sets M" 

48 
by (intro sets.finite_UN) auto 

49 
also have "(\<Union>x\<in>f ` space M. if x \<in> A then f ` {x} \<inter> space M else {}) = f ` A \<inter> space M" 

50 
by (auto split: split_if_asm) 

51 
finally show "f ` A \<inter> space M \<in> sets M" . 

52 
qed simp 

53 

54 
lemma borel_measurable_simple_function: 

55 
"simple_function M f \<Longrightarrow> f \<in> borel_measurable M" 

56 
by (auto dest!: measurable_simple_function simp: measurable_def) 

57 

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

59 
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

60 
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

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

62 
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

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

64 
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

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

66 

47694  67 
lemma simple_function_indicator_representation: 
43920  68 
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

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

72 
proof  

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

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

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

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

79 
finally show ?thesis by auto 

80 
qed 

36624  81 

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

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

88 
thus ?thesis unfolding simple_function_def by auto 

89 
qed 

90 

47694  91 
lemma simple_function_cong: 
38656  92 
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

93 
shows "simple_function M f \<longleftrightarrow> simple_function M g" 
38656  94 
proof  
95 
have "f ` space M = g ` space M" 

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

97 
using assms by (auto intro!: image_eqI) 

98 
thus ?thesis unfolding simple_function_def using assms by simp 

99 
qed 

100 

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

102 
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

103 
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

104 
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

105 

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

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

109 
shows "simple_function M f" 
38656  110 
using assms unfolding simple_function_def 
111 
by (auto intro: borel_measurable_vimage) 

112 

56949  113 
lemma simple_function_eq_measurable: 
43920  114 
fixes f :: "'a \<Rightarrow> ereal" 
56949  115 
shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> measurable M (count_space UNIV)" 
116 
using simple_function_borel_measurable[of f] measurable_simple_function[of M f] 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44666
diff
changeset

117 
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

118 

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

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

123 
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

124 
shows "simple_function M (g \<circ> f)" 
38656  125 
unfolding simple_function_def 
126 
proof safe 

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

56154
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
54611
diff
changeset

128 
using assms unfolding simple_function_def by (auto simp: image_comp [symmetric]) 
38656  129 
next 
130 
fix x assume "x \<in> space M" 

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

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

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

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

135 
using assms unfolding simple_function_def * 

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

136 
by (rule_tac sets.finite_UN) auto 
38656  137 
qed 
138 

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

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

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

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

147 
ultimately show ?thesis unfolding simple_function_def 

46905  148 
using assms by (auto simp: indicator_def [abs_def]) 
35692  149 
qed 
150 

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

152 
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

153 
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

154 
shows "simple_function M (\<lambda>x. (f x, g x))" (is "simple_function M ?p") 
38656  155 
unfolding simple_function_def 
156 
proof safe 

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

158 
using assms unfolding simple_function_def 

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

160 
next 

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

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

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

164 
by auto 

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

166 
using assms unfolding simple_function_def by auto 

167 
qed 

35692  168 

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

170 
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

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

35582  174 

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

176 
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

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

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

182 
qed 

35582  183 

47694  184 
lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"] 
38656  185 
and simple_function_diff[intro, simp] = simple_function_compose2[where h="op "] 
186 
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"] 

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

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

189 
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

190 
and simple_function_max[intro, simp] = simple_function_compose2[where h=max] 
38656  191 

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

193 
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

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

197 
qed auto 

35582  198 

56949  199 
lemma simple_function_ereal[intro, simp]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

200 
fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f" 
56949  201 
shows "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

202 
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

203 

56949  204 
lemma simple_function_real_of_nat[intro, simp]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

205 
fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f" 
56949  206 
shows "simple_function M (\<lambda>x. real (f x))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

207 
by (auto intro!: simple_function_compose1[OF sf]) 
35582  208 

47694  209 
lemma borel_measurable_implies_simple_function_sequence: 
43920  210 
fixes u :: "'a \<Rightarrow> ereal" 
38656  211 
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

212 
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

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

215 
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

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

217 
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

218 
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

219 
then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)" 
56536  220 
by (cases "u x") (auto intro!: natfloor_mono) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

221 
moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j" 
56536  222 
by (intro real_natfloor_le) auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

223 
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

224 
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

225 
qed auto } 
38656  226 
note f_upper = this 
35582  227 

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

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

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

230 
unfolding f_def by auto 
35582  231 

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

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

234 
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

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

236 
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

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

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

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

240 
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

241 
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

242 
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

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

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

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

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

248 
show "incseq ?g" 
43920  249 
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

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

251 
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

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

254 
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

255 
by (cases "u x") (auto intro!: le_natfloor) 
38656  256 
next 
43920  257 
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

258 
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

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

260 
next 
43920  261 
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

262 
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

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

264 
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

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

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

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

269 
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

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

272 
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

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

274 
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

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

276 
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

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

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

282 
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

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

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

286 
fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y" 
56571
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56537
diff
changeset

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

288 
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

289 
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

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

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

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

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

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

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

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

300 
with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p  r"] 
56536  301 
obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n  1" by (auto simp: field_simps) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

302 
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

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

304 
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

305 
using *[of "max N m"] m unfolding real_f using ux 
56536  306 
by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

307 
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

308 
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

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

311 
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

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

313 
qed 
56571
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56537
diff
changeset

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

315 
qed 
35582  316 

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

319 
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

320 
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

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

322 
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

323 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

354 

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

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

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

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

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

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

360 
assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

375 
next 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

376 

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

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

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

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

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

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

382 
using set[of "{}"] by (simp add: indicator_def[abs_def]) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

383 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

384 
case (insert x S) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

385 
{ fix z have "(\<Sum>y\<in>S. y * indicator (u ` {y} \<inter> space M) z) = 0 \<or> 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

386 
x * indicator (u ` {x} \<inter> space M) z = 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

387 
using insert by (subst setsum_ereal_0) (auto simp: indicator_def) } 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

388 
note disj = this 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

389 
from insert show ?case 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

390 
by (auto intro!: add mult set simple_functionD u setsum_nonneg simple_function_setsum disj) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

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

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

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

394 

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

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

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

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

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

399 
assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

400 
assumes mult': "\<And>u c. 0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < \<infinity>) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

401 
assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < \<infinity>) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> v x < \<infinity>) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

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

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

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

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

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

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

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

409 
using nn u sup by (auto simp: max_def) 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

410 

e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

411 
have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

412 
using U by (auto simp: image_iff eq_commute) 
49796
182fa22e7ee8
introduce induction rules for simple functions and for Borel measurable functions
hoelzl
parents:
49795
diff
changeset

413 

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

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

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

416 

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

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

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

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

420 
fix i show "P (U i)" 
56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

421 
using `simple_function M (U i)` nn[of i] not_inf[of _ i] 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

422 
proof (induct rule: simple_function_induct_nn) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

423 
case (mult u c) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

424 
show ?case 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

425 
proof cases 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

426 
assume "c = 0 \<or> space M = {} \<or> (\<forall>x\<in>space M. u x = 0)" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

427 
with mult(2) show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

428 
by (intro cong[of "\<lambda>x. c * u x" "indicator {}"] set) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

429 
(auto dest!: borel_measurable_simple_function) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

430 
next 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

431 
assume "\<not> (c = 0 \<or> space M = {} \<or> (\<forall>x\<in>space M. u x = 0))" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

432 
with mult obtain x where u_fin: "\<And>x. x \<in> space M \<Longrightarrow> u x < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

433 
and x: "x \<in> space M" "u x \<noteq> 0" "c \<noteq> 0" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

434 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

435 
with mult have "P u" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

436 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

437 
from x mult(5)[OF `x \<in> space M`] mult(1) mult(3)[of x] have "c < \<infinity>" 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

438 
by auto 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

439 
with u_fin mult 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

440 
show ?thesis 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

441 
by (intro mult') (auto dest!: borel_measurable_simple_function) 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

442 
qed 
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

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

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

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

446 

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

448 
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

449 
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

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

451 
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

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

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

454 
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

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

456 
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

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

458 
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

459 
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

460 
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

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

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

463 
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

464 
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

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

468 

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

470 
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

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

473 
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

474 
with simple_function_If_set[OF sf, of "{x. P x}"] P show ?thesis by simp 
38656  475 
qed 
476 

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

478 
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

479 
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

480 
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

481 
using assms unfolding simple_function_def by auto 
39092  482 

47694  483 
lemma simple_function_comp: 
484 
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

485 
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

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

489 
using T unfolding measurable_def by auto 

490 
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

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

494 
using T unfolding measurable_def by auto 

495 
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

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

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

500 
using T unfolding measurable_def by auto 

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

40859  502 
qed 
503 

56994  504 
subsection "Simple integral" 
38656  505 

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

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

507 
"integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f ` {x} \<inter> space M))" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

508 

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

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

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

511 

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

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

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

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

517 
shows "integral\<^sup>S M f = integral\<^sup>S M g" 
38656  518 
proof  
519 
have "f ` space M = g ` space M" 

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

521 
using assms by (auto intro!: image_eqI) 

522 
thus ?thesis unfolding simple_integral_def by simp 

523 
qed 

524 

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

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

529 
next 

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

531 
thus ?thesis unfolding simple_integral_def by simp 

35582  532 
qed 
533 

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

535 
assumes f: "simple_function M f" and g: "simple_function M g" 
56949  536 
assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y" 
537 
assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)" 

538 
shows "integral\<^sup>S M f = (\<Sum>y\<in>g ` space M. v y * emeasure M {x\<in>space M. g x = y})" 

539 
(is "_ = ?r") 

540 
proof  

541 
from f g have [simp]: "finite (f`space M)" "finite (g`space M)" 

542 
by (auto simp: simple_function_def) 

543 
from f g have [measurable]: "f \<in> measurable M (count_space UNIV)" "g \<in> measurable M (count_space UNIV)" 

544 
by (auto intro: measurable_simple_function) 

35582  545 

56949  546 
{ fix y assume "y \<in> space M" 
547 
then have "f ` space M \<inter> {i. \<exists>x\<in>space M. i = f x \<and> g y = g x} = {v (g y)}" 

548 
by (auto cong: sub simp: v[symmetric]) } 

549 
note eq = this 

35582  550 

56949  551 
have "integral\<^sup>S M f = 
552 
(\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M. 

553 
if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))" 

554 
unfolding simple_integral_def 

555 
proof (safe intro!: setsum_cong ereal_left_mult_cong) 

556 
fix y assume y: "y \<in> space M" "f y \<noteq> 0" 

557 
have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} = 

558 
{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}" 

559 
by auto 

560 
have eq:"(\<Union>i\<in>{z. \<exists>x\<in>space M. f y = f x \<and> z = g x}. {x \<in> space M. g x = i}) = 

561 
f ` {f y} \<inter> space M" 

562 
by (auto simp: eq_commute cong: sub rev_conj_cong) 

563 
have "finite (g`space M)" by simp 

564 
then have "finite {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}" 

565 
by (rule rev_finite_subset) auto 

566 
then show "emeasure M (f ` {f y} \<inter> space M) = 

567 
(\<Sum>z\<in>g ` space M. if \<exists>x\<in>space M. f y = f x \<and> z = g x then emeasure M {x \<in> space M. g x = z} else 0)" 

568 
apply (simp add: setsum_cases) 

569 
apply (subst setsum_emeasure) 

570 
apply (auto simp: disjoint_family_on_def eq) 

571 
done 

38656  572 
qed 
56949  573 
also have "\<dots> = (\<Sum>y\<in>f`space M. (\<Sum>z\<in>g`space M. 
574 
if \<exists>x\<in>space M. y = f x \<and> z = g x then y * emeasure M {x\<in>space M. g x = z} else 0))" 

575 
by (auto intro!: setsum_cong simp: setsum_ereal_right_distrib emeasure_nonneg) 

576 
also have "\<dots> = ?r" 

577 
by (subst setsum_commute) 

578 
(auto intro!: setsum_cong simp: setsum_cases scaleR_setsum_right[symmetric] eq) 

579 
finally show "integral\<^sup>S M f = ?r" . 

35582  580 
qed 
581 

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

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

584 
shows "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = integral\<^sup>S M f + integral\<^sup>S M g" 
35582  585 
proof  
56949  586 
have "(\<integral>\<^sup>Sx. f x + g x \<partial>M) = 
587 
(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. (fst y + snd y) * emeasure M {x\<in>space M. (f x, g x) = y})" 

588 
by (intro simple_function_partition) (auto intro: f g) 

589 
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) + 

590 
(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y})" 

591 
using assms(2,4) by (auto intro!: setsum_cong ereal_left_distrib simp: setsum_addf[symmetric]) 

592 
also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. f x \<partial>M)" 

593 
by (intro simple_function_partition[symmetric]) (auto intro: f g) 

594 
also have "(\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * emeasure M {x\<in>space M. (f x, g x) = y}) = (\<integral>\<^sup>Sx. g x \<partial>M)" 

595 
by (intro simple_function_partition[symmetric]) (auto intro: f g) 

596 
finally show ?thesis . 

35582  597 
qed 
598 

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

600 
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

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

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

605 
from this assms show ?thesis 

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

606 
by induct (auto simp: simple_function_setsum simple_integral_add setsum_nonneg) 
38656  607 
qed auto 
608 

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

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

611 
shows "(\<integral>\<^sup>Sx. c * f x \<partial>M) = c * integral\<^sup>S M f" 
38656  612 
proof  
56949  613 
have "(\<integral>\<^sup>Sx. c * f x \<partial>M) = (\<Sum>y\<in>f ` space M. (c * y) * emeasure M {x\<in>space M. f x = y})" 
614 
using f by (intro simple_function_partition) auto 

615 
also have "\<dots> = c * integral\<^sup>S M f" 

616 
using f unfolding simple_integral_def 

617 
by (subst setsum_ereal_right_distrib) (auto simp: emeasure_nonneg mult_assoc Int_def conj_commute) 

618 
finally show ?thesis . 

40871  619 
qed 
620 

47694  621 
lemma simple_integral_mono_AE: 
56949  622 
assumes f[measurable]: "simple_function M f" and g[measurable]: "simple_function M g" 
47694  623 
and mono: "AE x in M. f x \<le> g x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

624 
shows "integral\<^sup>S M f \<le> integral\<^sup>S M g" 
40859  625 
proof  
56949  626 
let ?\<mu> = "\<lambda>P. emeasure M {x\<in>space M. P x}" 
627 
have "integral\<^sup>S M f = (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. fst y * ?\<mu> (\<lambda>x. (f x, g x) = y))" 

628 
using f g by (intro simple_function_partition) auto 

629 
also have "\<dots> \<le> (\<Sum>y\<in>(\<lambda>x. (f x, g x))`space M. snd y * ?\<mu> (\<lambda>x. (f x, g x) = y))" 

630 
proof (clarsimp intro!: setsum_mono) 

40859  631 
fix x assume "x \<in> space M" 
56949  632 
let ?M = "?\<mu> (\<lambda>y. f y = f x \<and> g y = g x)" 
633 
show "f x * ?M \<le> g x * ?M" 

634 
proof cases 

635 
assume "?M \<noteq> 0" 

636 
then have "0 < ?M" 

637 
by (simp add: less_le emeasure_nonneg) 

638 
also have "\<dots> \<le> ?\<mu> (\<lambda>y. f x \<le> g x)" 

639 
using mono by (intro emeasure_mono_AE) auto 

640 
finally have "\<not> \<not> f x \<le> g x" 

641 
by (intro notI) auto 

642 
then show ?thesis 

643 
by (intro ereal_mult_right_mono) auto 

644 
qed simp 

40859  645 
qed 
56949  646 
also have "\<dots> = integral\<^sup>S M g" 
647 
using f g by (intro simple_function_partition[symmetric]) auto 

648 
finally show ?thesis . 

40859  649 
qed 
650 

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

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

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

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

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

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

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

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

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

671 
qed simp 

672 

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

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

676 
shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = 
56949  677 
(\<Sum>x \<in> f ` space M. x * emeasure M (f ` {x} \<inter> space M \<inter> A))" 
678 
proof  

679 
have eq: "(\<lambda>x. (f x, indicator A x)) ` space M \<inter> {x. snd x = 1} = (\<lambda>x. (f x, 1::ereal))`A" 

680 
using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: split_if_asm) 

681 
have eq2: "\<And>x. f x \<notin> f ` A \<Longrightarrow> f ` {f x} \<inter> space M \<inter> A = {}" 

682 
by (auto simp: image_iff) 

683 

684 
have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = 

685 
(\<Sum>y\<in>(\<lambda>x. (f x, indicator A x))`space M. (fst y * snd y) * emeasure M {x\<in>space M. (f x, indicator A x) = y})" 

686 
using assms by (intro simple_function_partition) auto 

687 
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ereal))`space M. 

688 
if snd y = 1 then fst y * emeasure M (f ` {fst y} \<inter> space M \<inter> A) else 0)" 

689 
by (auto simp: indicator_def split: split_if_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum_cong) 

690 
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ereal))`A. fst y * emeasure M (f ` {fst y} \<inter> space M \<inter> A))" 

691 
using assms by (subst setsum_cases) (auto intro!: simple_functionD(1) simp: eq) 

692 
also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ereal))`A. y * emeasure M (f ` {y} \<inter> space M \<inter> A))" 

693 
by (subst setsum_reindex[where f=fst]) (auto simp: inj_on_def) 

694 
also have "\<dots> = (\<Sum>x \<in> f ` space M. x * emeasure M (f ` {x} \<inter> space M \<inter> A))" 

695 
using A[THEN sets.sets_into_space] 

696 
by (intro setsum_mono_zero_cong_left simple_functionD f) (auto simp: image_comp comp_def eq2) 

697 
finally show ?thesis . 

38656  698 
qed 
35582  699 

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

702 
shows "integral\<^sup>S M (indicator A) = emeasure M A" 
56949  703 
using simple_integral_indicator[OF assms, of "\<lambda>x. 1"] sets.sets_into_space[OF assms] 
704 
by (simp_all add: image_constant_conv Int_absorb1 split: split_if_asm) 

35582  705 

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

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

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

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

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

713 
using assms apply (intro simple_integral_cong_AE) by auto 
40859  714 
then show ?thesis by simp 
38656  715 
qed 
35582  716 

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

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

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

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

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

725 
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

726 
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

727 

56996  728 
lemma simple_integral_nonneg: 
47694  729 
assumes f: "simple_function M f" and ae: "AE x in M. 0 \<le> f x" 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

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

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

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

733 
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

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

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

736 

56994  737 
subsection {* Integral on nonnegative functions *} 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

738 

56996  739 
definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>N") where 
740 
"integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)" 

35692  741 

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

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

744 

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

745 
translations 
56996  746 
"\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)" 
40872  747 

57025  748 
lemma nn_integral_nonneg: "0 \<le> integral\<^sup>N M f" 
56996  749 
by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def) 
40873  750 

56996  751 
lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> \<infinity>" 
752 
using nn_integral_nonneg[of M f] by auto 

47694  753 

56996  754 
lemma nn_integral_def_finite: 
755 
"integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)" 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56213
diff
changeset

756 
(is "_ = SUPREMUM ?A ?f") 
56996  757 
unfolding nn_integral_def 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44890
diff
changeset

758 
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

759 
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

760 
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

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

764 
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

765 
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

766 
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

767 
done 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56213
diff
changeset

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

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

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

773 
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

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

775 
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

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

777 
next 
50252  778 
assume \<mu>_G: "(emeasure M) ?G \<noteq> 0" 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56213
diff
changeset

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

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

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

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

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

788 
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

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

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

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

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

793 
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

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

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

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

797 
qed (auto intro: SUP_upper) 
40873  798 

56996  799 
lemma nn_integral_mono_AE: 
800 
assumes ae: "AE x in M. u x \<le> v x" shows "integral\<^sup>N M u \<le> integral\<^sup>N M v" 

801 
unfolding nn_integral_def 

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

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

803 
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

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

808 
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

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

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

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

812 
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

813 
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

814 
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

815 
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

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

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

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

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

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

821 
by force 
38656  822 
qed 
823 

56996  824 
lemma nn_integral_mono: 
825 
"(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^sup>N M u \<le> integral\<^sup>N M v" 

826 
by (auto intro: nn_integral_mono_AE) 

40859  827 

56996  828 
lemma nn_integral_cong_AE: 
829 
"AE x in M. u x = v x \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v" 

830 
by (auto simp: eq_iff intro!: nn_integral_mono_AE) 

40859  831 

56996  832 
lemma nn_integral_cong: 
833 
"(\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v" 

834 
by (auto intro: nn_integral_cong_AE) 

40859  835 

56996  836 
lemma nn_integral_cong_strong: 
837 
"M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N N v" 

838 
by (auto intro: nn_integral_cong) 

56993
e5366291d6aa
introduce Bochner integral: generalizes Lebesgue integral from realvalued function to functions on realnormed vector spaces
hoelzl
parents:
56949
diff
changeset

839 

56996  840 
lemma nn_integral_eq_simple_integral: 
841 
assumes f: "simple_function M f" "\<And>x. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f" 

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

842 
proof  
46731  843 
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

844 
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

845 
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

846 
by (auto simp: fun_eq_iff max_def split: split_indicator) 
56996  847 
have "integral\<^sup>N M ?f \<le> integral\<^sup>S M ?f" using f' 
848 
by (force intro!: SUP_least simple_integral_mono simp: le_fun_def nn_integral_def) 

849 
moreover have "integral\<^sup>S M ?f \<le> integral\<^sup>N M ?f" 

850 
unfolding nn_integral_def 

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

851 
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

852 
ultimately show ?thesis 
56996  853 
by (simp cong: nn_integral_cong simple_integral_cong) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

855 

56996  856 
lemma nn_integral_eq_simple_integral_AE: 
857 
assumes f: "simple_function M f" "AE x in M. 0 \<le> f x" shows "integral\<^sup>N M f = integral\<^sup>S M f" 

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

858 
proof  
47694  859 
have "AE x in M. f x = max 0 (f x)" using f by (auto split: split_max) 
56996  860 
with f have "integral\<^sup>N M f = integral\<^sup>S M (\<lambda>x. max 0 (f x))" 
861 
by (simp cong: nn_integral_cong_AE simple_integral_cong_AE 

862 
add: nn_integral_eq_simple_integral) 

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

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

864 
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

865 
qed 
40873  866 

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

868 
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

869 
and u: "simple_function M u" "u \<le> (SUP i. f i)" "u`space M \<subseteq> {0..<\<infinity>}" 
56996  870 
shows "integral\<^sup>S M u \<le> (SUP i. integral\<^sup>N M (f i))" (is "_ \<le> ?S") 
43920  871 
proof (rule ereal_le_mult_one_interval) 
56996  872 
have "0 \<le> (SUP i. integral\<^sup>N M (f i))" 
873 
using f(3) by (auto intro!: SUP_upper2 nn_integral_nonneg) 

874 
then show "(SUP i. integral\<^sup>N M (f i)) \<noteq> \<infinity>" by auto 

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

875 
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

876 
using u(3) by auto 
43920  877 
fix a :: ereal assume "0 < a" "a < 1" 
38656  878 
hence "a \<noteq> 0" by auto 
46731  879 
let ?B = "\<lambda>i. {x \<in> space M. a * u x \<le> f i x}" 
38656  880 
have B: "\<And>i. ?B i \<in> sets M" 
56949  881 
using f `simple_function M u`[THEN borel_measurable_simple_function] by auto 
38656  882 

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

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

886 
proof safe 

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

888 
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

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

892 
note B_mono = this 

35582  893 

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

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

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

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

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

900 
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

901 
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

902 
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

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

904 
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

905 
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

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

907 
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

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

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

910 
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

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

914 
finally obtain i where "a * u x < f i x" unfolding SUP_def 
56166  915 
by (auto simp add: less_SUP_iff) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

916 
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

917 
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

918 
qed 
40859  919 
qed 
47694  920 
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

921 
qed 
38656  922 

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

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

924 
unfolding simple_integral_indicator[OF B `simple_function M u`] 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

925 
proof (subst SUP_ereal_setsum, safe) 
38656  926 
fix x n assume "x \<in> space M" 
47694  927 
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)" 
928 
using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff) 

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

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

931 
using measure_conv u_range B_u unfolding simple_integral_def 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

932 
by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric]) 
38656  933 
qed 
934 
moreover 

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

935 
have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S" 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

936 
apply (subst SUP_ereal_cmult [symmetric]) 
38705  937 
proof (safe intro!: SUP_mono bexI) 
38656  938 
fix i 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

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

940 
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

941 
by (subst simple_integral_mult) (auto split: split_indicator) 
56996  942 
also have "\<dots> \<le> integral\<^sup>N M (f i)" 
38656  943 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

944 
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

945 
show ?thesis using f(3) * u_range `0 < a` 
56996  946 
by (subst nn_integral_eq_simple_integral[symmetric]) 
947 
(auto intro!: nn_integral_mono split: split_indicator) 

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

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

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

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

955 
ultimately show "a * integral\<^sup>S M u \<le> ?S" by simp 
35582  956 
qed 
957 

56996  958 
lemma incseq_nn_integral: 
959 
assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))" 

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

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

961 
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

962 
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

963 
then show ?thesis 
56996  964 
by (auto intro!: incseq_SucI nn_integral_mono) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

966 

35582  967 
text {* BeppoLevi monotone convergence theorem *} 
56996  968 
lemma nn_integral_monotone_convergence_SUP: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

969 
assumes f: "incseq f" "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x" 
56996  970 
shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

971 
proof (rule antisym) 
56996  972 
show "(SUP j. integral\<^sup>N M (f j)) \<le> (\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M)" 
973 
by (auto intro!: SUP_least SUP_upper nn_integral_mono) 

38656  974 
next 
56996  975 
show "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^sup>N M (f j))" 
976 
unfolding nn_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

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

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

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

980 
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

981 
using f by (auto intro!: SUP_upper2) 
56996  982 
with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>N M (f j))" 
983 
by (intro nn_integral_SUP_approx[OF f g _ g']) 

46884  984 
(auto simp: le_fun_def max_def) 
35582  985 
qed 
986 
qed 

987 

56996  988 
lemma nn_integral_monotone_convergence_SUP_AE: 
47694  989 
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" 
56996  990 
shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" 
40859  991 
proof  
47694  992 
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

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

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

997 
then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)" 
56996  998 
by (auto intro!: nn_integral_cong_AE) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

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

1001 
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

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

1003 
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

1004 
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

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

1007 
also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))" 
56996  1008 
using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

1011 

56996  1012 
lemma nn_integral_monotone_convergence_SUP_AE_incseq: 
47694  1013 
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" 
56996  1014 
shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1015 
using f[unfolded incseq_Suc_iff le_fun_def] 
56996  1016 
by (intro nn_integral_monotone_convergence_SUP_AE[OF _ borel]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

1018 

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

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

1021 
shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" 
56996  1022 
using assms unfolding nn_integral_monotone_convergence_SUP[OF f(1) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1023 
f(3)[THEN borel_measurable_simple_function] f(2)] 
56996  1024 
by (auto intro!: nn_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1025 

56996  1026 
lemma nn_integral_max_0: 
1027 
"(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>N M f" 

1028 
by (simp add: le_fun_def nn_integral_def) 

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

1029 

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

1031 
assumes "\<And>x. x \<in> space M \<Longrightarrow> f x \<le> 0 \<and> g x \<le> 0 \<or> f x = g x" 
56996  1032 
shows "integral\<^sup>N M f = integral\<^sup>N M g" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1033 
proof  
56996  1034 
have "integral\<^sup>N M (\<lambda>x. max 0 (f x)) = integral\<^sup>N M (\<lambda>x. max 0 (g x))" 
1035 
proof (intro nn_integral_cong) 

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

1036 
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

1037 
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

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

1039 
qed 
56996  1040 
then show ?thesis by (simp add: nn_integral_max_0) 
40859  1041 
qed 
1042 

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

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

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

1047 
shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56213
diff
changeset

1048 
(is "SUPREMUM _ ?F = SUPREMUM _ ?G") 
38656  1049 
proof  
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1050 
have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" 
56996  1051 
using f by (rule nn_integral_monotone_convergence_simple) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1052 
also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)" 
56996  1053 
unfolding eq[THEN nn_integral_cong_AE] .. 
38656  1054 
also have "\<dots> = (SUP i. ?G i)" 
56996  1055 
using g by (rule nn_integral_monotone_convergence_simple[symmetric]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1056 
finally show ?thesis by simp 
38656  1057 
qed 
1058 

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

1060 
"0 \<le> c \<Longrightarrow> (\<integral>\<^sup>+ x. c \<partial>M) = c * (emeasure M) (space M)" 
56996  1061 
by (subst nn_integral_eq_simple_integral) auto 
38656  1062 

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

1064 
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

1065 
and g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x" 
56996  1066 
shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g" 
1067 
(is "integral\<^sup>N M ?L = _") 

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

1069 
from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u . 
56996  1070 
note u = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1071 
from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v . 
56996  1072 
note v = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this 
46731  1073 
let ?L' = "\<lambda>i x. a * u i x + v i x" 
38656  1074 

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

1075 
have "?L \<in> borel_measurable M" using assms by auto 
38656  1076 
from borel_measurable_implies_simple_function_sequence'[OF this] guess l . 
56996  1077 
note l = nn_integral_monotone_convergence_simple[OF this(2,5,1)] this 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

1078 

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

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

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

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

1083 
have pos: "\<And>i. 0 \<le> integral\<^sup>S M (u i)" "\<And>i. 0 \<le> integral\<^sup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^sup>S M (u i)" 
56996  1084 
using u v `0 \<le> a` by (auto simp: simple_integral_nonneg) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

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

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

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

1088 

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

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

1090 
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

1091 
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

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

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

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

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

1097 
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

1098 
using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x] 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

1099 
by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`]) 
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

1100 
(auto intro!: SUP_ereal_add 
56537  1101 
simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) } 
47694  1102 
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

1103 
unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2) 
56537  1104 
by (intro AE_I2) (auto split: split_max) 
38656  1105 
qed 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

1106 
also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))" 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56213
diff
changeset

1107 
using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51340
diff
changeset

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

1109 
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

1110 
unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric] 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

1111 
apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`]) 
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

1112 
apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) . 
56996  1113 
then show ?thesis by (simp add: nn_integral_max_0) 
38656  1114 
qed 
1115 

56996  1116 
lemma nn_integral_cmult: 
49775
970964690b3d
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs
hoelzl
parents:
47761
diff
changeset

1117 
assumes f: "f \<in> borel_measurable M" "0 \<le> c" 
56996  1118 
shows "(\<integral>\<^sup>+ x. c * f x \<partial>M) = c * integral\<^sup>N M f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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