author  huffman 
Fri, 02 Sep 2011 13:57:12 0700  
changeset 44666  8670a39d4420 
parent 43920  cedb5cb948fd 
child 44890  22f665a2e91c 
permissions  rwrr 
42067  1 
(* Title: HOL/Probability/Lebesgue_Measure.thy 
2 
Author: Johannes Hölzl, TU München 

3 
Author: Robert Himmelmann, TU München 

4 
*) 

5 

38656  6 
header {* Lebsegue measure *} 
42067  7 

38656  8 
theory Lebesgue_Measure 
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42067
diff
changeset

9 
imports Finite_Product_Measure 
38656  10 
begin 
11 

12 
subsection {* Standard Cubes *} 

13 

40859  14 
definition cube :: "nat \<Rightarrow> 'a::ordered_euclidean_space set" where 
15 
"cube n \<equiv> {\<chi>\<chi> i.  real n .. \<chi>\<chi> i. real n}" 

16 

17 
lemma cube_closed[intro]: "closed (cube n)" 

18 
unfolding cube_def by auto 

19 

20 
lemma cube_subset[intro]: "n \<le> N \<Longrightarrow> cube n \<subseteq> cube N" 

21 
by (fastsimp simp: eucl_le[where 'a='a] cube_def) 

38656  22 

40859  23 
lemma cube_subset_iff: 
24 
"cube n \<subseteq> cube N \<longleftrightarrow> n \<le> N" 

25 
proof 

26 
assume subset: "cube n \<subseteq> (cube N::'a set)" 

27 
then have "((\<chi>\<chi> i. real n)::'a) \<in> cube N" 

28 
using DIM_positive[where 'a='a] 

29 
by (fastsimp simp: cube_def eucl_le[where 'a='a]) 

30 
then show "n \<le> N" 

31 
by (fastsimp simp: cube_def eucl_le[where 'a='a]) 

32 
next 

33 
assume "n \<le> N" then show "cube n \<subseteq> (cube N::'a set)" by (rule cube_subset) 

34 
qed 

38656  35 

36 
lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n" 

37 
unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta' 

38 
proof fix x::'a and i assume as:"x\<in>ball 0 (real n)" "i<DIM('a)" 

39 
thus " real n \<le> x $$ i" "real n \<ge> x $$ i" 

40 
using component_le_norm[of x i] by(auto simp: dist_norm) 

41 
qed 

42 

43 
lemma mem_big_cube: obtains n where "x \<in> cube n" 

44666  44 
proof from reals_Archimedean2[of "norm x"] guess n .. 
38656  45 
thus ?thesis applyapply(rule that[where n=n]) 
46 
apply(rule ball_subset_cube[unfolded subset_eq,rule_format]) 

47 
by (auto simp add:dist_norm) 

48 
qed 

49 

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

50 
lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

51 
unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto 
41654  52 

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

53 
subsection {* Lebesgue measure *} 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

54 

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

55 
definition lebesgue :: "'a::ordered_euclidean_space measure_space" where 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

56 
"lebesgue = \<lparr> space = UNIV, 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

57 
sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n}, 
43920  58 
measure = \<lambda>A. SUP n. ereal (integral (cube n) (indicator A)) \<rparr>" 
41661  59 

41654  60 
lemma space_lebesgue[simp]: "space lebesgue = UNIV" 
61 
unfolding lebesgue_def by simp 

62 

63 
lemma lebesgueD: "A \<in> sets lebesgue \<Longrightarrow> (indicator A :: _ \<Rightarrow> real) integrable_on cube n" 

64 
unfolding lebesgue_def by simp 

65 

66 
lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue" 

67 
unfolding lebesgue_def by simp 

68 

69 
lemma absolutely_integrable_on_indicator[simp]: 

70 
fixes A :: "'a::ordered_euclidean_space set" 

71 
shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow> 

72 
(indicator A :: _ \<Rightarrow> real) integrable_on X" 

73 
unfolding absolutely_integrable_on_def by simp 

74 

75 
lemma LIMSEQ_indicator_UN: 

76 
"(\<lambda>k. indicator (\<Union> i<k. A i) x) > (indicator (\<Union>i. A i) x :: real)" 

77 
proof cases 

78 
assume "\<exists>i. x \<in> A i" then guess i .. note i = this 

79 
then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1" 

80 
"(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def) 

81 
show ?thesis 

82 
apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto 

83 
qed (auto simp: indicator_def) 

38656  84 

41654  85 
lemma indicator_add: 
86 
"A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x" 

87 
unfolding indicator_def by auto 

38656  88 

41654  89 
interpretation lebesgue: sigma_algebra lebesgue 
90 
proof (intro sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI lebesgueI) 

91 
fix A n assume A: "A \<in> sets lebesgue" 

92 
have "indicator (space lebesgue  A) = (\<lambda>x. 1  indicator A x :: real)" 

93 
by (auto simp: fun_eq_iff indicator_def) 

94 
then show "(indicator (space lebesgue  A) :: _ \<Rightarrow> real) integrable_on cube n" 

95 
using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def) 

96 
next 

97 
fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n" 

98 
by (auto simp: cube_def indicator_def_raw) 

99 
next 

100 
fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue" 

101 
then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n" 

102 
by (auto dest: lebesgueD) 

103 
show "(indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n" (is "?g integrable_on _") 

104 
proof (intro dominated_convergence[where g="?g"] ballI) 

105 
fix k show "(indicator (\<Union>i<k. A i) :: _ \<Rightarrow> real) integrable_on cube n" 

106 
proof (induct k) 

107 
case (Suc k) 

108 
have *: "(\<Union> i<Suc k. A i) = (\<Union> i<k. A i) \<union> A k" 

109 
unfolding lessThan_Suc UN_insert by auto 

110 
have *: "(\<lambda>x. max (indicator (\<Union> i<k. A i) x) (indicator (A k) x) :: real) = 

111 
indicator (\<Union> i<Suc k. A i)" (is "(\<lambda>x. max (?f x) (?g x)) = _") 

112 
by (auto simp: fun_eq_iff * indicator_def) 

113 
show ?case 

114 
using absolutely_integrable_max[of ?f "cube n" ?g] A Suc by (simp add: *) 

115 
qed auto 

116 
qed (auto intro: LIMSEQ_indicator_UN simp: cube_def) 

117 
qed simp 

38656  118 

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

119 
interpretation lebesgue: measure_space lebesgue 
41654  120 
proof 
121 
have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff) 

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

122 
show "positive lebesgue (measure lebesgue)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

123 
proof (unfold positive_def, safe) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

124 
show "measure lebesgue {} = 0" by (simp add: integral_0 * lebesgue_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

125 
fix A assume "A \<in> sets lebesgue" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

126 
then show "0 \<le> measure lebesgue A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

131 
show "countably_additive lebesgue (measure lebesgue)" 
41654  132 
proof (intro countably_additive_def[THEN iffD2] allI impI) 
133 
fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A" 

134 
then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n" 

135 
by (auto dest: lebesgueD) 

136 
let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)" 

137 
let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)" 

138 
have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg) 

139 
assume "(\<Union>i. A i) \<in> sets lebesgue" 

140 
then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n" 

141 
by (auto dest: lebesgueD) 

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

142 
show "(\<Sum>n. measure lebesgue (A n)) = measure lebesgue (\<Union>i. A i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

143 
proof (simp add: lebesgue_def, subst suminf_SUP_eq, safe intro!: incseq_SucI) 
43920  144 
fix i n show "ereal (?m n i) \<le> ereal (?m (Suc n) i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

145 
using cube_subset[of n "Suc n"] by (auto intro!: integral_subset_le incseq_SucI) 
41654  146 
next 
43920  147 
fix i n show "0 \<le> ereal (?m n i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

148 
using rA unfolding lebesgue_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

150 
next 
43920  151 
show "(SUP n. \<Sum>i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))" 
152 
proof (intro arg_cong[where f="SUPR UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2]) 

41654  153 
fix n 
154 
have "\<And>m. (UNION {..<m} A) \<in> sets lebesgue" using rA by auto 

155 
from lebesgueD[OF this] 

156 
have "(\<lambda>m. ?M n {..< m}) > ?M n UNIV" 

157 
(is "(\<lambda>m. integral _ (?A m)) > ?I") 

158 
by (intro dominated_convergence(2)[where f="?A" and h="\<lambda>x. 1::real"]) 

159 
(auto intro: LIMSEQ_indicator_UN simp: cube_def) 

160 
moreover 

161 
{ fix m have *: "(\<Sum>x<m. ?m n x) = ?M n {..< m}" 

162 
proof (induct m) 

163 
case (Suc m) 

164 
have "(\<Union>i<m. A i) \<in> sets lebesgue" using rA by auto 

165 
then have "(indicator (\<Union>i<m. A i) :: _\<Rightarrow>real) integrable_on (cube n)" 

166 
by (auto dest!: lebesgueD) 

167 
moreover 

168 
have "(\<Union>i<m. A i) \<inter> A m = {}" 

169 
using rA(2)[unfolded disjoint_family_on_def, THEN bspec, of m] 

170 
by auto 

171 
then have "\<And>x. indicator (\<Union>i<Suc m. A i) x = 

172 
indicator (\<Union>i<m. A i) x + (indicator (A m) x :: real)" 

173 
by (auto simp: indicator_add lessThan_Suc ac_simps) 

174 
ultimately show ?case 

175 
using Suc A by (simp add: integral_add[symmetric]) 

176 
qed auto } 

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

177 
ultimately show "(\<lambda>m. \<Sum>x = 0..<m. ?m n x) > ?M n UNIV" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

178 
by (simp add: atLeast0LessThan) 
41654  179 
qed 
180 
qed 

181 
qed 

40859  182 
qed 
183 

41654  184 
lemma has_integral_interval_cube: 
185 
fixes a b :: "'a::ordered_euclidean_space" 

186 
shows "(indicator {a .. b} has_integral 

187 
content ({\<chi>\<chi> i. max ( real n) (a $$ i) .. \<chi>\<chi> i. min (real n) (b $$ i)} :: 'a set)) (cube n)" 

188 
(is "(?I has_integral content ?R) (cube n)") 

40859  189 
proof  
41654  190 
let "{?N .. ?P}" = ?R 
191 
have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R" 

192 
by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a]) 

193 
have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV" 

194 
unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp 

195 
also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R" 

196 
unfolding indicator_def_raw has_integral_restrict_univ .. 

197 
finally show ?thesis 

198 
using has_integral_const[of "1::real" "?N" "?P"] by simp 

40859  199 
qed 
38656  200 

41654  201 
lemma lebesgueI_borel[intro, simp]: 
202 
fixes s::"'a::ordered_euclidean_space set" 

40859  203 
assumes "s \<in> sets borel" shows "s \<in> sets lebesgue" 
41654  204 
proof  
205 
let ?S = "range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)})" 

206 
have *:"?S \<subseteq> sets lebesgue" 

207 
proof (safe intro!: lebesgueI) 

208 
fix n :: nat and a b :: 'a 

209 
let ?N = "\<chi>\<chi> i. max ( real n) (a $$ i)" 

210 
let ?P = "\<chi>\<chi> i. min (real n) (b $$ i)" 

211 
show "(indicator {a..b} :: 'a\<Rightarrow>real) integrable_on cube n" 

212 
unfolding integrable_on_def 

213 
using has_integral_interval_cube[of a b] by auto 

214 
qed 

40859  215 
have "s \<in> sigma_sets UNIV ?S" using assms 
216 
unfolding borel_eq_atLeastAtMost by (simp add: sigma_def) 

217 
thus ?thesis 

218 
using lebesgue.sigma_subset[of "\<lparr> space = UNIV, sets = ?S\<rparr>", simplified, OF *] 

219 
by (auto simp: sigma_def) 

38656  220 
qed 
221 

40859  222 
lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set" 
223 
assumes "negligible s" shows "s \<in> sets lebesgue" 

41654  224 
using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI) 
38656  225 

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

227 
fixes S :: "'a::ordered_euclidean_space set" assumes "negligible S" shows "lebesgue.\<mu> S = 0" 
40859  228 
proof  
41654  229 
have "\<And>n. integral (cube n) (indicator S :: 'a\<Rightarrow>real) = 0" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

230 
unfolding lebesgue_integral_def using 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

231 
by (intro integral_unique some1_equality ex_ex1I) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

232 
(auto simp: cube_def negligible_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

233 
then show ?thesis by (auto simp: lebesgue_def) 
40859  234 
qed 
235 

236 
lemma lmeasure_iff_LIMSEQ: 

237 
assumes "A \<in> sets lebesgue" "0 \<le> m" 

43920  238 
shows "lebesgue.\<mu> A = ereal m \<longleftrightarrow> (\<lambda>n. integral (cube n) (indicator A :: _ \<Rightarrow> real)) > 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

239 
proof (simp add: lebesgue_def, intro SUP_eq_LIMSEQ) 
41654  240 
show "mono (\<lambda>n. integral (cube n) (indicator A::_=>real))" 
241 
using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD) 

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

242 
qed 
38656  243 

41654  244 
lemma has_integral_indicator_UNIV: 
245 
fixes s A :: "'a::ordered_euclidean_space set" and x :: real 

246 
shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A" 

247 
proof  

248 
have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)" 

249 
by (auto simp: fun_eq_iff indicator_def) 

250 
then show ?thesis 

251 
unfolding has_integral_restrict_univ[where s=A, symmetric] by simp 

40859  252 
qed 
38656  253 

41654  254 
lemma 
255 
fixes s a :: "'a::ordered_euclidean_space set" 

256 
shows integral_indicator_UNIV: 

257 
"integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)" 

258 
and integrable_indicator_UNIV: 

259 
"(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A" 

260 
unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto 

261 

262 
lemma lmeasure_finite_has_integral: 

263 
fixes s :: "'a::ordered_euclidean_space set" 

43920  264 
assumes "s \<in> sets lebesgue" "lebesgue.\<mu> s = ereal m" "0 \<le> m" 
41654  265 
shows "(indicator s has_integral m) UNIV" 
266 
proof  

267 
let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real" 

268 
have **: "(?I s) integrable_on UNIV \<and> (\<lambda>k. integral UNIV (?I (s \<inter> cube k))) > integral UNIV (?I s)" 

269 
proof (intro monotone_convergence_increasing allI ballI) 

270 
have LIMSEQ: "(\<lambda>n. integral (cube n) (?I s)) > m" 

271 
using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1, 3)] . 

272 
{ fix n have "integral (cube n) (?I s) \<le> m" 

273 
using cube_subset assms 

274 
by (intro incseq_le[where L=m] LIMSEQ incseq_def[THEN iffD2] integral_subset_le allI impI) 

275 
(auto dest!: lebesgueD) } 

276 
moreover 

277 
{ fix n have "0 \<le> integral (cube n) (?I s)" 

278 
using assms by (auto dest!: lebesgueD intro!: integral_nonneg) } 

279 
ultimately 

280 
show "bounded {integral UNIV (?I (s \<inter> cube k)) k. True}" 

281 
unfolding bounded_def 

282 
apply (rule_tac exI[of _ 0]) 

283 
apply (rule_tac exI[of _ m]) 

284 
by (auto simp: dist_real_def integral_indicator_UNIV) 

285 
fix k show "?I (s \<inter> cube k) integrable_on UNIV" 

286 
unfolding integrable_indicator_UNIV using assms by (auto dest!: lebesgueD) 

287 
fix x show "?I (s \<inter> cube k) x \<le> ?I (s \<inter> cube (Suc k)) x" 

288 
using cube_subset[of k "Suc k"] by (auto simp: indicator_def) 

289 
next 

290 
fix x :: 'a 

291 
from mem_big_cube obtain k where k: "x \<in> cube k" . 

292 
{ fix n have "?I (s \<inter> cube (n + k)) x = ?I s x" 

293 
using k cube_subset[of k "n + k"] by (auto simp: indicator_def) } 

294 
note * = this 

295 
show "(\<lambda>k. ?I (s \<inter> cube k) x) > ?I s x" 

296 
by (rule LIMSEQ_offset[where k=k]) (auto simp: *) 

297 
qed 

298 
note ** = conjunctD2[OF this] 

299 
have m: "m = integral UNIV (?I s)" 

300 
apply (intro LIMSEQ_unique[OF _ **(2)]) 

301 
using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1,3)] integral_indicator_UNIV . 

302 
show ?thesis 

303 
unfolding m by (intro integrable_integral **) 

38656  304 
qed 
305 

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

306 
lemma lmeasure_finite_integrable: assumes s: "s \<in> sets lebesgue" and "lebesgue.\<mu> s \<noteq> \<infinity>" 
41654  307 
shows "(indicator s :: _ \<Rightarrow> real) integrable_on UNIV" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

308 
proof (cases "lebesgue.\<mu> s") 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

310 
with lmeasure_finite_has_integral[OF `s \<in> sets lebesgue` this] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

311 
lebesgue.positive_measure[OF s] 
41654  312 
show ?thesis unfolding integrable_on_def by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

313 
qed (insert assms lebesgue.positive_measure[OF s], auto) 
38656  314 

41654  315 
lemma has_integral_lebesgue: assumes "((indicator s :: _\<Rightarrow>real) has_integral m) UNIV" 
316 
shows "s \<in> sets lebesgue" 

317 
proof (intro lebesgueI) 

318 
let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real" 

319 
fix n show "(?I s) integrable_on cube n" unfolding cube_def 

320 
proof (intro integrable_on_subinterval) 

321 
show "(?I s) integrable_on UNIV" 

322 
unfolding integrable_on_def using assms by auto 

323 
qed auto 

38656  324 
qed 
325 

41654  326 
lemma has_integral_lmeasure: assumes "((indicator s :: _\<Rightarrow>real) has_integral m) UNIV" 
43920  327 
shows "lebesgue.\<mu> s = ereal m" 
41654  328 
proof (intro lmeasure_iff_LIMSEQ[THEN iffD2]) 
329 
let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real" 

330 
show "s \<in> sets lebesgue" using has_integral_lebesgue[OF assms] . 

331 
show "0 \<le> m" using assms by (rule has_integral_nonneg) auto 

332 
have "(\<lambda>n. integral UNIV (?I (s \<inter> cube n))) > integral UNIV (?I s)" 

333 
proof (intro dominated_convergence(2) ballI) 

334 
show "(?I s) integrable_on UNIV" unfolding integrable_on_def using assms by auto 

335 
fix n show "?I (s \<inter> cube n) integrable_on UNIV" 

336 
unfolding integrable_indicator_UNIV using `s \<in> sets lebesgue` by (auto dest: lebesgueD) 

337 
fix x show "norm (?I (s \<inter> cube n) x) \<le> ?I s x" by (auto simp: indicator_def) 

338 
next 

339 
fix x :: 'a 

340 
from mem_big_cube obtain k where k: "x \<in> cube k" . 

341 
{ fix n have "?I (s \<inter> cube (n + k)) x = ?I s x" 

342 
using k cube_subset[of k "n + k"] by (auto simp: indicator_def) } 

343 
note * = this 

344 
show "(\<lambda>k. ?I (s \<inter> cube k) x) > ?I s x" 

345 
by (rule LIMSEQ_offset[where k=k]) (auto simp: *) 

346 
qed 

347 
then show "(\<lambda>n. integral (cube n) (?I s)) > m" 

348 
unfolding integral_unique[OF assms] integral_indicator_UNIV by simp 

349 
qed 

350 

351 
lemma has_integral_iff_lmeasure: 

43920  352 
"(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> lebesgue.\<mu> A = ereal m)" 
40859  353 
proof 
41654  354 
assume "(indicator A has_integral m) UNIV" 
355 
with has_integral_lmeasure[OF this] has_integral_lebesgue[OF this] 

43920  356 
show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lebesgue.\<mu> A = ereal m" 
41654  357 
by (auto intro: has_integral_nonneg) 
40859  358 
next 
43920  359 
assume "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lebesgue.\<mu> A = ereal m" 
41654  360 
then show "(indicator A has_integral m) UNIV" by (intro lmeasure_finite_has_integral) auto 
38656  361 
qed 
362 

41654  363 
lemma lmeasure_eq_integral: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" 
43920  364 
shows "lebesgue.\<mu> s = ereal (integral UNIV (indicator s))" 
41654  365 
using assms unfolding integrable_on_def 
366 
proof safe 

367 
fix y :: real assume "(indicator s has_integral y) UNIV" 

368 
from this[unfolded has_integral_iff_lmeasure] integral_unique[OF this] 

43920  369 
show "lebesgue.\<mu> s = ereal (integral UNIV (indicator s))" by simp 
40859  370 
qed 
38656  371 

372 
lemma lebesgue_simple_function_indicator: 

43920  373 
fixes f::"'a::ordered_euclidean_space \<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

374 
assumes f:"simple_function lebesgue f" 
38656  375 
shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f ` {y}) 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

376 
by (rule, subst lebesgue.simple_function_indicator_representation[OF f]) auto 
38656  377 

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

379 
"(indicator s::_\<Rightarrow>real) integrable_on UNIV \<Longrightarrow> integral UNIV (indicator s) = real (lebesgue.\<mu> s)" 
41654  380 
by (subst lmeasure_eq_integral) (auto intro!: integral_nonneg) 
38656  381 

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

382 
lemma lmeasure_finite: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" shows "lebesgue.\<mu> s \<noteq> \<infinity>" 
41654  383 
using lmeasure_eq_integral[OF assms] by auto 
38656  384 

40859  385 
lemma negligible_iff_lebesgue_null_sets: 
386 
"negligible A \<longleftrightarrow> A \<in> lebesgue.null_sets" 

387 
proof 

388 
assume "negligible A" 

389 
from this[THEN lebesgueI_negligible] this[THEN lmeasure_eq_0] 

390 
show "A \<in> lebesgue.null_sets" by auto 

391 
next 

392 
assume A: "A \<in> lebesgue.null_sets" 

41654  393 
then have *:"((indicator A) has_integral (0::real)) UNIV" using lmeasure_finite_has_integral[of A] by auto 
394 
show "negligible A" unfolding negligible_def 

395 
proof (intro allI) 

396 
fix a b :: 'a 

397 
have integrable: "(indicator A :: _\<Rightarrow>real) integrable_on {a..b}" 

398 
by (intro integrable_on_subinterval has_integral_integrable) (auto intro: *) 

399 
then have "integral {a..b} (indicator A) \<le> (integral UNIV (indicator A) :: real)" 

400 
using * by (auto intro!: integral_subset_le has_integral_integrable) 

401 
moreover have "(0::real) \<le> integral {a..b} (indicator A)" 

402 
using integrable by (auto intro!: integral_nonneg) 

403 
ultimately have "integral {a..b} (indicator A) = (0::real)" 

404 
using integral_unique[OF *] by auto 

405 
then show "(indicator A has_integral (0::real)) {a..b}" 

406 
using integrable_integral[OF integrable] by simp 

407 
qed 

408 
qed 

409 

410 
lemma integral_const[simp]: 

411 
fixes a b :: "'a::ordered_euclidean_space" 

412 
shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c" 

413 
by (rule integral_unique) (rule has_integral_const) 

414 

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

415 
lemma lmeasure_UNIV[intro]: "lebesgue.\<mu> (UNIV::'a::ordered_euclidean_space set) = \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

416 
proof (simp add: lebesgue_def, intro SUP_PInfty bexI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

418 
have "indicator UNIV = (\<lambda>x::'a. 1 :: real)" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

420 
{ have "real n \<le> (2 * real n) ^ DIM('a)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

424 
case (Suc n') 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

425 
have "real n \<le> (2 * real n)^1" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

426 
also have "(2 * real n)^1 \<le> (2 * real n) ^ DIM('a)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

427 
using Suc DIM_positive[where 'a='a] by (intro power_increasing) (auto simp: real_of_nat_Suc) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

429 
qed } 
43920  430 
ultimately show "ereal (real n) \<le> ereal (integral (cube n) (indicator UNIV::'a\<Rightarrow>real))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

431 
using integral_const DIM_positive[where 'a='a] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

433 
qed simp 
40859  434 

435 
lemma 

436 
fixes a b ::"'a::ordered_euclidean_space" 

43920  437 
shows lmeasure_atLeastAtMost[simp]: "lebesgue.\<mu> {a..b} = ereal (content {a..b})" 
41654  438 
proof  
439 
have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV" 

440 
unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw) 

441 
from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV 

442 
by (simp add: indicator_def_raw) 

40859  443 
qed 
444 

445 
lemma atLeastAtMost_singleton_euclidean[simp]: 

446 
fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}" 

447 
by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a]) 

448 

449 
lemma content_singleton[simp]: "content {a} = 0" 

450 
proof  

451 
have "content {a .. a} = 0" 

452 
by (subst content_closed_interval) auto 

453 
then show ?thesis by simp 

454 
qed 

455 

456 
lemma lmeasure_singleton[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

457 
fixes a :: "'a::ordered_euclidean_space" shows "lebesgue.\<mu> {a} = 0" 
41654  458 
using lmeasure_atLeastAtMost[of a a] by simp 
40859  459 

460 
declare content_real[simp] 

461 

462 
lemma 

463 
fixes a b :: real 

464 
shows lmeasure_real_greaterThanAtMost[simp]: 

43920  465 
"lebesgue.\<mu> {a <.. b} = ereal (if a \<le> b then b  a else 0)" 
40859  466 
proof cases 
467 
assume "a < b" 

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

468 
then have "lebesgue.\<mu> {a <.. b} = lebesgue.\<mu> {a .. b}  lebesgue.\<mu> {a}" 
41654  469 
by (subst lebesgue.measure_Diff[symmetric]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

470 
(auto intro!: arg_cong[where f=lebesgue.\<mu>]) 
40859  471 
then show ?thesis by auto 
472 
qed auto 

473 

474 
lemma 

475 
fixes a b :: real 

476 
shows lmeasure_real_atLeastLessThan[simp]: 

43920  477 
"lebesgue.\<mu> {a ..< b} = ereal (if a \<le> b then b  a else 0)" 
40859  478 
proof cases 
479 
assume "a < b" 

41689
3e39b0e730d6
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 
then have "lebesgue.\<mu> {a ..< b} = lebesgue.\<mu> {a .. b}  lebesgue.\<mu> {b}" 
41654  481 
by (subst lebesgue.measure_Diff[symmetric]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

482 
(auto intro!: arg_cong[where f=lebesgue.\<mu>]) 
41654  483 
then show ?thesis by auto 
484 
qed auto 

485 

486 
lemma 

487 
fixes a b :: real 

488 
shows lmeasure_real_greaterThanLessThan[simp]: 

43920  489 
"lebesgue.\<mu> {a <..< b} = ereal (if a \<le> b then b  a else 0)" 
41654  490 
proof cases 
491 
assume "a < b" 

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

492 
then have "lebesgue.\<mu> {a <..< b} = lebesgue.\<mu> {a <.. b}  lebesgue.\<mu> {b}" 
41654  493 
by (subst lebesgue.measure_Diff[symmetric]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

494 
(auto intro!: arg_cong[where f=lebesgue.\<mu>]) 
40859  495 
then show ?thesis by auto 
496 
qed auto 

497 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

498 
subsection {* LebesgueBorel measure *} 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

499 

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

500 
definition "lborel = lebesgue \<lparr> sets := sets borel \<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

501 

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

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

503 
shows space_lborel[simp]: "space lborel = UNIV" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

504 
and sets_lborel[simp]: "sets lborel = sets borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

505 
and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

506 
and measurable_lborel[simp]: "measurable lborel = measurable borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

507 
by (simp_all add: measurable_def_raw lborel_def) 
40859  508 

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

509 
interpretation lborel: measure_space "lborel :: ('a::ordered_euclidean_space) measure_space" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

510 
where "space lborel = UNIV" 
3e39b0e730d6
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 
and "sets lborel = sets borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

512 
and "measure lborel = lebesgue.\<mu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

513 
and "measurable lborel = measurable borel" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

514 
proof (rule lebesgue.measure_space_subalgebra) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

515 
have "sigma_algebra (lborel::'a measure_space) \<longleftrightarrow> sigma_algebra (borel::'a algebra)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

517 
then show "sigma_algebra (lborel::'a measure_space)" by simp default 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

518 
qed auto 
40859  519 

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

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

521 
where "space lborel = UNIV" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

522 
and "sets lborel = sets borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

523 
and "measure lborel = lebesgue.\<mu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

524 
and "measurable lborel = measurable borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

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

527 
proof (default, intro conjI exI[of _ "\<lambda>n. cube n"]) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

528 
show "range cube \<subseteq> sets lborel" by (auto intro: borel_closed) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

529 
{ fix x have "\<exists>n. x\<in>cube n" using mem_big_cube by auto } 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

530 
thus "(\<Union>i. cube i) = space lborel" by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

531 
show "\<forall>i. measure lborel (cube i) \<noteq> \<infinity>" by (simp add: cube_def) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

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

534 

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

535 
interpretation lebesgue: sigma_finite_measure lebesgue 
40859  536 
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

537 
from lborel.sigma_finite guess A .. 
40859  538 
moreover then have "range A \<subseteq> sets lebesgue" using lebesgueI_borel by blast 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

539 
ultimately show "\<exists>A::nat \<Rightarrow> 'b set. range A \<subseteq> sets lebesgue \<and> (\<Union>i. A i) = space lebesgue \<and> (\<forall>i. lebesgue.\<mu> (A i) \<noteq> \<infinity>)" 
40859  540 
by auto 
541 
qed 

542 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

543 
subsection {* Lebesgue integrable implies Gauge integrable *} 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

544 

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

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

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

547 
assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

548 
shows "((\<lambda>x. c * f x) has_integral c * x) A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

551 
from has_integral_cmul[OF assms[OF this], of c] show ?thesis 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

554 

40859  555 
lemma simple_function_has_integral: 
43920  556 
fixes f::"'a::ordered_euclidean_space \<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

557 
assumes f:"simple_function lebesgue f" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

558 
and f':"range f \<subseteq> {0..<\<infinity>}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

559 
and om:"\<And>x. x \<in> range f \<Longrightarrow> lebesgue.\<mu> (f ` {x} \<inter> UNIV) = \<infinity> \<Longrightarrow> x = 0" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

560 
shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

562 
proof (subst lebesgue_simple_function_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

563 
let "?M x" = "lebesgue.\<mu> (f ` {x} \<inter> UNIV)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

564 
let "?F x" = "indicator (f ` {x})" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

565 
{ fix x y assume "y \<in> range f" 
43920  566 
from subsetD[OF f' this] have "y * ?F y x = ereal (real y * ?F y x)" 
567 
by (cases rule: ereal2_cases[of y "?F y x"]) 

568 
(auto simp: indicator_def one_ereal_def split: split_if_asm) } 

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

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

570 
{ fix x assume x: "x\<in>range f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

571 
have "x * ?M x = real x * real (?M x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

573 
assume "x \<noteq> 0" with om[OF x] have "?M x \<noteq> \<infinity>" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

574 
with subsetD[OF f' x] f[THEN lebesgue.simple_functionD(2)] show ?thesis 
43920  575 
by (cases rule: ereal2_cases[of x "?M x"]) auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

578 
have "((\<lambda>x. real (\<Sum>y\<in>range f. y * ?F y x)) has_integral real (\<Sum>x\<in>range f. x * ?M x)) UNIV \<longleftrightarrow> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

579 
((\<lambda>x. \<Sum>y\<in>range f. real y * ?F y x) has_integral (\<Sum>x\<in>range f. real x * real (?M x))) UNIV" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

581 
also have \<dots> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

582 
proof (intro has_integral_setsum has_integral_cmult_real lmeasure_finite_has_integral 
43920  583 
real_of_ereal_pos lebesgue.positive_measure ballI) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

584 
show *: "finite (range f)" "\<And>y. f ` {y} \<in> sets lebesgue" "\<And>y. f ` {y} \<inter> UNIV \<in> sets lebesgue" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

585 
using lebesgue.simple_functionD[OF f] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

586 
fix y assume "real y \<noteq> 0" "y \<in> range f" 
43920  587 
with * om[OF this(2)] show "lebesgue.\<mu> (f ` {y}) = ereal (real (?M y))" 
588 
by (auto simp: ereal_real) 

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

590 
finally show "((\<lambda>x. real (\<Sum>y\<in>range f. y * ?F y x)) has_integral real (\<Sum>x\<in>range f. x * ?M x)) UNIV" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

591 
qed fact 
40859  592 

593 
lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s" 

594 
unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI) 

595 
using assms by auto 

596 

597 
lemma simple_function_has_integral': 

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

599 
assumes f: "simple_function lebesgue f" "\<And>x. 0 \<le> f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

600 
and i: "integral\<^isup>S lebesgue f \<noteq> \<infinity>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

601 
shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>S lebesgue f))) UNIV" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

603 
let ?f = "\<lambda>x. if x \<in> f ` {\<infinity>} then 0 else f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

604 
note f(1)[THEN lebesgue.simple_functionD(2)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

605 
then have [simp, intro]: "\<And>X. f ` X \<in> sets lebesgue" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

606 
have f': "simple_function lebesgue ?f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

607 
using f by (intro lebesgue.simple_function_If_set) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

608 
have rng: "range ?f \<subseteq> {0..<\<infinity>}" using f by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

609 
have "AE x in lebesgue. f x = ?f x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

610 
using lebesgue.simple_integral_PInf[OF f i] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

611 
by (intro lebesgue.AE_I[where N="f ` {\<infinity>} \<inter> space lebesgue"]) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

612 
from f(1) f' this have eq: "integral\<^isup>S lebesgue f = integral\<^isup>S lebesgue ?f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

613 
by (rule lebesgue.simple_integral_cong_AE) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

614 
have real_eq: "\<And>x. real (f x) = real (?f x)" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

615 

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

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

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

618 
proof (rule simple_function_has_integral[OF f' rng]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

619 
fix x assume x: "x \<in> range ?f" and inf: "lebesgue.\<mu> (?f ` {x} \<inter> UNIV) = \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

620 
have "x * lebesgue.\<mu> (?f ` {x} \<inter> UNIV) = (\<integral>\<^isup>S y. x * indicator (?f ` {x}) y \<partial>lebesgue)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

621 
using f'[THEN lebesgue.simple_functionD(2)] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

623 
also have "\<dots> \<le> integral\<^isup>S lebesgue f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

624 
using f'[THEN lebesgue.simple_functionD(2)] f 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

625 
by (intro lebesgue.simple_integral_mono lebesgue.simple_function_mult lebesgue.simple_function_indicator) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

627 
finally show "x = 0" unfolding inf using i subsetD[OF rng x] by (auto split: split_if_asm) 
40859  628 
qed 
629 
qed 

630 

631 
lemma positive_integral_has_integral: 

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

633 
assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

634 
shows "((\<lambda>x. real (f x)) has_integral (real (integral\<^isup>P lebesgue f))) UNIV" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

637 
guess u . note u = this 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

639 
using u(4) f(2)[THEN subsetD] by (auto split: split_max) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

640 
let "?u i x" = "real (u i x)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

641 
note u_eq = lebesgue.positive_integral_eq_simple_integral[OF u(1,5), symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

644 
also have "integral\<^isup>P lebesgue (u i) \<le> (\<integral>\<^isup>+x. max 0 (f x) \<partial>lebesgue)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

645 
by (intro lebesgue.positive_integral_mono) (auto intro: le_SUPI simp: u(4)[symmetric]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

646 
finally have "integral\<^isup>S lebesgue (u i) \<noteq> \<infinity>" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

647 
unfolding positive_integral_max_0 using f by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

649 
then have u_int: "\<And>i. (?u i has_integral real (integral\<^isup>S lebesgue (u i))) UNIV" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

650 
by (rule simple_function_has_integral'[OF u(1,5)]) 
43920  651 
have "\<forall>x. \<exists>r\<ge>0. f x = ereal r" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

653 
fix x from f(2) have "0 \<le> f x" "f x \<noteq> \<infinity>" by (auto simp: subset_eq) 
43920  654 
then show "\<exists>r\<ge>0. f x = ereal r" by (cases "f x") auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

655 
qed 
43920  656 
from choice[OF this] obtain f' where f': "f = (\<lambda>x. ereal (f' x))" "\<And>x. 0 \<le> f' x" by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

657 

43920  658 
have "\<forall>i. \<exists>r. \<forall>x. 0 \<le> r x \<and> u i x = ereal (r x)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

659 
proof 
43920  660 
fix i show "\<exists>r. \<forall>x. 0 \<le> r x \<and> u i x = ereal (r x)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

662 
fix i x have "u i x \<noteq> \<infinity>" using u(3)[of i] by (auto simp: image_iff) metis 
43920  663 
then show "\<exists>r\<ge>0. u i x = ereal r" using u(5)[of i x] by (cases "u i x") auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

666 
from choice[OF this] obtain u' where 
43920  667 
u': "u = (\<lambda>i x. ereal (u' i x))" "\<And>i x. 0 \<le> u' i x" by (auto simp: fun_eq_iff) 
40859  668 

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

669 
have convergent: "f' integrable_on UNIV \<and> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

670 
(\<lambda>k. integral UNIV (u' k)) > integral UNIV f'" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

671 
proof (intro monotone_convergence_increasing allI ballI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

672 
show int: "\<And>k. (u' k) integrable_on UNIV" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

673 
using u_int unfolding integrable_on_def u' by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

674 
show "\<And>k x. u' k x \<le> u' (Suc k) x" using u(2,3,5) 
43920  675 
by (auto simp: incseq_Suc_iff le_fun_def image_iff u' intro!: real_of_ereal_positive_mono) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

676 
show "\<And>x. (\<lambda>k. u' k x) > f' x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

677 
using SUP_eq u(2) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

678 
by (intro SUP_eq_LIMSEQ[THEN iffD1]) (auto simp: u' f' incseq_mono incseq_Suc_iff le_fun_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

679 
show "bounded {integral UNIV (u' k)k. True}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

682 
have "\<bar>integral UNIV (u' k)\<bar> = integral UNIV (u' k)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

683 
by (intro abs_of_nonneg integral_nonneg int ballI u') 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

684 
also have "\<dots> = real (integral\<^isup>S lebesgue (u k))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

685 
using u_int[THEN integral_unique] by (simp add: u') 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

686 
also have "\<dots> = real (integral\<^isup>P lebesgue (u k))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

687 
using lebesgue.positive_integral_eq_simple_integral[OF u(1,5)] by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

688 
also have "\<dots> \<le> real (integral\<^isup>P lebesgue f)" using f 
43920  689 
by (auto intro!: real_of_ereal_positive_mono lebesgue.positive_integral_positive 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

690 
lebesgue.positive_integral_mono le_SUPI simp: SUP_eq[symmetric]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

691 
finally show "\<bar>integral UNIV (u' k)\<bar> \<le> real (integral\<^isup>P lebesgue f)" . 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

693 
qed 
40859  694 

43920  695 
have "integral\<^isup>P lebesgue f = ereal (integral UNIV f')" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

696 
proof (rule tendsto_unique[OF trivial_limit_sequentially]) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

697 
have "(\<lambda>i. integral\<^isup>S lebesgue (u i)) > (SUP i. integral\<^isup>P lebesgue (u i))" 
43920  698 
unfolding u_eq by (intro LIMSEQ_ereal_SUPR lebesgue.incseq_positive_integral u) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

699 
also note lebesgue.positive_integral_monotone_convergence_SUP 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

700 
[OF u(2) lebesgue.borel_measurable_simple_function[OF u(1)] u(5), symmetric] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

701 
finally show "(\<lambda>k. integral\<^isup>S lebesgue (u k)) > integral\<^isup>P lebesgue f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

703 

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

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

705 
have "0 \<le> integral\<^isup>S lebesgue (u k)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

706 
using u by (auto intro!: lebesgue.simple_integral_positive) 
43920  707 
then have "integral\<^isup>S lebesgue (u k) = ereal (real (integral\<^isup>S lebesgue (u k)))" 
708 
using u_fin by (auto simp: ereal_real) } 

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

709 
note * = this 
43920  710 
show "(\<lambda>k. integral\<^isup>S lebesgue (u k)) > ereal (integral UNIV f')" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

711 
using convergent using u_int[THEN integral_unique, symmetric] 
43920  712 
by (subst *) (simp add: lim_ereal u') 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

714 
then show ?thesis using convergent by (simp add: f' integrable_integral) 
40859  715 
qed 
716 

717 
lemma lebesgue_integral_has_integral: 

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

718 
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

720 
shows "(f has_integral (integral\<^isup>L lebesgue f)) UNIV" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

721 
proof  
43920  722 
let ?n = "\<lambda>x. real (ereal (max 0 ( f x)))" and ?p = "\<lambda>x. real (ereal (max 0 (f x)))" 
723 
have *: "f = (\<lambda>x. ?p x  ?n x)" by (auto simp del: ereal_max) 

724 
{ fix f have "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) = (\<integral>\<^isup>+ x. ereal (max 0 (f x)) \<partial>lebesgue)" 

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

725 
by (intro lebesgue.positive_integral_cong_pos) (auto split: split_max) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

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

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

729 
apply (subst *) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

730 
apply (rule has_integral_sub) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

731 
unfolding eq[of f] eq[of "\<lambda>x.  f x"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

733 
using integrableD[OF f] 
43920  734 
by (auto simp: zero_ereal_def[symmetric] positive_integral_max_0 split: split_max 
735 
intro!: lebesgue.measurable_If lebesgue.borel_measurable_ereal) 

40859  736 
qed 
737 

41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

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

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

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

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

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

743 
by (auto intro!: lebesgue.positive_integral_subalgebra[symmetric]) default 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

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

745 
qed 
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

746 

2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

747 
lemma lebesgue_integral_eq_borel: 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

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

749 
shows "integrable lebesgue f \<longleftrightarrow> integrable lborel f" (is ?P) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

750 
and "integral\<^isup>L lebesgue f = integral\<^isup>L lborel f" (is ?I) 
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

751 
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

752 
have *: "sigma_algebra lborel" by default 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

753 
have "sets lborel \<subseteq> sets lebesgue" by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

754 
from lebesgue.integral_subalgebra[of f lborel, OF _ this _ _ *] assms 
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

755 
show ?P ?I by auto 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

756 
qed 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

757 

2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

758 
lemma borel_integral_has_integral: 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

759 
fixes f::"'a::ordered_euclidean_space => real" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

760 
assumes f:"integrable lborel 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

761 
shows "(f has_integral (integral\<^isup>L lborel f)) UNIV" 
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

762 
proof  
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

763 
have borel: "f \<in> borel_measurable borel" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

764 
using f unfolding integrable_def by auto 
41546
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

765 
from f show ?thesis 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

766 
using lebesgue_integral_has_integral[of f] 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

767 
unfolding lebesgue_integral_eq_borel[OF borel] by simp 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

768 
qed 
2a12c23b7a34
integral on lebesgue measure is extension of integral on borel measure
hoelzl
parents:
41097
diff
changeset

769 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

770 
subsection {* Equivalence between product spaces and euclidean spaces *} 
40859  771 

772 
definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where 

773 
"e2p x = (\<lambda>i\<in>{..<DIM('a)}. x$$i)" 

774 

775 
definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where 

776 
"p2e x = (\<chi>\<chi> i. x i)" 

777 

41095  778 
lemma e2p_p2e[simp]: 
779 
"x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x" 

780 
by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def) 

40859  781 

41095  782 
lemma p2e_e2p[simp]: 
783 
"p2e (e2p x) = (x::'a::ordered_euclidean_space)" 

784 
by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def) 

40859  785 

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

786 
interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure_space" 
40859  787 
by default 
788 

41831  789 
interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure_space" "{..<n}" for n :: nat 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

790 
where "space lborel = UNIV" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

791 
and "sets lborel = sets borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

792 
and "measure lborel = lebesgue.\<mu>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

793 
and "measurable lborel = measurable borel" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

794 
proof  
41831  795 
show "finite_product_sigma_finite (\<lambda>x. lborel::real measure_space) {..<n}" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

797 
qed simp_all 
40859  798 

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

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

800 
assumes [intro]: "finite 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

801 
shows "sets (\<Pi>\<^isub>M i\<in>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

802 
\<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>) = 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

803 
sets (\<Pi>\<^isub>M i\<in>I. lborel)" (is "sets ?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

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

805 
have "sets ?G = sets (\<Pi>\<^isub>M i\<in>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

806 
sigma \<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

807 
by (subst sigma_product_algebra_sigma_eq[of I "\<lambda>_ i. {..<real i}" ]) 
44666  808 
(auto intro!: measurable_sigma_sigma incseq_SucI reals_Archimedean2 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

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

811 
unfolding lborel_def borel_eq_lessThan lebesgue_def sigma_def by simp 
40859  812 
qed 
813 

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

815 
"e2p \<in> measurable (borel::'a::ordered_euclidean_space algebra) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

816 
(\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space))" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

817 
(is "_ \<in> measurable ?E ?P") 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

819 
let ?B = "\<lparr> space = UNIV::real set, sets = range lessThan, measure = lebesgue.\<mu> \<rparr>" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

820 
let ?G = "product_algebra_generator {..<DIM('a)} (\<lambda>_. ?B)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

821 
have "e2p \<in> measurable ?E (sigma ?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

822 
proof (rule borel.measurable_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

823 
show "e2p \<in> space ?E \<rightarrow> space ?G" by (auto simp: e2p_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

824 
fix A assume "A \<in> sets ?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

825 
then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E 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

826 
and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

827 
by (auto elim!: product_algebraE simp: ) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

828 
then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

829 
from this[THEN bchoice] guess xs .. 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

830 
then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs 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

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

832 
have "e2p ` A = {..< (\<chi>\<chi> i. xs i) :: 'a}" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

833 
using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

834 
euclidean_eq[where 'a='a] eucl_less[where 'a='a]) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

835 
then show "e2p ` A \<inter> space ?E \<in> sets ?E" by simp 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

836 
qed (auto simp: product_algebra_generator_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

837 
with sets_product_borel[of "{..<DIM('a)}"] show ?thesis 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

839 
qed 
41661  840 

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

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

842 
"p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space)) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

843 
(borel :: 'a::ordered_euclidean_space algebra)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

844 
(is "p2e \<in> measurable ?P _") 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

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

846 
proof (intro lborel_space.measurable_sigma) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41661
diff
changeset

847 
let ?E = "\<lparr> space = UNIV :: 'a set, sets = range lessThan \<rparr>" 
41095  848 
show "p2e \<in> space ?P \<rightarrow> space ?E" by simp 
849 
fix A assume "A \<in> sets ?E" 

850 
then obtain x where "A = {..<x}" by auto 

851 
then have "p2e ` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x $$ i})" 

852 
using DIM_positive 

853 
by (auto simp: Pi_iff set_eq_iff p2e_def 

854 
euclidean_eq[where 'a='a] eucl_less[where 'a='a]) 

855 
then show "p2e ` A \<inter> space ?P \<in> sets ?P" by auto 

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

856 
qed simp 
41095  857 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

858 
lemma Int_stable_cuboids: 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

859 
fixes x::"'a::ordered_euclidean_space" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

860 
shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). {a..b})\<rparr>" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

861 
by (auto simp: inter_interval Int_stable_def) 
40859  862 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

863 
lemma lborel_eq_lborel_space: 
40859  864 
fixes A :: "('a::ordered_euclidean_space) set" 
865 
assumes "A \<in> sets borel" 

41831  866 
shows "lborel.\<mu> A = lborel_space.\<mu> DIM('a) (p2e ` A \<inter> (space (lborel_space.P DIM('a))))" 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

867 
(is "_ = measure ?P (?T A)") 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

868 
proof (rule measure_unique_Int_stable_vimage) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

869 
show "measure_space ?P" by default 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

870 
show "measure_space lborel" by default 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

871 

a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

872 
let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

873 
show "Int_stable ?E" using Int_stable_cuboids . 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

874 
show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

875 
show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI) 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

876 
{ fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastsimp } 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

877 
then show "(\<Union>i. cube i) = space ?E" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41831
diff
changeset

878 
{ fix i show "lborel.\<mu> (cube i) \<noteq> \<infinity>" unfolding cube_def by auto } 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

879 
show "A \<in> sets (sigma ?E)" "sets (sigma ?E) = sets lborel" "space ?E = space lborel" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

880 
using assms by (simp_all add: borel_eq_atLeastAtMost) 
40859  881 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

882 
show "p2e \<in> measurable ?P (lborel :: 'a measure_space)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

883 
using measurable_p2e unfolding measurable_def by simp 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

884 
{ fix X assume "X \<in> sets ?E" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

885 
then obtain a b where X[simp]: "X = {a .. b}" by auto 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

886 
have *: "?T X = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

887 
by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

888 
show "lborel.\<mu> X = measure ?P (?T X)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

889 
proof cases 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

890 
assume "X \<noteq> {}" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

891 
then have "a \<le> b" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

892 
by (simp add: interval_ne_empty eucl_le[where 'a='a]) 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

893 
then have "lborel.\<mu> X = (\<Prod>x<DIM('a). lborel.\<mu> {a $$ x .. b $$ x})" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

894 
by (auto simp: content_closed_interval eucl_le[where 'a='a] 
43920  895 
intro!: setprod_ereal[symmetric]) 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

896 
also have "\<dots> = measure ?P (?T X)" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

897 
unfolding * by (subst lborel_space.measure_times) auto 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

898 
finally show ?thesis . 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

899 
qed simp } 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

900 
qed 
40859  901 

41831  902 
lemma measure_preserving_p2e: 
903 
"p2e \<in> measure_preserving (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure_space)) 

904 
(lborel::'a::ordered_euclidean_space measure_space)" (is "_ \<in> measure_preserving ?P ?E") 

905 
proof 

906 
show "p2e \<in> measurable ?P ?E" 

907 
using measurable_p2e by (simp add: measurable_def) 

908 
fix A :: "'a set" assume "A \<in> sets lborel" 

909 
then show "lborel_space.\<mu> DIM('a) (p2e ` A \<inter> (space (lborel_space.P DIM('a)))) = lborel.\<mu> A" 

910 
by (intro lborel_eq_lborel_space[symmetric]) simp 

911 
qed 

912 

41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

913 
lemma lebesgue_eq_lborel_space_in_borel: 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

914 
fixes A :: "('a::ordered_euclidean_space) set" 
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

915 
assumes A: "A \<in> sets borel" 
41831  916 
shows "lebesgue.\<mu> A = lborel_space.\<mu> DIM('a) (p2e ` A \<inter> (space (lborel_space.P DIM('a))))" 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

917 
using lborel_eq_lborel_space[OF A] by simp 
40859  918 

919 
lemma borel_fubini_positiv_integral: 

43920  920 
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal" 
40859  921 
assumes f: "f \<in> borel_measurable borel" 
41831  922 
shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P DIM('a))" 
923 
proof (rule lborel_space.positive_integral_vimage[OF _ measure_preserving_p2e _]) 

924 
show "f \<in> borel_measurable lborel" 

925 
using f by (simp_all add: measurable_def) 

926 
qed default 

40859  927 

41704
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

928 
lemma borel_fubini_integrable: 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

929 
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

930 
shows "integrable lborel f \<longleftrightarrow> 
41831  931 
integrable (lborel_space.P DIM('a)) (\<lambda>x. f (p2e x))" 
41704
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

932 
(is "_ \<longleftrightarrow> integrable ?B ?f") 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

933 
proof 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

934 
assume "integrable lborel f" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

935 
moreover then have f: "f \<in> borel_measurable borel" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

936 
by auto 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

937 
moreover with measurable_p2e 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

938 
have "f \<circ> p2e \<in> borel_measurable ?B" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

939 
by (rule measurable_comp) 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

940 
ultimately show "integrable ?B ?f" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

941 
by (simp add: comp_def borel_fubini_positiv_integral integrable_def) 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

942 
next 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

943 
assume "integrable ?B ?f" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

944 
moreover then 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

945 
have "?f \<circ> e2p \<in> borel_measurable (borel::'a algebra)" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

946 
by (auto intro!: measurable_e2p measurable_comp) 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

947 
then have "f \<in> borel_measurable borel" 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

948 
by (simp cong: measurable_cong) 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

949 
ultimately show "integrable lborel f" 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

950 
by (simp add: borel_fubini_positiv_integral integrable_def) 
41704
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

951 
qed 
8c539202f854
add borel_fubini_integrable; remove unused bijectivity rules for measureable functions
hoelzl
parents:
41689
diff
changeset

952 

40859  953 
lemma borel_fubini: 
954 
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real" 

955 
assumes f: "f \<in> borel_measurable borel" 

41831  956 
shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P DIM('a))" 
41706
a207a858d1f6
prefer p2e before e2p; use measure_unique_Int_stable_vimage;
hoelzl
parents:
41704
diff
changeset

957 
using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def) 
38656  958 

42164  959 

960 
lemma Int_stable_atLeastAtMost: 

961 
"Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::'a::ordered_euclidean_space .. b}) \<rparr>" 

962 
proof (simp add: Int_stable_def image_iff, intro allI) 

963 
fix a1 b1 a2 b2 :: 'a 

964 
have "\<forall>i<DIM('a). \<exists>a b. {a1$$i..b1$$i} \<inter> {a2$$i..b2$$i} = {a..b}" by auto 

965 
then have "\<exists>a b. \<forall>i<DIM('a). {a1$$i..b1$$i} \<inter> {a2$$i..b2$$i} = {a i..b i}" 

966 
unfolding choice_iff' . 

967 
then guess a b by safe 

968 
then have "{a1..b1} \<inter> {a2..b2} = {(\<chi>\<chi> i. a i) .. (\<chi>\<chi> i. b i)}" 

969 
by (simp add: set_eq_iff eucl_le[where 'a='a] all_conj_distrib[symmetric]) blast 

970 
then show "\<exists>a' b'. {a1..b1} \<inter> {a2..b2} = {a'..b'}" by blast 

971 
qed 

972 

973 
lemma (in sigma_algebra) borel_measurable_sets: 

974 
assumes "f \<in> measurable borel M" "A \<in> sets M" 

975 
shows "f ` A \<in> sets borel" 

976 
using measurable_sets[OF assms] by simp 

977 

978 
lemma (in sigma_algebra) measurable_identity[intro,simp]: 

979 
"(\<lambda>x. x) \<in> measurable M M" 

980 
unfolding measurable_def by auto 

981 

982 
lemma lebesgue_real_affine: 

983 
fixes X :: "real set" 

984 
assumes "X \<in> sets borel" and "c \<noteq> 0" 

43920  985 
shows "measure lebesgue X = ereal \<bar>c\<bar> * measure lebesgue ((\<lambda>x. t + c * x) ` X)" 
42164  986 
(is "_ = ?\<nu> X") 
987 
proof  

988 
let ?E = "\<lparr>space = UNIV, sets = range (\<lambda>(a,b). {a::real .. b})\<rparr> :: real algebra" 

989 
let "?M \<nu>" = "\<lparr>space = space ?E, sets = sets (sigma ?E), measure = \<nu>\<rparr> :: real measure_space" 

990 
have *: "?M (measure lebesgue) = lborel" 

991 
unfolding borel_eq_atLeastAtMost[symmetric] 

992 
by (simp add: lborel_def lebesgue_def) 

993 
have **: "?M ?\<nu> = lborel \<lparr> measure := ?\<nu> \<rparr>" 

994 
unfolding borel_eq_atLeastAtMost[symmetric] 

995 
by (simp add: lborel_def lebesgue_def) 

996 
show ?thesis 

997 
proof (rule measure_unique_Int_stable[where X=X, OF Int_stable_atLeastAtMost], unfold * **) 

998 
show "X \<in> sets (sigma ?E)" 

999 
unfolding borel_eq_atLeastAtMost[symmetric] by fact 

1000 
have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp 

1001 
then show "(\<Union>i. cube i) = space ?E" by auto 

1002 
show "incseq cube" by (intro incseq_SucI cube_subset_Suc) 

1003 
show "range cube \<subseteq> sets ?E" 

1004 
unfolding cube_def_raw by auto 

1005 
show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>" 

1006 
by (simp add: cube_def) 

1007 
show "measure_space lborel" by default 

1008 
then interpret sigma_algebra "lborel\<lparr>measure := ?\<nu>\<rparr>" 

1009 
by (auto simp add: measure_space_def) 

1010 
show "measure_space (lborel\<lparr>measure := ?\<nu>\<rparr>)" 

1011 
proof 

1012 
show "positive (lborel\<lparr>measure := ?\<nu>\<rparr>) (measure (lborel\<lparr>measure := ?\<nu>\<rparr>))" 

43920  1013 
by (auto simp: positive_def intro!: ereal_0_le_mult borel.borel_measurable_sets) 
42164  1014 
show "countably_additive (lborel\<lparr>measure := ?\<nu>\<rparr>) (measure (lborel\<lparr>measure := ?\<nu>\<rparr>))" 
1015 
proof (simp add: countably_additive_def, safe) 

1016 
fix A :: "nat \<Rightarrow> real set" assume A: "range A \<subseteq> sets borel" "disjoint_family A" 

1017 
then have Ai: "\<And>i. A i \<in> sets borel" by auto 

1018 
have "(\<Sum>n. measure lebesgue ((\<lambda>x. t + c * x) ` A n)) = measure lebesgue (\<Union>n. (\<lambda>x. t + c * x) ` A n)" 

1019 
proof (intro lborel.measure_countably_additive) 

1020 
{ fix n have "(\<lambda>x. t + c * x) ` A n \<inter> space borel \<in> sets borel" 

1021 
using A borel.measurable_ident unfolding id_def 

1022 
by (intro measurable_sets[where A=borel] borel.borel_measurable_add[OF _ borel.borel_measurable_times]) auto } 

1023 
then show "range (\<lambda>i. (\<lambda>x. t + c * x) ` A i) \<subseteq> sets borel" by auto 

1024 
from `disjoint_family A` 

1025 
show "disjoint_family (\<lambda>i. (\<lambda>x. t + c * x) ` A i)" 

1026 
by (rule disjoint_family_on_bisimulation) auto 

1027 
qed 

1028 
with Ai show "(\<Sum>n. ?\<nu> (A n)) = ?\<nu> (UNION UNIV A)" 

43920  1029 
by (subst suminf_cmult_ereal) 
42164  1030 
(auto simp: vimage_UN borel.borel_measurable_sets) 
1031 
qed 

1032 
qed 

1033 
fix X assume "X \<in> sets ?E" 

1034 
then obtain a b where [simp]: "X = {a .. b}" by auto 

1035 
show "measure lebesgue X = ?\<nu> X" 

1036 
proof cases 

1037 
assume "0 < c" 

1038 
then have "(\<lambda>x. t + c * x) ` {a..b} = {(a  t) / c .. (b  t) / c}" 

1039 
by (auto simp: field_simps) 

1040 
with `0 < c` show ?thesis 

1041 
by (cases "a \<le> b") (auto simp: field_simps) 

1042 
next 

1043 
assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto 

1044 
then have *: "(\<lambda>x. t + c * x) ` {a..b} = {(b  t) / c .. (a  t) / c}" 

1045 
by (auto simp: field_simps) 

1046 
with `c < 0` show ?thesis 

1047 
by (cases "a \<le> b") (auto simp: field_simps) 

1048 
qed 

1049 
qed 

1050 
qed 

1051 

38656  1052 
end 