author  hoelzl 
Wed, 10 Oct 2012 12:12:23 +0200  
changeset 49784  5e5b2da42a69 
parent 49773  16907431e477 
child 49789  e0a4cb91a8a9 
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 

11 
Sigma_Algebra 

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]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

20 

47694  21 
lemma suminf_cmult_indicator: 
22 
fixes f :: "nat \<Rightarrow> ereal" 

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

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

25 
proof  

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

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

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

29 
by (auto simp: setsum_cases) 

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

31 
proof (rule ereal_SUPI) 

32 
fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y" 

33 
from this[of "Suc i"] show "f i \<le> y" by auto 

34 
qed (insert assms, simp) 

35 
ultimately show ?thesis using assms 

36 
by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def) 

37 
qed 

38 

39 
lemma suminf_indicator: 

40 
assumes "disjoint_family A" 

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

42 
proof cases 

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

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

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

46 
show ?thesis using * by simp 

47 
qed simp 

48 

49 
text {* 

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

51 
represent sigma algebras (with an arbitrary emeasure). 

52 
*} 

53 

54 
section "Extend binary sets" 

55 

56 
lemma LIMSEQ_binaryset: 

57 
assumes f: "f {} = 0" 

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

59 
proof  

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

61 
proof 

62 
fix n 

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

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

65 
qed 

66 
moreover 

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

68 
ultimately 

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

70 
by metis 

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

72 
by simp 

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

74 
qed 

75 

76 
lemma binaryset_sums: 

77 
assumes f: "f {} = 0" 

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

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

80 

81 
lemma suminf_binaryset_eq: 

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

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

84 
by (metis binaryset_sums sums_unique) 

85 

86 
section {* Properties of a premeasure @{term \<mu>} *} 

87 

88 
text {* 

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

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

91 
*} 

92 

93 
definition additive where 

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

95 

96 
definition increasing where 

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

98 

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

99 
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

100 
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

101 

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

104 
by (auto simp add: positive_def) 

105 

106 
lemma additiveD: 

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

108 
by (auto simp add: additive_def) 

109 

110 
lemma increasingD: 

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

112 
by (auto simp add: increasing_def) 

113 

114 
lemma countably_additiveI: 

115 
"(\<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)) 

116 
\<Longrightarrow> countably_additive M f" 

117 
by (simp add: countably_additive_def) 

118 

119 
lemma (in ring_of_sets) disjointed_additive: 

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

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

122 
proof (induct n) 

123 
case (Suc n) 

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

125 
by simp 

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

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

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

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

130 
finally show ?case . 

131 
qed simp 

132 

133 
lemma (in ring_of_sets) additive_sum: 

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

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

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

137 
and disj: "disjoint_family_on A S" 

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

139 
using `finite S` disj A proof induct 

140 
case empty show ?case using f by (simp add: positive_def) 

141 
next 

142 
case (insert s S) 

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

144 
by (auto simp add: disjoint_family_on_def neq_iff) 

145 
moreover 

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

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

148 
using insert `finite S` by auto 

149 
moreover 

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

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

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

153 
by (auto simp add: additive_def subset_insertI) 

154 
qed 

155 

156 
lemma (in ring_of_sets) additive_increasing: 

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

158 
shows "increasing M f" 

159 
proof (auto simp add: increasing_def) 

160 
fix x y 

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

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

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

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

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

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

167 
also have "... = f y" 

168 
by (metis Un_Diff_cancel Un_absorb1 xy(3)) 

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

170 
qed 

171 

172 
lemma (in ring_of_sets) countably_additive_additive: 

173 
assumes posf: "positive M f" and ca: "countably_additive M f" 

174 
shows "additive M f" 

175 
proof (auto simp add: additive_def) 

176 
fix x y 

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

178 
hence "disjoint_family (binaryset x y)" 

179 
by (auto simp add: disjoint_family_on_def binaryset_def) 

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

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

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

183 
using ca 

184 
by (simp add: countably_additive_def) 

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

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

187 
by (simp add: range_binaryset_eq UN_binaryset_eq) 

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

189 
by (auto simp add: Un suminf_binaryset_eq positive_def) 

190 
qed 

191 

192 
lemma (in algebra) increasing_additive_bound: 

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

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

195 
and inc: "increasing M f" 

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

197 
and disj: "disjoint_family A" 

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

199 
proof (safe intro!: suminf_bound) 

200 
fix N 

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

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

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

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

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

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

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

208 

209 
lemma (in ring_of_sets) countably_additiveI_finite: 

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

211 
shows "countably_additive M \<mu>" 

212 
proof (rule countably_additiveI) 

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

214 

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

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

217 

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

219 
proof (rule inj_onI, simp) 

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

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

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

223 
qed 

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

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

226 

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

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

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

230 
proof (rule finite_imageD) 

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

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

233 
by (rule finite_subset) fact 

234 
qed fact 

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

236 
by (rule finite_subset) 

237 

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

239 
using disj by (auto simp: disjoint_family_on_def) 

240 

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

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

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

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

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

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

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

250 
qed 

251 

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

252 
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

253 
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

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

255 
(\<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

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

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

258 
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

259 
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

260 
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

261 
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

262 
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

263 
by (auto simp: UN_disjointed_eq disjoint_family_disjointed) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

265 
using f(1)[unfolded positive_def] dA 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

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

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

269 
unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost . 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

270 
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

271 
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

272 
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

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

274 
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

275 
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

276 
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

277 
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

278 
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

279 
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

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

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

282 
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

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

284 
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

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

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

287 
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

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

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

290 
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

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

292 

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

293 
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

294 
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

295 
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

296 
\<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

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

298 
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

299 
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

300 
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

301 
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

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

303 
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

304 
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

305 

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

306 
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

307 
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

308 

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

309 
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

310 
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

311 
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

312 
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

313 
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

314 
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

315 
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

316 
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

317 
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

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

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

320 
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

321 
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

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

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

324 
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

325 
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

326 
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

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

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

329 
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

330 
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

331 
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

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

333 
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

334 
using A(4) f_fin f_Int_fin 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

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

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

338 
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

339 
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

340 
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

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

342 
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

343 
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

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

345 
with LIMSEQ_ereal_INFI[OF decseq_fA] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

346 
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

347 
qed 
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 
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

350 
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

351 
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

352 
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

353 
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

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

355 
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

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

357 
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

358 
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

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

360 
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

361 
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

362 
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

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

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

365 
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

366 
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

367 
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

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

369 
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

370 
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

371 
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

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

373 
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

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

375 
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

376 
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

377 
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

378 
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

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

380 

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

381 
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

382 
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

383 
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

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

385 
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

386 
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

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

388 

47694  389 
section {* Properties of @{const emeasure} *} 
390 

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

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

393 

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

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

396 

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

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

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

400 

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

402 
using emeasure_nonneg[of M A] by auto 

403 

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

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

406 

407 
lemma suminf_emeasure: 

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

409 
using countable_UN[of A UNIV M] emeasure_countably_additive[of M] 

410 
by (simp add: countably_additive_def) 

411 

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

413 
by (metis countably_additive_additive emeasure_positive emeasure_countably_additive) 

414 

415 
lemma plus_emeasure: 

416 
"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)" 

417 
using additiveD[OF emeasure_additive] .. 

418 

419 
lemma setsum_emeasure: 

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

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

422 
by (metis additive_sum emeasure_positive emeasure_additive) 

423 

424 
lemma emeasure_mono: 

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

426 
by (metis additive_increasing emeasure_additive emeasure_nonneg emeasure_notin_sets 

427 
emeasure_positive increasingD) 

428 

429 
lemma emeasure_space: 

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

431 
by (metis emeasure_mono emeasure_nonneg emeasure_notin_sets sets_into_space top) 

432 

433 
lemma emeasure_compl: 

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

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

436 
proof  

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

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

439 
by (metis Un_Diff_cancel Un_absorb1 s sets_into_space) 

440 
also have "... = emeasure M s + emeasure M (space M  s)" 

441 
by (rule plus_emeasure[symmetric]) (auto simp add: s) 

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

443 
then show ?thesis 

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

445 
unfolding ereal_eq_minus_iff by (auto simp: ac_simps) 

446 
qed 

447 

448 
lemma emeasure_Diff: 

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

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

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

452 
proof  

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

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

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

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

457 
using measurable by (subst plus_emeasure[symmetric]) auto 

458 
finally show "emeasure M (A  B) = emeasure M A  emeasure M B" 

459 
unfolding ereal_eq_minus_iff 

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

461 
qed 

462 

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

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

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

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

466 
by (auto simp add: countably_additive_iff_continuous_from_below emeasure_positive emeasure_additive) 
47694  467 

468 
lemma incseq_emeasure: 

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

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

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

472 

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

473 
lemma SUP_emeasure_incseq: 
47694  474 
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

475 
shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

476 
using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A] 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

477 
by (simp add: LIMSEQ_unique) 
47694  478 

479 
lemma decseq_emeasure: 

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

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

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

483 

484 
lemma INF_emeasure_decseq: 

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

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

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

488 
proof  

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

490 
using A by (auto intro!: emeasure_mono) 

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

492 

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

494 

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

496 
by (simp add: ereal_SUPR_uminus minus_ereal_def) 

497 
also have "\<dots> = (SUP n. emeasure M (A 0)  emeasure M (A n))" 

498 
unfolding minus_ereal_def using A0 assms 

499 
by (subst SUPR_ereal_add) (auto simp add: decseq_emeasure) 

500 
also have "\<dots> = (SUP n. emeasure M (A 0  A n))" 

501 
using A finite `decseq A`[unfolded decseq_def] by (subst emeasure_Diff) auto 

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

503 
proof (rule SUP_emeasure_incseq) 

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

505 
using A by auto 

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

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

508 
qed 

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

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

511 
finally show ?thesis 

512 
unfolding ereal_minus_eq_minus_iff using finite A0 by auto 

513 
qed 

514 

515 
lemma Lim_emeasure_decseq: 

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

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

518 
using LIMSEQ_ereal_INFI[OF decseq_emeasure, OF A] 

519 
using INF_emeasure_decseq[OF A fin] by simp 

520 

521 
lemma emeasure_subadditive: 

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

523 
shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B" 

524 
proof  

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

526 
have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B  A)" 

527 
using assms by (simp add: Diff) 

528 
also have "\<dots> \<le> emeasure M A + emeasure M B" 

529 
using assms by (auto intro!: add_left_mono emeasure_mono) 

530 
finally show ?thesis . 

531 
qed 

532 

533 
lemma emeasure_subadditive_finite: 

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

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

536 
using assms proof induct 

537 
case (insert i I) 

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

539 
by simp 

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

541 
using insert by (intro emeasure_subadditive finite_UN) auto 

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

543 
using insert by (intro add_mono) auto 

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

545 
using insert by auto 

546 
finally show ?case . 

547 
qed simp 

548 

549 
lemma emeasure_subadditive_countably: 

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

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

552 
proof  

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

554 
unfolding UN_disjointed_eq .. 

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

556 
using range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"] 

557 
by (simp add: disjoint_family_disjointed comp_def) 

558 
also have "\<dots> \<le> (\<Sum>i. emeasure M (f i))" 

559 
using range_disjointed_sets[OF assms] assms 

560 
by (auto intro!: suminf_le_pos emeasure_mono disjointed_subset) 

561 
finally show ?thesis . 

562 
qed 

563 

564 
lemma emeasure_insert: 

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

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

567 
proof  

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

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

570 
qed 

571 

572 
lemma emeasure_eq_setsum_singleton: 

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

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

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

576 
by (auto simp: disjoint_family_on_def subset_eq) 

577 

578 
lemma setsum_emeasure_cover: 

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

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

581 
assumes disj: "disjoint_family_on B S" 

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

583 
proof  

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

585 
proof (rule setsum_emeasure) 

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

587 
using `disjoint_family_on B S` 

588 
unfolding disjoint_family_on_def by auto 

589 
qed (insert assms, auto) 

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

591 
using A by auto 

592 
finally show ?thesis by simp 

593 
qed 

594 

595 
lemma emeasure_eq_0: 

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

597 
by (metis emeasure_mono emeasure_nonneg order_eq_iff) 

598 

599 
lemma emeasure_UN_eq_0: 

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

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

602 
proof  

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

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

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

606 
ultimately show ?thesis by simp 

607 
qed 

608 

609 
lemma measure_eqI_finite: 

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

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

612 
shows "M = N" 

613 
proof (rule measure_eqI) 

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

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

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

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

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

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

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

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

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

623 
qed simp 

624 

625 
lemma measure_eqI_generator_eq: 

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

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

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

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

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

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

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

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

634 
let ?\<mu> = "emeasure M" and ?\<nu> = "emeasure N" 
47694  635 
interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

636 
{ fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>" 
47694  637 
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

638 
let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

639 
have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

640 
interpret D: dynkin_system \<Omega> ?D 
47694  641 
proof (rule dynkin_systemI, simp_all) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

642 
fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)" 
47694  643 
then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto 
644 
next 

645 
have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto 

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

646 
then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)" 
47694  647 
using `F \<in> E` eq by (auto intro: sigma_sets_top) 
648 
next 

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

649 
fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)" 
47694  650 
then have **: "F \<inter> (\<Omega>  A) = F  (F \<inter> A)" 
651 
and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E" 

652 
using `F \<in> E` S.sets_into_space by auto 

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

653 
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

654 
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

655 
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

656 
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

657 
then have "?\<mu> (F \<inter> (\<Omega>  A)) = ?\<mu> F  ?\<mu> (F \<inter> A)" unfolding ** 
47694  658 
using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

660 
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

661 
using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>` 
47694  662 
by (auto intro!: emeasure_Diff[symmetric] simp: M N) 
49773
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

663 
finally show "\<Omega>  A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega>  A)) = ?\<nu> (F \<inter> (\<Omega>  A))" 
47694  664 
using * by auto 
665 
next 

666 
fix A :: "nat \<Rightarrow> 'a set" 

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

667 
assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

668 
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

669 
by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

670 
with A show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Union>x. A x)) = ?\<nu> (F \<inter> (\<Union>x. A x))" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

673 
have *: "sigma_sets \<Omega> E = ?D" 
47694  674 
using `F \<in> E` `Int_stable E` 
675 
by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq) 

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

676 
have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

677 
unfolding M by (subst (asm) *) auto } 
47694  678 
note * = this 
679 
show "M = N" 

680 
proof (rule measure_eqI) 

681 
show "sets M = sets N" 

682 
using M N by simp 

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

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

684 
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

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

686 
let ?D = "disjointed (\<lambda>i. F \<inter> A i)" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

687 
have "space M = \<Omega>" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

688 
using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

689 
then have F_eq: "F = (\<Union>i. ?D i)" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

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

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

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

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

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

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

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

697 
{ fix i 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

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

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

700 
then have "emeasure M (?D i) = emeasure N (?D i)" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

701 
using *[of "A i" "?D i", OF _ A(3)] A(1) by auto } 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

702 
ultimately show "emeasure M F = emeasure N F" 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

703 
using N M 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

704 
apply (subst (1 2) F_eq) 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

705 
apply (subst (1 2) suminf_emeasure[symmetric]) 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

706 
apply auto 
5e5b2da42a69
remove incseq assumption from measure_eqI_generator_eq
hoelzl
parents:
49773
diff
changeset

707 
done 
47694  708 
qed 
709 
qed 

710 

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

712 
proof (intro measure_eqI emeasure_measure_of_sigma) 

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

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

715 
by (simp add: positive_def emeasure_nonneg) 

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

717 
by (simp add: emeasure_countably_additive) 

718 
qed simp_all 

719 

720 
section "@{text \<mu>}null sets" 

721 

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

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

724 

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

726 
by (simp add: null_sets_def) 

727 

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

729 
unfolding null_sets_def by simp 

730 

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

732 
unfolding null_sets_def by simp 

733 

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

47762  735 
proof (rule ring_of_setsI) 
47694  736 
show "null_sets M \<subseteq> Pow (space M)" 
737 
using sets_into_space by auto 

738 
show "{} \<in> null_sets M" 

739 
by auto 

740 
fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M" 

741 
then have "A \<in> sets M" "B \<in> sets M" 

742 
by auto 

743 
moreover then have "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B" 

744 
"emeasure M (A  B) \<le> emeasure M A" 

745 
by (auto intro!: emeasure_subadditive emeasure_mono) 

746 
moreover have "emeasure M B = 0" "emeasure M A = 0" 

747 
using sets by auto 

748 
ultimately show "A  B \<in> null_sets M" "A \<union> B \<in> null_sets M" 

749 
by (auto intro!: antisym) 

750 
qed 

751 

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

753 
proof  

754 
have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)" 

755 
unfolding SUP_def image_compose 

756 
unfolding surj_from_nat .. 

757 
then show ?thesis by simp 

758 
qed 

759 

760 
lemma null_sets_UN[intro]: 

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

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

763 
proof (intro conjI CollectI null_setsI) 

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

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

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

767 
unfolding UN_from_nat[of N] 

768 
using assms by (intro emeasure_subadditive_countably) auto 

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

770 
using assms by (auto simp: null_setsD1) 

771 
qed 

772 

773 
lemma null_set_Int1: 

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

775 
proof (intro CollectI conjI null_setsI) 

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

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

778 
qed (insert assms, auto) 

779 

780 
lemma null_set_Int2: 

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

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

783 

784 
lemma emeasure_Diff_null_set: 

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

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

787 
proof  

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

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

790 
then show ?thesis 

791 
unfolding * using assms 

792 
by (subst emeasure_Diff) auto 

793 
qed 

794 

795 
lemma null_set_Diff: 

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

797 
proof (intro CollectI conjI null_setsI) 

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

799 
qed (insert assms, auto) 

800 

801 
lemma emeasure_Un_null_set: 

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

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

804 
proof  

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

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

807 
then show ?thesis 

808 
unfolding * using assms 

809 
by (subst plus_emeasure[symmetric]) auto 

810 
qed 

811 

812 
section "Formalize almost everywhere" 

813 

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

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

816 

817 
abbreviation 

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

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

820 

821 
syntax 

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

823 

824 
translations 

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

826 

827 
lemma eventually_ae_filter: 

828 
fixes M P 

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

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

831 
unfolding ae_filter_def F_def[symmetric] 

832 
proof (rule eventually_Abs_filter) 

833 
show "is_filter F" 

834 
proof 

835 
fix P Q assume "F P" "F Q" 

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

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

838 
by auto 

839 
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 

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

841 
next 

842 
fix P Q assume "F P" 

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

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

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

846 
then show "F Q" by auto 

847 
qed auto 

848 
qed 

849 

850 
lemma AE_I': 

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

852 
unfolding eventually_ae_filter by auto 

853 

854 
lemma AE_iff_null: 

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

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

857 
proof 

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

859 
unfolding eventually_ae_filter by auto 

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

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

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

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

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

865 
next 

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

867 
qed 

868 

869 
lemma AE_iff_null_sets: 

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

871 
using Int_absorb1[OF sets_into_space, of N M] 

872 
by (subst AE_iff_null) (auto simp: Int_def[symmetric]) 

873 

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

876 
by (metis AE_iff_null_sets null_setsD2) 

877 

47694  878 
lemma AE_iff_measurable: 
879 
"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" 

880 
using AE_iff_null[of _ P] by auto 

881 

882 
lemma AE_E[consumes 1]: 

883 
assumes "AE x in M. P x" 

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

885 
using assms unfolding eventually_ae_filter by auto 

886 

887 
lemma AE_E2: 

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

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

890 
proof  

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

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

893 
qed 

894 

895 
lemma AE_I: 

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

897 
shows "AE x in M. P x" 

898 
using assms unfolding eventually_ae_filter by auto 

899 

900 
lemma AE_mp[elim!]: 

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

902 
shows "AE x in M. Q x" 

903 
proof  

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

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

906 
by (auto elim!: AE_E) 

907 

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

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

910 
by (auto elim!: AE_E) 

911 

912 
show ?thesis 

913 
proof (intro AE_I) 

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

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

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

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

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

919 
using P imp by auto 

920 
qed 

921 
qed 

922 

923 
(* depricated replace by laws about eventually *) 

924 
lemma 

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

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

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

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

929 
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)" 

930 
by auto 

931 

932 
lemma AE_impI: 

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

934 
by (cases P) auto 

935 

936 
lemma AE_measure: 

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

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

939 
proof  

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

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

942 
by (intro emeasure_mono) auto 

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

944 
using sets N by (intro emeasure_subadditive) auto 

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

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

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

948 
qed 

949 

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

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

952 

953 
lemma AE_I2[simp, intro]: 

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

955 
using AE_space by force 

956 

957 
lemma AE_Ball_mp: 

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

959 
by auto 

960 

961 
lemma AE_cong[cong]: 

962 
"(\<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)" 

963 
by auto 

964 

965 
lemma AE_all_countable: 

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

967 
proof 

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

969 
from this[unfolded eventually_ae_filter Bex_def, THEN choice] 

970 
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 

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

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

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

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

975 
by (intro null_sets_UN) auto 

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

977 
unfolding eventually_ae_filter by auto 

978 
qed auto 

979 

980 
lemma AE_finite_all: 

981 
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)" 

982 
using f by induct auto 

983 

984 
lemma AE_finite_allI: 

985 
assumes "finite S" 

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

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

988 

989 
lemma emeasure_mono_AE: 

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

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

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

993 
proof cases 

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

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

996 
by (auto simp: eventually_ae_filter) 

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

998 
using N A by (subst emeasure_Diff_null_set) auto 

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

1000 
using N A B sets_into_space by (auto intro!: emeasure_mono) 

1001 
also have "emeasure M (B  N) = emeasure M B" 

1002 
using N B by (subst emeasure_Diff_null_set) auto 

1003 
finally show ?thesis . 

1004 
qed (simp add: emeasure_nonneg emeasure_notin_sets) 

1005 

1006 
lemma emeasure_eq_AE: 

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

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

1009 
shows "emeasure M A = emeasure M B" 

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

1011 

1012 
section {* @{text \<sigma>}finite Measures *} 

1013 

1014 
locale sigma_finite_measure = 

1015 
fixes M :: "'a measure" 

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

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

1018 

1019 
lemma (in sigma_finite_measure) sigma_finite_disjoint: 

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

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

1022 
proof atomize_elim 

1023 
case goal1 

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

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

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

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

1028 
using sigma_finite by auto 

1029 
note range' = range_disjointed_sets[OF range] range 

1030 
{ fix i 

1031 
have "emeasure M (disjointed A i) \<le> emeasure M (A i)" 

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

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

1034 
using measure[of i] by auto } 

1035 
with disjoint_family_disjointed UN_disjointed_eq[of A] space range' 

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

1037 
qed 

1038 

1039 
lemma (in sigma_finite_measure) sigma_finite_incseq: 

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

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

1042 
proof atomize_elim 

1043 
case goal1 

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

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

1046 
using sigma_finite by auto 

1047 
then show ?case 

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

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

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

1051 
using F by fastforce 

1052 
next 

1053 
fix n 

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

1055 
by (auto intro!: emeasure_subadditive_finite) 

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

1057 
using F by (auto simp: setsum_Pinfty) 

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

1059 
qed (force simp: incseq_def)+ 

1060 
qed 

1061 

1062 
section {* Measure space induced by distribution of @{const measurable}functions *} 

1063 

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

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

1066 

1067 
lemma 

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

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

1070 
by (auto simp: distr_def) 

1071 

1072 
lemma 

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

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

1075 
by (auto simp: measurable_def) 

1076 

1077 
lemma emeasure_distr: 

1078 
fixes f :: "'a \<Rightarrow> 'b" 

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

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

1081 
unfolding distr_def 

1082 
proof (rule emeasure_measure_of_sigma) 

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

1084 
by (auto simp: positive_def) 

1085 

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

1087 
proof (intro countably_additiveI) 

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

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

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

1091 
using f by (auto simp: measurable_def) 

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

1093 
using * by blast 

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

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

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

1097 
using suminf_emeasure[OF _ **] A f 

1098 
by (auto simp: comp_def vimage_UN) 

1099 
qed 

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

1101 
qed fact 

1102 

1103 
lemma AE_distrD: 

1104 
assumes f: "f \<in> measurable M M'" 

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

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

1107 
proof  

1108 
from AE[THEN AE_E] guess N . 

1109 
with f show ?thesis 

1110 
unfolding eventually_ae_filter 

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

1112 
(auto simp: emeasure_distr measurable_def) 

1113 
qed 

1114 

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

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

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

1117 
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

1118 
proof (subst (1 2) AE_iff_measurable[OF _ refl]) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

1120 
by (auto intro!: sets_Collect_neg) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

1122 
have "f ` {x \<in> space N. P x} \<inter> space M = {x \<in> space M. P (f x)}" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1123 
using f by (auto dest: measurable_space) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1124 
then show "{x \<in> space M. \<not> P (f x)} \<in> sets M" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1125 
using measurable_sets[OF f P] by (auto intro!: sets_Collect_neg) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1126 
moreover have "f ` {x\<in>space N. \<not> P x} \<inter> space M = {x \<in> space M. \<not> P (f x)}" 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

1127 
using f by (auto dest: measurable_space) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

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

1130 
using f by (simp add: emeasure_distr) 
16907431e477
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
hoelzl
parents:
47762
diff
changeset

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

1132 

47694  1133 
lemma null_sets_distr_iff: 
1134 
"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" 

1135 
by (auto simp add: null_sets_def emeasure_distr measurable_sets) 

1136 

1137 
lemma distr_distr: 

1138 
assumes f: "g \<in> measurable N L" and g: "f \<in> measurable M N" 

1139 
shows "distr (distr M N f) L g = distr M L (g \<circ> f)" (is "?L = ?R") 

1140 
using measurable_comp[OF g f] f g 

1141 
by (auto simp add: emeasure_distr measurable_sets measurable_space 

1142 
intro!: arg_cong[where f="emeasure M"] measure_eqI) 

1143 

1144 
section {* Real measure values *} 

1145 

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

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

1148 

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

1150 
unfolding measure_def by simp 

1151 

1152 
lemma emeasure_eq_ereal_measure: 

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

1154 
using emeasure_nonneg[of M A] 

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

1156 

1157 
lemma measure_Union: 

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

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

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

1161 
unfolding measure_def 

1162 
using plus_emeasure[OF measurable, symmetric] finite 

1163 
by (simp add: emeasure_eq_ereal_measure) 

1164 

1165 
lemma measure_finite_Union: 

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

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

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

1169 
unfolding measure_def 

1170 
using setsum_emeasure[OF measurable, symmetric] finite 

1171 
by (simp add: emeasure_eq_ereal_measure) 

1172 

1173 
lemma measure_Diff: 

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

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

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

1177 
proof  

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

1179 
using measurable by (auto intro!: emeasure_mono) 

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

1181 
using measurable finite by (rule_tac measure_Union) auto 

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

1183 
qed 

1184 

1185 
lemma measure_UNION: 

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

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

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

1189 
proof  

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

1191 
suminf_emeasure[OF measurable] emeasure_nonneg[of M] 

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

1193 
moreover 

1194 
{ fix i 

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

1196 
using measurable by (auto intro!: emeasure_mono) 

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

1198 
using finite by (intro emeasure_eq_ereal_measure) auto } 

1199 
ultimately show ?thesis using finite 

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

1201 
qed 

1202 

1203 
lemma measure_subadditive: 

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

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

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

1207 
proof  

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

1209 
using emeasure_subadditive[OF measurable] fin by auto 

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

1211 
using emeasure_subadditive[OF measurable] fin 

1212 
by (auto simp: emeasure_eq_ereal_measure) 

1213 
qed 

1214 

1215 
lemma measure_subadditive_finite: 

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

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

1218 
proof  

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

1220 
using emeasure_subadditive_finite[OF A] . 

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

1222 
using fin by (simp add: setsum_Pinfty) 

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

1224 
then show ?thesis 

1225 
using emeasure_subadditive_finite[OF A] fin 

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

1227 
qed 

1228 

1229 
lemma measure_subadditive_countably: 

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

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

1232 
proof  

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

1234 
moreover 

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

1236 
using emeasure_subadditive_countably[OF A] . 

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

1238 
using fin by simp 

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

1240 
ultimately show ?thesis 

1241 
using emeasure_subadditive_countably[OF A] fin 

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

1243 
qed 

1244 

1245 
lemma measure_eq_setsum_singleton: 

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

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

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

1249 
unfolding measure_def 

1250 
using emeasure_eq_setsum_singleton[OF S] fin 

1251 
by simp (simp add: emeasure_eq_ereal_measure) 

1252 

1253 
lemma Lim_measure_incseq: 

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

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

1256 
proof  

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

1258 
using fin by (auto simp: emeasure_eq_ereal_measure) 

1259 
then show ?thesis 

1260 
using Lim_emeasure_incseq[OF A] 

1261 
unfolding measure_def 

1262 
by (intro lim_real_of_ereal) simp 

1263 
qed 

1264 

1265 
lemma Lim_measure_decseq: 

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

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

1268 
proof  

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

1270 
using A by (auto intro!: emeasure_mono) 

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

1272 
using fin[of 0] by auto 

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

1274 
by (auto simp: emeasure_eq_ereal_measure) 

1275 
then show ?thesis 

1276 
unfolding measure_def 

1277 
using Lim_emeasure_decseq[OF A fin] 

1278 
by (intro lim_real_of_ereal) simp 

1279 
qed 

1280 

1281 
section {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *} 

1282 

1283 
locale finite_measure = sigma_finite_measure M for M + 

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

1285 

1286 
lemma finite_measureI[Pure.intro!]: 

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

1288 
shows "finite_measure M" 

1289 
proof 

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

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

1292 
qed fact 

1293 

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

1295 
using finite_emeasure_space emeasure_space[of M A] by auto 

1296 

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

1298 
unfolding measure_def by (simp add: emeasure_eq_ereal_measure) 

1299 

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

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

1302 

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

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

1305 

1306 
lemma (in finite_measure) finite_measure_Diff: 

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

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

1309 
using measure_Diff[OF _ assms] by simp 

1310 

1311 
lemma (in finite_measure) finite_measure_Union: 

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

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

1314 
using measure_Union[OF _ _ assms] by simp 

1315 

1316 
lemma (in finite_measure) finite_measure_finite_Union: 

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

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

1319 
using measure_finite_Union[OF assms] by simp 

1320 

1321 
lemma (in finite_measure) finite_measure_UNION: 

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

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

1324 
using measure_UNION[OF A] by simp 

1325 

1326 
lemma (in finite_measure) finite_measure_mono: 

1327 
assumes "A \<subseteq> B" "B \<in> sets M" shows "measure M A \<le> measure M B" 

1328 
using emeasure_mono[OF assms] emeasure_real[of A] emeasure_real[of B] by (auto simp: measure_def) 

1329 

1330 
lemma (in finite_measure) finite_measure_subadditive: 

1331 
assumes m: "A \<in> sets M" "B \<in> sets M" 

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

1333 
using measure_subadditive[OF m] by simp 

1334 

1335 
lemma (in finite_measure) finite_measure_subadditive_finite: 

1336 
assumes "finite I" "A`I \<subseteq> sets M" shows "measure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. measure M (A i))" 

1337 
using measure_subadditive_finite[OF assms] by simp 

1338 

1339 
lemma (in finite_measure) finite_measure_subadditive_countably: 

1340 
assumes A: "range A \<subseteq> sets M" and sum: "summable (\<lambda>i. measure M (A i))" 

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

1342 
proof  

1343 
from `summable (\<lambda>i. measure M (A i))` 

1344 
have "(\<lambda>i. ereal (measure M (A i))) sums ereal (\<Sum>i. measure M (A i))" 

1345 
by (simp add: sums_ereal) (rule summable_sums) 

1346 
from sums_unique[OF this, symmetric] 

1347 
measure_subadditive_countably[OF A] 

1348 
show ?thesis by (simp add: emeasure_eq_measure) 

1349 
qed 

1350 

1351 
lemma (in finite_measure) finite_measure_eq_setsum_singleton: 

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

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

1354 
using measure_eq_setsum_singleton[OF assms] by simp 

1355 

1356 
lemma (in finite_measure) finite_Lim_measure_incseq: 

1357 
assumes A: "range A \<subseteq> sets M" "incseq A" 

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

1359 
using Lim_measure_incseq[OF A] by simp 

1360 

1361 
lemma (in finite_measure) finite_Lim_measure_decseq: 

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

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

1364 
using Lim_measure_decseq[OF A] by simp 

1365 

1366 
lemma (in finite_measure) finite_measure_compl: 

1367 
assumes S: "S \<in> sets M" 

1368 
shows "measure M (space M  S) = measure M (space M)  measure M S" 

1369 
using measure_Diff[OF _ top S sets_into_space] S by simp 

1370 

1371 
lemma (in finite_measure) finite_measure_mono_AE: 

1372 
assumes imp: "AE x in M. x \<in> A \<longrightarrow> x \<in> B" and B: "B \<in> sets M" 

1373 
shows "measure M A \<le> measure M B" 

1374 
using assms emeasure_mono_AE[OF imp B] 

1375 
by (simp add: emeasure_eq_measure) 

1376 

1377 
lemma (in finite_measure) finite_measure_eq_AE: 

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

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

1380 
shows "measure M A = measure M B" 

1381 
using assms emeasure_eq_AE[OF assms] by (simp add: emeasure_eq_measure) 

1382 

1383 
section {* Counting space *} 

1384 

1385 
definition count_space :: "'a set \<Rightarrow> 'a measure" where 

1386 
"count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)" 

1387 

1388 
lemma 

1389 
shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>" 

1390 
and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>" 

1391 
using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>] 

05663f75964c
reworked Probability theory
h 