author  hoelzl 
Tue, 20 May 2014 19:24:39 +0200  
changeset 57025  e7fd64f82876 
parent 56994  8d5e5ec1cac3 
child 57137  f174712d0a84 
permissions  rwrr 
47694  1 
(* Title: HOL/Probability/Measure_Space.thy 
2 
Author: Lawrence C Paulson 

3 
Author: Johannes Hölzl, TU München 

4 
Author: Armin Heller, TU München 

5 
*) 

6 

7 
header {* Measure spaces and their properties *} 

8 

9 
theory Measure_Space 

10 
imports 

50387  11 
Measurable 
47694  12 
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" 
13 
begin 

14 

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

15 
lemma sums_def2: 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

16 
"f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) > x" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

17 
unfolding sums_def 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

18 
apply (subst LIMSEQ_Suc_iff[symmetric]) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56154
diff
changeset

19 
unfolding lessThan_Suc_atMost .. 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

20 

50104  21 
subsection "Relate extended reals and the indicator function" 
22 

23 
lemma ereal_indicator: "ereal (indicator A x) = indicator A x" 

24 
by (auto simp: indicator_def one_ereal_def) 

25 

26 
lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)" 

27 
unfolding indicator_def by auto 

28 

29 
lemma LIMSEQ_indicator_UN: 

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

31 
proof cases 

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

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

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

35 
show ?thesis 

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

37 
qed (auto simp: indicator_def) 

38 

39 
lemma indicator_add: 

40 
"A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x" 

41 
unfolding indicator_def by auto 

42 

47694  43 
lemma suminf_cmult_indicator: 
44 
fixes f :: "nat \<Rightarrow> ereal" 

45 
assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i" 

46 
shows "(\<Sum>n. f n * indicator (A n) x) = f i" 

47 
proof  

48 
have **: "\<And>n. f n * indicator (A n) x = (if n = i then f n else 0 :: ereal)" 

49 
using `x \<in> A i` assms unfolding disjoint_family_on_def indicator_def by auto 

50 
then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)" 

51 
by (auto simp: setsum_cases) 

52 
moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)" 

51000  53 
proof (rule SUP_eqI) 
47694  54 
fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y" 
55 
from this[of "Suc i"] show "f i \<le> y" by auto 

56 
qed (insert assms, simp) 

57 
ultimately show ?thesis using assms 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

58 
by (subst suminf_ereal_eq_SUP) (auto simp: indicator_def) 
47694  59 
qed 
60 

61 
lemma suminf_indicator: 

62 
assumes "disjoint_family A" 

63 
shows "(\<Sum>n. indicator (A n) x :: ereal) = indicator (\<Union>i. A i) x" 

64 
proof cases 

65 
assume *: "x \<in> (\<Union>i. A i)" 

66 
then obtain i where "x \<in> A i" by auto 

67 
from suminf_cmult_indicator[OF assms(1), OF `x \<in> A i`, of "\<lambda>k. 1"] 

68 
show ?thesis using * by simp 

69 
qed simp 

70 

71 
text {* 

72 
The type for emeasure spaces is already defined in @{theory Sigma_Algebra}, as it is also used to 

73 
represent sigma algebras (with an arbitrary emeasure). 

74 
*} 

75 

56994  76 
subsection "Extend binary sets" 
47694  77 

78 
lemma LIMSEQ_binaryset: 

79 
assumes f: "f {} = 0" 

80 
shows "(\<lambda>n. \<Sum>i<n. f (binaryset A B i)) > f A + f B" 

81 
proof  

82 
have "(\<lambda>n. \<Sum>i < Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)" 

83 
proof 

84 
fix n 

85 
show "(\<Sum>i < Suc (Suc n). f (binaryset A B i)) = f A + f B" 

86 
by (induct n) (auto simp add: binaryset_def f) 

87 
qed 

88 
moreover 

89 
have "... > f A + f B" by (rule tendsto_const) 

90 
ultimately 

91 
have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) > f A + f B" 

92 
by metis 

93 
hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) > f A + f B" 

94 
by simp 

95 
thus ?thesis by (rule LIMSEQ_offset [where k=2]) 

96 
qed 

97 

98 
lemma binaryset_sums: 

99 
assumes f: "f {} = 0" 

100 
shows "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)" 

101 
by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan) 

102 

103 
lemma suminf_binaryset_eq: 

104 
fixes f :: "'a set \<Rightarrow> 'b::{comm_monoid_add, t2_space}" 

105 
shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B" 

106 
by (metis binaryset_sums sums_unique) 

107 

56994  108 
subsection {* Properties of a premeasure @{term \<mu>} *} 
47694  109 

110 
text {* 

111 
The definitions for @{const positive} and @{const countably_additive} should be here, by they are 

112 
necessary to define @{typ "'a measure"} in @{theory Sigma_Algebra}. 

113 
*} 

114 

115 
definition additive where 

116 
"additive M \<mu> \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> \<mu> (x \<union> y) = \<mu> x + \<mu> y)" 

117 

118 
definition increasing where 

119 
"increasing M \<mu> \<longleftrightarrow> (\<forall>x\<in>M. \<forall>y\<in>M. x \<subseteq> y \<longrightarrow> \<mu> x \<le> \<mu> y)" 

120 

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

121 
lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

122 
lemma positiveD2: "positive M f \<Longrightarrow> A \<in> M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

123 

47694  124 
lemma positiveD_empty: 
125 
"positive M f \<Longrightarrow> f {} = 0" 

126 
by (auto simp add: positive_def) 

127 

128 
lemma additiveD: 

129 
"additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) = f x + f y" 

130 
by (auto simp add: additive_def) 

131 

132 
lemma increasingD: 

133 
"increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>M \<Longrightarrow> y\<in>M \<Longrightarrow> f x \<le> f y" 

134 
by (auto simp add: increasing_def) 

135 

50104  136 
lemma countably_additiveI[case_names countably]: 
47694  137 
"(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i)) 
138 
\<Longrightarrow> countably_additive M f" 

139 
by (simp add: countably_additive_def) 

140 

141 
lemma (in ring_of_sets) disjointed_additive: 

142 
assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" "incseq A" 

143 
shows "(\<Sum>i\<le>n. f (disjointed A i)) = f (A n)" 

144 
proof (induct n) 

145 
case (Suc n) 

146 
then have "(\<Sum>i\<le>Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))" 

147 
by simp 

148 
also have "\<dots> = f (A n \<union> disjointed A (Suc n))" 

149 
using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq) 

150 
also have "A n \<union> disjointed A (Suc n) = A (Suc n)" 

151 
using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq) 

152 
finally show ?case . 

153 
qed simp 

154 

155 
lemma (in ring_of_sets) additive_sum: 

156 
fixes A:: "'i \<Rightarrow> 'a set" 

157 
assumes f: "positive M f" and ad: "additive M f" and "finite S" 

158 
and A: "A`S \<subseteq> M" 

159 
and disj: "disjoint_family_on A S" 

160 
shows "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)" 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

161 
using `finite S` disj A 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

162 
proof induct 
47694  163 
case empty show ?case using f by (simp add: positive_def) 
164 
next 

165 
case (insert s S) 

166 
then have "A s \<inter> (\<Union>i\<in>S. A i) = {}" 

167 
by (auto simp add: disjoint_family_on_def neq_iff) 

168 
moreover 

169 
have "A s \<in> M" using insert by blast 

170 
moreover have "(\<Union>i\<in>S. A i) \<in> M" 

171 
using insert `finite S` by auto 

172 
ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)" 

173 
using ad UNION_in_sets A by (auto simp add: additive_def) 

174 
with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A] 

175 
by (auto simp add: additive_def subset_insertI) 

176 
qed 

177 

178 
lemma (in ring_of_sets) additive_increasing: 

179 
assumes posf: "positive M f" and addf: "additive M f" 

180 
shows "increasing M f" 

181 
proof (auto simp add: increasing_def) 

182 
fix x y 

183 
assume xy: "x \<in> M" "y \<in> M" "x \<subseteq> y" 

184 
then have "y  x \<in> M" by auto 

185 
then have "0 \<le> f (yx)" using posf[unfolded positive_def] by auto 

186 
then have "f x + 0 \<le> f x + f (yx)" by (intro add_left_mono) auto 

187 
also have "... = f (x \<union> (yx))" using addf 

188 
by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2)) 

189 
also have "... = f y" 

190 
by (metis Un_Diff_cancel Un_absorb1 xy(3)) 

191 
finally show "f x \<le> f y" by simp 

192 
qed 

193 

50087  194 
lemma (in ring_of_sets) subadditive: 
195 
assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" and S: "finite S" 

196 
shows "f (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. f (A i))" 

197 
using S 

198 
proof (induct S) 

199 
case empty thus ?case using f by (auto simp: positive_def) 

200 
next 

201 
case (insert x F) 

202 
hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i)  A x \<in> M" using A by force+ 

203 
have subs: "(\<Union> i\<in>F. A i)  A x \<subseteq> (\<Union> i\<in>F. A i)" by auto 

204 
have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i)  A x)" by auto 

205 
hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i)  A x))" 

206 
by simp 

207 
also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i)  A x)" 

208 
using f(2) by (rule additiveD) (insert in_M, auto) 

209 
also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)" 

210 
using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono) 

211 
also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono) 

212 
finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp 

213 
qed 

214 

47694  215 
lemma (in ring_of_sets) countably_additive_additive: 
216 
assumes posf: "positive M f" and ca: "countably_additive M f" 

217 
shows "additive M f" 

218 
proof (auto simp add: additive_def) 

219 
fix x y 

220 
assume x: "x \<in> M" and y: "y \<in> M" and "x \<inter> y = {}" 

221 
hence "disjoint_family (binaryset x y)" 

222 
by (auto simp add: disjoint_family_on_def binaryset_def) 

223 
hence "range (binaryset x y) \<subseteq> M \<longrightarrow> 

224 
(\<Union>i. binaryset x y i) \<in> M \<longrightarrow> 

225 
f (\<Union>i. binaryset x y i) = (\<Sum> n. f (binaryset x y n))" 

226 
using ca 

227 
by (simp add: countably_additive_def) 

228 
hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow> 

229 
f (x \<union> y) = (\<Sum>n. f (binaryset x y n))" 

230 
by (simp add: range_binaryset_eq UN_binaryset_eq) 

231 
thus "f (x \<union> y) = f x + f y" using posf x y 

232 
by (auto simp add: Un suminf_binaryset_eq positive_def) 

233 
qed 

234 

235 
lemma (in algebra) increasing_additive_bound: 

236 
fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ereal" 

237 
assumes f: "positive M f" and ad: "additive M f" 

238 
and inc: "increasing M f" 

239 
and A: "range A \<subseteq> M" 

240 
and disj: "disjoint_family A" 

241 
shows "(\<Sum>i. f (A i)) \<le> f \<Omega>" 

242 
proof (safe intro!: suminf_bound) 

243 
fix N 

244 
note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"] 

245 
have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)" 

246 
using A by (intro additive_sum [OF f ad _ _]) (auto simp: disj_N) 

247 
also have "... \<le> f \<Omega>" using space_closed A 

248 
by (intro increasingD[OF inc] finite_UN) auto 

249 
finally show "(\<Sum>i<N. f (A i)) \<le> f \<Omega>" by simp 

250 
qed (insert f A, auto simp: positive_def) 

251 

252 
lemma (in ring_of_sets) countably_additiveI_finite: 

253 
assumes "finite \<Omega>" "positive M \<mu>" "additive M \<mu>" 

254 
shows "countably_additive M \<mu>" 

255 
proof (rule countably_additiveI) 

256 
fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> M" "(\<Union>i. F i) \<in> M" and disj: "disjoint_family F" 

257 

258 
have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto 

259 
from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto 

260 

261 
have inj_f: "inj_on f {i. F i \<noteq> {}}" 

262 
proof (rule inj_onI, simp) 

263 
fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}" 

264 
then have "f i \<in> F i" "f j \<in> F j" using f by force+ 

265 
with disj * show "i = j" by (auto simp: disjoint_family_on_def) 

266 
qed 

267 
have "finite (\<Union>i. F i)" 

268 
by (metis F(2) assms(1) infinite_super sets_into_space) 

269 

270 
have F_subset: "{i. \<mu> (F i) \<noteq> 0} \<subseteq> {i. F i \<noteq> {}}" 

271 
by (auto simp: positiveD_empty[OF `positive M \<mu>`]) 

272 
moreover have fin_not_empty: "finite {i. F i \<noteq> {}}" 

273 
proof (rule finite_imageD) 

274 
from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto 

275 
then show "finite (f`{i. F i \<noteq> {}})" 

276 
by (rule finite_subset) fact 

277 
qed fact 

278 
ultimately have fin_not_0: "finite {i. \<mu> (F i) \<noteq> 0}" 

279 
by (rule finite_subset) 

280 

281 
have disj_not_empty: "disjoint_family_on F {i. F i \<noteq> {}}" 

282 
using disj by (auto simp: disjoint_family_on_def) 

283 

284 
from fin_not_0 have "(\<Sum>i. \<mu> (F i)) = (\<Sum>i  \<mu> (F i) \<noteq> 0. \<mu> (F i))" 

47761  285 
by (rule suminf_finite) auto 
47694  286 
also have "\<dots> = (\<Sum>i  F i \<noteq> {}. \<mu> (F i))" 
287 
using fin_not_empty F_subset by (rule setsum_mono_zero_left) auto 

288 
also have "\<dots> = \<mu> (\<Union>i\<in>{i. F i \<noteq> {}}. F i)" 

289 
using `positive M \<mu>` `additive M \<mu>` fin_not_empty disj_not_empty F by (intro additive_sum) auto 

290 
also have "\<dots> = \<mu> (\<Union>i. F i)" 

291 
by (rule arg_cong[where f=\<mu>]) auto 

292 
finally show "(\<Sum>i. \<mu> (F i)) = \<mu> (\<Union>i. F i)" . 

293 
qed 

294 

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

295 
lemma (in ring_of_sets) countably_additive_iff_continuous_from_below: 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

296 
assumes f: "positive M f" "additive M f" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

297 
shows "countably_additive M f \<longleftrightarrow> 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

298 
(\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) > f (\<Union>i. A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

299 
unfolding countably_additive_def 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

300 
proof safe 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

301 
assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

302 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

303 
then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

304 
with count_sum[THEN spec, of "disjointed A"] A(3) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

305 
have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

306 
by (auto simp: UN_disjointed_eq disjoint_family_disjointed) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56154
diff
changeset

307 
moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) > (\<Sum>i. f (disjointed A i))" 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

308 
using f(1)[unfolded positive_def] dA 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56154
diff
changeset

309 
by (auto intro!: summable_LIMSEQ summable_ereal_pos) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

310 
from LIMSEQ_Suc[OF this] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

311 
have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) > (\<Sum>i. f (disjointed A i))" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56154
diff
changeset

312 
unfolding lessThan_Suc_atMost . 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

313 
moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

314 
using disjointed_additive[OF f A(1,2)] . 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

315 
ultimately show "(\<lambda>i. f (A i)) > f (\<Union>i. A i)" by simp 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

316 
next 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

317 
assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) > f (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

318 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

319 
have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

320 
have "(\<lambda>n. f (\<Union>i\<le>n. A i)) > f (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

321 
proof (unfold *[symmetric], intro cont[rule_format]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

322 
show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> M" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

323 
using A * by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

324 
qed (force intro!: incseq_SucI) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

325 
moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

326 
using A 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

327 
by (intro additive_sum[OF f, of _ A, symmetric]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

328 
(auto intro: disjoint_family_on_mono[where B=UNIV]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

329 
ultimately 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

330 
have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

331 
unfolding sums_def2 by simp 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

332 
from sums_unique[OF this] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

333 
show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

334 
qed 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

335 

16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

336 
lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous: 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

337 
assumes f: "positive M f" "additive M f" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

338 
shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) > f (\<Inter>i. A i)) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

339 
\<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) > 0)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

340 
proof safe 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

341 
assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) > f (\<Inter>i. A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

342 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

343 
with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

344 
using `positive M f`[unfolded positive_def] by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

345 
next 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

346 
assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

347 
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

348 

16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

349 
have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

350 
using additive_increasing[OF f] unfolding increasing_def by simp 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

351 

16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

352 
have decseq_fA: "decseq (\<lambda>i. f (A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

353 
using A by (auto simp: decseq_def intro!: f_mono) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

354 
have decseq: "decseq (\<lambda>i. A i  (\<Inter>i. A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

355 
using A by (auto simp: decseq_def) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

356 
then have decseq_f: "decseq (\<lambda>i. f (A i  (\<Inter>i. A i)))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

357 
using A unfolding decseq_def by (auto intro!: f_mono Diff) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

358 
have "f (\<Inter>x. A x) \<le> f (A 0)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

359 
using A by (auto intro!: f_mono) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

360 
then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

361 
using A by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

362 
{ fix i 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

363 
have "f (A i  (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

364 
then have "f (A i  (\<Inter>i. A i)) \<noteq> \<infinity>" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

365 
using A by auto } 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

366 
note f_fin = this 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

367 
have "(\<lambda>i. f (A i  (\<Inter>i. A i))) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

368 
proof (intro cont[rule_format, OF _ decseq _ f_fin]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

369 
show "range (\<lambda>i. A i  (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i  (\<Inter>i. A i)) = {}" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

370 
using A by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

371 
qed 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

372 
from INF_Lim_ereal[OF decseq_f this] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

373 
have "(INF n. f (A n  (\<Inter>i. A i))) = 0" . 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

374 
moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

375 
by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

376 
ultimately have "(INF n. f (A n  (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

377 
using A(4) f_fin f_Int_fin 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

378 
by (subst INF_ereal_add) (auto simp: decseq_f) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

379 
moreover { 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

380 
fix n 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

381 
have "f (A n  (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n  (\<Inter>i. A i)) \<union> (\<Inter>i. A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

382 
using A by (subst f(2)[THEN additiveD]) auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

383 
also have "(A n  (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

384 
by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

385 
finally have "f (A n  (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . } 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

386 
ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

387 
by simp 
51351  388 
with LIMSEQ_INF[OF decseq_fA] 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

389 
show "(\<lambda>i. f (A i)) > f (\<Inter>i. A i)" by simp 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

390 
qed 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

391 

16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

392 
lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below: 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

393 
assumes f: "positive M f" "additive M f" "\<forall>A\<in>M. f A \<noteq> \<infinity>" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

394 
assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

395 
assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

396 
shows "(\<lambda>i. f (A i)) > f (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

397 
proof  
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

398 
have "\<forall>A\<in>M. \<exists>x. f A = ereal x" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

399 
proof 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

400 
fix A assume "A \<in> M" with f show "\<exists>x. f A = ereal x" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

401 
unfolding positive_def by (cases "f A") auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

402 
qed 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

403 
from bchoice[OF this] guess f' .. note f' = this[rule_format] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

404 
from A have "(\<lambda>i. f ((\<Union>i. A i)  A i)) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

405 
by (intro cont[rule_format]) (auto simp: decseq_def incseq_def) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

406 
moreover 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

407 
{ fix i 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

408 
have "f ((\<Union>i. A i)  A i) + f (A i) = f ((\<Union>i. A i)  A i \<union> A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

409 
using A by (intro f(2)[THEN additiveD, symmetric]) auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

410 
also have "(\<Union>i. A i)  A i \<union> A i = (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

411 
by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

412 
finally have "f' (\<Union>i. A i)  f' (A i) = f' ((\<Union>i. A i)  A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

413 
using A by (subst (asm) (1 2 3) f') auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

414 
then have "f ((\<Union>i. A i)  A i) = ereal (f' (\<Union>i. A i)  f' (A i))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

415 
using A f' by auto } 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

416 
ultimately have "(\<lambda>i. f' (\<Union>i. A i)  f' (A i)) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

417 
by (simp add: zero_ereal_def) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

418 
then have "(\<lambda>i. f' (A i)) > f' (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

419 
by (rule LIMSEQ_diff_approach_zero2[OF tendsto_const]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

420 
then show "(\<lambda>i. f (A i)) > f (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

421 
using A by (subst (1 2) f') auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

422 
qed 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

423 

16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

424 
lemma (in ring_of_sets) empty_continuous_imp_countably_additive: 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

425 
assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>M. f A \<noteq> \<infinity>" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

426 
assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) > 0" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

427 
shows "countably_additive M f" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

428 
using countably_additive_iff_continuous_from_below[OF f] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

429 
using empty_continuous_imp_continuous_from_below[OF f fin] cont 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

430 
by blast 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

431 

56994  432 
subsection {* Properties of @{const emeasure} *} 
47694  433 

434 
lemma emeasure_positive: "positive (sets M) (emeasure M)" 

435 
by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def) 

436 

437 
lemma emeasure_empty[simp, intro]: "emeasure M {} = 0" 

438 
using emeasure_positive[of M] by (simp add: positive_def) 

439 

440 
lemma emeasure_nonneg[intro!]: "0 \<le> emeasure M A" 

441 
using emeasure_notin_sets[of A M] emeasure_positive[of M] 

442 
by (cases "A \<in> sets M") (auto simp: positive_def) 

443 

444 
lemma emeasure_not_MInf[simp]: "emeasure M A \<noteq>  \<infinity>" 

445 
using emeasure_nonneg[of M A] by auto 

50419  446 

447 
lemma emeasure_le_0_iff: "emeasure M A \<le> 0 \<longleftrightarrow> emeasure M A = 0" 

448 
using emeasure_nonneg[of M A] by auto 

449 

450 
lemma emeasure_less_0_iff: "emeasure M A < 0 \<longleftrightarrow> False" 

451 
using emeasure_nonneg[of M A] by auto 

47694  452 

453 
lemma emeasure_countably_additive: "countably_additive (sets M) (emeasure M)" 

454 
by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def) 

455 

456 
lemma suminf_emeasure: 

457 
"range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Sum>i. emeasure M (A i)) = emeasure M (\<Union>i. A i)" 

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

458 
using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M] 
47694  459 
by (simp add: countably_additive_def) 
460 

461 
lemma emeasure_additive: "additive (sets M) (emeasure M)" 

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

462 
by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive) 
47694  463 

464 
lemma plus_emeasure: 

465 
"a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)" 

466 
using additiveD[OF emeasure_additive] .. 

467 

468 
lemma setsum_emeasure: 

469 
"F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow> 

470 
(\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)" 

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

471 
by (metis sets.additive_sum emeasure_positive emeasure_additive) 
47694  472 

473 
lemma emeasure_mono: 

474 
"a \<subseteq> b \<Longrightarrow> b \<in> sets M \<Longrightarrow> emeasure M a \<le> emeasure M b" 

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

475 
by (metis sets.additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets 
47694  476 
emeasure_positive increasingD) 
477 

478 
lemma emeasure_space: 

479 
"emeasure M A \<le> emeasure M (space M)" 

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

480 
by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets.sets_into_space sets.top) 
47694  481 

482 
lemma emeasure_compl: 

483 
assumes s: "s \<in> sets M" and fin: "emeasure M s \<noteq> \<infinity>" 

484 
shows "emeasure M (space M  s) = emeasure M (space M)  emeasure M s" 

485 
proof  

486 
from s have "0 \<le> emeasure M s" by auto 

487 
have "emeasure M (space M) = emeasure M (s \<union> (space M  s))" using s 

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

488 
by (metis Un_Diff_cancel Un_absorb1 s sets.sets_into_space) 
47694  489 
also have "... = emeasure M s + emeasure M (space M  s)" 
490 
by (rule plus_emeasure[symmetric]) (auto simp add: s) 

491 
finally have "emeasure M (space M) = emeasure M s + emeasure M (space M  s)" . 

492 
then show ?thesis 

493 
using fin `0 \<le> emeasure M s` 

494 
unfolding ereal_eq_minus_iff by (auto simp: ac_simps) 

495 
qed 

496 

497 
lemma emeasure_Diff: 

498 
assumes finite: "emeasure M B \<noteq> \<infinity>" 

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

499 
and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A" 
47694  500 
shows "emeasure M (A  B) = emeasure M A  emeasure M B" 
501 
proof  

502 
have "0 \<le> emeasure M B" using assms by auto 

503 
have "(A  B) \<union> B = A" using `B \<subseteq> A` by auto 

504 
then have "emeasure M A = emeasure M ((A  B) \<union> B)" by simp 

505 
also have "\<dots> = emeasure M (A  B) + emeasure M B" 

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

506 
by (subst plus_emeasure[symmetric]) auto 
47694  507 
finally show "emeasure M (A  B) = emeasure M A  emeasure M B" 
508 
unfolding ereal_eq_minus_iff 

509 
using finite `0 \<le> emeasure M B` by auto 

510 
qed 

511 

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

512 
lemma Lim_emeasure_incseq: 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

513 
"range A \<subseteq> sets M \<Longrightarrow> incseq A \<Longrightarrow> (\<lambda>i. (emeasure M (A i))) > emeasure M (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

515 
by (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive 
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

516 
emeasure_additive) 
47694  517 

518 
lemma incseq_emeasure: 

519 
assumes "range B \<subseteq> sets M" "incseq B" 

520 
shows "incseq (\<lambda>i. emeasure M (B i))" 

521 
using assms by (auto simp: incseq_def intro!: emeasure_mono) 

522 

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

523 
lemma SUP_emeasure_incseq: 
47694  524 
assumes A: "range A \<subseteq> sets M" "incseq A" 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

525 
shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)" 
51000  526 
using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A] 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

527 
by (simp add: LIMSEQ_unique) 
47694  528 

529 
lemma decseq_emeasure: 

530 
assumes "range B \<subseteq> sets M" "decseq B" 

531 
shows "decseq (\<lambda>i. emeasure M (B i))" 

532 
using assms by (auto simp: decseq_def intro!: emeasure_mono) 

533 

534 
lemma INF_emeasure_decseq: 

535 
assumes A: "range A \<subseteq> sets M" and "decseq A" 

536 
and finite: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" 

537 
shows "(INF n. emeasure M (A n)) = emeasure M (\<Inter>i. A i)" 

538 
proof  

539 
have le_MI: "emeasure M (\<Inter>i. A i) \<le> emeasure M (A 0)" 

540 
using A by (auto intro!: emeasure_mono) 

541 
hence *: "emeasure M (\<Inter>i. A i) \<noteq> \<infinity>" using finite[of 0] by auto 

542 

543 
have A0: "0 \<le> emeasure M (A 0)" using A by auto 

544 

545 
have "emeasure M (A 0)  (INF n. emeasure M (A n)) = emeasure M (A 0) + (SUP n.  emeasure M (A n))" 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

546 
by (simp add: ereal_SUP_uminus minus_ereal_def) 
47694  547 
also have "\<dots> = (SUP n. emeasure M (A 0)  emeasure M (A n))" 
548 
unfolding minus_ereal_def using A0 assms 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56193
diff
changeset

549 
by (subst SUP_ereal_add) (auto simp add: decseq_emeasure) 
47694  550 
also have "\<dots> = (SUP n. emeasure M (A 0  A n))" 
551 
using A finite `decseq A`[unfolded decseq_def] by (subst emeasure_Diff) auto 

552 
also have "\<dots> = emeasure M (\<Union>i. A 0  A i)" 

553 
proof (rule SUP_emeasure_incseq) 

554 
show "range (\<lambda>n. A 0  A n) \<subseteq> sets M" 

555 
using A by auto 

556 
show "incseq (\<lambda>n. A 0  A n)" 

557 
using `decseq A` by (auto simp add: incseq_def decseq_def) 

558 
qed 

559 
also have "\<dots> = emeasure M (A 0)  emeasure M (\<Inter>i. A i)" 

560 
using A finite * by (simp, subst emeasure_Diff) auto 

561 
finally show ?thesis 

562 
unfolding ereal_minus_eq_minus_iff using finite A0 by auto 

563 
qed 

564 

565 
lemma Lim_emeasure_decseq: 

566 
assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" 

567 
shows "(\<lambda>i. emeasure M (A i)) > emeasure M (\<Inter>i. A i)" 

51351  568 
using LIMSEQ_INF[OF decseq_emeasure, OF A] 
47694  569 
using INF_emeasure_decseq[OF A fin] by simp 
570 

571 
lemma emeasure_subadditive: 

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

572 
assumes [measurable]: "A \<in> sets M" "B \<in> sets M" 
47694  573 
shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B" 
574 
proof  

575 
from plus_emeasure[of A M "B  A"] 

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

576 
have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B  A)" by simp 
47694  577 
also have "\<dots> \<le> emeasure M A + emeasure M B" 
578 
using assms by (auto intro!: add_left_mono emeasure_mono) 

579 
finally show ?thesis . 

580 
qed 

581 

582 
lemma emeasure_subadditive_finite: 

583 
assumes "finite I" "A ` I \<subseteq> sets M" 

584 
shows "emeasure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. emeasure M (A i))" 

585 
using assms proof induct 

586 
case (insert i I) 

587 
then have "emeasure M (\<Union>i\<in>insert i I. A i) = emeasure M (A i \<union> (\<Union>i\<in>I. A i))" 

588 
by simp 

589 
also have "\<dots> \<le> emeasure M (A i) + emeasure M (\<Union>i\<in>I. A i)" 

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

590 
using insert by (intro emeasure_subadditive) auto 
47694  591 
also have "\<dots> \<le> emeasure M (A i) + (\<Sum>i\<in>I. emeasure M (A i))" 
592 
using insert by (intro add_mono) auto 

593 
also have "\<dots> = (\<Sum>i\<in>insert i I. emeasure M (A i))" 

594 
using insert by auto 

595 
finally show ?case . 

596 
qed simp 

597 

598 
lemma emeasure_subadditive_countably: 

599 
assumes "range f \<subseteq> sets M" 

600 
shows "emeasure M (\<Union>i. f i) \<le> (\<Sum>i. emeasure M (f i))" 

601 
proof  

602 
have "emeasure M (\<Union>i. f i) = emeasure M (\<Union>i. disjointed f i)" 

603 
unfolding UN_disjointed_eq .. 

604 
also have "\<dots> = (\<Sum>i. emeasure M (disjointed f i))" 

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

605 
using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"] 
47694  606 
by (simp add: disjoint_family_disjointed comp_def) 
607 
also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))" 

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

608 
using sets.range_disjointed_sets[OF assms] assms 
47694  609 
by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset) 
610 
finally show ?thesis . 

611 
qed 

612 

613 
lemma emeasure_insert: 

614 
assumes sets: "{x} \<in> sets M" "A \<in> sets M" and "x \<notin> A" 

615 
shows "emeasure M (insert x A) = emeasure M {x} + emeasure M A" 

616 
proof  

617 
have "{x} \<inter> A = {}" using `x \<notin> A` by auto 

618 
from plus_emeasure[OF sets this] show ?thesis by simp 

619 
qed 

620 

621 
lemma emeasure_eq_setsum_singleton: 

622 
assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M" 

623 
shows "emeasure M S = (\<Sum>x\<in>S. emeasure M {x})" 

624 
using setsum_emeasure[of "\<lambda>x. {x}" S M] assms 

625 
by (auto simp: disjoint_family_on_def subset_eq) 

626 

627 
lemma setsum_emeasure_cover: 

628 
assumes "finite S" and "A \<in> sets M" and br_in_M: "B ` S \<subseteq> sets M" 

629 
assumes A: "A \<subseteq> (\<Union>i\<in>S. B i)" 

630 
assumes disj: "disjoint_family_on B S" 

631 
shows "emeasure M A = (\<Sum>i\<in>S. emeasure M (A \<inter> (B i)))" 

632 
proof  

633 
have "(\<Sum>i\<in>S. emeasure M (A \<inter> (B i))) = emeasure M (\<Union>i\<in>S. A \<inter> (B i))" 

634 
proof (rule setsum_emeasure) 

635 
show "disjoint_family_on (\<lambda>i. A \<inter> B i) S" 

636 
using `disjoint_family_on B S` 

637 
unfolding disjoint_family_on_def by auto 

638 
qed (insert assms, auto) 

639 
also have "(\<Union>i\<in>S. A \<inter> (B i)) = A" 

640 
using A by auto 

641 
finally show ?thesis by simp 

642 
qed 

643 

644 
lemma emeasure_eq_0: 

645 
"N \<in> sets M \<Longrightarrow> emeasure M N = 0 \<Longrightarrow> K \<subseteq> N \<Longrightarrow> emeasure M K = 0" 

646 
by (metis emeasure_mono emeasure_nonneg order_eq_iff) 

647 

648 
lemma emeasure_UN_eq_0: 

649 
assumes "\<And>i::nat. emeasure M (N i) = 0" and "range N \<subseteq> sets M" 

650 
shows "emeasure M (\<Union> i. N i) = 0" 

651 
proof  

652 
have "0 \<le> emeasure M (\<Union> i. N i)" using assms by auto 

653 
moreover have "emeasure M (\<Union> i. N i) \<le> 0" 

654 
using emeasure_subadditive_countably[OF assms(2)] assms(1) by simp 

655 
ultimately show ?thesis by simp 

656 
qed 

657 

658 
lemma measure_eqI_finite: 

659 
assumes [simp]: "sets M = Pow A" "sets N = Pow A" and "finite A" 

660 
assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}" 

661 
shows "M = N" 

662 
proof (rule measure_eqI) 

663 
fix X assume "X \<in> sets M" 

664 
then have X: "X \<subseteq> A" by auto 

665 
then have "emeasure M X = (\<Sum>a\<in>X. emeasure M {a})" 

666 
using `finite A` by (subst emeasure_eq_setsum_singleton) (auto dest: finite_subset) 

667 
also have "\<dots> = (\<Sum>a\<in>X. emeasure N {a})" 

668 
using X eq by (auto intro!: setsum_cong) 

669 
also have "\<dots> = emeasure N X" 

670 
using X `finite A` by (subst emeasure_eq_setsum_singleton) (auto dest: finite_subset) 

671 
finally show "emeasure M X = emeasure N X" . 

672 
qed simp 

673 

674 
lemma measure_eqI_generator_eq: 

675 
fixes M N :: "'a measure" and E :: "'a set set" and A :: "nat \<Rightarrow> 'a set" 

676 
assumes "Int_stable E" "E \<subseteq> Pow \<Omega>" 

677 
and eq: "\<And>X. X \<in> E \<Longrightarrow> emeasure M X = emeasure N X" 

678 
and M: "sets M = sigma_sets \<Omega> E" 

679 
and N: "sets N = sigma_sets \<Omega> E" 

49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

680 
and A: "range A \<subseteq> E" "(\<Union>i. A i) = \<Omega>" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" 
47694  681 
shows "M = N" 
682 
proof  

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

683 
let ?\<mu> = "emeasure M" and ?\<nu> = "emeasure N" 
47694  684 
interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

685 
have "space M = \<Omega>" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

686 
using sets.top[of M] sets.space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` 
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

687 
by blast 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

688 

e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

689 
{ fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>" 
47694  690 
then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

691 
have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

692 
assume "D \<in> sets M" 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

693 
with `Int_stable E` `E \<subseteq> Pow \<Omega>` have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)" 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

694 
unfolding M 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

695 
proof (induct rule: sigma_sets_induct_disjoint) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

696 
case (basic A) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

697 
then have "F \<inter> A \<in> E" using `Int_stable E` `F \<in> E` by (auto simp: Int_stable_def) 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

698 
then show ?case using eq by auto 
47694  699 
next 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

700 
case empty then show ?case by simp 
47694  701 
next 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

702 
case (compl A) 
47694  703 
then have **: "F \<inter> (\<Omega>  A) = F  (F \<inter> A)" 
704 
and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E" 

49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

705 
using `F \<in> E` S.sets_into_space by (auto simp: M) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

706 
have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

707 
then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

708 
have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

709 
then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

710 
then have "?\<mu> (F \<inter> (\<Omega>  A)) = ?\<mu> F  ?\<mu> (F \<inter> A)" unfolding ** 
47694  711 
using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N) 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

712 
also have "\<dots> = ?\<nu> F  ?\<nu> (F \<inter> A)" using eq `F \<in> E` compl by simp 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

713 
also have "\<dots> = ?\<nu> (F \<inter> (\<Omega>  A))" unfolding ** 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

714 
using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>` 
47694  715 
by (auto intro!: emeasure_Diff[symmetric] simp: M N) 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

716 
finally show ?case 
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

717 
using `space M = \<Omega>` by auto 
47694  718 
next 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

719 
case (union A) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

720 
then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

721 
by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N) 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

722 
with A show ?case 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

723 
by auto 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

724 
qed } 
47694  725 
note * = this 
726 
show "M = N" 

727 
proof (rule measure_eqI) 

728 
show "sets M = sets N" 

729 
using M N by simp 

49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

730 
have [simp, intro]: "\<And>i. A i \<in> sets M" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

731 
using A(1) by (auto simp: subset_eq M) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

732 
fix F assume "F \<in> sets M" 
49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

733 
let ?D = "disjointed (\<lambda>i. F \<inter> A i)" 
49789
e0a4cb91a8a9
add induction rule for intersectionstable sigmasets
hoelzl
parents:
49784
diff
changeset

734 
from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

735 
using `F \<in> sets M`[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq) 
49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

736 
have [simp, intro]: "\<And>i. ?D i \<in> sets M" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

737 
using sets.range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M` 
49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

738 
by (auto simp: subset_eq) 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

739 
have "disjoint_family ?D" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

740 
by (auto simp: disjoint_family_disjointed) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

742 
have "(\<Sum>i. emeasure M (?D i)) = (\<Sum>i. emeasure N (?D i))" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

743 
proof (intro arg_cong[where f=suminf] ext) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

744 
fix i 
49784
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

745 
have "A i \<inter> ?D i = ?D i" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

746 
by (auto simp: disjointed_def) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

747 
then show "emeasure M (?D i) = emeasure N (?D i)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

748 
using *[of "A i" "?D i", OF _ A(3)] A(1) by auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

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

750 
ultimately show "emeasure M F = emeasure N F" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

751 
by (simp add: image_subset_iff `sets M = sets N`[symmetric] F_eq[symmetric] suminf_emeasure) 
47694  752 
qed 
753 
qed 

754 

755 
lemma measure_of_of_measure: "measure_of (space M) (sets M) (emeasure M) = M" 

756 
proof (intro measure_eqI emeasure_measure_of_sigma) 

757 
show "sigma_algebra (space M) (sets M)" .. 

758 
show "positive (sets M) (emeasure M)" 

759 
by (simp add: positive_def emeasure_nonneg) 

760 
show "countably_additive (sets M) (emeasure M)" 

761 
by (simp add: emeasure_countably_additive) 

762 
qed simp_all 

763 

56994  764 
subsection {* @{text \<mu>}null sets *} 
47694  765 

766 
definition null_sets :: "'a measure \<Rightarrow> 'a set set" where 

767 
"null_sets M = {N\<in>sets M. emeasure M N = 0}" 

768 

769 
lemma null_setsD1[dest]: "A \<in> null_sets M \<Longrightarrow> emeasure M A = 0" 

770 
by (simp add: null_sets_def) 

771 

772 
lemma null_setsD2[dest]: "A \<in> null_sets M \<Longrightarrow> A \<in> sets M" 

773 
unfolding null_sets_def by simp 

774 

775 
lemma null_setsI[intro]: "emeasure M A = 0 \<Longrightarrow> A \<in> sets M \<Longrightarrow> A \<in> null_sets M" 

776 
unfolding null_sets_def by simp 

777 

778 
interpretation null_sets: ring_of_sets "space M" "null_sets M" for M 

47762  779 
proof (rule ring_of_setsI) 
47694  780 
show "null_sets M \<subseteq> Pow (space M)" 
50244
de72bbe42190
qualified interpretation of sigma_algebra, to avoid name clashes
immler
parents:
50104
diff
changeset

781 
using sets.sets_into_space by auto 
47694  782 
show "{} \<in> null_sets M" 
783 
by auto 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

784 
fix A B assume null_sets: "A \<in> null_sets M" "B \<in> null_sets M" 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

785 
then have sets: "A \<in> sets M" "B \<in> sets M" 
47694  786 
by auto 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

787 
then have *: "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B" 
47694  788 
"emeasure M (A  B) \<le> emeasure M A" 
789 
by (auto intro!: emeasure_subadditive emeasure_mono) 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

790 
then have "emeasure M B = 0" "emeasure M A = 0" 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

791 
using null_sets by auto 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
51351
diff
changeset

792 
with sets * show "A  B \<in> null_sets M" "A \<union> B \<in> null_sets M" 
47694  793 
by (auto intro!: antisym) 
794 
qed 

795 

796 
lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))" 

797 
proof  

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

798 
have "\<Union>range N = \<Union>(N ` range from_nat)" by simp 
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
54417
diff
changeset

799 
then have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)" 
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
54417
diff
changeset

800 
by (simp only: SUP_def image_comp) 
47694  801 
then show ?thesis by simp 
802 
qed 

803 

804 
lemma null_sets_UN[intro]: 

805 
assumes "\<And>i::'i::countable. N i \<in> null_sets M" 

806 
shows "(\<Union>i. N i) \<in> null_sets M" 

807 
proof (intro conjI CollectI null_setsI) 

808 
show "(\<Union>i. N i) \<in> sets M" using assms by auto 

809 
have "0 \<le> emeasure M (\<Union>i. N i)" by (rule emeasure_nonneg) 

810 
moreover have "emeasure M (\<Union>i. N i) \<le> (\<Sum>n. emeasure M (N (Countable.from_nat n)))" 

811 
unfolding UN_from_nat[of N] 

812 
using assms by (intro emeasure_subadditive_countably) auto 

813 
ultimately show "emeasure M (\<Union>i. N i) = 0" 

814 
using assms by (auto simp: null_setsD1) 

815 
qed 

816 

817 
lemma null_set_Int1: 

818 
assumes "B \<in> null_sets M" "A \<in> sets M" shows "A \<inter> B \<in> null_sets M" 

819 
proof (intro CollectI conjI null_setsI) 

820 
show "emeasure M (A \<inter> B) = 0" using assms 

821 
by (intro emeasure_eq_0[of B _ "A \<inter> B"]) auto 

822 
qed (insert assms, auto) 

823 

824 
lemma null_set_Int2: 

825 
assumes "B \<in> null_sets M" "A \<in> sets M" shows "B \<inter> A \<in> null_sets M" 

826 
using assms by (subst Int_commute) (rule null_set_Int1) 

827 

828 
lemma emeasure_Diff_null_set: 

829 
assumes "B \<in> null_sets M" "A \<in> sets M" 

830 
shows "emeasure M (A  B) = emeasure M A" 

831 
proof  

832 
have *: "A  B = (A  (A \<inter> B))" by auto 

833 
have "A \<inter> B \<in> null_sets M" using assms by (rule null_set_Int1) 

834 
then show ?thesis 

835 
unfolding * using assms 

836 
by (subst emeasure_Diff) auto 

837 
qed 

838 

839 
lemma null_set_Diff: 

840 
assumes "B \<in> null_sets M" "A \<in> sets M" shows "B  A \<in> null_sets M" 

841 
proof (intro CollectI conjI null_setsI) 

842 
show "emeasure M (B  A) = 0" using assms by (intro emeasure_eq_0[of B _ "B  A"]) auto 

843 
qed (insert assms, auto) 

844 

845 
lemma emeasure_Un_null_set: 

846 
assumes "A \<in> sets M" "B \<in> null_sets M" 

847 
shows "emeasure M (A \<union> B) = emeasure M A" 

848 
proof  

849 
have *: "A \<union> B = A \<union> (B  A)" by auto 

850 
have "B  A \<in> null_sets M" using assms(2,1) by (rule null_set_Diff) 

851 
then show ?thesis 

852 
unfolding * using assms 

853 
by (subst plus_emeasure[symmetric]) auto 

854 
qed 

855 

56994  856 
subsection {* The almost everywhere filter (i.e.\ quantifier) *} 
47694  857 

858 
definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where 

859 
"ae_filter M = Abs_filter (\<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)" 

860 

861 
abbreviation 

862 
almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where 

863 
"almost_everywhere M P \<equiv> eventually P (ae_filter M)" 

864 

865 
syntax 

866 
"_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10) 

867 

868 
translations 

869 
"AE x in M. P" == "CONST almost_everywhere M (%x. P)" 

870 

871 
lemma eventually_ae_filter: 

872 
fixes M P 

873 
defines [simp]: "F \<equiv> \<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N" 

874 
shows "eventually P (ae_filter M) \<longleftrightarrow> F P" 

875 
unfolding ae_filter_def F_def[symmetric] 

876 
proof (rule eventually_Abs_filter) 

877 
show "is_filter F" 

878 
proof 

879 
fix P Q assume "F P" "F Q" 

880 
then obtain N L where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N" 

881 
and L: "L \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> L" 

882 
by auto 

883 
then have "L \<union> N \<in> null_sets M" "{x \<in> space M. \<not> (P x \<and> Q x)} \<subseteq> L \<union> N" by auto 

884 
then show "F (\<lambda>x. P x \<and> Q x)" by auto 

885 
next 

886 
fix P Q assume "F P" 

887 
then obtain N where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N" by auto 

888 
moreover assume "\<forall>x. P x \<longrightarrow> Q x" 

889 
ultimately have "N \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> N" by auto 

890 
then show "F Q" by auto 

891 
qed auto 

892 
qed 

893 

894 
lemma AE_I': 

895 
"N \<in> null_sets M \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x in M. P x)" 

896 
unfolding eventually_ae_filter by auto 

897 

898 
lemma AE_iff_null: 

899 
assumes "{x\<in>space M. \<not> P x} \<in> sets M" (is "?P \<in> sets M") 

900 
shows "(AE x in M. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets M" 

901 
proof 

902 
assume "AE x in M. P x" then obtain N where N: "N \<in> sets M" "?P \<subseteq> N" "emeasure M N = 0" 

903 
unfolding eventually_ae_filter by auto 

904 
have "0 \<le> emeasure M ?P" by auto 

905 
moreover have "emeasure M ?P \<le> emeasure M N" 

906 
using assms N(1,2) by (auto intro: emeasure_mono) 

907 
ultimately have "emeasure M ?P = 0" unfolding `emeasure M N = 0` by auto 

908 
then show "?P \<in> null_sets M" using assms by auto 

909 
next 

910 
assume "?P \<in> null_sets M" with assms show "AE x in M. P x" by (auto intro: AE_I') 

911 
qed 

912 

913 
lemma AE_iff_null_sets: 

914 
"N \<in> sets M \<Longrightarrow> N \<in> null_sets M \<longleftrightarrow> (AE x in M. x \<notin> N)" 

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

915 
using Int_absorb1[OF sets.sets_into_space, of N M] 
47694  916 
by (subst AE_iff_null) (auto simp: Int_def[symmetric]) 
917 

47761  918 
lemma AE_not_in: 
919 
"N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N" 

920 
by (metis AE_iff_null_sets null_setsD2) 

921 

47694  922 
lemma AE_iff_measurable: 
923 
"N \<in> sets M \<Longrightarrow> {x\<in>space M. \<not> P x} = N \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> emeasure M N = 0" 

924 
using AE_iff_null[of _ P] by auto 

925 

926 
lemma AE_E[consumes 1]: 

927 
assumes "AE x in M. P x" 

928 
obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M" 

929 
using assms unfolding eventually_ae_filter by auto 

930 

931 
lemma AE_E2: 

932 
assumes "AE x in M. P x" "{x\<in>space M. P x} \<in> sets M" 

933 
shows "emeasure M {x\<in>space M. \<not> P x} = 0" (is "emeasure M ?P = 0") 

934 
proof  

935 
have "{x\<in>space M. \<not> P x} = space M  {x\<in>space M. P x}" by auto 

936 
with AE_iff_null[of M P] assms show ?thesis by auto 

937 
qed 

938 

939 
lemma AE_I: 

940 
assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M" 

941 
shows "AE x in M. P x" 

942 
using assms unfolding eventually_ae_filter by auto 

943 

944 
lemma AE_mp[elim!]: 

945 
assumes AE_P: "AE x in M. P x" and AE_imp: "AE x in M. P x \<longrightarrow> Q x" 

946 
shows "AE x in M. Q x" 

947 
proof  

948 
from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A" 

949 
and A: "A \<in> sets M" "emeasure M A = 0" 

950 
by (auto elim!: AE_E) 

951 

952 
from AE_imp obtain B where imp: "{x\<in>space M. P x \<and> \<not> Q x} \<subseteq> B" 

953 
and B: "B \<in> sets M" "emeasure M B = 0" 

954 
by (auto elim!: AE_E) 

955 

956 
show ?thesis 

957 
proof (intro AE_I) 

958 
have "0 \<le> emeasure M (A \<union> B)" using A B by auto 

959 
moreover have "emeasure M (A \<union> B) \<le> 0" 

960 
using emeasure_subadditive[of A M B] A B by auto 

961 
ultimately show "A \<union> B \<in> sets M" "emeasure M (A \<union> B) = 0" using A B by auto 

962 
show "{x\<in>space M. \<not> Q x} \<subseteq> A \<union> B" 

963 
using P imp by auto 

964 
qed 

965 
qed 

966 

967 
(* depricated replace by laws about eventually *) 

968 
lemma 

969 
shows AE_iffI: "AE x in M. P x \<Longrightarrow> AE x in M. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x in M. Q x" 

970 
and AE_disjI1: "AE x in M. P x \<Longrightarrow> AE x in M. P x \<or> Q x" 

971 
and AE_disjI2: "AE x in M. Q x \<Longrightarrow> AE x in M. P x \<or> Q x" 

972 
and AE_conjI: "AE x in M. P x \<Longrightarrow> AE x in M. Q x \<Longrightarrow> AE x in M. P x \<and> Q x" 

973 
and AE_conj_iff[simp]: "(AE x in M. P x \<and> Q x) \<longleftrightarrow> (AE x in M. P x) \<and> (AE x in M. Q x)" 

974 
by auto 

975 

976 
lemma AE_impI: 

977 
"(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x" 

978 
by (cases P) auto 

979 

980 
lemma AE_measure: 

981 
assumes AE: "AE x in M. P x" and sets: "{x\<in>space M. P x} \<in> sets M" (is "?P \<in> sets M") 

982 
shows "emeasure M {x\<in>space M. P x} = emeasure M (space M)" 

983 
proof  

984 
from AE_E[OF AE] guess N . note N = this 

985 
with sets have "emeasure M (space M) \<le> emeasure M (?P \<union> N)" 

986 
by (intro emeasure_mono) auto 

987 
also have "\<dots> \<le> emeasure M ?P + emeasure M N" 

988 
using sets N by (intro emeasure_subadditive) auto 

989 
also have "\<dots> = emeasure M ?P" using N by simp 

990 
finally show "emeasure M ?P = emeasure M (space M)" 

991 
using emeasure_space[of M "?P"] by auto 

992 
qed 

993 

994 
lemma AE_space: "AE x in M. x \<in> space M" 

995 
by (rule AE_I[where N="{}"]) auto 

996 

997 
lemma AE_I2[simp, intro]: 

998 
"(\<And>x. x \<in> space M \<Longrightarrow> P x) \<Longrightarrow> AE x in M. P x" 

999 
using AE_space by force 

1000 

1001 
lemma AE_Ball_mp: 

1002 
"\<forall>x\<in>space M. P x \<Longrightarrow> AE x in M. P x \<longrightarrow> Q x \<Longrightarrow> AE x in M. Q x" 

1003 
by auto 

1004 

1005 
lemma AE_cong[cong]: 

1006 
"(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in M. Q x)" 

1007 
by auto 

1008 

1009 
lemma AE_all_countable: 

1010 
"(AE x in M. \<forall>i. P i x) \<longleftrightarrow> (\<forall>i::'i::countable. AE x in M. P i x)" 

1011 
proof 

1012 
assume "\<forall>i. AE x in M. P i x" 

1013 
from this[unfolded eventually_ae_filter Bex_def, THEN choice] 

1014 
obtain N where N: "\<And>i. N i \<in> null_sets M" "\<And>i. {x\<in>space M. \<not> P i x} \<subseteq> N i" by auto 

1015 
have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. {x\<in>space M. \<not> P i x})" by auto 

1016 
also have "\<dots> \<subseteq> (\<Union>i. N i)" using N by auto 

1017 
finally have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. N i)" . 

1018 
moreover from N have "(\<Union>i. N i) \<in> null_sets M" 

1019 
by (intro null_sets_UN) auto 

1020 
ultimately show "AE x in M. \<forall>i. P i x" 

1021 
unfolding eventually_ae_filter by auto 

1022 
qed auto 

1023 

1024 
lemma AE_finite_all: 

1025 
assumes f: "finite S" shows "(AE x in M. \<forall>i\<in>S. P i x) \<longleftrightarrow> (\<forall>i\<in>S. AE x in M. P i x)" 

1026 
using f by induct auto 

1027 

1028 
lemma AE_finite_allI: 

1029 
assumes "finite S" 

1030 
shows "(\<And>s. s \<in> S \<Longrightarrow> AE x in M. Q s x) \<Longrightarrow> AE x in M. \<forall>s\<in>S. Q s x" 

1031 
using AE_finite_all[OF `finite S`] by auto 

1032 

1033 
lemma emeasure_mono_AE: 

1034 
assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" 

1035 
and B: "B \<in> sets M" 

1036 
shows "emeasure M A \<le> emeasure M B" 

1037 
proof cases 

1038 
assume A: "A \<in> sets M" 

1039 
from imp obtain N where N: "{x\<in>space M. \<not> (x \<in> A \<longrightarrow> x \<in> B)} \<subseteq> N" "N \<in> null_sets M" 

1040 
by (auto simp: eventually_ae_filter) 

1041 
have "emeasure M A = emeasure M (A  N)" 

1042 
using N A by (subst emeasure_Diff_null_set) auto 

1043 
also have "emeasure M (A  N) \<le> emeasure M (B  N)" 

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

1044 
using N A B sets.sets_into_space by (auto intro!: emeasure_mono) 
47694  1045 
also have "emeasure M (B  N) = emeasure M B" 
1046 
using N B by (subst emeasure_Diff_null_set) auto 

1047 
finally show ?thesis . 

1048 
qed (simp add: emeasure_nonneg emeasure_notin_sets) 

1049 

1050 
lemma emeasure_eq_AE: 

1051 
assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B" 

1052 
assumes A: "A \<in> sets M" and B: "B \<in> sets M" 

1053 
shows "emeasure M A = emeasure M B" 

1054 
using assms by (safe intro!: antisym emeasure_mono_AE) auto 

1055 

56994  1056 
subsection {* @{text \<sigma>}finite Measures *} 
47694  1057 

1058 
locale sigma_finite_measure = 

1059 
fixes M :: "'a measure" 

1060 
assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set. 

1061 
range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. emeasure M (A i) \<noteq> \<infinity>)" 

1062 

1063 
lemma (in sigma_finite_measure) sigma_finite_disjoint: 

1064 
obtains A :: "nat \<Rightarrow> 'a set" 

1065 
where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "disjoint_family A" 

1066 
proof atomize_elim 

1067 
case goal1 

1068 
obtain A :: "nat \<Rightarrow> 'a set" where 

1069 
range: "range A \<subseteq> sets M" and 

1070 
space: "(\<Union>i. A i) = space M" and 

1071 
measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" 

1072 
using sigma_finite by auto 

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

1073 
note range' = sets.range_disjointed_sets[OF range] range 
47694  1074 
{ fix i 
1075 
have "emeasure M (disjointed A i) \<le> emeasure M (A i)" 

1076 
using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono) 

1077 
then have "emeasure M (disjointed A i) \<noteq> \<infinity>" 

1078 
using measure[of i] by auto } 

1079 
with disjoint_family_disjointed UN_disjointed_eq[of A] space range' 

1080 
show ?case by (auto intro!: exI[of _ "disjointed A"]) 

1081 
qed 

1082 

1083 
lemma (in sigma_finite_measure) sigma_finite_incseq: 

1084 
obtains A :: "nat \<Rightarrow> 'a set" 

1085 
where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A" 

1086 
proof atomize_elim 

1087 
case goal1 

1088 
obtain F :: "nat \<Rightarrow> 'a set" where 

1089 
F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>" 

1090 
using sigma_finite by auto 

1091 
then show ?case 

1092 
proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI) 

1093 
from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto 

1094 
then show "(\<Union>n. \<Union> i\<le>n. F i) = space M" 

1095 
using F by fastforce 

1096 
next 

1097 
fix n 

1098 
have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))" using F 

1099 
by (auto intro!: emeasure_subadditive_finite) 

1100 
also have "\<dots> < \<infinity>" 

1101 
using F by (auto simp: setsum_Pinfty) 

1102 
finally show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp 

1103 
qed (force simp: incseq_def)+ 

1104 
qed 

1105 

56994  1106 
subsection {* Measure space induced by distribution of @{const measurable}functions *} 
47694  1107 

1108 
definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where 

1109 
"distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f ` A \<inter> space M))" 

1110 

1111 
lemma 

1112 
shows sets_distr[simp]: "sets (distr M N f) = sets N" 

1113 
and space_distr[simp]: "space (distr M N f) = space N" 

1114 
by (auto simp: distr_def) 

1115 

1116 
lemma 

1117 
shows measurable_distr_eq1[simp]: "measurable (distr Mf Nf f) Mf' = measurable Nf Mf'" 

1118 
and measurable_distr_eq2[simp]: "measurable Mg' (distr Mg Ng g) = measurable Mg' Ng" 

1119 
by (auto simp: measurable_def) 

1120 

54417  1121 
lemma distr_cong: 
1122 
"M = K \<Longrightarrow> sets N = sets L \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> distr M N f = distr K L g" 

1123 
using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong) 

1124 

47694  1125 
lemma emeasure_distr: 
1126 
fixes f :: "'a \<Rightarrow> 'b" 

1127 
assumes f: "f \<in> measurable M N" and A: "A \<in> sets N" 

1128 
shows "emeasure (distr M N f) A = emeasure M (f ` A \<inter> space M)" (is "_ = ?\<mu> A") 

1129 
unfolding distr_def 

1130 
proof (rule emeasure_measure_of_sigma) 

1131 
show "positive (sets N) ?\<mu>" 

1132 
by (auto simp: positive_def) 

1133 

1134 
show "countably_additive (sets N) ?\<mu>" 

1135 
proof (intro countably_additiveI) 

1136 
fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets N" "disjoint_family A" 

1137 
then have A: "\<And>i. A i \<in> sets N" "(\<Union>i. A i) \<in> sets N" by auto 

1138 
then have *: "range (\<lambda>i. f ` (A i) \<inter> space M) \<subseteq> sets M" 

1139 
using f by (auto simp: measurable_def) 

1140 
moreover have "(\<Union>i. f ` A i \<inter> space M) \<in> sets M" 

1141 
using * by blast 

1142 
moreover have **: "disjoint_family (\<lambda>i. f ` A i \<inter> space M)" 

1143 
using `disjoint_family A` by (auto simp: disjoint_family_on_def) 

1144 
ultimately show "(\<Sum>i. ?\<mu> (A i)) = ?\<mu> (\<Union>i. A i)" 

1145 
using suminf_emeasure[OF _ **] A f 

1146 
by (auto simp: comp_def vimage_UN) 

1147 
qed 

1148 
show "sigma_algebra (space N) (sets N)" .. 

1149 
qed fact 

1150 

50104  1151 
lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N" 
1152 
by (rule measure_eqI) (auto simp: emeasure_distr) 

1153 

50001
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49789
diff
changeset

1154 
lemma measure_distr: 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49789
diff
changeset

1155 
"f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f ` S \<inter> space M)" 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49789
diff
changeset

1156 
by (simp add: emeasure_distr measure_def) 
382bd3173584
add syntax and a.e.rules for (conditional) probability on predicates
hoelzl
parents:
49789
diff
changeset

1157 

47694  1158 
lemma AE_distrD: 
1159 
assumes f: "f \<in> measurable M M'" 

1160 
and AE: "AE x in distr M M' f. P x" 

1161 
shows "AE x in M. P (f x)" 

1162 
proof  

1163 
from AE[THEN AE_E] guess N . 

1164 
with f show ?thesis 

1165 
unfolding eventually_ae_filter 

1166 
by (intro bexI[of _ "f ` N \<inter> space M"]) 

1167 
(auto simp: emeasure_distr measurable_def) 

1168 
qed 

1169 

49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

1171 
assumes f[measurable]: "f \<in> measurable M N" and P[measurable]: "{x \<in> space N. P x} \<in> sets N" 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1172 
shows "(AE x in distr M N f. P x) \<longleftrightarrow> (AE x in M. P (f x))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1173 
proof (subst (1 2) AE_iff_measurable[OF _ refl]) 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1174 
have "f ` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1175 
using f[THEN measurable_space] by auto 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1176 
then show "(emeasure (distr M N f) {x \<in> space (distr M N f). \<not> P x} = 0) = 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1177 
(emeasure M {x \<in> space M. \<not> P (f x)} = 0)" 
50002
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1178 
by (simp add: emeasure_distr) 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1179 
qed auto 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1180 

47694  1181 
lemma null_sets_distr_iff: 
1182 
"f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f ` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N" 

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

1183 
by (auto simp add: null_sets_def emeasure_distr) 
47694  1184 

1185 
lemma distr_distr: 

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

1186 
"g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)" 
ce0d316b5b44
add measurability prover; add support for Borel sets
hoelzl
parents:
50001
diff
changeset

1187 
by (auto simp add: emeasure_distr measurable_space 
47694  1188 
intro!: arg_cong[where f="emeasure M"] measure_eqI) 
1189 

56994  1190 
subsection {* Real measure values *} 
47694  1191 

1192 
lemma measure_nonneg: "0 \<le> measure M A" 

1193 
using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos) 

1194 

1195 
lemma measure_empty[simp]: "measure M {} = 0" 

1196 
unfolding measure_def by simp 

1197 

1198 
lemma emeasure_eq_ereal_measure: 

1199 
"emeasure M A \<noteq> \<infinity> \<Longrightarrow> emeasure M A = ereal (measure M A)" 

1200 
using emeasure_nonneg[of M A] 

1201 
by (cases "emeasure M A") (auto simp: measure_def) 

1202 

1203 
lemma measure_Union: 

1204 
assumes finite: "emeasure M A \<noteq> \<infinity>" "emeasure M B \<noteq> \<infinity>" 

1205 
and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}" 

1206 
shows "measure M (A \<union> B) = measure M A + measure M B" 

1207 
unfolding measure_def 

1208 
using plus_emeasure[OF measurable, symmetric] finite 

1209 
by (simp add: emeasure_eq_ereal_measure) 

1210 

1211 
lemma measure_finite_Union: 

1212 
assumes measurable: "A`S \<subseteq> sets M" "disjoint_family_on A S" "finite S" 

1213 
assumes finite: "\<And>i. i \<in> S \<Longrightarrow> emeasure M (A i) \<noteq> \<infinity>" 

1214 
shows "measure M (\<Union>i\<in>S. A i) = (\<Sum>i\<in>S. measure M (A i))" 

1215 
unfolding measure_def 

1216 
using setsum_emeasure[OF measurable, symmetric] finite 

1217 
by (simp add: emeasure_eq_ereal_measure) 

1218 

1219 
lemma measure_Diff: 

1220 
assumes finite: "emeasure M A \<noteq> \<infinity>" 

1221 
and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A" 

1222 
shows "measure M (A  B) = measure M A  measure M B" 

1223 
proof  

1224 
have "emeasure M (A  B) \<le> emeasure M A" "emeasure M B \<le> emeasure M A" 

1225 
using measurable by (auto intro!: emeasure_mono) 

1226 
hence "measure M ((A  B) \<union> B) = measure M (A  B) + measure M B" 

1227 
using measurable finite by (rule_tac measure_Union) auto 

1228 
thus ?thesis using `B \<subseteq> A` by (auto simp: Un_absorb2) 

1229 
qed 

1230 

1231 
lemma measure_UNION: 

1232 
assumes measurable: "range A \<subseteq> sets M" "disjoint_family A" 

1233 
assumes finite: "emeasure M (\<Union>i. A i) \<noteq> \<infinity>" 

1234 
shows "(\<lambda>i. measure M (A i)) sums (measure M (\<Union>i. A i))" 

1235 
proof  

1236 
from summable_sums[OF summable_ereal_pos, of "\<lambda>i. emeasure M (A i)"] 

1237 
suminf_emeasure[OF measurable] emeasure_nonneg[of M] 

1238 
have "(\<lambda>i. emeasure M (A i)) sums (emeasure M (\<Union>i. A i))" by simp 

1239 
moreover 

1240 
{ fix i 

1241 
have "emeasure M (A i) \<le> emeasure M (\<Union>i. A i)" 

1242 
using measurable by (auto intro!: emeasure_mono) 

1243 
then have "emeasure M (A i) = ereal ((measure M (A i)))" 

1244 
using finite by (intro emeasure_eq_ereal_measure) auto } 

1245 
ultimately show ?thesis using finite 

1246 
unfolding sums_ereal[symmetric] by (simp add: emeasure_eq_ereal_measure) 

1247 
qed 

1248 

1249 
lemma measure_subadditive: 

1250 
assumes measurable: "A \<in> sets M" "B \<in> sets M" 

1251 
and fin: "emeasure M A \<noteq> \<infinity>" "emeasure M B \<noteq> \<infinity>" 

1252 
shows "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)" 

1253 
proof  

1254 
have "emeasure M (A \<union> B) \<noteq> \<infinity>" 

1255 
using emeasure_subadditive[OF measurable] fin by auto 

1256 
then show "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)" 

1257 
using emeasure_subadditive[OF measurable] fin 

1258 
by (auto simp: emeasure_eq_ereal_measure) 

1259 
qed 

1260 

1261 
lemma measure_subadditive_finite: 

1262 
assumes A: "finite I" "A`I \<subseteq> sets M" and fin: "\<And>i. i \<in> I \<Longrightarrow> emeasure M (A i) \<noteq> \<infinity>" 

1263 
shows "measure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. measure M (A i))" 

1264 
proof  

1265 
{ have "emeasure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. emeasure M (A i))" 

1266 
using emeasure_subadditive_finite[OF A] . 

1267 
also have "\<dots> < \<infinity>" 

1268 
using fin by (simp add: setsum_Pinfty) 

1269 
finally have "emeasure M (\<Union>i\<in>I. A i) \<noteq> \<infinity>" by simp } 

1270 
then show ?thesis 

1271 
using emeasure_subadditive_finite[OF A] fin 

1272 
unfolding measure_def by (simp add: emeasure_eq_ereal_measure suminf_ereal measure_nonneg) 

1273 
qed 

1274 

1275 
lemma measure_subadditive_countably: 

1276 
assumes A: "range A \<subseteq> sets M" and fin: "(\<Sum>i. emeasure M (A i)) \<noteq> \<infinity>" 

1277 
shows "measure M (\<Union>i. A i) \<le> (\<Sum>i. measure M (A i))" 

1278 
proof  

1279 
from emeasure_nonneg fin have "\<And>i. emeasure M (A i) \<noteq> \<infinity>" by (rule suminf_PInfty) 

1280 
moreover 

1281 
{ have "emeasure M (\<Union>i. A i) \<le> (\<Sum>i. emeasure M (A i))" 

1282 
using emeasure_subadditive_countably[OF A] . 

1283 
also have "\<dots> < \<infinity>" 

1284 
using fin by simp 

1285 
finally have "emeasure M (\<Union>i. A i) \<noteq> \<infinity>" by simp } 

1286 
ultimately show ?thesis 

1287 
using emeasure_subadditive_countably[OF A] fin 

1288 
unfolding measure_def by (simp add: emeasure_eq_ereal_measure suminf_ereal measure_nonneg) 

1289 
qed 

1290 

1291 
lemma measure_eq_setsum_singleton: 

1292 
assumes S: "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M" 

1293 
and fin: "\<And>x. x \<in> S \<Longrightarrow> emeasure M {x} \<noteq> \<infinity>" 

1294 
shows "(measure M S) = (\<Sum>x\<in>S. (measure M {x}))" 

1295 
unfolding measure_def 

1296 
using emeasure_eq_setsum_singleton[OF S] fin 

1297 
by simp (simp add: emeasure_eq_ereal_measure) 

1298 

1299 
lemma Lim_measure_incseq: 

1300 
assumes A: "range A \<subseteq> sets M" "incseq A" and fin: "emeasure M (\<Union>i. A i) \<noteq> \<infinity>" 

1301 
shows "(\<lambda>i. (measure M (A i))) > (measure M (\<Union>i. A i))" 

1302 
proof  

1303 
have "ereal ((measure M (\<Union>i. A i))) = emeasure M (\<Union>i. A i)" 

1304 
using fin by (auto simp: emeasure_eq_ereal_measure) 

1305 
then show ?thesis 

1306 
using Lim_emeasure_incseq[OF A] 

1307 
unfolding measure_def 

1308 
by (intro lim_real_of_ereal) simp 

1309 
qed 

1310 

1311 
lemma Lim_measure_decseq: 

1312 
assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" 

1313 
shows "(\<lambda>n. measure M (A n)) > measure M (\<Inter>i. A i)" 

1314 
proof  

1315 
have "emeasure M (\<Inter>i. A i) \<le> emeasure M (A 0)" 

1316 
using A by (auto intro!: emeasure_mono) 

1317 
also have "\<dots> < \<infinity>" 

1318 
using fin[of 0] by auto 

1319 
finally have "ereal ((measure M (\<Inter>i. A i))) = emeasure M (\<Inter>i. A i)" 

1320 
by (auto simp: emeasure_eq_ereal_measure) 

1321 
then show ?thesis 

1322 
unfolding measure_def 

1323 
using Lim_emeasure_decseq[OF A fin] 

1324 
by (intro lim_real_of_ereal) simp 

1325 
qed 

1326 

56994  1327 
subsection {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *} 
47694  1328 

1329 
locale finite_measure = sigma_finite_measure M for M + 

1330 
assumes finite_emeasure_space: "emeasure M (space M) \<noteq> \<infinity>" 

1331 

1332 
lemma finite_measureI[Pure.intro!]: 

1333 
assumes *: "emeasure M (space M) \<noteq> \<infinity>" 

1334 
shows "finite_measure M" 

1335 
proof 

1336 
show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. emeasure M (A i) \<noteq> \<infinity>)" 

1337 
using * by (auto intro!: exI[of _ "\<lambda>_. space M"]) 

1338 
qed fact 

1339 

1340 
lemma (in finite_measure) emeasure_finite[simp, intro]: "emeasure M A \<noteq> \<infinity>" 

1341 
using finite_emeasure_space emeasure_space[of M A] by auto 

1342 

1343 
lemma (in finite_measure) emeasure_eq_measure: "emeasure M A = ereal (measure M A)" 

1344 
unfolding measure_def by (simp add: emeasure_eq_ereal_measure) 

1345 

1346 
lemma (in finite_measure) emeasure_real: "\<exists>r. 0 \<le> r \<and> emeasure M A = ereal r" 

1347 
using emeasure_finite[of A] emeasure_nonneg[of M A] by (cases "emeasure M A") auto 

1348 

1349 
lemma (in finite_measure) bounded_measure: "measure M A \<le> measure M (space M)" 

1350 
using emeasure_space[of M A] emeasure_real[of A] emeasure_real[of "space M"] by (auto simp: measure_def) 

1351 

1352 
lemma (in finite_measure) finite_measure_Diff: 

1353 
assumes sets: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A" 

1354 
shows "measure M (A  B) = measure M A  measure M B" 

1355 
using measure_Diff[OF _ assms] by simp 

1356 

1357 
lemma (in finite_measure) finite_measure_Union: 

1358 
assumes sets: "A \<in> sets M" "B \<in> sets M" and "A \<inter> B = {}" 

1359 
shows "measure M (A \<union> B) = measure M A + measure M B" 
